set n1 = 2;
set n2 = 2;
set n12 = 4;
let ap, bm, cp, dm be non pair set ; :: thesis: for cin being set st cin <> [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] 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)*>,and2b ] implies for s being State of (BitFTA1Circ ap,bm,cp,dm,cin) holds Following s,4 is stable )
set S = BitFTA1Str ap,bm,cp,dm,cin;
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 apbm0 = [<*ap,bm*>,xor2c ];
set apbm = [<*ap,bm*>,and2c ];
set bmcp = [<*bm,cp*>,and2a ];
set cpap = [<*cp,ap*>,and2 ];
set A1cin0 = [<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ];
set A1cin = [<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ];
set cindm = [<*cin,dm*>,and2c ];
set dmA1 = [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ];
assume A1: cin <> [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] ; :: 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:68;
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:33;
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:33;
A3: ( InputVertices (BitGFA1Str ap,bm,cp) misses InnerVertices (BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm) & Following s1,2 is stable ) by Lm12, GFACIRC1:85;
Following s2,2 is stable by A1, Lm11, GFACIRC1:122;
then Following s,(2 + 2) is stable by A3, CIRCCMB2:20, CIRCCOMB:68;
hence Following s,4 is stable ; :: thesis: verum