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,4)) . (STC0OutputS0 (x1,x2,x3,x4,x5,x6,x7)) = (((((a1 'xor' a2) 'xor' a3) 'xor' a4) 'xor' a5) 'xor' a6) 'xor' a7
set A1out = GFA0AdderOutput (x1,x2,x3);
set A2out = GFA0AdderOutput (x5,x6,x7);
set A3out = GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
( GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) = STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7) & GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) = STC0OutputS0 (x1,x2,x3,x4,x5,x6,x7) ) ;
hence 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,4)) . (STC0OutputS0 (x1,x2,x3,x4,x5,x6,x7)) = (((((a1 'xor' a2) 'xor' a3) 'xor' a4) 'xor' a5) 'xor' a6) 'xor' a7 by LmSTC0S15s4b; :: thesis: verum