Module Arr
module Arr: sig end
Reducing patterns of the form select(update(a,i,x), j)
according to the equations
select(create(a), j) = a
i = j => select(update(a,i,x), j) = x
i <> j => select(update(a,i,x),j) = select(a,j)
val create : Sym.t
val update : Sym.t
val select : Sym.t
val mk_create : Term.t -> Term.t
Reducing patterns of the form select(update(a,i,x), j)
according to the equations
select(create(a), j) = a
i = j => select(update(a,i,x), j) = x
i <> j => select(update(a,i,x),j) = select(a,j)
val mk_select : (Term.t -> Term.t -> Three.t) -> Term.t -> Term.t -> Term.t
val mk_update : (Term.t -> Term.t -> Three.t) -> Term.t -> Term.t -> Term.t -> Term.t
val sigma : (Term.t -> Term.t -> Three.t) -> Sym.arrays -> Term.t list -> Term.t
val map : (Term.t -> Term.t -> Three.t) -> (Term.t -> Term.t) -> Term.t -> Term.t