675 path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))" |
675 path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))" |
676 "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union> |
676 "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union> |
677 path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union> |
677 path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union> |
678 path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union> |
678 path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union> |
679 path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2) |
679 path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2) |
680 by(auto simp add: path_image_join path_linepath) |
680 by(auto simp add: path_image_join) |
681 have abab: "cbox a b \<subseteq> cbox ?a ?b" |
681 have abab: "cbox a b \<subseteq> cbox ?a ?b" |
682 unfolding interval_cbox_cart[symmetric] |
682 unfolding interval_cbox_cart[symmetric] |
683 by (auto simp add:less_eq_vec_def forall_2 vector_2) |
683 by (auto simp add:less_eq_vec_def forall_2) |
684 obtain z where |
684 obtain z where |
685 "z \<in> path_image |
685 "z \<in> path_image |
686 (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++ |
686 (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++ |
687 linepath (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f) +++ |
687 linepath (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f) +++ |
688 f +++ |
688 f +++ |