[STATEMENT]
lemma disjE[elim!]:
  assumes "eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')"
  shows "eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[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 \<gamma> \<or> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[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 \<gamma> \<or> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[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> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
from \<open>eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. \<gamma> t n \<or> \<gamma>' t n)"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<or> \<gamma>' t n)
[PROOF STEP]
using disj_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')
?\<gamma> \<or>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<or> ?\<gamma>' t n

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[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. \<gamma> t n \<or> \<gamma>' t n)
[PROOF STEP]
have "\<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> \<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>)"
[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. \<gamma> t n \<or> \<gamma>' t n)

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

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

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

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
using validCI_act[of n cid t \<gamma> t'] validCI_act[of n cid t \<gamma>' t']
[PROOF STATE]
proof (prove)
using this:
\<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>) \<or> \<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>)
\<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>
\<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 cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'

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

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<or> \<gamma>' t n)
[PROOF STEP]
using disj_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')
?\<gamma> \<or>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<or> ?\<gamma>' t n

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

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[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>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<or> \<gamma>' (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>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<or> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
using validCI_cont[of cid t n \<gamma> t'] validCI_cont[of cid t n \<gamma>' t']
[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>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<or> \<gamma>' (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>); \<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>
\<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 cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<or> \<gamma>' t n)
[PROOF STEP]
using disj_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')
?\<gamma> \<or>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<or> ?\<gamma>' t n

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[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. \<gamma> t n \<or> \<gamma>' t n)
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
    \<or> \<gamma>' (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. \<gamma> t n \<or> \<gamma>' t n)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<or> \<gamma>' (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. \<gamma> t n \<or> \<gamma>' 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. \<gamma> t n \<or> \<gamma>' t n)
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t n \<or> \<gamma>' t n)\<rbrakk> \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n \<or> \<gamma>' (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
using validCI_not_act[of cid t \<gamma> t' n] validCI_not_act[of cid t \<gamma>' t' n]
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<or> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^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>
\<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 cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma conjI[intro!]:
  assumes "eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'"
  shows "eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[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 (\<gamma> \<and>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[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 (\<gamma> \<and>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[PROOF STEP]
with \<open>eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<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>)
      \<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>)"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<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>) \<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>)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
\<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. \<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>) \<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>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<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>) \<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>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[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>
\<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>) \<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>)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)"
[PROOF STATE]
proof (prove)
using this:
\<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>) \<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>)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)
[PROOF STEP]
using validCI_act[where \<gamma>="\<lambda> t n. \<gamma> t n \<and> \<gamma>' t n"]
[PROOF STATE]
proof (prove)
using this:
\<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>) \<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>)
\<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>) \<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>)\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[PROOF STEP]
using conj_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)
?\<gamma> \<and>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<and> ?\<gamma>' t n

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[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 (\<gamma> \<and>\<^sup>b \<gamma>')
[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 (\<gamma> \<and>\<^sup>b \<gamma>')
[PROOF STEP]
with \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close> \<open>eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
      \<and> \<gamma>' (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>
eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<and> \<gamma>' (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>
eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
\<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. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<and> \<gamma>' (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:
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<and> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[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>)
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<and> \<gamma>' (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. \<gamma> t n \<and> \<gamma>' 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>)
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<and> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)
[PROOF STEP]
using validCI_cont[where \<gamma>="\<lambda> t n. \<gamma> t n \<and> \<gamma>' 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>)
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<and> \<gamma>' (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>); \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<and> \<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 (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[PROOF STEP]
using conj_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)
?\<gamma> \<and>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<and> ?\<gamma>' t n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[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 (\<gamma> \<and>\<^sup>b \<gamma>')
[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 (\<gamma> \<and>\<^sup>b \<gamma>')
[PROOF STEP]
with \<open>eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
    \<and> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

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

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
[PROOF STEP]
using conj_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)
?\<gamma> \<and>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<and> ?\<gamma>' t n

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)
[PROOF STEP]
using conj_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
?\<gamma> \<and>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<and> ?\<gamma>' t n

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
[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. \<gamma> t n \<and> \<gamma>' t n)
[PROOF STEP]
have "\<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>)
      \<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>)"
[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. \<gamma> t n \<and> \<gamma>' t n)

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
[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>
\<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>) \<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>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<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>) \<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>)

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<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>) \<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>)
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. eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'

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

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)
[PROOF STEP]
using conj_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
?\<gamma> \<and>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<and> ?\<gamma>' t n

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

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
[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>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<and> \<gamma>' (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>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<and> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

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

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)
[PROOF STEP]
using conj_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<and>\<^sup>b \<gamma>')
?\<gamma> \<and>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<and> ?\<gamma>' t n

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n \<gamma> \<and> eval cid t t' n \<gamma>'
[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. \<gamma> t n \<and> \<gamma>' t n)
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<and> \<gamma>' (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. \<gamma> t n \<and> \<gamma>' t n)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<and> \<gamma>' (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. \<gamma> t n \<and> \<gamma>' 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. \<gamma> t n \<and> \<gamma>' t n)
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t n \<and> \<gamma>' t n)\<rbrakk> \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n \<and> \<gamma>' (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma negI[intro!]:
  assumes "\<not> eval cid t t' n \<gamma>"
  shows "eval cid t t' n (\<not>\<^sup>b \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<not>\<^sup>b \<gamma>)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<not>\<^sup>b \<gamma>)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<not>\<^sup>b \<gamma>)
[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 (\<not>\<^sup>b \<gamma>)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<not>\<^sup>b \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<not>\<^sup>b \<gamma>)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<not>\<^sup>b \<gamma>)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<not>\<^sup>b \<gamma>)
[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 (\<not>\<^sup>b \<gamma>)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<not>\<^sup>b \<gamma>)
[PROOF STEP]
with \<open>\<not> eval cid t t' n \<gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> eval cid t t' n \<gamma>
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<not> \<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>)"
[PROOF STATE]
proof (prove)
using this:
\<not> eval cid t t' n \<gamma>
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

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

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

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

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<not>\<^sup>b \<gamma>)
[PROOF STEP]
using neg_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<not> \<gamma> t n)
\<not>\<^sup>b ?\<gamma> \<equiv> \<lambda>t n. \<not> ?\<gamma> t n

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

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

