Alternate version of defining properties for subset, using projections instead of pairs

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

Proof of alternate defining property for subset | OTTER output file

list(usable).
a(subset,x) = p1 | a(a(p1,x),notsub(a(p1,x),a(p2,x))) = p1.
a(subset,x) = p1 | a(a(p2,x),notsub(a(p1,x),a(p2,x))) != p1.
end_of_list.

Proof of converse alternate defining property for subset | OTTER output file

up show outline