for ap, bp, cp, dp, cin being set holds
( ap in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & bp in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & cp in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & dp in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & cin in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*ap,bp*>,xor2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput (ap,bp,cp) in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*ap,bp*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*bp,cp*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cp,ap*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput (ap,bp,cp) in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cin,dp*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in the carrier of (BitFTA0Str (ap,bp,cp,dp,cin)) )