isp1 is a projection from functions to characteristic functions.push, I started by proving a set of clauses that define its basic behavior. In most cases, by extensionality, these clauses uniquely determine the combinator. That is, in most cases, the first set of clauses that I proved completely specifies the behavior of the combinator.
After proving the basic defining clauses, I tried to think of other natural, simple facts about the term, in the hope that these would come in handy for later proofs. One such clause follows. This particular clause did not prove to be crucial to the subsequent argument.
Once the basic defining clauses have been proved, I remove the demodulator that eliminates the name of the new combinator in favor of its definition. Further properties are then proved from the basic defining clauses.
list(usable). a(isp1,a(isp1,x)) = a(isp1,x). end_of_list. list(demodulators). a(isp1,a(isp1,x)) = a(isp1,x). end_of_list.
First proof of a(isp1,a(isp1,x)) = a(isp1,x). | OTTER output file
I noticed that the first proof was a bit long and that the use of the term eq in the proof seemed unecessary. I removed the axioms defining eq and ran OTTER. This time it took OTTER longer to find a proof, but when it did find the proof, it was shorter.
Second proof of a(isp1,a(isp1,x)) = a(isp1,x). | OTTER output file