let x1, x2, x3, x5, x6, x7 be non pair set ; :: thesis:
set S = STC0IIStr (x1,x2,x3,x5,x6,x7);
set S1 = BitGFA0Str (x1,x2,x3);
set S2 = BitGFA0Str (x5,x6,x7);
set C = STC0IICirc (x1,x2,x3,x5,x6,x7);
set C1 = BitGFA0Circ (x1,x2,x3);
set C2 = BitGFA0Circ (x5,x6,x7);
set C1out = STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7);
set A1out = STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7);
set C2out = STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7);
set A2out = STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7);
let s be State of (STC0IICirc (x1,x2,x3,x5,x6,x7)); :: thesis:
let a1, a2, a3, a5, a6, a7 be Element of BOOLEAN ; :: thesis:
assume A1: ( a1 = s . x1 & a2 = s . x2 & a3 = s . x3 & a5 = s . x5 & a6 = s . x6 & a7 = s . x7 ) ; :: thesis:
A2: ( x1 in InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x2 in InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x3 in InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x5 in InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x6 in InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) & x7 in InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) ) by ThSTC0IIS8;
reconsider t = s as State of ((BitGFA0Circ (x1,x2,x3)) +* (BitGFA0Circ (x5,x6,x7))) ;
reconsider s1 = s | the carrier of (BitGFA0Str (x1,x2,x3)) as State of (BitGFA0Circ (x1,x2,x3)) by FACIRC_1:26;
A10: dom s1 = the carrier of (BitGFA0Str (x1,x2,x3)) by CIRCUIT1:3;
( STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7) in the carrier of (BitGFA0Str (x1,x2,x3)) & STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7) in the carrier of (BitGFA0Str (x1,x2,x3)) & InputVertices (BitGFA0Str (x1,x2,x3)) misses InnerVertices (BitGFA0Str (x5,x6,x7)) ) by GFACIRC1:36, LmSTC0IIS09a;
then A11: ( (Following (t,2)) . (STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7)) = (Following (s1,2)) . (STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7)) & (Following (t,2)) . (STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7)) = (Following (s1,2)) . (STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7)) ) by FACIRC_1:32;
A3: ( a1 = s1 . x1 & a2 = s1 . x2 & a3 = s1 . x3 ) by GFACIRC1:36, A1, A10, FUNCT_1:47;
reconsider s2 = s | the carrier of (BitGFA0Str (x5,x6,x7)) as State of (BitGFA0Circ (x5,x6,x7)) by FACIRC_1:26;
A13: dom s2 = the carrier of (BitGFA0Str (x5,x6,x7)) by CIRCUIT1:3;
( STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7) in the carrier of (BitGFA0Str (x5,x6,x7)) & STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7) in the carrier of (BitGFA0Str (x5,x6,x7)) & InnerVertices (BitGFA0Str (x1,x2,x3)) misses InputVertices (BitGFA0Str (x5,x6,x7)) ) by GFACIRC1:36, LmSTC0IIS09a;
then A14: ( (Following (t,2)) . (STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7)) = (Following (s2,2)) . (STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7)) & (Following (t,2)) . (STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7)) = (Following (s2,2)) . (STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7)) ) by FACIRC_1:33;
( a5 = s2 . x5 & a6 = s2 . x6 & a7 = s2 . x7 ) by GFACIRC1:36, A1, A13, FUNCT_1:47;
hence ( (Following (s,2)) . (STC0IICarryOutputC1 (x1,x2,x3,x5,x6,x7)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) & (Following (s,2)) . (STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7)) = ((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5) & (Following (s,2)) . (STC0IIAdderOutputA2 (x1,x2,x3,x5,x6,x7)) = (a5 'xor' a6) 'xor' a7 & (Following (s,2)) . x1 = a1 & (Following (s,2)) . x2 = a2 & (Following (s,2)) . x3 = a3 & (Following (s,2)) . x5 = a5 & (Following (s,2)) . x6 = a6 & (Following (s,2)) . x7 = a7 ) by A1, A2, CIRCCMB3:1, A3, A11, A14, GFACIRC1:39; :: thesis: