for am, bp, cm, dp being non pair set
for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] & not cin in InnerVertices (BitGFA2Str (am,bp,cm)) holds
InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) = {am,bp,cm,dp,cin}