theorem :: WALLACE1:19

for x1, x2, x3, x4, x5, x6, x7 being non pair set
for s being State of (STC0ICirc (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,2)) . (STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) & (Following (s,2)) . (STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)) = ((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5) & (Following (s,4)) . (STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)) = ((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3)) & (Following (s,4)) . (STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7)) = (((((a1 'xor' a2) 'xor' a3) 'xor' a4) 'xor' a5) 'xor' a6) 'xor' a7 & (Following (s,4)) . x1 = a1 & (Following (s,4)) . x2 = a2 & (Following (s,4)) . x3 = a3 & (Following (s,4)) . x4 = a4 & (Following (s,4)) . x5 = a5 & (Following (s,4)) . x6 = a6 & (Following (s,4)) . x7 = a7 ) by LmSTC0IS15C1, LmSTC0IS15C2, LmSTC0IS15C3, LmSTC0IS15A3;