[STATEMENT]
lemma add_leaf_awalk_new_split:
  fixes u v a
  defines "T' \<equiv> \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a},
                tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>"
  assumes "v \<notin> verts T" and "u \<in> verts T" and "p \<noteq> []" and "pre_digraph.awalk T' x p v"
  shows "\<exists>as. as @ [a] = p \<and> pre_digraph.awalk T' x as u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>as. as @ [a] = p \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
T' \<equiv> \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
v \<notin> verts T
u \<in> verts T
p \<noteq> []
pre_digraph.awalk T' x p v

goal (1 subgoal):
 1. \<exists>as. as @ [a] = p \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
proof(induction p arbitrary: x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; [] \<noteq> []; pre_digraph.awalk T' x [] v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = [] \<and> pre_digraph.awalk T' x as u
 2. \<And>aa p x. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p \<noteq> []; pre_digraph.awalk T' x p v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; aa # p \<noteq> []; pre_digraph.awalk T' x (aa # p) v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = aa # p \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' ?x2 ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' ?x2 as u
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
v \<notin> verts T
u \<in> verts T
p # ps \<noteq> []
pre_digraph.awalk T' x (p # ps) v

goal (2 subgoals):
 1. \<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; [] \<noteq> []; pre_digraph.awalk T' x [] v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = [] \<and> pre_digraph.awalk T' x as u
 2. \<And>aa p x. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p \<noteq> []; pre_digraph.awalk T' x p v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; aa # p \<noteq> []; pre_digraph.awalk T' x (aa # p) v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = aa # p \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' ?x2 ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' ?x2 as u
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
v \<notin> verts T
u \<in> verts T
p # ps \<noteq> []
pre_digraph.awalk T' x (p # ps) v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' ?x2 ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' ?x2 as u
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
v \<notin> verts T
u \<in> verts T
p # ps \<noteq> []
pre_digraph.awalk T' x (p # ps) v

goal (1 subgoal):
 1. \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
proof(cases "ps = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ps = []

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ps = []
[PROOF STEP]
have "head T' p = v"
[PROOF STATE]
proof (prove)
using this:
ps = []

goal (1 subgoal):
 1. head T' p = v
[PROOF STEP]
using Cons.prems(4)
[PROOF STATE]
proof (prove)
using this:
ps = []
pre_digraph.awalk T' x (p # ps) v

goal (1 subgoal):
 1. head T' p = v
[PROOF STEP]
by (simp add: pre_digraph.awalk_def pre_digraph.cas.simps)
[PROOF STATE]
proof (state)
this:
head T' p = v

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
head T' p = v
[PROOF STEP]
have "head T p = v \<or> p = a"
[PROOF STATE]
proof (prove)
using this:
head T' p = v

goal (1 subgoal):
 1. head T p = v \<or> p = a
[PROOF STEP]
using Cons.hyps(2)
[PROOF STATE]
proof (prove)
using this:
head T' p = v
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>

goal (1 subgoal):
 1. head T p = v \<or> p = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
head T p = v \<or> p = a

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
head T p = v \<or> p = a

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
have "p \<in> arcs T \<or> p = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> arcs T \<or> p = a
[PROOF STEP]
using Cons.hyps(2) Cons.prems(4)
[PROOF STATE]
proof (prove)
using this:
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
pre_digraph.awalk T' x (p # ps) v

goal (1 subgoal):
 1. p \<in> arcs T \<or> p = a
[PROOF STEP]
by (auto simp: pre_digraph.awalk_def)
[PROOF STATE]
proof (state)
this:
p \<in> arcs T \<or> p = a

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
head T p = v \<or> p = a
p \<in> arcs T \<or> p = a
[PROOF STEP]
have "p = a"
[PROOF STATE]
proof (prove)
using this:
head T p = v \<or> p = a
p \<in> arcs T \<or> p = a

goal (1 subgoal):
 1. p = a
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
head T p = v \<or> p = a
p \<in> arcs T \<or> p = a
v \<notin> verts T

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

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = a
[PROOF STEP]
have "[] @ [a] = p # ps"
[PROOF STATE]
proof (prove)
using this:
p = a

goal (1 subgoal):
 1. [] @ [a] = p # ps
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
p = a
ps = []

goal (1 subgoal):
 1. [] @ [a] = p # ps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[] @ [a] = p # ps

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
have "tail T' p = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tail T' p = u
[PROOF STEP]
using Cons.hyps(2) \<open>p = a\<close>
[PROOF STATE]
proof (prove)
using this:
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
p = a

goal (1 subgoal):
 1. tail T' p = u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
tail T' p = u

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tail T' p = u
[PROOF STEP]
have "u = x"
[PROOF STATE]
proof (prove)
using this:
tail T' p = u

goal (1 subgoal):
 1. u = x
[PROOF STEP]
using Cons.prems(4)
[PROOF STATE]
proof (prove)
using this:
tail T' p = u
pre_digraph.awalk T' x (p # ps) v

goal (1 subgoal):
 1. u = x
[PROOF STEP]
by (simp add: pre_digraph.awalk_def pre_digraph.cas.simps(2))
[PROOF STATE]
proof (state)
this:
u = x

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = x
[PROOF STEP]
have "pre_digraph.awalk T' x [] u"
[PROOF STATE]
proof (prove)
using this:
u = x

goal (1 subgoal):
 1. pre_digraph.awalk T' x [] u
[PROOF STEP]
using Cons.hyps(2) Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
u = x
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
u \<in> verts T

goal (1 subgoal):
 1. pre_digraph.awalk T' x [] u
[PROOF STEP]
by (simp add: pre_digraph.awalk_def pre_digraph.cas.simps)
[PROOF STATE]
proof (state)
this:
pre_digraph.awalk T' x [] u

goal (2 subgoals):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps = []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
 2. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pre_digraph.awalk T' x [] u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pre_digraph.awalk T' x [] u

goal (1 subgoal):
 1. \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
using \<open>[] @ [a] = p # ps\<close>
[PROOF STATE]
proof (prove)
using this:
pre_digraph.awalk T' x [] u
[] @ [a] = p # ps

goal (1 subgoal):
 1. \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ps \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ps \<noteq> []
[PROOF STEP]
have "pre_digraph.cas T' (head T' p) ps v"
[PROOF STATE]
proof (prove)
using this:
ps \<noteq> []

goal (1 subgoal):
 1. pre_digraph.cas T' (head T' p) ps v
[PROOF STEP]
using Cons.prems(4)
[PROOF STATE]
proof (prove)
using this:
ps \<noteq> []
pre_digraph.awalk T' x (p # ps) v

goal (1 subgoal):
 1. pre_digraph.cas T' (head T' p) ps v
[PROOF STEP]
by (simp add: pre_digraph.awalk_def pre_digraph.cas.simps)
[PROOF STATE]
proof (state)
this:
pre_digraph.cas T' (head T' p) ps v

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pre_digraph.cas T' (head T' p) ps v
[PROOF STEP]
have "pre_digraph.awalk T' (head T' p) ps v"
[PROOF STATE]
proof (prove)
using this:
pre_digraph.cas T' (head T' p) ps v

