2.5 LIST

spec

LIST[sort Elem] =

generated type

List[Elem] ::=
empty | sort Elem | __ __(Elem; List[Elem])

pred

__is_empty : List[Elem]

vars

e : Elem; l : List[Elem]

axioms

empty is_empty;
¬ (e is_empty);
¬ (e l is_empty);
e = e empty %%  OK since e:List[Elem]

end