let x, y, z be set ; :: thesis: InnerVertices (GFA3AdderStr (x,y,z)) = {[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}
GFA3AdderOutput (x,y,z) = GFA0AdderOutput (x,y,z) ;
hence InnerVertices (GFA3AdderStr (x,y,z)) = {[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))} by Th24; :: thesis: verum