closedunderclosedunder pair(xs,xf) != p2, then xs (regarded as a set {x : (xs x = p1)}) is closed under xf (regarded as a function).list(usable). a(closedunder,pair(xs,xf)) = p2 | a(xs,x) != p1 | a(xs,a(xf,x)) = p1. end_of_list.
Proof of defining property of closedunder | OTTER output file
The above proof, obtained without human intervention, is a bit long, so I include the proof below, which used the interactive_given option of OTTER to let me select given clauses manually.
Manual Proof | OTTER output file
The following clause says that if closedunder pair(xs,xf) != p1, then xs (regarded as a set {x : (xs x = p1)}) fails to be closed under xf (regarded as a function).
list(usable). a(closedunder,pair(xs,xf)) = p1 | a(xs,notclosed(xs,xf)) = p1. a(closedunder,pair(xs,xf)) = p1 | a(xs,a(xf,notclosed(xs,xf))) != p1. end_of_list.
notclosed(xs,xf), I could take the answer literal returned in the following proof and replace bad with x throughout. However, the resulting term seemed a bit long, so I opted for using a new Skolem function in stating the result.Proof of converse defining property of closedunder | OTTER output file
up | previous | next | detailed contents | brief contents