Piecewise characterization of push

list(usable).
a(a(closure,pair(a(notp1,charq),setof)),x) = p1 | a(push,x) = x.
end_of_list.

Proof of piecewise characterization of push, case 1 | OTTER output file

list(usable).
a(a(closure,pair(a(notp1,charq),setof)),x) = p2 | a(push,x) = a(setof,x).
end_of_list.

Proof of piecewise characterization of push, case 2 | OTTER output file

up | previous | next | detailed contents | brief contents