[STATEMENT]
lemma baIA[intro]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
  assumes "\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and "\<phi> (\<sigma>\<^bsub>c\<^esub>(t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>))"
  shows "eval c t t' n (ba \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
have "\<phi> (\<sigma>\<^bsub>c\<^esub>(t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "\<sigma>\<^bsub>c\<^esub>(t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) = lnth (\<pi>\<^bsub>c\<^esub>(inf_llist t)) (the_enat (\<langle>c #\<^bsub>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
have "enat (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) < llength (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) < llength (inf_llist t)
[PROOF STEP]
using enat_ord_code
[PROOF STATE]
proof (prove)
using this:
(enat ?m \<le> enat ?n) = (?m \<le> ?n)
(enat ?m < enat ?n) = (?m < ?n)
(?q \<le> \<infinity>) = True
(enat ?m < \<infinity>) = True
(\<infinity> \<le> enat ?n) = False
(\<infinity> < ?q) = False

goal (1 subgoal):
 1. enat (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) < llength (inf_llist t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) < llength (inf_llist t)

goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enat (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) < llength (inf_llist t)

goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
have "\<parallel>c\<parallel>\<^bsub>t (\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
using nxtActI
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<Longrightarrow> ?n \<le> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<and> \<parallel>?c\<parallel>\<^bsub>?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>\<^esub> \<and> \<not> (\<exists>k\<ge>?n. latestAct_cond ?c ?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> k)

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

goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
hence "\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (1 subgoal):
 1. \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enat (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) < llength (inf_llist t)
\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
enat (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) < llength (inf_llist t)
\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using proj_active_nth
[PROOF STATE]
proof (prove)
using this:
enat (Suc \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) < llength (inf_llist t)
\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
\<lbrakk>enat (Suc ?i) < llength ?t; \<parallel>?c\<parallel>\<^bsub>lnth ?t ?i\<^esub>\<rbrakk> \<Longrightarrow> lnth (\<pi>\<^bsub>?c\<^esub>?t) (the_enat \<langle>?c #\<^bsub>enat ?i\<^esub>?t\<rangle>) = \<sigma>\<^bsub>?c\<^esub>lnth ?t ?i

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
have "\<phi> (lnth (\<pi>\<^bsub>c\<^esub>(inf_llist t)) (the_enat(\<langle>c #\<^bsub>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> inf_llist t\<rangle>)))"
[PROOF STATE]
proof (prove)
using this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>))

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle> = \<langle>c #\<^bsub>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
have "\<nexists>k. n\<le>k \<and> k<\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<and> \<parallel>c\<parallel>\<^bsub>t k\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
[PROOF STEP]
using nxtActI
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<Longrightarrow> ?n \<le> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<and> \<parallel>?c\<parallel>\<^bsub>?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>\<^esub> \<and> \<not> (\<exists>k\<ge>?n. latestAct_cond ?c ?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> k)

goal (1 subgoal):
 1. \<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
hence "\<not> (\<exists>k\<ge>n. k < \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<and> \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) k\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

goal (1 subgoal):
 1. \<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)
[PROOF STEP]
by (simp add: one_enat_def)
[PROOF STATE]
proof (state)
this:
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
have "\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<ge>n"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
[PROOF STEP]
using nxtActI
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<Longrightarrow> ?n \<le> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<and> \<parallel>?c\<parallel>\<^bsub>?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>\<^esub> \<and> \<not> (\<exists>k\<ge>?n. latestAct_cond ?c ?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> k)

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

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using nAct_not_active_same[of n "\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>" "inf_llist t" c]
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<lbrakk>enat n \<le> enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>; enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t); \<nexists>k. enat n \<le> enat k \<and> enat k < enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<and> \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) k\<^esub>\<rbrakk> \<Longrightarrow> \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>))
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "\<phi> (lnth (\<pi>\<^bsub>c\<^esub>(inf_llist t)) (the_enat(\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)))"
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>))
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "enat (the_enat (\<langle>c #\<^bsub>enat n\<^esub> inf_llist t\<rangle>)) < llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
have "ltake \<infinity> (inf_llist t) = (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltake \<infinity> (inf_llist t) = inf_llist t
[PROOF STEP]
using ltake_all[of "inf_llist t"]
[PROOF STATE]
proof (prove)
using this:
llength (inf_llist t) \<le> ?m \<Longrightarrow> ltake ?m (inf_llist t) = inf_llist t

goal (1 subgoal):
 1. ltake \<infinity> (inf_llist t) = inf_llist t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ltake \<infinity> (inf_llist t) = inf_llist t

goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
hence "llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)) = \<langle>c #\<^bsub>\<infinity>\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
ltake \<infinity> (inf_llist t) = inf_llist t

goal (1 subgoal):
 1. llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using nAct_def
[PROOF STATE]
proof (prove)
using this:
ltake \<infinity> (inf_llist t) = inf_llist t
\<langle>?c #\<^bsub>?n\<^esub>?t\<rangle> \<equiv> llength (\<pi>\<^bsub>?c\<^esub>ltake ?n ?t)

goal (1 subgoal):
 1. llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
have "\<langle>c #\<^bsub>enat n\<^esub> inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
have "\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<ge>n" and "\<parallel>c\<parallel>\<^bsub>t (\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> &&& \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
using nxtActI
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<Longrightarrow> ?n \<le> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<and> \<parallel>?c\<parallel>\<^bsub>?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>\<^esub> \<and> \<not> (\<exists>k\<ge>?n. latestAct_cond ?c ?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> k)

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

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using nAct_less[of "\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>" "inf_llist t" n \<infinity>]
[PROOF STATE]
proof (prove)
using this:
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
\<lbrakk>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t); enat n \<le> enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>; enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < \<infinity>; \<parallel>?c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> \<langle>?c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>?c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
hence "lnth (\<pi>\<^bsub>c\<^esub>(inf_llist t)) (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)) =
    lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using lnth_lappend1[of "the_enat (\<langle>c #\<^bsub>enat n\<^esub> inf_llist t\<rangle>)" "\<pi>\<^bsub>c\<^esub>(inf_llist t)" "inf_llist t'"]
[PROOF STATE]
proof (prove)
using this:
enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<Longrightarrow> lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
have "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (the_enat(\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)))"
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
hence "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)))"
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))

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

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
have "\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<ge>n" and "\<parallel>c\<parallel>\<^bsub>t (\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> &&& \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
using nxtActI
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub> \<Longrightarrow> ?n \<le> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<and> \<parallel>?c\<parallel>\<^bsub>?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>\<^esub> \<and> \<not> (\<exists>k\<ge>?n. latestAct_cond ?c ?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub> k)

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
have "(\<exists>i\<ge>snd (t, n). \<parallel>c\<parallel>\<^bsub>fst (t, n) i\<^esub>) \<and>
    \<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist (fst (t, n)))) @\<^sub>l (inf_llist t'))
    (the_enat (\<langle>c #\<^bsub>the_enat (snd (t,n))\<^esub> inf_llist (fst (t, n))\<rangle>)))"
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (1 subgoal):
 1. (\<exists>i\<ge>snd (t, n). \<parallel>c\<parallel>\<^bsub>fst (t, n) i\<^esub>) \<and> \<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist (fst (t, n)) @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat (the_enat (enat (snd (t, n))))\<^esub>inf_llist (fst (t, n))\<rangle>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>i\<ge>snd (t, n). \<parallel>c\<parallel>\<^bsub>fst (t, n) i\<^esub>) \<and> \<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist (fst (t, n)) @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat (the_enat (enat (snd (t, n))))\<^esub>inf_llist (fst (t, n))\<rangle>))

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>i\<ge>snd (t, n). \<parallel>c\<parallel>\<^bsub>fst (t, n) i\<^esub>) \<and> \<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist (fst (t, n)) @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat (the_enat (enat (snd (t, n))))\<^esub>inf_llist (fst (t, n))\<rangle>))

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
using ba_def
[PROOF STATE]
proof (prove)
using this:
(\<exists>i\<ge>snd (t, n). \<parallel>c\<parallel>\<^bsub>fst (t, n) i\<^esub>) \<and> \<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist (fst (t, n)) @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat (the_enat (enat (snd (t, n))))\<^esub>inf_llist (fst (t, n))\<rangle>))
[?\<phi>]\<^sub>b \<equiv> \<lambda>t n. ?\<phi> (t n)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma baIN1[intro]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
  assumes act: "\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and nAct: "\<nexists>i. i\<ge>n \<and> \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and al: "\<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))"
  shows "eval c t t' n (ba \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "t' (n - \<langle>c \<and> t\<rangle> - 1) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t' (n - \<langle>c \<and> t\<rangle> - 1) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t' (n - \<langle>c \<and> t\<rangle> - 1) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t' (n - \<langle>c \<and> t\<rangle> - 1) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "\<dots> = lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
