[STATEMENT]
theorem bags_separate:
  assumes st: "s \<rightarrow>\<^bsub>T\<^esub> t" and v: "v \<in> left_part s t" and w: "w \<in> left_part t s" and xs: "v \<leadsto>xs\<leadsto> w"
  shows "set xs \<inter> bag s \<inter> bag t \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<inter> bag s \<inter> bag t \<noteq> {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
\<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}

goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}

goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "u \<in> set xs"
[PROOF STATE]
proof (state)
this:
u \<in> set xs

goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
with xs v \<open>\<not>?thesis\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<leadsto>xs\<leadsto> w
v \<in> left_part s t
\<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}
u \<in> set xs
[PROOF STEP]
have "vertex_subtree u \<subseteq> T.left_tree s t"
[PROOF STATE]
proof (prove)
using this:
v \<leadsto>xs\<leadsto> w
v \<in> left_part s t
\<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}
u \<in> set xs

goal (1 subgoal):
 1. vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
proof (induct xs arbitrary: v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
case (Cons x xs v)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v \<leadsto>xs\<leadsto> w; ?v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
v \<leadsto>(x # xs)\<leadsto> w
v \<in> left_part s t
\<not> set (x # xs) \<inter> bag s \<inter> bag t \<noteq> {}
u \<in> set (x # xs)

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
hence contra: "v \<notin> bag s \<or> v \<notin> bag t"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<leadsto>xs\<leadsto> w; ?v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
v \<leadsto>(x # xs)\<leadsto> w
v \<in> left_part s t
\<not> set (x # xs) \<inter> bag s \<inter> bag t \<noteq> {}
u \<in> set (x # xs)

goal (1 subgoal):
 1. v \<notin> bag s \<or> v \<notin> bag t
[PROOF STEP]
by (metis path_from_toE IntI empty_iff hd_in_set)
[PROOF STATE]
proof (state)
this:
v \<notin> bag s \<or> v \<notin> bag t

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v \<notin> bag s \<or> v \<notin> bag t

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
assume "x = u" "\<not>vertex_subtree u \<subseteq> T.left_tree s t"
[PROOF STATE]
proof (state)
this:
x = u
\<not> vertex_subtree u \<subseteq> T.left_tree s t

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = u
\<not> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
obtain z where z: "z \<in> vertex_subtree u" "z \<notin> T.left_tree s t"
[PROOF STATE]
proof (prove)
using this:
x = u
\<not> vertex_subtree u \<subseteq> T.left_tree s t

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> vertex_subtree u; z \<notin> T.left_tree s t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> vertex_subtree u
z \<notin> T.left_tree s t

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
hence "z \<in> vertex_subtree v"
[PROOF STATE]
proof (prove)
using this:
z \<in> vertex_subtree u
z \<notin> T.left_tree s t

goal (1 subgoal):
 1. z \<in> vertex_subtree v
[PROOF STEP]
using Cons.prems(1,3) \<open>x = u\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> vertex_subtree u
z \<notin> T.left_tree s t
v \<leadsto>(x # xs)\<leadsto> w
\<not> set (x # xs) \<inter> bag s \<inter> bag t \<noteq> {}
x = u

goal (1 subgoal):
 1. z \<in> vertex_subtree v
[PROOF STEP]
by (metis list.sel(1) path_from_to_def)
[PROOF STATE]
proof (state)
this:
z \<in> vertex_subtree v

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
hence "v \<in> left_part t s"
[PROOF STATE]
proof (prove)
using this:
z \<in> vertex_subtree v

goal (1 subgoal):
 1. v \<in> left_part t s
[PROOF STEP]
unfolding vertex_subtree_def
[PROOF STATE]
proof (prove)
using this:
z \<in> {t \<in> V\<^bsub>T\<^esub>. v \<in> bag t}

goal (1 subgoal):
 1. v \<in> left_part t s
[PROOF STEP]
using T.left_tree_union_V z st
[PROOF STATE]
proof (prove)
using this:
z \<in> {t \<in> V\<^bsub>T\<^esub>. v \<in> bag t}
?s \<rightarrow>\<^bsub>T\<^esub> ?t \<Longrightarrow> T.left_tree ?s ?t \<union> T.left_tree ?t ?s = V\<^bsub>T\<^esub>
z \<in> vertex_subtree u
z \<notin> T.left_tree s t
s \<rightarrow>\<^bsub>T\<^esub> t

goal (1 subgoal):
 1. v \<in> left_part t s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> left_part t s

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
v \<in> left_part t s

goal (1 subgoal):
 1. False
[PROOF STEP]
using vertex_in_separator contra st Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
v \<in> left_part t s
\<lbrakk>?s \<rightarrow>\<^bsub>T\<^esub> ?t; ?v \<in> left_part ?s ?t; ?v \<in> left_part ?t ?s\<rbrakk> \<Longrightarrow> ?v \<in> bag ?s
\<lbrakk>?s \<rightarrow>\<^bsub>T\<^esub> ?t; ?v \<in> left_part ?s ?t; ?v \<in> left_part ?t ?s\<rbrakk> \<Longrightarrow> ?v \<in> bag ?t
v \<notin> bag s \<or> v \<notin> bag t
s \<rightarrow>\<^bsub>T\<^esub> t
v \<in> left_part s t

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

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = u; \<not> vertex_subtree u \<subseteq> T.left_tree s t\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = u; \<not> vertex_subtree u \<subseteq> T.left_tree s t\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = u; \<not> vertex_subtree u \<subseteq> T.left_tree s t\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
assume "x \<noteq> u"
[PROOF STATE]
proof (state)
this:
x \<noteq> u

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
hence "u \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> u

goal (1 subgoal):
 1. u \<in> set xs
[PROOF STEP]
using Cons.prems(4)
[PROOF STATE]
proof (prove)
using this:
x \<noteq> u
u \<in> set (x # xs)

goal (1 subgoal):
 1. u \<in> set xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> set xs

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<in> set xs

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
hence "xs \<noteq> Nil"
[PROOF STATE]
proof (prove)
using this:
u \<in> set xs

goal (1 subgoal):
 1. xs \<noteq> []
[PROOF STEP]
using empty_iff list.set(1)
[PROOF STATE]
proof (prove)
using this:
u \<in> set xs
(?c \<in> {}) = False
set [] = {}

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

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
hence "last xs = w"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. last xs = w
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
v \<leadsto>(x # xs)\<leadsto> w

goal (1 subgoal):
 1. last xs = w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
last xs = w

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last xs = w

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
have "path xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path xs
[PROOF STEP]
using Cons.prems(1) walk_tl
[PROOF STATE]
proof (prove)
using this:
v \<leadsto>(x # xs)\<leadsto> w
walk ?xs \<Longrightarrow> walk (tl ?xs)

goal (1 subgoal):
 1. path xs
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
path xs

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path xs

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
have "hd xs \<in> left_part s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd xs \<in> left_part s t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hd xs \<in> left_part s t
[PROOF STEP]
have "v\<rightarrow>hd xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<rightarrow> hd xs
[PROOF STEP]
using Cons.prems(1,3) \<open>xs \<noteq> Nil\<close> walk_first_edge'
[PROOF STATE]
proof (prove)
using this:
v \<leadsto>(x # xs)\<leadsto> w
\<not> set (x # xs) \<inter> bag s \<inter> bag t \<noteq> {}
xs \<noteq> []
\<lbrakk>walk (?v # ?xs); ?xs \<noteq> []\<rbrakk> \<Longrightarrow> ?v \<rightarrow> hd ?xs

goal (1 subgoal):
 1. v \<rightarrow> hd xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<rightarrow> hd xs

goal (1 subgoal):
 1. hd xs \<in> left_part s t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<rightarrow> hd xs
[PROOF STEP]
obtain u' where u': "u' \<in> V\<^bsub>T\<^esub>" "v \<in> bag u'" "hd xs \<in> bag u'"
[PROOF STATE]
proof (prove)
using this:
v \<rightarrow> hd xs

goal (1 subgoal):
 1. (\<And>u'. \<lbrakk>u' \<in> V\<^bsub>T\<^esub>; v \<in> bag u'; hd xs \<in> bag u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bags_edges
[PROOF STATE]
proof (prove)
using this:
v \<rightarrow> hd xs
?v \<rightarrow> ?w \<Longrightarrow> \<exists>t\<in>V\<^bsub>T\<^esub>. ?v \<in> bag t \<and> ?w \<in> bag t

goal (1 subgoal):
 1. (\<And>u'. \<lbrakk>u' \<in> V\<^bsub>T\<^esub>; v \<in> bag u'; hd xs \<in> bag u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' \<in> V\<^bsub>T\<^esub>
v \<in> bag u'
hd xs \<in> bag u'

goal (1 subgoal):
 1. hd xs \<in> left_part s t
[PROOF STEP]
hence "u' \<in> T.left_tree s t"
[PROOF STATE]
proof (prove)
using this:
u' \<in> V\<^bsub>T\<^esub>
v \<in> bag u'
hd xs \<in> bag u'

goal (1 subgoal):
 1. u' \<in> T.left_tree s t
[PROOF STEP]
using contra vertex_in_separator st T.left_tree_union_V Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
u' \<in> V\<^bsub>T\<^esub>
v \<in> bag u'
hd xs \<in> bag u'
v \<notin> bag s \<or> v \<notin> bag t
\<lbrakk>?s \<rightarrow>\<^bsub>T\<^esub> ?t; ?v \<in> left_part ?s ?t; ?v \<in> left_part ?t ?s\<rbrakk> \<Longrightarrow> ?v \<in> bag ?s
\<lbrakk>?s \<rightarrow>\<^bsub>T\<^esub> ?t; ?v \<in> left_part ?s ?t; ?v \<in> left_part ?t ?s\<rbrakk> \<Longrightarrow> ?v \<in> bag ?t
s \<rightarrow>\<^bsub>T\<^esub> t
?s \<rightarrow>\<^bsub>T\<^esub> ?t \<Longrightarrow> T.left_tree ?s ?t \<union> T.left_tree ?t ?s = V\<^bsub>T\<^esub>
v \<in> left_part s t

goal (1 subgoal):
 1. u' \<in> T.left_tree s t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' \<in> T.left_tree s t

goal (1 subgoal):
 1. hd xs \<in> left_part s t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u' \<in> T.left_tree s t

goal (1 subgoal):
 1. hd xs \<in> left_part s t
[PROOF STEP]
using u'(3)
[PROOF STATE]
proof (prove)
using this:
u' \<in> T.left_tree s t
hd xs \<in> bag u'

goal (1 subgoal):
 1. hd xs \<in> left_part s t
[PROOF STEP]
unfolding left_part_def
[PROOF STATE]
proof (prove)
using this:
u' \<in> T.left_tree s t
hd xs \<in> bag u'

goal (1 subgoal):
 1. hd xs \<in> \<Union> {bag u |u. u \<in> T.left_tree s t}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hd xs \<in> left_part s t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hd xs \<in> left_part s t

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hd xs \<in> left_part s t

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
have "\<not>set xs \<inter> bag s \<inter> bag t \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}
[PROOF STEP]
using Cons.prems(3)
          IntI disjoint_iff_not_equal inf_le1 inf_le2 set_subset_Cons subsetCE
[PROOF STATE]
proof (prove)
using this:
\<not> set (x # xs) \<inter> bag s \<inter> bag t \<noteq> {}
\<lbrakk>?c \<in> ?A; ?c \<in> ?B\<rbrakk> \<Longrightarrow> ?c \<in> ?A \<inter> ?B
(?A \<inter> ?B = {}) = (\<forall>x\<in>?A. \<forall>y\<in>?B. x \<noteq> y)
inf ?x ?y \<le> ?x
inf ?x ?y \<le> ?y
set ?xs \<subseteq> set (?x # ?xs)
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?A \<Longrightarrow> ?P; ?c \<in> ?B \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<in> set xs
xs \<noteq> []
last xs = w
path xs
hd xs \<in> left_part s t
\<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}
[PROOF STEP]
have "vertex_subtree u \<subseteq> T.left_tree s t"
[PROOF STATE]
proof (prove)
using this:
u \<in> set xs
xs \<noteq> []
last xs = w
path xs
hd xs \<in> left_part s t
\<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}

goal (1 subgoal):
 1. vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
u \<in> set xs
xs \<noteq> []
last xs = w
path xs
hd xs \<in> left_part s t
\<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}
\<lbrakk>?v \<leadsto>xs\<leadsto> w; ?v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t

goal (1 subgoal):
 1. vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vertex_subtree u \<subseteq> T.left_tree s t

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x \<noteq> u \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t

goal (2 subgoals):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
 2. \<And>a xs v. \<lbrakk>\<And>v. \<lbrakk>v \<leadsto>xs\<leadsto> w; v \<in> left_part s t; \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set xs\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t; v \<leadsto>(a # xs)\<leadsto> w; v \<in> left_part s t; \<not> set (a # xs) \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set (a # xs)\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x = u; \<not> vertex_subtree u \<subseteq> T.left_tree s t\<rbrakk> \<Longrightarrow> False
x \<noteq> u \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = u; \<not> vertex_subtree u \<subseteq> T.left_tree s t\<rbrakk> \<Longrightarrow> False
x \<noteq> u \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t

goal (1 subgoal):
 1. vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vertex_subtree u \<subseteq> T.left_tree s t

goal (1 subgoal):
 1. \<And>v. \<lbrakk>v \<leadsto>[]\<leadsto> w; v \<in> left_part s t; \<not> set [] \<inter> bag s \<inter> bag t \<noteq> {}; u \<in> set []\<rbrakk> \<Longrightarrow> vertex_subtree u \<subseteq> T.left_tree s t
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
vertex_subtree u \<subseteq> T.left_tree s t

goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?u2 \<in> set xs \<Longrightarrow> vertex_subtree ?u2 \<subseteq> T.left_tree s t

goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
hence "vertex_subtree w \<subseteq> T.left_tree s t"
[PROOF STATE]
proof (prove)
using this:
?u2 \<in> set xs \<Longrightarrow> vertex_subtree ?u2 \<subseteq> T.left_tree s t

goal (1 subgoal):
 1. vertex_subtree w \<subseteq> T.left_tree s t
[PROOF STEP]
using xs last_in_set
[PROOF STATE]
proof (prove)
using this:
?u2 \<in> set xs \<Longrightarrow> vertex_subtree ?u2 \<subseteq> T.left_tree s t
v \<leadsto>xs\<leadsto> w
?as \<noteq> [] \<Longrightarrow> last ?as \<in> set ?as

goal (1 subgoal):
 1. vertex_subtree w \<subseteq> T.left_tree s t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vertex_subtree w \<subseteq> T.left_tree s t

goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vertex_subtree w \<subseteq> T.left_tree s t

goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
have "vertex_subtree w \<inter> T.left_tree t s \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertex_subtree w \<inter> T.left_tree t s \<noteq> {}
[PROOF STEP]
using w
[PROOF STATE]
proof (prove)
using this:
w \<in> left_part t s

goal (1 subgoal):
 1. vertex_subtree w \<inter> T.left_tree t s \<noteq> {}
[PROOF STEP]
unfolding left_part_def T.left_tree_def
[PROOF STATE]
proof (prove)
using this:
w \<in> \<Union> {bag u |u. u \<in> {u \<in> V\<^bsub>T\<^esub>. t \<in> set (u \<leadsto>\<^bsub>T\<^esub> s)}}

goal (1 subgoal):
 1. vertex_subtree w \<inter> {u \<in> V\<^bsub>T\<^esub>. t \<in> set (u \<leadsto>\<^bsub>T\<^esub> s)} \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vertex_subtree w \<inter> T.left_tree t s \<noteq> {}

goal (1 subgoal):
 1. \<not> set xs \<inter> bag s \<inter> bag t \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vertex_subtree w \<subseteq> T.left_tree s t
vertex_subtree w \<inter> T.left_tree t s \<noteq> {}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
vertex_subtree w \<subseteq> T.left_tree s t
vertex_subtree w \<inter> T.left_tree t s \<noteq> {}

goal (1 subgoal):
 1. False
[PROOF STEP]
using T.left_tree_disjoint st
[PROOF STATE]
proof (prove)
using this:
vertex_subtree w \<subseteq> T.left_tree s t
vertex_subtree w \<inter> T.left_tree t s \<noteq> {}
?s \<rightarrow>\<^bsub>T\<^esub> ?t \<Longrightarrow> T.left_tree ?s ?t \<inter> T.left_tree ?t ?s = {}
s \<rightarrow>\<^bsub>T\<^esub> t

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_result1_converg_phi:
  assumes "\<phi> i x \<down>= v"
  shows "\<exists>t.
    (\<forall>t'\<ge>t. eval r_result1 [t', i, x] \<down>= Suc v) \<and>
    (\<forall>t'<t. eval r_result1 [t', i, x] \<down>= 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. (\<forall>t'\<ge>t. eval r_result1 [t', i, x] \<down>= Suc v) \<and> (\<forall>t'<t. eval r_result1 [t', i, x] \<down>= 0)
[PROOF STEP]
using assms r_result1_converg' phi_def
[PROOF STATE]
proof (prove)
using this:
\<phi> i x \<down>= v
eval r_phi [?i, ?x] \<down>= ?v \<Longrightarrow> \<exists>t. (\<forall>t'\<ge>t. eval r_result1 [t', ?i, ?x] \<down>= Suc ?v) \<and> (\<forall>t'<t. eval r_result1 [t', ?i, ?x] \<down>= 0)
\<phi> ?i ?x \<equiv> eval r_phi [?i, ?x]

goal (1 subgoal):
 1. \<exists>t. (\<forall>t'\<ge>t. eval r_result1 [t', i, x] \<down>= Suc v) \<and> (\<forall>t'<t. eval r_result1 [t', i, x] \<down>= 0)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma r_result1_bivalent':
  assumes "eval r_phi [i, x] \<down>= v"
  shows "eval r_result1 [t, i, x] \<down>= Suc v \<or> eval r_result1 [t, i, x] \<down>= 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_result1 [t, i, x] \<down>= Suc v \<or> eval r_result1 [t, i, x] \<down>= 0
[PROOF STEP]
using assms r_result1 r_result_bivalent' r_phi''
[PROOF STATE]
proof (prove)
using this:
eval r_phi [i, x] \<down>= v
eval r_result1 [?t, ?i, ?x] = eval r_result [?t, ?i, singleton_encode ?x]
eval r_univ [?i, ?x] \<down>= ?v \<Longrightarrow> eval r_result [?t, ?i, ?x] \<down>= Suc ?v \<or> eval r_result [?t, ?i, ?x] \<down>= 0
eval r_phi [?i, ?x] = eval r_univ [?i, singleton_encode ?x]

goal (1 subgoal):
 1. eval r_result1 [t, i, x] \<down>= Suc v \<or> eval r_result1 [t, i, x] \<down>= 0
[PROOF STEP]
by simp


[STATEMENT]
lemma r_result1_bivalent_phi:
  assumes "\<phi> i x \<down>= v"
  shows "eval r_result1 [t, i, x] \<down>= Suc v \<or> eval r_result1 [t, i, x] \<down>= 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_result1 [t, i, x] \<down>= Suc v \<or> eval r_result1 [t, i, x] \<down>= 0
[PROOF STEP]
using assms r_result1_bivalent' phi_def
[PROOF STATE]
proof (prove)
using this:
\<phi> i x \<down>= v
eval r_phi [?i, ?x] \<down>= ?v \<Longrightarrow> eval r_result1 [?t, ?i, ?x] \<down>= Suc ?v \<or> eval r_result1 [?t, ?i, ?x] \<down>= 0
\<phi> ?i ?x \<equiv> eval r_phi [?i, ?x]

goal (1 subgoal):
 1. eval r_result1 [t, i, x] \<down>= Suc v \<or> eval r_result1 [t, i, x] \<down>= 0
[PROOF STEP]
by simp_all


[STATEMENT]
lemma r_result1_diverg_phi:
  assumes "\<phi> i x \<up>"
  shows "eval r_result1 [t, i, x] \<down>= 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_result1 [t, i, x] \<down>= 0
[PROOF STEP]
using assms phi_def r_result1_diverg'
[PROOF STATE]
proof (prove)
using this:
\<phi> i x \<up>
\<phi> ?i ?x \<equiv> eval r_phi [?i, ?x]
eval r_phi [?i, ?x] \<up> \<Longrightarrow> eval r_result1 [?t, ?i, ?x] \<down>= 0

goal (1 subgoal):
 1. eval r_result1 [t, i, x] \<down>= 0
[PROOF STEP]
by simp


[STATEMENT]
lemma r_result1_some_phi:
  assumes "eval r_result1 [t, i, x] \<down>= Suc v"
  shows "\<phi> i x \<down>= v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i x \<down>= v
[PROOF STEP]
using assms phi_def r_result1_Some'
[PROOF STATE]
proof (prove)
using this:
eval r_result1 [t, i, x] \<down>= Suc v
\<phi> ?i ?x \<equiv> eval r_phi [?i, ?x]
eval r_result1 [?t, ?i, ?x] \<down>= Suc ?v \<Longrightarrow> eval r_phi [?i, ?x] \<down>= ?v

goal (1 subgoal):
 1. \<phi> i x \<down>= v
[PROOF STEP]
by simp


[STATEMENT]
lemma r_result1_saturating_the:
  assumes "the (eval r_result1 [t, i, x]) > 0" and "t' \<ge> t"
  shows "the (eval r_result1 [t', i, x]) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < the (eval r_result1 [t', i, x])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < the (eval r_result1 [t', i, x])
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
0 < the (eval r_result1 [t, i, x])
[PROOF STEP]
obtain v where "eval r_result1 [t, i, x] \<down>= Suc v"
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [t, i, x])

goal (1 subgoal):
 1. (\<And>v. eval r_result1 [t, i, x] \<down>= Suc v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using r_result1_bivalent_phi r_result1_diverg_phi
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [t, i, x])
\<phi> ?i ?x \<down>= ?v \<Longrightarrow> eval r_result1 [?t, ?i, ?x] \<down>= Suc ?v \<or> eval r_result1 [?t, ?i, ?x] \<down>= 0
\<phi> ?i ?x \<up> \<Longrightarrow> eval r_result1 [?t, ?i, ?x] \<down>= 0

goal (1 subgoal):
 1. (\<And>v. eval r_result1 [t, i, x] \<down>= Suc v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis inc_induct le_0_eq not_less_zero option.discI option.expand option.sel)
[PROOF STATE]
proof (state)
this:
eval r_result1 [t, i, x] \<down>= Suc v

goal (1 subgoal):
 1. 0 < the (eval r_result1 [t', i, x])
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < the (eval r_result1 [t, i, x])
t \<le> t'
eval r_result1 [t, i, x] \<down>= Suc v
[PROOF STEP]
have "eval r_result1 [t', i, x] \<down>= Suc v"
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [t, i, x])
t \<le> t'
eval r_result1 [t, i, x] \<down>= Suc v

goal (1 subgoal):
 1. eval r_result1 [t', i, x] \<down>= Suc v
[PROOF STEP]
using r_result1_saturating' le_Suc_ex
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [t, i, x])
t \<le> t'
eval r_result1 [t, i, x] \<down>= Suc v
eval r_result1 [?t, ?i, ?x] \<down>= Suc ?v \<Longrightarrow> eval r_result1 [?t + ?d, ?i, ?x] \<down>= Suc ?v
?k \<le> ?l \<Longrightarrow> \<exists>n. ?l = ?k + n

goal (1 subgoal):
 1. eval r_result1 [t', i, x] \<down>= Suc v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval r_result1 [t', i, x] \<down>= Suc v

goal (1 subgoal):
 1. 0 < the (eval r_result1 [t', i, x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_result1 [t', i, x] \<down>= Suc v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval r_result1 [t', i, x] \<down>= Suc v

goal (1 subgoal):
 1. 0 < the (eval r_result1 [t', i, x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < the (eval r_result1 [t', i, x])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Greatest_bounded_Suc:
  fixes P :: "nat \<Rightarrow> nat"
  shows "(if P n > 0 then Suc n
          else if \<exists>j<n. P j > 0 then Suc (GREATEST j. j < n \<and> P j > 0) else 0) =
    (if \<exists>j<Suc n. P j > 0 then Suc (GREATEST j. j < Suc n \<and> P j > 0) else 0)"
      (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
proof (cases "\<exists>j<Suc n. P j > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>j<Suc n. 0 < P j \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
 2. \<not> (\<exists>j<Suc n. 0 < P j) \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
case 1: True
[PROOF STATE]
proof (state)
this:
\<exists>j<Suc n. 0 < P j

goal (2 subgoals):
 1. \<exists>j<Suc n. 0 < P j \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
 2. \<not> (\<exists>j<Suc n. 0 < P j) \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
proof (cases "P n > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
 2. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < P n

goal (2 subgoals):
 1. 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
 2. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < P n
[PROOF STEP]
have "(GREATEST j. j < Suc n \<and> P j > 0) = n"
[PROOF STATE]
proof (prove)
using this:
0 < P n

goal (1 subgoal):
 1. (GREATEST j. j < Suc n \<and> 0 < P j) = n
[PROOF STEP]
using Greatest_equality[of "\<lambda>j. j < Suc n \<and> P j > 0"]
[PROOF STATE]
proof (prove)
using this:
0 < P n
\<lbrakk>?x < Suc n \<and> 0 < P ?x; \<And>y. y < Suc n \<and> 0 < P y \<Longrightarrow> y \<le> ?x\<rbrakk> \<Longrightarrow> (GREATEST j. j < Suc n \<and> 0 < P j) = ?x

goal (1 subgoal):
 1. (GREATEST j. j < Suc n \<and> 0 < P j) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < Suc n \<and> 0 < P j) = n

goal (2 subgoals):
 1. 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
 2. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < Suc n \<and> 0 < P j) = n

goal (2 subgoals):
 1. 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
 2. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
have "?rhs = Suc (GREATEST j. j < Suc n \<and> P j > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<exists>j<Suc n. 0 < P j

goal (1 subgoal):
 1. (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)

goal (2 subgoals):
 1. 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
 2. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < Suc n \<and> 0 < P j) = n
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)
[PROOF STEP]
have "?rhs = Suc n"
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < Suc n \<and> 0 < P j) = n
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)

goal (1 subgoal):
 1. (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc n

goal (2 subgoals):
 1. 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
 2. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc n

goal (1 subgoal):
 1. (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc n
0 < P n

goal (1 subgoal):
 1. (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)

goal (1 subgoal):
 1. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < P n

goal (1 subgoal):
 1. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 0 < P n
[PROOF STEP]
have "?lhs = Suc (GREATEST j. j < n \<and> P j > 0)"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < P n

goal (1 subgoal):
 1. (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < n \<and> 0 < P j)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < P n
\<exists>j<Suc n. 0 < P j

goal (1 subgoal):
 1. (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < n \<and> 0 < P j)
[PROOF STEP]
by (metis less_SucE)
[PROOF STATE]
proof (state)
this:
(if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < n \<and> 0 < P j)

goal (1 subgoal):
 1. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < n \<and> 0 < P j)

goal (1 subgoal):
 1. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
have "?rhs = Suc (GREATEST j. j < Suc n \<and> P j > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<exists>j<Suc n. 0 < P j

goal (1 subgoal):
 1. (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)

goal (1 subgoal):
 1. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)

goal (1 subgoal):
 1. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
have "(GREATEST j. j < n \<and> P j > 0) =
        (GREATEST j. j < Suc n \<and> P j > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST j. j < n \<and> 0 < P j) = (GREATEST j. j < Suc n \<and> 0 < P j)
[PROOF STEP]
using 1 False
[PROOF STATE]
proof (prove)
using this:
\<exists>j<Suc n. 0 < P j
\<not> 0 < P n

goal (1 subgoal):
 1. (GREATEST j. j < n \<and> 0 < P j) = (GREATEST j. j < Suc n \<and> 0 < P j)
[PROOF STEP]
by (metis less_SucI less_Suc_eq)
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < n \<and> 0 < P j) = (GREATEST j. j < Suc n \<and> 0 < P j)

goal (1 subgoal):
 1. \<not> 0 < P n \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < n \<and> 0 < P j)
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)
(GREATEST j. j < n \<and> 0 < P j) = (GREATEST j. j < Suc n \<and> 0 < P j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < n \<and> 0 < P j)
(if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0) = Suc (GREATEST j. j < Suc n \<and> 0 < P j)
(GREATEST j. j < n \<and> 0 < P j) = (GREATEST j. j < Suc n \<and> 0 < P j)

goal (1 subgoal):
 1. (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)

goal (1 subgoal):
 1. \<not> (\<exists>j<Suc n. 0 < P j) \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>j<Suc n. 0 < P j) \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>j<Suc n. 0 < P j)

goal (1 subgoal):
 1. \<not> (\<exists>j<Suc n. 0 < P j) \<Longrightarrow> (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>j<Suc n. 0 < P j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j<Suc n. 0 < P j)

goal (1 subgoal):
 1. (if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if 0 < P n then Suc n else if \<exists>j<n. 0 < P j then Suc (GREATEST j. j < n \<and> 0 < P j) else 0) = (if \<exists>j<Suc n. 0 < P j then Suc (GREATEST j. j < Suc n \<and> 0 < P j) else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_delay_aux_prim: "prim_recfn 3 r_delay_aux"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prim_recfn 3 r_delay_aux
[PROOF STEP]
unfolding r_delay_aux_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prim_recfn 3 (Pr 2 (r_constn 1 0) (Cn 4 r_ifz [Cn 4 r_result1 [Cn 4 r_length [recf.Id 4 3], recf.Id 4 2, Cn 4 r_take [Cn 4 S [recf.Id 4 0], recf.Id 4 3]], recf.Id 4 1, Cn 4 S [recf.Id 4 0]]))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma r_delay_aux_total: "total r_delay_aux"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Recursive.total r_delay_aux
[PROOF STEP]
using  prim_recfn_total[OF r_delay_aux_prim]
[PROOF STATE]
proof (prove)
using this:
Partial_Recursive.total r_delay_aux

goal (1 subgoal):
 1. Partial_Recursive.total r_delay_aux
[PROOF STEP]
.


[STATEMENT]
lemma r_delay_aux:
  assumes "n \<le> e_length x"
  shows "eval r_delay_aux [n, i, x] \<down>=
   (if \<exists>j<n. the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0
    then Suc (GREATEST j.
                 j < n \<and>
                 the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0)
    else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
define z where "z \<equiv>
    Cn 4 r_result1
      [Cn 4 r_length [Id 4 3], Id 4 2, Cn 4 r_take [Cn 4 S [Id 4 0], Id 4 3]]"
[PROOF STATE]
proof (state)
this:
z \<equiv> Cn 4 r_result1 [Cn 4 r_length [recf.Id 4 3], recf.Id 4 2, Cn 4 r_take [Cn 4 S [recf.Id 4 0], recf.Id 4 3]]

goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<equiv> Cn 4 r_result1 [Cn 4 r_length [recf.Id 4 3], recf.Id 4 2, Cn 4 r_take [Cn 4 S [recf.Id 4 0], recf.Id 4 3]]
[PROOF STEP]
have z_recfn: "recfn 4 z"
[PROOF STATE]
proof (prove)
using this:
z \<equiv> Cn 4 r_result1 [Cn 4 r_length [recf.Id 4 3], recf.Id 4 2, Cn 4 r_take [Cn 4 S [recf.Id 4 0], recf.Id 4 3]]

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

goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
have z: "eval z [j, r, i, x] = eval r_result1 [e_length x, i, e_take (Suc j) x]"
      if "j < e_length x" for j r i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval z [j, r, i, x] = eval r_result1 [e_length x, i, e_take (Suc j) x]
[PROOF STEP]
unfolding z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 4 r_result1 [Cn 4 r_length [recf.Id 4 3], recf.Id 4 2, Cn 4 r_take [Cn 4 S [recf.Id 4 0], recf.Id 4 3]]) [j, r, i, x] = eval r_result1 [e_length x, i, e_take (Suc j) x]
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
j < e_length x

goal (1 subgoal):
 1. eval (Cn 4 r_result1 [Cn 4 r_length [recf.Id 4 3], recf.Id 4 2, Cn 4 r_take [Cn 4 S [recf.Id 4 0], recf.Id 4 3]]) [j, r, i, x] = eval r_result1 [e_length x, i, e_take (Suc j) x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?j < e_length ?x \<Longrightarrow> eval z [?j, ?r, ?i, ?x] = eval r_result1 [e_length ?x, ?i, e_take (Suc ?j) ?x]

goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
define g where "g \<equiv> Cn 4 r_ifz [z, Id 4 1, Cn 4 S [Id 4 0]]"
[PROOF STATE]
proof (state)
this:
g \<equiv> Cn 4 r_ifz [z, recf.Id 4 1, Cn 4 S [recf.Id 4 0]]

goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<equiv> Cn 4 r_ifz [z, recf.Id 4 1, Cn 4 S [recf.Id 4 0]]
[PROOF STEP]
have g: "eval g [j, r, i, x] \<down>=
      (if the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0 then Suc j else r)"
      if "j < e_length x" for j r i x
[PROOF STATE]
proof (prove)
using this:
g \<equiv> Cn 4 r_ifz [z, recf.Id 4 1, Cn 4 S [recf.Id 4 0]]

goal (1 subgoal):
 1. eval g [j, r, i, x] \<down>= (if 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc j else r)
[PROOF STEP]
using that z prim_recfn_total z_recfn
[PROOF STATE]
proof (prove)
using this:
g \<equiv> Cn 4 r_ifz [z, recf.Id 4 1, Cn 4 S [recf.Id 4 0]]
j < e_length x
?j < e_length ?x \<Longrightarrow> eval z [?j, ?r, ?i, ?x] = eval r_result1 [e_length ?x, ?i, e_take (Suc ?j) ?x]
prim_recfn ?n ?f \<Longrightarrow> Partial_Recursive.total ?f
recfn 4 z

goal (1 subgoal):
 1. eval g [j, r, i, x] \<down>= (if 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc j else r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?j < e_length ?x \<Longrightarrow> eval g [?j, ?r, ?i, ?x] \<down>= (if 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc ?j) ?x]) then Suc ?j else ?r)

goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n \<le> e_length x

goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> e_length x \<Longrightarrow> eval r_delay_aux [0, i, x] \<down>= (if \<exists>j<0. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < 0 \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
 2. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 \<le> e_length x

goal (2 subgoals):
 1. 0 \<le> e_length x \<Longrightarrow> eval r_delay_aux [0, i, x] \<down>= (if \<exists>j<0. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < 0 \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
 2. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> e_length x

goal (2 subgoals):
 1. 0 \<le> e_length x \<Longrightarrow> eval r_delay_aux [0, i, x] \<down>= (if \<exists>j<0. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < 0 \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
 2. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
have "eval r_delay_aux [0, i, x] \<down>= 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_delay_aux [0, i, x] \<down>= 0
[PROOF STEP]
using eval_Pr_0 r_delay_aux_def r_delay_aux_prim r_constn
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>recfn (Suc ?n) (Pr ?n ?f ?g); ?n = length ?xs\<rbrakk> \<Longrightarrow> eval (Pr ?n ?f ?g) (0 # ?xs) = eval ?f ?xs
r_delay_aux \<equiv> Pr 2 (r_constn 1 0) (Cn 4 r_ifz [Cn 4 r_result1 [Cn 4 r_length [recf.Id 4 3], recf.Id 4 2, Cn 4 r_take [Cn 4 S [recf.Id 4 0], recf.Id 4 3]], recf.Id 4 1, Cn 4 S [recf.Id 4 0]])
prim_recfn 3 r_delay_aux
length ?xs = Suc ?n \<Longrightarrow> eval (r_constn ?n ?c) ?xs \<down>= ?c

goal (1 subgoal):
 1. eval r_delay_aux [0, i, x] \<down>= 0
[PROOF STEP]
by (simp add: r_delay_aux_def)
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [0, i, x] \<down>= 0

goal (2 subgoals):
 1. 0 \<le> e_length x \<Longrightarrow> eval r_delay_aux [0, i, x] \<down>= (if \<exists>j<0. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < 0 \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
 2. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> e_length x
eval r_delay_aux [0, i, x] \<down>= 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> e_length x
eval r_delay_aux [0, i, x] \<down>= 0

goal (1 subgoal):
 1. eval r_delay_aux [0, i, x] \<down>= (if \<exists>j<0. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < 0 \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [0, i, x] \<down>= (if \<exists>j<0. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < 0 \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
Suc n \<le> e_length x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
let ?P = "\<lambda>j. the (eval r_result1 [e_length x, i, e_take (Suc j) x])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
have "eval r_delay_aux [n, i, x] \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
Suc n \<le> e_length x

goal (1 subgoal):
 1. eval r_delay_aux [n, i, x] \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [n, i, x] \<down>

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [n, i, x] \<down>

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
have "eval r_delay_aux [Suc n, i, x] =
        eval (Pr 2 (r_constn 1 0) g) [Suc n, i, x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_delay_aux [Suc n, i, x] = eval (Pr 2 (r_constn 1 0) g) [Suc n, i, x]
[PROOF STEP]
unfolding r_delay_aux_def g_def z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 2 (r_constn 1 0) (Cn 4 r_ifz [Cn 4 r_result1 [Cn 4 r_length [recf.Id 4 3], recf.Id 4 2, Cn 4 r_take [Cn 4 S [recf.Id 4 0], recf.Id 4 3]], recf.Id 4 1, Cn 4 S [recf.Id 4 0]])) [Suc n, i, x] = eval (Pr 2 (r_constn 1 0) (Cn 4 r_ifz [Cn 4 r_result1 [Cn 4 r_length [recf.Id 4 3], recf.Id 4 2, Cn 4 r_take [Cn 4 S [recf.Id 4 0], recf.Id 4 3]], recf.Id 4 1, Cn 4 S [recf.Id 4 0]])) [Suc n, i, x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [Suc n, i, x] = eval (Pr 2 (r_constn 1 0) g) [Suc n, i, x]

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval r_delay_aux [n, i, x] \<down>
eval r_delay_aux [Suc n, i, x] = eval (Pr 2 (r_constn 1 0) g) [Suc n, i, x]
[PROOF STEP]
have "eval r_delay_aux [Suc n, i, x] =
        eval g [n, the (eval r_delay_aux [n, i, x]), i, x]"
[PROOF STATE]
proof (prove)
using this:
eval r_delay_aux [n, i, x] \<down>
eval r_delay_aux [Suc n, i, x] = eval (Pr 2 (r_constn 1 0) g) [Suc n, i, x]

goal (1 subgoal):
 1. eval r_delay_aux [Suc n, i, x] = eval g [n, the (eval r_delay_aux [n, i, x]), i, x]
[PROOF STEP]
using r_delay_aux_prim Suc eval_Pr_converg_Suc
[PROOF STATE]
proof (prove)
using this:
eval r_delay_aux [n, i, x] \<down>
eval r_delay_aux [Suc n, i, x] = eval (Pr 2 (r_constn 1 0) g) [Suc n, i, x]
prim_recfn 3 r_delay_aux
n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
Suc n \<le> e_length x
\<lbrakk>recfn (Suc ?n) (Pr ?n ?f ?g); ?n = length ?xs; eval (Pr ?n ?f ?g) (?x # ?xs) \<down>\<rbrakk> \<Longrightarrow> eval (Pr ?n ?f ?g) (Suc ?x # ?xs) = eval ?g (?x # the (eval (Pr ?n ?f ?g) (?x # ?xs)) # ?xs)

goal (1 subgoal):
 1. eval r_delay_aux [Suc n, i, x] = eval g [n, the (eval r_delay_aux [n, i, x]), i, x]
[PROOF STEP]
by (simp add: r_delay_aux_def g_def z_def numeral_3_eq_3)
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [Suc n, i, x] = eval g [n, the (eval r_delay_aux [n, i, x]), i, x]

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_delay_aux [Suc n, i, x] = eval g [n, the (eval r_delay_aux [n, i, x]), i, x]
[PROOF STEP]
have "eval r_delay_aux [Suc n, i, x] \<down>=
        (if ?P n > 0 then Suc n
         else if \<exists>j<n. ?P j > 0 then Suc (GREATEST j. j < n \<and> ?P j > 0) else 0)"
[PROOF STATE]
proof (prove)
using this:
eval r_delay_aux [Suc n, i, x] = eval g [n, the (eval r_delay_aux [n, i, x]), i, x]

goal (1 subgoal):
 1. eval r_delay_aux [Suc n, i, x] \<down>= (if 0 < the (eval r_result1 [e_length x, i, e_take (Suc n) x]) then Suc n else if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
using g Suc
[PROOF STATE]
proof (prove)
using this:
eval r_delay_aux [Suc n, i, x] = eval g [n, the (eval r_delay_aux [n, i, x]), i, x]
?j < e_length ?x \<Longrightarrow> eval g [?j, ?r, ?i, ?x] \<down>= (if 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc ?j) ?x]) then Suc ?j else ?r)
n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
Suc n \<le> e_length x

goal (1 subgoal):
 1. eval r_delay_aux [Suc n, i, x] \<down>= (if 0 < the (eval r_result1 [e_length x, i, e_take (Suc n) x]) then Suc n else if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [Suc n, i, x] \<down>= (if 0 < the (eval r_result1 [e_length x, i, e_take (Suc n) x]) then Suc n else if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_delay_aux [Suc n, i, x] \<down>= (if 0 < the (eval r_result1 [e_length x, i, e_take (Suc n) x]) then Suc n else if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
have "eval r_delay_aux [Suc n, i, x] \<down>=
        (if \<exists>j<Suc n. ?P j > 0 then Suc (GREATEST j. j < Suc n \<and> ?P j > 0) else 0)"
[PROOF STATE]
proof (prove)
using this:
eval r_delay_aux [Suc n, i, x] \<down>= (if 0 < the (eval r_result1 [e_length x, i, e_take (Suc n) x]) then Suc n else if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)

goal (1 subgoal):
 1. eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
using Greatest_bounded_Suc[where ?P="?P"]
[PROOF STATE]
proof (prove)
using this:
eval r_delay_aux [Suc n, i, x] \<down>= (if 0 < the (eval r_result1 [e_length x, i, e_take (Suc n) x]) then Suc n else if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
(if 0 < the (eval r_result1 [e_length x, i, e_take (Suc ?n) x]) then Suc ?n else if \<exists>j<?n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < ?n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0) = (if \<exists>j<Suc ?n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc ?n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)

goal (1 subgoal):
 1. eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> e_length x \<Longrightarrow> eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0); Suc n \<le> e_length x\<rbrakk> \<Longrightarrow> eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)

goal (1 subgoal):
 1. eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [Suc n, i, x] \<down>= (if \<exists>j<Suc n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < Suc n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval r_delay_aux [n, i, x] \<down>= (if \<exists>j<n. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < n \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_delay_recfn [simp]: "recfn 2 r_delay"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 r_delay
[PROOF STEP]
unfolding r_delay_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (Cn 2 r_delay_aux [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1])
[PROOF STEP]
by (simp add: r_delay_aux_prim)


[STATEMENT]
lemma delay_in_R2: "delay \<in> \<R>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay \<in> \<R>\<^sup>2
[PROOF STEP]
using r_delay totalI2 R2I delay_def r_delay_recfn
[PROOF STATE]
proof (prove)
using this:
eval r_delay [?i, ?x] \<down>= (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)
\<lbrakk>recfn 2 ?f; \<And>x y. eval ?f [x, y] \<down>\<rbrakk> \<Longrightarrow> Partial_Recursive.total ?f
\<lbrakk>recfn 2 ?r; Partial_Recursive.total ?r; \<And>x y. eval ?r [x, y] = ?f x y\<rbrakk> \<Longrightarrow> ?f \<in> \<R>\<^sup>2
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)
recfn 2 r_delay

goal (1 subgoal):
 1. delay \<in> \<R>\<^sup>2
[PROOF STEP]
by (metis (no_types, lifting) numeral_2_eq_2 option.simps(3))


[STATEMENT]
lemma delay_le_length: "the (delay i x) \<le> e_length x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (delay i x) \<le> e_length x
[PROOF STEP]
proof (cases "\<exists>j<e_length x. the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])

goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
let ?P = "\<lambda>j. j < e_length x \<and> the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])
[PROOF STEP]
have "\<exists>j. ?P j"
[PROOF STATE]
proof (prove)
using this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])

goal (1 subgoal):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])

goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])

goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
have "\<And>y. ?P y \<Longrightarrow> y \<le> e_length x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc y) x]) \<Longrightarrow> y \<le> e_length x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc ?y) x]) \<Longrightarrow> ?y \<le> e_length x

goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])
?y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc ?y) x]) \<Longrightarrow> ?y \<le> e_length x
[PROOF STEP]
have "?P (Greatest ?P)"
[PROOF STATE]
proof (prove)
using this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])
?y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc ?y) x]) \<Longrightarrow> ?y \<le> e_length x

