let am, bm, cm, dm be non pair set ; :: thesis: for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds
( am in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & bm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & dm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cin in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) )
let cin be set ; :: thesis: ( cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) implies ( am in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & bm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & dm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cin in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) ) )
set S = BitFTA3Str (am,bm,cm,dm,cin);
set S1 = BitGFA3Str (am,bm,cm);
set A1 = GFA3AdderOutput (am,bm,cm);
set dmA1 = [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2];
assume ( cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) ) ; :: thesis: ( am in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & bm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & dm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cin in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) )
then InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) = {am,bm,cm,dm,cin} by Th33;
hence ( am in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & bm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & dm in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) & cin in InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) ) by ENUMSET1:def 3; :: thesis: verum