let am, bp, cm, dp be non pair set ; :: thesis: for cin being set st cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] & not cin in InnerVertices (BitGFA2Str am,bp,cm) holds
( am in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & bp in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & cm in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & dp in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & cin in InputVertices (BitFTA2Str am,bp,cm,dp,cin) )
let cin be set ; :: thesis: ( cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] & not cin in InnerVertices (BitGFA2Str am,bp,cm) implies ( am in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & bp in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & cm in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & dp in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & cin in InputVertices (BitFTA2Str am,bp,cm,dp,cin) ) )
set S = BitFTA2Str am,bp,cm,dp,cin;
set S1 = BitGFA2Str am,bp,cm;
set A1 = GFA2AdderOutput am,bp,cm;
set dpA1 = [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ];
assume ( cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] & not cin in InnerVertices (BitGFA2Str am,bp,cm) ) ; :: thesis: ( am in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & bp in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & cm in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & dp in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & cin in InputVertices (BitFTA2Str am,bp,cm,dp,cin) )
then InputVertices (BitFTA2Str am,bp,cm,dp,cin) = {am,bp,cm,dp,cin} by Th23;
hence ( am in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & bp in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & cm in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & dp in InputVertices (BitFTA2Str am,bp,cm,dp,cin) & cin in InputVertices (BitFTA2Str am,bp,cm,dp,cin) ) by ENUMSET1:def 3; :: thesis: verum