goal (1 subgoal):
 1. (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])
[PROOF STEP]
using GreatestI_ex_nat[where ?P="?P"]
[PROOF STATE]
proof (prove)
using this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])
?y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc ?y) x]) \<Longrightarrow> ?y \<le> e_length x
\<lbrakk>\<exists>k<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc k) x]); \<And>y. y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc y) x]) \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])

goal (1 subgoal):
 1. (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])

goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])
[PROOF STEP]
have "Greatest ?P < e_length x"
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])

goal (1 subgoal):
 1. (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x

goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x

goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
have "delay i x \<down>= Suc (Greatest ?P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay i x \<down>= Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
[PROOF STEP]
using delay_def True
[PROOF STATE]
proof (prove)
using this:
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])

goal (1 subgoal):
 1. delay i x \<down>= Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
delay i x \<down>= Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))

goal (2 subgoals):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) \<Longrightarrow> the (delay i x) \<le> e_length x
 2. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x
delay i x \<down>= Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x
delay i x \<down>= Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))

goal (1 subgoal):
 1. the (delay i x) \<le> e_length x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (delay i x) \<le> e_length x

goal (1 subgoal):
 1. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))

goal (1 subgoal):
 1. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> the (delay i x) \<le> e_length x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))

goal (1 subgoal):
 1. the (delay i x) \<le> e_length x
