theorem Th6: :: FTACELL1:6

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
( ap in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & bp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & dp in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & cin in InputVertices (BitFTA0Str (ap,bp,cp,dp,cin)) )