let ap, bm, cp, dm be non pair set ; :: thesis: for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds
( ap in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) )
let cin be set ; :: thesis: ( cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) implies ( ap in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) ) )
set S = BitFTA1Str (ap,bm,cp,dm,cin);
set S1 = BitGFA1Str (ap,bm,cp);
set A1 = GFA1AdderOutput (ap,bm,cp);
set dmA1 = [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2];
assume ( cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) ) ; :: thesis: ( ap in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) )
then InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = {ap,bm,cp,dm,cin} by Th13;
hence ( ap in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) ) by ENUMSET1:def 3; :: thesis: verum