theorem Th31: :: GFACIRC1:31

for x, y, z being set holds InnerVertices (BitGFA0Str (x,y,z)) = (({[<*x,y*>,xor2]} \/ {(GFA0AdderOutput (x,y,z))}) \/ {[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]}) \/ {(GFA0CarryOutput (x,y,z))}