goal (1 subgoal):
 1. pre_digraph.awalk T' (head T' p) ps v
[PROOF STEP]
using Cons.hyps(2) Cons.prems(4)
[PROOF STATE]
proof (prove)
using this:
pre_digraph.cas T' (head T' p) ps v
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
pre_digraph.awalk T' x (p # ps) v

goal (1 subgoal):
 1. pre_digraph.awalk T' (head T' p) ps v
[PROOF STEP]
unfolding pre_digraph.awalk_def
[PROOF STATE]
proof (prove)
using this:
pre_digraph.cas T' (head T' p) ps v
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
x \<in> verts T' \<and> set (p # ps) \<subseteq> arcs T' \<and> pre_digraph.cas T' x (p # ps) v

goal (1 subgoal):
 1. head T' p \<in> verts T' \<and> set ps \<subseteq> arcs T' \<and> pre_digraph.cas T' (head T' p) ps v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pre_digraph.awalk T' (head T' p) ps v

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pre_digraph.awalk T' (head T' p) ps v
[PROOF STEP]
obtain as where as_def: "as @ [a] = ps" "pre_digraph.awalk T' (head T' p) as u"
[PROOF STATE]
proof (prove)
using this:
pre_digraph.awalk T' (head T' p) ps v

goal (1 subgoal):
 1. (\<And>as. \<lbrakk>as @ [a] = ps; pre_digraph.awalk T' (head T' p) as u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons False
