let x1, x2, x3, x4, x5, x6, x7 be non pair set ; :: thesis: for s being State of (STC0Circ (x1,x2,x3,x4,x5,x6,x7))
for a1, a2, a3, a4, a5, a6, a7 being Element of BOOLEAN st a1 = s . x1 & a2 = s . x2 & a3 = s . x3 & a4 = s . x4 & a5 = s . x5 & a6 = s . x6 & a7 = s . x7 holds
(Following (s,5)) . (GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) = ((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))
set S = STC0Str (x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ (x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr (x1,x2,x3,x4,x5,x6,x7);
set C1 = STC0ICirc (x1,x2,x3,x4,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 C3out = GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
set S2 = BitGFA0Str ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)));
set C2 = BitGFA0Circ ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)));
set n1 = 4;
set n2 = 5;
let s be State of (STC0Circ (x1,x2,x3,x4,x5,x6,x7)); :: thesis: for a1, a2, a3, a4, a5, a6, a7 being Element of BOOLEAN st a1 = s . x1 & a2 = s . x2 & a3 = s . x3 & a4 = s . x4 & a5 = s . x5 & a6 = s . x6 & a7 = s . x7 holds
(Following (s,5)) . (GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) = ((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))
let a1, a2, a3, a4, a5, a6, a7 be Element of BOOLEAN ; :: thesis: ( a1 = s . x1 & a2 = s . x2 & a3 = s . x3 & a4 = s . x4 & a5 = s . x5 & a6 = s . x6 & a7 = s . x7 implies (Following (s,5)) . (GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) = ((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3)) )
assume A2: ( a1 = s . x1 & a2 = s . x2 & a3 = s . x3 & a4 = s . x4 & a5 = s . x5 & a6 = s . x6 & a7 = s . x7 ) ; :: thesis: (Following (s,5)) . (GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) = ((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))
reconsider t = s as State of ((STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) +* (BitGFA0Circ ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))))) ;
reconsider s1 = s | the carrier of (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) as State of (STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) by FACIRC_1:26;
A3: dom s1 = the carrier of (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) by CIRCUIT1:3;
A4: Following (s1,5) = Following (s1,4) by ThSTC0IS18, CIRCCMB2:4;
( GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) in the carrier of (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) & InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) misses InnerVertices (BitGFA0Str ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))) ) by ThSTC0IS6, LmSTC0S2b;
then A5: (Following (t,5)) . (GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) = (Following (s1,4)) . (GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) by A4, FACIRC_1:32;
( a1 = s1 . x1 & a2 = s1 . x2 & a3 = s1 . x3 & a4 = s1 . x4 & a5 = s1 . x5 & a6 = s1 . x6 & a7 = s1 . x7 ) by ThSTC0IS6, A2, A3, FUNCT_1:47;
hence (Following (s,5)) . (GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) = ((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3)) by A5, LmSTC0IS15C3; :: thesis: verum