[STATEMENT]
lemma evtEN[elim]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
    and n'::nat
  assumes "\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)"
    and "eval c t t' n (\<diamond>\<^sub>b(\<gamma>))"
  shows "\<exists>n'\<ge>n. eval c t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
assume "\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
from \<open>eval c t t' n (\<diamond>\<^sub>b(\<gamma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<diamond>\<^sub>b\<gamma>)

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
using evt_def
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<diamond>\<^sub>b\<gamma>)
\<diamond>\<^sub>b?\<gamma> \<equiv> \<lambda>t n. \<exists>n'\<ge>n. ?\<gamma> t n'

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
have "\<exists>n'\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')

goal (1 subgoal):
 1. \<exists>n'\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
using validCE_cont[where \<gamma>="(\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')"] \<open>\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
\<lbrakk>\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>); eval ?cid ?t ?t' ?n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n. \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) n'
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<exists>n'\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n'\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n'\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
obtain x where "x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)" and " \<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) x"
[PROOF STATE]
proof (prove)
using this:
\<exists>n'\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
have "the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1 < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
[PROOF STEP]
have "\<langle>c \<and> t\<rangle> < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c \<and> t\<rangle> < n
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
assume "\<not>\<langle>c \<and> t\<rangle> < n"
[PROOF STATE]
proof (state)
this:
\<not> \<langle>c \<and> t\<rangle> < n

goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
hence "\<langle>c \<and> t\<rangle> \<ge> n"
[PROOF STATE]
proof (prove)
using this:
\<not> \<langle>c \<and> t\<rangle> < n

goal (1 subgoal):
 1. n \<le> \<langle>c \<and> t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<le> \<langle>c \<and> t\<rangle>

goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<le> \<langle>c \<and> t\<rangle>

goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
from \<open>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> \<open>\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "\<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>
[PROOF STEP]
using lActive_active less_or_eq_imp_le
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<lbrakk>\<parallel>?c\<parallel>\<^bsub>?t ?i\<^esub>; \<forall>n'>?n. \<not> \<parallel>?c\<parallel>\<^bsub>?t n'\<^esub>\<rbrakk> \<Longrightarrow> \<parallel>?c\<parallel>\<^bsub>?t \<langle>?c \<and> ?t\<rangle>\<^esub>
?m < ?n \<or> ?m = ?n \<Longrightarrow> ?m \<le> ?n

goal (1 subgoal):
 1. \<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>

goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<le> \<langle>c \<and> t\<rangle>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<le> \<langle>c \<and> t\<rangle>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> \<langle>c \<and> t\<rangle>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c \<and> t\<rangle> < n

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
[PROOF STEP]
hence "the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1 < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<and> t\<rangle> < n

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n
[PROOF STEP]
using cnf2bhv_greater_llength
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<and> t\<rangle> < n
\<langle>?c \<and> ?t\<rangle> < ?n \<Longrightarrow> the_enat (llength (\<pi>\<^bsub>?c\<^esub>inf_llist ?t)) - 1 < \<^bsub>?c\<^esub>\<down>\<^bsub>?t\<^esub>?n

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
[PROOF STEP]
with \<open>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
hence "x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x))"
[PROOF STATE]
proof (prove)
using this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x

goal (1 subgoal):
 1. x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)
[PROOF STEP]
using cnf2bhv_bhv2cnf
[PROOF STATE]
proof (prove)
using this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
the_enat (llength (\<pi>\<^bsub>?c\<^esub>inf_llist ?t)) - 1 \<le> ?n \<Longrightarrow> \<^bsub>?c\<^esub>\<down>\<^bsub>?t\<^esub>(\<^bsub>?c\<^esub>\<up>\<^bsub>?t\<^esub>?n) = ?n

goal (1 subgoal):
 1. x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)
