Basic defining properties of isp1

list(usable).
a(x,y) != p1 | a(a(isp1,x),y) = p1.
end_of_list.

Proof of a(x,y) != p1 | a(a(isp1,x),y) = p1. | OTTER output file

The following clause says that if x y != p1 then isp1 x y = p2.

list(usable).
a(x,y) = p1 | a(a(isp1,x),y) = p2.
end_of_list.

Proof of a(x,y) = p1 | a(a(isp1,x),y) = p2. | OTTER output file

up | previous | next | detailed contents | brief contents