[STATEMENT]
lemma untilIN[intro]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
    and n'::nat
  assumes "\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)"
    and "n'\<ge>n"
    and "eval c t t' n' \<gamma>"
    and a1: "\<And>n''. \<lbrakk>n\<le>n''; n''<n'\<rbrakk> \<Longrightarrow> 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. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

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

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<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')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>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]
from \<open>n'\<ge>n\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<le> n'
[PROOF STEP]
have "\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n') \<ge> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)"
[PROOF STATE]
proof (prove)
using this:
n \<le> n'

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<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:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
have "\<forall>x::nat\<ge> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n). 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>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. 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.allI[OF HOL.impI[OF HOL.impI]])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)" and "x<\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n')"
[PROOF STATE]
proof (state)
this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
x < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
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 "\<langle>c \<and> t\<rangle> \<le> n"
[PROOF STATE]
proof (prove)
using this:
\<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 \<open>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> lActive_less
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<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. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
with \<open>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<langle>c \<and> t\<rangle> \<le> n
[PROOF STEP]
have "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> n"
[PROOF STATE]
proof (prove)
using this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<langle>c \<and> t\<rangle> \<le> n

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

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
moreover
[PROOF STATE]
proof (state)
this:
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
from \<open>\<langle>c \<and> t\<rangle> \<le> n\<close> \<open>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n) \<le> x\<close>
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<and> t\<rangle> \<le> n
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
[PROOF STEP]
have "x \<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
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x
[PROOF STEP]
using cnf2bhv_ge_llength dual_order.trans
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<and> t\<rangle> \<le> n
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<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
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
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]
have "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) < n'"
[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[of c t x n']
[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> x; x < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'\<rbrakk> \<Longrightarrow> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x < 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 (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
moreover
[PROOF STATE]
proof (state)
this:
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x < n'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
from \<open>\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close> \<open>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> n\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>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)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
n \<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]
by auto
[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 (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x < n'
\<not> (\<exists>i''\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i''\<^esub>)
[PROOF STEP]
have "eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)) \<gamma>'"
[PROOF STATE]
proof (prove)
using this:
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x < n'
\<not> (\<exists>i''\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i''\<^esub>)

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

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
with \<open>\<not> (\<exists>i''\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i''\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<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>'
[PROOF STEP]
have "\<gamma>' (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)))"
[PROOF STATE]
proof (prove)
using this:
\<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>'

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. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
\<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>'
\<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. \<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 (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
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 (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
have "x \<ge> the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 \<le> x
[PROOF STEP]
using \<open>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n) \<le> x\<close> cnf2bhv_def
[PROOF STATE]
proof (prove)
using this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x
\<^bsub>?c\<^esub>\<down>\<^bsub>?t\<^esub>?n \<equiv> the_enat (llength (\<pi>\<^bsub>?c\<^esub>inf_llist ?t)) - 1 + (?n - \<langle>?c \<and> ?t\<rangle>)

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 (1 subgoal):
 1. \<And>x. \<lbrakk>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<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]
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 "\<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')) (\<^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
[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> ?n \<Longrightarrow> \<^bsub>?c\<^esub>\<down>\<^bsub>?t\<^esub>(\<^bsub>?c\<^esub>\<up>\<^bsub>?t\<^esub>?n) = ?n

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:
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. 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 (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')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n')
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. 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')
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. 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 validCI_cont[of c t n "\<lambda> t n. \<exists>n''\<ge>n. \<gamma> t n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' t n')" t']
    \<open>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> \<open>\<not>(\<exists>i'\<ge>n. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n')
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. 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
\<lbrakk>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<not> (\<exists>i'\<ge>n. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>); \<exists>n''\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'' \<and> (\<forall>n'\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. 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'))
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i'\<ge>n. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
n \<le> n'
eval c t t' n' \<gamma>
\<lbrakk>n \<le> ?n''2; ?n''2 < n'\<rbrakk> \<Longrightarrow> eval c t t' ?n''2 \<gamma>'
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<exists>n''\<ge>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'' \<and>
    (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n')"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
n \<le> n'
eval c t t' n' \<gamma>
\<lbrakk>n \<le> ?n''2; ?n''2 < n'\<rbrakk> \<Longrightarrow> eval c t t' ?n''2 \<gamma>'
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
with \<open>\<not>(\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<exists>n''\<ge>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<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:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<exists>n''\<ge>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<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_not_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:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<exists>n''\<ge>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n')
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<exists>n''\<ge>?n. \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) n'' \<and> (\<forall>n'\<ge>?n. 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 (1 subgoal):
 1. \<nexists>i. \<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