up | previous | next | detailed contents | brief contents

Lemmas on pushset

The following clauses state that in the definition of pushset = closure pair(notp1 charq, setof), the term setof can be replaced with push.
list(usable).
a(a(closure,pair(a(notp1,charq),push)),x) = p2| a(a(closure,pair(a(notp1,charq),setof)),x) = p1.
end_of_list.

Proof of pushset Lemma 1 | OTTER output file


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

Proof of pushset Lemma 2 | OTTER output file


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

Proof of pushset Lemma 3 | OTTER output file


up | previous | next | detailed contents | brief contents