x is a superset of s and is closed under f then closure pair(s, f) is a subset of x.list(usable). a(closedunder,pair(x,xf)) = p2 | a(subset,pair(xs,x)) = p2 | a(subset,pair(a(closure,pair(xs,xf)),x)) = p1. end_of_list.
Proof that closure pair(s, f) is the smallest such set | OTTER output file