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