let x, b be non pair set ; :: thesis: for s being State of (CompCirc (x,b)) holds
( (Following s) . (CompOutput (x,b)) = xor2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
let s be State of (CompCirc (x,b)); :: thesis: ( (Following s) . (CompOutput (x,b)) = xor2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
set p = <*x,b*>;
set S = CompStr (x,b);
A1: ( dom s = the carrier of (CompStr (x,b)) & x in the carrier of (CompStr (x,b)) ) by CIRCUIT1:3, FACIRC_1:43;
A2: b in the carrier of (CompStr (x,b)) by FACIRC_1:43;
InnerVertices (CompStr (x,b)) = the carrier' of (CompStr (x,b)) by FACIRC_1:37;
hence (Following s) . (CompOutput (x,b)) = xor2a . (s * <*x,b*>) by FACIRC_1:35
.= xor2a . <*(s . x),(s . b)*> by A1, A2, FINSEQ_2:125 ;
:: thesis: ( (Following s) . x = s . x & (Following s) . b = s . b )
InputVertices (CompStr (x,b)) = {x,b} by FACIRC_1:40;
then ( x in InputVertices (CompStr (x,b)) & b in InputVertices (CompStr (x,b)) ) by TARSKI:def 2;
hence ( (Following s) . x = s . x & (Following s) . b = s . b ) by CIRCUIT2:def 5; :: thesis: verum