theorem Th63: :: GFACIRC1:63

for x, y, z being set holds InnerVertices (BitGFA1Str (x,y,z)) = (({[<*x,y*>,xor2c]} \/ {(GFA1AdderOutput (x,y,z))}) \/ {[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]}) \/ {(GFA1CarryOutput (x,y,z))}