list(usable). a(closedunder,pair(x2,a(p2,x1))) = p2 | a(subset,pair(a(p1,x1),x2)) = p2 | a(subset,pair(a(closure,x1),x2)) = p1. end_of_list.
Proof that the closure is the smallest such set | OTTER output file
up | previous | next | detailed contents | brief contents