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