# Theory Dynamic_Architecture_Calculus

(*
Title:      Dynamic_Architecture_Calculus
Author:     Diego Marmsoler
*)
section "A Calculus for Dynamic Architectures"
text ‹
The following theory formalizes our calculus for dynamic architectures~\<^cite>‹"Marmsoler2017b" and "Marmsoler2017c"› and verifies its soundness.
The calculus allows to reason about temporal-logic specifications of component behavior in a dynamic setting.
The theory is based on our theory of configuration traces and introduces the notion of behavior trace assertion to specify component behavior in a dynamic setting.
›
theory Dynamic_Architecture_Calculus
imports Configuration_Traces
begin

subsection "Extended Natural Numbers"
text ‹
We first provide one additional property for extended natural numbers.
›

lemma the_enat_mono[simp]:
assumes "m ≠ ∞"
and "n ≤ m"
shows "the_enat n ≤ the_enat m"
using assms(1) assms(2) enat_ile by fastforce

subsection "Lazy Lists"
text ‹
Finally, we provide an additional property for lazy lists.
›

lemma llength_geq_enat_lfiniteD: "llength xs ≤ enat n ⟹ lfinite xs"
using not_lfinite_llength by force

context dynamic_component
begin

subsection "Dynamic Evaluation of Temporal Operators"
text ‹
In the following we introduce a function to evaluate a behavior trace assertion over a given configuration trace.
›
type_synonym 'c bta = "(nat ⇒ 'c) ⇒ nat ⇒ bool"

definition eval:: "'id ⇒ (nat ⇒ cnf) ⇒ (nat ⇒ 'cmp) ⇒ nat
⇒ 'cmp bta ⇒ bool"
where "eval cid t t' n γ ≡
(∃i≥n. ∥cid∥⇘t i⇙) ∧ γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat(⟨cid #⇘n⇙ inf_llist t⟩)) ∨
(∃i. ∥cid∥⇘t i⇙) ∧ (∄i'. i'≥n ∧ ∥cid∥⇘t i'⇙) ∧ γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘cid⇙↓⇘t⇙(n)) ∨
(∄i. ∥cid∥⇘t i⇙) ∧ γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) n"
text ‹
@{const eval} takes a component identifier @{term cid}, a configuration trace @{term t}, a behavior trace @{term t'}, and point in time @{term n} and evaluates behavior trace assertion @{term γ} as follows:
\begin{itemize}
\item If component @{term cid} is again activated in the future, @{term γ} is evaluated at the next point in time where @{term cid} is active in @{term t}.
\item If component @{term cid} is not again activated in the future but it is activated at least once in @{term t}, then @{term γ} is evaluated at the point in time given by @{term "(⇘cid⇙↓⇘t⇙(n))"}.
\item If component @{term cid} is never active in @{term t}, then @{term γ} is evaluated at time point @{term n}.
\end{itemize}
›

text ‹
The following proposition evaluates definition @{const eval} by showing that a behavior trace assertion @{term γ} holds over configuration trace @{term t} and continuation @{term t'} whenever it holds for the concatenation of the corresponding projection with @{term t'}.
›
proposition eval_corr:
"eval cid t t' 0 γ ⟷ γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) 0"
proof
assume "eval cid t t' 0 γ"
with eval_def have "(∃i≥0. ∥cid∥⇘t i⇙) ∧
γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat 0⇙inf_llist t⟩) ∨
(∃i. ∥cid∥⇘t i⇙) ∧ ¬ (∃i'≥0. ∥cid∥⇘t i'⇙) ∧ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙0) ∨
(∄i. ∥cid∥⇘t i⇙) ∧ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) 0" by simp
thus "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) 0"
proof
assume "(∃i≥0. ∥cid∥⇘t i⇙) ∧ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat 0⇙inf_llist t⟩)"
moreover have "the_enat ⟨cid #⇘enat 0⇙inf_llist t⟩ = 0" using zero_enat_def by auto
ultimately show ?thesis by simp
next
assume "(∃i. ∥cid∥⇘t i⇙) ∧ ¬ (∃i'≥0. ∥cid∥⇘t i'⇙) ∧ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙0) ∨
(∄i. ∥cid∥⇘t i⇙) ∧ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) 0"
thus ?thesis by auto
qed
next
assume "γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) 0"
show "eval cid t t' 0 γ"
proof cases
assume "∃i. ∥cid∥⇘t i⇙"
hence "∃i≥0. ∥cid∥⇘t i⇙" by simp
moreover from ‹γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) 0› have
"γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat(⟨cid #⇘enat 0⇙ inf_llist t⟩))"
using zero_enat_def by auto
ultimately show ?thesis using eval_def by simp
next
assume "∄i. ∥cid∥⇘t i⇙"
with ‹γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) 0› show ?thesis using eval_def by simp
qed
qed

subsubsection "Simplification Rules"

lemma validCI_act[simp]:
assumes "∃i≥n. ∥cid∥⇘t i⇙"
and "γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat(⟨cid #⇘n⇙ inf_llist t⟩))"
shows "eval cid t t' n γ"
using assms eval_def by simp

lemma validCI_cont[simp]:
assumes "∃i. ∥cid∥⇘t i⇙"
and "∄i'. i'≥n ∧ ∥cid∥⇘t i'⇙"
and "γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘cid⇙↓⇘t⇙(n))"
shows "eval cid t t' n γ"
using assms eval_def by simp

lemma validCI_not_act[simp]:
assumes "∄i. ∥cid∥⇘t i⇙"
and "γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) n"
shows "eval cid t t' n γ"
using assms eval_def by simp

lemma validCE_act[simp]:
assumes "∃i≥n. ∥cid∥⇘t i⇙"
and "eval cid t t' n γ"
shows "γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat(⟨cid #⇘n⇙ inf_llist t⟩))"
using assms eval_def by auto

lemma validCE_cont[simp]:
assumes "∃i. ∥cid∥⇘t i⇙"
and "∄i'. i'≥n ∧ ∥cid∥⇘t i'⇙"
and "eval cid t t' n γ"
shows "γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘cid⇙↓⇘t⇙(n))"
using assms eval_def by auto

lemma validCE_not_act[simp]:
assumes "∄i. ∥cid∥⇘t i⇙"
and "eval cid t t' n γ"
shows "γ (lnth ((π⇘cid⇙(inf_llist t)) @⇩l (inf_llist t'))) n"
using assms eval_def by auto

subsubsection "No Activations"

proposition validity1:
assumes "n≤n'"
and "∃i≥n'. ∥c∥⇘t i⇙"
and "∀k≥n. k<n' ⟶ ¬ ∥c∥⇘t k⇙"
shows "eval c t t' n γ ⟹ eval c t t' n' γ"
proof -
assume "eval c t t' n γ"
moreover from assms have "∃i≥n. ∥c∥⇘t i⇙" by (meson order.trans)
ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘enat n⇙ inf_llist t⟩))"
using validCE_act by blast
moreover have "enat n' - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
with assms have "the_enat (⟨c #⇘enat n⇙ inf_llist t⟩) = the_enat (⟨c #⇘enat n'⇙ inf_llist t⟩)"
using nAct_not_active_same[of n n' "inf_llist t" c] by simp
ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘enat n'⇙ inf_llist t⟩))"
by simp
with assms show ?thesis using validCI_act by blast
qed

proposition validity2:
assumes "n≤n'"
and "∃i≥n'. ∥c∥⇘t i⇙"
and "∀k≥n. k<n' ⟶ ¬ ∥c∥⇘t k⇙"
shows "eval c t t' n' γ ⟹ eval c t t' n γ"
proof -
assume "eval c t t' n' γ"
with ‹∃i≥n'. ∥c∥⇘t i⇙›
have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘enat n'⇙ inf_llist t⟩))"
using validCE_act by blast
moreover have "enat n' - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
with assms have "the_enat (⟨c #⇘enat n⇙ inf_llist t⟩) = the_enat (⟨c #⇘enat n'⇙ inf_llist t⟩)"
using nAct_not_active_same by simp
ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘enat n⇙ inf_llist t⟩))"
by simp
moreover from assms have "∃i≥n. ∥c∥⇘t i⇙" by (meson order.trans)
ultimately show ?thesis using validCI_act by blast
qed

