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