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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
from \<open>eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[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:
eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)

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 until_def
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
?\<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 (\<lambda>t n. \<exists>n''\<ge>n. \<gamma> t n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' t n'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval c t t' n (\<lambda>t n. \<exists>n''\<ge>n. \<gamma> t n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' t n'))

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n (\<lambda>t n. \<exists>n''\<ge>n. \<gamma> t n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' t n'))
[PROOF STEP]
have "\<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')"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
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. \<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')
[PROOF STEP]
using validCE_cont[where \<gamma>="\<lambda> t n. \<exists>n''\<ge>n. \<gamma> t n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' t n')"]
    \<open>\<nexists>i. i\<ge>n \<and> \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
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'))
\<lbrakk>\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>); eval ?cid ?t ?t' ?n (\<lambda>t n. \<exists>n''\<ge>n. \<gamma> t n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' t n'))\<rbrakk> \<Longrightarrow> \<exists>n''\<ge>\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n. \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) n'' \<and> (\<forall>n'\<ge>\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n. n' < n'' \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) n')
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<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')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<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')

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
from \<open>\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1 < x"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x
[PROOF STEP]
have "\<langle>c \<and> t\<rangle> < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c \<and> t\<rangle> < n
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
assume "\<not>\<langle>c \<and> t\<rangle> < n"
[PROOF STATE]
proof (state)
this:
\<not> \<langle>c \<and> t\<rangle> < n

goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
hence "\<langle>c \<and> t\<rangle> \<ge> n"
[PROOF STATE]
proof (prove)
using this:
\<not> \<langle>c \<and> t\<rangle> < n

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

goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<le> \<langle>c \<and> t\<rangle>

goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
from \<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 (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 "\<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>"
[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. \<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>
[PROOF STEP]
using lActive_active less_or_eq_imp_le
[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>\<parallel>?c\<parallel>\<^bsub>?t ?i\<^esub>; \<forall>n'>?n. \<not> \<parallel>?c\<parallel>\<^bsub>?t n'\<^esub>\<rbrakk> \<Longrightarrow> \<parallel>?c\<parallel>\<^bsub>?t \<langle>?c \<and> ?t\<rangle>\<^esub>
?m < ?n \<or> ?m = ?n \<Longrightarrow> ?m \<le> ?n

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

goal (1 subgoal):
 1. \<not> \<langle>c \<and> t\<rangle> < n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<le> \<langle>c \<and> t\<rangle>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<le> \<langle>c \<and> t\<rangle>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> \<langle>c \<and> t\<rangle>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<and> t\<rangle>\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c \<and> t\<rangle> < n

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

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

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
hence "x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x))"
[PROOF STATE]
proof (prove)
using this:
the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t)) - 1 < x

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
from \<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 (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 "\<langle>c \<and> t\<rangle> \<le> 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. \<langle>c \<and> t\<rangle> \<le> n
[PROOF STEP]
using lActive_less[of c t _ 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>)
\<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 (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[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 "n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)"
[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 blast
[PROOF STATE]
proof (state)
this:
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
have "\<forall>n''\<ge>n. n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<longrightarrow> eval c t t' n'' \<gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n''\<ge>n. n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x \<longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
proof (rule HOL.allI[OF HOL.impI[OF HOL.impI]])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n''. \<lbrakk>n \<le> n''; n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
fix n''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n''. \<lbrakk>n \<le> n''; n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
assume "n \<le> n''" and "n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)"
[PROOF STATE]
proof (state)
this:
n \<le> n''
n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<And>n''. \<lbrakk>n \<le> n''; n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
hence "\<^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''
n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

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'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
?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 (1 subgoal):
 1. \<And>n''. \<lbrakk>n \<le> n''; n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<rbrakk> \<Longrightarrow> eval c t t' n'' \<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 (1 subgoal):
 1. \<And>n''. \<lbrakk>n \<le> n''; n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
have "n''<\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
by (simp add: \<open>n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<close>)
[PROOF STATE]
proof (state)
this:
n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

goal (1 subgoal):
 1. \<And>n''. \<lbrakk>n \<le> n''; n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
with \<open>\<langle>c \<and> t\<rangle> \<le> n\<close> \<open>n \<le> n''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<langle>c \<and> t\<rangle> \<le> n
n \<le> n''
n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
[PROOF STEP]
have "\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n'')<\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x))"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<and> t\<rangle> \<le> n
n \<le> n''
n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x

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

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

goal (1 subgoal):
 1. \<And>n''. \<lbrakk>n \<le> n''; n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
with \<open>x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x))\<close>
[PROOF STATE]
proof (chain)
picking this:
x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'' < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)
[PROOF STEP]
have "\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n'')< x"
[PROOF STATE]
proof (prove)
using this:
x = \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'' < \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x)

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

goal (1 subgoal):
 1. \<And>n''. \<lbrakk>n \<le> n''; n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n''
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'' < x
[PROOF STEP]
have "\<gamma>' (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n''))"
[PROOF STATE]
proof (prove)
using this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n''
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'' < x

goal (1 subgoal):
 1. \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'')
[PROOF STEP]
using \<open>\<forall>x'\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n). x'<x \<longrightarrow> \<gamma>' (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) x'\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n''
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'' < x
\<forall>x'\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. x' < x \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x'

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