[PROOF STATE]
proof (prove)
using this:
pre_digraph.awalk T' (head T' p) ps v
\<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' ?x2 ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' ?x2 as u
T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>
v \<notin> verts T
u \<in> verts T
p # ps \<noteq> []
pre_digraph.awalk T' x (p # ps) v
ps \<noteq> []

goal (1 subgoal):
 1. (\<And>as. \<lbrakk>as @ [a] = ps; pre_digraph.awalk T' (head T' p) as u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
as @ [a] = ps
pre_digraph.awalk T' (head T' p) as u

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as @ [a] = ps
pre_digraph.awalk T' (head T' p) as u
[PROOF STEP]
have "x \<in> verts T'" "set (p#as) \<subseteq> arcs T'" "tail T' p = x"
[PROOF STATE]
proof (prove)
using this:
as @ [a] = ps
pre_digraph.awalk T' (head T' p) as u

goal (1 subgoal):
 1. x \<in> verts T' &&& set (p # as) \<subseteq> arcs T' &&& tail T' p = x
[PROOF STEP]
using Cons.prems(4)
[PROOF STATE]
proof (prove)
using this:
as @ [a] = ps
pre_digraph.awalk T' (head T' p) as u
pre_digraph.awalk T' x (p # ps) v

goal (1 subgoal):
 1. x \<in> verts T' &&& set (p # as) \<subseteq> arcs T' &&& tail T' p = x
