let am, bm, cm, dm be non pair set ; :: thesis: for cin being set st cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] & 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)*>,and2b ] & 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)*>,and2b ];
assume ( cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] & 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