for ap, bm, cp, dm, cin being set holds
( ap in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1AdderOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*bm,cp*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cp,ap*>,and2] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1CarryOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cin,dm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) )