theorem Th31: :: FTACELL1:31

for am, bm, cm, dm, cin being set holds InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) = (({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}