theorem Th3: :: FTACELL1:3

for ap, bp, cp, dp being non pair set
for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] & not cin in InnerVertices (BitGFA0Str (ap,bp,cp)) holds
InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) = {ap,bp,cp,dp,cin}