[PROOF STEP]
using delay_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)

goal (1 subgoal):
 1. the (delay i x) \<le> e_length x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (delay i x) \<le> e_length x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma e_take_delay_init:
  assumes "f \<in> \<R>" and "the (delay i (f \<triangleright> n)) > 0"
  shows "e_take (the (delay i (f \<triangleright> n))) (f \<triangleright> n) = f \<triangleright> (the (delay i (f \<triangleright> n)) - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_take (the (delay i (f \<triangleright> n))) (f \<triangleright> n) = f \<triangleright> (the (delay i (f \<triangleright> n)) - 1)
[PROOF STEP]
using assms e_take_init[of f _ n] length_init[of f n] delay_le_length[of i "f \<triangleright> n"]
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>
0 < the (delay i (f \<triangleright> n))
\<lbrakk>f \<in> \<R>; ?k < Suc n\<rbrakk> \<Longrightarrow> e_take (Suc ?k) (f \<triangleright> n) = f \<triangleright> ?k
e_length (f \<triangleright> n) = Suc n
the (delay i (f \<triangleright> n)) \<le> e_length (f \<triangleright> n)

goal (1 subgoal):
 1. e_take (the (delay i (f \<triangleright> n))) (f \<triangleright> n) = f \<triangleright> (the (delay i (f \<triangleright> n)) - 1)
[PROOF STEP]
by (metis One_nat_def Suc_le_lessD Suc_pred)