Basic defining properties of remove_singleton

If x is a member of xset and x != x1 then remove_singleton pair(xset, k(x1)) x = p1.

list(usable).
a(xset,x) != p1 | x = x1 | a(a(remove_singleton,pair(xset,k(x1))),x) = p1.
end_of_list.

Proof of basic defining property of remove_singleton | OTTER output file

The set remove_singleton pair(xset, y) is a subset of xset.

list(usable).
a(xset,x) = p1 | a(a(remove_singleton,pair(xset,y)),x) = p2.
end_of_list.

Proof that the set remove_singleton pair(xset, y) is a subset of xset | OTTER output file

Finally, x is never an element of remove_singleton pair(xset, k(x)).

list(usable).
a(a(remove_singleton,pair(xset,k(x))),x) = p2.
end_of_list.

Proof of remove_singleton pair(xset,k(x)) x = p2. | OTTER output file

up | previous | next | detailed contents | brief contents