theorem Th25: :: FTACELL1:25

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