The closure is the smallest such set.

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 show outline