[STATEMENT]
lemma isSPath_nt_parallel_old:
  "isSimplePath u p v \<Longrightarrow> (\<forall>(u, v) \<in> set p. (v, u) \<notin> set p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath u p v \<Longrightarrow> \<forall>(u, v)\<in>set p. (v, u) \<notin> set p
[PROOF STEP]
using isSPath_nt_parallel[of u p v]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isSimplePath u p v; ?e \<in> set p\<rbrakk> \<Longrightarrow> prod.swap ?e \<notin> set p

goal (1 subgoal):
 1. isSimplePath u p v \<Longrightarrow> \<forall>(u, v)\<in>set p. (v, u) \<notin> set p
[PROOF STEP]
by auto


[STATEMENT]
lemma isSPath_distinct: "isSimplePath u p v \<Longrightarrow> distinct p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath u p v \<Longrightarrow> distinct p
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isSimplePath u p v; \<not> distinct p\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto dest!: not_distinct_decomp simp: split_path_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adjacent_edges_not_on_path:
  assumes PATH: "isPath s p t"
  assumes VNV: "v\<notin>set (pathVertices_fwd s p)"
  shows "adjacent v \<inter> set p = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent v \<inter> set p = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. adjacent v \<inter> set p = {}
[PROOF STEP]
from VNV
[PROOF STATE]
proof (chain)
picking this:
v \<notin> set (pathVertices_fwd s p)
[PROOF STEP]
have "\<forall>u. (u,v)\<notin>set p \<and> (v,u)\<notin>set p"
[PROOF STATE]
proof (prove)
using this:
v \<notin> set (pathVertices_fwd s p)

goal (1 subgoal):
 1. \<forall>u. (u, v) \<notin> set p \<and> (v, u) \<notin> set p
[PROOF STEP]
by (auto dest: pathVertices_edge[OF PATH])
[PROOF STATE]
proof (state)
this:
\<forall>u. (u, v) \<notin> set p \<and> (v, u) \<notin> set p

goal (1 subgoal):
 1. adjacent v \<inter> set p = {}
[PROOF STEP]
thus "adjacent v \<inter> set p = {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>u. (u, v) \<notin> set p \<and> (v, u) \<notin> set p

goal (1 subgoal):
 1. adjacent v \<inter> set p = {}
[PROOF STEP]
by (auto simp: incoming_def outgoing_def adjacent_def)
[PROOF STATE]
proof (state)
this:
adjacent v \<inter> set p = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjacent_edges_on_simple_path:
  assumes SPATH: "isSimplePath s p t"
  assumes VNV: "v\<in>set (pathVertices_fwd s p)" "v\<noteq>s" "v\<noteq>t"
  obtains p1 u w p2 where
    "p = p1@(u,v)#(v,w)#p2"
    "incoming v \<inter> set p = {(u,v)}"
    "outgoing v \<inter> set p = {(v,w)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1 u w p2. \<lbrakk>p = p1 @ (u, v) # (v, w) # p2; incoming v \<inter> set p = {(u, v)}; outgoing v \<inter> set p = {(v, w)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p1 u w p2. \<lbrakk>p = p1 @ (u, v) # (v, w) # p2; incoming v \<inter> set p = {(u, v)}; outgoing v \<inter> set p = {(v, w)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from SPATH
[PROOF STATE]
proof (chain)
picking this:
isSimplePath s p t
[PROOF STEP]
have
    PATH: "isPath s p t" and
    DIST: "distinct (pathVertices_fwd s p)"
[PROOF STATE]
proof (prove)
using this:
isSimplePath s p t

goal (1 subgoal):
 1. isPath s p t &&& distinct (pathVertices_fwd s p)
[PROOF STEP]
by (auto simp: isSimplePath_def pathVertices_fwd)
[PROOF STATE]
proof (state)
this:
isPath s p t
distinct (pathVertices_fwd s p)

