-- RELALGP2proof


Derivation of

All x y:((dom((R/\(R*C(I)))/\(C(I)*R))<=>dom((((C(I)*R)/\R)*C(I))/\R))(x,y))

Narrowing the preceding formula (33 steps) leads to 

All x z:(R(x,z) & Any z0:(R(x,z0) & z0 =/= z) ==> 
         Any z1:(Any z2:(Any z3:(x =/= z3 & R(z3,z2)) & R(x,z2) & z2 =/= z1) & 
                 R(x,z1)))

Reducts have been simplified.

Substituting z for z1 at position [0,0,0,1] of the preceding formula leads to 

All x z:(R(x,z) & Any z0:(R(x,z0) & z0 =/= z) ==> 
         Any z2:(Any z3:(x =/= z3 & R(z3,z2)) & R(x,z2) & z2 =/= z))

Reducts have been simplified.

Substituting z for z2 at position [0,0,0,1] of the preceding formula leads to 

All x z:(R(x,z) & Any z0:(R(x,z0) & z0 =/= z) ==> Any z3:(x =/= z3 & R(z3,z))) & 
All x z:(R(x,z) & Any z0:(R(x,z0) & z0 =/= z) ==> False)

Reducts have been simplified.

Substituting x for z3 at position [0,0,0,0,0] of the preceding formula leads to 

All x z:(R(x,z) & Any z0:(R(x,z0) & z0 =/= z) ==> False)

Reducts have been simplified.

Number of proof steps: 4