[PROOF STEP]
have "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)))"
[PROOF STATE]
proof (prove)
using this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
from \<open>\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "\<not>(\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x). \<parallel>c\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
from \<open>\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "lfinite (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
using proj_finite2
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<forall>n'. enat n' \<le> llength ?t \<longrightarrow> ?n \<le> n' \<longrightarrow> \<not> \<parallel>?c\<parallel>\<^bsub>lnth ?t n'\<^esub> \<Longrightarrow> lfinite (\<pi>\<^bsub>?c\<^esub>?t)

goal (1 subgoal):
 1. lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
obtain z where "\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>"
[PROOF STATE]
proof (prove)
using this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. (\<And>z. \<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using proj_finite_bound
[PROOF STATE]
proof (prove)
using this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
lfinite (\<pi>\<^bsub>?c\<^esub>inf_llist ?t) \<Longrightarrow> \<exists>n. \<forall>n'>n. \<not> \<parallel>?c\<parallel>\<^bsub>?t n'\<^esub>

goal (1 subgoal):
 1. (\<And>z. \<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
from \<open>the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1 < x\<close>
[PROOF STATE]
proof (chain)
picking this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
[PROOF STEP]
have "\<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)"
[PROOF STATE]
proof (prove)
using this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x

goal (1 subgoal):
 1. \<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
using bhv2cnf_greater_lActive
[PROOF STATE]
proof (prove)
using this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
the_enat (llength (\<pi>\<^bsub>?c\<^esub>inf_llist ?t)) - 1 < ?n \<Longrightarrow> \<langle>?c \<and> ?t\<rangle> < \<^bsub>?c\<^esub>\<up>\<^bsub>?t\<^esub>?n

goal (1 subgoal):
 1. \<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
using lActive_greater_active_all
[PROOF STATE]
proof (prove)
using this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<forall>n''>?n'. \<not> \<parallel>?c\<parallel>\<^bsub>?t n''\<^esub> \<Longrightarrow> \<not> (\<exists>n>\<langle>?c \<and> ?t\<rangle>. \<parallel>?c\<parallel>\<^bsub>?t n\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
\<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
\<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
[PROOF STEP]
using validCI_cont[of c t "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)" \<gamma>] \<open>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
\<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<lbrakk>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>); \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist ?t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))\<rbrakk> \<Longrightarrow> eval c t ?t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
from \<open>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> \<open>\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "\<langle>c \<and> t\<rangle> \<le> n"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<langle>c \<and> t\<rangle> \<le> n
[PROOF STEP]
using lActive_less[of c t _ n]
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<lbrakk>\<parallel>c\<parallel>\<^bsub>t ?i\<^esub>; \<forall>n'>n. \<not> \<parallel>c\<parallel>\<^bsub>t n'\<^esub>\<rbrakk> \<Longrightarrow> \<langle>c \<and> t\<rangle> \<le> n

goal (1 subgoal):
 1. \<langle>c \<and> t\<rangle> \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>c \<and> t\<rangle> \<le> n

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
with \<open>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<langle>c \<and> t\<rangle> \<le> n
[PROOF STEP]
have "n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)"
[PROOF STATE]
proof (prove)
using this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<langle>c \<and> t\<rangle> \<le> n

goal (1 subgoal):
 1. n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
using p2c_mono_c2p
[PROOF STATE]
proof (prove)
using this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<langle>c \<and> t\<rangle> \<le> n
\<lbrakk>\<langle>?c \<and> ?t\<rangle> \<le> ?n; \<^bsub>?c\<^esub>\<down>\<^bsub>?t\<^esub>?n \<le> ?n'\<rbrakk> \<Longrightarrow> ?n \<le> \<^bsub>?c\<^esub>\<up>\<^bsub>?t\<^esub>?n'