goal (1 subgoal):
 1. \<not> \<gamma> (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>
\<not> eval cid t t' n \<gamma>
\<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. \<not> \<gamma> (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:
\<not> \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<not>\<^sup>b \<gamma>)
[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>)
\<not> \<gamma> (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. \<not> \<gamma> 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>)
\<not> \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<not> \<gamma> t n)
[PROOF STEP]
using validCI_cont[where \<gamma>="\<lambda> t n. \<not> \<gamma> 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>)
\<not> \<gamma> (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>); \<not> \<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 (\<lambda>t n. \<not> \<gamma> t n)

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<not>\<^sup>b \<gamma>)
[PROOF STEP]
using neg_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<not> \<gamma> t n)
\<not>\<^sup>b ?\<gamma> \<equiv> \<lambda>t n. \<not> ?\<gamma> t n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<not>\<^sup>b \<gamma>)

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<not>\<^sup>b \<gamma>)
[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 (\<not>\<^sup>b \<gamma>)
[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 (\<not>\<^sup>b \<gamma>)
[PROOF STEP]
with \<open>\<not> eval cid t t' n \<gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> eval cid t t' n \<gamma>
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<not> \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n"
[PROOF STATE]
proof (prove)
using this:
\<not> eval cid t t' n \<gamma>
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

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

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<not>\<^sup>b \<gamma>)
[PROOF STEP]
using neg_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<not> \<gamma> t n)
\<not>\<^sup>b ?\<gamma> \<equiv> \<lambda>t n. \<not> ?\<gamma> t n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma negE[elim!]:
  assumes "eval cid t t' n (\<not>\<^sup>b \<gamma>)"
  shows "\<not> eval cid t t' n \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> eval cid t t' n \<gamma>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<not> eval cid t t' n \<gamma>
 2. \<not> ?P \<Longrightarrow> \<not> eval cid t t' n \<gamma>
[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> \<not> eval cid t t' n \<gamma>
 2. \<not> ?P \<Longrightarrow> \<not> eval cid t t' n \<gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> eval cid t t' n \<gamma>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<not> eval cid t t' n \<gamma>
 2. \<not> ?P \<Longrightarrow> \<not> eval cid t t' n \<gamma>
[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> \<not> eval cid t t' n \<gamma>
 2. \<not> ?P \<Longrightarrow> \<not> eval cid t t' n \<gamma>
[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> \<not> eval cid t t' n \<gamma>
 2. \<not> ?P \<Longrightarrow> \<not> eval cid t t' n \<gamma>
[PROOF STEP]
from \<open>eval cid t t' n (\<not>\<^sup>b \<gamma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<not>\<^sup>b \<gamma>)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. \<not> \<gamma> t n)"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<not>\<^sup>b \<gamma>)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<not> \<gamma> t n)
[PROOF STEP]
using neg_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<not>\<^sup>b \<gamma>)
\<not>\<^sup>b ?\<gamma> \<equiv> \<lambda>t n. \<not> ?\<gamma> t n

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<not> eval cid t t' n \<gamma>
 2. \<not> ?P \<Longrightarrow> \<not> eval cid t t' n \<gamma>
[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. \<not> \<gamma> t n)
[PROOF STEP]
have "\<not> \<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>)"
[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. \<not> \<gamma> t n)

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

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

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

goal (1 subgoal):
 1. \<not> eval cid t t' n \<gamma>
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> \<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>)
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. \<not> eval cid t t' n \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> eval cid t t' n \<gamma>

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

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<not> \<gamma> t n)
[PROOF STEP]
using neg_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<not>\<^sup>b \<gamma>)
\<not>\<^sup>b ?\<gamma> \<equiv> \<lambda>t n. \<not> ?\<gamma> t n

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

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

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> \<not> eval cid t t' n \<gamma>
[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>
\<not> \<gamma> (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>
\<not> \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

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

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

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

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<not> \<gamma> t n)
[PROOF STEP]
using neg_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<not>\<^sup>b \<gamma>)
\<not>\<^sup>b ?\<gamma> \<equiv> \<lambda>t n. \<not> ?\<gamma> t n

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

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

goal (1 subgoal):
 1. \<not> \<gamma> (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. \<not> \<gamma> 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. \<not> \<gamma> t n)
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n (\<lambda>t n. \<not> \<gamma> t n)\<rbrakk> \<Longrightarrow> \<not> \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

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

goal (1 subgoal):
 1. \<not> eval cid t t' n \<gamma>
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> \<gamma> (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. \<not> eval cid t t' n \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> eval cid t t' n \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed