let x1, x2, x3, x4, x5, x6, x7 be non pair set ; 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 (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) '&' (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) & (Following (s,5)) . [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] = (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) '&' (((((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,5)) . [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] = (((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))) '&' (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) )
set S = STC0Str (x1,x2,x3,x4,x5,x6,x7);
set C = STC0Circ (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 C1C2a = [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2];
set C2C3a = [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2];
set C3C1a = [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2];
let s be 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 (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) '&' (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) & (Following (s,5)) . [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] = (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) '&' (((((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,5)) . [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] = (((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))) '&' (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) )
let a1, a2, a3, a4, a5, a6, a7 be Element of BOOLEAN ; ( 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 (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) '&' (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) & (Following (s,5)) . [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] = (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) '&' (((((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,5)) . [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] = (((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))) '&' (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) ) )
assume A2:
( a1 = s . x1 & a2 = s . x2 & a3 = s . x3 & a4 = s . x4 & a5 = s . x5 & a6 = s . x6 & a7 = s . x7 )
; ( (Following (s,5)) . [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) '&' (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) & (Following (s,5)) . [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] = (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) '&' (((((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,5)) . [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] = (((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))) '&' (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) )
A5:
( (Following (s,4)) . (GFA0CarryOutput (x1,x2,x3)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) & (Following (s,4)) . (GFA0CarryOutput (x5,x6,x7)) = ((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5) & (Following (s,4)) . (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 A2, LmSTC0S15s4a, LmSTC0S15s4b;
Following (s,(4 + 1)) = Following (Following (s,4))
by FACIRC_1:12;
hence
( (Following (s,5)) . [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) '&' (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) & (Following (s,5)) . [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] = (((a5 '&' a6) 'or' (a6 '&' a7)) 'or' (a7 '&' a5)) '&' (((((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,5)) . [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] = (((((a1 'xor' a2) 'xor' a3) '&' ((a5 'xor' a6) 'xor' a7)) 'or' (((a5 'xor' a6) 'xor' a7) '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))) '&' (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) )
by A5, LmSTC0S15S2s4; verum