let x, y, z be set ; :: thesis: InnerVertices (GFA2AdderStr (x,y,z)) = {[<*x,y*>,xor2c]} \/ {(GFA2AdderOutput (x,y,z))}
GFA2AdderOutput (x,y,z) = GFA1AdderOutput (x,y,z) ;
hence InnerVertices (GFA2AdderStr (x,y,z)) = {[<*x,y*>,xor2c]} \/ {(GFA2AdderOutput (x,y,z))} by Th55; :: thesis: verum