[STATEMENT]
lemma allI[intro!]:
  assumes "\<forall>p. eval cid t t' n (\<gamma> p)"
  shows "eval cid t t' n (all (\<lambda>p. \<gamma> p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
assume "\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
assume "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

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

goal (1 subgoal):
 1. \<forall>p. \<gamma> p (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>)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p. eval cid t t' n (\<gamma> p)
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<forall>p. \<gamma> p (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>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (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>)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<forall>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
[PROOF STEP]
using validCI_act[where \<gamma>="\<lambda>t n. (\<forall>y. (\<gamma> y t n))"]
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (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>)
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<forall>y. \<gamma> y (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 (\<lambda>t n. \<forall>y. \<gamma> y t n)

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
using all_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
local.all \<gamma> \<equiv> \<lambda>t n. \<forall>y. \<gamma> y t n

goal (1 subgoal):
 1. eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close> \<open>\<forall>p. eval cid t t' n (\<gamma> p)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. eval cid t t' n (\<gamma> p)
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "\<forall>p. (\<gamma> p) (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. eval cid t t' n (\<gamma> p)
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. eval cid t t' n (\<gamma> p)
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close> \<open>\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<forall>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
[PROOF STEP]
using validCI_cont[where \<gamma>="\<lambda>t n. (\<forall>y. (\<gamma> y t n))"]
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^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>); \<forall>y. \<gamma> y (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 (\<lambda>t n. \<forall>y. \<gamma> y t n)

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
using all_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
local.all \<gamma> \<equiv> \<lambda>t n. \<forall>y. \<gamma> y t n

goal (1 subgoal):
 1. eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<forall>p. eval cid t t' n (\<gamma> p)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>p. eval cid t t' n (\<gamma> p)
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<forall>p. (\<gamma> p) (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. eval cid t t' n (\<gamma> p)
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p. eval cid t t' n (\<gamma> p)
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<forall>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n

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

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
using all_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
local.all \<gamma> \<equiv> \<lambda>t n. \<forall>y. \<gamma> y t n

goal (1 subgoal):
 1. eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma allE[elim!]:
  assumes "eval cid t t' n (all (\<lambda>p. \<gamma> p))"
  shows "\<forall>p. eval cid t t' n (\<gamma> p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
 2. \<not> ?P \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
assume "(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
 2. \<not> ?P \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
 2. \<not> ?P \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
assume "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
 2. \<not> ?P \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
from \<open>eval cid t t' n (all (\<lambda>p. \<gamma> p))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<forall>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
[PROOF STEP]
using all_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
local.all \<gamma> \<equiv> \<lambda>t n. \<forall>y. \<gamma> y t n

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

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

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

goal (1 subgoal):
 1. \<forall>p. \<gamma> p (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>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

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

goal (1 subgoal):
 1. \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (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>)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
from \<open>eval cid t t' n (all (\<lambda>p. \<gamma> p))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<forall>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
[PROOF STEP]
using all_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
local.all \<gamma> \<equiv> \<lambda>t n. \<forall>y. \<gamma> y t n

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
[PROOF STEP]
have "\<forall>p. (\<gamma> p) (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)

goal (1 subgoal):
 1. \<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
using validCE_cont[where \<gamma>="\<lambda>t n. (\<forall>y. (\<gamma> y t n))"] \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y 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. \<forall>y. \<gamma> y t n)\<rbrakk> \<Longrightarrow> \<forall>y. \<gamma> y (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n)
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

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

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

goal (1 subgoal):
 1. \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p. eval cid t t' n (\<gamma> p)

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

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
from \<open>eval cid t t' n (all (\<lambda>p. \<gamma> p))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<forall>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
[PROOF STEP]
using all_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<forall>\<^sub>bp. \<gamma> p)
local.all \<gamma> \<equiv> \<lambda>t n. \<forall>y. \<gamma> y t n

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
[PROOF STEP]
have "\<forall>p. (\<gamma> p) (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)

goal (1 subgoal):
 1. \<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
using validCE_not_act[where \<gamma>="\<lambda>t n. (\<forall>y. (\<gamma> y t n))"]
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<forall>y. \<gamma> y t n)
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n (\<lambda>t n. \<forall>y. \<gamma> y t n)\<rbrakk> \<Longrightarrow> \<forall>y. \<gamma> y (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
with \<open>\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n

goal (1 subgoal):
 1. \<forall>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<forall>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exI[intro!]:
  assumes "\<exists>p. eval cid t t' n (\<gamma> p)"
  shows "eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
assume "\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
assume "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<exists>p. eval cid t t' n (\<gamma> p)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. eval cid t t' n (\<gamma> p)
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<exists>p. (\<gamma> p) (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>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. eval cid t t' n (\<gamma> p)
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<exists>p. \<gamma> p (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>)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>p. eval cid t t' n (\<gamma> p)
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<exists>p. \<gamma> p (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>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (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>)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<exists>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
[PROOF STEP]
using validCI_act[where \<gamma>="\<lambda>t n. (\<exists>y. (\<gamma> y t n))"]
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (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>)
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<exists>y. \<gamma> y (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 (\<lambda>t n. \<exists>y. \<gamma> y t n)

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)

goal (1 subgoal):
 1. eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
using ex_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
local.ex \<gamma> \<equiv> \<lambda>t n. \<exists>y. \<gamma> y t n

goal (1 subgoal):
 1. eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close> \<open>\<exists>p. eval cid t t' n (\<gamma> p)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. eval cid t t' n (\<gamma> p)
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "\<exists>p. (\<gamma> p) (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. eval cid t t' n (\<gamma> p)
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. eval cid t t' n (\<gamma> p)
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close> \<open>\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<exists>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
[PROOF STEP]
using validCI_cont[where \<gamma>="\<lambda>t n. (\<exists>y. (\<gamma> y t n))"]
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^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>); \<exists>y. \<gamma> y (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 (\<lambda>t n. \<exists>y. \<gamma> y t n)

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)

goal (1 subgoal):
 1. eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
using ex_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
local.ex \<gamma> \<equiv> \<lambda>t n. \<exists>y. \<gamma> y t n

goal (1 subgoal):
 1. eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<exists>p. eval cid t t' n (\<gamma> p)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. eval cid t t' n (\<gamma> p)
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<exists>p. (\<gamma> p) (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. eval cid t t' n (\<gamma> p)
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>p. eval cid t t' n (\<gamma> p)
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
with \<open>\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<exists>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
[PROOF STEP]
using validCI_not_act[where \<gamma>="\<lambda>t n. (\<exists>y. (\<gamma> y t n))"]
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<exists>y. \<gamma> y (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<lambda>t n. \<exists>y. \<gamma> y t n)

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)

goal (1 subgoal):
 1. eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
using ex_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
local.ex \<gamma> \<equiv> \<lambda>t n. \<exists>y. \<gamma> y t n

goal (1 subgoal):
 1. eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exE[elim!]:
  assumes "eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)"
  shows "\<exists>p. eval cid t t' n (\<gamma> p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
 2. \<not> ?P \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
assume "(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
 2. \<not> ?P \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
 2. \<not> ?P \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
assume "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
 2. \<not> ?P \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
from \<open>eval cid t t' n (ex (\<lambda>p. \<gamma> p))\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<exists>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
[PROOF STEP]
using ex_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
local.ex \<gamma> \<equiv> \<lambda>t n. \<exists>y. \<gamma> y t n

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

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

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

goal (1 subgoal):
 1. \<exists>p. \<gamma> p (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>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

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

goal (1 subgoal):
 1. \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (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>)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
from \<open>eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<exists>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
[PROOF STEP]
using ex_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
local.ex \<gamma> \<equiv> \<lambda>t n. \<exists>y. \<gamma> y t n

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
[PROOF STEP]
have "\<exists>p. (\<gamma> p) (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)

goal (1 subgoal):
 1. \<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
using validCE_cont[where \<gamma>="\<lambda>t n. (\<exists>y. (\<gamma> y t n))"] \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y 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>y. \<gamma> y t n)\<rbrakk> \<Longrightarrow> \<exists>y. \<gamma> y (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n)
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

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

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

goal (1 subgoal):
 1. \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>p. eval cid t t' n (\<gamma> p)

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

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
from \<open>eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. (\<exists>y. (\<gamma> y t n)))"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
[PROOF STEP]
using ex_def[of \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<exists>\<^sub>bp. \<gamma> p)
local.ex \<gamma> \<equiv> \<lambda>t n. \<exists>y. \<gamma> y t n

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
[PROOF STEP]
have "\<exists>p. (\<gamma> p) (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)

goal (1 subgoal):
 1. \<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
using validCE_not_act[where \<gamma>="\<lambda>t n. (\<exists>y. (\<gamma> y t n))"]
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<exists>y. \<gamma> y t n)
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n (\<lambda>t n. \<exists>y. \<gamma> y t n)\<rbrakk> \<Longrightarrow> \<exists>y. \<gamma> y (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
with \<open>\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n

goal (1 subgoal):
 1. \<exists>p. eval cid t t' n (\<gamma> p)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<exists>p. \<gamma> p (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<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>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal:
No subgoals!
[PROOF STEP]
qed