goal (1 subgoal):
 1. n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n'\<ge>n. eval c t t' n' \<gamma>

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
assume "\<not>(\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
from \<open>eval c t t' n (\<diamond>\<^sub>b(\<gamma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<diamond>\<^sub>b\<gamma>)

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
using evt_def
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<diamond>\<^sub>b\<gamma>)
\<diamond>\<^sub>b?\<gamma> \<equiv> \<lambda>t n. \<exists>n'\<ge>n. ?\<gamma> t n'

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
obtain n' where "n'\<ge>n" and "\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>n \<le> n'; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<not>(\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close> validCE_not_act[where \<gamma>="\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n'"]
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>?n. \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) n'

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>n \<le> n'; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<le> n'
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
with \<open>\<not>(\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
n \<le> n'
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
n \<le> n'
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
using validCI_not_act[of c t \<gamma> t' n']
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
n \<le> n'
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
\<lbrakk>\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'\<rbrakk> \<Longrightarrow> eval c t t' n' \<gamma>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval c t t' n' \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n'\<ge>n. eval c t t' n' \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma globIA[intro]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
  assumes "\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and "\<And>n'. \<lbrakk>\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<rbrakk> \<Longrightarrow> \<exists>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n''\<le>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval c t t' n'' \<gamma>"
    and "\<And>n'. \<lbrakk>\<not>(\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>); n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<rbrakk> \<Longrightarrow> eval c t t' n' \<gamma>"
  shows "eval c t t' n (\<box>\<^sub>b(\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
have "\<forall>n'\<ge>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n'\<ge>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> n' \<longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
fix x::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> n' \<longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
show
      "x\<ge>the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>) \<longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x \<longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
assume "x\<ge>the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
show "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
assume "(x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))"
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
hence "lfinite (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (1 subgoal):
 1. lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
using llength_geq_enat_lfiniteD[of "\<pi>\<^bsub>c\<^esub>(inf_llist t)" x]
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
obtain z where "\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>"
[PROOF STATE]
proof (prove)
using this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. (\<And>z. \<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using proj_finite_bound
[PROOF STATE]
proof (prove)
using this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
lfinite (\<pi>\<^bsub>?c\<^esub>inf_llist ?t) \<Longrightarrow> \<exists>n. \<forall>n'>n. \<not> \<parallel>?c\<parallel>\<^bsub>?t n'\<^esub>

goal (1 subgoal):
 1. (\<And>z. \<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
have "\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
by (simp add: \<open>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> nxtActI)
[PROOF STATE]
proof (state)
this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
have "\<langle>c \<and> t\<rangle>\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<langle>c \<and> t\<rangle>
[PROOF STEP]
using lActive_greatest[of c t "\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>"]
[PROOF STATE]
proof (prove)
using this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
\<lbrakk>\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>; \<forall>n'>?n. \<not> \<parallel>c\<parallel>\<^bsub>t n'\<^esub>\<rbrakk> \<Longrightarrow> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<langle>c \<and> t\<rangle>

goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<langle>c \<and> t\<rangle>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<langle>c \<and> t\<rangle>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<langle>c \<and> t\<rangle>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
have "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> \<langle>c \<and> t\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c \<and> t\<rangle> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c \<and> t\<rangle> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<langle>c \<and> t\<rangle>
\<langle>c \<and> t\<rangle> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
have "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<langle>c \<and> t\<rangle>
\<langle>c \<and> t\<rangle> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
have "\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x). \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
from \<open>lfinite (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<close> \<open>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))) = Suc (\<langle>c \<and> t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) = Suc \<langle>c \<and> t\<rangle>
[PROOF STEP]
using bhv2cnf_lActive
[PROOF STATE]
proof (prove)
using this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<lbrakk>\<exists>i. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub>; lfinite (\<pi>\<^bsub>?c\<^esub>inf_llist ?t)\<rbrakk> \<Longrightarrow> \<^bsub>?c\<^esub>\<up>\<^bsub>?t\<^esub>the_enat (llength (\<pi>\<^bsub>?c\<^esub>inf_llist ?t)) = Suc \<langle>?c \<and> ?t\<rangle>

goal (1 subgoal):
 1. \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) = Suc \<langle>c \<and> t\<rangle>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) = Suc \<langle>c \<and> t\<rangle>

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) = Suc \<langle>c \<and> t\<rangle>

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
from \<open>(x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))\<close>
[PROOF STATE]
proof (chain)
picking this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
[PROOF STEP]
have "x \<ge> the_enat(llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))"
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> x
[PROOF STEP]
using the_enat_mono
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
\<lbrakk>?m \<noteq> \<infinity>; ?n \<le> ?m\<rbrakk> \<Longrightarrow> the_enat ?n \<le> the_enat ?m

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> x

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
hence "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))))"
[PROOF STATE]
proof (prove)
using this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> x

