theorem Th13: :: FTACELL1:13

for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds
InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = {ap,bm,cp,dm,cin}