push always agrees with the identity function or with setoflist(usable). a(push,x) = x | a(push,x) = a(setof,x). end_of_list.
Proof that the function push always agrees with the identity function or with setof | OTTER output file
up | previous | next | detailed contents | brief contents