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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^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 (\<gamma>' \<UU>\<^sub>b \<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
have "the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>) \<le> the_enat (\<langle>c #\<^bsub>n''\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
from \<open>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>\<le>n'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
[PROOF STEP]
have "\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle> \<le> \<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
moreover
[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 (\<gamma>' \<UU>\<^sub>b \<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
have "\<forall>n'\<ge>the_enat \<langle>c #\<^bsub>n\<^esub>inf_llist t\<rangle>. n' < (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)
    \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n'\<ge>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>. n' < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> n' \<longrightarrow> n' < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
fix x::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> n' \<longrightarrow> n' < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
show "x\<ge>the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)
      \<longrightarrow> x < (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x \<longrightarrow> x < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
proof (rule HOL.impI[OF HOL.impI])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x; x < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>\<rbrakk> \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
assume "x\<ge>the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)" and "x < (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>)"
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x
x < the_enat \<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; x < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>\<rbrakk> \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x
x < the_enat \<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; x < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>\<rbrakk> \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
have "the_enat (\<langle>c #\<^bsub>enat n''\<^esub> inf_llist t\<rangle>) = \<langle>c #\<^bsub>enat n''\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>) = \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>) = \<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; x < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>\<rbrakk> \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> x
x < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
enat (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>) = \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "x<llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[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 n''\<^esub>inf_llist t\<rangle>
enat (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>) = \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
using nAct_le_proj[of c n'' "inf_llist t"]
[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 n''\<^esub>inf_llist t\<rangle>
enat (the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>) = \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle> \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
by (metis enat_ord_simps(2) less_le_trans)
[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; x < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>\<rbrakk> \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
hence "x<llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (prove)
using this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

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; x < the_enat \<langle>c #\<^bsub>enat n''\<^esub>inf_llist t\<rangle>\<rbrakk> \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
obtain n'::nat where "x=\<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. eval c t t' n' \<gamma> &&& \<forall>n''\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> (\<exists>i\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> (\<exists>n'''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval c t t' n''' \<gamma>') \<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:
eval c t t' n' \<gamma>
\<forall>n''\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> (\<exists>i\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> (\<exists>n'''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval c t t' n''' \<gamma>') \<or> \<not> (\<exists>i\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n'' \<gamma>'

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[PROOF STEP]
have "the_enat(llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1 \<ge> the_enat(\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1
[PROOF STEP]
from \<open>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)) \<ge> eSuc (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. eSuc \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
using nAct_llength_proj
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<Longrightarrow> eSuc \<langle>?c #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle> \<le> llength (\<pi>\<^bsub>?c\<^esub>inf_llist ?t)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> x
[PROOF STEP]
using enat_ord_simps(1)
[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) = enat (the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)))
(enat ?m \<le> enat ?n) = (?m \<le> ?n)

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

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

goal (1 subgoal):
 1. \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x < n'
[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
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<exists>i. enat i < llength ?t \<and> \<parallel>?c\<parallel>\<^bsub>lnth ?t i\<^esub> \<Longrightarrow> 1 \<le> llength (\<pi>\<^bsub>?c\<^esub>?t)

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

goal (1 subgoal):
 1. \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x < n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> x
1 \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
have "the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x"
[PROOF STATE]
proof (prove)
using this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) \<le> x
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 \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x

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

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

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

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

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

goal (1 subgoal):
 1. eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>'
[PROOF STEP]
using a2
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x < n'
\<forall>n''\<ge>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> (\<exists>i\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> (\<exists>n'''\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval c t t' n''' \<gamma>') \<or> \<not> (\<exists>i\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<and> eval c t t' n'' \<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. ?P \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
 2. \<not> ?P \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
hence "\<gamma>' (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. i < n'
[PROOF STEP]
with \<open>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)
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'

goal (1 subgoal):
 1. i < n'
[PROOF STEP]
using \<open>\<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)\<close> \<open>\<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> le_neq_implies_less nat_le_linear
[PROOF STATE]
proof (prove)
using this:
enat x < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
\<not> (\<exists>i'\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<lbrakk>?m \<le> ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> ?m < ?n
?m \<le> ?n \<or> ?n \<le> ?m

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i < n'

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

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

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

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

goal (1 subgoal):
 1. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
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. \<not> llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<le> enat x \<Longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
with \<open>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 less_or_eq_imp_le
[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>
?m < ?n \<or> ?m = ?n \<Longrightarrow> ?m \<le> ?n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed