let k be Nat; :: thesis: for ap, bm, cp, dm being nonpair-yielding FinSequence holds InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))) = {(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))}
let ap, bm, cp, dm be nonpair-yielding FinSequence; :: thesis: InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))) = {(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))}
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;
thus InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))) = {(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))} by A1, LmT1CO, GFACIRC1:97; :: thesis: verum