kintersection takes a set of sets, and returns a constant function whose value is the intersection.
The following clause says that if kintersection f y x != p2 then for every z such that f z = p1, we have z x = p1. The variable y is present only for purposes of stratification, so that f is two levels higher than x.
list(usable). a(a(a(kintersection,xf),y),x) = p2 | a(xf,z) != p1 | a(z,x) = p1. end_of_list. list(usable). % trivial corollary. choice of eq is arbitrary a(a(a(kintersection,xf),eq),x) = p2 | a(xf,z) != p1 | a(z,x) = p1. % (not used in later proofs) end_of_list.
y with the value eq. The choice of eq is totally arbitrary. The proof of the second statement is not included here, but if you code its negation, OTTER will of course detect the contradiction with the first statement immediately. I added the second version because when OTTER'S weights are set to discard all variables, OTTER will never use the first clause in the right-to-left direction.Proof of defining property for kintersecton | OTTER output file
list(usable). a(a(a(kintersection,xf),y),x) = p1 | a(xf,notinint(xf,x)) = p1. a(a(a(kintersection,xf),y),x) = p1 | a(notinint(xf,x),x) != p1. end_of_list.
list(usable). a(a(a(kintersection,xf),eq),x) = p1 | a(xf,notinint(xf,x)) = p1. % (not used in later proofs) a(a(a(kintersection,xf),eq),x) = p1 | a(notinint(xf,x),x) != p1. % (not used in later proofs) end_of_list.
para_ones_rule, specialized for the study of combinatory logic. Again, I proved the first pair of clauses above using OTTER. The second pair are obtained from the first by instantiating y with the (arbitrarily chosen) constant eq.Proof of converse defining property for kintersecton | OTTER output file
up | previous | next | detailed contents | brief contents