subsection "Specification Operators"
text ‹
In the following we introduce some basic operators for behavior trace assertions.
›

subsubsection "Predicates"
text ‹
Every predicate can be transformed to a behavior trace assertion.
›

definition pred :: "bool ⇒ ('cmp bta)"
where "pred P ≡ λ t n. P"

lemma predI[intro]:
fixes cid t t' n P
assumes "P"
shows "eval cid t t' n (pred P)"
proof cases
assume "(∃i. ∥cid∥⇘t i⇙)"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
with assms show ?thesis using eval_def pred_def by auto
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
with assms show ?thesis using eval_def pred_def by auto
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
with assms show ?thesis using eval_def pred_def by auto
qed

lemma predE[elim]:
fixes cid t t' n P
assumes "eval cid t t' n (pred P)"
shows "P"
proof cases
assume "(∃i. ∥cid∥⇘t i⇙)"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
with assms show ?thesis using eval_def pred_def by auto
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
with assms show ?thesis using eval_def pred_def by auto
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
with assms show ?thesis using eval_def pred_def by auto
qed

subsubsection "True and False"

abbreviation true :: "'cmp bta"
where "true ≡ λt n. HOL.True"

abbreviation false :: "'cmp bta"
where "false ≡ λt n. HOL.False"

subsubsection "Implication"

definition imp :: "('cmp bta) ⇒ ('cmp bta) ⇒ ('cmp bta)" (infixl "⟶⇧b" 10)
where "γ ⟶⇧b γ' ≡ λ t n. γ t n ⟶ γ' t n"

lemma impI[intro!]:
assumes "eval cid t t' n γ ⟶ eval cid t t' n γ'"
shows "eval cid t t' n (γ ⟶⇧b γ')"
proof cases
assume "∃i. ∥cid∥⇘t i⇙"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
with ‹eval cid t t' n γ ⟶ eval cid t t' n γ'›
have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)
⟶ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using eval_def by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› have "eval cid t t' n (λt n. γ t n ⟶ γ' t n)"
using validCI_act[where γ="λ t n. γ t n ⟶ γ' t n"] by blast
thus ?thesis using imp_def by simp
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
with ‹∃i. ∥cid∥⇘t i⇙› ‹eval cid t t' n γ ⟶ eval cid t t' n γ'›
have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)
⟶ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)" using eval_def by blast
with ‹∃i. ∥cid∥⇘t i⇙› ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. γ t n ⟶ γ' t n)"
using validCI_cont[where γ="λ t n. γ t n ⟶ γ' t n"] by blast
thus ?thesis using imp_def by simp
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
with ‹eval cid t t' n γ ⟶ eval cid t t' n γ'›
have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n ⟶ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n"
using eval_def by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. γ t n ⟶ γ' t n)"
using validCI_not_act[where γ="λ t n. γ t n ⟶ γ' t n"] by blast
thus ?thesis using imp_def by simp
qed

