let x, y, z be Element of BOOLEAN ; :: thesis: inv1 . <*(xor2c . <*(xor2b . <*x,y*>),z*>)*> = xor2 . <*(xor2 . <*x,y*>),z*>
thus inv1 . <*(xor2c . <*(xor2b . <*x,y*>),z*>)*> = inv1 . <*(xor2c . <*(('not' x) 'xor' ('not' y)),z*>)*> by TWOSCOMP:def 15
.= inv1 . <*((('not' x) 'xor' ('not' y)) 'xor' ('not' z))*> by Def4
.= 'not' ((('not' x) 'xor' ('not' y)) 'xor' ('not' z)) by Def1
.= (x 'xor' y) 'xor' z by XBOOLEAN:74
.= xor2 . <*(x 'xor' y),z*> by FACIRC_1:def 4
.= xor2 . <*(xor2 . <*x,y*>),z*> by FACIRC_1:def 4 ; :: thesis: verum