Algebra of notp1 and isp1 under composition

list(usable).
a(notp1,a(notp1,x)) = a(isp1,x).
end_of_list.

list(demodulators).
a(notp1,a(notp1,x)) = a(isp1,x).
end_of_list.

Proof of a(notp1,a(notp1,x)) = a(isp1,x). | OTTER output file

list(usable).
a(notp1,a(isp1,x)) = a(notp1,x).
end_of_list.

list(demodulators).
a(notp1,a(isp1,x)) = a(notp1,x).
end_of_list.

Proof of a(notp1,a(isp1,x)) = a(notp1,x). | OTTER output file

list(usable).
a(isp1,a(notp1,x)) = a(notp1,x).     %    (not used in later proofs)
end_of_list.

list(demodulators).
a(isp1,a(notp1,x)) = a(notp1,x).     %    (not used in later proofs)
end_of_list.

Proof of a(isp1,a(notp1,x)) = a(notp1,x). | OTTER output file

up | previous | next | detailed contents | brief contents