[STATEMENT]
lemma globIN[intro]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
  assumes "\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)"
    and "\<And>n'. n'\<ge>n \<Longrightarrow> eval c t t' n' \<gamma>"
  shows "eval c t t' n (\<box>\<^sub>b(\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<box>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<box>\<^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 (\<box>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
from \<open>\<not>(\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "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 (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n (\<box>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<box>\<^sub>b\<gamma>)
[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> eval c t t' n (\<box>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
have "\<forall>x::nat\<ge> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n). \<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. \<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. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x \<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. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x \<longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
show "(x\<ge>\<^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. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x \<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. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x \<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)"
[PROOF STATE]
proof (state)
this:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x

goal (1 subgoal):
 1. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> 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:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x

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

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. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> 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' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>

goal (1 subgoal):
 1. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x \<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. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
lfinite (\<pi>\<^bsub>c\<^esub>inf_llist t)
\<exists>i. \<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. \<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. \<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>\<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 "n>\<langle>c \<and> t\<rangle>"
[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> < n
[PROOF STEP]
by (meson \<open>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> lActive_active leI le_eq_less_or_eq)
[PROOF STATE]
proof (state)
this:
\<langle>c \<and> t\<rangle> < n

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 "n\<ge>Suc (\<langle>c \<and> t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<and> t\<rangle> < n

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

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>n\<ge>Suc(\<langle>c \<and> t\<rangle>)\<close> \<open>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> n\<close>
[PROOF STATE]
proof (chain)
picking this:
Suc \<langle>c \<and> t\<rangle> \<le> n
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
Suc \<langle>c \<and> t\<rangle> \<le> n
[PROOF STEP]
have "\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>(x) \<ge> Suc (\<langle>c \<and> t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
Suc \<langle>c \<and> t\<rangle> \<le> n
n \<le> \<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x
Suc \<langle>c \<and> t\<rangle> \<le> n

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 (1 subgoal):
 1. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> 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' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<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>(\<^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>
\<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]
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:
eval c t t' (\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x) \<gamma>
\<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>)
\<lbrakk>\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; \<not> (\<exists>i'\<ge>\<^bsub>c\<^esub>\<up>\<^bsub>t\<^esub>x. \<parallel>c\<parallel>\<^bsub>t i'\<^esub>); 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. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> 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')) (\<^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 \<le> x \<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. \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> 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')) (\<^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:
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> x \<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>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<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 (\<box>\<^sub>b\<gamma>)
 2. \<not> ?P \<Longrightarrow> eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
with \<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>)
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<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. \<forall>n'\<ge>n. \<gamma> 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>)
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<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. \<forall>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
using validCI_cont[of c t n "\<lambda> t n. \<forall>n'\<ge>n. \<gamma> t n'" t']
[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>)
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<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>); \<forall>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'\<rbrakk> \<Longrightarrow> eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')

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

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

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

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

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

goal (1 subgoal):
 1. \<forall>n'\<ge>n. \<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'2 \<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. \<forall>n'\<ge>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>n'\<ge>n. \<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 (\<box>\<^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>
\<forall>n'\<ge>n. \<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. \<forall>n'\<ge>n. \<gamma> t n')"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>n'\<ge>n. \<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. \<forall>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
using validCI_not_act[where \<gamma>="\<lambda> t n. \<forall>n'\<ge>n. \<gamma> t n'"]
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<forall>n'\<ge>n. \<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>; \<forall>n'\<ge>?n. \<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. \<forall>n'\<ge>n. \<gamma> t n')

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma globEA[elim]:
  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 "eval c t t' n (\<box>\<^sub>b(\<gamma>))"
    and "n'\<ge>\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>"
  shows "eval c t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n' \<gamma>
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<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>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<gamma>
[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'
\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "the_enat (\<langle>c #\<^bsub>n'\<^esub> inf_llist t\<rangle>) \<ge> the_enat (\<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'
\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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]
using nAct_mono_lNact \<open>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<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>
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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 (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<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>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<gamma>
[PROOF STEP]
from \<open>eval c t t' n (\<box>\<^sub>b(\<gamma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<box>\<^sub>b\<gamma>)

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<gamma>
[PROOF STEP]
hence "\<forall>x\<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')) x"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')

goal (1 subgoal):
 1. \<forall>x\<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')) x
[PROOF STEP]
using validCE_act \<open>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')
\<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>)
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking 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>
\<forall>x\<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')) x
[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:
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>
\<forall>x\<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')) x

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

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

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

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

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

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

goal (1 subgoal):
 1. eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<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>
[PROOF STEP]
hence "\<forall>x\<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')) x"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')

goal (1 subgoal):
 1. \<forall>x\<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')) x
[PROOF STEP]
using validCE_act \<open>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')
\<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>)
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<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')) x

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n' \<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]
have "\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>\<le>llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
using nAct_le_proj
[PROOF STATE]
proof (prove)
using this:
\<langle>?c #\<^bsub>?n\<^esub>?t\<rangle> \<le> llength (\<pi>\<^bsub>?c\<^esub>?t)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<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> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<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> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[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 "llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))\<noteq>\<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<noteq> \<infinity>
[PROOF STEP]
by (metis llength_eq_infty_conv_lfinite lnth_inf_llist proj_finite2)
[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> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<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(\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)\<le>the_enat(llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)))"
[PROOF STATE]
proof (prove)
using this:
\<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 \<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 \<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> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[PROOF STEP]
moreover
[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))

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'>\<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> < n'
[PROOF STEP]
using lActive_active
[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> \<parallel>?c\<parallel>\<^bsub>?t \<langle>?c \<and> ?t\<rangle>\<^esub>

goal (1 subgoal):
 1. \<langle>c \<and> t\<rangle> < n'
[PROOF STEP]
by (meson leI le_eq_less_or_eq)
[PROOF STATE]
proof (state)
this:
\<langle>c \<and> t\<rangle> < 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') > the_enat (llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))) - 1"
[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. 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 \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t))
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:
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> the_enat (llength (\<pi>\<^bsub>c\<^esub>inf_llist t))
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 \<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>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<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')) x
the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[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:
\<forall>x\<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')) x
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. \<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. \<not> (\<exists>i\<ge>n'. \<parallel>c\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval c t t' n' \<gamma>
[PROOF STEP]
with \<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>)
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n')
[PROOF STEP]
show ?thesis
[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>)
\<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. eval c t t' n' \<gamma>
[PROOF STEP]
using validCI_cont
[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>)
\<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n')
\<lbrakk>\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>); ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^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]
by blast
[PROOF STATE]
proof (state)
this:
eval c t t' n' \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma globEANow:
  fixes c t t' n i \<gamma>
  assumes "n \<le> i"
    and "\<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and "eval c t t' n (\<box>\<^sub>b\<gamma>)"
  shows "eval c t t' i \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' i \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval c t t' i \<gamma>
