for ap, bp, cp, dp being non pair set
for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] holds
for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) holds Following (s,4) is stable