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