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)) holds Following (s,6) is stable
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 C1C2x = [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2];
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];
set n1 = 4;
set n2 = 2;
let s be State of (STC0Circ (x1,x2,x3,x4,x5,x6,x7)); :: thesis: Following (s,6) is stable
STC0ICirc (x1,x2,x3,x4,x5,x6,x7) tolerates BitGFA0Circ ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))) by CIRCCOMB:60;
then A2: the Sorts of (STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) tolerates the Sorts of (BitGFA0Circ ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))) by CIRCCOMB:def 3;
then 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 CIRCCOMB:26;
reconsider s2 = (Following (s,4)) | the carrier of (BitGFA0Str ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))) as State of (BitGFA0Circ ((GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)))) by A2, CIRCCOMB:26;
A3: ( 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)))) & Following (s1,4) is stable ) by LmSTC0S2b, ThSTC0IS18;
( GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) <> [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,xor2] & GFA0CarryOutput (x1,x2,x3) <> [<*(GFA0CarryOutput (x5,x6,x7)),(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4))*>,and2] & GFA0CarryOutput (x5,x6,x7) <> [<*(GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)),(GFA0CarryOutput (x1,x2,x3))*>,and2] & GFA0CarryOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) <> [<*(GFA0CarryOutput (x1,x2,x3)),(GFA0CarryOutput (x5,x6,x7))*>,and2] ) by LmSTC0S1;
then Following (s2,2) is stable by GFACIRC1:40;
then Following (s,(4 + 2)) is stable by A3, CIRCCMB2:19, CIRCCOMB:60;
hence Following (s,6) is stable ; :: thesis: verum