let x1, x2, x3, x4, x5, x6, x7 be non pair set ; :: thesis: for s being State of (STC0ICirc (x1,x2,x3,x4,x5,x6,x7)) holds Following (s,4) is stable
set C = STC0ICirc (x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IIStr (x1,x2,x3,x5,x6,x7);
set C1 = STC0IICirc (x1,x2,x3,x5,x6,x7);
set A1out = GFA0AdderOutput (x1,x2,x3);
set A2out = GFA0AdderOutput (x5,x6,x7);
set S2 = BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
set C2 = BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);
set n1 = 2;
set n2 = 2;
let s be State of (STC0ICirc (x1,x2,x3,x4,x5,x6,x7)); :: thesis: Following (s,4) is stable
STC0IICirc (x1,x2,x3,x5,x6,x7) tolerates BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4) by CIRCCOMB:60;
then A2: the Sorts of (STC0IICirc (x1,x2,x3,x5,x6,x7)) tolerates the Sorts of (BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) by CIRCCOMB:def 3;
then reconsider s1 = s | the carrier of (STC0IIStr (x1,x2,x3,x5,x6,x7)) as State of (STC0IICirc (x1,x2,x3,x5,x6,x7)) by CIRCCOMB:26;
reconsider s2 = (Following (s,2)) | the carrier of (BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) as State of (BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) by A2, CIRCCOMB:26;
A3: ( InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) misses InnerVertices (BitGFA0Str ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4)) & Following (s1,2) is stable ) by LmSTC0IS2b, ThSTC0IIS12;
( GFA0AdderOutput (x1,x2,x3) <> [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] & GFA0AdderOutput (x5,x6,x7) <> [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] ) by LmSTC0IS1;
then Following (s2,2) is stable by GFACIRC1:40;
then Following (s,(2 + 2)) is stable by A3, CIRCCMB2:19, CIRCCOMB:60;
hence Following (s,4) is stable ; :: thesis: verum