goal (1 subgoal):
 1. \<And>n''. \<lbrakk>n \<le> n''; n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x\<rbrakk> \<Longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<gamma>' (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'')

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
using \<open>\<nexists>i. i\<ge>n \<and> \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> n''
\<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>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<ge>n''. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

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

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

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
 2. \<not> ?P \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<forall>n''\<ge>n. n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x \<longrightarrow> eval c t t' n'' \<gamma>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
\<forall>n''\<ge>n. n'' < \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x \<longrightarrow> eval c t t' n'' \<gamma>'

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

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
from \<open>eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[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:
eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)

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 until_def
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
?\<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 (\<lambda>t n. \<exists>n''\<ge>n. \<gamma> t n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' t n'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval c t t' n (\<lambda>t n. \<exists>n''\<ge>n. \<gamma> t n'' \<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> \<exists>n'\<ge>n. eval c t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval c t t' n'' \<gamma>')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n (\<lambda>t n. \<exists>n''\<ge>n. \<gamma> t n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' t n'))
[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:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
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. \<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 \<open>\<not>(\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
    validCE_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>
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'))
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n (\<lambda>t n. \<exists>n''\<ge>n. \<gamma> t n'' \<and> (\<forall>n'\<ge>n. n' < n'' \<longrightarrow> \<gamma>' t n'))\<rbrakk> \<Longrightarrow> \<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')

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extNTA2J_iff [simp]:
  "extNTA2J P (C, M, a) = ({this:Class (fst (method P C M))=\<lfloor>Addr a\<rfloor>; snd (the (snd (snd (snd (method P C M)))))}, Map.empty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extNTA2J P (C, M, a) = ({this:Class (fst (method P C M))=\<lfloor>Addr a\<rfloor>; snd (the (snd (snd (snd (method P C M)))))}, Map.empty)
[PROOF STEP]
by(simp add: extNTA2J_def split_beta)


[STATEMENT]
lemma extTA2J_\<epsilon>: "extTA2J P \<epsilon> = \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extTA2J P \<lbrace>\<rbrace> = \<lbrace>\<rbrace>
[PROOF STEP]
by(simp)


[STATEMENT]
lemma [iff]:
  "\<not> extTA,P,t \<turnstile> \<langle>Val v, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> extTA,P,t \<turnstile> \<langle>Val v,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>
[PROOF STEP]
by(fastforce elim:red.cases)


[STATEMENT]
lemma red_no_val [dest]:
  "\<lbrakk> extTA,P,t \<turnstile> \<langle>e, s\<rangle> -tas\<rightarrow> \<langle>e', s'\<rangle>; is_val e \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -tas\<rightarrow> \<langle>e',s'\<rangle>; is_val e\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(auto)


[STATEMENT]
lemma [iff]: "\<not> extTA,P,t \<turnstile> \<langle>Throw a, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> extTA,P,t \<turnstile> \<langle>Throw a,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>
[PROOF STEP]
by(fastforce elim: red_cases)


[STATEMENT]
lemma reds_map_Val_Throw:
  "extTA,P,t \<turnstile> \<langle>map Val vs @ Throw a # es, s\<rangle> [-ta\<rightarrow>] \<langle>es', s'\<rangle> \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>map Val vs @ Throw a # es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle> = False
[PROOF STEP]
by(induct vs arbitrary: es')(auto elim!: reds_cases)


[STATEMENT]
lemma reds_preserves_len:
  "extTA,P,t \<turnstile> \<langle>es, s\<rangle> [-ta\<rightarrow>] \<langle>es', s'\<rangle> \<Longrightarrow> length es' = length es"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> length es' = length es
[PROOF STEP]
by(induct es arbitrary: es')(auto elim: reds.cases)


[STATEMENT]
lemma red_lcl_incr: "extTA,P,t \<turnstile> \<langle>e, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s')"
  and reds_lcl_incr: "extTA,P,t \<turnstile> \<langle>es, s\<rangle> [-ta\<rightarrow>] \<langle>es', s'\<rangle> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s')) &&& (extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s'))
[PROOF STEP]
apply(induct rule:red_reds.inducts)
[PROOF STATE]
proof (prove)
goal (98 subgoals):
 1. \<And>h' a h C l. (h', a) \<in> allocate h (Class_type C) \<Longrightarrow> dom (lcl (h, l)) \<subseteq> dom (lcl (h', l))
 2. \<And>h C l. allocate h (Class_type C) = {} \<Longrightarrow> dom (lcl (h, l)) \<subseteq> dom (lcl (h, l))
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; dom (lcl s) \<subseteq> dom (lcl s')\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s')
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i)))\<rbrakk> \<Longrightarrow> dom (lcl (h, l)) \<subseteq> dom (lcl (h', l))
 5. \<And>i T s. i <s 0 \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s)
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}\<rbrakk> \<Longrightarrow> dom (lcl (h, l)) \<subseteq> dom (lcl (h, l))
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; dom (lcl s) \<subseteq> dom (lcl s')\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s')
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s)
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s)
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; dom (lcl s) \<subseteq> dom (lcl s')\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s')
A total of 98 subgoals...
[PROOF STEP]
apply(auto simp del: fun_upd_apply split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done