Proof of a(charq,xf) = p2 | a(a(xf,x),pair(p1,p2)) = a(xf,x).

-----> EMPTY CLAUSE at   1.56 sec ----> 606 [back_demod,556,demod,595,2,7,595,unit_del,65,65] $F.

Length of proof is 7.  Level of proof is 3.

Proof

2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
7 [reference] eq pair(x,x)=p1.
8 [reference] x=x.
16 [reference] x=y|eq pair(x,y) =p2.
18 [reference] p1!=p2.
32 [reference] charq xf=p2|xf x =p1|xf x =p2.
45 [assumption to refute] charq badf!=p2.
46 [assumption to refute] badf badx pair(p1,p2)!=badf badx.
56 [para_into,45.1.1,32.2.1,unit_del,45,flip.1] p2!=p1|charq charq =p2.
64 [para_from,56.2.2,18.1.2,flip.1] charq charq!=p1|p2!=p1.
65 [para_into,64.1.1,56.2.1] p2!=p1.
76 [ur,46,16] eq pair(badf badx pair(p1,p2),badf badx)=p2.
78 [para_into,46.1.1.1,32.3.1,demod,3,unit_del,45,flip.1] badf badx!=p2|badf badx =p1.
556 [para_into,76.1.1.2.2,32.2.1,unit_del,45] eq pair(badf badx pair(p1,p2),p1)=p2|badf badx =p2.
595,594 [para_into,78.1.1,32.3.1,unit_del,8,45] badf badx=p1.
606 [back_demod,556,demod,595,2,7,595,unit_del,65,65] $F.