using act nAct cnf2bhv_lnth_lappend
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<lbrakk>\<exists>i. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub>)\<rbrakk> \<Longrightarrow> lnth (\<pi>\<^bsub>?c\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t') (\<^bsub>?c\<^esub>\<down>\<^bsub>?t\<^esub>?n) = lnth (inf_llist ?t') (?n - \<langle>?c \<and> ?t\<rangle> - 1)

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t' (n - \<langle>c \<and> t\<rangle> - 1) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)
lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
have "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)))"
[PROOF STATE]
proof (prove)
using this:
t' (n - \<langle>c \<and> t\<rangle> - 1) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)
lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. \<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))
[PROOF STEP]
using al
[PROOF STATE]
proof (prove)
using this:
t' (n - \<langle>c \<and> t\<rangle> - 1) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)
lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n)
\<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))

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

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
using ba_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))
[?\<phi>]\<^sub>b \<equiv> \<lambda>t n. ?\<phi> (t n)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma baIN2[intro]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
  assumes nAct: "\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and al: "\<phi> (t' n)"
  shows "eval c t t' n (ba \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "t' n = lnth (inf_llist t') n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t' n = lnth (inf_llist t') n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t' n = lnth (inf_llist t') n

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t' n = lnth (inf_llist t') n

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "\<dots> = lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lnth (inf_llist t') n = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lnth (inf_llist t') n = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n
[PROOF STEP]
from nAct
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<pi>\<^bsub>c\<^esub>(inf_llist t) = []\<^sub>l"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

goal (1 subgoal):
 1. lnth (inf_llist t') n = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n
[PROOF STEP]
hence "(\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t') = inf_llist t'"
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^bsub>c\<^esub>inf_llist t = []\<^sub>l

goal (1 subgoal):
 1. \<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t' = inf_llist t'
[PROOF STEP]
by (simp add: \<open>\<pi>\<^bsub>c\<^esub>inf_llist t = []\<^sub>l\<close>)
[PROOF STATE]
proof (state)
this:
\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t' = inf_llist t'

goal (1 subgoal):
 1. lnth (inf_llist t') n = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t' = inf_llist t'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lnth (inf_llist t') n = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t' n = lnth (inf_llist t') n
lnth (inf_llist t') n = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n
[PROOF STEP]
have "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) n)"
[PROOF STATE]
proof (prove)
using this:
t' n = lnth (inf_llist t') n
lnth (inf_llist t') n = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n

goal (1 subgoal):
 1. \<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n)
[PROOF STEP]
using al
[PROOF STATE]
proof (prove)
using this:
t' n = lnth (inf_llist t') n
lnth (inf_llist t') n = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n
\<phi> (t' n)

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
hence "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) n)"
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n)

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

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
with nAct
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n)

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
using ba_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n)
[?\<phi>]\<^sub>b \<equiv> \<lambda>t n. ?\<phi> (t n)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma baIANow[intro]:
  fixes t n c \<phi>
  assumes "\<phi> (\<sigma>\<^bsub>c\<^esub>(t n))"
    and "\<parallel>c\<parallel>\<^bsub>t n\<^esub>"
  shows "eval c t t' n (ba \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t n)
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
have "\<phi>(\<sigma>\<^bsub>c\<^esub>(t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>))"
[PROOF STATE]
proof (prove)
using this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t n)
\<parallel>c\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
using nxtAct_active
[PROOF STATE]
proof (prove)
using this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t n)
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
\<parallel>?c\<parallel>\<^bsub>?t ?i\<^esub> \<Longrightarrow> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?i\<^esub> = ?i

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t n)
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t n)
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
using baIA
[PROOF STATE]
proof (prove)
using this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t n)
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub>; ?\<phi> (\<sigma>\<^bsub>?c\<^esub>?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>)\<rbrakk> \<Longrightarrow> eval ?c ?t ?t' ?n [?\<phi>]\<^sub>b

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma baEA[elim]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
    and i::nat
  assumes "\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and "eval c t t' n (ba \<phi>)"
  shows "\<phi> (\<sigma>\<^bsub>c\<^esub>(t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