lemma impE[elim!]:
assumes "eval cid t t' n (γ ⟶⇧b γ')"
shows "eval cid t t' n γ ⟶ eval cid t t' n γ'"
proof cases
assume "(∃i. ∥cid∥⇘t i⇙)"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
moreover from ‹eval cid t t' n (γ ⟶⇧b γ')› have "eval cid t t' n (λt n. γ t n ⟶ γ' t n)"
using imp_def by simp
ultimately have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)
⟶ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using validCE_act[where γ="λ t n. γ t n ⟶ γ' t n"] by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (γ ⟶⇧b γ')› have "eval cid t t' n (λt n. γ t n ⟶ γ' t n)"
using imp_def by simp
ultimately have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)
⟶ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)"
using validCE_cont[where γ="λ t n. γ t n ⟶ γ' t n"] ‹∃i. ∥cid∥⇘t i⇙› by blast
with ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› ‹∃i. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (γ ⟶⇧b γ')› have "eval cid t t' n (λt n. γ t n ⟶ γ' t n)"
using imp_def by simp
ultimately have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n
⟶ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n"
using validCE_not_act[where γ="λ t n. γ t n ⟶ γ' t n"] by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› show ?thesis using eval_def by blast
qed

subsubsection "Disjunction"

definition disj :: "('cmp bta) ⇒ ('cmp bta) ⇒ ('cmp bta)" (infixl "∨⇧b" 15)
where "γ ∨⇧b γ' ≡ λ t n. γ t n ∨ γ' t n"

lemma disjI[intro!]:
assumes "eval cid t t' n γ ∨ eval cid t t' n γ'"
shows "eval cid t t' n (γ ∨⇧b γ')"
using assms disj_def eval_def by auto

lemma disjE[elim!]:
assumes "eval cid t t' n (γ ∨⇧b γ')"
shows "eval cid t t' n γ ∨ eval cid t t' n γ'"
proof cases
assume "(∃i. ∥cid∥⇘t i⇙)"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
moreover from ‹eval cid t t' n (γ ∨⇧b γ')› have "eval cid t t' n (λt n. γ t n ∨ γ' t n)"
using disj_def by simp
ultimately have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)
∨ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using validCE_act[where γ="λ t n. γ t n ∨ γ' t n"] by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› show ?thesis
using validCI_act[of n cid t γ t'] validCI_act[of n cid t γ' t'] by blast
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (γ ∨⇧b γ')› have "eval cid t t' n (λt n. γ t n ∨ γ' t n)"
using disj_def by simp
ultimately have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)
∨ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)"
using validCE_cont[where γ="λ t n. γ t n ∨ γ' t n"] ‹∃i. ∥cid∥⇘t i⇙› by blast
with ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› ‹∃i. ∥cid∥⇘t i⇙› show ?thesis
using validCI_cont[of cid t n γ t'] validCI_cont[of cid t n γ' t'] by blast
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (γ ∨⇧b γ')› have "eval cid t t' n (λt n. γ t n ∨ γ' t n)"
using disj_def by simp
ultimately have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n
∨ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n"
using validCE_not_act[where γ="λ t n. γ t n ∨ γ' t n"] by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› show ?thesis
using validCI_not_act[of cid t γ t' n] validCI_not_act[of cid t γ' t' n] by blast
qed

subsubsection "Conjunction"

definition conj :: "('cmp bta) ⇒ ('cmp bta) ⇒ ('cmp bta)" (infixl "∧⇧b" 20)
where "γ ∧⇧b γ' ≡ λ t n. γ t n ∧ γ' t n"

lemma conjI[intro!]:
assumes "eval cid t t' n γ ∧ eval cid t t' n γ'"
shows "eval cid t t' n (γ ∧⇧b γ')"
proof cases
assume "∃i. ∥cid∥⇘t i⇙"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
with ‹eval cid t t' n γ ∧ eval cid t t' n γ'›
have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)
∧ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using eval_def by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› have "eval cid t t' n (λt n. γ t n ∧ γ' t n)"
using validCI_act[where γ="λ t n. γ t n ∧ γ' t n"] by blast
thus ?thesis using conj_def by simp
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
with ‹∃i. ∥cid∥⇘t i⇙› ‹eval cid t t' n γ ∧ eval cid t t' n γ'›
have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)
∧ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)" using eval_def by blast
with ‹∃i. ∥cid∥⇘t i⇙› ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. γ t n ∧ γ' t n)"
using validCI_cont[where γ="λ t n. γ t n ∧ γ' t n"] by blast
thus ?thesis using conj_def by simp
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
with ‹eval cid t t' n γ ∧ eval cid t t' n γ'› have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n
∧ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n" using eval_def by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. γ t n ∧ γ' t n)"
using validCI_not_act[where γ="λ t n. γ t n ∧ γ' t n"] by blast
thus ?thesis using conj_def by simp
qed

lemma conjE[elim!]:
assumes "eval cid t t' n (γ ∧⇧b γ')"
shows "eval cid t t' n γ ∧ eval cid t t' n γ'"
proof cases
assume "(∃i. ∥cid∥⇘t i⇙)"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
moreover from ‹eval cid t t' n (γ ∧⇧b γ')› have "eval cid t t' n (λt n. γ t n ∧ γ' t n)"
using conj_def by simp
ultimately have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)
∧ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using validCE_act[where γ="λ t n. γ t n ∧ γ' t n"] by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (γ ∧⇧b γ')› have "eval cid t t' n (λt n. γ t n ∧ γ' t n)"
using conj_def by simp
ultimately have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)
∧ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)"
using validCE_cont[where γ="λ t n. γ t n ∧ γ' t n"] ‹∃i. ∥cid∥⇘t i⇙› by blast
with ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› ‹∃i. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (γ ∧⇧b γ')› have "eval cid t t' n (λt n. γ t n ∧ γ' t n)"
using conj_def by simp
ultimately have "γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n ∧ γ' (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n"
using validCE_not_act[where γ="λ t n. γ t n ∧ γ' t n"] by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› show ?thesis using eval_def by blast
qed

subsubsection "Negation"

definition neg :: "('cmp bta) ⇒ ('cmp bta)" ("¬⇧b _" [19] 19)
where "¬⇧b γ ≡ λ t n. ¬ γ t n"

lemma negI[intro!]:
assumes "¬ eval cid t t' n γ"
shows "eval cid t t' n (¬⇧b γ)"
proof cases
assume "∃i. ∥cid∥⇘t i⇙"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
with ‹¬ eval cid t t' n γ›
have "¬ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using eval_def by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› have "eval cid t t' n (λt n. ¬ γ t n)"
using validCI_act[where γ="λ t n. ¬ γ t n"] by blast
thus ?thesis using neg_def by simp
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
with ‹∃i. ∥cid∥⇘t i⇙› ‹¬ eval cid t t' n γ›
have "¬ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)" using eval_def by blast
with ‹∃i. ∥cid∥⇘t i⇙› ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. ¬ γ t n)"
using validCI_cont[where γ="λ t n. ¬ γ t n"] by blast
thus ?thesis using neg_def by simp
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
with ‹¬ eval cid t t' n γ› have "¬ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n" using eval_def by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. ¬ γ t n)"
using validCI_not_act[where γ="λ t n. ¬ γ t n"] by blast
thus ?thesis using neg_def by simp
qed

lemma negE[elim!]:
assumes "eval cid t t' n (¬⇧b γ)"
shows "¬ eval cid t t' n γ"
proof cases
assume "(∃i. ∥cid∥⇘t i⇙)"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
moreover from ‹eval cid t t' n (¬⇧b γ)› have "eval cid t t' n (λt n. ¬ γ t n)" using neg_def by simp
ultimately have "¬ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using validCE_act[where γ="λ t n. ¬ γ t n"] by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (¬⇧b γ)› have "eval cid t t' n (λt n. ¬ γ t n)" using neg_def by simp
ultimately have "¬ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)"
using validCE_cont[where γ="λ t n. ¬ γ t n"] ‹∃i. ∥cid∥⇘t i⇙› by blast
with ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› ‹∃i. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (¬⇧b γ)› have "eval cid t t' n (λt n. ¬ γ t n)" using neg_def by simp
ultimately have "¬ γ (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n"
using validCE_not_act[where γ="λ t n. ¬ γ t n"] by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› show ?thesis using eval_def by blast
qed

subsubsection "Quantifiers"

definition all :: "('a ⇒ ('cmp bta))
⇒ ('cmp bta)" (binder "∀⇩b" 10)
where "all P ≡ λt n. (∀y. (P y t n))"

lemma allI[intro!]:
assumes "∀p. eval cid t t' n (γ p)"
shows "eval cid t t' n (all (λp. γ p))"
proof cases
assume "∃i. ∥cid∥⇘t i⇙"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
with ‹∀p. eval cid t t' n (γ p)›
have "∀p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using eval_def by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› have "eval cid t t' n (λt n. (∀y. (γ y t n)))"
using validCI_act[where γ="λt n. (∀y. (γ y t n))"] by blast
thus ?thesis using all_def[of γ] by auto
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
with ‹∃i. ∥cid∥⇘t i⇙› ‹∀p. eval cid t t' n (γ p)›
have "∀p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)"
using eval_def by blast
with ‹∃i. ∥cid∥⇘t i⇙› ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. (∀y. (γ y t n)))"
using validCI_cont[where γ="λt n. (∀y. (γ y t n))"] by blast
thus ?thesis using all_def[of γ] by auto
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
with ‹∀p. eval cid t t' n (γ p)› have "∀p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n"
using eval_def by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. (∀y. (γ y t n)))"
using validCI_not_act[where γ="λt n. (∀y. (γ y t n))"] by blast
thus ?thesis using all_def[of γ] by auto
qed

lemma allE[elim!]:
assumes "eval cid t t' n (all (λp. γ p))"
shows "∀p. eval cid t t' n (γ p)"
proof cases
assume "(∃i. ∥cid∥⇘t i⇙)"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
moreover from ‹eval cid t t' n (all (λp. γ p))› have "eval cid t t' n (λt n. (∀y. (γ y t n)))"
using all_def[of γ] by auto
ultimately have "∀p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using validCE_act[where γ="λt n. (∀y. (γ y t n))"] by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (all (λp. γ p))› have "eval cid t t' n (λt n. (∀y. (γ y t n)))"
using all_def[of γ] by auto
ultimately have "∀p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)"
using validCE_cont[where γ="λt n. (∀y. (γ y t n))"] ‹∃i. ∥cid∥⇘t i⇙› by blast
with ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› ‹∃i. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (all (λp. γ p))› have "eval cid t t' n (λt n. (∀y. (γ y t n)))"
using all_def[of γ] by auto
ultimately have "∀p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n"
using validCE_not_act[where γ="λt n. (∀y. (γ y t n))"] by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› show ?thesis using eval_def by blast
qed

definition ex :: "('a ⇒ ('cmp bta))
⇒ ('cmp bta)" (binder "∃⇩b" 10)
where "ex P ≡ λt n. (∃y. (P y t n))"

lemma exI[intro!]:
assumes "∃p. eval cid t t' n (γ p)"
shows "eval cid t t' n (∃⇩bp. γ p)"
proof cases
assume "∃i. ∥cid∥⇘t i⇙"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
with ‹∃p. eval cid t t' n (γ p)›
have "∃p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using eval_def by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› have "eval cid t t' n (λt n. (∃y. (γ y t n)))"
using validCI_act[where γ="λt n. (∃y. (γ y t n))"] by blast
thus ?thesis using ex_def[of γ] by auto
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
with ‹∃i. ∥cid∥⇘t i⇙› ‹∃p. eval cid t t' n (γ p)›
have "∃p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)" using eval_def by blast
with ‹∃i. ∥cid∥⇘t i⇙› ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. (∃y. (γ y t n)))"
using validCI_cont[where γ="λt n. (∃y. (γ y t n))"] by blast
thus ?thesis using ex_def[of γ] by auto
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
with ‹∃p. eval cid t t' n (γ p)› have "∃p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n"
using eval_def by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› have "eval cid t t' n (λt n. (∃y. (γ y t n)))"
using validCI_not_act[where γ="λt n. (∃y. (γ y t n))"] by blast
thus ?thesis using ex_def[of γ] by auto
qed

lemma exE[elim!]:
assumes "eval cid t t' n (∃⇩bp. γ p)"
shows "∃p. eval cid t t' n (γ p)"
proof cases
assume "(∃i. ∥cid∥⇘t i⇙)"
show ?thesis
proof cases
assume "∃i≥n. ∥cid∥⇘t i⇙"
moreover from ‹eval cid t t' n (ex (λp. γ p))› have "eval cid t t' n (λt n. (∃y. (γ y t n)))"
using ex_def[of γ] by auto
ultimately have "∃p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (the_enat ⟨cid #⇘enat n⇙inf_llist t⟩)"
using validCE_act[where γ="λt n. (∃y. (γ y t n))"] by blast
with ‹∃i≥n. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
next
assume "¬ (∃i≥n. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (∃⇩bp. γ p)› have "eval cid t t' n (λt n. (∃y. (γ y t n)))"
using ex_def[of γ] by auto
ultimately have "∃p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) (⇘cid⇙↓⇘t⇙n)"
using validCE_cont[where γ="λt n. (∃y. (γ y t n))"] ‹∃i. ∥cid∥⇘t i⇙› by blast
with ‹¬ (∃i≥n. ∥cid∥⇘t i⇙)› ‹∃i. ∥cid∥⇘t i⇙› show ?thesis using eval_def by blast
qed
next
assume "¬(∃i. ∥cid∥⇘t i⇙)"
moreover from ‹eval cid t t' n (∃⇩bp. γ p)› have "eval cid t t' n (λt n. (∃y. (γ y t n)))"
using ex_def[of γ] by auto
ultimately have "∃p. (γ p) (lnth (π⇘cid⇙inf_llist t @⇩l inf_llist t')) n"
using validCE_not_act[where γ="λt n. (∃y. (γ y t n))"] by blast
with ‹¬(∃i. ∥cid∥⇘t i⇙)› show ?thesis using eval_def by blast
qed

subsubsection "Behavior Assertions"
text ‹
First we provide rules for basic behavior assertions.
›

definition ba :: "('cmp ⇒ bool) ⇒ ('cmp bta)" ("[_]⇩b")
where "ba φ ≡ λ t n. φ (t n)"

