let x1, x2, x3, x4, x5, x6, x7 be 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,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 )
set S = STC0IStr (x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc (x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput (x1,x2,x3);
set A2out = GFA0AdderOutput (x5,x6,x7);
set A1A20 = [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2];
set A3out = STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7);
let s be 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,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 )
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,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 ) )
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,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 )
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;
A4:
Following (s,(3 + 1)) = Following (Following (s,3))
by FACIRC_1:12;
A5:
( (Following (s,3)) . [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,xor2] = ((a1 'xor' a2) 'xor' a3) 'xor' ((a5 'xor' a6) 'xor' a7) & (Following (s,3)) . x4 = a4 )
by A2, LmSTC0IS15A3s6;
(Following (s,4)) . (STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7)) =
(((a1 'xor' a2) 'xor' a3) 'xor' ((a5 'xor' a6) 'xor' a7)) 'xor' a4
by A4, A5, LmSTC0IS15A3s8
.=
((((a1 'xor' a2) 'xor' a3) 'xor' (a5 'xor' a6)) 'xor' a7) 'xor' a4
by XBOOLEAN:73
.=
(((((a1 'xor' a2) 'xor' a3) 'xor' a5) 'xor' a6) 'xor' a7) 'xor' a4
by XBOOLEAN:73
.=
(((((a1 'xor' a2) 'xor' a3) 'xor' a5) 'xor' a6) 'xor' a4) 'xor' a7
by XBOOLEAN:73
.=
(((((a1 'xor' a2) 'xor' a3) 'xor' a5) 'xor' a4) 'xor' a6) 'xor' a7
by XBOOLEAN:73
.=
(((((a1 'xor' a2) 'xor' a3) 'xor' a4) 'xor' a5) 'xor' a6) 'xor' a7
by XBOOLEAN:73
;
hence
( (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 A2, A3, CIRCCMB3:1; verum