from \<open>eval c t t' n (ba \<phi>)\<close>
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "eval c t t' n (\<lambda> t n. \<phi> (t n))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n [\<phi>]\<^sub>b

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

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

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval c t t' n (\<lambda>t n. \<phi> (t n))

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<ge>n" and "\<parallel>c\<parallel>\<^bsub>t (\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n [\<phi>]\<^sub>b

goal (1 subgoal):
 1. n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> &&& \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
using nxtActI[of n c t]
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n [\<phi>]\<^sub>b
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<and> \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> \<and> \<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

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

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n (\<lambda>t n. \<phi> (t n))
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
have "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n (\<lambda>t n. \<phi> (t n))
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

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

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

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
hence "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)))"
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))

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

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

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
have "enat (the_enat (\<langle>c #\<^bsub>enat n\<^esub> inf_llist t\<rangle>)) < llength (\<pi>\<^bsub>c\<^esub>(inf_llist t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
have "ltake \<infinity> (inf_llist t) = (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltake \<infinity> (inf_llist t) = inf_llist t
[PROOF STEP]
using ltake_all[of "inf_llist t"]
[PROOF STATE]
proof (prove)
using this:
llength (inf_llist t) \<le> ?m \<Longrightarrow> ltake ?m (inf_llist t) = inf_llist t

goal (1 subgoal):
 1. ltake \<infinity> (inf_llist t) = inf_llist t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ltake \<infinity> (inf_llist t) = inf_llist t

goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
hence "llength (\<pi>\<^bsub>c\<^esub>(inf_llist t)) = \<langle>c #\<^bsub>\<infinity>\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
using this:
ltake \<infinity> (inf_llist t) = inf_llist t

goal (1 subgoal):
 1. llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using nAct_def
[PROOF STATE]
proof (prove)
using this:
ltake \<infinity> (inf_llist t) = inf_llist t
\<langle>?c #\<^bsub>?n\<^esub>?t\<rangle> \<equiv> llength (\<pi>\<^bsub>?c\<^esub>ltake ?n ?t)

goal (1 subgoal):
 1. llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
have "\<langle>c #\<^bsub>enat n\<^esub> inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
with \<open>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<ge>n\<close> \<open>\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using nAct_less
[PROOF STATE]
proof (prove)
using this:
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> < llength (inf_llist t)
\<lbrakk>enat ?k < llength ?t; ?n \<le> enat ?k; enat ?k < ?n'; \<parallel>?c\<parallel>\<^bsub>lnth ?t ?k\<^esub>\<rbrakk> \<Longrightarrow> \<langle>?c #\<^bsub>?n\<^esub>?t\<rangle> < \<langle>?c #\<^bsub>?n'\<^esub>?t\<rangle>

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
llength (\<pi>\<^bsub>c\<^esub>inf_llist t) = \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> < \<langle>c #\<^bsub>\<infinity>\<^esub>inf_llist t\<rangle>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
hence "lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)) =
    lnth (\<pi>\<^bsub>c\<^esub>(inf_llist t)) (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)

goal (1 subgoal):
 1. lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using lnth_lappend1[of "the_enat (\<langle>c #\<^bsub>enat n\<^esub> inf_llist t\<rangle>)" "\<pi>\<^bsub>c\<^esub>(inf_llist t)" "inf_llist t'"]
[PROOF STATE]
proof (prove)
using this:
enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t)
enat (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) < llength (\<pi>\<^bsub>c\<^esub>inf_llist t) \<Longrightarrow> lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

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

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
have "\<phi> (lnth (\<pi>\<^bsub>c\<^esub>(inf_llist t)) (the_enat (\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle>)))"
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

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

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
have "\<langle>c #\<^bsub>n\<^esub> inf_llist t\<rangle> = \<langle>c #\<^bsub>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> inf_llist t\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "\<nexists>k. n\<le>k \<and> k<\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<and> \<parallel>c\<parallel>\<^bsub>t k\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n [\<phi>]\<^sub>b

goal (1 subgoal):
 1. \<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
[PROOF STEP]
using nxtActI[of n c t]
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
eval c t t' n [\<phi>]\<^sub>b
\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<and> \<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> \<and> \<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

goal (1 subgoal):
 1. \<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
hence "\<not> (\<exists>k\<ge>n. k < \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<and> \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) k\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>k\<ge>n. latestAct_cond c t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

goal (1 subgoal):
 1. \<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
