let k be Nat; :: thesis: for ap, bp, cp, dp being nonpair-yielding FinSequence holds InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) = {(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))}
let ap, bp, cp, dp be nonpair-yielding FinSequence; :: thesis: InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) = {(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))}
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;
thus InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) = {(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))} by A1, A2, GFACIRC1:33; :: thesis: verum