theorem Th21: :: FTACELL1:21

for am, bp, cm, dp, cin being set holds InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) = (({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c],(GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c],[<*cin,dp*>,and2a],[<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2],(GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}