have "enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)
[PROOF STEP]
by (simp add: one_enat_def)
[PROOF STATE]
proof (state)
this:
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
using \<open>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<ge>n\<close> nAct_not_active_same
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>k\<ge>n. latestAct_cond c (lnth (inf_llist t)) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> k)
enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> - 1 < llength (inf_llist t)
n \<le> \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>
\<lbrakk>enat ?n \<le> ?n'; ?n' - 1 < llength ?t; \<nexists>k. enat ?n \<le> enat k \<and> enat k < ?n' \<and> \<parallel>?c\<parallel>\<^bsub>lnth ?t k\<^esub>\<rbrakk> \<Longrightarrow> \<langle>?c #\<^bsub>?n'\<^esub>?t\<rangle> = \<langle>?c #\<^bsub>enat ?n\<^esub>?t\<rangle>

goal (1 subgoal):
 1. \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
have "\<sigma>\<^bsub>c\<^esub>(t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>) = lnth (\<pi>\<^bsub>c\<^esub>(inf_llist t)) (the_enat (\<langle>c #\<^bsub>\<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
have "enat (Suc i) < llength (inf_llist t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (Suc i) < llength (inf_llist t)
[PROOF STEP]
using enat_ord_code
[PROOF STATE]
proof (prove)
using this:
(enat ?m \<le> enat ?n) = (?m \<le> ?n)
(enat ?m < enat ?n) = (?m < ?n)
(?q \<le> \<infinity>) = True
(enat ?m < \<infinity>) = True
(\<infinity> \<le> enat ?n) = False
(\<infinity> < ?q) = False

goal (1 subgoal):
 1. enat (Suc i) < llength (inf_llist t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat (Suc i) < llength (inf_llist t)

goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enat (Suc i) < llength (inf_llist t)

goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
from \<open>\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
have "\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<parallel>c\<parallel>\<^bsub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (1 subgoal):
 1. \<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enat (Suc i) < llength (inf_llist t)
\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
enat (Suc i) < llength (inf_llist t)
\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>

goal (1 subgoal):
 1. \<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using proj_active_nth
[PROOF STATE]
proof (prove)
using this:
enat (Suc i) < llength (inf_llist t)
\<parallel>c\<parallel>\<^bsub>lnth (inf_llist t) \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>
\<lbrakk>enat (Suc ?i) < llength ?t; \<parallel>?c\<parallel>\<^bsub>lnth ?t ?i\<^esub>\<rbrakk> \<Longrightarrow> lnth (\<pi>\<^bsub>?c\<^esub>?t) (the_enat \<langle>?c #\<^bsub>enat ?i\<^esub>?t\<rangle>) = \<sigma>\<^bsub>?c\<^esub>lnth ?t ?i

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle>))
\<langle>c #\<^bsub>enat n\<^esub>inf_llist t\<rangle> = \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>
\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = lnth (\<pi>\<^bsub>c\<^esub>inf_llist t) (the_enat \<langle>c #\<^bsub>enat \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma baEN1[elim]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
  assumes act: "\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and nAct: "\<nexists>i. i\<ge>n \<and> \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and al: "eval c t t' n (ba \<phi>)"
  shows "\<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))
[PROOF STEP]
from al
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n [\<phi>]\<^sub>b

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

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

goal (1 subgoal):
 1. \<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))
[PROOF STEP]
hence "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)))"
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))

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

goal (1 subgoal):
 1. \<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))

goal (1 subgoal):
 1. \<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))
[PROOF STEP]
have "lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>(n)) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)
[PROOF STEP]
using act nAct cnf2bhv_lnth_lappend
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>c\<parallel>\<^bsub>t i\<^esub>)
\<lbrakk>\<exists>i. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub>)\<rbrakk> \<Longrightarrow> lnth (\<pi>\<^bsub>?c\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t') (\<^bsub>?c\<^esub>\<down>\<^bsub>?t\<^esub>?n) = lnth (inf_llist ?t') (?n - \<langle>?c \<and> ?t\<rangle> - 1)

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

goal (1 subgoal):
 1. \<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)

goal (1 subgoal):
 1. \<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))
[PROOF STEP]
have "\<dots> = t' (n - \<langle>c \<and> t\<rangle> - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1) = t' (n - \<langle>c \<and> t\<rangle> - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1) = t' (n - \<langle>c \<and> t\<rangle> - 1)

goal (1 subgoal):
 1. \<phi> (t' (n - \<langle>c \<and> t\<rangle> - 1))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)
lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1) = t' (n - \<langle>c \<and> t\<rangle> - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n))
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') (\<^bsub>c\<^esub>\<down>\<^bsub>t\<^esub>n) = lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1)
lnth (inf_llist t') (n - \<langle>c \<and> t\<rangle> - 1) = t' (n - \<langle>c \<and> t\<rangle> - 1)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma baEN2[elim]:
  fixes c::'id
    and t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
  assumes nAct: "\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>"
    and al: "eval c t t' n (ba \<phi>)"
  shows "\<phi> (t' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (t' n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (t' n)
[PROOF STEP]
from al
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n [\<phi>]\<^sub>b
[PROOF STEP]
have "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) n)"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n [\<phi>]\<^sub>b

goal (1 subgoal):
 1. \<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n)
