kintersection defined in the next major section, I thought a series of simple lemmas might help. One of them was never used in later proofs.list(usable). a(charq,eq) = p1. end_of_list.
Proof of a(charq,eq) = p1. | OTTER output file
list(usable). a(charq,xf) = p2 | a(a(xf,x),pair(p1,p2)) = a(xf,x). % (not used in later proofs) end_of_list.
Proof of a(charq,xf) = p2 | a(a(xf,x),pair(p1,p2)) = a(xf,x). | OTTER output file
list(usable). a(a(abst,k(x)),k(y)) = k(a(x,y)). end_of_list. list(demodulators). a(a(abst,k(x)),k(y)) = k(a(x,y)). end_of_list.
Proof of a(a(abst,k(x)),k(y)) = k(a(x,y)). | OTTER output file
list(usable). pair(x1,y1) != pair(x2,y2) | x1 = x2. end_of_list.
Proof of pair(x1,y1) != pair(x2,y2) | x1 = x2. | OTTER output file
list(usable). pair(x1,y1) != pair(x2,y2) | y1 = y2. end_of_list.
Proof of pair(x1,y1) != pair(x2,y2) | y1 = y2. | OTTER output file
up | previous | next | detailed contents | brief contents