set n1 = 2;
set n2 = 2;
let ap, bm, cp, dm be non pair set ; :: thesis: for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] holds
for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) holds Following (s,4) is stable
let cin be set ; :: thesis: ( cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] implies for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) holds Following (s,4) is stable )
set C = BitFTA1Circ (ap,bm,cp,dm,cin);
set S1 = BitGFA1Str (ap,bm,cp);
set C1 = BitGFA1Circ (ap,bm,cp);
set A1 = GFA1AdderOutput (ap,bm,cp);
set S2 = BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm);
set C2 = BitGFA2Circ ((GFA1AdderOutput (ap,bm,cp)),cin,dm);
set dmA1 = [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2];
assume A1: cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] ; :: thesis: for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) holds Following (s,4) is stable
let s be State of (BitFTA1Circ (ap,bm,cp,dm,cin)); :: thesis: Following (s,4) is stable
BitGFA1Circ (ap,bm,cp) tolerates BitGFA2Circ ((GFA1AdderOutput (ap,bm,cp)),cin,dm) by CIRCCOMB:60;
then A2: the Sorts of (BitGFA1Circ (ap,bm,cp)) tolerates the Sorts of (BitGFA2Circ ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) by CIRCCOMB:def 3;
then reconsider s1 = s | the carrier of (BitGFA1Str (ap,bm,cp)) as State of (BitGFA1Circ (ap,bm,cp)) by CIRCCOMB:26;
reconsider s2 = (Following (s,2)) | the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) as State of (BitGFA2Circ ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) by A2, CIRCCOMB:26;
A3: ( InputVertices (BitGFA1Str (ap,bm,cp)) misses InnerVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) & Following (s1,2) is stable ) by Lm12, GFACIRC1:72;
Following (s2,2) is stable by A1, Lm11, GFACIRC1:104;
then Following (s,(2 + 2)) is stable by A3, CIRCCMB2:19, CIRCCOMB:60;
hence Following (s,4) is stable ; :: thesis: verum