[STATEMENT]
lemma evtIA[intro]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
    and n'::nat
  assumes "\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and "n'\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>"
    and "\<lbrakk>\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^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 "\<lbrakk>\<not>(\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<rbrakk> \<Longrightarrow> eval c t t' n' \<gamma>"
  shows "eval c t t' n (\<diamond>\<^sub>b(\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
assume "\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<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>
\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
obtain n'' where "n'' \<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>" and "n''\<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>" and "eval c t t' n'' \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<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>
\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
hence "\<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>
eval c t t' n'' \<gamma>

goal (1 subgoal):
 1. \<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
using \<open>\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>\<close> nxtActI
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>
eval c t t' n'' \<gamma>
\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<Longrightarrow> ?n \<le> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<and> \<parallel>?c\<parallel>\<^bsub>?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>\<^esub> \<and> \<not> (\<exists>k\<ge>?n. latestAct_cond ?c ?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> k)

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
with \<open>eval c t t' n'' \<gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n'' \<gamma>
\<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>
\<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
[PROOF STATE]
proof (prove)
using this:
eval c t t' n'' \<gamma>
\<exists>i'\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n ?\<gamma>\<rbrakk> \<Longrightarrow> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^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 (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[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 (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
have "the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>) \<le> the_enat (\<langle>c #\<^bsub>n''\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
from \<open>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>\<le>n''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n''
[PROOF STEP]
have "\<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>n''\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n''

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using nAct_mono_lNact
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n''
\<langle>?c \<Leftarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<le> ?n' \<Longrightarrow> \<langle>?c #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle> \<le> \<langle>?c #\<^bsub>enat ?n'\<^esub>inf_llist ?t\<rangle>

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<le> \<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> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<le> \<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> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
from \<open>n'\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
[PROOF STEP]
have "\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using nAct_mono_lNact
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
\<langle>?c \<Leftarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<le> ?n' \<Longrightarrow> \<langle>?c #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle> \<le> \<langle>?c #\<^bsub>enat ?n'\<^esub>inf_llist ?t\<rangle>

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<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> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<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> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "\<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle> \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^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 n''\<^esub>inf_llist t\<rangle>

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[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]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i'\<ge>n. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
from \<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>
[PROOF STEP]
obtain i' where "i'\<ge>n'" and "\<parallel>c\<parallel>\<^bsub>t i'\<^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>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n' \<le> i'
\<parallel>c\<parallel>\<^bsub>t i'\<^esub>

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

goal (1 subgoal):
 1. n \<le> i'
[PROOF STEP]
using lNactGe le_trans
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
n' \<le> i'
\<parallel>c\<parallel>\<^bsub>t i'\<^esub>
\<lbrakk>\<langle>?c \<Leftarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<le> ?n'; \<parallel>?c\<parallel>\<^bsub>?t ?n'\<^esub>\<rbrakk> \<Longrightarrow> ?n \<le> ?n'
\<lbrakk>?i \<le> ?j; ?j \<le> ?k\<rbrakk> \<Longrightarrow> ?i \<le> ?k

goal (1 subgoal):
 1. n \<le> i'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<le> i'

goal (1 subgoal):
 1. \<exists>i'\<ge>n. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[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>
n \<le> i'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t i'\<^esub>
n \<le> i'

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[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> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<exists>i'\<ge>n. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')"
[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> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<exists>i'\<ge>n. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
using validCI_act[where \<gamma>="(\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')"]
[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> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<exists>i'\<ge>n. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<exists>n'\<ge>the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>. \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) n'\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<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 blast
[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> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')

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

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>) \<Longrightarrow> eval c t t' n (\<diamond>\<^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>
\<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
have "n' \<ge> \<langle>c \<and> t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<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
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<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 (1 subgoal):
 1. \<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>) \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
hence "\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n') \<ge> the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<and> t\<rangle> \<le> n'

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

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> \<^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 \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>) \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>) \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
have "the_enat(llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1 \<ge> the_enat(\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
from \<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>
[PROOF STEP]
have "llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)) \<ge> eSuc (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
using nAct_llength_proj
[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> eSuc \<langle>?c #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle> \<le> llength (\<pi>\<^bsub>?c\<^esub>inf_llist ?t)

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

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[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[of "inf_llist t"]
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
\<forall>n'. enat n' \<le> llength (inf_llist t) \<longrightarrow> ?n \<le> n' \<longrightarrow> \<not> \<parallel>?c\<parallel>\<^bsub>lnth (inf_llist t) n'\<^esub> \<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 (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
hence "llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<noteq>\<infinity>"
[PROOF STATE]
proof (prove)
using this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)

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 ?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 (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>
[PROOF STEP]
have "the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) \<ge> the_enat(eSuc (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>

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

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t))

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
have "\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>\<noteq>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t))
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>
[PROOF STEP]
have "the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) \<ge> Suc (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t))
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>

goal (1 subgoal):
 1. Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t))
[PROOF STEP]
using the_enat_eSuc
[PROOF STATE]
proof (prove)
using this:
the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t))
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>
?n \<noteq> \<infinity> \<Longrightarrow> the_enat (eSuc ?n) = Suc (the_enat ?n)

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

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t))

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>) \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>) \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<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 "eval c t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)

goal (1 subgoal):
 1. eval c t t' n' \<gamma>
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
\<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n' \<gamma>

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

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>) \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
with \<open>\<exists>i\<ge>n. \<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\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
eval c t t' n' \<gamma>
[PROOF STEP]
have "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n'))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
eval c t t' n' \<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>n')
[PROOF STEP]
using validCE_cont
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
eval c t t' n' \<gamma>
\<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 ?\<gamma>\<rbrakk> \<Longrightarrow> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n)

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>n')
[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>n')

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

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
using \<open>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> validCI_act[where \<gamma>="(\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')"]
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n')
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<exists>n'\<ge>the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>. \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) n'\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<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 blast
[PROOF STATE]
proof (state)
this:
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>) \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma evtIN[intro]:
  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 "n'\<ge>n"
    and "eval c t t' n' \<gamma>"
  shows "eval c t t' n (\<diamond>\<^sub>b(\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<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> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
from assms(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
n \<le> n'
[PROOF STEP]
have "\<not>(\<exists>i'\<ge>n'. \<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>)
n \<le> n'

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
ultimately
[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 "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(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. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n')
[PROOF STEP]
using validCE_cont[of c t n' t' \<gamma>] \<open>eval c t t' n' \<gamma>\<close>
[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>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<not> (\<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')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n')
eval c t t' n' \<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>n')
[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>n')

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<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>n')

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

goal (1 subgoal):
 1. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[PROOF STEP]
using cnf2bhv_mono
[PROOF STATE]
proof (prove)
using this:
n \<le> n'
?n \<le> ?n' \<Longrightarrow> \<^bsub>?c\<^esub>\<down>\<^bsub>?t\<^esub>?n \<le> \<^bsub>?c\<^esub>\<down>\<^bsub>?t\<^esub>?n'

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<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>n')
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')"
[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>n')
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
using validCI_cont[where \<gamma>="(\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')"] \<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 (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n')
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
\<lbrakk>\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>); \<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'\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
\<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. eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
by blast
[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> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')

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

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval c t t' n (\<diamond>\<^sub>b\<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> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
n \<le> n'
eval c t t' n' \<gamma>
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
n \<le> n'
eval c t t' n' \<gamma>
\<nexists>i. \<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')) n'
[PROOF STEP]
using validCE_not_act
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
n \<le> n'
eval c t t' n' \<gamma>
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n ?\<gamma>\<rbrakk> \<Longrightarrow> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<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> eval c t t' n (\<diamond>\<^sub>b\<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>
\<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. \<exists>n'\<ge>n. \<gamma> t n')"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<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. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
using validCI_not_act[where \<gamma>="\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n'"] \<open>n'\<ge>n\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<exists>n'\<ge>?n. \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) n'\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
n \<le> n'

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
by blast
[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> eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')

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

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

goal:
No subgoals!
[PROOF STEP]
qed