theorem Th11: :: FTACELL1:11

for ap, bm, cp, dm, cin being set holds InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = (({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}