goal (1 subgoal):
 1. \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
using bhv2cnf_mono[of "the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))" x]
[PROOF STATE]
proof (prove)
using this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> x
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> x \<Longrightarrow> \<^bsub>?c\<^esub>\<up>\<^bsub>?t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> \<^bsub>?c\<^esub>\<up>\<^bsub>?t\<^esub>x

goal (1 subgoal):
 1. \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) = Suc \<langle>c \<and> t\<rangle>
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
have "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> Suc (\<langle>c \<and> t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) = Suc \<langle>c \<and> t\<rangle>
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. Suc \<langle>c \<and> t\<rangle> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc \<langle>c \<and> t\<rangle> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
hence "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) > \<langle>c \<and> t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
Suc \<langle>c \<and> t\<rangle> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
with \<open>\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
using lActive_greater_active_all
[PROOF STATE]
proof (prove)
using this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<langle>c \<and> t\<rangle> < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<forall>n''>?n'. \<not> \<parallel>?c\<parallel>\<^bsub>?t n''\<^esub> \<Longrightarrow> \<not> (\<exists>n>\<langle>?c \<and> ?t\<rangle>. \<parallel>?c\<parallel>\<^bsub>?t n\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
have "eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)) \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)

goal (1 subgoal):
 1. eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
\<lbrakk>\<not> (\<exists>i\<ge>?n'2. \<parallel>c\<parallel>\<^bsub>t i\<^esub>); \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> ?n'2\<rbrakk> \<Longrightarrow> eval c t t' ?n'2 \<gamma>

goal (1 subgoal):
 1. eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
hence "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
[PROOF STEP]
using validCE_cont[of c t "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)" t' \<gamma>] \<open>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> \<open>\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x). \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)\<close>
[PROOF STATE]
proof (prove)
using this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
\<lbrakk>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>); eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>\<rbrakk> \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
from \<open>(x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))\<close>
[PROOF STATE]
proof (chain)
picking this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
[PROOF STEP]
have "(enat x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))"
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (1 subgoal):
 1. llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
with \<open>lfinite (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<close>
[PROOF STATE]
proof (chain)
picking this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
[PROOF STEP]
have "llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<noteq>\<infinity>"
[PROOF STATE]
proof (prove)
using this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (1 subgoal):
 1. llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>
[PROOF STEP]
using llength_eq_infty_conv_lfinite
[PROOF STATE]
proof (prove)
using this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
(llength ?xs = \<infinity>) = (\<not> lfinite ?xs)

goal (1 subgoal):
 1. llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
with \<open>(x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))\<close>
[PROOF STATE]
proof (chain)
picking this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>
[PROOF STEP]
have "the_enat(llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1 \<le> x"
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
using cnf2bhv_bhv2cnf[of c t x]
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x \<Longrightarrow> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) = x

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
assume "\<not>(x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))"
[PROOF STATE]
proof (state)
this:
\<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
hence "x<llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (prove)
using this:
\<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (1 subgoal):
 1. enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
obtain n'::nat where "x=\<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. (\<And>n'. enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nAct_exists
[PROOF STATE]
proof (prove)
using this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
enat ?x < llength (\<pi>\<^bsub>?c\<^esub>?t) \<Longrightarrow> \<exists>n'. enat ?x = \<langle>?c #\<^bsub>enat n'\<^esub>?t\<rangle>

