Defining clauses for setof using pair

list(usable).
a(a(setof,xf),pair(x,a(xf,x))) = p1.
end_of_list.

Proof of a(a(setof,xf),pair(x,a(xf,x))) = p1. | OTTER output file

list(usable).
a(a(setof,xf),pair(x,y)) = p2 | a(xf,x) = y.
end_of_list.

Proof of a(a(setof,xf),pair(x,y)) = p2 | a(xf,x) = y. | OTTER output file

up | previous | next | detailed contents | brief contents