subsetsubset pair(x1,x2) = p2 or if x1 y = p1 then x2 y = p1.list(usable). a(subset,pair(x1,x2)) = p2 | a(x1,xc) != p1 | a(x2,xc) = p1. end_of_list.
Proof of defining property for subset | OTTER output file
If subset pair(x1, x2) != p1 then there is a witness c = notsub(x1, x2) such that x1 c = p1 and x2 c != p1.
list(usable). a(subset,pair(x1,x2)) = p1 | a(x1,notsub(x1,x2)) = p1. a(subset,pair(x1,x2)) = p1 | a(x2,notsub(x1,x2)) != p1. end_of_list.
Proof of converse defining property for subset | OTTER output file
up | previous | next | detailed contents | brief contents