goal (1 subgoal):
 1. (\<And>n'. enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
from \<open>enat x < llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<close> \<open>enat x = \<langle>c #\<^bsub>enat n'\<^esub> inf_llist t\<rangle>\<close>
[PROOF STATE]
proof (chain)
picking this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (prove)
using this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
using nAct_less_llength_active
[PROOF STATE]
proof (prove)
using this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>
\<lbrakk>enat ?x < llength (\<pi>\<^bsub>?c\<^esub>?t); enat ?x = \<langle>?c #\<^bsub>enat ?n'\<^esub>?t\<rangle>\<rbrakk> \<Longrightarrow> \<exists>i\<ge>?n'. enat i < llength ?t \<and> \<parallel>?c\<parallel>\<^bsub>lnth ?t i\<^esub>

goal (1 subgoal):
 1. \<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
obtain i where "i\<ge>n'" and "\<parallel>c\<parallel>\<^bsub>t i\<^esub>" and "\<not> (\<exists>k\<ge>n'. k < i \<and> \<parallel>c\<parallel>\<^bsub>t k\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>n' \<le> i; \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nact_exists
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<Longrightarrow> \<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<and> \<not> (\<exists>k\<ge>?n. latestAct_cond ?c ?t i k)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>n' \<le> i; \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n' \<le> i
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n' \<le> i
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
have "enat i - 1 < llength (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat i - 1 < llength (inf_llist t)
[PROOF STEP]
by (simp add: one_enat_def)
[PROOF STATE]
proof (state)
this:
enat i - 1 < llength (inf_llist t)

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>
n' \<le> i
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)
enat i - 1 < llength (inf_llist t)
[PROOF STEP]
have "x=\<langle>c #\<^bsub>i\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>
n' \<le> i
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)
enat i - 1 < llength (inf_llist t)

goal (1 subgoal):
 1. enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using one_enat_def nAct_not_active_same
[PROOF STATE]
proof (prove)
using this:
enat x = \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>
n' \<le> i
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)
enat i - 1 < llength (inf_llist t)
1 = enat 1
\<lbrakk>enat ?n \<le> ?n'; ?n' - 1 < llength ?t; \<nexists>k. enat ?n \<le> enat k \<and> enat k < ?n' \<and> \<parallel>?c\<parallel>\<^bsub>lnth ?t k\<^esub>\<rbrakk> \<Longrightarrow> \<langle>?c #\<^bsub>?n'\<^esub>?t\<rangle> = \<langle>?c #\<^bsub>enat ?n\<^esub>?t\<rangle>

goal (1 subgoal):
 1. enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
have "\<langle>c #\<^bsub>i\<^esub> inf_llist t\<rangle>\<noteq>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>
[PROOF STEP]
have "x=the_enat(\<langle>c #\<^bsub>i\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>

goal (1 subgoal):
 1. x = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
from \<open>x\<ge>the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)\<close> \<open>x=the_enat(\<langle>c #\<^bsub>i\<^esub> inf_llist t\<rangle>)\<close>
[PROOF STATE]
proof (chain)
picking this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x
x = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "the_enat (\<langle>c #\<^bsub>i\<^esub> inf_llist t\<rangle>)\<ge>the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x
x = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
with \<open>\<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "i\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
[PROOF STEP]
using active_geq_nxtAct
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
\<lbrakk>\<parallel>?c\<parallel>\<^bsub>?t ?i\<^esub>; the_enat \<langle>?c #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle> \<le> the_enat \<langle>?c #\<^bsub>enat ?i\<^esub>inf_llist ?t\<rangle>\<rbrakk> \<Longrightarrow> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<le> ?i

goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
from \<open>x=\<langle>c #\<^bsub>i\<^esub> inf_llist t\<rangle>\<close> \<open>x < llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<close>
[PROOF STATE]
proof (chain)
picking this:
enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
have "\<exists>i'. i \<le> enat i' \<and> \<parallel>c\<parallel>\<^bsub>t i'\<^esub>"
[PROOF STATE]
proof (prove)
using this:
enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. \<exists>i'. enat i \<le> enat i' \<and> \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
using nAct_less_llength_active[of x c "inf_llist t" i]
[PROOF STATE]
proof (prove)
using this:
enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
\<lbrakk>enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t); enat x = \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>\<rbrakk> \<Longrightarrow> \<exists>ia\<ge>i. enat ia < llength (inf_llist t) \<and> \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) ia\<^esub>

