spec SimpleRawTreeWithOp =

sorts Nat free with 0 | succ(Nat);

Tree free with empty | node(Tree; Nat; Tree)

ops empty : Tree;

node : Tree * Nat * Tree -> Tree;

num : Nat -> Nat;

fun sum(t:Tree):Nat =

let fun plus(x:Nat; n:Nat):Nat =

case x of 0 => n | succ(m) => succ(plus(m,n))

in case t of empty => 0

| node(t1,n,t2) => plus(plus(num(n),sum(t1)), sum(t2));

fun eq (t1: Tree; t2 : Tree) : Bool =

if t1 = t2 then true else false;

fun snd (t1: Tree; t2 : Tree) : Tree = case eq(t1, t2) of

true => t1 | false => t2

. forall t1: Tree; t2 : Tree . eq(t1, t2) = true