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)) 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)); 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
; verum