theorem Th26: :: FTACELL1:26

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
( am in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) & bp in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) & cm in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) & dp in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) & cin in InputVertices (BitFTA2Str (am,bp,cm,dp,cin)) )