[PROOF STEP]
using nAct validCE_not_act ba_def
[PROOF STATE]
proof (prove)
using this:
eval c t t' n [\<phi>]\<^sub>b
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n ?\<gamma>\<rbrakk> \<Longrightarrow> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n
[?\<phi>]\<^sub>b \<equiv> \<lambda>t n. ?\<phi> (t n)

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

goal (1 subgoal):
 1. \<phi> (t' n)
[PROOF STEP]
hence "\<phi> (lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) n)"
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n)

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

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

goal (1 subgoal):
 1. \<phi> (t' n)
[PROOF STEP]
have "lnth ((\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t')) n = lnth (inf_llist t') n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n = lnth (inf_llist t') n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n = lnth (inf_llist t') n
[PROOF STEP]
from nAct
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<pi>\<^bsub>c\<^esub>(inf_llist t) = []\<^sub>l"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>c\<parallel>\<^bsub>t i\<^esub>

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

goal (1 subgoal):
 1. lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n = lnth (inf_llist t') n
[PROOF STEP]
hence "(\<pi>\<^bsub>c\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t') = inf_llist t'"
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^bsub>c\<^esub>inf_llist t = []\<^sub>l

goal (1 subgoal):
 1. \<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t' = inf_llist t'
[PROOF STEP]
by (simp add: \<open>\<pi>\<^bsub>c\<^esub>inf_llist t = []\<^sub>l\<close>)
[PROOF STATE]
proof (state)
this:
\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t' = inf_llist t'

goal (1 subgoal):
 1. lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n = lnth (inf_llist t') n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t' = inf_llist t'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n = lnth (inf_llist t') n

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

goal (1 subgoal):
 1. \<phi> (t' n)
[PROOF STEP]
have "\<dots> = t' n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lnth (inf_llist t') n = t' n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lnth (inf_llist t') n = t' n

goal (1 subgoal):
 1. \<phi> (t' n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n)
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n = lnth (inf_llist t') n
lnth (inf_llist t') n = t' n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n)
lnth (\<pi>\<^bsub>c\<^esub>inf_llist t @\<^sub>l inf_llist t') n = lnth (inf_llist t') n
lnth (inf_llist t') n = t' n

goal (1 subgoal):
 1. \<phi> (t' n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (t' n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma baEANow[elim]:
  fixes t n c \<phi>
  assumes "eval c t t' n (ba \<phi>)"
    and "\<parallel>c\<parallel>\<^bsub>t n\<^esub>"
  shows "\<phi> (\<sigma>\<^bsub>c\<^esub>(t n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t n)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n [\<phi>]\<^sub>b
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
have "\<phi>(\<sigma>\<^bsub>c\<^esub>(t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>))"
[PROOF STATE]
proof (prove)
using this:
eval c t t' n [\<phi>]\<^sub>b
\<parallel>c\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
using baEA
[PROOF STATE]
proof (prove)
using this:
eval c t t' n [\<phi>]\<^sub>b
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub>; eval ?c ?t ?t' ?n [?\<phi>]\<^sub>b\<rbrakk> \<Longrightarrow> ?\<phi> (\<sigma>\<^bsub>?c\<^esub>?t \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?n\<^esub>)

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

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t n)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eval c t t' n [\<phi>]\<^sub>b
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval c t t' n [\<phi>]\<^sub>b
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>c\<^esub>t n)
[PROOF STEP]
using nxtAct_active
[PROOF STATE]
proof (prove)
using this:
eval c t t' n [\<phi>]\<^sub>b
\<parallel>c\<parallel>\<^bsub>t n\<^esub>
\<phi> (\<sigma>\<^bsub>c\<^esub>t \<langle>c \<rightarrow> t\<rangle>\<^bsub>n\<^esub>)
\<parallel>?c\<parallel>\<^bsub>?t ?i\<^esub> \<Longrightarrow> \<langle>?c \<rightarrow> ?t\<rangle>\<^bsub>?i\<^esub> = ?i

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

goal:
No subgoals!
[PROOF STEP]
qed