let k be Nat; :: thesis: for ap, bm, cp, dm being nonpair-yielding FinSequence
for s being State of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))) holds Following (s,2) is stable
let ap, bm, cp, dm be nonpair-yielding FinSequence; :: thesis: for s being State of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))) holds Following (s,2) is stable
set X = GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)));
set Y = k -BitFTA1CarryOutput (ap,bm,cp,dm);
set d = dm . (k + 1);
A1: GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) <> [<*(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))*>,and2c] by XTUPLE_0:1, GFACIRC1:4, GFACIRC1:3;
let s be State of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))); :: thesis: Following (s,2) is stable
thus Following (s,2) is stable by A1, LmT1CO, GFACIRC1:104; :: thesis: verum