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