theorem Th95: :: GFACIRC1:95

for x, y, z being set holds InnerVertices (BitGFA2Str (x,y,z)) = (({[<*x,y*>,xor2c]} \/ {(GFA2AdderOutput (x,y,z))}) \/ {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]}) \/ {(GFA2CarryOutput (x,y,z))}