let ap, bp, cp, dp be non pair set ; :: thesis: for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds
( ap in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & bp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & dp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cin in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) )
let cin be set ; :: thesis: ( cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) implies ( ap in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & bp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & dp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cin in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) ) )
set S = BitFTA0Str (ap,bp,cp,dp,cin);
set S1 = BitGFA0Str (ap,bp,cp);
set A1 = GFA0AdderOutput (ap,bp,cp);
set dpA1 = [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2];
assume ( cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) ) ; :: thesis: ( ap in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & bp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & dp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cin in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) )
then InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) = {ap,bp,cp,dp,cin} by Th3;
hence ( ap in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & bp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & dp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cin in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) ) by ENUMSET1:def 3; :: thesis: verum