E.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