goal (1 subgoal):
 1. (\<And>p1 u w p2. \<lbrakk>p = p1 @ (u, v) # (v, w) # p2; incoming v \<inter> set p = {(u, v)}; outgoing v \<inter> set p = {(v, w)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from split_path_at_vertex[OF VNV(1) PATH]
[PROOF STATE]
proof (chain)
picking this:
(\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 v; isPath v p2 t\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain p1 p2 where
    [simp]: "p=p1@p2" and P1: "isPath s p1 v" and P2: "isPath v p2 t"
[PROOF STATE]
proof (prove)
using this:
(\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 v; isPath v p2 t\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 v; isPath v p2 t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p = p1 @ p2
isPath s p1 v
isPath v p2 t

goal (1 subgoal):
 1. (\<And>p1 u w p2. \<lbrakk>p = p1 @ (u, v) # (v, w) # p2; incoming v \<inter> set p = {(u, v)}; outgoing v \<inter> set p = {(v, w)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>v\<noteq>s\<close> P1
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> s
isPath s p1 v
[PROOF STEP]
obtain p1' u where
    [simp]: "p1=p1'@[(u,v)]" and P1': "isPath s p1' u" and UV: "(u,v)\<in>E"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> s
isPath s p1 v

goal (1 subgoal):
 1. (\<And>p1' u. \<lbrakk>p1 = p1' @ [(u, v)]; isPath s p1' u; (u, v) \<in> E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases p1 rule: rev_cases) (auto simp: split_path_simps)
[PROOF STATE]
proof (state)
this:
p1 = p1' @ [(u, v)]
isPath s p1' u
(u, v) \<in> E

goal (1 subgoal):
 1. (\<And>p1 u w p2. \<lbrakk>p = p1 @ (u, v) # (v, w) # p2; incoming v \<inter> set p = {(u, v)}; outgoing v \<inter> set p = {(v, w)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>v\<noteq>t\<close> P2
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> t
isPath v p2 t
[PROOF STEP]
obtain w p2' where
    [simp]: "p2=(v,w)#p2'" and VW: "(v,w)\<in>E" and P2': "isPath w p2' t"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> t
isPath v p2 t

goal (1 subgoal):
 1. (\<And>w p2'. \<lbrakk>p2 = (v, w) # p2'; (v, w) \<in> E; isPath w p2' t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases p2) (auto)
[PROOF STATE]
proof (state)
this:
p2 = (v, w) # p2'
(v, w) \<in> E
isPath w p2' t

goal (1 subgoal):
 1. (\<And>p1 u w p2. \<lbrakk>p = p1 @ (u, v) # (v, w) # p2; incoming v \<inter> set p = {(u, v)}; outgoing v \<inter> set p = {(v, w)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (rule that[of p1' u w p2'])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. p = p1' @ (u, v) # (v, w) # p2'
 2. incoming v \<inter> set p = {(u, v)}
 3. outgoing v \<inter> set p = {(v, w)}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. incoming v \<inter> set p = {(u, v)}
 2. outgoing v \<inter> set p = {(v, w)}
[PROOF STEP]
using
      isSPath_sg_outgoing[OF SPATH, of v w]
      isSPath_sg_incoming[OF SPATH, of u v]
      isPath_edgeset[OF PATH]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(v, w) \<in> set p; w \<noteq> ?v2.0\<rbrakk> \<Longrightarrow> (v, ?v2.0) \<notin> set p
\<lbrakk>(u, v) \<in> set p; u \<noteq> ?u2.0\<rbrakk> \<Longrightarrow> (?u2.0, v) \<notin> set p
?e \<in> set p \<Longrightarrow> ?e \<in> E

goal (2 subgoals):
 1. incoming v \<inter> set p = {(u, v)}
 2. outgoing v \<inter> set p = {(v, w)}
[PROOF STEP]
apply (fastforce simp: incoming_def outgoing_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma connected_by_dist: "connected v v' = (\<exists>d. dist v d v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected v v' = (\<exists>d. dist v d v')
[PROOF STEP]
by (auto simp: dist_def connected_def)


[STATEMENT]
lemma min_distI2:
  "\<lbrakk>connected v v'; \<And>d. \<lbrakk>dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> Q d\<rbrakk>
    \<Longrightarrow> Q (min_dist v v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>connected v v'; \<And>d. \<lbrakk>dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> Q d\<rbrakk> \<Longrightarrow> Q (min_dist v v')
[PROOF STEP]
unfolding min_dist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>connected v v'; \<And>d. \<lbrakk>dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> Q d\<rbrakk> \<Longrightarrow> Q (LEAST d. dist v d v')
[PROOF STEP]
apply (rule LeastI2_wellorder[where Q=Q and a="SOME d. dist v d v'"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>connected v v'; \<And>d. \<lbrakk>dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> Q d\<rbrakk> \<Longrightarrow> dist v (SOME d. dist v d v') v'
 2. \<And>a. \<lbrakk>connected v v'; \<And>d. \<lbrakk>dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> Q d; dist v a v'; \<forall>b. dist v b v' \<longrightarrow> a \<le> b\<rbrakk> \<Longrightarrow> Q a
[PROOF STEP]
apply (auto simp: connected_by_dist intro: someI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma min_distI_eq:
  "\<lbrakk> dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d' \<rbrakk> \<Longrightarrow> min_dist v v' = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> min_dist v v' = d
[PROOF STEP]
by (force intro: min_distI2 simp: connected_by_dist)


[STATEMENT]
lemma dist_z_iff[simp]: "dist v 0 v' \<longleftrightarrow> v'=v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist v 0 v' = (v' = v)
[PROOF STEP]
by (auto simp: dist_def)


[STATEMENT]
lemma dist_z[simp, intro!]: "dist v 0 v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist v 0 v
[PROOF STEP]
by simp


[STATEMENT]
lemma dist_suc: "\<lbrakk>dist v d v'; (v',v'')\<in>E\<rbrakk> \<Longrightarrow> dist v (Suc d) v''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dist v d v'; (v', v'') \<in> E\<rbrakk> \<Longrightarrow> dist v (Suc d) v''
[PROOF STEP]
by (auto simp: dist_def intro: isPath_append_edge)


[STATEMENT]
lemma dist_cases[case_names dist_z dist_suc, consumes 1, cases pred]:
  assumes "dist v d v'"
  obtains "v=v'" "d=0"
   | vh dd where "d=Suc dd" "dist v dd vh" "(vh,v')\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>v = v'; d = 0\<rbrakk> \<Longrightarrow> thesis; \<And>dd vh. \<lbrakk>d = Suc dd; dist v dd vh; (vh, v') \<in> E\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dist v d v'

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>v = v'; d = 0\<rbrakk> \<Longrightarrow> thesis; \<And>dd vh. \<lbrakk>d = Suc dd; dist v dd vh; (vh, v') \<in> E\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases d; clarsimp simp add: dist_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat p. \<lbrakk>\<And>dd vh. \<lbrakk>nat = dd; \<exists>p. isPath v p vh \<and> length p = dd; (vh, v') \<in> E\<rbrakk> \<Longrightarrow> thesis; d = Suc nat; isPath v p v'; length p = Suc nat\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for \<dots> p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>dd vh. \<lbrakk>nat_ = dd; \<exists>p. isPath v p vh \<and> length p = dd; (vh, v') \<in> E\<rbrakk> \<Longrightarrow> thesis; d = Suc nat_; isPath v p v'; length p = Suc nat_\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(cases p rule: rev_cases)(fastforce simp add: isPath_append)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma min_dist_z[simp]: "min_dist v v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_dist v v = 0
[PROOF STEP]
by (rule min_distI2) auto


[STATEMENT]
lemma min_dist_z_iff[simp]: "connected v v' \<Longrightarrow> min_dist v v' = 0 \<longleftrightarrow> v'=v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected v v' \<Longrightarrow> (min_dist v v' = 0) = (v' = v)
[PROOF STEP]
by (rule min_distI2) (auto)


[STATEMENT]
lemma min_dist_is_dist: "connected v v' \<Longrightarrow> dist v (min_dist v v') v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected v v' \<Longrightarrow> dist v (min_dist v v') v'
[PROOF STEP]
by (auto intro: min_distI2)


[STATEMENT]
lemma min_dist_minD: "dist v d v' \<Longrightarrow> min_dist v v' \<le> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist v d v' \<Longrightarrow> min_dist v v' \<le> d
[PROOF STEP]
by (auto intro: min_distI2)


[STATEMENT]
lemma min_dist_succ:
  "\<lbrakk> connected v v'; (v',v'') \<in> E \<rbrakk> \<Longrightarrow> min_dist v v'' \<le> Suc (min_dist v v') "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>connected v v'; (v', v'') \<in> E\<rbrakk> \<Longrightarrow> min_dist v v'' \<le> Suc (min_dist v v')
[PROOF STEP]
apply (rule min_distI2[where v'=v'])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>connected v v'; (v', v'') \<in> E\<rbrakk> \<Longrightarrow> connected v v'
 2. \<And>d. \<lbrakk>connected v v'; (v', v'') \<in> E; dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> min_dist v v'' \<le> Suc d
[PROOF STEP]
apply (auto intro!: min_dist_minD intro: dist_suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma min_dist_suc:
  assumes c: "connected v v'" "min_dist v v' = Suc d"
  shows "\<exists>v''. connected v v'' \<and> (v'',v') \<in> E \<and> min_dist v v'' = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d
[PROOF STEP]
from min_dist_is_dist[OF c(1)]
[PROOF STATE]
proof (chain)
picking this:
dist v (min_dist v v') v'
[PROOF STEP]
have "min_dist v v' = Suc d \<longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
using this:
dist v (min_dist v v') v'

goal (1 subgoal):
 1. min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>v = v'; min_dist v v' = 0\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)
 2. \<And>vh dd. \<lbrakk>min_dist v v' = Suc dd; dist v dd vh; (vh, v') \<in> E\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)
[PROOF STEP]
case (dist_suc v'' d')
[PROOF STATE]
proof (state)
this:
min_dist v v' = Suc d'
dist v d' v''
(v'', v') \<in> E

goal (2 subgoals):
 1. \<lbrakk>v = v'; min_dist v v' = 0\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)
 2. \<And>vh dd. \<lbrakk>min_dist v v' = Suc dd; dist v dd vh; (vh, v') \<in> E\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
min_dist v v' = Suc d'
dist v d' v''
(v'', v') \<in> E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
min_dist v v' = Suc d'
dist v d' v''
(v'', v') \<in> E

goal (1 subgoal):
 1. min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)
[PROOF STEP]
using min_dist_succ[of v v'' v'] min_dist_minD[of v d v'']
[PROOF STATE]
proof (prove)
using this:
min_dist v v' = Suc d'
dist v d' v''
(v'', v') \<in> E
\<lbrakk>connected v v''; (v'', v') \<in> E\<rbrakk> \<Longrightarrow> min_dist v v' \<le> Suc (min_dist v v'')
dist v d v'' \<Longrightarrow> min_dist v v'' \<le> d

goal (1 subgoal):
 1. min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)
[PROOF STEP]
by (auto simp: connected_distI)
[PROOF STATE]
proof (state)
this:
min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)

goal (1 subgoal):
 1. \<lbrakk>v = v'; min_dist v v' = 0\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)

goal (1 subgoal):
 1. \<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d
[PROOF STEP]
with c
[PROOF STATE]
proof (chain)
picking this:
connected v v'
min_dist v v' = Suc d
min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
connected v v'
min_dist v v' = Suc d
min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d)

goal (1 subgoal):
 1. \<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>v''. connected v v'' \<and> (v'', v') \<in> E \<and> min_dist v v'' = d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_dist_less:
  assumes "connected src v" "min_dist src v = d" and "d' < d"
  shows "\<exists>v'. connected src v' \<and> min_dist src v' = d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v'. connected src v' \<and> min_dist src v' = d'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
connected src v
min_dist src v = d
d' < d

goal (1 subgoal):
 1. \<exists>v'. connected src v' \<and> min_dist src v' = d'
[PROOF STEP]
proof (induct d arbitrary: v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>connected src v; min_dist src v = 0; d' < 0\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'
 2. \<And>d v. \<lbrakk>\<And>v. \<lbrakk>connected src v; min_dist src v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'; connected src v; min_dist src v = Suc d; d' < Suc d\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'
[PROOF STEP]
case (Suc d)
[PROOF STATE]
proof (state)
this:
\<lbrakk>connected src ?v; min_dist src ?v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'
connected src v
min_dist src v = Suc d
d' < Suc d

goal (2 subgoals):
 1. \<And>v. \<lbrakk>connected src v; min_dist src v = 0; d' < 0\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'
 2. \<And>d v. \<lbrakk>\<And>v. \<lbrakk>connected src v; min_dist src v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'; connected src v; min_dist src v = Suc d; d' < Suc d\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'
[PROOF STEP]
with min_dist_suc[of src v]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>connected src v; min_dist src v = Suc ?d\<rbrakk> \<Longrightarrow> \<exists>v''. connected src v'' \<and> (v'', v) \<in> E \<and> min_dist src v'' = ?d
\<lbrakk>connected src ?v; min_dist src ?v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'
connected src v
min_dist src v = Suc d
d' < Suc d
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>connected src v; min_dist src v = Suc ?d\<rbrakk> \<Longrightarrow> \<exists>v''. connected src v'' \<and> (v'', v) \<in> E \<and> min_dist src v'' = ?d
\<lbrakk>connected src ?v; min_dist src ?v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'
connected src v
min_dist src v = Suc d
d' < Suc d

goal (1 subgoal):
 1. \<exists>v'. connected src v' \<and> min_dist src v' = d'
[PROOF STEP]
by (cases "d' = d") auto
[PROOF STATE]
proof (state)
this:
\<exists>v'. connected src v' \<and> min_dist src v' = d'

goal (1 subgoal):
 1. \<And>v. \<lbrakk>connected src v; min_dist src v = 0; d' < 0\<rbrakk> \<Longrightarrow> \<exists>v'. connected src v' \<and> min_dist src v' = d'
[PROOF STEP]
qed auto


[STATEMENT]
lemma dist_trans[trans]: "dist u d1 w \<Longrightarrow> dist w d2 v \<Longrightarrow> dist u (d1+d2) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dist u d1 w; dist w d2 v\<rbrakk> \<Longrightarrow> dist u (d1 + d2) v
[PROOF STEP]
apply (clarsimp simp: dist_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p pa. \<lbrakk>isPath u p w; d1 = length p; isPath w pa v; d2 = length pa\<rbrakk> \<Longrightarrow> \<exists>pb. isPath u pb v \<and> length pb = length p + length pa
[PROOF STEP]
apply (rename_tac p1 p2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p1 p2. \<lbrakk>isPath u p1 w; d1 = length p1; isPath w p2 v; d2 = length p2\<rbrakk> \<Longrightarrow> \<exists>p. isPath u p v \<and> length p = length p1 + length p2
[PROOF STEP]
apply (rule_tac x="p1@p2" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p1 p2. \<lbrakk>isPath u p1 w; d1 = length p1; isPath w p2 v; d2 = length p2\<rbrakk> \<Longrightarrow> isPath u (p1 @ p2) v \<and> length (p1 @ p2) = length p1 + length p2
[PROOF STEP]
by (auto simp: isPath_append)


[STATEMENT]
lemma min_dist_split:
  assumes D1: "dist u d1 w" and D2: "dist w d2 v" and MIN: "min_dist u v = d1+d2"
  shows "min_dist u w = d1" "min_dist w v = d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_dist u w = d1 &&& min_dist w v = d2
[PROOF STEP]
apply (metis assms ab_semigroup_add_class.add.commute add_le_cancel_left
    dist_trans min_distI_eq min_dist_minD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
by (metis assms add_le_cancel_left dist_trans min_distI_eq min_dist_minD)


[STATEMENT]
lemma \<comment> \<open>Manual proof\<close>
  assumes D1: "dist u d1 w" and D2: "dist w d2 v" and MIN: "min_dist u v = d1+d2"
  shows "min_dist u w = d1" "min_dist w v = d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_dist u w = d1 &&& min_dist w v = d2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
from min_dist_minD[OF \<open>dist u d1 w\<close>]
[PROOF STATE]
proof (chain)
picking this:
min_dist u w \<le> d1
[PROOF STEP]
have "min_dist u w \<le> d1"
[PROOF STATE]
proof (prove)
using this:
min_dist u w \<le> d1

goal (1 subgoal):
 1. min_dist u w \<le> d1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
min_dist u w \<le> d1

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
min_dist u w \<le> d1

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
min_dist u w \<le> d1

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
have "dist u (min_dist u w) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist u (min_dist u w) w
[PROOF STEP]
apply (rule min_dist_is_dist)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected u w
[PROOF STEP]
using D1
[PROOF STATE]
proof (prove)
using this:
dist u d1 w

goal (1 subgoal):
 1. connected u w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist u (min_dist u w) w

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist u (min_dist u w) w

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
note D2
[PROOF STATE]
proof (state)
this:
dist w d2 v

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist u (min_dist u w + d2) v
[PROOF STEP]
have "dist u (min_dist u w + d2) v"
[PROOF STATE]
proof (prove)
using this:
dist u (min_dist u w + d2) v

goal (1 subgoal):
 1. dist u (min_dist u w + d2) v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist u (min_dist u w + d2) v

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dist u (min_dist u w + d2) v

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
assume "min_dist u w < d1"
[PROOF STATE]
proof (state)
this:
min_dist u w < d1

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
min_dist u w < d1

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
note MIN
[PROOF STATE]
proof (state)
this:
min_dist u v = d1 + d2

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dist u (min_dist u w + d2) v
min_dist u w < d1
min_dist u v = d1 + d2
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
dist u (min_dist u w + d2) v
min_dist u w < d1
min_dist u v = d1 + d2

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

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
min_dist u w < d1 \<Longrightarrow> False

goal (2 subgoals):
 1. min_dist u w = d1
 2. min_dist w v = d2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
min_dist u w \<le> d1
min_dist u w < d1 \<Longrightarrow> False
[PROOF STEP]
show "min_dist u w = d1"
[PROOF STATE]
proof (prove)
using this:
min_dist u w \<le> d1
min_dist u w < d1 \<Longrightarrow> False

goal (1 subgoal):
 1. min_dist u w = d1
[PROOF STEP]
unfolding not_less[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<not> d1 < min_dist u w
min_dist u w < d1 \<Longrightarrow> False

goal (1 subgoal):
 1. min_dist u w = d1
[PROOF STEP]
using nat_neq_iff
[PROOF STATE]
proof (prove)
using this:
\<not> d1 < min_dist u w
min_dist u w < d1 \<Longrightarrow> False
(?m \<noteq> ?n) = (?m < ?n \<or> ?n < ?m)

goal (1 subgoal):
 1. min_dist u w = d1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
min_dist u w = d1

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
from min_dist_minD[OF \<open>dist w d2 v\<close>]
[PROOF STATE]
proof (chain)
picking this:
min_dist w v \<le> d2
[PROOF STEP]
have "min_dist w v \<le> d2"
[PROOF STATE]
proof (prove)
using this:
min_dist w v \<le> d2

goal (1 subgoal):
 1. min_dist w v \<le> d2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
min_dist w v \<le> d2

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
min_dist w v \<le> d2

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
min_dist w v \<le> d2

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
note D1
[PROOF STATE]
proof (state)
this:
dist u d1 w

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist u d1 w

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
have "dist w (min_dist w v) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist w (min_dist w v) v
[PROOF STEP]
apply (rule min_dist_is_dist)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected w v
[PROOF STEP]
using D2
[PROOF STATE]
proof (prove)
using this:
dist w d2 v

goal (1 subgoal):
 1. connected w v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist w (min_dist w v) v

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist u (d1 + min_dist w v) v
[PROOF STEP]
have "dist u (d1 + min_dist w v) v"
[PROOF STATE]
proof (prove)
using this:
dist u (d1 + min_dist w v) v

goal (1 subgoal):
 1. dist u (d1 + min_dist w v) v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist u (d1 + min_dist w v) v

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dist u (d1 + min_dist w v) v

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
assume "min_dist w v < d2"
[PROOF STATE]
proof (state)
this:
min_dist w v < d2

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
min_dist w v < d2

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
note MIN
[PROOF STATE]
proof (state)
this:
min_dist u v = d1 + d2

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dist u (d1 + min_dist w v) v
min_dist w v < d2
min_dist u v = d1 + d2
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
dist u (d1 + min_dist w v) v
min_dist w v < d2
min_dist u v = d1 + d2

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

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
min_dist w v < d2 \<Longrightarrow> False

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
min_dist w v \<le> d2
min_dist w v < d2 \<Longrightarrow> False
[PROOF STEP]
show "min_dist w v = d2"
[PROOF STATE]
proof (prove)
using this:
min_dist w v \<le> d2
min_dist w v < d2 \<Longrightarrow> False

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
unfolding not_less[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<not> d2 < min_dist w v
min_dist w v < d2 \<Longrightarrow> False

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
using nat_neq_iff
[PROOF STATE]
proof (prove)
using this:
\<not> d2 < min_dist w v
min_dist w v < d2 \<Longrightarrow> False
(?m \<noteq> ?n) = (?m < ?n \<or> ?n < ?m)

goal (1 subgoal):
 1. min_dist w v = d2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
min_dist w v = d2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isShortestPath_min_dist_def:
  "isShortestPath u p v \<longleftrightarrow> isPath u p v \<and> length p = min_dist u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isShortestPath u p v = (isPath u p v \<and> length p = min_dist u v)
[PROOF STEP]
unfolding isShortestPath_def min_dist_def dist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (isPath u p v \<and> (\<forall>p'. isPath u p' v \<longrightarrow> length p \<le> length p')) = (isPath u p v \<and> length p = (LEAST d. \<exists>p. isPath u p v \<and> length p = d))
[PROOF STEP]
apply (rule iffI; clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isPath u p v; \<forall>p'. isPath u p' v \<longrightarrow> length p \<le> length p'\<rbrakk> \<Longrightarrow> length p = (LEAST d. \<exists>p. isPath u p v \<and> length p = d)
 2. \<And>p'. \<lbrakk>isPath u p v; length p = (LEAST d. \<exists>p. isPath u p v \<and> length p = d); isPath u p' v\<rbrakk> \<Longrightarrow> (LEAST d. \<exists>p. isPath u p v \<and> length p = d) \<le> length p'
[PROOF STEP]
apply (rule Least_equality[symmetric]; auto; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>isPath u p v; length p = (LEAST d. \<exists>p. isPath u p v \<and> length p = d); isPath u p' v\<rbrakk> \<Longrightarrow> (LEAST d. \<exists>p. isPath u p v \<and> length p = d) \<le> length p'
[PROOF STEP]
apply (rule Least_le; auto; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma obtain_shortest_path:
  assumes CONN: "connected u v"
  obtains p where "isShortestPath u p v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. isShortestPath u p v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using min_dist_is_dist[OF CONN]
[PROOF STATE]
proof (prove)
using this:
dist u (min_dist u v) v

goal (1 subgoal):
 1. (\<And>p. isShortestPath u p v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dist_def isShortestPath_min_dist_def
[PROOF STATE]
proof (prove)
using this:
\<exists>p. isPath u p v \<and> length p = min_dist u v

goal (1 subgoal):
 1. (\<And>p. isPath u p v \<and> length p = min_dist u v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma shortestPath_is_simple:
  assumes "isShortestPath s p t"
  shows "isSimplePath s p t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath s p t
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
isShortestPath s p t
[PROOF STEP]
have PATH: "isPath s p t"
    and SHORTEST: "\<forall>p'. isPath s p' t \<longrightarrow> length p \<le> length p'"
[PROOF STATE]
proof (prove)
using this:
isShortestPath s p t

goal (1 subgoal):
 1. isPath s p t &&& \<forall>p'. isPath s p' t \<longrightarrow> length p \<le> length p'
[PROOF STEP]
by (auto simp: isShortestPath_def)
[PROOF STATE]
proof (state)
this:
isPath s p t
\<forall>p'. isPath s p' t \<longrightarrow> length p \<le> length p'

goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
assume "\<not>isSimplePath s p t"
[PROOF STATE]
proof (state)
this:
\<not> isSimplePath s p t

goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
with PATH
[PROOF STATE]
proof (chain)
picking this:
isPath s p t
\<not> isSimplePath s p t
[PROOF STEP]
have "\<not>distinct (pathVertices_fwd s p)"
[PROOF STATE]
proof (prove)
using this:
isPath s p t
\<not> isSimplePath s p t

goal (1 subgoal):
 1. \<not> distinct (pathVertices_fwd s p)
[PROOF STEP]
by (auto simp: isSimplePath_fwd)
[PROOF STATE]
proof (state)
this:
\<not> distinct (pathVertices_fwd s p)

goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> distinct (pathVertices_fwd s p)
[PROOF STEP]
obtain pv1 u pv2 pv3 where PV: "pathVertices_fwd s p = pv1@u#pv2@u#pv3"
[PROOF STATE]
proof (prove)
using this:
\<not> distinct (pathVertices_fwd s p)

goal (1 subgoal):
 1. (\<And>pv1 u pv2 pv3. pathVertices_fwd s p = pv1 @ u # pv2 @ u # pv3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: not_distinct_decomp)
[PROOF STATE]
proof (state)
this:
pathVertices_fwd s p = pv1 @ u # pv2 @ u # pv3

goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
from split_path_at_vertex_complete[OF PATH PV]
[PROOF STATE]
proof (chain)
picking this:
(\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv2 @ u # pv3\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain p1 p23 where
    [simp]: "p=p1@p23" and
      P1: "isPath s p1 u" "pathVertices_fwd s p1 = pv1@[u]" and
      P23: "isPath u p23 t" "pathVertices_fwd u p23 = (u#pv2)@u#pv3"
[PROOF STATE]
proof (prove)
using this:
(\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv2 @ u # pv3\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p1 p23. \<lbrakk>p = p1 @ p23; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p23 t; pathVertices_fwd u p23 = (u # pv2) @ u # pv3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = p1 @ p23
isPath s p1 u
pathVertices_fwd s p1 = pv1 @ [u]
isPath u p23 t
pathVertices_fwd u p23 = (u # pv2) @ u # pv3

goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
from split_path_at_vertex_complete[OF P23]
[PROOF STATE]
proof (chain)
picking this:
(\<And>p1 p2. \<lbrakk>p23 = p1 @ p2; isPath u p1 u; pathVertices_fwd u p1 = (u # pv2) @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv3\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain p2 p3 where
    [simp]: "p23 = p2@p3" and
    P2: "isPath u p2 u" "pathVertices_fwd u p2 = u#pv2@[u]" and
    P3: "isPath u p3 t" "pathVertices_fwd u p3 = u#pv3"
[PROOF STATE]
proof (prove)
using this:
(\<And>p1 p2. \<lbrakk>p23 = p1 @ p2; isPath u p1 u; pathVertices_fwd u p1 = (u # pv2) @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv3\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p2 p3. \<lbrakk>p23 = p2 @ p3; isPath u p2 u; pathVertices_fwd u p2 = u # pv2 @ [u]; isPath u p3 t; pathVertices_fwd u p3 = u # pv3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p23 = p2 @ p3
isPath u p2 u
pathVertices_fwd u p2 = u # pv2 @ [u]
isPath u p3 t
pathVertices_fwd u p3 = u # pv3

goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
from P1(1) P3(1)
[PROOF STATE]
proof (chain)
picking this:
isPath s p1 u
isPath u p3 t
[PROOF STEP]
have SHORTER_PATH: "isPath s (p1@p3) t"
[PROOF STATE]
proof (prove)
using this:
isPath s p1 u
isPath u p3 t

goal (1 subgoal):
 1. isPath s (p1 @ p3) t
[PROOF STEP]
by (auto simp: isPath_append)
[PROOF STATE]
proof (state)
this:
isPath s (p1 @ p3) t

goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
isPath u p2 u
pathVertices_fwd u p2 = u # pv2 @ [u]
[PROOF STEP]
have "p2\<noteq>[]"
[PROOF STATE]
proof (prove)
using this:
isPath u p2 u
pathVertices_fwd u p2 = u # pv2 @ [u]

goal (1 subgoal):
 1. p2 \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p2 \<noteq> []

goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
hence LESS: "length (p1@p3) < length p"
[PROOF STATE]
proof (prove)
using this:
p2 \<noteq> []

goal (1 subgoal):
 1. length (p1 @ p3) < length p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (p1 @ p3) < length p

goal (1 subgoal):
 1. \<not> isSimplePath s p t \<Longrightarrow> False
[PROOF STEP]
with SHORTER_PATH SHORTEST
[PROOF STATE]
proof (chain)
picking this:
isPath s (p1 @ p3) t
\<forall>p'. isPath s p' t \<longrightarrow> length p \<le> length p'
length (p1 @ p3) < length p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
isPath s (p1 @ p3) t
\<forall>p'. isPath s p' t \<longrightarrow> length p \<le> length p'
length (p1 @ p3) < length p

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shortestPath_is_path: "isShortestPath u p v \<Longrightarrow> isPath u p v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isShortestPath u p v \<Longrightarrow> isPath u p v
[PROOF STEP]
by (auto simp: isShortestPath_def)


[STATEMENT]
lemma split_shortest_path: "isShortestPath u (p1@p2) v
  \<Longrightarrow> (\<exists>w. isShortestPath u p1 w \<and> isShortestPath w p2 v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isShortestPath u (p1 @ p2) v \<Longrightarrow> \<exists>w. isShortestPath u p1 w \<and> isShortestPath w p2 v
[PROOF STEP]
apply (auto simp: isShortestPath_min_dist_def isPath_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> \<exists>w. isPath u p1 w \<and> length p1 = min_dist u w \<and> isPath w p2 v \<and> length p2 = min_dist w v
[PROOF STEP]
apply (rule exI; intro conjI; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> length p1 = min_dist u w
 2. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> length p2 = min_dist w v
[PROOF STEP]
apply (drule isPath_distD)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; dist u (length p1) w; dist w (length p2) v\<rbrakk> \<Longrightarrow> length p1 = min_dist u w
 2. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> length p2 = min_dist w v
[PROOF STEP]
using min_dist_split
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>dist ?u ?d1.0 ?w; dist ?w ?d2.0 ?v; min_dist ?u ?v = ?d1.0 + ?d2.0\<rbrakk> \<Longrightarrow> min_dist ?u ?w = ?d1.0
\<lbrakk>dist ?u ?d1.0 ?w; dist ?w ?d2.0 ?v; min_dist ?u ?v = ?d1.0 + ?d2.0\<rbrakk> \<Longrightarrow> min_dist ?w ?v = ?d2.0

goal (2 subgoals):
 1. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; dist u (length p1) w; dist w (length p2) v\<rbrakk> \<Longrightarrow> length p1 = min_dist u w
 2. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> length p2 = min_dist w v
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> length p2 = min_dist w v
[PROOF STEP]
apply (drule isPath_distD)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; dist u (length p1) w; dist w (length p2) v\<rbrakk> \<Longrightarrow> length p2 = min_dist w v
[PROOF STEP]
using min_dist_split
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>dist ?u ?d1.0 ?w; dist ?w ?d2.0 ?v; min_dist ?u ?v = ?d1.0 + ?d2.0\<rbrakk> \<Longrightarrow> min_dist ?u ?w = ?d1.0
\<lbrakk>dist ?u ?d1.0 ?w; dist ?w ?d2.0 ?v; min_dist ?u ?v = ?d1.0 + ?d2.0\<rbrakk> \<Longrightarrow> min_dist ?w ?v = ?d2.0

goal (1 subgoal):
 1. \<And>w. \<lbrakk>length p1 + length p2 = min_dist u v; dist u (length p1) w; dist w (length p2) v\<rbrakk> \<Longrightarrow> length p2 = min_dist w v
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isShortestPath_level_edge:
  assumes SP: "isShortestPath s p t"
  assumes EIP: "(u,v)\<in>set p"
  shows
    "connected s u" "connected u v" "connected v t" and
    "min_dist s v = min_dist s u + 1" (is ?G1) and
    "min_dist u t = 1 + min_dist v t" (is ?G2) and
    "min_dist s t = min_dist s u + 1 + min_dist v t" (is ?G3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((connected s u &&& connected u v &&& connected v t) &&& min_dist s v = min_dist s u + 1) &&& min_dist u t = 1 + min_dist v t &&& min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
proof -
  \<comment> \<open>Split the original path at the edge\<close>
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. connected s u
 2. connected u v
 3. connected v t
 4. min_dist s v = min_dist s u + 1
 5. min_dist u t = 1 + min_dist v t
 6. min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
from EIP
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> set p
[PROOF STEP]
obtain p1 p2 where [simp]: "p=p1@(u,v)#p2"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> set p

goal (1 subgoal):
 1. (\<And>p1 p2. p = p1 @ (u, v) # p2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: in_set_conv_decomp)
[PROOF STATE]
proof (state)
this:
p = p1 @ (u, v) # p2

goal (6 subgoals):
 1. connected s u
 2. connected u v
 3. connected v t
 4. min_dist s v = min_dist s u + 1
 5. min_dist u t = 1 + min_dist v t
 6. min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
from \<open>isShortestPath s p t\<close>
[PROOF STATE]
proof (chain)
picking this:
isShortestPath s p t
[PROOF STEP]
have
    MIN: "min_dist s t = length p" and
      P: "isPath s p t" and
     DV: "distinct (pathVertices s p)"
[PROOF STATE]
proof (prove)
using this:
isShortestPath s p t

goal (1 subgoal):
 1. min_dist s t = length p &&& isPath s p t &&& distinct (pathVertices s p)
[PROOF STEP]
by (auto simp: isShortestPath_alt isSimplePath_def)
[PROOF STATE]
proof (state)
this:
min_dist s t = length p
isPath s p t
distinct (pathVertices s p)

goal (6 subgoals):
 1. connected s u
 2. connected u v
 3. connected v t
 4. min_dist s v = min_dist s u + 1
 5. min_dist u t = 1 + min_dist v t
 6. min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
isPath s p t
[PROOF STEP]
have DISTS: "dist s (length p1) u" "dist u 1 v" "dist v (length p2) t"
[PROOF STATE]
proof (prove)
using this:
isPath s p t

goal (1 subgoal):
 1. dist s (length p1) u &&& dist u 1 v &&& dist v (length p2) t
[PROOF STEP]
by (auto simp: isPath_append dist_def intro: exI[where x="[(u,v)]"])
[PROOF STATE]
proof (state)
this:
dist s (length p1) u
dist u 1 v
dist v (length p2) t

goal (6 subgoals):
 1. connected s u
 2. connected u v
 3. connected v t
 4. min_dist s v = min_dist s u + 1
 5. min_dist u t = 1 + min_dist v t
 6. min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
from DISTS
[PROOF STATE]
proof (chain)
picking this:
dist s (length p1) u
dist u 1 v
dist v (length p2) t
[PROOF STEP]
show "connected s u" "connected u v" "connected v t"
[PROOF STATE]
proof (prove)
using this:
dist s (length p1) u
dist u 1 v
dist v (length p2) t

goal (1 subgoal):
 1. connected s u &&& connected u v &&& connected v t
[PROOF STEP]
by auto

  \<comment> \<open>Express the minimum distances in terms of the split original path\<close>
[PROOF STATE]
proof (state)
this:
connected s u
connected u v
connected v t

goal (3 subgoals):
 1. min_dist s v = min_dist s u + 1
 2. min_dist u t = 1 + min_dist v t
 3. min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
from MIN
[PROOF STATE]
proof (chain)
picking this:
min_dist s t = length p
[PROOF STEP]
have MIN': "min_dist s t = length p1 + 1 + length p2"
[PROOF STATE]
proof (prove)
using this:
min_dist s t = length p

goal (1 subgoal):
 1. min_dist s t = length p1 + 1 + length p2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min_dist s t = length p1 + 1 + length p2

goal (3 subgoals):
 1. min_dist s v = min_dist s u + 1
 2. min_dist u t = 1 + min_dist v t
 3. min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
from min_dist_split[OF dist_trans[OF DISTS(1,2)] DISTS(3) MIN']
[PROOF STATE]
proof (chain)
picking this:
min_dist s v = length p1 + 1
min_dist v t = length p2
[PROOF STEP]
have
      MDSV: "min_dist s v = length p1 + 1" and
    [simp]: "length p2 = min_dist v t"
[PROOF STATE]
proof (prove)
using this:
min_dist s v = length p1 + 1
min_dist v t = length p2

goal (1 subgoal):
 1. min_dist s v = length p1 + 1 &&& length p2 = min_dist v t
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
min_dist s v = length p1 + 1
length p2 = min_dist v t

goal (3 subgoals):
 1. min_dist s v = min_dist s u + 1
 2. min_dist u t = 1 + min_dist v t
 3. min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
from min_dist_split[OF DISTS(1) dist_trans[OF DISTS(2,3)]] MIN'
[PROOF STATE]
proof (chain)
picking this:
min_dist s t = length p1 + (1 + length p2) \<Longrightarrow> min_dist s u = length p1
min_dist s t = length p1 + (1 + length p2) \<Longrightarrow> min_dist u t = 1 + length p2
min_dist s t = length p1 + 1 + length p2
[PROOF STEP]
have
      MDUT: "min_dist u t = 1 + length p2" and
    [simp]: "length p1 = min_dist s u"
[PROOF STATE]
proof (prove)
using this:
min_dist s t = length p1 + (1 + length p2) \<Longrightarrow> min_dist s u = length p1
min_dist s t = length p1 + (1 + length p2) \<Longrightarrow> min_dist u t = 1 + length p2
min_dist s t = length p1 + 1 + length p2

goal (1 subgoal):
 1. min_dist u t = 1 + length p2 &&& length p1 = min_dist s u
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
min_dist u t = 1 + length p2
length p1 = min_dist s u

goal (3 subgoals):
 1. min_dist s v = min_dist s u + 1
 2. min_dist u t = 1 + min_dist v t
 3. min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
from MDSV MDUT MIN'
[PROOF STATE]
proof (chain)
picking this:
min_dist s v = length p1 + 1
min_dist u t = 1 + length p2
min_dist s t = length p1 + 1 + length p2
[PROOF STEP]
show ?G1 ?G2 ?G3
[PROOF STATE]
proof (prove)
using this:
min_dist s v = length p1 + 1
min_dist u t = 1 + length p2
min_dist s t = length p1 + 1 + length p2

goal (1 subgoal):
 1. min_dist s v = min_dist s u + 1 &&& min_dist u t = 1 + min_dist v t &&& min_dist s t = min_dist s u + 1 + min_dist v t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min_dist s v = min_dist s u + 1
min_dist u t = 1 + min_dist v t
min_dist s t = min_dist s u + 1 + min_dist v t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isShortestPath_length_less_V:
  assumes SV: "s\<in>V"
  assumes PATH: "isShortestPath s p t"
  shows "length p < card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
using simplePath_length_less_V[OF SV]
[PROOF STATE]
proof (prove)
using this:
isSimplePath s ?p ?v \<Longrightarrow> length ?p < card V

goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
using shortestPath_is_simple[OF PATH]
[PROOF STATE]
proof (prove)
using this:
isSimplePath s ?p ?v \<Longrightarrow> length ?p < card V
isSimplePath s p t

goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
.


[STATEMENT]
lemma d_equal_trans:
"\<lbrakk> m =\<^bsub>d\<^esub> m'; m' =\<^bsub>d\<^esub> m'' \<rbrakk> \<Longrightarrow> m =\<^bsub>d\<^esub> m''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m =\<^bsub>d\<^esub> m'; m' =\<^bsub>d\<^esub> m''\<rbrakk> \<Longrightarrow> m =\<^bsub>d\<^esub> m''
[PROOF STEP]
by (simp add: d_equal_def)


[STATEMENT]
lemma strongdB_aux: "\<And>V V' m1 m1' m2 W i. \<lbrakk> Strong_d_Bisimulation d R;
 i < length V ; (V,V') \<in> R; \<langle>V!i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1' \<rbrakk>
 \<Longrightarrow> (\<exists>W' m2'. \<langle>V'!i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (W,W') \<in> R \<and> m2 =\<^bsub>d\<^esub> m2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V V' m1 m1' m2 W i. \<lbrakk>Strong_d_Bisimulation d R; i < length V; (V, V') \<in> R; \<langle>V ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (W, W') \<in> R \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
by (simp add: Strong_d_Bisimulation_def, fastforce)


[STATEMENT]
lemma trivialpair_in_USdB:
"[] \<approx>\<^bsub>d\<^esub> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<approx>\<^bsub>d\<^esub> []
[PROOF STEP]
by (simp add: USdB_def Strong_d_Bisimulation_def,
  rule_tac x="{([],[])}" in exI, simp add: sym_def)


[STATEMENT]
lemma USdBsym: "sym (\<approx>\<^bsub>d\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (\<approx>\<^bsub>d\<^esub>)
[PROOF STEP]
by (simp add: USdB_def Strong_d_Bisimulation_def sym_def, auto)


[STATEMENT]
lemma USdBeqlen:
  "V \<approx>\<^bsub>d\<^esub> V' \<Longrightarrow> length V = length V'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<approx>\<^bsub>d\<^esub> V' \<Longrightarrow> length V = length V'
[PROOF STEP]
by (simp add: USdB_def Strong_d_Bisimulation_def, auto)


[STATEMENT]
lemma USdB_Strong_d_Bisimulation:
  "Strong_d_Bisimulation d (\<approx>\<^bsub>d\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Strong_d_Bisimulation d (\<approx>\<^bsub>d\<^esub>)
[PROOF STEP]
proof (simp add: Strong_d_Bisimulation_def, auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sym (\<approx>\<^bsub>d\<^esub>)
 2. \<And>a b. a \<approx>\<^bsub>d\<^esub> b \<Longrightarrow> length a = length b
 3. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
show "sym (\<approx>\<^bsub>d\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (\<approx>\<^bsub>d\<^esub>)
[PROOF STEP]
by (rule USdBsym)
[PROOF STATE]
proof (state)
this:
sym (\<approx>\<^bsub>d\<^esub>)

goal (2 subgoals):
 1. \<And>a b. a \<approx>\<^bsub>d\<^esub> b \<Longrightarrow> length a = length b
 2. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. a \<approx>\<^bsub>d\<^esub> b \<Longrightarrow> length a = length b
 2. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
fix V V'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. a \<approx>\<^bsub>d\<^esub> b \<Longrightarrow> length a = length b
 2. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
show "V \<approx>\<^bsub>d\<^esub> V' \<Longrightarrow> length V = length V'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<approx>\<^bsub>d\<^esub> V' \<Longrightarrow> length V = length V'
[PROOF STEP]
by (rule USdBeqlen, auto)
[PROOF STATE]
proof (state)
this:
V \<approx>\<^bsub>d\<^esub> V' \<Longrightarrow> length V = length V'

goal (1 subgoal):
 1. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
fix V V' m1 m1' m2 W i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume inUSdB: "V \<approx>\<^bsub>d\<^esub> V'"
[PROOF STATE]
proof (state)
this:
V \<approx>\<^bsub>d\<^esub> V'

goal (1 subgoal):
 1. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume stepV: "\<langle>V!i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>"
[PROOF STATE]
proof (state)
this:
\<langle>V ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>

goal (1 subgoal):
 1. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume irange: "i < length V"
[PROOF STATE]
proof (state)
this:
i < length V

goal (1 subgoal):
 1. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume dequal: "m1 =\<^bsub>d\<^esub> m1'"
[PROOF STATE]
proof (state)
this:
m1 =\<^bsub>d\<^esub> m1'

goal (1 subgoal):
 1. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
from inUSdB
[PROOF STATE]
proof (chain)
picking this:
V \<approx>\<^bsub>d\<^esub> V'
[PROOF STEP]
obtain R where someR:
    "Strong_d_Bisimulation d R \<and> (V,V') \<in> R"
[PROOF STATE]
proof (prove)
using this:
V \<approx>\<^bsub>d\<^esub> V'

goal (1 subgoal):
 1. (\<And>R. Strong_d_Bisimulation d R \<and> (V, V') \<in> R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: USdB_def, auto)
[PROOF STATE]
proof (state)
this:
Strong_d_Bisimulation d R \<and> (V, V') \<in> R

goal (1 subgoal):
 1. \<And>a b i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
with strongdB_aux stepV irange dequal
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Strong_d_Bisimulation ?d ?R; ?i < length ?V; (?V, ?V') \<in> ?R; \<langle>?V ! ?i,?m1.0\<rangle> \<rightarrow> \<langle>?W,?m2.0\<rangle>; ?m1.0 =\<^bsub>?d\<^esub> ?m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>?V' ! ?i,?m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (?W, W') \<in> ?R \<and> ?m2.0 =\<^bsub>?d\<^esub> m2'
\<langle>V ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>
i < length V
m1 =\<^bsub>d\<^esub> m1'
Strong_d_Bisimulation d R \<and> (V, V') \<in> R
[PROOF STEP]
show
    "\<exists>W' m2'. \<langle>V'!i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Strong_d_Bisimulation ?d ?R; ?i < length ?V; (?V, ?V') \<in> ?R; \<langle>?V ! ?i,?m1.0\<rangle> \<rightarrow> \<langle>?W,?m2.0\<rangle>; ?m1.0 =\<^bsub>?d\<^esub> ?m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>?V' ! ?i,?m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (?W, W') \<in> ?R \<and> ?m2.0 =\<^bsub>?d\<^esub> m2'
\<langle>V ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>
i < length V
m1 =\<^bsub>d\<^esub> m1'
Strong_d_Bisimulation d R \<and> (V, V') \<in> R

goal (1 subgoal):
 1. \<exists>W' m2'. \<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
by (simp add: USdB_def, fastforce)
[PROOF STATE]
proof (state)
this:
\<exists>W' m2'. \<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma USdBtrans: "trans (\<approx>\<^bsub>d\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (\<approx>\<^bsub>d\<^esub>)
[PROOF STEP]
proof (simp add: trans_def, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<approx>\<^bsub>d\<^esub> y; y \<approx>\<^bsub>d\<^esub> z\<rbrakk> \<Longrightarrow> x \<approx>\<^bsub>d\<^esub> z
[PROOF STEP]
fix V V' V''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<approx>\<^bsub>d\<^esub> y; y \<approx>\<^bsub>d\<^esub> z\<rbrakk> \<Longrightarrow> x \<approx>\<^bsub>d\<^esub> z
[PROOF STEP]
assume p1: "V \<approx>\<^bsub>d\<^esub> V'"
[PROOF STATE]
proof (state)
this:
V \<approx>\<^bsub>d\<^esub> V'

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<approx>\<^bsub>d\<^esub> y; y \<approx>\<^bsub>d\<^esub> z\<rbrakk> \<Longrightarrow> x \<approx>\<^bsub>d\<^esub> z
[PROOF STEP]
assume p2: "V' \<approx>\<^bsub>d\<^esub> V''"
[PROOF STATE]
proof (state)
this:
V' \<approx>\<^bsub>d\<^esub> V''

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<approx>\<^bsub>d\<^esub> y; y \<approx>\<^bsub>d\<^esub> z\<rbrakk> \<Longrightarrow> x \<approx>\<^bsub>d\<^esub> z
[PROOF STEP]
let ?R = "{(V,V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<approx>\<^bsub>d\<^esub> y; y \<approx>\<^bsub>d\<^esub> z\<rbrakk> \<Longrightarrow> x \<approx>\<^bsub>d\<^esub> z
[PROOF STEP]
from p1 p2
[PROOF STATE]
proof (chain)
picking this:
V \<approx>\<^bsub>d\<^esub> V'
V' \<approx>\<^bsub>d\<^esub> V''
[PROOF STEP]
have inRest: "(V,V'') \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
V \<approx>\<^bsub>d\<^esub> V'
V' \<approx>\<^bsub>d\<^esub> V''

goal (1 subgoal):
 1. (V, V'') \<in> {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(V, V'') \<in> {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<approx>\<^bsub>d\<^esub> y; y \<approx>\<^bsub>d\<^esub> z\<rbrakk> \<Longrightarrow> x \<approx>\<^bsub>d\<^esub> z
[PROOF STEP]
have SdB_rest: "Strong_d_Bisimulation d ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Strong_d_Bisimulation d {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}
[PROOF STEP]
proof (simp add: Strong_d_Bisimulation_def sym_def, auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y V'. \<lbrakk>x \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> y\<rbrakk> \<Longrightarrow> \<exists>V'. y \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> x
 2. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 3. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
fix V V' V''
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y V'. \<lbrakk>x \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> y\<rbrakk> \<Longrightarrow> \<exists>V'. y \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> x
 2. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 3. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume p1: "V \<approx>\<^bsub>d\<^esub> V'"
[PROOF STATE]
proof (state)
this:
V \<approx>\<^bsub>d\<^esub> V'

goal (3 subgoals):
 1. \<And>x y V'. \<lbrakk>x \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> y\<rbrakk> \<Longrightarrow> \<exists>V'. y \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> x
 2. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 3. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V \<approx>\<^bsub>d\<^esub> V'

goal (3 subgoals):
 1. \<And>x y V'. \<lbrakk>x \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> y\<rbrakk> \<Longrightarrow> \<exists>V'. y \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> x
 2. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 3. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume p2: "V' \<approx>\<^bsub>d\<^esub> V''"
[PROOF STATE]
proof (state)
this:
V' \<approx>\<^bsub>d\<^esub> V''

goal (3 subgoals):
 1. \<And>x y V'. \<lbrakk>x \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> y\<rbrakk> \<Longrightarrow> \<exists>V'. y \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> x
 2. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 3. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V' \<approx>\<^bsub>d\<^esub> V''

goal (3 subgoals):
 1. \<And>x y V'. \<lbrakk>x \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> y\<rbrakk> \<Longrightarrow> \<exists>V'. y \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> x
 2. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 3. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
from p1 USdBsym
[PROOF STATE]
proof (chain)
picking this:
V \<approx>\<^bsub>d\<^esub> V'
sym (\<approx>\<^bsub>?d\<^esub>)
[PROOF STEP]
have "V' \<approx>\<^bsub>d\<^esub> V"
[PROOF STATE]
proof (prove)
using this:
V \<approx>\<^bsub>d\<^esub> V'
sym (\<approx>\<^bsub>?d\<^esub>)

goal (1 subgoal):
 1. V' \<approx>\<^bsub>d\<^esub> V
[PROOF STEP]
by (simp add: sym_def)
[PROOF STATE]
proof (state)
this:
V' \<approx>\<^bsub>d\<^esub> V

goal (3 subgoals):
 1. \<And>x y V'. \<lbrakk>x \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> y\<rbrakk> \<Longrightarrow> \<exists>V'. y \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> x
 2. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 3. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V' \<approx>\<^bsub>d\<^esub> V

goal (3 subgoals):
 1. \<And>x y V'. \<lbrakk>x \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> y\<rbrakk> \<Longrightarrow> \<exists>V'. y \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> x
 2. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 3. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
from p2 USdBsym
[PROOF STATE]
proof (chain)
picking this:
V' \<approx>\<^bsub>d\<^esub> V''
sym (\<approx>\<^bsub>?d\<^esub>)
[PROOF STEP]
have "V'' \<approx>\<^bsub>d\<^esub> V'"
[PROOF STATE]
proof (prove)
using this:
V' \<approx>\<^bsub>d\<^esub> V''
sym (\<approx>\<^bsub>?d\<^esub>)

goal (1 subgoal):
 1. V'' \<approx>\<^bsub>d\<^esub> V'
[PROOF STEP]
by (simp add: sym_def)
[PROOF STATE]
proof (state)
this:
V'' \<approx>\<^bsub>d\<^esub> V'

goal (3 subgoals):
 1. \<And>x y V'. \<lbrakk>x \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> y\<rbrakk> \<Longrightarrow> \<exists>V'. y \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> x
 2. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 3. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V \<approx>\<^bsub>d\<^esub> V'
V' \<approx>\<^bsub>d\<^esub> V''
V' \<approx>\<^bsub>d\<^esub> V
V'' \<approx>\<^bsub>d\<^esub> V'
[PROOF STEP]
show
        "\<exists>V'. V'' \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V"
[PROOF STATE]
proof (prove)
using this:
V \<approx>\<^bsub>d\<^esub> V'
V' \<approx>\<^bsub>d\<^esub> V''
V' \<approx>\<^bsub>d\<^esub> V
V'' \<approx>\<^bsub>d\<^esub> V'

goal (1 subgoal):
 1. \<exists>V'. V'' \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V
[PROOF STEP]
by (rule_tac x="V'" in exI, auto)
[PROOF STATE]
proof (state)
this:
\<exists>V'. V'' \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V

goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
fix V V' V''
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume p1: "V \<approx>\<^bsub>d\<^esub> V'"
[PROOF STATE]
proof (state)
this:
V \<approx>\<^bsub>d\<^esub> V'

goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V \<approx>\<^bsub>d\<^esub> V'

goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume p2: "V' \<approx>\<^bsub>d\<^esub> V''"
[PROOF STATE]
proof (state)
this:
V' \<approx>\<^bsub>d\<^esub> V''

goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V' \<approx>\<^bsub>d\<^esub> V''

goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
from p1 USdBeqlen[of "V" "V'"]
[PROOF STATE]
proof (chain)
picking this:
V \<approx>\<^bsub>d\<^esub> V'
V \<approx>\<^bsub>?d\<^esub> V' \<Longrightarrow> length V = length V'
[PROOF STEP]
have "length V = length V'"
[PROOF STATE]
proof (prove)
using this:
V \<approx>\<^bsub>d\<^esub> V'
V \<approx>\<^bsub>?d\<^esub> V' \<Longrightarrow> length V = length V'

goal (1 subgoal):
 1. length V = length V'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length V = length V'

goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length V = length V'

goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
from p2 USdBeqlen[of "V'" "V''"]
[PROOF STATE]
proof (chain)
picking this:
V' \<approx>\<^bsub>d\<^esub> V''
V' \<approx>\<^bsub>?d\<^esub> V'' \<Longrightarrow> length V' = length V''
[PROOF STEP]
have "length V' = length V''"
[PROOF STATE]
proof (prove)
using this:
V' \<approx>\<^bsub>d\<^esub> V''
V' \<approx>\<^bsub>?d\<^esub> V'' \<Longrightarrow> length V' = length V''

goal (1 subgoal):
 1. length V' = length V''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length V' = length V''

goal (2 subgoals):
 1. \<And>a b V'. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b\<rbrakk> \<Longrightarrow> length a = length b
 2. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V \<approx>\<^bsub>d\<^esub> V'
V' \<approx>\<^bsub>d\<^esub> V''
length V = length V'
length V' = length V''
[PROOF STEP]
show eqlen: "length V = length V''"
[PROOF STATE]
proof (prove)
using this:
V \<approx>\<^bsub>d\<^esub> V'
V' \<approx>\<^bsub>d\<^esub> V''
length V = length V'
length V' = length V''

goal (1 subgoal):
 1. length V = length V''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length V = length V''

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
fix V V' V'' i m1 m1' W m2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume step: "\<langle>V!i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>"
[PROOF STATE]
proof (state)
this:
\<langle>V ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume dequal: "m1 =\<^bsub>d\<^esub> m1'"
[PROOF STATE]
proof (state)
this:
m1 =\<^bsub>d\<^esub> m1'

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume p1: "V \<approx>\<^bsub>d\<^esub> V'"
[PROOF STATE]
proof (state)
this:
V \<approx>\<^bsub>d\<^esub> V'

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume p2: "V' \<approx>\<^bsub>d\<^esub> V''"
[PROOF STATE]
proof (state)
this:
V' \<approx>\<^bsub>d\<^esub> V''

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
assume irange: "i < length V"
[PROOF STATE]
proof (state)
this:
i < length V

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
from p1 USdBeqlen[of "V" "V'"]
[PROOF STATE]
proof (chain)
picking this:
V \<approx>\<^bsub>d\<^esub> V'
V \<approx>\<^bsub>?d\<^esub> V' \<Longrightarrow> length V = length V'
[PROOF STEP]
have leq: "length V = length V'"
[PROOF STATE]
proof (prove)
using this:
V \<approx>\<^bsub>d\<^esub> V'
V \<approx>\<^bsub>?d\<^esub> V' \<Longrightarrow> length V = length V'

goal (1 subgoal):
 1. length V = length V'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
length V = length V'

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
have deq_same: "m1' =\<^bsub>d\<^esub> m1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1' =\<^bsub>d\<^esub> m1'
[PROOF STEP]
by (simp add: d_equal_def)
[PROOF STATE]
proof (state)
this:
m1' =\<^bsub>d\<^esub> m1'

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
from irange step dequal p1 USdB_Strong_d_Bisimulation
          strongdB_aux[of "d" "\<approx>\<^bsub>d\<^esub>" "i" "V" "V'" "m1" "W" "m2" "m1'"]
[PROOF STATE]
proof (chain)
picking this:
i < length V
\<langle>V ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>
m1 =\<^bsub>d\<^esub> m1'
V \<approx>\<^bsub>d\<^esub> V'
Strong_d_Bisimulation ?d (\<approx>\<^bsub>?d\<^esub>)
\<lbrakk>Strong_d_Bisimulation d (\<approx>\<^bsub>d\<^esub>); i < length V; V \<approx>\<^bsub>d\<^esub> V'; \<langle>V ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
obtain W' m2' where p1concl:
          "\<langle>V'!i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'"
[PROOF STATE]
proof (prove)
using this:
i < length V
\<langle>V ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>
m1 =\<^bsub>d\<^esub> m1'
V \<approx>\<^bsub>d\<^esub> V'
Strong_d_Bisimulation ?d (\<approx>\<^bsub>?d\<^esub>)
\<lbrakk>Strong_d_Bisimulation d (\<approx>\<^bsub>d\<^esub>); i < length V; V \<approx>\<^bsub>d\<^esub> V'; \<langle>V ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'

goal (1 subgoal):
 1. (\<And>W' m2'. \<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
with deq_same leq USdB_Strong_d_Bisimulation
          strongdB_aux[of "d" "\<approx>\<^bsub>d\<^esub>" "i" "V'" "V''" "m1'" "W'" "m2'" "m1'"]
          irange p2 dequal
[PROOF STATE]
proof (chain)
picking this:
m1' =\<^bsub>d\<^esub> m1'
length V = length V'
Strong_d_Bisimulation ?d (\<approx>\<^bsub>?d\<^esub>)
\<lbrakk>Strong_d_Bisimulation d (\<approx>\<^bsub>d\<^esub>); i < length V'; V' \<approx>\<^bsub>d\<^esub> V''; \<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle>; m1' =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W'a m2'a. \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'a,m2'a\<rangle> \<and> W' \<approx>\<^bsub>d\<^esub> W'a \<and> m2' =\<^bsub>d\<^esub> m2'a
i < length V
V' \<approx>\<^bsub>d\<^esub> V''
m1 =\<^bsub>d\<^esub> m1'
\<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
obtain W'' m2'' where p2concl:
          "W' \<approx>\<^bsub>d\<^esub> W'' \<and> \<langle>V''!i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> m2' =\<^bsub>d\<^esub> m2''"
[PROOF STATE]
proof (prove)
using this:
m1' =\<^bsub>d\<^esub> m1'
length V = length V'
Strong_d_Bisimulation ?d (\<approx>\<^bsub>?d\<^esub>)
\<lbrakk>Strong_d_Bisimulation d (\<approx>\<^bsub>d\<^esub>); i < length V'; V' \<approx>\<^bsub>d\<^esub> V''; \<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle>; m1' =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W'a m2'a. \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'a,m2'a\<rangle> \<and> W' \<approx>\<^bsub>d\<^esub> W'a \<and> m2' =\<^bsub>d\<^esub> m2'a
i < length V
V' \<approx>\<^bsub>d\<^esub> V''
m1 =\<^bsub>d\<^esub> m1'
\<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'

goal (1 subgoal):
 1. (\<And>W'' m2''. W' \<approx>\<^bsub>d\<^esub> W'' \<and> \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> m2' =\<^bsub>d\<^esub> m2'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W' \<approx>\<^bsub>d\<^esub> W'' \<and> \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> m2' =\<^bsub>d\<^esub> m2''

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
from p1concl p2concl d_equal_trans
[PROOF STATE]
proof (chain)
picking this:
\<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
W' \<approx>\<^bsub>d\<^esub> W'' \<and> \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> m2' =\<^bsub>d\<^esub> m2''
\<lbrakk>?m =\<^bsub>?d\<^esub> ?m'; ?m' =\<^bsub>?d\<^esub> ?m''\<rbrakk> \<Longrightarrow> ?m =\<^bsub>?d\<^esub> ?m''
[PROOF STEP]
have tt'': "m2 =\<^bsub>d\<^esub> m2''"
[PROOF STATE]
proof (prove)
using this:
\<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
W' \<approx>\<^bsub>d\<^esub> W'' \<and> \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> m2' =\<^bsub>d\<^esub> m2''
\<lbrakk>?m =\<^bsub>?d\<^esub> ?m'; ?m' =\<^bsub>?d\<^esub> ?m''\<rbrakk> \<Longrightarrow> ?m =\<^bsub>?d\<^esub> ?m''

goal (1 subgoal):
 1. m2 =\<^bsub>d\<^esub> m2''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m2 =\<^bsub>d\<^esub> m2''

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
from p1concl p2concl
[PROOF STATE]
proof (chain)
picking this:
\<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
W' \<approx>\<^bsub>d\<^esub> W'' \<and> \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> m2' =\<^bsub>d\<^esub> m2''
[PROOF STEP]
have "(W,W'') \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
\<langle>V' ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> W \<approx>\<^bsub>d\<^esub> W' \<and> m2 =\<^bsub>d\<^esub> m2'
W' \<approx>\<^bsub>d\<^esub> W'' \<and> \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> m2' =\<^bsub>d\<^esub> m2''

goal (1 subgoal):
 1. (W, W'') \<in> {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(W, W'') \<in> {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}

goal (1 subgoal):
 1. \<And>a b V' i m1 m1' m2 W. \<lbrakk>a \<approx>\<^bsub>d\<^esub> V'; V' \<approx>\<^bsub>d\<^esub> b; i < length a; \<langle>a ! i,m1\<rangle> \<rightarrow> \<langle>W,m2\<rangle>; m1 =\<^bsub>d\<^esub> m1'\<rbrakk> \<Longrightarrow> \<exists>W' m2'. \<langle>b ! i,m1'\<rangle> \<rightarrow> \<langle>W',m2'\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W') \<and> m2 =\<^bsub>d\<^esub> m2'
[PROOF STEP]
with p2concl tt''
[PROOF STATE]
proof (chain)
picking this:
W' \<approx>\<^bsub>d\<^esub> W'' \<and> \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> m2' =\<^bsub>d\<^esub> m2''
m2 =\<^bsub>d\<^esub> m2''
(W, W'') \<in> {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}
[PROOF STEP]
show "\<exists>W'' m2''. \<langle>V''!i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and>
          (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W'') \<and> m2 =\<^bsub>d\<^esub> m2''"
[PROOF STATE]
proof (prove)
using this:
W' \<approx>\<^bsub>d\<^esub> W'' \<and> \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> m2' =\<^bsub>d\<^esub> m2''
m2 =\<^bsub>d\<^esub> m2''
(W, W'') \<in> {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}

goal (1 subgoal):
 1. \<exists>W'' m2''. \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W'') \<and> m2 =\<^bsub>d\<^esub> m2''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>W'' m2''. \<langle>V'' ! i,m1'\<rangle> \<rightarrow> \<langle>W'',m2''\<rangle> \<and> (\<exists>V'. W \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> W'') \<and> m2 =\<^bsub>d\<^esub> m2''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Strong_d_Bisimulation d {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<approx>\<^bsub>d\<^esub> y; y \<approx>\<^bsub>d\<^esub> z\<rbrakk> \<Longrightarrow> x \<approx>\<^bsub>d\<^esub> z
[PROOF STEP]
hence liftup: "?R \<subseteq> (\<approx>\<^bsub>d\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
Strong_d_Bisimulation d {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}

goal (1 subgoal):
 1. {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''} \<subseteq> \<approx>\<^bsub>d\<^esub>
[PROOF STEP]
by (simp add: USdB_def, auto)
[PROOF STATE]
proof (state)
this:
{(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''} \<subseteq> \<approx>\<^bsub>d\<^esub>

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<approx>\<^bsub>d\<^esub> y; y \<approx>\<^bsub>d\<^esub> z\<rbrakk> \<Longrightarrow> x \<approx>\<^bsub>d\<^esub> z
[PROOF STEP]
with inRest
[PROOF STATE]
proof (chain)
picking this:
(V, V'') \<in> {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}
{(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''} \<subseteq> \<approx>\<^bsub>d\<^esub>
[PROOF STEP]
show "V \<approx>\<^bsub>d\<^esub> V''"
[PROOF STATE]
proof (prove)
using this:
(V, V'') \<in> {(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''}
{(V, V''). \<exists>V'. V \<approx>\<^bsub>d\<^esub> V' \<and> V' \<approx>\<^bsub>d\<^esub> V''} \<subseteq> \<approx>\<^bsub>d\<^esub>

goal (1 subgoal):
 1. V \<approx>\<^bsub>d\<^esub> V''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<approx>\<^bsub>d\<^esub> V''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sets_distinct1: "(n::int) \<noteq> m \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> m \<Longrightarrow> {(a, b). a = n} \<noteq> {(a, b). a = m}
[PROOF STEP]
by auto


[STATEMENT]
lemma sets_distinct2: "(m::int) \<noteq> n \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<noteq> n \<Longrightarrow> {(a, b). a = n} \<noteq> {(a, b). a = m}
[PROOF STEP]
by auto


[STATEMENT]
lemma sets_distinct3: "{((a::int),(b::int)). a = n} \<noteq> {(a,b). a > n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(a, b). a = n} \<noteq> {(a, b). n < a}
[PROOF STEP]
by auto


[STATEMENT]
lemma sets_distinct4: "{((a::int),(b::int)). a > n} \<noteq> {(a,b). a = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(a, b). n < a} \<noteq> {(a, b). a = n}
[PROOF STEP]
by auto


[STATEMENT]
lemma aux: "\<lbrakk>a \<in> c; a \<notin> d; c = d\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> c; a \<notin> d; c = d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto