[STATEMENT]
lemma nxtIA[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 "\<lbrakk>\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<rbrakk> \<Longrightarrow> \<exists>n' \<ge> n. (\<exists>!i. n\<le>i \<and> i<n' \<and> \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>"
    and "\<lbrakk>\<not>(\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<rbrakk> \<Longrightarrow> eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>"
  shows "eval c t t' n (\<circle>\<^sub>b(\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
assume "\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>n \<le> n'; \<exists>!i. n \<le> i \<and> latestAct_cond c t n' i; eval c t t' n' \<gamma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<le> n'
\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i
eval c t t' n' \<gamma>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<le> n'
\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i
eval c t t' n' \<gamma>

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

goal (1 subgoal):
 1. \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> &&& n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
[PROOF STEP]
using nxtActI
[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> ?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. \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> &&& n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>

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

goal (1 subgoal):
 1. \<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
by (metis \<open>\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> dual_order.strict_trans2 leI nat_less_le)
[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 (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^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>enat 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 (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^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 (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
have "the_enat(\<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle>) = Suc (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> = Suc (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> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
from \<open>\<exists>!i. n\<le>i \<and> i<n' \<and> \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i
[PROOF STEP]
obtain i where "n\<le>i" and "i<n'" and "\<parallel>c\<parallel>\<^bsub>t i\<^esub>"
      and "\<forall>i'. n\<le>i' \<and> i'<n' \<and> \<parallel>c\<parallel>\<^bsub>t i'\<^esub> \<longrightarrow> i'=i"
[PROOF STATE]
proof (prove)
using this:
\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i

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

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<le> i
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i

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

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<le> i
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i
enat (n' - 1) < llength (inf_llist t)
[PROOF STEP]
have "the_enat(\<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle>) = the_enat(eSuc (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
n \<le> i
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i
enat (n' - 1) < llength (inf_llist t)

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using nAct_active_suc[of "inf_llist t" n' n i c]
[PROOF STATE]
proof (prove)
using this:
n \<le> i
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i
enat (n' - 1) < llength (inf_llist t)
\<lbrakk>\<not> lfinite (inf_llist t) \<or> enat n' - 1 < llength (inf_llist t); n \<le> i; enat i < enat n'; \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) i\<^esub>; \<forall>i'. n \<le> i' \<and> enat i' < enat n' \<and> enat i' < llength (inf_llist t) \<and> \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) i'\<^esub> \<longrightarrow> i' = i\<rbrakk> \<Longrightarrow> \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = eSuc \<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 (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
by (simp add: \<open>n \<le> i\<close>)
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<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> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<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> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[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. the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
\<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
\<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^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> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
have "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (Suc (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)))"
[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> = Suc (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')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. (\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i) \<and> eval c t t' n' \<gamma>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. (\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i) \<and> eval c t t' n' \<gamma>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))

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

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

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

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
\<not> (\<exists>i\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<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>(Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
\<not> (\<exists>i\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
using assms(1) validCE_cont[of c t "Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>" t' \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
\<not> (\<exists>i\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>); eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>\<rbrakk> \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
from assms(1) \<open>\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<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>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
[PROOF STEP]
have "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (Suc (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)))"
[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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>

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

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^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')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>" and "\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<ge> n"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> &&& n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
[PROOF STEP]
using nxtActI
[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> ?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. \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> &&& n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^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')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
with \<open>\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>\<close> \<open>\<not> (\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
\<not> (\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
\<not> (\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))

goal (1 subgoal):
 1. eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
using nxt_def
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
\<not> (\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))
\<circle>\<^sub>b?\<gamma> \<equiv> \<lambda>t n. ?\<gamma> t (Suc n)

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^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>Suc 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>(Suc n))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>Suc 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>Suc n)
[PROOF STEP]
using validCE_cont \<open>eval c t t' (Suc n) \<gamma>\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>Suc n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<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)
eval c t t' (Suc 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>Suc 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>Suc n)

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
with \<open>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<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>Suc n)
[PROOF STEP]
have "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (Suc (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<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>Suc n)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))
[PROOF STEP]
using \<open>\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close> lActive_less
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<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>Suc n)
\<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. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))

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

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval c t t' n (\<circle>\<^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 (\<circle>\<^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 (\<circle>\<^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>)
eval c t t' (Suc 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')) (Suc n)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
eval c t t' (Suc 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')) (Suc 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>)
eval c t t' (Suc 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')) (Suc n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc n)

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval c t t' n (\<circle>\<^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')) (Suc n)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<gamma> t (Suc 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')) (Suc n)

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))
[PROOF STEP]
using validCI_not_act[where \<gamma>="(\<lambda>t n. \<gamma> t (Suc 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')) (Suc n)
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (Suc ?n)\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t (Suc n))

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nxtEA1[elim]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
  assumes "\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and "eval c t t' n (\<circle>\<^sub>b(\<gamma>))"
    and "n'\<ge>n"
    and "\<exists>!i. i\<ge>n \<and> i<n' \<and> \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
  shows "eval c t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n' \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval c t t' n' \<gamma>
[PROOF STEP]
from \<open>eval c t t' n (\<circle>\<^sub>b(\<gamma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<circle>\<^sub>b\<gamma>)

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

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

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

goal (1 subgoal):
 1. eval c t t' n' \<gamma>
[PROOF STEP]
from assms(4)
[PROOF STATE]
proof (chain)
picking this:
\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i
[PROOF STEP]
obtain i where "i\<ge>n" and "i<n'" and "\<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and "\<forall>i'. n\<le>i' \<and> i'<n' \<and> \<parallel>c\<parallel>\<^bsub>t i'\<^esub> \<longrightarrow> i'=i"
[PROOF STATE]
proof (prove)
using this:
\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i

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

goal (1 subgoal):
 1. eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))
n \<le> i
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))
n \<le> i
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
[PROOF STEP]
using validCE_act[of n c t t' "\<lambda>t n. \<gamma> t (Suc n)"]
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))
n \<le> i
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i
\<lbrakk>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))\<rbrakk> \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (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')) (Suc (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')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))

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

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

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
with \<open>i<n'\<close> and \<open>\<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> and \<open>\<forall>i'. n\<le>i' \<and> i'<n' \<and> \<parallel>c\<parallel>\<^bsub>t i'\<^esub> \<longrightarrow> i'=i\<close>
[PROOF STATE]
proof (chain)
picking this:
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i
enat (n' - 1) < llength (inf_llist t)
[PROOF STEP]
have "the_enat(\<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle>) = the_enat(eSuc (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i
enat (n' - 1) < llength (inf_llist t)

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using nAct_active_suc[of "inf_llist t" n' n i c]
[PROOF STATE]
proof (prove)
using this:
i < n'
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i
enat (n' - 1) < llength (inf_llist t)
\<lbrakk>\<not> lfinite (inf_llist t) \<or> enat n' - 1 < llength (inf_llist t); n \<le> i; enat i < enat n'; \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) i\<^esub>; \<forall>i'. n \<le> i' \<and> enat i' < enat n' \<and> enat i' < llength (inf_llist t) \<and> \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) i'\<^esub> \<longrightarrow> i' = i\<rbrakk> \<Longrightarrow> \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = eSuc \<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 (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
by (simp add: \<open>n \<le> i\<close>)
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<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> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<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> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[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. the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
\<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = the_enat (eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
\<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> \<noteq> \<infinity>

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

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

goal (1 subgoal):
 1. 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')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[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:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle> = Suc (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 simp
[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. 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')) (the_enat \<langle>c #\<^bsub>enat n'\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. eval c t t' n' \<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 assms(4)
[PROOF STATE]
proof (chain)
picking this:
\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i
[PROOF STEP]
have "\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<ge>n" and "\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i

goal (1 subgoal):
 1. n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> &&& \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
using nxtActI
[PROOF STATE]
proof (prove)
using this:
\<exists>!i. n \<le> i \<and> latestAct_cond c t n' i
\<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. n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> &&& \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

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

goal (1 subgoal):
 1. \<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>i'. n \<le> i' \<and> latestAct_cond c t n' i' \<longrightarrow> i' = i
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
[PROOF STEP]
by (metis leI le_trans less_le)
[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 (1 subgoal):
 1. 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')) (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]
show ?thesis
[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>)
\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>

goal (1 subgoal):
 1. eval c t t' n' \<gamma>
[PROOF STEP]
using validCI_act
[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>)
\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; ?\<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>)\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n ?\<gamma>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nxtEA2[elim]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
    and "i"
  assumes "\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>" and "\<not>(\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)"
    and "eval c t t' n (\<circle>\<^sub>b(\<gamma>))"
  shows "eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
[PROOF STEP]
from \<open>eval c t t' n (\<circle>\<^sub>b(\<gamma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<circle>\<^sub>b\<gamma>)

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

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

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

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

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

goal (1 subgoal):
 1. eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
[PROOF STEP]
from assms(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)=\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

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

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

goal (1 subgoal):
 1. eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^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>(Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>))"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
Suc (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
[PROOF STEP]
from assms(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "\<not>(\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[PROOF STEP]
using nxtActive_no_active
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<exists>!i. ?n \<le> i \<and> \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<Longrightarrow> \<not> (\<exists>i'\<ge>Suc \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>. \<parallel>?c\<parallel>\<^bsub>?t i'\<^esub>)

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

goal (1 subgoal):
 1. eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<not> (\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
[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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<not> (\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)

goal (1 subgoal):
 1. eval c t t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) \<gamma>
[PROOF STEP]
using validCI_cont[where n="Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>"] assms(1)
[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>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<not> (\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
\<lbrakk>\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i'\<ge>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>); ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) ?\<gamma>
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nxtEN[elim]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
  assumes "\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)"
    and "eval c t t' n (\<circle>\<^sub>b(\<gamma>))"
  shows "eval c t t' (Suc n) \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' (Suc n) \<gamma>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' (Suc n) \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' (Suc 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> eval c t t' (Suc n) \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' (Suc 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> eval c t t' (Suc n) \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' (Suc n) \<gamma>
[PROOF STEP]
from \<open>eval c t t' n (\<circle>\<^sub>b(\<gamma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<circle>\<^sub>b\<gamma>)

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

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' (Suc n) \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' (Suc n) \<gamma>
[PROOF STEP]
hence "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(Suc n))"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (\<^bsub>c\<^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>Suc n)
[PROOF STEP]
using \<open>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> assms(1) lActive_less
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))
\<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. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>Suc n)
[PROOF STEP]
by auto
[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>Suc n)

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' (Suc n) \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' (Suc 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>Suc n)
\<not> (\<exists>i\<ge>Suc n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[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>Suc n)
\<not> (\<exists>i\<ge>Suc n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. eval c t t' (Suc n) \<gamma>
[PROOF STEP]
using validCI_cont[where n="Suc n"] \<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>Suc n)
\<not> (\<exists>i\<ge>Suc n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<lbrakk>\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i'\<ge>Suc n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>); ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>Suc n)\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' (Suc n) ?\<gamma>
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval c t t' (Suc n) \<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' (Suc 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> eval c t t' (Suc 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> eval c t t' (Suc n) \<gamma>
[PROOF STEP]
from \<open>eval c t t' n (\<circle>\<^sub>b(\<gamma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<circle>\<^sub>b\<gamma>)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<circle>\<^sub>b\<gamma>)

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

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval c t t' (Suc 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. \<gamma> t (Suc n))
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc n)"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n (\<lambda>t n. \<gamma> t (Suc n))

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

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval c t t' (Suc 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>
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (Suc n)
[PROOF STEP]
show ?thesis
[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')) (Suc n)

goal (1 subgoal):
 1. eval c t t' (Suc n) \<gamma>
[PROOF STEP]
using validCI_not_act[of c t \<gamma> t' "Suc 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')) (Suc 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')) (Suc n)\<rbrakk> \<Longrightarrow> eval c t t' (Suc n) \<gamma>

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

goal:
No subgoals!
[PROOF STEP]
qed