Proof of a(a(setof,xf),pair(x,a(xf,x))) = p1.

----> UNIT CONFLICT at   0.08 sec ----> 37 [binary,36.1,8.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof

1 [reference] k(x) y=x.
2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
4 [reference] pair(x,y) z=pair(x z,y z).
6 [reference] abst x y z=x k(z) (y z).
7 [reference] eq pair(x,x)=p1.
8 [reference] x=x.
33 [reference] setof=abst k(abst k(eq)) pair(k(p2),abst abst k(p1)).
34 [assumption to refute] p.
35 [assumption to refute] -p|setof badf pair(badx,badf badx) !=p1.
36 [ur,35,34,demod,33,6,1,4,1,6,1,6,1,4,3,6,1,2,7] p1!=p1.
37 [binary,36.1,8.1] $F.

up | previous | next | detailed contents | brief contents | OTTER output file