let k be Nat; :: thesis: for ap, bp, cp, dp being nonpair-yielding FinSequence
for s being State of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) holds Following (s,2) is stable
let ap, bp, cp, dp be nonpair-yielding FinSequence; :: thesis: for s being State of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) holds Following (s,2) is stable
set X = GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)));
set Y = k -BitFTA0CarryOutput (ap,bp,cp,dp);
set d = dp . (k + 1);
A1: GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) <> [<*(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))*>,and2] by XTUPLE_0:1, TWOSCOMP:11, TWOSCOMP:9;
A2: k -BitFTA0CarryOutput (ap,bp,cp,dp) <> [<*(dp . (k + 1)),(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))*>,and2] by LmT0CO;
let s be State of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))); :: thesis: Following (s,2) is stable
thus Following (s,2) is stable by A1, A2, GFACIRC1:40; :: thesis: verum