Skip to content

Instantly share code, notes, and snippets.

@rsoeldner

rsoeldner/DPO.thy

Created August 10, 2021 18:17
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save rsoeldner/0f35aa5b1e8b88df568bd5d8fcdbf02f to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save rsoeldner/0f35aa5b1e8b88df568bd5d8fcdbf02f to your computer and use it in GitHub Desktop.
Download ZIP
Isabelle DPO
Raw
DPO.thy
theory DPO
imports Main
begin
record ('v,'e,'l,'m) graph =
nodes :: "'v set"
edges :: "'e set"
src :: "'e ⇒ 'v"
trg :: "'e ⇒ 'v"
me :: "'e ⇒ 'l"
mv :: "'v ⇒ 'm"
definition wf_graph :: "('v,'e,'l,'m) graph ⇒ bool" where
"wf_graph G ≡
finite (nodes G)
∧ finite (edges G)
∧ src G ` edges G ⊆ nodes G
∧ trg G ` edges G ⊆ nodes G"
lemma wf_gr_finite_nodes: "wf_graph G ⟹ finite (nodes G)"
by (simp add: wf_graph_def)
lemma wf_gr_finite_edges: "wf_graph G ⟹ finite (edges G)"
by (simp add: wf_graph_def)
lemma wf_gr_src: "wf_graph G ⟹ src G ` edges G ⊆ nodes G"
by (simp add: wf_graph_def)
lemma wf_gr_trg: "wf_graph G ⟹ trg G ` edges G ⊆ nodes G"
by (simp add: wf_graph_def)
record ('v,'e) morph =
morph_node :: "'v ⇒ 'v"
morph_edge :: "'e ⇒ 'e"
definition wf_morph :: "('v,'e) morph ⇒ ('v,'e,'l,'m) graph ⇒ ('v,'e,'l,'m) graph ⇒ bool" where
"wf_morph m G H ≡
(∀e ∈ edges G.
morph_edge m e ∈ edges H ― ‹required for the proof›
∧ morph_node m (src G e) = src H (morph_edge m e)
∧ morph_node m (trg G e) = trg H (morph_edge m e)
∧ me G e = me H (morph_edge m e))
∧ (∀v ∈ nodes G. morph_node m v ∈ nodes H ∧ mv G v = mv H (morph_node m v))"
abbreviation morphism_comp ::
"('v, 'e) morph ⇒ ('v,'e) morph⇒ ('v,'e) morph" (infixl "∘⇩M" 50) where
"morphism_comp g f ≡ ⦇morph_node = morph_node g ∘ morph_node f, morph_edge = morph_edge g ∘ morph_edge f⦈"
text ‹Fact 2.5; Composition of graph morphisms (P. 22)›
lemma "⟦wf_morph f F G; wf_morph g G H⟧ ⟹ wf_morph (g ∘⇩M f) F H"
by (simp add: wf_morph_def)
― ‹Initially stay with inj, surj, bij, later move to inj_on, .... which is not as strong
surj is trivial
›
definition inj_morph :: "('v,'e) morph ⇒ bool" where
"inj_morph m ≡ inj (morph_node m) ∧ inj (morph_edge m)"
definition surj_morph :: "('v,'e) morph ⇒ bool" where
"surj_morph m ≡ surj (morph_node m) ∧ surj (morph_edge m)"
definition bij_morph :: "('v,'e) morph ⇒ bool" where
"bij_morph m ≡ bij (morph_node m) ∧ bij (morph_edge m)"
abbreviation iso_morph where "iso_morph ≡ bij_morph"
lemma "⟦inj_morph m; surj_morph m⟧ ⟹ iso_morph m"
apply (simp add: inj_morph_def surj_morph_def bij_morph_def)
by (simp add: bijI)
definition is_iso :: "('v,'e,'l,'m) graph ⇒ ('v,'e,'l,'m) graph ⇒ bool" where
"is_iso G H ≡ ∃m . wf_morph m G H ∧ iso_morph m"
definition iso_graphs :: "('v,'e,'l,'m) graph ⇒ ('v,'e,'l,'m) graph set" where
"iso_graphs G ≡ {X. is_iso X G}"
lemma "wf_graph G ⟹ G ∈ iso_graphs G"
apply (simp add: iso_graphs_def is_iso_def bij_morph_def wf_morph_def wf_graph_def)
by (metis bij_betw_id id_apply morph.select_convs(1) morph.select_convs(2))
definition inc_morph :: "('v,'e) morph ⇒ ('v,'e,'l,'m) graph ⇒ ('v,'e,'l,'m) graph ⇒ bool" where
"inc_morph f G H ≡
(∀v ∈ nodes G. v ∈ nodes H ∧ morph_node f v = v)
∧ (∀e ∈ edges G. e ∈ edges H ∧ morph_edge f e = e)"
definition subgraph :: "('v,'e,'l,'m) graph ⇒ ('v,'e,'l,'m) graph ⇒ bool" where
"subgraph G H ≡
nodes G ⊆ nodes H
∧ edges G ⊆ edges H
∧ (∀e ∈ edges G. src G e = src H e ∧ trg G e = trg H e ∧ me G e = me H e)
∧ (∀v ∈ nodes G. mv G v = mv H v)"
lemma "wf_graph g ⟹ subgraph g g"
by (simp add: subgraph_def)
lemma ex_subgraph_inc_morph:
"⟦wf_graph G; wf_graph H; (∃f. wf_morph f G H ∧ inc_morph f G H)⟧ ⟹ subgraph G H"
apply (simp add: subgraph_def inc_morph_def wf_morph_def wf_graph_def)
apply safe
apply fastforce
apply fastforce
apply fastforce
apply (metis image_subset_iff)
apply metis
by metis
record ('v,'e,'l,'m) rule =
rule_lhs :: "('v,'e,'l,'m) graph"
rule_int :: "('v,'e,'l,'m) graph"
rule_rhs :: "('v,'e,'l,'m) graph"
definition wf_rule :: "('v,'e,'l,'m) rule ⇒ bool" where
"wf_rule r ≡ wf_graph (rule_lhs r)
∧ wf_graph (rule_int r)
∧ wf_graph (rule_rhs r)
∧ (∃l. wf_morph l (rule_int r) (rule_lhs r) ∧ inc_morph l (rule_int r) (rule_lhs r))
∧ (∃k. wf_morph k (rule_int r) (rule_rhs r) ∧ inc_morph k (rule_int r) (rule_rhs r))"
abbreviation rule_inverse :: "('v, 'e, 'lv, 'le) rule ⇒ ('v, 'e, 'lv, 'le) rule" ("_¯" [10] 11) where
"rule_inverse r ≡ ⦇rule_lhs = rule_rhs r, rule_int = rule_int r, rule_rhs = rule_lhs r⦈"
lemma rule_inv_inv[simp] : "rule_inverse (rule_inverse r) = r"
by simp
lemma "wf_rule r ⟹ wf_rule (rule_inverse r)"
by (simp add: wf_rule_def)
lemma "wf_rule r ⟹ subgraph (rule_int r) (rule_lhs r)"
apply (simp add: subgraph_def wf_rule_def wf_graph_def)
by (meson ex_subgraph_inc_morph subgraph_def wf_graph_def)
lemma "wf_rule r ⟹ ∃m. wf_morph m (rule_int r) (rule_lhs r) ∧ inc_morph m (rule_int r) (rule_lhs r)"
by (simp add: wf_rule_def inc_morph_def wf_graph_def)
text ‹Definition 12.2 Dangling condition›
definition dang :: "('v,'e,'l,'m) rule ⇒ ('v,'e,'l,'m) graph ⇒ ('v,'e) morph ⇒ bool" where
"dang r G f ≡ (let
E = edges G - morph_edge f ` (edges (rule_lhs r) - edges (rule_int r));
V = morph_node f ` nodes (rule_lhs r) - morph_node f ` nodes (rule_int r)
in ∀e ∈ E. src G e ∉ V ∧ trg G e ∉ V)"
lemma "⟦wf_rule r; wf_graph g; edges g = {}; wf_morph m g h⟧ ⟹ dang r g m"
by (simp add: dang_def)
text ‹Definition 12.3 Direct derivability›
abbreviation disjoint_union :: "'a set ⇒ 'a set ⇒ ('a + 'a) set" (infixl "|+|" 65) where
"disjoint_union A B ≡ Inl ` A ∪ Inr ` B"
lemma finite_disjoint_union[simp]: "⟦finite a; finite b⟧ ⟹ finite (a|+|b)"
by simp
definition wf_match :: "('v,'e,'l,'m) graph ⇒ ('v,'e,'l,'m) rule ⇒ ('v,'e) morph ⇒ bool" where
"wf_match G r f ≡ wf_morph f (rule_lhs r) G ∧ inj_morph f ∧ dang r G f"
definition po :: "('v,'e,'l,'m) graph ⇒ ('v,'e,'l,'m) rule ⇒ ('v,'e) morph ⇒ ('v,'e,'l,'m) graph" where
"po G r f ≡ (let
V = nodes G - (morph_node f ` (nodes (rule_lhs r) - nodes (rule_int r)));
E = edges G - (morph_edge f ` (edges (rule_lhs r) - edges (rule_int r)))
in G⦇nodes := V, edges := E⦈)"
lemma wf_graph_po:
"⟦wf_graph G; wf_rule r; wf_match G r m⟧ ⟹ wf_graph (po G r m)"
apply (simp add: po_def wf_graph_def dang_def wf_match_def)
by (simp add: image_set_diff image_subset_iff inj_morph_def)
definition glue ::
"('v,'e,'l,'m) graph
⇒ ('v,'e,'l,'m) rule
⇒ ('v,'e) morph
⇒ ('v+'v,'e+'e,'l,'m) graph" where
"glue D r f ≡ (let
V = nodes D |+| ((nodes (rule_rhs r) - nodes (rule_int r)));
E = edges D |+| ((edges (rule_rhs r) - edges (rule_int r)));
s = λe. case e of
Inl e' ⇒ Inl (src D e')
| Inr e' ⇒ if e' ∈ (edges (rule_rhs r) - edges (rule_int r)) ∧ (src (rule_rhs r) e') ∈ nodes (rule_int r)
then Inl (morph_node f (src (rule_rhs r) e')) else Inr (src (rule_rhs r) e');
t = λe. case e of
Inl e' ⇒ Inl (trg D e')
| Inr e' ⇒ if e' ∈ (edges (rule_rhs r) - edges (rule_int r)) ∧ (trg (rule_rhs r) e') ∈ nodes (rule_int r)
then Inl (morph_node f (trg (rule_rhs r) e')) else Inr (trg (rule_rhs r) e');
me = λe. case e of
Inl e' ⇒ me D e'
| Inr e' ⇒ me (rule_rhs r) e';
mv = λv. case v of
Inl v' ⇒ mv D v'
| Inr v' ⇒ mv (rule_rhs r) v'
in ⦇nodes = V, edges = E, src = s, trg = t, me = me, mv = mv⦈)"
definition wf_restriction :: "('v,'e,'l,'m) graph ⇒ ('v,'e,'l,'m) rule ⇒ ('v,'e) morph ⇒ ('v,'e) morph ⇒ bool" where
"wf_restriction D r m f ≡ wf_morph f (rule_int r) D ∧ inj_morph f
∧ (∀x ∈ nodes (rule_int r). morph_node f x = morph_node m x)
∧ (∀x ∈ edges (rule_int r). morph_edge f x = morph_edge m x)"
lemma wf_graph_glue:
"⟦wf_graph D
;wf_graph G
;wf_rule r
;wf_match G r m
;wf_restriction D r f d⟧
⟹ wf_graph (glue D r f)"
apply (simp add: glue_def wf_graph_def)
apply (rule conjI)
apply (simp add: wf_gr_finite_nodes wf_rule_def)
apply (rule conjI)
apply (simp add: wf_gr_finite_edges wf_rule_def)
apply (rule conjI)
apply clarsimp
apply safe
apply auto[1]
apply (simp add: wf_restriction_def)
apply (metis (no_types, hide_lams) DiffI imageI image_subset_iff wf_graph_def wf_morph_def wf_rule_def)
apply (simp add: image_subset_iff)
apply (simp add: wf_restriction_def)
by (metis (no_types, hide_lams) DiffI imageI subset_iff wf_graph_def wf_morph_def wf_rule_def)
definition rule_apply ::
"('v,'e,'l,'m) graph
⇒ ('v,'e,'l,'m) rule
⇒ ('v,'e) morph
⇒ ('v+'v,'e+'e,'l,'m) graph" where
"rule_apply G r m ≡ glue (po G r m) r m"
lemma rule_apply_finite_node[simp]:
"⟦wf_graph G; wf_rule r⟧ ⟹ finite (nodes (rule_apply G r m))"
apply (simp add: rule_apply_def glue_def po_def)
by (simp add: wf_gr_finite_nodes wf_rule_def)
lemma rule_apply_finite_edge[simp]:
"⟦wf_graph G; wf_rule r⟧ ⟹ finite (edges (rule_apply G r m))"
apply (simp add: rule_apply_def glue_def po_def)
by (simp add: wf_gr_finite_edges wf_rule_def)
lemma "⟦wf_graph G; wf_rule r; wf_match G r m⟧ ⟹ src (rule_apply G r m) ` edges (rule_apply G r m) ⊆ nodes (rule_apply G r m)"
apply (simp add: rule_apply_def glue_def po_def wf_match_def wf_morph_def)
apply safe
apply (smt (verit, best) DiffI dang_def image_iff image_set_diff image_subset_iff inj_morph_def old.sum.simps(5) wf_gr_src)
apply clarsimp
apply (rule conjI)
apply (metis (full_types) DiffD2 DiffI imageI inc_morph_def inj_image_mem_iff inj_morph_def wf_rule_def)
by (metis DiffI image_eqI image_subset_iff wf_gr_src wf_rule_def)
lemma rule_apply_src_pres[simp]:
"⟦wf_graph G; wf_rule r; wf_match G r m⟧ ⟹ src (rule_apply G r m) ` edges (rule_apply G r m) ⊆ nodes (rule_apply G r m)"
apply (simp add: rule_apply_def glue_def po_def)
proof -
assume a1: "wf_graph G"
assume a2: "wf_match G r m"
assume a3: "wf_rule r"
obtain bb :: "'b set ⇒ 'b set ⇒ 'b" where
"∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ x0) = (bb x0 x1 ∈ x1 ∧ bb x0 x1 ∉ x0)"
by moura
then have f4: "∀B Ba. (¬ B ⊆ Ba ∨ (∀b. b ∉ B ∨ b ∈ Ba)) ∧ (B ⊆ Ba ∨ bb Ba B ∈ B ∧ bb Ba B ∉ Ba)"
by blast
have f5: "∀x0 x1. ((¬ x1 ⊆ x0 ∨ (∀v2. v2 ∉ x1 ∨ v2 ∈ x0)) ∧ (x1 ⊆ x0 ∨ bb x0 x1 ∈ x1 ∧ bb x0 x1 ∉ x0)) = ((¬ x1 ⊆ x0 ∨ (∀v2. v2 ∉ x1 ∨ v2 ∈ x0)) ∧ (x1 ⊆ x0 ∨ bb x0 x1 ∈ x1 ∧ bb x0 x1 ∉ x0))"
by fastforce
obtain bba :: "'b set ⇒ ('b ⇒ 'b + 'b) ⇒ 'b + 'b ⇒ 'b" where
"∀x0 x1 x2. (∃v3. x2 = x1 v3 ∧ v3 ∈ x0) = (x2 = x1 (bba x0 x1 x2) ∧ bba x0 x1 x2 ∈ x0)"
by moura
then have f6: "∀s f B. s ∉ f ` B ∨ s = f (bba B f s) ∧ bba B f s ∈ B"
by auto
obtain ss :: "('b + 'b) set ⇒ ('b + 'b ⇒ 'a + 'a) ⇒ 'a + 'a ⇒ 'b + 'b" where
"∀x0 x1 x2. (∃v3. x2 = x1 v3 ∧ v3 ∈ x0) = (x2 = x1 (ss x0 x1 x2) ∧ ss x0 x1 x2 ∈ x0)"
by moura
then have f7: "∀s f S. s ∉ f ` S ∨ s = f (ss S f s) ∧ ss S f s ∈ S"
by (meson imageE)
obtain ssa :: "('a + 'a) set ⇒ ('a + 'a) set ⇒ 'a + 'a" where
"∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ x0) = (ssa x0 x1 ∈ x1 ∧ ssa x0 x1 ∉ x0)"
by moura
then have f8: "∀S Sa. (¬ S ⊆ Sa ∨ (∀s. s ∉ S ∨ s ∈ Sa)) ∧ (S ⊆ Sa ∨ ssa Sa S ∈ S ∧ ssa Sa S ∉ Sa)"
by blast
have f9: "∀b. b ∉ edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) ∨ b ∈ edges G"
by blast
have f10: "wf_morph m (rule_lhs r) G ∧ inj_morph m ∧ dang r G m"
using a2 by (simp add: wf_match_def)
obtain mm :: "('a, 'b, 'c, 'd) rule ⇒ ('a, 'b) morph" where
"∀x0. (∃v1. wf_morph v1 (rule_int x0) (rule_rhs x0) ∧ inc_morph v1 (rule_int x0) (rule_rhs x0)) = (wf_morph (mm x0) (rule_int x0) (rule_rhs x0) ∧ inc_morph (mm x0) (rule_int x0) (rule_rhs x0))"
by moura
then obtain mma :: "('a, 'b, 'c, 'd) rule ⇒ ('a, 'b) morph" where
f11: "wf_graph (rule_lhs r) ∧ wf_graph (rule_int r) ∧ wf_graph (rule_rhs r) ∧ wf_morph (mma r) (rule_int r) (rule_lhs r) ∧ inc_morph (mma r) (rule_int r) (rule_lhs r) ∧ wf_morph (mm r) (rule_int r) (rule_rhs r) ∧ inc_morph (mm r) (rule_int r) (rule_rhs r)"
using a3 by (meson wf_rule_def)
have f12: "(∀b. b ∉ edges (rule_lhs r) ∨ morph_edge m b ∈ edges G ∧ morph_node m (src (rule_lhs r) b) = src G (morph_edge m b) ∧ morph_node m (trg (rule_lhs r) b) = trg G (morph_edge m b) ∧ me (rule_lhs r) b = me G (morph_edge m b)) ∧ (∀a. a ∉ nodes (rule_lhs r) ∨ morph_node m a ∈ nodes G ∧ mv (rule_lhs r) a = mv G (morph_node m a))"
using f10 by (simp add: wf_morph_def)
have f13: "(∀a. a ∉ nodes (rule_int r) ∨ a ∈ nodes (rule_lhs r) ∧ morph_node (mma r) a = a) ∧ (∀b. b ∉ edges (rule_int r) ∨ b ∈ edges (rule_lhs r) ∧ morph_edge (mma r) b = b)"
using f11 by (simp add: inc_morph_def)
{ assume "src (rule_rhs r) (bba (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∈ src (rule_rhs r) ` edges (rule_rhs r)"
{ assume "ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ≠ Inr (bba (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∨ bba (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))))) ∉ edges (rule_rhs r) - edges (rule_int r)"
then have "ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∈ Inl ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inl ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) ∧ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inr ` (edges (rule_rhs r) - edges (rule_int r))"
using f6 by meson }
then have "(ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ≠ Inr (bba (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∨ bba (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))))) ∉ edges (rule_rhs r) - edges (rule_int r)) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∈ Inl ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) ∨ (case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (src G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ∈ Inl ` (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r))) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inl ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) ∧ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inr ` (edges (rule_rhs r) - edges (rule_int r)) ∨ (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))) ≠ (case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (src G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) ∨ ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))) ∉ case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) ∨ ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))) ∈ nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))"
using f13 f12 f11 f10 f4 by (smt (z3) DiffD2 DiffI Diff_subset Un_iff image_eqI image_set_diff inj_morph_def old.sum.simps(6) subset_eq wf_gr_src) }
moreover
{ assume "ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∈ Inl ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)))"
then have "(ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) = Inl (bba (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) Inl (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∧ bba (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) Inl (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))))) ∈ edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) ∧ src G (bba (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) Inl (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∈ nodes G"
using f9 f6 a1 by (meson image_eqI subset_eq wf_gr_src)
then have "(case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (src G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (src G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ∈ Inl ` (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)))"
using f10 by (smt (z3) DiffI dang_def image_eqI image_set_diff inj_morph_def old.sum.simps(5)) }
ultimately show "(λs. case s of Inl b ⇒ Inl (src G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ src (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (src (rule_rhs r) b)) else Inr (src (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) ⊆ nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))"
using f8 f7 f6 f5 f4 by (smt (z3) Diff_subset Un_iff image_eqI)
qed
lemma "⟦wf_graph G; wf_rule r; wf_match G r m⟧ ⟹ trg (rule_apply G r m) ` edges (rule_apply G r m) ⊆ nodes (rule_apply G r m)"
apply (simp add: rule_apply_def glue_def po_def wf_match_def wf_morph_def)
apply safe
apply (smt (z3) DiffI dang_def image_iff image_set_diff image_subset_iff inj_morph_def old.sum.simps(5) wf_gr_trg)
apply clarsimp
apply (rule conjI)
apply (metis (full_types) DiffD2 DiffI imageI inc_morph_def inj_image_mem_iff inj_morph_def wf_rule_def)
by (metis DiffI image_eqI image_subset_iff wf_gr_trg wf_rule_def)
lemma rule_apply_trg_pres[simp]:
"⟦wf_graph G; wf_rule r; wf_match G r m⟧ ⟹ trg (rule_apply G r m) ` edges (rule_apply G r m) ⊆ nodes (rule_apply G r m)"
apply (simp add: rule_apply_def glue_def po_def)
proof -
assume a1: "wf_rule r"
assume a2: "wf_match G r m"
assume a3: "wf_graph G"
obtain bb :: "'b set ⇒ ('b ⇒ 'b + 'b) ⇒ 'b + 'b ⇒ 'b" where
"∀x0 x1 x2. (∃v3. x2 = x1 v3 ∧ v3 ∈ x0) = (x2 = x1 (bb x0 x1 x2) ∧ bb x0 x1 x2 ∈ x0)"
by moura
then have f4: "∀s f B. s ∉ f ` B ∨ s = f (bb B f s) ∧ bb B f s ∈ B"
by auto
obtain ss :: "('b + 'b) set ⇒ ('b + 'b ⇒ 'a + 'a) ⇒ 'a + 'a ⇒ 'b + 'b" where
"∀x0 x1 x2. (∃v3. x2 = x1 v3 ∧ v3 ∈ x0) = (x2 = x1 (ss x0 x1 x2) ∧ ss x0 x1 x2 ∈ x0)"
by moura
then have f5: "∀s f S. s ∉ f ` S ∨ s = f (ss S f s) ∧ ss S f s ∈ S"
by (meson imageE)
obtain ssa :: "('a + 'a) set ⇒ ('a + 'a) set ⇒ 'a + 'a" where
"∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ x0) = (ssa x0 x1 ∈ x1 ∧ ssa x0 x1 ∉ x0)"
by moura
then have f6: "∀S Sa. (¬ S ⊆ Sa ∨ (∀s. s ∉ S ∨ s ∈ Sa)) ∧ (S ⊆ Sa ∨ ssa Sa S ∈ S ∧ ssa Sa S ∉ Sa)"
by blast
have f7: "∀a A Aa. (a::'a) ∉ A ∨ a ∈ Aa ∨ a ∈ A - Aa"
by force
obtain mm :: "('a, 'b, 'c, 'd) rule ⇒ ('a, 'b) morph" where
"∀x0. (∃v1. wf_morph v1 (rule_int x0) (rule_rhs x0) ∧ inc_morph v1 (rule_int x0) (rule_rhs x0)) = (wf_morph (mm x0) (rule_int x0) (rule_rhs x0) ∧ inc_morph (mm x0) (rule_int x0) (rule_rhs x0))"
by moura
then obtain mma :: "('a, 'b, 'c, 'd) rule ⇒ ('a, 'b) morph" where
f8: "wf_graph (rule_lhs r) ∧ wf_graph (rule_int r) ∧ wf_graph (rule_rhs r) ∧ wf_morph (mma r) (rule_int r) (rule_lhs r) ∧ inc_morph (mma r) (rule_int r) (rule_lhs r) ∧ wf_morph (mm r) (rule_int r) (rule_rhs r) ∧ inc_morph (mm r) (rule_int r) (rule_rhs r)"
using a1 wf_rule_def by moura
have f9: "∀s f a A. (s::'a + 'a) ≠ f (a::'a) ∨ a ∉ A ∨ s ∈ f ` A"
by blast
have f10: "wf_morph m (rule_lhs r) G ∧ inj_morph m ∧ dang r G m"
using a2 by (simp add: wf_match_def)
then have f11: "(∀b. b ∉ edges (rule_lhs r) ∨ morph_edge m b ∈ edges G ∧ morph_node m (src (rule_lhs r) b) = src G (morph_edge m b) ∧ morph_node m (trg (rule_lhs r) b) = trg G (morph_edge m b) ∧ me (rule_lhs r) b = me G (morph_edge m b)) ∧ (∀a. a ∉ nodes (rule_lhs r) ∨ morph_node m a ∈ nodes G ∧ mv (rule_lhs r) a = mv G (morph_node m a))"
by (simp add: wf_morph_def)
have f12: "(∀a. a ∉ nodes (rule_int r) ∨ a ∈ nodes (rule_lhs r) ∧ morph_node (mma r) a = a) ∧ (∀b. b ∉ edges (rule_int r) ∨ b ∈ edges (rule_lhs r) ∧ morph_edge (mma r) b = b)"
using f8 by (simp add: inc_morph_def)
{ assume "trg G (bb (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) Inl (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∈ trg G ` edges G"
moreover
{ assume "trg G (bb (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) Inl (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∈ nodes G - (morph_node m ` nodes (rule_lhs r) - morph_node m ` nodes (rule_int r))"
moreover
{ assume "trg G (bb (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) Inl (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∈ nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) ∧ (case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (trg G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ∉ Inl ` (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)))"
then have "ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∈ Inr ` (edges (rule_rhs r) - edges (rule_int r)) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inl ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) ∧ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inr ` (edges (rule_rhs r) - edges (rule_int r))"
using f9 f4 by (smt (z3) old.sum.simps(5)) }
ultimately have "ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∈ Inr ` (edges (rule_rhs r) - edges (rule_int r)) ∨ (case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (trg G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ∈ Inl ` (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r))) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inl ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) ∧ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inr ` (edges (rule_rhs r) - edges (rule_int r))"
using f10 by (smt (z3) image_set_diff inj_morph_def) }
ultimately have "(ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ≠ Inl (bb (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) Inl (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∨ bb (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) Inl (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))))) ∉ edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∈ Inr ` (edges (rule_rhs r) - edges (rule_int r)) ∨ (case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (trg G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ∈ Inl ` (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r))) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inl ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r))) ∧ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ Inr ` (edges (rule_rhs r) - edges (rule_int r))"
using f10 f7 a3 by (meson dang_def subset_iff wf_gr_trg) }
moreover
{ assume "ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∈ Inr ` (edges (rule_rhs r) - edges (rule_int r))"
moreover
{ assume "(ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) = Inr (bb (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∧ bb (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))))) ∈ edges (rule_rhs r) - edges (rule_int r)) ∧ (bb (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))))) ∉ edges (rule_rhs r) ∨ bb (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))))) ∈ edges (rule_int r) ∨ trg (rule_rhs r) (bb (edges (rule_rhs r) - edges (rule_int r)) Inr (ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))))) ∉ nodes (rule_int r))"
then have "(case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (trg G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ∈ Inr ` (nodes (rule_rhs r) - nodes (rule_int r))"
using f8 f7 by (smt (z3) DiffD2 Diff_subset image_eqI old.sum.simps(6) subset_iff wf_gr_trg)
then have "(ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))) ∈ Inr ` (nodes (rule_rhs r) - nodes (rule_int r)) ∨ ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))) ∈ Inl ` (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)))) ∨ ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))) ≠ (case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (trg G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))"
by (smt (z3)) }
ultimately have "(case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (trg G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ∈ Inl ` (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r))) ∨ (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))) ∈ Inr ` (nodes (rule_rhs r) - nodes (rule_int r)) ∨ ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))) ∈ Inl ` (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)))) ∨ ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r)))) ≠ (case ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) of Inl b ⇒ Inl (trg G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ∨ ss (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b))) (ssa (nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))) (case_sum (λb. Inl (trg G b)) (λb. if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))))) ∉ edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))"
using f12 f11 f10 f7 f4 by (smt (z3) DiffD2 image_eqI image_set_diff inj_morph_def old.sum.simps(6)) }
ultimately show "(λs. case s of Inl b ⇒ Inl (trg G b) | Inr b ⇒ if b ∈ edges (rule_rhs r) ∧ b ∉ edges (rule_int r) ∧ trg (rule_rhs r) b ∈ nodes (rule_int r) then Inl (morph_node m (trg (rule_rhs r) b)) else Inr (trg (rule_rhs r) b)) ` (edges G - morph_edge m ` (edges (rule_lhs r) - edges (rule_int r)) |+| (edges (rule_rhs r) - edges (rule_int r))) ⊆ nodes G - morph_node m ` (nodes (rule_lhs r) - nodes (rule_int r)) |+| (nodes (rule_rhs r) - nodes (rule_int r))"
using f6 f5 f4 by (smt (z3) Diff_subset UnCI UnE image_eqI subset_iff)
qed
lemma "⟦wf_graph G; wf_rule r; wf_match G r m⟧ ⟹ wf_graph (rule_apply G r m)"
by (simp add: wf_graph_def)
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment