bench/valid/misfix.why

   1
   2 theory Misfix
   3
   4   type t
   5
   6   function ([])   (a: t) (i: int) : int
   7   function ([<-]) (a: t) (i: int) (v: int) : t
   8
   9   axiom a1 : forall a: t, i v: int. a[i <- v][i] = v
  10   axiom a2 : forall a: t, i j v: int. i<>j -> a[i <- v][j] = a[j]
  11
  12   goal g1 : forall a: t, i j v: int. a[a[i] <- i][a[i]] = i
  13
  14 end