let x1, x2, x3, x4, x5, x6, x7 be non pair set ; :: thesis:
set S = STC0IStr (x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc (x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr (x1,x2,x3,x5,x6,x7);
set C1 = STC0IICirc (x1,x2,x3,x5,x6,x7);
set A1out = GFA0AdderOutput (x1,x2,x3);
set A2out = GFA0AdderOutput (x5,x6,x7);
set C1out = GFA0CarryOutput (x1,x2,x3);
set C2out = GFA0CarryOutput (x5,x6,x7);
set S2 = BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
set C2 = BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
let s be State of (STC0ICirc (x1,x2,x3,x4,x5,x6,x7)); :: thesis:
let a1, a2, a3, a4, a5, a6, a7 be Element of BOOLEAN ; :: thesis:
assume A2: ( a1 = s . x1 & a2 = s . x2 & a3 = s . x3 & a4 = s . x4 & a5 = s . x5 & a6 = s . x6 & a7 = s . x7 ) ; :: thesis:
A3: ( x1 in InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x2 in InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x3 in InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x4 in InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x5 in InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x6 in InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & x7 in InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) ) by ThSTC0IS9;
reconsider t = s as State of ((STC0IICirc (x1,x2,x3,x5,x6,x7)) +* (BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) ;
reconsider s1 = s | the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) as State of (STC0IICirc (x1,x2,x3,x5,x6,x7)) by FACIRC_1:26;
A4: dom s1 = the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) by CIRCUIT1:3;
( GFA0CarryOutput (x1,x2,x3) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0CarryOutput (x5,x6,x7) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0AdderOutput (x1,x2,x3) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & GFA0AdderOutput (x5,x6,x7) in the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) & InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) misses InnerVertices (BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) ) by ThSTC0IIS6, LmSTC0IS2b;
then A5: ( (Following (t,2)) . (GFA0CarryOutput (x1,x2,x3)) = (Following (s1,2)) . (GFA0CarryOutput (x1,x2,x3)) & (Following (t,2)) . (GFA0CarryOutput (x5,x6,x7)) = (Following (s1,2)) . (GFA0CarryOutput (x5,x6,x7)) & (Following (t,2)) . (GFA0AdderOutput (x1,x2,x3)) = (Following (s1,2)) . (GFA0AdderOutput (x1,x2,x3)) & (Following (t,2)) . (GFA0AdderOutput (x5,x6,x7)) = (Following (s1,2)) . (GFA0AdderOutput (x5,x6,x7)) ) by FACIRC_1:32;
( a1 = s1 . x1 & a2 = s1 . x2 & a3 = s1 . x3 & a5 = s1 . x5 & a6 = s1 . x6 & a7 = s1 . x7 ) by ThSTC0IIS6, A2, A4, 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)) . (STC0IICarryOutputC2 (x1,x2,x3,x5,x6,x7)) = ((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5) & (Following (s,2)) . (STC0IIAdderOutputA1 (x1,x2,x3,x5,x6,x7)) = (a1 'xor' a2) 'xor' a3 & (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)) . x4 = a4 & (Following (s,2)) . x5 = a5 & (Following (s,2)) . x6 = a6 & (Following (s,2)) . x7 = a7 ) by A2, A3, CIRCCMB3:1, A5, ThSTC0IIS10; :: thesis: