The term closure x is a characteristic function.

list(usable).
a(a(closure,x),y) = p1 | a(a(closure,x),y) = p2.
end_of_list.

Proof that closure x is a characteristic function | OTTER output file

up show outline