[STATEMENT]
lemma evtEA[elim]:
  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 "eval c t t' n (\<diamond>\<^sub>b(\<gamma>))"
  shows "\<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>.
          (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge> \<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n''\<le>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or>
          (\<not>(\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
from \<open>eval c t t' n (\<diamond>\<^sub>b(\<gamma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<diamond>\<^sub>b\<gamma>)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<exists>n'\<ge>n. \<gamma> t n')"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<diamond>\<^sub>b\<gamma>)

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x

goal (1 subgoal):
 1. \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
assume "x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
from \<open>(x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))\<close>
[PROOF STATE]
proof (chain)
picking this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
[PROOF STEP]
have "llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<noteq>\<infinity>"
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

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

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[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>1"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. 1 \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
using proj_one[of "inf_llist t"]
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<exists>i. enat i < llength (inf_llist t) \<and> \<parallel>?c\<parallel>\<^bsub>lnth (inf_llist t) i\<^esub> \<Longrightarrow> 1 \<le> llength (\<pi>\<^bsub>?c\<^esub>inf_llist t)

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

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>
1 \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
have "the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1 < x"
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>
1 \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
[PROOF STEP]
by (metis One_nat_def Suc_ile_eq antisym_conv2 diff_Suc_less enat_ord_simps(2)
          enat_the_enat less_imp_diff_less one_enat_def)
[PROOF STATE]
proof (state)
this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
hence "x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x))"
[PROOF STATE]
proof (prove)
using this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x

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

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

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
with \<open>\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) x\<close>
[PROOF STATE]
proof (chain)
picking this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)
[PROOF STEP]
have "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)))"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)

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

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
have "\<not>(\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x). \<parallel>c\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
from \<open>x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<close>
[PROOF STATE]
proof (chain)
picking this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
[PROOF STEP]
have "lfinite (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
\<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x))
\<not> (\<exists>i\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

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

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

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
have "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
from \<open>x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<close>
[PROOF STATE]
proof (chain)
picking this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x
[PROOF STEP]
have "lfinite (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
have "\<langle>c \<and> t\<rangle>\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>n''>z. \<not> \<parallel>c\<parallel>\<^bsub>t n''\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

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

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

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

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

goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<langle>c \<and> t\<rangle>
\<langle>c \<and> t\<rangle> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
show "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<langle>c \<and> t\<rangle>
\<langle>c \<and> t\<rangle> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (2 subgoals):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
 2. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> ?P2\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

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

goal (1 subgoal):
 1. \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>

goal (1 subgoal):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
assume "\<not>(x \<ge> llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))"
[PROOF STATE]
proof (state)
this:
\<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n' \<le> i
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)

goal (1 subgoal):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
have "(\<forall>n''\<ge> \<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub>. n''\<le>\<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n''. \<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n'' \<longrightarrow> n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>
[PROOF STEP]
fix n''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n''. \<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n'' \<longrightarrow> n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>
[PROOF STEP]
show "\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n'' \<longrightarrow> n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n'' \<longrightarrow> n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>
[PROOF STEP]
proof(rule HOL.impI[OF HOL.impI])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''; n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>
[PROOF STEP]
assume "\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''" and "n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''
n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''; n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>
[PROOF STEP]
from \<open>\<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''; n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>
[PROOF STEP]
have "\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (the_enat (\<langle>c #\<^bsub>enat i\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
have "enat i - 1 < llength (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat i - 1 < llength (inf_llist t)
[PROOF STEP]
by (simp add: one_enat_def)
[PROOF STATE]
proof (state)
this:
enat i - 1 < llength (inf_llist t)

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

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

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

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

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

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = the_enat \<langle>c #\<^bsub>enat i\<^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 i\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using \<open>\<gamma> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) x\<close>
[PROOF STATE]
proof (prove)
using this:
x = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x

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

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

goal (1 subgoal):
 1. \<lbrakk>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''; n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>
[PROOF STEP]
with \<open>the_enat (\<langle>c #\<^bsub>enat i\<^esub> inf_llist t\<rangle>) = the_enat (\<langle>c #\<^bsub>enat n''\<^esub> inf_llist t\<rangle>)\<close>
[PROOF STATE]
proof (chain)
picking this:
the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> = the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat i\<^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>enat n''\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> = the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>c #\<^bsub>enat i\<^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. \<lbrakk>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n''; n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub>\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> = the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<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')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
show "eval c t t' n'' \<gamma>"
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> = the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<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')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. eval c t t' n'' \<gamma>
[PROOF STEP]
using validCI_act
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle> = the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<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')) (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)
\<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
[PROOF STATE]
proof (state)
this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub> \<le> n'' \<longrightarrow> n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>

goal (1 subgoal):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>

goal (1 subgoal):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
have "i\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
[PROOF STEP]
have "enat i - 1 < llength (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat i - 1 < llength (inf_llist t)
[PROOF STEP]
by (simp add: one_enat_def)
[PROOF STATE]
proof (state)
this:
enat i - 1 < llength (inf_llist t)

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

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

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

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

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

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

goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
[PROOF STEP]
with \<open>x\<ge>the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)\<close>
[PROOF STATE]
proof (chain)
picking this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x
x = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "the_enat (\<langle>c #\<^bsub>i\<^esub> inf_llist t\<rangle>)\<ge>the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x
x = the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

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

goal (1 subgoal):
 1. \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
[PROOF STEP]
with \<open>\<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat i\<^esub>inf_llist t\<rangle>

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

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

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

goal (1 subgoal):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x; \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n' \<le> i
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)
\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' \<le> i
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>k\<ge>n'. latestAct_cond c t i k)
\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>i\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>i\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i

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

goal (1 subgoal):
 1. \<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n'\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval c t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n' \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed