theorem Th35: :: FTACELL1:35

for am, bm, cm, dm, cin being set holds
( [<*am,bm*>,xor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput (am,bm,cm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput (am,bm,cm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) )