[STATEMENT]
lemma (in valid_unMultigraph) connectivity_split:
  assumes "connected" "\<not>valid_unMultigraph.connected (del_unEdge v w v' G)"
          "(v,w,v')\<in>E"
  obtains G1 G2 where
         "nodes G1={n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}"
         and "edges G1={(n,e,n'). (n,e,n')\<in>edges (del_unEdge v w v' G)
            \<and> n\<in>nodes G1 \<and> n'\<in>nodes G1}"
         and "nodes G2={n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}"
         and "edges G2={(n,e,n'). (n,e,n')\<in>edges (del_unEdge v w v' G)
            \<and> n\<in>nodes G2 \<and> n'\<in>nodes G2}"
         and "edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)"
         and "edges G1 \<inter> edges G2={}"
         and "nodes G1 \<union> nodes G2=nodes (del_unEdge v w v' G)"
         and "nodes G1 \<inter> nodes G2={}"
         and "valid_unMultigraph G1"
         and "valid_unMultigraph G2"
         and "valid_unMultigraph.connected G1"
         and "valid_unMultigraph.connected G2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have valid0:"valid_graph (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph (del_unEdge v w v' G)
[PROOF STEP]
using valid_graph_axioms
[PROOF STATE]
proof (prove)
using this:
valid_graph G

goal (1 subgoal):
 1. valid_graph (del_unEdge v w v' G)
[PROOF STEP]
by (metis del_undirected delete_edge_valid)
[PROOF STATE]
proof (state)
this:
valid_graph (del_unEdge v w v' G)

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have valid0':"valid_unMultigraph (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v w v' G)
[PROOF STEP]
using valid_unMultigraph_axioms
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G

goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v w v' G)
[PROOF STEP]
by (metis del_unEdge_valid)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge v w v' G)

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain G1_nodes where G1_nodes:"G1_nodes=
      {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>G1_nodes. G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
[PROOF STEP]
obtain G1 where G1:"G1=
      \<lparr>nodes=G1_nodes, edges={(n,e,n'). (n,e,n')\<in>edges (del_unEdge v w v' G)
      \<and> n\<in>G1_nodes \<and> n'\<in>G1_nodes}\<rparr>"
[PROOF STATE]
proof (prove)
using this:
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}

goal (1 subgoal):
 1. (\<And>G1. G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain G2_nodes where G2_nodes:"G2_nodes=
      {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>G2_nodes. G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
[PROOF STEP]
obtain G2 where G2:"G2=
      \<lparr>nodes=G2_nodes, edges={(n,e,n'). (n,e,n')\<in>edges (del_unEdge v w v' G)
      \<and> n\<in>G2_nodes \<and> n'\<in>G2_nodes}\<rparr>"
[PROOF STATE]
proof (prove)
using this:
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}

goal (1 subgoal):
 1. (\<And>G2. G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have valid_G1:"valid_unMultigraph G1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph G1
[PROOF STEP]
using G1 valid_unMultigraph.corres[OF valid0'] valid_unMultigraph.no_id[OF valid0']
[PROOF STATE]
proof (prove)
using this:
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
((?v, ?w, ?u') \<in> edges (del_unEdge v w v' G)) = ((?u', ?w, ?v) \<in> edges (del_unEdge v w v' G))
(?v, ?w, ?v) \<notin> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. valid_unMultigraph G1
[PROOF STEP]
by (unfold_locales,auto)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph G1

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence valid_G1':"valid_graph G1"
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G1

goal (1 subgoal):
 1. valid_graph G1
[PROOF STEP]
using valid_unMultigraph_def
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G1
valid_unMultigraph ?G \<equiv> valid_graph ?G \<and> valid_unMultigraph_axioms ?G

goal (1 subgoal):
 1. valid_graph G1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph G1

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have valid_G2:"valid_unMultigraph G2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph G2
[PROOF STEP]
using G2 valid_unMultigraph.corres[OF valid0'] valid_unMultigraph.no_id[OF valid0']
[PROOF STATE]
proof (prove)
using this:
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
((?v, ?w, ?u') \<in> edges (del_unEdge v w v' G)) = ((?u', ?w, ?v) \<in> edges (del_unEdge v w v' G))
(?v, ?w, ?v) \<notin> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. valid_unMultigraph G2
[PROOF STEP]
by (unfold_locales,auto)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph G2

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence valid_G2': "valid_graph G2"
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G2

goal (1 subgoal):
 1. valid_graph G2
[PROOF STEP]
using valid_unMultigraph_def
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G2
valid_unMultigraph ?G \<equiv> valid_graph ?G \<and> valid_unMultigraph_axioms ?G

goal (1 subgoal):
 1. valid_graph G2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph G2

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "nodes G1={n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
[PROOF STEP]
using G1_nodes G1
[PROOF STATE]
proof (prove)
using this:
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>

goal (1 subgoal):
 1. nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "edges G1={(n,e,n'). (n,e,n')\<in>edges (del_unEdge v w v' G)
                 \<and> n\<in>nodes G1 \<and> n'\<in>nodes G1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}
[PROOF STEP]
using G1_nodes G1
[PROOF STATE]
proof (prove)
using this:
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>

goal (1 subgoal):
 1. edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "nodes G2={n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
[PROOF STEP]
using G2_nodes G2
[PROOF STATE]
proof (prove)
using this:
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>

goal (1 subgoal):
 1. nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "edges G2={(n,e,n'). (n,e,n')\<in>edges (del_unEdge v w v' G)
                 \<and> n\<in>nodes G2 \<and> n'\<in>nodes G2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}
[PROOF STEP]
using G2_nodes G2
[PROOF STATE]
proof (prove)
using this:
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>

goal (1 subgoal):
 1. edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "nodes G1 \<union> nodes G2=nodes (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
assume "nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G)"
[PROOF STATE]
proof (state)
this:
nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "nodes G1 \<subseteq> nodes (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes G1 \<subseteq> nodes (del_unEdge v w v' G)
[PROOF STEP]
using valid_graph.is_path_memb[OF valid0] G1 G1_nodes
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) ?v ?p ?v' \<Longrightarrow> ?v \<in> nodes (del_unEdge v w v' G) \<and> ?v' \<in> nodes (del_unEdge v w v' G)
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}

goal (1 subgoal):
 1. nodes G1 \<subseteq> nodes (del_unEdge v w v' G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes G1 \<subseteq> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nodes G1 \<subseteq> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "nodes G2 \<subseteq> nodes (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes G2 \<subseteq> nodes (del_unEdge v w v' G)
[PROOF STEP]
using valid_graph.is_path_memb[OF valid0] G2 G2_nodes
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) ?v ?p ?v' \<Longrightarrow> ?v \<in> nodes (del_unEdge v w v' G) \<and> ?v' \<in> nodes (del_unEdge v w v' G)
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}

goal (1 subgoal):
 1. nodes G2 \<subseteq> nodes (del_unEdge v w v' G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes G2 \<subseteq> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G)
nodes G1 \<subseteq> nodes (del_unEdge v w v' G)
nodes G2 \<subseteq> nodes (del_unEdge v w v' G)
[PROOF STEP]
obtain n where n:
          "n\<in>nodes (del_unEdge v w v' G)" "n\<notin>nodes G1" "n\<notin>nodes G2"
[PROOF STATE]
proof (prove)
using this:
nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G)
nodes G1 \<subseteq> nodes (del_unEdge v w v' G)
nodes G2 \<subseteq> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in> nodes (del_unEdge v w v' G); n \<notin> nodes G1; n \<notin> nodes G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> nodes (del_unEdge v w v' G)
n \<notin> nodes G1
n \<notin> nodes G2

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
hence n_neg_v : "\<not>(\<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v)" and
            n_neg_v': "\<not>(\<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v')"
[PROOF STATE]
proof (prove)
using this:
n \<in> nodes (del_unEdge v w v' G)
n \<notin> nodes G1
n \<notin> nodes G2

goal (1 subgoal):
 1. \<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v &&& \<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'
[PROOF STEP]
using G1 G1_nodes G2 G2_nodes
[PROOF STATE]
proof (prove)
using this:
n \<in> nodes (del_unEdge v w v' G)
n \<notin> nodes G1
n \<notin> nodes G2
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}

goal (1 subgoal):
 1. \<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v &&& \<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v
\<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
hence "n\<noteq>v"
[PROOF STATE]
proof (prove)
using this:
\<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v
\<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'

goal (1 subgoal):
 1. n \<noteq> v
[PROOF STEP]
by (metis n(1) valid0 valid_graph.is_path_simps(1))
[PROOF STATE]
proof (state)
this:
n \<noteq> v

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> v
[PROOF STEP]
obtain nvs where nvs: "is_path n nvs v"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> v

goal (1 subgoal):
 1. (\<And>nvs. is_path n nvs v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>connected\<close>
[PROOF STATE]
proof (prove)
using this:
n \<noteq> v
local.connected

goal (1 subgoal):
 1. (\<And>nvs. is_path n nvs v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis E_validD(1) assms(3) connected_def del_UnEdge_node n(1))
[PROOF STATE]
proof (state)
this:
is_path n nvs v

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_path n nvs v
[PROOF STEP]
obtain nvs' where nvs': "nvs'=takeWhile (\<lambda>x. x\<noteq>(v,w,v')\<and>x\<noteq>(v',w,v)) nvs"
[PROOF STATE]
proof (prove)
using this:
is_path n nvs v

goal (1 subgoal):
 1. (\<And>nvs'. nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have nvs_nvs':"nvs=nvs'@dropWhile (\<lambda>x. x\<noteq>(v,w,v')\<and>x\<noteq>(v',w,v)) nvs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nvs = nvs' @ dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs
[PROOF STEP]
using nvs' takeWhile_dropWhile_id
[PROOF STATE]
proof (prove)
using this:
nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs
takeWhile ?P ?xs @ dropWhile ?P ?xs = ?xs

goal (1 subgoal):
 1. nvs = nvs' @ dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nvs = nvs' @ dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs
nvs = nvs' @ dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs
[PROOF STEP]
obtain n' where is_path_nvs': "is_path n nvs' n'"
          and "is_path n' (dropWhile (\<lambda>x. x\<noteq>(v,w,v')\<and>x\<noteq>(v',w,v)) nvs) v"
[PROOF STATE]
proof (prove)
using this:
nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs
nvs = nvs' @ dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>is_path n nvs' n'; is_path n' (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nvs is_path_split[of n nvs' "dropWhile (\<lambda>x. x\<noteq>(v,w,v')\<and>x\<noteq>(v',w,v)) nvs"]
[PROOF STATE]
proof (prove)
using this:
nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs
nvs = nvs' @ dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs
is_path n nvs v
is_path n (nvs' @ dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) ?v' = (\<exists>u. is_path n nvs' u \<and> is_path u (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) ?v')

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>is_path n nvs' n'; is_path n' (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path n nvs' n'
is_path n' (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) v

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "n'=v \<or> n'=v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' = v \<or> n' = v'
[PROOF STEP]
proof (cases "dropWhile (\<lambda>x. x\<noteq>(v,w,v')\<and>x\<noteq>(v',w,v)) nvs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = [] \<Longrightarrow> n' = v \<or> n' = v'
 2. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = []

goal (2 subgoals):
 1. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = [] \<Longrightarrow> n' = v \<or> n' = v'
 2. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
hence "nvs=nvs'"
[PROOF STATE]
proof (prove)
using this:
dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = []

goal (1 subgoal):
 1. nvs = nvs'
[PROOF STEP]
using nvs_nvs'
[PROOF STATE]
proof (prove)
using this:
dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = []
nvs = nvs' @ dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. nvs = nvs'
[PROOF STEP]
by (metis append_Nil2)
[PROOF STATE]
proof (state)
this:
nvs = nvs'

goal (2 subgoals):
 1. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = [] \<Longrightarrow> n' = v \<or> n' = v'
 2. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
hence "n'=v"
[PROOF STATE]
proof (prove)
using this:
nvs = nvs'

goal (1 subgoal):
 1. n' = v
[PROOF STEP]
using  nvs is_path_nvs' path_end
[PROOF STATE]
proof (prove)
using this:
nvs = nvs'
is_path n nvs v
is_path n nvs' n'
\<lbrakk>?ps \<noteq> []; is_path ?v ?ps ?v'\<rbrakk> \<Longrightarrow> ?v' = snd (snd (last ?ps))

goal (1 subgoal):
 1. n' = v
[PROOF STEP]
by (metis (mono_tags) is_path.simps(1))
[PROOF STATE]
proof (state)
this:
n' = v

goal (2 subgoals):
 1. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = [] \<Longrightarrow> n' = v \<or> n' = v'
 2. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n' = v

goal (1 subgoal):
 1. n' = v \<or> n' = v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n' = v \<or> n' = v'

goal (1 subgoal):
 1. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = x # xs

goal (1 subgoal):
 1. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
hence "dropWhile (\<lambda>x. x\<noteq>(v,w,v')\<and>x\<noteq>(v',w,v)) nvs\<noteq>[]"
[PROOF STATE]
proof (prove)
using this:
dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = x # xs

goal (1 subgoal):
 1. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs \<noteq> []

goal (1 subgoal):
 1. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
hence "hd (dropWhile (\<lambda>x. x\<noteq>(v,w,v')\<and>x\<noteq>(v',w,v)) nvs)=(v,w,v')
                 \<or> hd (dropWhile (\<lambda>x. x\<noteq>(v,w,v')\<and>x\<noteq>(v',w,v)) nvs)=(v',w,v)"
[PROOF STATE]
proof (prove)
using this:
dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs \<noteq> []

goal (1 subgoal):
 1. hd (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) = (v, w, v') \<or> hd (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) = (v', w, v)
[PROOF STEP]
by (metis (lifting, full_types) hd_dropWhile)
[PROOF STATE]
proof (state)
this:
hd (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) = (v, w, v') \<or> hd (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) = (v', w, v)

goal (1 subgoal):
 1. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
hence "x=(v,w,v')\<or>x=(v',w,v)"
[PROOF STATE]
proof (prove)
using this:
hd (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) = (v, w, v') \<or> hd (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) = (v', w, v)

goal (1 subgoal):
 1. x = (v, w, v') \<or> x = (v', w, v)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
hd (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) = (v, w, v') \<or> hd (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) = (v', w, v)
dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = x # xs

goal (1 subgoal):
 1. x = (v, w, v') \<or> x = (v', w, v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (v, w, v') \<or> x = (v', w, v)

goal (1 subgoal):
 1. \<And>a list. dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs = a # list \<Longrightarrow> n' = v \<or> n' = v'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = (v, w, v') \<or> x = (v', w, v)

goal (1 subgoal):
 1. n' = v \<or> n' = v'
[PROOF STEP]
using \<open>is_path n' (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) v\<close>
[PROOF STATE]
proof (prove)
using this:
x = (v, w, v') \<or> x = (v', w, v)
is_path n' (dropWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) v

goal (1 subgoal):
 1. n' = v \<or> n' = v'
[PROOF STEP]
by (metis Cons  is_path.simps(2))
[PROOF STATE]
proof (state)
this:
n' = v \<or> n' = v'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n' = v \<or> n' = v'

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n' = v \<or> n' = v'

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "valid_graph.is_path (del_unEdge v w v' G) n nvs' n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) n nvs' n'
[PROOF STEP]
using is_path_nvs' nvs'
[PROOF STATE]
proof (prove)
using this:
is_path n nvs' n'
nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) n nvs' n'
[PROOF STEP]
proof (induct nvs' arbitrary:n nvs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n nvs. \<lbrakk>is_path n [] n'; [] = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n [] n'
 2. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
is_path n [] n'
[] = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (2 subgoals):
 1. \<And>n nvs. \<lbrakk>is_path n [] n'; [] = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n [] n'
 2. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_path n [] n'
[] = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) n [] n'
[PROOF STEP]
by (metis del_UnEdge_node is_path.simps(1) valid0 valid_graph.is_path_simps(1))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n [] n'

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_path ?n xs n'; xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) ?nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) ?n xs n'
is_path n (x # xs) n'
x # xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
obtain x1 x2 x3 where x:"x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
hence "is_path x3 xs n'"
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. is_path x3 xs n'
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)
\<lbrakk>is_path ?n xs n'; xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) ?nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) ?n xs n'
is_path n (x # xs) n'
x # xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. is_path x3 xs n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path x3 xs n'

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path x3 xs n'

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
have "xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) (tl nvs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) (tl nvs)
[PROOF STEP]
using \<open>x # xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<close>
[PROOF STATE]
proof (prove)
using this:
x # xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) (tl nvs)
[PROOF STEP]
by (metis (lifting, no_types) append_Cons list.distinct(1) takeWhile.simps(2)
                takeWhile_dropWhile_id list.sel(3))
[PROOF STATE]
proof (state)
this:
xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) (tl nvs)

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path x3 xs n'
xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) (tl nvs)
[PROOF STEP]
have "valid_graph.is_path (del_unEdge v w v' G) x3 xs n'"
[PROOF STATE]
proof (prove)
using this:
is_path x3 xs n'
xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) (tl nvs)

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) x3 xs n'
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
is_path x3 xs n'
xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) (tl nvs)
\<lbrakk>is_path ?n xs n'; xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) ?nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) ?n xs n'
is_path n (x # xs) n'
x # xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) x3 xs n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs n'

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs n'

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
have "x\<noteq>(v,w,v') \<and> x\<noteq>(v',w,v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)
[PROOF STEP]
using Cons(3) set_takeWhileD[of x "(\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v))" nvs]
[PROOF STATE]
proof (prove)
using this:
x # xs = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs
x \<in> set (takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs) \<Longrightarrow> x \<in> set nvs \<and> x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)

goal (1 subgoal):
 1. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)
[PROOF STEP]
by (metis List.set_simps(2) insertI1)
[PROOF STATE]
proof (state)
this:
x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
hence "x\<in>edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)

goal (1 subgoal):
 1. x \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
by (metis Cons.prems(1) del_UnEdge_frame is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
x \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>a nvs' n nvs. \<lbrakk>\<And>n nvs. \<lbrakk>is_path n nvs' n'; nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n nvs' n'; is_path n (a # nvs') n'; a # nvs' = takeWhile (\<lambda>x. x \<noteq> (v, w, v') \<and> x \<noteq> (v', w, v)) nvs\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v w v' G) n (a # nvs') n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs n'
x \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs n'
x \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) n (x # xs) n'
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs n'
x \<in> edges (del_unEdge v w v' G)
x = (x1, x2, x3)

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) n (x # xs) n'
[PROOF STEP]
by (metis Cons.prems(1) is_path.simps(2) valid0 valid_graph.is_path.simps(2))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n (x # xs) n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n nvs' n'

goal (1 subgoal):
 1. nodes G1 \<union> nodes G2 \<noteq> nodes (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n' = v \<or> n' = v'
valid_graph.is_path (del_unEdge v w v' G) n nvs' n'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n' = v \<or> n' = v'
valid_graph.is_path (del_unEdge v w v' G) n nvs' n'

goal (1 subgoal):
 1. False
[PROOF STEP]
using n_neg_v n_neg_v'
[PROOF STATE]
proof (prove)
using this:
n' = v \<or> n' = v'
valid_graph.is_path (del_unEdge v w v' G) n nvs' n'
\<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v
\<nexists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "nodes G1 \<inter> nodes G2={}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes G1 \<inter> nodes G2 = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nodes G1 \<inter> nodes G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "nodes G1 \<inter> nodes G2 \<noteq> {}"
[PROOF STATE]
proof (state)
this:
nodes G1 \<inter> nodes G2 \<noteq> {}

goal (1 subgoal):
 1. nodes G1 \<inter> nodes G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nodes G1 \<inter> nodes G2 \<noteq> {}
[PROOF STEP]
obtain n where n:"n\<in>nodes G1" "n\<in>nodes G2"
[PROOF STATE]
proof (prove)
using this:
nodes G1 \<inter> nodes G2 \<noteq> {}

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in> nodes G1; n \<in> nodes G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> nodes G1
n \<in> nodes G2

goal (1 subgoal):
 1. nodes G1 \<inter> nodes G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> nodes G1
n \<in> nodes G2
[PROOF STEP]
obtain nvs nv's where
          nvs  : "valid_graph.is_path (del_unEdge v w v' G) n nvs v" and
          nv's : "valid_graph.is_path (del_unEdge v w v' G) n nv's v'"
[PROOF STATE]
proof (prove)
using this:
n \<in> nodes G1
n \<in> nodes G2

goal (1 subgoal):
 1. (\<And>nvs nv's. \<lbrakk>valid_graph.is_path (del_unEdge v w v' G) n nvs v; valid_graph.is_path (del_unEdge v w v' G) n nv's v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G1 G2 G1_nodes G2_nodes
[PROOF STATE]
proof (prove)
using this:
n \<in> nodes G1
n \<in> nodes G2
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}

goal (1 subgoal):
 1. (\<And>nvs nv's. \<lbrakk>valid_graph.is_path (del_unEdge v w v' G) n nvs v; valid_graph.is_path (del_unEdge v w v' G) n nv's v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n nvs v
valid_graph.is_path (del_unEdge v w v' G) n nv's v'

goal (1 subgoal):
 1. nodes G1 \<inter> nodes G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
hence "valid_graph.is_path (del_unEdge v w v' G) v ((rev_path nvs)@nv's) v'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n nvs v
valid_graph.is_path (del_unEdge v w v' G) n nv's v'

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) v (rev_path nvs @ nv's) v'
[PROOF STEP]
using valid_unMultigraph.is_path_rev[OF valid0'] valid_graph.is_path_split[OF valid0]
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n nvs v
valid_graph.is_path (del_unEdge v w v' G) n nv's v'
valid_graph.is_path (del_unEdge v w v' G) ?v' (rev_path ?ps) ?v = valid_graph.is_path (del_unEdge v w v' G) ?v ?ps ?v'
valid_graph.is_path (del_unEdge v w v' G) ?v (?p1.0 @ ?p2.0) ?v' = (\<exists>u. valid_graph.is_path (del_unEdge v w v' G) ?v ?p1.0 u \<and> valid_graph.is_path (del_unEdge v w v' G) u ?p2.0 ?v')

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) v (rev_path nvs @ nv's) v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) v (rev_path nvs @ nv's) v'

goal (1 subgoal):
 1. nodes G1 \<inter> nodes G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
hence "valid_unMultigraph.connected (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) v (rev_path nvs @ nv's) v'

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v w v' G)
[PROOF STEP]
by (metis assms(1) del_unEdge_connectivity)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.connected (del_unEdge v w v' G)

goal (1 subgoal):
 1. nodes G1 \<inter> nodes G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph.connected (del_unEdge v w v' G)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis assms(2))
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nodes G1 \<inter> nodes G2 = {}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nodes G1 \<inter> nodes G2 = {}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
assume "edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (state)
this:
edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "edges G1 \<subseteq> edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges G1 \<subseteq> edges (del_unEdge v w v' G)
[PROOF STEP]
using G1
[PROOF STATE]
proof (prove)
using this:
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>

goal (1 subgoal):
 1. edges G1 \<subseteq> edges (del_unEdge v w v' G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges G1 \<subseteq> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
edges G1 \<subseteq> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "edges G2 \<subseteq> edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges G2 \<subseteq> edges (del_unEdge v w v' G)
[PROOF STEP]
using G2
[PROOF STATE]
proof (prove)
using this:
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>

goal (1 subgoal):
 1. edges G2 \<subseteq> edges (del_unEdge v w v' G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges G2 \<subseteq> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G)
edges G1 \<subseteq> edges (del_unEdge v w v' G)
edges G2 \<subseteq> edges (del_unEdge v w v' G)
[PROOF STEP]
obtain n e n' where
          nen':
          "(n,e,n')\<in>edges (del_unEdge v w v' G)"
          "(n,e,n')\<notin>edges G1" "(n,e,n')\<notin>edges G2"
[PROOF STATE]
proof (prove)
using this:
edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G)
edges G1 \<subseteq> edges (del_unEdge v w v' G)
edges G2 \<subseteq> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (\<And>n e n'. \<lbrakk>(n, e, n') \<in> edges (del_unEdge v w v' G); (n, e, n') \<notin> edges G1; (n, e, n') \<notin> edges G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(n, e, n') \<in> edges (del_unEdge v w v' G)
(n, e, n') \<notin> edges G1
(n, e, n') \<notin> edges G2

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(n, e, n') \<in> edges (del_unEdge v w v' G)
(n, e, n') \<notin> edges G1
(n, e, n') \<notin> edges G2

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "n\<in>nodes (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> nodes (del_unEdge v w v' G)
[PROOF STEP]
by (metis nen'(1) valid0 valid_graph.E_validD(1))
[PROOF STATE]
proof (state)
this:
n \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "n'\<in>nodes (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' \<in> nodes (del_unEdge v w v' G)
[PROOF STEP]
by (metis nen'(1) valid0 valid_graph.E_validD(2))
[PROOF STATE]
proof (state)
this:
n' \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(n, e, n') \<in> edges (del_unEdge v w v' G)
(n, e, n') \<notin> edges G1
(n, e, n') \<notin> edges G2
n \<in> nodes (del_unEdge v w v' G)
n' \<in> nodes (del_unEdge v w v' G)
[PROOF STEP]
have "(n\<in>nodes G1 \<and> n'\<in>nodes G2)\<or>(n\<in>nodes G2\<and>n'\<in>nodes G1)"
[PROOF STATE]
proof (prove)
using this:
(n, e, n') \<in> edges (del_unEdge v w v' G)
(n, e, n') \<notin> edges G1
(n, e, n') \<notin> edges G2
n \<in> nodes (del_unEdge v w v' G)
n' \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. n \<in> nodes G1 \<and> n' \<in> nodes G2 \<or> n \<in> nodes G2 \<and> n' \<in> nodes G1
[PROOF STEP]
using G1 G2 \<open>nodes G1 \<union> nodes G2=nodes (del_unEdge v w v' G)\<close>
[PROOF STATE]
proof (prove)
using this:
(n, e, n') \<in> edges (del_unEdge v w v' G)
(n, e, n') \<notin> edges G1
(n, e, n') \<notin> edges G2
n \<in> nodes (del_unEdge v w v' G)
n' \<in> nodes (del_unEdge v w v' G)
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. n \<in> nodes G1 \<and> n' \<in> nodes G2 \<or> n \<in> nodes G2 \<and> n' \<in> nodes G1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> nodes G1 \<and> n' \<in> nodes G2 \<or> n \<in> nodes G2 \<and> n' \<in> nodes G1

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<in> nodes G1 \<and> n' \<in> nodes G2 \<or> n \<in> nodes G2 \<and> n' \<in> nodes G1

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "n\<in>nodes G1 \<Longrightarrow> n'\<in>nodes G2 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "n\<in>nodes G1" "n'\<in>nodes G2"
[PROOF STATE]
proof (state)
this:
n \<in> nodes G1
n' \<in> nodes G2

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> nodes G1
n' \<in> nodes G2
[PROOF STEP]
obtain nvs nv's where
              nvs  : "valid_graph.is_path (del_unEdge v w v' G) n nvs v" and
              nv's : "valid_graph.is_path (del_unEdge v w v' G) n' nv's v'"
[PROOF STATE]
proof (prove)
using this:
n \<in> nodes G1
n' \<in> nodes G2

goal (1 subgoal):
 1. (\<And>nvs nv's. \<lbrakk>valid_graph.is_path (del_unEdge v w v' G) n nvs v; valid_graph.is_path (del_unEdge v w v' G) n' nv's v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G1 G2 G1_nodes G2_nodes
[PROOF STATE]
proof (prove)
using this:
n \<in> nodes G1
n' \<in> nodes G2
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}

goal (1 subgoal):
 1. (\<And>nvs nv's. \<lbrakk>valid_graph.is_path (del_unEdge v w v' G) n nvs v; valid_graph.is_path (del_unEdge v w v' G) n' nv's v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n nvs v
valid_graph.is_path (del_unEdge v w v' G) n' nv's v'

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "valid_graph.is_path (del_unEdge v w v' G) v
                  ((rev_path nvs)@(n,e,n')#nv's) v'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n nvs v
valid_graph.is_path (del_unEdge v w v' G) n' nv's v'

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) v (rev_path nvs @ (n, e, n') # nv's) v'
[PROOF STEP]
using valid_unMultigraph.is_path_rev[OF valid0'] valid_graph.is_path_split'[OF valid0]
                  \<open>(n,e,n')\<in>edges (del_unEdge v w v' G)\<close>
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n nvs v
valid_graph.is_path (del_unEdge v w v' G) n' nv's v'
valid_graph.is_path (del_unEdge v w v' G) ?v' (rev_path ?ps) ?v = valid_graph.is_path (del_unEdge v w v' G) ?v ?ps ?v'
valid_graph.is_path (del_unEdge v w v' G) ?v (?p1.0 @ (?u, ?w, ?u') # ?p2.0) ?v' = (valid_graph.is_path (del_unEdge v w v' G) ?v ?p1.0 ?u \<and> (?u, ?w, ?u') \<in> edges (del_unEdge v w v' G) \<and> valid_graph.is_path (del_unEdge v w v' G) ?u' ?p2.0 ?v')
(n, e, n') \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) v (rev_path nvs @ (n, e, n') # nv's) v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) v (rev_path nvs @ (n, e, n') # nv's) v'

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "valid_unMultigraph.connected (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) v (rev_path nvs @ (n, e, n') # nv's) v'

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v w v' G)
[PROOF STEP]
by (metis assms(1) del_unEdge_connectivity)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.connected (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph.connected (del_unEdge v w v' G)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis assms(2))
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
have "n\<in>nodes G2 \<Longrightarrow> n'\<in>nodes G1 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "n'\<in>nodes G1" "n\<in>nodes G2"
[PROOF STATE]
proof (state)
this:
n' \<in> nodes G1
n \<in> nodes G2

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n' \<in> nodes G1
n \<in> nodes G2
[PROOF STEP]
obtain n'vs nvs where
              n'vs  : "valid_graph.is_path (del_unEdge v w v' G) n' n'vs v" and
              nvs : "valid_graph.is_path (del_unEdge v w v' G) n nvs v'"
[PROOF STATE]
proof (prove)
using this:
n' \<in> nodes G1
n \<in> nodes G2

goal (1 subgoal):
 1. (\<And>n'vs nvs. \<lbrakk>valid_graph.is_path (del_unEdge v w v' G) n' n'vs v; valid_graph.is_path (del_unEdge v w v' G) n nvs v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G1 G2 G1_nodes G2_nodes
[PROOF STATE]
proof (prove)
using this:
n' \<in> nodes G1
n \<in> nodes G2
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}

goal (1 subgoal):
 1. (\<And>n'vs nvs. \<lbrakk>valid_graph.is_path (del_unEdge v w v' G) n' n'vs v; valid_graph.is_path (del_unEdge v w v' G) n nvs v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n' n'vs v
valid_graph.is_path (del_unEdge v w v' G) n nvs v'

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n' n'vs v
valid_graph.is_path (del_unEdge v w v' G) n nvs v'

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(n',e,n)\<in>edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n', e, n) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
by (metis nen'(1) valid0' valid_unMultigraph.corres)
[PROOF STATE]
proof (state)
this:
(n', e, n) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_graph.is_path (del_unEdge v w v' G) n' n'vs v
valid_graph.is_path (del_unEdge v w v' G) n nvs v'
(n', e, n) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
have "valid_graph.is_path (del_unEdge v w v' G) v
                  ((rev_path n'vs)@(n',e,n)#nvs) v'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n' n'vs v
valid_graph.is_path (del_unEdge v w v' G) n nvs v'
(n', e, n) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) v (rev_path n'vs @ (n', e, n) # nvs) v'
[PROOF STEP]
using valid_unMultigraph.is_path_rev[OF valid0'] valid_graph.is_path_split'[OF valid0]
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n' n'vs v
valid_graph.is_path (del_unEdge v w v' G) n nvs v'
(n', e, n) \<in> edges (del_unEdge v w v' G)
valid_graph.is_path (del_unEdge v w v' G) ?v' (rev_path ?ps) ?v = valid_graph.is_path (del_unEdge v w v' G) ?v ?ps ?v'
valid_graph.is_path (del_unEdge v w v' G) ?v (?p1.0 @ (?u, ?w, ?u') # ?p2.0) ?v' = (valid_graph.is_path (del_unEdge v w v' G) ?v ?p1.0 ?u \<and> (?u, ?w, ?u') \<in> edges (del_unEdge v w v' G) \<and> valid_graph.is_path (del_unEdge v w v' G) ?u' ?p2.0 ?v')

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) v (rev_path n'vs @ (n', e, n) # nvs) v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) v (rev_path n'vs @ (n', e, n) # nvs) v'

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "valid_unMultigraph.connected (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) v (rev_path n'vs @ (n', e, n) # nvs) v'

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v w v' G)
[PROOF STEP]
by (metis assms(1) del_unEdge_connectivity)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.connected (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph.connected (del_unEdge v w v' G)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis assms(2))
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. edges G1 \<union> edges G2 \<noteq> edges (del_unEdge v w v' G) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<in> nodes G1 \<and> n' \<in> nodes G2 \<or> n \<in> nodes G2 \<and> n' \<in> nodes G1
\<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False
\<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<in> nodes G1 \<and> n' \<in> nodes G2 \<or> n \<in> nodes G2 \<and> n' \<in> nodes G1
\<lbrakk>n \<in> nodes G1; n' \<in> nodes G2\<rbrakk> \<Longrightarrow> False
\<lbrakk>n \<in> nodes G2; n' \<in> nodes G1\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "edges G1 \<inter> edges G2={}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges G1 \<inter> edges G2 = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. edges G1 \<inter> edges G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "edges G1 \<inter> edges G2 \<noteq> {}"
[PROOF STATE]
proof (state)
this:
edges G1 \<inter> edges G2 \<noteq> {}

goal (1 subgoal):
 1. edges G1 \<inter> edges G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
edges G1 \<inter> edges G2 \<noteq> {}
[PROOF STEP]
obtain n e n' where "(n,e,n')\<in>edges G1" "(n,e,n')\<in>edges G2"
[PROOF STATE]
proof (prove)
using this:
edges G1 \<inter> edges G2 \<noteq> {}

goal (1 subgoal):
 1. (\<And>n e n'. \<lbrakk>(n, e, n') \<in> edges G1; (n, e, n') \<in> edges G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(n, e, n') \<in> edges G1
(n, e, n') \<in> edges G2

goal (1 subgoal):
 1. edges G1 \<inter> edges G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
hence "n\<in>nodes G1" "n\<in>nodes G2"
[PROOF STATE]
proof (prove)
using this:
(n, e, n') \<in> edges G1
(n, e, n') \<in> edges G2

goal (1 subgoal):
 1. n \<in> nodes G1 &&& n \<in> nodes G2
[PROOF STEP]
using G1 G2
[PROOF STATE]
proof (prove)
using this:
(n, e, n') \<in> edges G1
(n, e, n') \<in> edges G2
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>

goal (1 subgoal):
 1. n \<in> nodes G1 &&& n \<in> nodes G2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> nodes G1
n \<in> nodes G2

goal (1 subgoal):
 1. edges G1 \<inter> edges G2 \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
n \<in> nodes G1
n \<in> nodes G2

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>nodes G1 \<inter> nodes G2={}\<close>
[PROOF STATE]
proof (prove)
using this:
n \<in> nodes G1
n \<in> nodes G2
nodes G1 \<inter> nodes G2 = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
edges G1 \<inter> edges G2 = {}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
edges G1 \<inter> edges G2 = {}

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "valid_unMultigraph.connected G1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph.connected G1
[PROOF STEP]
unfolding valid_unMultigraph.connected_def[OF valid_G1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>nodes G1. \<forall>v'\<in>nodes G1. v \<noteq> v' \<longrightarrow> (\<exists>ps. valid_graph.is_path G1 v ps v')
[PROOF STEP]
proof (rule,rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
fix n n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
assume  n : "n \<in>nodes G1"
[PROOF STATE]
proof (state)
this:
n \<in> nodes G1

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
assume  n': "n'\<in>nodes G1"
[PROOF STATE]
proof (state)
this:
n' \<in> nodes G1

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
assume "n\<noteq>n'"
[PROOF STATE]
proof (state)
this:
n \<noteq> n'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
obtain ps where "valid_graph.is_path (del_unEdge v w v' G) n ps v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G1 G1_nodes n
[PROOF STATE]
proof (prove)
using this:
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
n \<in> nodes G1

goal (1 subgoal):
 1. (\<And>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n ps v

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
hence ps:"valid_graph.is_path G1 n ps v"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n ps v

goal (1 subgoal):
 1. valid_graph.is_path G1 n ps v
[PROOF STEP]
proof (induct ps arbitrary:n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. valid_graph.is_path (del_unEdge v w v' G) n [] v \<Longrightarrow> valid_graph.is_path G1 n [] v
 2. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n [] v

goal (2 subgoals):
 1. \<And>n. valid_graph.is_path (del_unEdge v w v' G) n [] v \<Longrightarrow> valid_graph.is_path G1 n [] v
 2. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n [] v

goal (2 subgoals):
 1. \<And>n. valid_graph.is_path (del_unEdge v w v' G) n [] v \<Longrightarrow> valid_graph.is_path G1 n [] v
 2. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
have "v\<in>nodes G1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> nodes G1
[PROOF STEP]
using G1 G1_nodes valid0
[PROOF STATE]
proof (prove)
using this:
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
valid_graph (del_unEdge v w v' G)

goal (1 subgoal):
 1. v \<in> nodes G1
[PROOF STEP]
by (metis (lifting, no_types) calculation mem_Collect_eq select_convs(1)
                valid_graph.is_path.simps(1))
[PROOF STATE]
proof (state)
this:
v \<in> nodes G1

goal (2 subgoals):
 1. \<And>n. valid_graph.is_path (del_unEdge v w v' G) n [] v \<Longrightarrow> valid_graph.is_path G1 n [] v
 2. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_graph.is_path (del_unEdge v w v' G) n [] v
v \<in> nodes G1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n [] v
v \<in> nodes G1

goal (1 subgoal):
 1. valid_graph.is_path G1 n [] v
[PROOF STEP]
by (metis valid0 valid_G1 valid_unMultigraph.is_trail.simps(1)
                 valid_graph.is_path.simps(1)  valid_unMultigraph.is_trail_intro)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 n [] v

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) ?n xs v \<Longrightarrow> valid_graph.is_path G1 ?n xs v
valid_graph.is_path (del_unEdge v w v' G) n (x # xs) v

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
obtain x1 x2 x3 where x:"x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
have "x1\<in>nodes G1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<in> nodes G1
[PROOF STEP]
using G1 G1_nodes Cons.prems x
[PROOF STATE]
proof (prove)
using this:
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
valid_graph.is_path (del_unEdge v w v' G) n (x # xs) v
x = (x1, x2, x3)

goal (1 subgoal):
 1. x1 \<in> nodes G1
[PROOF STEP]
by (metis (lifting) mem_Collect_eq select_convs(1) valid0 valid_graph.is_path.simps(2))
[PROOF STATE]
proof (state)
this:
x1 \<in> nodes G1

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 \<in> nodes G1

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
have "(x1,x2,x3)\<in>edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 \<in> nodes G1
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
have "(x1,x2,x3)\<in>edges G1"
[PROOF STATE]
proof (prove)
using this:
x1 \<in> nodes G1
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges G1
[PROOF STEP]
using G1 G2 \<open>nodes G1 \<inter> nodes G2={}\<close> \<open>edges G1 \<union> edges G2=edges (del_unEdge v w v' G)\<close>
[PROOF STATE]
proof (prove)
using this:
x1 \<in> nodes G1
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
nodes G1 \<inter> nodes G2 = {}
edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges G1
[PROOF STEP]
by (metis (full_types) IntI Un_iff  bex_empty   valid_G2' valid_graph.E_validD(1) )
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges G1

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges G1

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
have "valid_graph.is_path (del_unEdge v w v' G) x3 xs v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) x3 xs v
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
hence "valid_graph.is_path G1 x3 xs v"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v

goal (1 subgoal):
 1. valid_graph.is_path G1 x3 xs v
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v
valid_graph.is_path (del_unEdge v w v' G) ?n xs v \<Longrightarrow> valid_graph.is_path G1 ?n xs v

goal (1 subgoal):
 1. valid_graph.is_path G1 x3 xs v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 x3 xs v

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 x3 xs v

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
have "x1=n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = n
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
x1 = n

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v \<Longrightarrow> valid_graph.is_path G1 n ps v; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n (a # ps) v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x1, x2, x3) \<in> edges G1
valid_graph.is_path G1 x3 xs v
x1 = n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges G1
valid_graph.is_path G1 x3 xs v
x1 = n

goal (1 subgoal):
 1. valid_graph.is_path G1 n (x # xs) v
[PROOF STEP]
using x valid_G1'
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges G1
valid_graph.is_path G1 x3 xs v
x1 = n
x = (x1, x2, x3)
valid_graph G1

goal (1 subgoal):
 1. valid_graph.is_path G1 n (x # xs) v
[PROOF STEP]
by (metis valid_graph.is_path.simps(2))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 n (x # xs) v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 n ps v

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
obtain ps' where "valid_graph.is_path (del_unEdge v w v' G) n' ps' v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G1 G1_nodes n'
[PROOF STATE]
proof (prove)
using this:
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
n' \<in> nodes G1

goal (1 subgoal):
 1. (\<And>ps'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n' ps' v

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
hence ps':"valid_graph.is_path G1 n' ps' v"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n' ps' v

goal (1 subgoal):
 1. valid_graph.is_path G1 n' ps' v
[PROOF STEP]
proof (induct ps' arbitrary:n')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' [] v \<Longrightarrow> valid_graph.is_path G1 n' [] v
 2. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n' [] v

goal (2 subgoals):
 1. \<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' [] v \<Longrightarrow> valid_graph.is_path G1 n' [] v
 2. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n' [] v

goal (2 subgoals):
 1. \<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' [] v \<Longrightarrow> valid_graph.is_path G1 n' [] v
 2. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
have "v\<in>nodes G1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> nodes G1
[PROOF STEP]
using G1 G1_nodes valid0
[PROOF STATE]
proof (prove)
using this:
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
valid_graph (del_unEdge v w v' G)

goal (1 subgoal):
 1. v \<in> nodes G1
[PROOF STEP]
by (metis (lifting, no_types) calculation mem_Collect_eq select_convs(1)
                valid_graph.is_path.simps(1))
[PROOF STATE]
proof (state)
this:
v \<in> nodes G1

goal (2 subgoals):
 1. \<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' [] v \<Longrightarrow> valid_graph.is_path G1 n' [] v
 2. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_graph.is_path (del_unEdge v w v' G) n' [] v
v \<in> nodes G1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n' [] v
v \<in> nodes G1

goal (1 subgoal):
 1. valid_graph.is_path G1 n' [] v
[PROOF STEP]
by (metis valid0 valid_G1 valid_unMultigraph.is_trail.simps(1)
                 valid_graph.is_path.simps(1)  valid_unMultigraph.is_trail_intro)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 n' [] v

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) ?n' xs v \<Longrightarrow> valid_graph.is_path G1 ?n' xs v
valid_graph.is_path (del_unEdge v w v' G) n' (x # xs) v

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
obtain x1 x2 x3 where x:"x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
have "x1\<in>nodes G1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<in> nodes G1
[PROOF STEP]
using G1 G1_nodes Cons.prems x
[PROOF STATE]
proof (prove)
using this:
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G1_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
valid_graph.is_path (del_unEdge v w v' G) n' (x # xs) v
x = (x1, x2, x3)

goal (1 subgoal):
 1. x1 \<in> nodes G1
[PROOF STEP]
by (metis (lifting) mem_Collect_eq select_convs(1) valid0 valid_graph.is_path.simps(2))
[PROOF STATE]
proof (state)
this:
x1 \<in> nodes G1

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 \<in> nodes G1

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
have "(x1,x2,x3)\<in>edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 \<in> nodes G1
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
have "(x1,x2,x3)\<in>edges G1"
[PROOF STATE]
proof (prove)
using this:
x1 \<in> nodes G1
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges G1
[PROOF STEP]
using G1 G2 \<open>nodes G1 \<inter> nodes G2={}\<close>
              \<open>edges G1 \<union> edges G2=edges (del_unEdge v w v' G)\<close>
[PROOF STATE]
proof (prove)
using this:
x1 \<in> nodes G1
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)
G1 = \<lparr>nodes = G1_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G1_nodes \<and> n' \<in> G1_nodes}\<rparr>
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
nodes G1 \<inter> nodes G2 = {}
edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges G1
[PROOF STEP]
by (metis (full_types) IntI Un_iff  bex_empty  valid_G2' valid_graph.E_validD(1))
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges G1

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges G1

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
have "valid_graph.is_path (del_unEdge v w v' G) x3 xs v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) x3 xs v
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
hence "valid_graph.is_path G1 x3 xs v"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v

goal (1 subgoal):
 1. valid_graph.is_path G1 x3 xs v
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v
valid_graph.is_path (del_unEdge v w v' G) ?n' xs v \<Longrightarrow> valid_graph.is_path G1 ?n' xs v

goal (1 subgoal):
 1. valid_graph.is_path G1 x3 xs v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 x3 xs v

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 x3 xs v

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
have "x1=n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = n'
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
x1 = n'

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v \<Longrightarrow> valid_graph.is_path G1 n' ps' v; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v\<rbrakk> \<Longrightarrow> valid_graph.is_path G1 n' (a # ps') v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x1, x2, x3) \<in> edges G1
valid_graph.is_path G1 x3 xs v
x1 = n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges G1
valid_graph.is_path G1 x3 xs v
x1 = n'

goal (1 subgoal):
 1. valid_graph.is_path G1 n' (x # xs) v
[PROOF STEP]
using x valid_G1'
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges G1
valid_graph.is_path G1 x3 xs v
x1 = n'
x = (x1, x2, x3)
valid_graph G1

goal (1 subgoal):
 1. valid_graph.is_path G1 n' (x # xs) v
[PROOF STEP]
by (metis valid_graph.is_path.simps(2))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 n' (x # xs) v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 n' ps' v

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
hence "valid_graph.is_path G1 v (rev_path ps') n'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G1 n' ps' v

goal (1 subgoal):
 1. valid_graph.is_path G1 v (rev_path ps') n'
[PROOF STEP]
using valid_unMultigraph.is_path_rev[OF valid_G1]
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G1 n' ps' v
valid_graph.is_path G1 ?v' (rev_path ?ps) ?v = valid_graph.is_path G1 ?v ?ps ?v'

goal (1 subgoal):
 1. valid_graph.is_path G1 v (rev_path ps') n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 v (rev_path ps') n'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
hence "valid_graph.is_path G1 n (ps@(rev_path ps')) n'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G1 v (rev_path ps') n'

goal (1 subgoal):
 1. valid_graph.is_path G1 n (ps @ rev_path ps') n'
[PROOF STEP]
using ps valid_graph.is_path_split[OF valid_G1',of n ps "rev_path ps'" n']
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G1 v (rev_path ps') n'
valid_graph.is_path G1 n ps v
valid_graph.is_path G1 n (ps @ rev_path ps') n' = (\<exists>u. valid_graph.is_path G1 n ps u \<and> valid_graph.is_path G1 u (rev_path ps') n')

goal (1 subgoal):
 1. valid_graph.is_path G1 n (ps @ rev_path ps') n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G1 n (ps @ rev_path ps') n'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G1; v' \<in> nodes G1; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G1 v ps v'
[PROOF STEP]
thus "\<exists>ps. valid_graph.is_path G1 n ps n'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G1 n (ps @ rev_path ps') n'

goal (1 subgoal):
 1. \<exists>ps. valid_graph.is_path G1 n ps n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ps. valid_graph.is_path G1 n ps n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.connected G1

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.connected G1

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "valid_unMultigraph.connected G2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph.connected G2
[PROOF STEP]
unfolding valid_unMultigraph.connected_def[OF valid_G2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>nodes G2. \<forall>v'\<in>nodes G2. v \<noteq> v' \<longrightarrow> (\<exists>ps. valid_graph.is_path G2 v ps v')
[PROOF STEP]
proof (rule,rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
fix n n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
assume  n : "n \<in>nodes G2"
[PROOF STATE]
proof (state)
this:
n \<in> nodes G2

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
assume  n': "n'\<in>nodes G2"
[PROOF STATE]
proof (state)
this:
n' \<in> nodes G2

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
assume "n\<noteq>n'"
[PROOF STATE]
proof (state)
this:
n \<noteq> n'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
obtain ps where "valid_graph.is_path (del_unEdge v w v' G) n ps v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G2 G2_nodes n
[PROOF STATE]
proof (prove)
using this:
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
n \<in> nodes G2

goal (1 subgoal):
 1. (\<And>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n ps v'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
hence ps:"valid_graph.is_path G2 n ps v'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n ps v'

goal (1 subgoal):
 1. valid_graph.is_path G2 n ps v'
[PROOF STEP]
proof (induct ps arbitrary:n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. valid_graph.is_path (del_unEdge v w v' G) n [] v' \<Longrightarrow> valid_graph.is_path G2 n [] v'
 2. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n [] v'

goal (2 subgoals):
 1. \<And>n. valid_graph.is_path (del_unEdge v w v' G) n [] v' \<Longrightarrow> valid_graph.is_path G2 n [] v'
 2. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n [] v'

goal (2 subgoals):
 1. \<And>n. valid_graph.is_path (del_unEdge v w v' G) n [] v' \<Longrightarrow> valid_graph.is_path G2 n [] v'
 2. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
have "v'\<in>nodes G2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<in> nodes G2
[PROOF STEP]
using G2 G2_nodes valid0
[PROOF STATE]
proof (prove)
using this:
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
valid_graph (del_unEdge v w v' G)

goal (1 subgoal):
 1. v' \<in> nodes G2
[PROOF STEP]
by (metis (lifting, no_types) calculation mem_Collect_eq select_convs(1)
                valid_graph.is_path.simps(1))
[PROOF STATE]
proof (state)
this:
v' \<in> nodes G2

goal (2 subgoals):
 1. \<And>n. valid_graph.is_path (del_unEdge v w v' G) n [] v' \<Longrightarrow> valid_graph.is_path G2 n [] v'
 2. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_graph.is_path (del_unEdge v w v' G) n [] v'
v' \<in> nodes G2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n [] v'
v' \<in> nodes G2

goal (1 subgoal):
 1. valid_graph.is_path G2 n [] v'
[PROOF STEP]
by (metis valid0 valid_G2 valid_unMultigraph.is_trail.simps(1)
                 valid_graph.is_path.simps(1)  valid_unMultigraph.is_trail_intro)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 n [] v'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) ?n xs v' \<Longrightarrow> valid_graph.is_path G2 ?n xs v'
valid_graph.is_path (del_unEdge v w v' G) n (x # xs) v'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
obtain x1 x2 x3 where x:"x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
have "x1\<in>nodes G2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<in> nodes G2
[PROOF STEP]
using G2 G2_nodes Cons.prems x
[PROOF STATE]
proof (prove)
using this:
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
valid_graph.is_path (del_unEdge v w v' G) n (x # xs) v'
x = (x1, x2, x3)

goal (1 subgoal):
 1. x1 \<in> nodes G2
[PROOF STEP]
by (metis (lifting) mem_Collect_eq select_convs(1) valid0 valid_graph.is_path.simps(2))
[PROOF STATE]
proof (state)
this:
x1 \<in> nodes G2

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 \<in> nodes G2

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
have "(x1,x2,x3)\<in>edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 \<in> nodes G2
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
have "(x1,x2,x3)\<in>edges G2"
[PROOF STATE]
proof (prove)
using this:
x1 \<in> nodes G2
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges G2
[PROOF STEP]
using \<open>nodes G1 \<inter> nodes G2={}\<close> \<open>edges G1 \<union> edges G2=edges (del_unEdge v w v' G)\<close>
[PROOF STATE]
proof (prove)
using this:
x1 \<in> nodes G2
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)
nodes G1 \<inter> nodes G2 = {}
edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges G2
[PROOF STEP]
by (metis IntI Un_iff assms(1) bex_empty connected_def del_UnEdge_node valid0 valid0'
              valid_G1' valid_graph.E_validD(1) valid_graph.E_validD(2) valid_unMultigraph.no_id)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges G2

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges G2

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
have "valid_graph.is_path (del_unEdge v w v' G) x3 xs v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) x3 xs v'
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
hence "valid_graph.is_path G2 x3 xs v'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v'

goal (1 subgoal):
 1. valid_graph.is_path G2 x3 xs v'
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v'
valid_graph.is_path (del_unEdge v w v' G) ?n xs v' \<Longrightarrow> valid_graph.is_path G2 ?n xs v'

goal (1 subgoal):
 1. valid_graph.is_path G2 x3 xs v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 x3 xs v'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 x3 xs v'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
have "x1=n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = n
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
x1 = n

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. valid_graph.is_path (del_unEdge v w v' G) n ps v' \<Longrightarrow> valid_graph.is_path G2 n ps v'; valid_graph.is_path (del_unEdge v w v' G) n (a # ps) v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n (a # ps) v'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x1, x2, x3) \<in> edges G2
valid_graph.is_path G2 x3 xs v'
x1 = n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges G2
valid_graph.is_path G2 x3 xs v'
x1 = n

goal (1 subgoal):
 1. valid_graph.is_path G2 n (x # xs) v'
[PROOF STEP]
using x valid_G2'
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges G2
valid_graph.is_path G2 x3 xs v'
x1 = n
x = (x1, x2, x3)
valid_graph G2

goal (1 subgoal):
 1. valid_graph.is_path G2 n (x # xs) v'
[PROOF STEP]
by (metis valid_graph.is_path.simps(2))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 n (x # xs) v'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 n ps v'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
obtain ps' where "valid_graph.is_path (del_unEdge v w v' G) n' ps' v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G2 G2_nodes n'
[PROOF STATE]
proof (prove)
using this:
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
n' \<in> nodes G2

goal (1 subgoal):
 1. (\<And>ps'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n' ps' v'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
hence ps':"valid_graph.is_path G2 n' ps' v'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n' ps' v'

goal (1 subgoal):
 1. valid_graph.is_path G2 n' ps' v'
[PROOF STEP]
proof (induct ps' arbitrary:n')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' [] v' \<Longrightarrow> valid_graph.is_path G2 n' [] v'
 2. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n' [] v'

goal (2 subgoals):
 1. \<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' [] v' \<Longrightarrow> valid_graph.is_path G2 n' [] v'
 2. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) n' [] v'

goal (2 subgoals):
 1. \<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' [] v' \<Longrightarrow> valid_graph.is_path G2 n' [] v'
 2. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
have "v'\<in>nodes G2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<in> nodes G2
[PROOF STEP]
using G2 G2_nodes valid0
[PROOF STATE]
proof (prove)
using this:
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
valid_graph (del_unEdge v w v' G)

goal (1 subgoal):
 1. v' \<in> nodes G2
[PROOF STEP]
by (metis (lifting, no_types) calculation mem_Collect_eq select_convs(1)
                valid_graph.is_path.simps(1))
[PROOF STATE]
proof (state)
this:
v' \<in> nodes G2

goal (2 subgoals):
 1. \<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' [] v' \<Longrightarrow> valid_graph.is_path G2 n' [] v'
 2. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_graph.is_path (del_unEdge v w v' G) n' [] v'
v' \<in> nodes G2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) n' [] v'
v' \<in> nodes G2

goal (1 subgoal):
 1. valid_graph.is_path G2 n' [] v'
[PROOF STEP]
by (metis valid0 valid_G2 valid_unMultigraph.is_trail.simps(1)
                 valid_graph.is_path.simps(1)  valid_unMultigraph.is_trail_intro)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 n' [] v'

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) ?n' xs v' \<Longrightarrow> valid_graph.is_path G2 ?n' xs v'
valid_graph.is_path (del_unEdge v w v' G) n' (x # xs) v'

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
obtain x1 x2 x3 where x:"x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
have "x1\<in>nodes G2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<in> nodes G2
[PROOF STEP]
using G2 G2_nodes Cons.prems x
[PROOF STATE]
proof (prove)
using this:
G2 = \<lparr>nodes = G2_nodes, edges = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> G2_nodes \<and> n' \<in> G2_nodes}\<rparr>
G2_nodes = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
valid_graph.is_path (del_unEdge v w v' G) n' (x # xs) v'
x = (x1, x2, x3)

goal (1 subgoal):
 1. x1 \<in> nodes G2
[PROOF STEP]
by (metis (lifting) mem_Collect_eq select_convs(1) valid0 valid_graph.is_path.simps(2))
[PROOF STATE]
proof (state)
this:
x1 \<in> nodes G2

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 \<in> nodes G2

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
have "(x1,x2,x3)\<in>edges (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 \<in> nodes G2
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)
[PROOF STEP]
have "(x1,x2,x3)\<in>edges G2"
[PROOF STATE]
proof (prove)
using this:
x1 \<in> nodes G2
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges G2
[PROOF STEP]
using  \<open>nodes G1 \<inter> nodes G2={}\<close> \<open>edges G1 \<union> edges G2=edges (del_unEdge v w v' G)\<close>
[PROOF STATE]
proof (prove)
using this:
x1 \<in> nodes G2
(x1, x2, x3) \<in> edges (del_unEdge v w v' G)
nodes G1 \<inter> nodes G2 = {}
edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)

goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges G2
[PROOF STEP]
by (metis IntI Un_iff assms(1) bex_empty connected_def del_UnEdge_node valid0 valid0'
              valid_G1' valid_graph.E_validD(1) valid_graph.E_validD(2) valid_unMultigraph.no_id)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges G2

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges G2

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
have "valid_graph.is_path (del_unEdge v w v' G) x3 xs v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v w v' G) x3 xs v'
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v'

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
hence "valid_graph.is_path G2 x3 xs v'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v'

goal (1 subgoal):
 1. valid_graph.is_path G2 x3 xs v'
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v w v' G) x3 xs v'
valid_graph.is_path (del_unEdge v w v' G) ?n' xs v' \<Longrightarrow> valid_graph.is_path G2 ?n' xs v'

goal (1 subgoal):
 1. valid_graph.is_path G2 x3 xs v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 x3 xs v'

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 x3 xs v'

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
have "x1=n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = n'
[PROOF STEP]
by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
x1 = n'

goal (1 subgoal):
 1. \<And>a ps' n'. \<lbrakk>\<And>n'. valid_graph.is_path (del_unEdge v w v' G) n' ps' v' \<Longrightarrow> valid_graph.is_path G2 n' ps' v'; valid_graph.is_path (del_unEdge v w v' G) n' (a # ps') v'\<rbrakk> \<Longrightarrow> valid_graph.is_path G2 n' (a # ps') v'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x1, x2, x3) \<in> edges G2
valid_graph.is_path G2 x3 xs v'
x1 = n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges G2
valid_graph.is_path G2 x3 xs v'
x1 = n'

goal (1 subgoal):
 1. valid_graph.is_path G2 n' (x # xs) v'
[PROOF STEP]
using x valid_G2'
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges G2
valid_graph.is_path G2 x3 xs v'
x1 = n'
x = (x1, x2, x3)
valid_graph G2

goal (1 subgoal):
 1. valid_graph.is_path G2 n' (x # xs) v'
[PROOF STEP]
by (metis valid_graph.is_path.simps(2))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 n' (x # xs) v'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 n' ps' v'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
hence "valid_graph.is_path G2 v' (rev_path ps') n'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G2 n' ps' v'

goal (1 subgoal):
 1. valid_graph.is_path G2 v' (rev_path ps') n'
[PROOF STEP]
using valid_unMultigraph.is_path_rev[OF valid_G2]
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G2 n' ps' v'
valid_graph.is_path G2 ?v' (rev_path ?ps) ?v = valid_graph.is_path G2 ?v ?ps ?v'

goal (1 subgoal):
 1. valid_graph.is_path G2 v' (rev_path ps') n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 v' (rev_path ps') n'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
hence "valid_graph.is_path G2 n (ps@(rev_path ps')) n'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G2 v' (rev_path ps') n'

goal (1 subgoal):
 1. valid_graph.is_path G2 n (ps @ rev_path ps') n'
[PROOF STEP]
using ps valid_graph.is_path_split[OF valid_G2',of n ps "rev_path ps'" n']
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G2 v' (rev_path ps') n'
valid_graph.is_path G2 n ps v'
valid_graph.is_path G2 n (ps @ rev_path ps') n' = (\<exists>u. valid_graph.is_path G2 n ps u \<and> valid_graph.is_path G2 u (rev_path ps') n')

goal (1 subgoal):
 1. valid_graph.is_path G2 n (ps @ rev_path ps') n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path G2 n (ps @ rev_path ps') n'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> nodes G2; v' \<in> nodes G2; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path G2 v ps v'
[PROOF STEP]
thus "\<exists>ps. valid_graph.is_path G2 n ps n'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path G2 n (ps @ rev_path ps') n'

goal (1 subgoal):
 1. \<exists>ps. valid_graph.is_path G2 n ps n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ps. valid_graph.is_path G2 n ps n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.connected G2

goal (1 subgoal):
 1. (\<And>G1 G2. \<lbrakk>nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}; nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}; edges G1 \<union> edges G2 = edges (del_unEdge v w v' G); edges G1 \<inter> edges G2 = {}; nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G); nodes G1 \<inter> nodes G2 = {}; valid_unMultigraph G1; valid_unMultigraph G2; valid_unMultigraph.connected G1; valid_unMultigraph.connected G2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}
nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}
nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G)
nodes G1 \<inter> nodes G2 = {}
edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)
edges G1 \<inter> edges G2 = {}
valid_unMultigraph.connected G1
valid_unMultigraph.connected G2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}
nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}
nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G)
nodes G1 \<inter> nodes G2 = {}
edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)
edges G1 \<inter> edges G2 = {}
valid_unMultigraph.connected G1
valid_unMultigraph.connected G2

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using valid_G1 valid_G2 that
[PROOF STATE]
proof (prove)
using this:
nodes G1 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}
edges G1 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G1 \<and> n' \<in> nodes G1}
nodes G2 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}
edges G2 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes G2 \<and> n' \<in> nodes G2}
nodes G1 \<union> nodes G2 = nodes (del_unEdge v w v' G)
nodes G1 \<inter> nodes G2 = {}
edges G1 \<union> edges G2 = edges (del_unEdge v w v' G)
edges G1 \<inter> edges G2 = {}
valid_unMultigraph.connected G1
valid_unMultigraph.connected G2
valid_unMultigraph G1
valid_unMultigraph G2
\<lbrakk>nodes ?G1.0 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}; edges ?G1.0 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes ?G1.0 \<and> n' \<in> nodes ?G1.0}; nodes ?G2.0 = {n. \<exists>ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}; edges ?G2.0 = {(n, e, n'). (n, e, n') \<in> edges (del_unEdge v w v' G) \<and> n \<in> nodes ?G2.0 \<and> n' \<in> nodes ?G2.0}; edges ?G1.0 \<union> edges ?G2.0 = edges (del_unEdge v w v' G); edges ?G1.0 \<inter> edges ?G2.0 = {}; nodes ?G1.0 \<union> nodes ?G2.0 = nodes (del_unEdge v w v' G); nodes ?G1.0 \<inter> nodes ?G2.0 = {}; valid_unMultigraph ?G1.0; valid_unMultigraph ?G2.0; valid_unMultigraph.connected ?G1.0; valid_unMultigraph.connected ?G2.0\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed