up | previous | next | detailed contents | brief contents

(push x) is a characteristic function

The following are two different ways of saying that push is a characteristic function.
list(usable).
a(charq,a(push,x)) = p1.
end_of_list.

Proof of charq push x = p1 | OTTER output file


list(usable).
a(a(push,x),y) = p1 | a(a(push,x),y) = p2.     %    (not used in later proofs)
end_of_list.

Proof of push x y = p1 | push x y = p2 | OTTER output file


up | previous | next | detailed contents | brief contents