lemma baIA[intro]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes "∃i≥n. ∥c∥⇘t i⇙"
and "φ (σ⇘c⇙(t ⟨c → t⟩⇘n⇙))"
shows "eval c t t' n (ba φ)"
proof -
from assms have "φ (σ⇘c⇙(t ⟨c → t⟩⇘n⇙))" by simp
moreover have "σ⇘c⇙(t ⟨c → t⟩⇘n⇙) = lnth (π⇘c⇙(inf_llist t)) (the_enat (⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩))"
proof -
have "enat (Suc ⟨c → t⟩⇘n⇙) < llength (inf_llist t)" using enat_ord_code by simp
moreover from assms have "∥c∥⇘t (⟨c → t⟩⇘n⇙)⇙" using nxtActI by simp
hence "∥c∥⇘lnth (inf_llist t) ⟨c → t⟩⇘n⇙⇙" by simp
ultimately show ?thesis using proj_active_nth by simp
qed
ultimately have "φ (lnth (π⇘c⇙(inf_llist t)) (the_enat(⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩)))" by simp
moreover have "⟨c #⇘n⇙ inf_llist t⟩ = ⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩"
proof -
from assms have "∄k. n≤k ∧ k<⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘t k⇙" using nxtActI by simp
hence "¬ (∃k≥n. k < ⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘lnth (inf_llist t) k⇙)" by simp
moreover have "enat ⟨c → t⟩⇘n⇙ - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
moreover from assms have "⟨c → t⟩⇘n⇙≥n" using nxtActI by simp
ultimately show ?thesis using nAct_not_active_same[of n "⟨c → t⟩⇘n⇙" "inf_llist t" c] by simp
qed
ultimately have "φ (lnth (π⇘c⇙(inf_llist t)) (the_enat(⟨c #⇘n⇙ inf_llist t⟩)))" by simp
moreover have "enat (the_enat (⟨c #⇘enat n⇙ inf_llist t⟩)) < llength (π⇘c⇙(inf_llist t))"
proof -
have "ltake ∞ (inf_llist t) = (inf_llist t)" using ltake_all[of "inf_llist t"] by simp
hence "llength (π⇘c⇙(inf_llist t)) = ⟨c #⇘∞⇙ inf_llist t⟩" using nAct_def by simp
moreover have "⟨c #⇘enat n⇙ inf_llist t⟩ < ⟨c #⇘∞⇙ inf_llist t⟩"
proof -
have "enat ⟨c → t⟩⇘n⇙ < llength (inf_llist t)" by simp
moreover from assms have "⟨c → t⟩⇘n⇙≥n" and "∥c∥⇘t (⟨c → t⟩⇘n⇙)⇙" using nxtActI by auto
ultimately show ?thesis using nAct_less[of "⟨c → t⟩⇘n⇙" "inf_llist t" n ∞] by simp
qed
ultimately show ?thesis by simp
qed
hence "lnth (π⇘c⇙(inf_llist t)) (the_enat (⟨c #⇘n⇙ inf_llist t⟩)) =
lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (the_enat (⟨c #⇘n⇙ inf_llist t⟩))"
using lnth_lappend1[of "the_enat (⟨c #⇘enat n⇙ inf_llist t⟩)" "π⇘c⇙(inf_llist t)" "inf_llist t'"] by simp
ultimately have "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (the_enat(⟨c #⇘n⇙ inf_llist t⟩)))" by simp
hence "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (the_enat (⟨c #⇘n⇙ inf_llist t⟩)))" by simp
moreover from assms have "⟨c → t⟩⇘n⇙≥n" and "∥c∥⇘t (⟨c → t⟩⇘n⇙)⇙" using nxtActI by auto
ultimately have "(∃i≥snd (t, n). ∥c∥⇘fst (t, n) i⇙) ∧
φ (lnth ((π⇘c⇙(inf_llist (fst (t, n)))) @⇩l (inf_llist t'))
(the_enat (⟨c #⇘the_enat (snd (t,n))⇙ inf_llist (fst (t, n))⟩)))" by auto
thus ?thesis using ba_def by simp
qed

lemma baIN1[intro]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes act: "∃i. ∥c∥⇘t i⇙"
and nAct: "∄i. i≥n ∧ ∥c∥⇘t i⇙"
and al: "φ (t' (n - ⟨c ∧ t⟩ - 1))"
shows "eval c t t' n (ba φ)"
proof -
have "t' (n - ⟨c ∧ t⟩ - 1) = lnth (inf_llist t') (n - ⟨c ∧ t⟩ - 1)" by simp
moreover have "… = lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (⇘c⇙↓⇘t⇙(n))"
using act nAct cnf2bhv_lnth_lappend by simp
ultimately have "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (⇘c⇙↓⇘t⇙(n)))" using al by simp
with act nAct show ?thesis using ba_def by simp
qed

lemma baIN2[intro]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes nAct: "∄i. ∥c∥⇘t i⇙"
and al: "φ (t' n)"
shows "eval c t t' n (ba φ)"
proof -
have "t' n = lnth (inf_llist t') n" by simp
moreover have "… = lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) n"
proof -
from nAct have "π⇘c⇙(inf_llist t) = []⇩l" by simp
hence "(π⇘c⇙(inf_llist t)) @⇩l (inf_llist t') = inf_llist t'" by (simp add: ‹π⇘c⇙inf_llist t = []⇩l›)
thus ?thesis by simp
qed
ultimately have "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) n)" using al by simp
hence "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) n)" by simp
with nAct show ?thesis using ba_def by simp
qed

lemma baIANow[intro]:
fixes t n c φ
assumes "φ (σ⇘c⇙(t n))"
and "∥c∥⇘t n⇙"
shows "eval c t t' n (ba φ)"
proof -
from assms have "φ(σ⇘c⇙(t ⟨c → t⟩⇘n⇙))" using nxtAct_active by simp
with assms show ?thesis using baIA by blast
qed

lemma baEA[elim]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
and i::nat
assumes "∃i≥n. ∥c∥⇘t i⇙"
and "eval c t t' n (ba φ)"
shows "φ (σ⇘c⇙(t ⟨c → t⟩⇘n⇙))"
proof -
from ‹eval c t t' n (ba φ)› have "eval c t t' n (λ t n. φ (t n))" using ba_def by simp
moreover from assms have "⟨c → t⟩⇘n⇙≥n" and "∥c∥⇘t (⟨c → t⟩⇘n⇙)⇙" using nxtActI[of n c t] by auto
ultimately have "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (the_enat (⟨c #⇘n⇙ inf_llist t⟩)))"
using validCE_act by blast
hence "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (the_enat (⟨c #⇘n⇙ inf_llist t⟩)))" by simp
moreover have "enat (the_enat (⟨c #⇘enat n⇙ inf_llist t⟩)) < llength (π⇘c⇙(inf_llist t))"
proof -
have "ltake ∞ (inf_llist t) = (inf_llist t)" using ltake_all[of "inf_llist t"] by simp
hence "llength (π⇘c⇙(inf_llist t)) = ⟨c #⇘∞⇙ inf_llist t⟩" using nAct_def by simp
moreover have "⟨c #⇘enat n⇙ inf_llist t⟩ < ⟨c #⇘∞⇙ inf_llist t⟩"
proof -
have "enat ⟨c → t⟩⇘n⇙ < llength (inf_llist t)" by simp
with ‹⟨c → t⟩⇘n⇙≥n› ‹∥c∥⇘t ⟨c → t⟩⇘n⇙⇙› show ?thesis using nAct_less by simp
qed
ultimately show ?thesis by simp
qed
hence "lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (the_enat (⟨c #⇘n⇙ inf_llist t⟩)) =
lnth (π⇘c⇙(inf_llist t)) (the_enat (⟨c #⇘n⇙ inf_llist t⟩))"
using lnth_lappend1[of "the_enat (⟨c #⇘enat n⇙ inf_llist t⟩)" "π⇘c⇙(inf_llist t)" "inf_llist t'"] by simp
ultimately have "φ (lnth (π⇘c⇙(inf_llist t)) (the_enat (⟨c #⇘n⇙ inf_llist t⟩)))" by simp
moreover have "⟨c #⇘n⇙ inf_llist t⟩ = ⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩"
proof -
from assms have "∄k. n≤k ∧ k<⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘t k⇙" using nxtActI[of n c t] by auto
hence "¬ (∃k≥n. k < ⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘lnth (inf_llist t) k⇙)" by simp
moreover have "enat ⟨c → t⟩⇘n⇙ - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
ultimately show ?thesis using ‹⟨c → t⟩⇘n⇙≥n› nAct_not_active_same by simp
qed
moreover have "σ⇘c⇙(t ⟨c → t⟩⇘n⇙) = lnth (π⇘c⇙(inf_llist t)) (the_enat (⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩))"
proof -
have "enat (Suc i) < llength (inf_llist t)" using enat_ord_code by simp
moreover from ‹∥c∥⇘t ⟨c → t⟩⇘n⇙⇙› have "∥c∥⇘lnth (inf_llist t) ⟨c → t⟩⇘n⇙⇙" by simp
ultimately show ?thesis using proj_active_nth by simp
qed
ultimately show ?thesis by simp
qed

lemma baEN1[elim]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes act: "∃i. ∥c∥⇘t i⇙"
and nAct: "∄i. i≥n ∧ ∥c∥⇘t i⇙"
and al: "eval c t t' n (ba φ)"
shows "φ (t' (n - ⟨c ∧ t⟩ - 1))"
proof -
from al have "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (⇘c⇙↓⇘t⇙(n)))"
using act nAct validCE_cont ba_def by metis
hence "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (⇘c⇙↓⇘t⇙(n)))" by simp
moreover have "lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (⇘c⇙↓⇘t⇙(n)) = lnth (inf_llist t') (n - ⟨c ∧ t⟩ - 1)"
using act nAct cnf2bhv_lnth_lappend by simp
moreover have "… = t' (n - ⟨c ∧ t⟩ - 1)" by simp
ultimately show ?thesis by simp
qed

lemma baEN2[elim]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes nAct: "∄i. ∥c∥⇘t i⇙"
and al: "eval c t t' n (ba φ)"
shows "φ (t' n)"
proof -
from al have "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) n)"
using nAct validCE_not_act ba_def by metis
hence "φ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) n)" by simp
moreover have "lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) n = lnth (inf_llist t') n"
proof -
from nAct have "π⇘c⇙(inf_llist t) = []⇩l" by simp
hence "(π⇘c⇙(inf_llist t)) @⇩l (inf_llist t') = inf_llist t'" by (simp add: ‹π⇘c⇙inf_llist t = []⇩l›)
thus ?thesis by simp
qed
moreover have "… = t' n" by simp
ultimately show ?thesis by simp
qed

lemma baEANow[elim]:
fixes t n c φ
assumes "eval c t t' n (ba φ)"
and "∥c∥⇘t n⇙"
shows "φ (σ⇘c⇙(t n))"
proof -
from assms have "φ(σ⇘c⇙(t ⟨c → t⟩⇘n⇙))" using baEA by blast
with assms show ?thesis using nxtAct_active by simp
qed

subsubsection "Next Operator"

definition nxt :: "('cmp bta) ⇒ ('cmp bta)" ("○⇩b(_)" 24)
where "○⇩b(γ) ≡ λ t n. γ t (Suc n)"

lemma nxtIA[intro]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes "∃i≥n. ∥c∥⇘t i⇙"
and "⟦∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙⟧ ⟹ ∃n' ≥ n. (∃!i. n≤i ∧ i<n' ∧ ∥c∥⇘t i⇙) ∧ eval c t t' n' γ"
and "⟦¬(∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙)⟧ ⟹ eval c t t' (Suc ⟨c → t⟩⇘n⇙) γ"
shows "eval c t t' n (○⇩b(γ))"
proof (cases)
assume "∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙"
with assms(2) obtain n' where "n'≥n" and "∃!i. n≤i ∧ i<n' ∧ ∥c∥⇘t i⇙" and "eval c t t' n' γ" by blast
moreover from assms(1) have "∥c∥⇘t ⟨c → t⟩⇘n⇙⇙" and "⟨c → t⟩⇘n⇙≥n" using nxtActI by auto
ultimately have "∃i'≥n'. ∥c∥⇘t i'⇙" by (metis ‹∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙› dual_order.strict_trans2 leI nat_less_le)
with ‹eval c t t' n' γ›
have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘enat n'⇙ inf_llist t⟩))"
using validCE_act by blast
moreover have "the_enat(⟨c #⇘n'⇙ inf_llist t⟩) = Suc (the_enat (⟨c #⇘n⇙ inf_llist t⟩))"
proof -
from ‹∃!i. n≤i ∧ i<n' ∧ ∥c∥⇘t i⇙› obtain i where "n≤i" and "i<n'" and "∥c∥⇘t i⇙"
and "∀i'. n≤i' ∧ i'<n' ∧ ∥c∥⇘t i'⇙ ⟶ i'=i" by blast
moreover have "n' - 1 < llength (inf_llist t)" by simp
ultimately have "the_enat(⟨c #⇘n'⇙ inf_llist t⟩) = the_enat(eSuc (⟨c #⇘n⇙ inf_llist t⟩))"
using nAct_active_suc[of "inf_llist t" n' n i c]  by (simp add: ‹n ≤ i›)
moreover have "⟨c #⇘i⇙ inf_llist t⟩ ≠ ∞" by simp
ultimately show ?thesis using the_enat_eSuc by simp
qed
ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (Suc (the_enat (⟨c #⇘n⇙ inf_llist t⟩)))"
by simp
with assms have "eval c t t' n (λt n. γ t (Suc n))"
using validCI_act[of n c t "λt n. γ t (Suc n)" t'] by blast
thus ?thesis using nxt_def by simp
next
assume "¬ (∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙)"
with assms(3) have "eval c t t' (Suc ⟨c → t⟩⇘n⇙) γ" by simp
moreover from ‹¬ (∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙)› have "¬ (∃i≥Suc ⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙)" by simp
ultimately have "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) (⇘c⇙↓⇘t⇙(Suc ⟨c → t⟩⇘n⇙))"
using assms(1) validCE_cont[of c t "Suc ⟨c → t⟩⇘n⇙" t' γ] by blast
moreover from assms(1) ‹¬ (∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙)›
have "Suc (the_enat ⟨c #⇘enat n⇙inf_llist t⟩) = ⇘c⇙↓⇘t⇙(Suc ⟨c → t⟩⇘n⇙)"
using nAct_cnf2proj_Suc_dist by simp
ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (Suc (the_enat (⟨c #⇘n⇙ inf_llist t⟩)))"
by simp
moreover from assms(1) have "∥c∥⇘t ⟨c → t⟩⇘n⇙⇙" and "⟨c → t⟩⇘n⇙ ≥ n" using nxtActI by auto
ultimately have "eval c t t' n (λt n. γ t (Suc n))" using validCI_act[of n c t "λt n. γ t (Suc n)" t']
by blast
with ‹∥c∥⇘t ⟨c → t⟩⇘n⇙⇙› ‹¬ (∃i'≥Suc ⟨c → t⟩⇘n⇙. ∥c∥⇘t i'⇙)› show ?thesis using nxt_def by simp
qed

lemma nxtIN[intro]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes "¬(∃i≥n. ∥c∥⇘t i⇙)"
and "eval c t t' (Suc n) γ"
shows "eval c t t' n (○⇩b(γ))"
proof cases
assume "∃i. ∥c∥⇘t i⇙"
moreover from ‹¬ (∃i≥n. ∥c∥⇘t i⇙)› have "¬ (∃i≥Suc n. ∥c∥⇘t i⇙)" by simp
ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(Suc n))"
using validCE_cont ‹eval c t t' (Suc n) γ› by blast
with ‹∃i. ∥c∥⇘t i⇙› have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (Suc (⇘c⇙↓⇘t⇙(n)))"
using ‹¬(∃i≥n. ∥c∥⇘t i⇙)› lActive_less by auto
with ‹¬(∃i≥n. ∥c∥⇘t i⇙)› ‹∃i. ∥c∥⇘t i⇙› have "eval c t t' n (λt n. γ t (Suc n))"
using validCI_cont[where γ="(λt n. γ t (Suc n))"] by simp
thus ?thesis using nxt_def by simp
next
assume "¬(∃i. ∥c∥⇘t i⇙)"
with assms have "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) (Suc n)" using validCE_not_act by blast
with ‹¬(∃i. ∥c∥⇘t i⇙)› have "eval c t t' n (λt n. γ t (Suc n))"
using validCI_not_act[where γ="(λt n. γ t (Suc n))"] by blast
thus ?thesis using nxt_def by simp
qed

lemma nxtEA1[elim]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes "∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙"
and "eval c t t' n (○⇩b(γ))"
and "n'≥n"
and "∃!i. i≥n ∧ i<n' ∧ ∥c∥⇘t i⇙"
shows "eval c t t' n' γ"
proof -
from ‹eval c t t' n (○⇩b(γ))› have "eval c t t' n (λt n. γ t (Suc n))" using nxt_def by simp
moreover from assms(4) obtain i where "i≥n" and "i<n'" and "∥c∥⇘t i⇙"
and "∀i'. n≤i' ∧ i'<n' ∧ ∥c∥⇘t i'⇙ ⟶ i'=i" by blast
ultimately have "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) (Suc (the_enat ⟨c #⇘enat n⇙inf_llist t⟩))"
using validCE_act[of n c t t' "λt n. γ t (Suc n)"] by blast
moreover have "the_enat(⟨c #⇘n'⇙ inf_llist t⟩) = Suc (the_enat (⟨c #⇘n⇙ inf_llist t⟩))"
proof -
have "n' - 1 < llength (inf_llist t)" by simp
with ‹i<n'› and ‹∥c∥⇘t i⇙› and ‹∀i'. n≤i' ∧ i'<n' ∧ ∥c∥⇘t i'⇙ ⟶ i'=i›
have "the_enat(⟨c #⇘n'⇙ inf_llist t⟩) = the_enat(eSuc (⟨c #⇘n⇙ inf_llist t⟩))"
using nAct_active_suc[of "inf_llist t" n' n i c]  by (simp add: ‹n ≤ i›)
moreover have "⟨c #⇘i⇙ inf_llist t⟩ ≠ ∞" by simp
ultimately show ?thesis using the_enat_eSuc by simp
qed
ultimately have "γ (lnth ((π⇘c⇙inf_llist t) @⇩l inf_llist t')) (the_enat (⟨c #⇘n'⇙ inf_llist t⟩))" by simp
moreover have "∃i'≥n'. ∥c∥⇘t i'⇙"
proof -
from assms(4) have "⟨c → t⟩⇘n⇙≥n" and "∥c∥⇘t ⟨c → t⟩⇘n⇙⇙" using nxtActI by auto
with ‹∀i'. n≤i' ∧ i'<n' ∧ ∥c∥⇘t i'⇙ ⟶ i'=i› show ?thesis
using assms(1) by (metis leI le_trans less_le)
qed
ultimately show ?thesis using validCI_act by blast
qed

lemma nxtEA2[elim]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
and "i"
assumes "∃i≥n. ∥c∥⇘t i⇙" and "¬(∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙)"
and "eval c t t' n (○⇩b(γ))"
shows "eval c t t' (Suc ⟨c → t⟩⇘n⇙) γ"
proof -
from ‹eval c t t' n (○⇩b(γ))› have "eval c t t' n (λt n. γ t (Suc n))" using nxt_def by simp
with assms(1) have "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) (Suc (the_enat ⟨c #⇘enat n⇙inf_llist t⟩))"
using validCE_act[of n c t t' "λt n. γ t (Suc n)"] by blast
moreover from assms(1) assms(2) have "Suc (the_enat ⟨c #⇘enat n⇙inf_llist t⟩)=⇘c⇙↓⇘t⇙(Suc ⟨c → t⟩⇘n⇙)"
using nAct_cnf2proj_Suc_dist by simp
ultimately have "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) (⇘c⇙↓⇘t⇙(Suc ⟨c → t⟩⇘n⇙))" by simp
moreover from assms(1) assms(2) have "¬(∃i'≥Suc ⟨c → t⟩⇘n⇙. ∥c∥⇘t i'⇙)"
using nxtActive_no_active by simp
ultimately show ?thesis using validCI_cont[where n="Suc ⟨c → t⟩⇘n⇙"] assms(1) by blast
qed

lemma nxtEN[elim]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes "¬(∃i≥n. ∥c∥⇘t i⇙)"
and "eval c t t' n (○⇩b(γ))"
shows "eval c t t' (Suc n) γ"
proof cases
assume "∃i. ∥c∥⇘t i⇙"
moreover from ‹eval c t t' n (○⇩b(γ))› have "eval c t t' n (λt n. γ t (Suc n))" using nxt_def by simp
ultimately have "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) (Suc (⇘c⇙↓⇘t⇙n))"
using ‹¬(∃i≥n. ∥c∥⇘t i⇙)› validCE_cont[where γ="(λt n. γ t (Suc n))"] by simp
hence "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(Suc n))"
using ‹∃i. ∥c∥⇘t i⇙› assms(1) lActive_less by auto
moreover from ‹¬ (∃i≥n. ∥c∥⇘t i⇙)› have "¬ (∃i≥Suc n. ∥c∥⇘t i⇙)" by simp
ultimately show ?thesis using validCI_cont[where n="Suc n"] ‹∃i. ∥c∥⇘t i⇙› by blast
next
assume "¬(∃i. ∥c∥⇘t i⇙)"
moreover from ‹eval c t t' n (○⇩b(γ))› have "eval c t t' n (λt n. γ t (Suc n))" using nxt_def by simp
ultimately have "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) (Suc n)"
using ‹¬(∃i. ∥c∥⇘t i⇙)› validCE_not_act[where γ="(λt n. γ t (Suc n))"] by blast
with ‹¬(∃i. ∥c∥⇘t i⇙)› show ?thesis using validCI_not_act[of c t γ t' "Suc n"] by blast
qed

subsubsection "Eventually Operator"

definition evt :: "('cmp bta) ⇒ ('cmp bta)" ("◇⇩b(_)" 23)
where "◇⇩b(γ) ≡ λ t n. ∃n'≥n. γ t n'"

lemma evtIA[intro]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
and n'::nat
assumes "∃i≥n. ∥c∥⇘t i⇙"
and "n'≥⟨c ⇐ t⟩⇘n⇙"
and "⟦∃i≥n'. ∥c∥⇘t i⇙⟧ ⟹ ∃n''≥⟨c ⇐ t⟩⇘n'⇙. n''≤ ⟨c → t⟩⇘n'⇙ ∧ eval c t t' n'' γ"
and "⟦¬(∃i≥n'. ∥c∥⇘t i⇙)⟧ ⟹ eval c t t' n' γ"
shows "eval c t t' n (◇⇩b(γ))"
proof cases  assume "∃i'≥n'. ∥c∥⇘t i'⇙"
with assms(3) obtain n'' where "n'' ≥⟨c ⇐ t⟩⇘n'⇙" and "n''≤ ⟨c → t⟩⇘n'⇙" and "eval c t t' n'' γ" by auto
hence "∃i'≥n''. ∥c∥⇘t i'⇙" using ‹∃i'≥n'. ∥c∥⇘t i'⇙› nxtActI by blast
with ‹eval c t t' n'' γ› have
"γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘n''⇙ inf_llist t⟩))"
using validCE_act by blast
moreover have "the_enat (⟨c #⇘n⇙ inf_llist t⟩) ≤ the_enat (⟨c #⇘n''⇙ inf_llist t⟩)"
proof -
from ‹⟨c ⇐ t⟩⇘n'⇙≤n''› have "⟨c #⇘n'⇙ inf_llist t⟩ ≤ ⟨c #⇘n''⇙ inf_llist t⟩"
using nAct_mono_lNact by simp
moreover from ‹n'≥⟨c ⇐ t⟩⇘n⇙› have "⟨c #⇘n⇙ inf_llist t⟩ ≤ ⟨c #⇘n'⇙ inf_llist t⟩"
using nAct_mono_lNact by simp
moreover have "⟨c #⇘n'⇙ inf_llist t⟩ ≠ ∞" by simp
ultimately show ?thesis by simp
qed
moreover have "∃i'≥n. ∥c∥⇘t i'⇙"
proof -
from ‹∃i'≥n'. ∥c∥⇘t i'⇙› obtain i' where "i'≥n'" and "∥c∥⇘t i'⇙" by blast
with ‹n'≥⟨c ⇐ t⟩⇘n⇙› have "i'≥ n" using lNactGe le_trans by blast
with ‹∥c∥⇘t i'⇙› show ?thesis by blast
qed
ultimately have "eval c t t' n (λt n. ∃n'≥n. γ t n')"
using validCI_act[where γ="(λt n. ∃n'≥n. γ t n')"] by blast
thus ?thesis using evt_def by simp
next
assume "¬(∃i'≥n'. ∥c∥⇘t i'⇙)"
with ‹(∃i≥n. ∥c∥⇘t i⇙)› have "n' ≥ ⟨c ∧ t⟩" using lActive_less by auto
hence "⇘c⇙↓⇘t⇙(n') ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1" using cnf2bhv_ge_llength by simp
moreover have "the_enat(llength (π⇘c⇙(inf_llist t))) - 1 ≥ the_enat(⟨c #⇘n⇙ inf_llist t⟩)"
proof -
from ‹∃i≥n. ∥c∥⇘t i⇙› have "llength (π⇘c⇙(inf_llist t)) ≥ eSuc (⟨c #⇘n⇙ inf_llist t⟩)"
using nAct_llength_proj by simp
moreover from ‹¬(∃i'≥n'. ∥c∥⇘t i'⇙)› have "lfinite (π⇘c⇙(inf_llist t))"
using proj_finite2[of "inf_llist t"] by simp
hence "llength (π⇘c⇙(inf_llist t))≠∞" using llength_eq_infty_conv_lfinite by auto
ultimately have "the_enat (llength (π⇘c⇙(inf_llist t))) ≥ the_enat(eSuc (⟨c #⇘n⇙ inf_llist t⟩))"
by simp
moreover have "⟨c #⇘n⇙ inf_llist t⟩≠∞" by simp
ultimately have "the_enat (llength (π⇘c⇙(inf_llist t))) ≥ Suc (the_enat (⟨c #⇘n⇙ inf_llist t⟩))"
using the_enat_eSuc by simp
thus ?thesis by simp
qed
ultimately have "⇘c⇙↓⇘t⇙(n') ≥ the_enat (⟨c #⇘n⇙ inf_llist t⟩)" by simp
moreover from ‹¬(∃i'≥n'. ∥c∥⇘t i'⇙)› have "eval c t t' n' γ" using assms(4) by simp
with ‹∃i≥n. ∥c∥⇘t i⇙› ‹¬(∃i'≥n'. ∥c∥⇘t i'⇙)›
have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(n'))" using validCE_cont by blast
ultimately have "eval c t t' n (λt n. ∃n'≥n. γ t n')"
using ‹∃i≥n. ∥c∥⇘t i⇙› validCI_act[where γ="(λt n. ∃n'≥n. γ t n')"] by blast
thus ?thesis using evt_def by simp
qed

lemma evtIN[intro]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
and n'::nat
assumes "¬(∃i≥n. ∥c∥⇘t i⇙)"
and "n'≥n"
and "eval c t t' n' γ"
shows "eval c t t' n (◇⇩b(γ))"
proof cases
assume "∃i. ∥c∥⇘t i⇙"
moreover from assms(1) assms(2) have "¬(∃i'≥n'. ∥c∥⇘t i'⇙)" by simp
ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(n'))"
using validCE_cont[of c t n' t' γ] ‹eval c t t' n' γ› by blast
moreover from ‹n'≥n› have "⇘c⇙↓⇘t⇙(n') ≥ ⇘c⇙↓⇘t⇙(n)" using cnf2bhv_mono by simp
ultimately have "eval c t t' n (λt n. ∃n'≥n. γ t n')"
using validCI_cont[where γ="(λt n. ∃n'≥n. γ t n')"] ‹∃i. ∥c∥⇘t i⇙› ‹¬(∃i≥n. ∥c∥⇘t i⇙)› by blast
thus ?thesis using evt_def by simp
next
assume "¬(∃i. ∥c∥⇘t i⇙)"
with assms have "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n'" using validCE_not_act by blast
with ‹¬(∃i. ∥c∥⇘t i⇙)› have "eval c t t' n (λt n. ∃n'≥n. γ t n')"
using validCI_not_act[where γ="λt n. ∃n'≥n. γ t n'"] ‹n'≥n› by blast
thus ?thesis using evt_def by simp
qed

lemma evtEA[elim]:
fixes c::'id
and t::"nat ⇒ cnf"
and t'::"nat ⇒ 'cmp"
and n::nat
assumes "∃i≥n. ∥c∥⇘t i⇙"
and "eval c t t' n (◇⇩b(γ))"
shows "∃n'≥⟨c → t⟩⇘n⇙.
(∃i≥n'. ∥c∥⇘t i⇙ ∧ (∀n''≥ ⟨c ⇐ t⟩⇘n'⇙. n''≤⟨c → t⟩⇘n'⇙ ⟶ eval c t t' n'' γ)) ∨
(¬(∃i≥n'. ∥c∥⇘t i⇙) ∧ eval c t t' n' γ)"
proof -
from ‹eval c t t' n (◇⇩b(γ))› have "eval c t t' n (λt n. ∃n'≥n. γ t n')" using evt_def by simp
with ‹∃i≥n. ∥c∥⇘t i⇙›
have "∃n'≥the_enat ⟨c #⇘enat n⇙inf_llist t⟩. γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n'"
using validCE_act[where γ="λt n. ∃n'≥n. γ t n'"] by blast
then obtain x where "x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)" and
"γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x" by auto
thus ?thesis
proof (cases)
assume "x ≥ llength (π⇘c⇙(inf_llist t))"
moreover from ‹(x ≥ llength (π⇘c⇙(inf_llist t)))› have "llength (π⇘c⇙(inf_llist t))≠∞"
by (metis infinity_ileE)
moreover from ‹∃i≥n. ∥c∥⇘t i⇙› have "llength (π⇘c⇙(inf_llist t))≥1"
using proj_one[of "inf_llist t"] by auto
ultimately have "the_enat (llength (π⇘c⇙(inf_llist t))) - 1 < x"
by (metis One_nat_def Suc_ile_eq antisym_conv2 diff_Suc_less enat_ord_simps(2)
enat_the_enat less_imp_diff_less one_enat_def)
hence "x = ⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x))" using cnf2bhv_bhv2cnf by simp
with ‹γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x›
have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x)))" by simp
moreover have "¬(∃i≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i⇙)"
proof -
from ‹x ≥ llength (π⇘c⇙(inf_llist t))› have "lfinite (π⇘c⇙(inf_llist t))"
using llength_geq_enat_lfiniteD[of "π⇘c⇙(inf_llist t)" x] by simp
then obtain z where "∀n''>z. ¬ ∥c∥⇘t n''⇙" using proj_finite_bound by blast
moreover from ‹the_enat (llength (π⇘c⇙(inf_llist t))) - 1 < x› have "⟨c ∧ t⟩ < ⇘c⇙↑⇘t⇙(x)"
using bhv2cnf_greater_lActive by simp
ultimately show ?thesis using lActive_greater_active_all by simp
qed
ultimately have "eval c t t' (⇘c⇙↑⇘t⇙x) γ"
using ‹∃i≥n. ∥c∥⇘t i⇙› validCI_cont[of c t "⇘c⇙↑⇘t⇙(x)"] by blast
moreover have "⇘c⇙↑⇘t⇙(x) ≥ ⟨c → t⟩⇘n⇙"
proof -
from ‹x ≥ llength (π⇘c⇙(inf_llist t))› have "lfinite (π⇘c⇙(inf_llist t))"
using llength_geq_enat_lfiniteD[of "π⇘c⇙(inf_llist t)" x] by simp
then obtain z where "∀n''>z. ¬ ∥c∥⇘t n''⇙" using proj_finite_bound by blast
moreover from ‹∃i≥n. ∥c∥⇘t i⇙› have "∥c∥⇘t ⟨c → t⟩⇘n⇙⇙" using nxtActI by simp
ultimately have "⟨c ∧ t⟩≥⟨c → t⟩⇘n⇙" using lActive_greatest by fastforce
moreover have "⇘c⇙↑⇘t⇙(x) ≥ ⟨c ∧ t⟩" by simp
ultimately show "⇘c⇙↑⇘t⇙(x) ≥ ⟨c → t⟩⇘n⇙" by arith
qed
ultimately show ?thesis using ‹¬(∃i≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i⇙)› by blast
next
assume "¬(x ≥ llength (π⇘c⇙(inf_llist t)))"
hence "x<llength (π⇘c⇙(inf_llist t))" by