openr NATARR .
  op _R_ : Stack Stack -> Bool .
  var I1 I2 I : Nat .  var A1 A2 A : Arr .
  eq (s I1 || A1) R (I2 || A2) = 
     s I1 == I2 and A1[I1] == A2[I1] and (I1 || A1) R (I1 || A2) .
  eq (0 || A1) R (I || A2) = I == 0 .
  eq (I || A)  R (I || A)  = true .
close