goal (1 subgoal):
 1. \<exists>i'. enat i \<le> enat i' \<and> \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>i'. enat i \<le> enat i' \<and> \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
hence "\<exists>i'\<ge>i. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i'. enat i \<le> enat i' \<and> \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

goal (1 subgoal):
 1. \<exists>i'\<ge>i. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>i'\<ge>i. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
\<exists>i'\<ge>i. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
obtain n'' where "eval c t t' n'' \<gamma>" and "n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub>" and "n''\<le>\<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
\<exists>i'\<ge>i. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

goal (1 subgoal):
 1. (\<And>n''. \<lbrakk>eval c t t' n'' \<gamma>; \<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''; n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
\<exists>i'\<ge>i. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
\<lbrakk>\<exists>i\<ge>?n'2. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> ?n'2\<rbrakk> \<Longrightarrow> \<exists>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>?n'2\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>?n'2\<^esub> \<and> eval c t t' n'' \<gamma>

goal (1 subgoal):
 1. (\<And>n''. \<lbrakk>eval c t t' n'' \<gamma>; \<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''; n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval c t t' n'' \<gamma>
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval c t t' n'' \<gamma>
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
have "\<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
using \<open>\<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> \<open>n''\<le>\<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<close> less_or_eq_imp_le nxtAct_active
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>
?m < ?n \<or> ?m = ?n \<Longrightarrow> ?m \<le> ?n
\<parallel>?c\<parallel>\<^bsub>?t ?i\<^esub> \<Longrightarrow> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?i\<^esub> = ?i

goal (1 subgoal):
 1. \<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n'' \<gamma>
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>
\<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
have "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (the_enat (\<langle>c #\<^bsub>n''\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n'' \<gamma>
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>
\<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using validCE_act[of n'' c t t' \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval c t t' n'' \<gamma>
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>
\<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
\<lbrakk>\<exists>i\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; eval c t t' n'' \<gamma>\<rbrakk> \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
from \<open>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub>\<close> and \<open>n''\<le>\<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>
[PROOF STEP]
have "the_enat (\<langle>c #\<^bsub>n''\<^esub> inf_llist t\<rangle>)=the_enat (\<langle>c #\<^bsub>i\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using nAct_same
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>
\<lbrakk>\<langle>?c \<Leftarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<le> ?n'; ?n' \<le> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>\<rbrakk> \<Longrightarrow> the_enat \<langle>?c #\<^bsub>enat ?n'\<^esub>inf_llist ?t\<rangle> = the_enat \<langle>?c #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
hence "the_enat (\<langle>c #\<^bsub>n''\<^esub> inf_llist t\<rangle>) = x"
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> = x
[PROOF STEP]
by (simp add: \<open>x = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>\<close>)
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> = x

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)
the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> = x
[PROOF STEP]
have "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (the_enat x)"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)
the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> = x

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat (enat x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat (enat x))

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat (enat x))

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x \<longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n'\<ge>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'

goal (1 subgoal):
 1. eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
with \<open>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>n'\<ge>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>n'\<ge>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
using validCI_act[of n c t "\<lambda> t n. \<forall>n'\<ge>n. \<gamma> t n'" t']
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>n'\<ge>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
\<lbrakk>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<forall>n'\<ge>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'\<rbrakk> \<Longrightarrow> eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')

goal (1 subgoal):
 1. eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')

goal (1 subgoal):
 1. eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
using glob_def
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')
\<box>\<^sub>b?\<gamma> \<equiv> \<lambda>t n. \<forall>n'\<ge>n. ?\<gamma> t n'

goal (1 subgoal):
 1. eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval c t t' n (\<box>\<^sub>b\<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed