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

----> UNIT CONFLICT at   0.13 sec ----> 60 [binary,58.1,36.1] $F.

Length of proof is 2.  Level of proof is 2.

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).
16 [reference] x=y|eq pair(x,y) =p2.
32 [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,bady) !=p2.
36 [assumption to refute] badf badx!=bady.
37 [ur,35,34,demod,32,6,1,4,1,6,1,6,1,4,3,6,1,2] eq pair(bady,badf badx)!=p2.
58 [ur,37,16,flip.1] badf badx=bady.
60 [binary,58.1,36.1] $F.

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