[PROOF STEP]
by (auto simp: pre_digraph.awalk_def pre_digraph.cas.simps)
[PROOF STATE]
proof (state)
this:
x \<in> verts T'
set (p # as) \<subseteq> arcs T'
tail T' p = x

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> verts T'
set (p # as) \<subseteq> arcs T'
tail T' p = x
[PROOF STEP]
have "pre_digraph.cas T' x (p#as) u"
[PROOF STATE]
proof (prove)
using this:
x \<in> verts T'
set (p # as) \<subseteq> arcs T'
tail T' p = x

goal (1 subgoal):
 1. pre_digraph.cas T' x (p # as) u
[PROOF STEP]
using as_def(2) pre_digraph.cas.simps(2)
[PROOF STATE]
proof (prove)
using this:
x \<in> verts T'
set (p # as) \<subseteq> arcs T'
tail T' p = x
pre_digraph.awalk T' (head T' p) as u
pre_digraph.cas ?G ?u (?e # ?es) ?v = (tail ?G ?e = ?u \<and> pre_digraph.cas ?G (head ?G ?e) ?es ?v)

goal (1 subgoal):
 1. pre_digraph.cas T' x (p # as) u
[PROOF STEP]
unfolding pre_digraph.awalk_def
[PROOF STATE]
proof (prove)
using this:
x \<in> verts T'
set (p # as) \<subseteq> arcs T'
tail T' p = x
head T' p \<in> verts T' \<and> set as \<subseteq> arcs T' \<and> pre_digraph.cas T' (head T' p) as u
pre_digraph.cas ?G ?u (?e # ?es) ?v = (tail ?G ?e = ?u \<and> pre_digraph.cas ?G (head ?G ?e) ?es ?v)

goal (1 subgoal):
 1. pre_digraph.cas T' x (p # as) u
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
pre_digraph.cas T' x (p # as) u

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pre_digraph.cas T' x (p # as) u
[PROOF STEP]
have "pre_digraph.awalk T' x (p#as) u"
[PROOF STATE]
proof (prove)
using this:
pre_digraph.cas T' x (p # as) u

goal (1 subgoal):
 1. pre_digraph.awalk T' x (p # as) u
[PROOF STEP]
using \<open>x \<in> verts T'\<close> \<open>set (p#as) \<subseteq> arcs T'\<close>
[PROOF STATE]
proof (prove)
using this:
pre_digraph.cas T' x (p # as) u
x \<in> verts T'
set (p # as) \<subseteq> arcs T'

goal (1 subgoal):
 1. pre_digraph.awalk T' x (p # as) u
[PROOF STEP]
by (simp add: pre_digraph.awalk_def)
[PROOF STATE]
proof (state)
this:
pre_digraph.awalk T' x (p # as) u

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; ps \<noteq> []; pre_digraph.awalk T' x ps v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = ps \<and> pre_digraph.awalk T' x as u; T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; p # ps \<noteq> []; pre_digraph.awalk T' x (p # ps) v; ps \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pre_digraph.awalk T' x (p # as) u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pre_digraph.awalk T' x (p # as) u

goal (1 subgoal):
 1. \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
using as_def(1)
[PROOF STATE]
proof (prove)
using this:
pre_digraph.awalk T' x (p # as) u
as @ [a] = ps

goal (1 subgoal):
 1. \<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>as. as @ [a] = p # ps \<and> pre_digraph.awalk T' x as u

goal (1 subgoal):
 1. \<And>x. \<lbrakk>T' = \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>; v \<notin> verts T; u \<in> verts T; [] \<noteq> []; pre_digraph.awalk T' x [] v\<rbrakk> \<Longrightarrow> \<exists>as. as @ [a] = [] \<and> pre_digraph.awalk T' x as u
[PROOF STEP]
qed(simp)


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


[STATEMENT]
lemma (in fin_digraph) sp_costs_finite: "finite (sp_costs f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (sp_costs f)
[PROOF STEP]
unfolding sp_costs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {uu_. \<exists>u v c. uu_ = c \<and> u \<in> verts G \<and> v \<in> verts G \<and> \<mu> f u v = c}
[PROOF STEP]
by auto


[STATEMENT]
lemma source_mem_nnvs: "n_nearest_verts w u n U \<Longrightarrow> u \<in> verts G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_nearest_verts w u n U \<Longrightarrow> u \<in> verts G
[PROOF STEP]
by (induction rule: n_nearest_verts.induct) auto


[STATEMENT]
lemma new_element_get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t:
  "h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M ptr getter) h h'
[PROOF STEP]
by(auto simp add: new_element_def get_M_defs preserved_def
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)


[STATEMENT]
lemma sorted_list_of_set_inj_aux:
    fixes A B :: "'a set"
    assumes "finite A"
    assumes "finite B"
    assumes "sorted_list_of_set A = sorted_list_of_set B"
    shows "A=B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
sorted_list_of_set A = sorted_list_of_set B

goal (1 subgoal):
 1. A = B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; sorted_list_of_set A = sorted_list_of_set B\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
from \<open>finite B\<close>
[PROOF STATE]
proof (chain)
picking this:
finite B
[PROOF STEP]
have "B = set (sorted_list_of_set B)"
[PROOF STATE]
proof (prove)
using this:
finite B

goal (1 subgoal):
 1. B = set (sorted_list_of_set B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B = set (sorted_list_of_set B)

goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; sorted_list_of_set A = sorted_list_of_set B\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B = set (sorted_list_of_set B)

goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; sorted_list_of_set A = sorted_list_of_set B\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
finite B
sorted_list_of_set A = sorted_list_of_set B
[PROOF STEP]
have "\<dots> = set (sorted_list_of_set (A))"
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
sorted_list_of_set A = sorted_list_of_set B

goal (1 subgoal):
 1. set (sorted_list_of_set B) = set (sorted_list_of_set A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (sorted_list_of_set B) = set (sorted_list_of_set A)

goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; sorted_list_of_set A = sorted_list_of_set B\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (sorted_list_of_set B) = set (sorted_list_of_set A)

goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; sorted_list_of_set A = sorted_list_of_set B\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
from \<open>finite A\<close>
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "set (sorted_list_of_set (A)) = A"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. set (sorted_list_of_set A) = A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (sorted_list_of_set A) = A

goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; sorted_list_of_set A = sorted_list_of_set B\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
B = A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
B = A

goal (1 subgoal):
 1. A = B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A = B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma redT_updWs_not_Suspend_Some:
  "\<lbrakk> redT_updWs t ws was ws'; ws' t = \<lfloor>w'\<rfloor>; ws t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set was \<rbrakk>
  \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>redT_updWs t ws was ws'; ws' t = \<lfloor>w'\<rfloor>; ws t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set was\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
unfolding redT_updWs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rtrancl3p (redT_updW t) ws was ws'; ws' t = \<lfloor>w'\<rfloor>; ws t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set was\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
proof(induct arbitrary: w rule: rtrancl3p_converse_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a w. \<lbrakk>a t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set []\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
 2. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
a_ t = \<lfloor>w'\<rfloor>
a_ t = \<lfloor>w\<rfloor>
Suspend ?w \<notin> set []

goal (2 subgoals):
 1. \<And>a w. \<lbrakk>a t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set []\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
 2. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a_ t = \<lfloor>w'\<rfloor>
a_ t = \<lfloor>w\<rfloor>
Suspend ?w \<notin> set []

goal (1 subgoal):
 1. w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
case (step ws wa ws' was ws'')
[PROOF STATE]
proof (state)
this:
rtrancl3p (redT_updW t) ws' was ws''
redT_updW t ws wa ws'
\<lbrakk>ws'' t = \<lfloor>w'\<rfloor>; ws' t = \<lfloor>?w\<rfloor>; \<And>w. Suspend w \<notin> set was\<rbrakk> \<Longrightarrow> w' = ?w \<or> (\<exists>w'' w'''. ?w = InWS w'' \<and> w' = PostWS w''')
ws'' t = \<lfloor>w'\<rfloor>
ws t = \<lfloor>w\<rfloor>
Suspend ?w \<notin> set (wa # was)

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
note \<open>ws'' t = \<lfloor>w'\<rfloor>\<close>
[PROOF STATE]
proof (state)
this:
ws'' t = \<lfloor>w'\<rfloor>

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ws'' t = \<lfloor>w'\<rfloor>

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
have "ws' t \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ws' t \<noteq> None
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ws' t = None \<Longrightarrow> False
[PROOF STEP]
assume "ws' t = None"
[PROOF STATE]
proof (state)
this:
ws' t = None

goal (1 subgoal):
 1. ws' t = None \<Longrightarrow> False
[PROOF STEP]
with \<open>rtrancl3p (redT_updW t) ws' was ws''\<close> \<open>ws'' t = \<lfloor>w'\<rfloor>\<close>
[PROOF STATE]
proof (chain)
picking this:
rtrancl3p (redT_updW t) ws' was ws''
ws'' t = \<lfloor>w'\<rfloor>
ws' t = None
[PROOF STEP]
obtain w' where "Suspend w' \<in> set was"
[PROOF STATE]
proof (prove)
using this:
rtrancl3p (redT_updW t) ws' was ws''
ws'' t = \<lfloor>w'\<rfloor>
ws' t = None

goal (1 subgoal):
 1. (\<And>w'. Suspend w' \<in> set was \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding redT_updWs_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
redT_updWs t ws' was ws''
ws'' t = \<lfloor>w'\<rfloor>
ws' t = None

goal (1 subgoal):
 1. (\<And>w'. Suspend w' \<in> set was \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto dest: redT_updWs_None_SomeD)
[PROOF STATE]
proof (state)
this:
Suspend w' \<in> set was

goal (1 subgoal):
 1. ws' t = None \<Longrightarrow> False
[PROOF STEP]
with \<open>Suspend w' \<notin> set (wa # was)\<close>
[PROOF STATE]
proof (chain)
picking this:
Suspend w' \<notin> set (wa # was)
Suspend w' \<in> set was
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Suspend w' \<notin> set (wa # was)
Suspend w' \<in> set was

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ws' t \<noteq> None

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ws' t \<noteq> None
[PROOF STEP]
obtain w'' where "ws' t = \<lfloor>w''\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
ws' t \<noteq> None

goal (1 subgoal):
 1. (\<And>w''. ws' t = \<lfloor>w''\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ws' t = \<lfloor>w''\<rfloor>

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ws' t = \<lfloor>w''\<rfloor>

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ws' t = \<lfloor>w''\<rfloor>

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
from \<open>Suspend w \<notin> set (wa # was)\<close>
[PROOF STATE]
proof (chain)
picking this:
Suspend w \<notin> set (wa # was)
[PROOF STEP]
have "Suspend w \<notin> set was"
[PROOF STATE]
proof (prove)
using this:
Suspend w \<notin> set (wa # was)

goal (1 subgoal):
 1. Suspend w \<notin> set was
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suspend w \<notin> set was

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Suspend ?wc2 \<notin> set was

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ws'' t = \<lfloor>w'\<rfloor>
ws' t = \<lfloor>w''\<rfloor>
Suspend ?wc2 \<notin> set was
[PROOF STEP]
have "w' = w'' \<or> (\<exists>w''' w''''. w'' = InWS w''' \<and> w' = PostWS w'''')"
[PROOF STATE]
proof (prove)
using this:
ws'' t = \<lfloor>w'\<rfloor>
ws' t = \<lfloor>w''\<rfloor>
Suspend ?wc2 \<notin> set was

goal (1 subgoal):
 1. w' = w'' \<or> (\<exists>w''' w''''. w'' = InWS w''' \<and> w' = PostWS w'''')
[PROOF STEP]
by(rule step.hyps)
[PROOF STATE]
proof (state)
this:
w' = w'' \<or> (\<exists>w''' w''''. w'' = InWS w''' \<and> w' = PostWS w'''')

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w' = w'' \<or> (\<exists>w''' w''''. w'' = InWS w''' \<and> w' = PostWS w'''')

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
w' = w'' \<or> (\<exists>w''' w''''. w'' = InWS w''' \<and> w' = PostWS w'''')

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
from \<open>Suspend w \<notin> set (wa # was)\<close>
[PROOF STATE]
proof (chain)
picking this:
Suspend w \<notin> set (wa # was)
[PROOF STEP]
have "wa \<noteq> Suspend w"
[PROOF STATE]
proof (prove)
using this:
Suspend w \<notin> set (wa # was)

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

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
wa \<noteq> Suspend ?wc2

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
note redT_updW_not_Suspend_Some[OF \<open>redT_updW t ws wa ws'\<close>, OF \<open>ws' t = \<lfloor>w''\<rfloor>\<close> \<open>ws t = \<lfloor>w\<rfloor>\<close> this]
[PROOF STATE]
proof (state)
this:
w'' = w \<or> (\<exists>w''a w'''. w = InWS w''a \<and> w'' = PostWS w''')

goal (1 subgoal):
 1. \<And>a b a' bs a'' w. \<lbrakk>rtrancl3p (redT_updW t) a' bs a''; redT_updW t a b a'; \<And>w. \<lbrakk>a'' t = \<lfloor>w'\<rfloor>; a' t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set bs\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w'''); a'' t = \<lfloor>w'\<rfloor>; a t = \<lfloor>w\<rfloor>; \<And>w. Suspend w \<notin> set (b # bs)\<rbrakk> \<Longrightarrow> w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w' = w'' \<or> (\<exists>w''' w''''. w'' = InWS w''' \<and> w' = PostWS w'''')
w'' = w \<or> (\<exists>w''a w'''. w = InWS w''a \<and> w'' = PostWS w''')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
w' = w'' \<or> (\<exists>w''' w''''. w'' = InWS w''' \<and> w' = PostWS w'''')
w'' = w \<or> (\<exists>w''a w'''. w = InWS w''a \<and> w'' = PostWS w''')

goal (1 subgoal):
 1. w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w' = w \<or> (\<exists>w'' w'''. w = InWS w'' \<and> w' = PostWS w''')

goal:
No subgoals!
[PROOF STEP]
qed