[PROOF STEP]
from \<open>\<parallel>c\<parallel>\<^bsub>t i\<^esub>\<close> \<open>n \<le> i\<close>
[PROOF STATE]
proof (chain)
picking this:
\<parallel>c\<parallel>\<^bsub>t i\<^esub>
n \<le> i
[PROOF STEP]
have "\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
[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 auto
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

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

goal (1 subgoal):
 1. \<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
[PROOF STEP]
using dual_order.trans lNactLe
[PROOF STATE]
proof (prove)
using this:
n \<le> i
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
\<langle>?c \<Leftarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<le> ?n

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

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

goal (1 subgoal):
 1. eval c t t' i \<gamma>
[PROOF STEP]
using globEA[of n c t t' \<gamma> i] \<open>eval c t t' n (\<box>\<^sub>b\<gamma>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i
\<lbrakk>\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>; eval c t t' n (\<box>\<^sub>b\<gamma>); \<langle>c \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> i\<rbrakk> \<Longrightarrow> eval c t t' i \<gamma>
eval c t t' n (\<box>\<^sub>b\<gamma>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma globEN[elim]:
  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 "eval c t t' n (\<box>\<^sub>b(\<gamma>))"
    and "n'\<ge>n"
  shows "eval c t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n' \<gamma>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval c t t' n' \<gamma>
 2. \<not> ?P \<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> eval c t t' n' \<gamma>
 2. \<not> ?P \<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> eval c t t' n' \<gamma>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<gamma>
[PROOF STEP]
from \<open>eval c t t' n (\<box>\<^sub>b(\<gamma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<box>\<^sub>b\<gamma>)
[PROOF STEP]
have "eval c t t' n (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<box>\<^sub>b\<gamma>)

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

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

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

goal (1 subgoal):
 1. \<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
using validCE_cont[of c t n t' "\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n'"] \<open>\<not>(\<exists>i\<ge>n. \<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. \<forall>n'\<ge>n. \<gamma> t n')
\<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 (\<lambda>t n. \<forall>n'\<ge>n. \<gamma> t n')\<rbrakk> \<Longrightarrow> \<forall>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'
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<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>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<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>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<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>
 2. \<not> ?P \<Longrightarrow> eval c t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'
[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:
\<forall>x\<ge>\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) x
\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n \<le> \<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n'

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

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

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

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

goal (1 subgoal):
 1. \<forall>n'\<ge>n. \<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. \<forall>n'\<ge>n. \<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. \<forall>n'\<ge>n. \<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. \<forall>n'\<ge>n. \<gamma> t n')\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>?n. \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) n'

goal (1 subgoal):
 1. \<forall>n'\<ge>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>n'\<ge>n. \<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>
[PROOF STEP]
with \<open>\<not>(\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)\<close> \<open>n'\<ge>n\<close>
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
n \<le> n'
\<forall>n'\<ge>n. \<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>
n \<le> n'
\<forall>n'\<ge>n. \<gamma> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t')) n'

goal (1 subgoal):
 1. 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>
n \<le> n'
\<forall>n'\<ge>n. \<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. 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