theorem Th36: :: FTACELL1:36

for am, bm, cm, dm being non pair set
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)) )