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 simp
    then obtain n'::nat where "x=⟨c #⇘n'⇙ inf_llist t⟩" using nAct_exists by blast
    with ‹enat x < llength (π⇘c⇙(inf_llist t))› have "∃i≥n'. ∥c∥⇘t i⇙" using nAct_less_llength_active by force
    then obtain i where "i≥n'" and "∥c∥⇘t i⇙" and "¬ (∃k≥n'. k < i ∧ ∥c∥⇘t k⇙)" using nact_exists by blast
    moreover have "(∀n''≥ ⟨c ⇐ t⟩⇘i⇙. n''≤⟨c → t⟩⇘i⇙ ⟶ eval c t t' n'' γ)"
    proof
      fix n'' show "⟨c ⇐ t⟩⇘i⇙ ≤ n'' ⟶ n'' ≤ ⟨c → t⟩⇘i⇙ ⟶ eval c t t' n'' γ"
      proof(rule HOL.impI[OF HOL.impI])
        assume "⟨c ⇐ t⟩⇘i⇙ ≤ n''" and "n'' ≤ ⟨c → t⟩⇘i⇙"
        hence "the_enat (⟨c #⇘enat i⇙ inf_llist t⟩) = the_enat (⟨c #⇘enat n''⇙ inf_llist t⟩)"
          using nAct_same by simp
        moreover from ‹∥c∥⇘t i⇙› have "∥c∥⇘t ⟨c → t⟩⇘i⇙⇙" using nxtActI by auto
        with ‹n'' ≤ ⟨c → t⟩⇘i⇙› have "∃i≥n''. ∥c∥⇘t i⇙" using dual_order.strict_implies_order by auto
        moreover have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘enat i⇙ inf_llist t⟩))"
        proof -
          have "enat i - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
          with ‹x=⟨c #⇘n'⇙ inf_llist t⟩› ‹i≥n'› ‹¬ (∃k≥n'. k < i ∧ ∥c∥⇘t k⇙)› have "x=⟨c #⇘i⇙ inf_llist t⟩"
            using one_enat_def nAct_not_active_same by simp
          moreover have "⟨c #⇘i⇙ inf_llist t⟩≠∞" by simp
          ultimately have "x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)" by fastforce        
          thus ?thesis using ‹γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x› by blast
        qed
        with ‹the_enat (⟨c #⇘enat i⇙ inf_llist t⟩) = the_enat (⟨c #⇘enat n''⇙ inf_llist t⟩)› have
          "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘enat n''⇙ inf_llist t⟩))" by simp
        ultimately show "eval c t t' n'' γ" using validCI_act by blast
      qed
    qed
    moreover have "i≥⟨c → t⟩⇘n⇙"
    proof -
      have "enat i - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
      with ‹x=⟨c #⇘n'⇙ inf_llist t⟩› ‹i≥n'› ‹¬ (∃k≥n'. k < i ∧ ∥c∥⇘t k⇙)› have "x=⟨c #⇘i⇙ inf_llist t⟩"
        using one_enat_def nAct_not_active_same by simp
      moreover have "⟨c #⇘i⇙ inf_llist t⟩≠∞" by simp
      ultimately have "x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)" by fastforce        
      with ‹x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)›
        have "the_enat (⟨c #⇘i⇙ inf_llist t⟩)≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)" by simp
      with ‹∥c∥⇘t i⇙› show ?thesis using active_geq_nxtAct by simp
    qed
    ultimately show ?thesis using ‹∥c∥⇘t i⇙› by auto
  qed    
qed
    
lemma evtEN[elim]:
  fixes c::'id
    and t::"nat ⇒ cnf"
    and t'::"nat ⇒ 'cmp"
    and n::nat
    and n'::nat  
  assumes "¬(∃i≥n. ∥c∥⇘t i⇙)"
    and "eval c t t' n (◇⇩b(γ))"
  shows "∃n'≥n. eval c t t' n' γ" 
proof cases
  assume "∃i. ∥c∥⇘t i⇙"
  moreover from ‹eval c t t' n (◇⇩b(γ))› have "eval c t t' n (λt n. ∃n'≥n. γ t n')" using evt_def by simp
  ultimately have "∃n'≥⇘c⇙↓⇘t⇙n. γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n'"
    using validCE_cont[where γ="(λt n. ∃n'≥n. γ t n')"] ‹¬(∃i≥n. ∥c∥⇘t i⇙)› by blast
  then obtain x where "x≥⇘c⇙↓⇘t⇙(n)" and " γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x" by auto
  moreover have "the_enat (llength (π⇘c⇙(inf_llist t))) - 1 < x"
  proof -
    have "⟨c ∧ t⟩ < n"
    proof (rule ccontr)
      assume "¬⟨c ∧ t⟩ < n"
      hence "⟨c ∧ t⟩ ≥ n" by simp
      moreover from ‹∃i. ∥c∥⇘t i⇙› ‹¬ (∃i≥n. ∥c∥⇘t i⇙)› have "∥c∥⇘t ⟨c ∧ t⟩⇙"
        using lActive_active less_or_eq_imp_le by blast
      ultimately show False using ‹¬ (∃i≥n. ∥c∥⇘t i⇙)› by simp
    qed
    hence "the_enat (llength (π⇘c⇙(inf_llist t))) - 1 < ⇘c⇙↓⇘t⇙(n)" using cnf2bhv_greater_llength by simp
    with ‹x≥⇘c⇙↓⇘t⇙(n)› show ?thesis by simp
  qed
  hence "x = ⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x))" using cnf2bhv_bhv2cnf by simp
  ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x)))" by simp
  moreover from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "¬(∃i≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i⇙)"
  proof -
    from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "lfinite (π⇘c⇙(inf_llist t))" using proj_finite2 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 validCI_cont[of c t "⇘c⇙↑⇘t⇙(x)" γ] ‹∃i. ∥c∥⇘t i⇙› by blast
  moreover from ‹∃i. ∥c∥⇘t i⇙› ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "⟨c ∧ t⟩ ≤ n" using lActive_less[of c t _ n] by auto
  with ‹x≥⇘c⇙↓⇘t⇙(n)› have "n ≤ ⇘c⇙↑⇘t⇙(x)" using p2c_mono_c2p by blast  
  ultimately show ?thesis by auto
next
  assume "¬(∃i. ∥c∥⇘t i⇙)"
  moreover from ‹eval c t t' n (◇⇩b(γ))› have "eval c t t' n (λt n. ∃n'≥n. γ t n')" using evt_def by simp
  ultimately obtain n' where "n'≥n" and "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n'"
    using ‹¬(∃i. ∥c∥⇘t i⇙)› validCE_not_act[where γ="λt n. ∃n'≥n. γ t n'"] by blast
  with ‹¬(∃i. ∥c∥⇘t i⇙)› show ?thesis using validCI_not_act[of c t γ t' n'] by blast
qed    

subsubsection "Globally Operator"

definition glob :: "('cmp bta) ⇒ ('cmp bta)" (‹□⇩b(_)› 22)
  where "□⇩b(γ) ≡ λ t n. ∀n'≥n. γ t n'"
    
lemma globIA[intro]:
  fixes c::'id
    and t::"nat ⇒ cnf"
    and t'::"nat ⇒ 'cmp"
    and n::nat  
  assumes "∃i≥n. ∥c∥⇘t i⇙"
    and "⋀n'. ⟦∃i≥n'. ∥c∥⇘t i⇙; n'≥⟨c → t⟩⇘n⇙⟧ ⟹ ∃n''≥⟨c ⇐ t⟩⇘n'⇙. n''≤⟨c → t⟩⇘n'⇙ ∧ eval c t t' n'' γ"
    and "⋀n'. ⟦¬(∃i≥n'. ∥c∥⇘t i⇙); n'≥⟨c → t⟩⇘n⇙⟧ ⟹ eval c t t' n' γ" 
  shows "eval c t t' n (□⇩b(γ))"
proof -
  have "∀n'≥the_enat ⟨c #⇘enat n⇙inf_llist t⟩. γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n'"
  proof
    fix x::nat show
      "x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩) ⟶ γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
    proof
      assume "x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)"
      show "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x"
      proof (cases)
        assume "(x ≥ llength (π⇘c⇙(inf_llist t)))"
        hence "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 have "∥c∥⇘t ⟨c → t⟩⇘n⇙⇙" by (simp add: ‹∃i≥n. ∥c∥⇘t i⇙› nxtActI)
        ultimately have "⟨c ∧ t⟩≥⟨c → t⟩⇘n⇙" using lActive_greatest[of c t "⟨c → t⟩⇘n⇙"] by blast
        moreover have "⇘c⇙↑⇘t⇙(x) ≥ ⟨c ∧ t⟩" by simp
        ultimately have "⇘c⇙↑⇘t⇙(x) ≥ ⟨c → t⟩⇘n⇙" by arith
        moreover have "¬ (∃i'≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i'⇙)"
        proof -
          from ‹lfinite (π⇘c⇙(inf_llist t))› ‹∃i≥n. ∥c∥⇘t i⇙›
            have "⇘c⇙↑⇘t⇙(the_enat (llength (π⇘c⇙(inf_llist t)))) = Suc (⟨c ∧ t⟩)"
            using bhv2cnf_lActive by blast
          moreover from ‹(x ≥ llength (π⇘c⇙(inf_llist t)))› have "x ≥ the_enat(llength (π⇘c⇙(inf_llist t)))"
            using the_enat_mono by fastforce
          hence "⇘c⇙↑⇘t⇙(x) ≥ ⇘c⇙↑⇘t⇙(the_enat (llength (π⇘c⇙(inf_llist t))))"
            using bhv2cnf_mono[of "the_enat (llength (π⇘c⇙(inf_llist t)))" x] by simp
          ultimately have "⇘c⇙↑⇘t⇙(x) ≥ Suc (⟨c ∧ t⟩)" by simp
          hence "⇘c⇙↑⇘t⇙(x) > ⟨c ∧ t⟩" by simp
          with ‹∀n''>z. ¬ ∥c∥⇘t n''⇙› show ?thesis using lActive_greater_active_all by simp
        qed
        ultimately have "eval c t t' (⇘c⇙↑⇘t⇙(x)) γ" using assms(3) by simp
        hence "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x)))"
          using validCE_cont[of c t "⇘c⇙↑⇘t⇙(x)" t' γ] ‹∃i≥n. ∥c∥⇘t i⇙› ‹¬ (∃i'≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i'⇙)› by blast
        moreover from ‹(x ≥ llength (π⇘c⇙(inf_llist t)))›
          have "(enat x ≥ llength (π⇘c⇙(inf_llist t)))" by auto
        with ‹lfinite (π⇘c⇙(inf_llist t))› have "llength (π⇘c⇙(inf_llist t))≠∞"
          using llength_eq_infty_conv_lfinite by auto
        with ‹(x ≥ llength (π⇘c⇙(inf_llist t)))›
          have "the_enat(llength (π⇘c⇙(inf_llist t))) - 1 ≤ x" by auto
        ultimately show ?thesis using cnf2bhv_bhv2cnf[of c t x] by simp
      next
        assume "¬(x ≥ llength (π⇘c⇙(inf_llist t)))"
        hence "x<llength (π⇘c⇙(inf_llist t))" by simp
        then obtain n'::nat where "x=⟨c #⇘n'⇙ inf_llist t⟩" using nAct_exists by blast
        moreover from ‹enat x < llength (π⇘c⇙(inf_llist t))› ‹enat x = ⟨c #⇘enat n'⇙ inf_llist t⟩›
          have "∃i≥n'. ∥c∥⇘t i⇙" using nAct_less_llength_active by force
        then obtain i where "i≥n'" and "∥c∥⇘t i⇙" and "¬ (∃k≥n'. k < i ∧ ∥c∥⇘t k⇙)"
          using nact_exists by blast
        moreover have "enat i - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
        ultimately have "x=⟨c #⇘i⇙ inf_llist t⟩" using one_enat_def nAct_not_active_same by simp
        moreover have "⟨c #⇘i⇙ inf_llist t⟩≠∞" by simp
        ultimately have "x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)" by fastforce
        from ‹x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)› ‹x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)›
        have "the_enat (⟨c #⇘i⇙ inf_llist t⟩)≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)" by simp
        with ‹∥c∥⇘t i⇙› have "i≥⟨c → t⟩⇘n⇙" using active_geq_nxtAct by simp
        moreover from ‹x=⟨c #⇘i⇙ inf_llist t⟩› ‹x < llength (π⇘c⇙(inf_llist t))›
          have "∃i'. i ≤ enat i' ∧ ∥c∥⇘t i'⇙" using nAct_less_llength_active[of x c "inf_llist t" i] by simp
        hence "∃i'≥i. ∥c∥⇘t i'⇙" by simp
        ultimately obtain n'' where "eval c t t' n'' γ" and "n''≥⟨c ⇐ t⟩⇘i⇙" and "n''≤⟨c → t⟩⇘i⇙"
          using assms(2) by blast
        moreover have "∃i'≥n''. ∥c∥⇘t i'⇙"
          using ‹∥c∥⇘t i⇙› ‹n''≤⟨c → t⟩⇘i⇙› less_or_eq_imp_le nxtAct_active by auto
        ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘n''⇙ inf_llist t⟩))"
          using validCE_act[of n'' c t t' γ] by blast
        moreover from ‹n''≥⟨c ⇐ t⟩⇘i⇙› and ‹n''≤⟨c → t⟩⇘i⇙›
          have "the_enat (⟨c #⇘n''⇙ inf_llist t⟩)=the_enat (⟨c #⇘i⇙ inf_llist t⟩)" using nAct_same by simp
        hence "the_enat (⟨c #⇘n''⇙ inf_llist t⟩) = x" by (simp add: ‹x = the_enat ⟨c #⇘enat i⇙inf_llist t⟩›)
        ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat x)" by simp
        thus ?thesis by simp
      qed
    qed
  qed
  with ‹∃i≥n. ∥c∥⇘t i⇙› have "eval c t t' n (λt n. ∀n'≥n. γ t n')"
    using validCI_act[of n c t "λ t n. ∀n'≥n. γ t n'" t'] by blast
  thus ?thesis using glob_def by simp
qed
  
lemma globIN[intro]:
  fixes c::'id
    and t::"nat ⇒ cnf"
    and t'::"nat ⇒ 'cmp"
    and n::nat  
  assumes "¬(∃i≥n. ∥c∥⇘t i⇙)"
    and "⋀n'. n'≥n ⟹ eval c t t' n' γ"
  shows "eval c t t' n (□⇩b(γ))"
proof cases
  assume "∃i. ∥c∥⇘t i⇙"    
  from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "lfinite (π⇘c⇙(inf_llist t))" using proj_finite2 by simp
  then obtain z where "∀n''>z. ¬ ∥c∥⇘t n''⇙" using proj_finite_bound by blast
    
  have "∀x::nat≥ ⇘c⇙↓⇘t⇙(n). γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
  proof
    fix x::nat show "(x≥⇘c⇙↓⇘t⇙(n)) ⟶ γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
    proof
      assume "x≥⇘c⇙↓⇘t⇙(n)"
      moreover from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "⟨c ∧ t⟩ ≤ n" using ‹∃i. ∥c∥⇘t i⇙› lActive_less by auto
      ultimately have "⇘c⇙↑⇘t⇙(x) ≥ n" using p2c_mono_c2p by simp
      with assms have "eval c t t' (⇘c⇙↑⇘t⇙(x)) γ" by simp    
      moreover have "¬ (∃i'≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i'⇙)"
      proof -
        from ‹lfinite (π⇘c⇙(inf_llist t))› ‹∃i. ∥c∥⇘t i⇙›
          have "⇘c⇙↑⇘t⇙(the_enat (llength (π⇘c⇙(inf_llist t)))) = Suc (⟨c ∧ t⟩)"
          using bhv2cnf_lActive by blast
        moreover from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "n>⟨c ∧ t⟩"
          by (meson ‹∃i. ∥c∥⇘t i⇙› lActive_active leI le_eq_less_or_eq)
        hence "n≥Suc (⟨c ∧ t⟩)" by simp
        with ‹n≥Suc(⟨c ∧ t⟩)› ‹⇘c⇙↑⇘t⇙(x) ≥ n› have "⇘c⇙↑⇘t⇙(x) ≥ Suc (⟨c ∧ t⟩)" by simp
        hence "⇘c⇙↑⇘t⇙(x) > ⟨c ∧ t⟩" by simp
        with ‹∀n''>z. ¬ ∥c∥⇘t n''⇙› show ?thesis using lActive_greater_active_all by simp
      qed
      ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x)))"
        using validCE_cont[of c t "⇘c⇙↑⇘t⇙(x)" t' γ] ‹∃i. ∥c∥⇘t i⇙› by blast
      moreover have "x ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1"
        using ‹⇘c⇙↓⇘t⇙(n) ≤ x› cnf2bhv_def by auto
      ultimately show "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x"
        using cnf2bhv_bhv2cnf by simp
    qed
  qed
  with ‹∃i. ∥c∥⇘t i⇙› ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "eval c t t' n (λt n. ∀n'≥n. γ t n')"
    using validCI_cont[of c t n "λ t n. ∀n'≥n. γ t n'" t'] by simp
  thus ?thesis using glob_def by simp
next
  assume "¬(∃i. ∥c∥⇘t i⇙)"
  with assms have "∀n'≥n. γ (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'"] by blast
  thus ?thesis using glob_def by simp
qed
      
lemma globEA[elim]:
  fixes c::'id
    and t::"nat ⇒ cnf"
    and t'::"nat ⇒ 'cmp"
    and n::nat
    and n'::nat
  assumes "∃i≥n. ∥c∥⇘t i⇙"
    and "eval c t t' n (□⇩b(γ))"
    and "n'≥⟨c ⇐ t⟩⇘n⇙"
  shows "eval c t t' n' γ"
proof (cases)
  assume "∃i≥n'. ∥c∥⇘t i⇙"
  with ‹n'≥⟨c ⇐ t⟩⇘n⇙› have "the_enat (⟨c #⇘n'⇙ inf_llist t⟩) ≥ the_enat (⟨c #⇘n⇙ inf_llist t⟩)"
    using nAct_mono_lNact ‹∃i≥n. ∥c∥⇘t i⇙› by simp
  moreover from ‹eval c t t' n (□⇩b(γ))› have "eval c t t' n (λt n. ∀n'≥n. γ t n')"
    using glob_def by simp
  hence "∀x≥the_enat ⟨c #⇘enat n⇙inf_llist t⟩. γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
    using validCE_act ‹∃i≥n. ∥c∥⇘t i⇙› by blast
  ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘n'⇙ inf_llist t⟩))" by simp
  with ‹∃i≥n'. ∥c∥⇘t i⇙› show ?thesis using validCI_act by blast    
next
  assume "¬(∃i≥n'. ∥c∥⇘t i⇙)"
  from ‹eval c t t' n (□⇩b(γ))› have "eval c t t' n (λt n. ∀n'≥n. γ t n')" using glob_def by simp
  hence "∀x≥the_enat ⟨c #⇘enat n⇙inf_llist t⟩. γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
    using validCE_act ‹∃i≥n. ∥c∥⇘t i⇙› by blast
  moreover have "⇘c⇙↓⇘t⇙(n') ≥ the_enat (⟨c #⇘n⇙ inf_llist t⟩)"
  proof -
    have "⟨c #⇘n⇙ inf_llist t⟩≤llength (π⇘c⇙(inf_llist t))" using nAct_le_proj by metis
    moreover from ‹¬ (∃i≥n'. ∥c∥⇘t i⇙)› have "llength (π⇘c⇙(inf_llist t))≠∞"
      by (metis llength_eq_infty_conv_lfinite lnth_inf_llist proj_finite2)
    ultimately have "the_enat(⟨c #⇘n⇙ inf_llist t⟩)≤the_enat(llength (π⇘c⇙(inf_llist t)))" by simp
    moreover from ‹∃i≥n. ∥c∥⇘t i⇙› ‹¬ (∃i≥n'. ∥c∥⇘t i⇙)› have "n'>⟨c ∧ t⟩"
      using lActive_active by (meson leI le_eq_less_or_eq)
    hence "⇘c⇙↓⇘t⇙(n') > the_enat (llength (π⇘c⇙(inf_llist t))) - 1" using cnf2bhv_greater_llength by simp
    ultimately show ?thesis by simp
  qed
  ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(n'))" by simp
  with ‹∃i≥n. ∥c∥⇘t i⇙› ‹¬(∃i≥n'. ∥c∥⇘t i⇙)› show ?thesis using validCI_cont by blast
qed

lemma globEANow:
  fixes c t t' n i γ
  assumes "n ≤ i"
    and "∥c∥⇘t i⇙"
    and "eval c t t' n (□⇩bγ)"
  shows "eval c t t' i γ"
proof -
  from ‹∥c∥⇘t i⇙› ‹n ≤ i› have "∃i≥n. ∥c∥⇘t i⇙" by auto
  moreover from ‹n ≤ i› have "⟨c ⇐ t⟩⇘n⇙ ≤ i" using dual_order.trans lNactLe by blast
  ultimately show ?thesis using globEA[of n c t t' γ i] ‹eval c t t' n (□⇩bγ)› by simp
qed

lemma globEN[elim]:
  fixes c::'id
    and t::"nat ⇒ cnf"
    and t'::"nat ⇒ 'cmp"
    and n::nat
    and n'::nat
  assumes "¬(∃i≥n. ∥c∥⇘t i⇙)"
    and "eval c t t' n (□⇩b(γ))"
    and "n'≥n"
  shows "eval c t t' n' γ"
proof cases
  assume "∃i. ∥c∥⇘t i⇙"
  moreover from ‹eval c t t' n (□⇩b(γ))› have "eval c t t' n (λt n. ∀n'≥n. γ t n')"
    using glob_def by simp
  ultimately have "∀x≥⇘c⇙↓⇘t⇙n. γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
    using validCE_cont[of c t n t' "λt n. ∀n'≥n. γ t n'"] ‹¬(∃i≥n. ∥c∥⇘t i⇙)› by blast
  moreover from ‹n'≥n› have "⇘c⇙↓⇘t⇙(n') ≥ ⇘c⇙↓⇘t⇙(n)" using cnf2bhv_mono by simp
  ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(n'))" by simp
  moreover from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› ‹n'≥n› have "¬(∃i≥n'. ∥c∥⇘t i⇙)" by simp
  ultimately show ?thesis using validCI_cont ‹∃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. ∀n'≥n. γ t n')"
    using glob_def by simp
  ultimately have "∀n'≥n. γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n'"
    using ‹¬(∃i. ∥c∥⇘t i⇙)› validCE_not_act[where γ="λt n. ∀n'≥n. γ t n'"] by blast
  with ‹¬(∃i. ∥c∥⇘t i⇙)› ‹n'≥n› show ?thesis using validCI_not_act by blast
qed

subsubsection "Until Operator"

definition until :: "('cmp bta) ⇒ ('cmp bta) ⇒ ('cmp bta)" (infixl ‹𝔘⇩b› 21)
  where "γ' 𝔘⇩b γ ≡ λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"
    
lemma untilIA[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'' γ ∧
      (∀n'''≥⟨c → t⟩⇘n⇙. n'''< ⟨c ⇐ t⟩⇘n''⇙
      ⟶ (∃n''''≥⟨c ⇐ t⟩⇘n'''⇙. n''''≤ ⟨c → t⟩⇘n'''⇙ ∧ eval c t t' n'''' γ'))"
    and "⟦¬(∃i≥n'. ∥c∥⇘t i⇙)⟧ ⟹ eval c t t' n' γ ∧
      (∀n''≥⟨c → t⟩⇘n⇙. n''< 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'' γ'))"
  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'' γ" and
    a1: "∀n'''≥⟨c → t⟩⇘n⇙. n'''< ⟨c ⇐ t⟩⇘n''⇙
    ⟶ (∃n''''≥⟨c ⇐ t⟩⇘n'''⇙. n''''≤ ⟨c → t⟩⇘n'''⇙ ∧ eval c t t' n'''' γ')" by blast
  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 ‹⟨c ⇐ t⟩⇘n'⇙≤n''› have "⟨c #⇘n'⇙ inf_llist t⟩ ≤ ⟨c #⇘n''⇙ inf_llist t⟩"
      using nAct_mono_lNact by simp        
    ultimately have "⟨c #⇘n⇙ inf_llist t⟩ ≤ ⟨c #⇘n''⇙ inf_llist t⟩" 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
  moreover have "∀n'≥the_enat ⟨c #⇘n⇙inf_llist t⟩. n' < (the_enat ⟨c #⇘enat n''⇙inf_llist t⟩)
    ⟶ γ' (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n'"
  proof
    fix x::nat show "x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)
      ⟶ x < (the_enat ⟨c #⇘enat n''⇙inf_llist t⟩) ⟶ γ' (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
    proof (rule HOL.impI[OF HOL.impI])
      assume "x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)" and "x < (the_enat ⟨c #⇘enat n''⇙inf_llist t⟩)"
      moreover have "the_enat (⟨c #⇘enat n''⇙ inf_llist t⟩) = ⟨c #⇘enat n''⇙ inf_llist t⟩" by simp
      ultimately have "x<llength (π⇘c⇙(inf_llist t))" using nAct_le_proj[of c n'' "inf_llist t"]
        by (metis enat_ord_simps(2) less_le_trans)
      hence "x<llength (π⇘c⇙(inf_llist t))" by simp
      then obtain n'::nat where "x=⟨c #⇘n'⇙ inf_llist t⟩" using nAct_exists by blast
      moreover from ‹enat x < llength (π⇘c⇙(inf_llist t))› ‹enat x = ⟨c #⇘enat n'⇙ inf_llist t⟩›
        have "∃i≥n'. ∥c∥⇘t i⇙" using nAct_less_llength_active by force
      then obtain i where "i≥n'" and "∥c∥⇘t i⇙" and "¬ (∃k≥n'. k < i ∧ ∥c∥⇘t k⇙)" using nact_exists by blast
      moreover have "enat i - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
      ultimately have "x=⟨c #⇘i⇙ inf_llist t⟩" using one_enat_def nAct_not_active_same by simp
      moreover have "⟨c #⇘i⇙ inf_llist t⟩≠∞" by simp
      ultimately have "x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)" by fastforce
      from ‹x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)› ‹x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)›
      have "the_enat (⟨c #⇘i⇙ inf_llist t⟩)≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)" by simp
      with ‹∥c∥⇘t i⇙› have "i≥⟨c → t⟩⇘n⇙" using active_geq_nxtAct by simp
      moreover have "i < ⟨c ⇐ t⟩⇘n''⇙"
      proof -
        have "the_enat ⟨c #⇘enat n''⇙inf_llist t⟩ = ⟨c #⇘enat n''⇙inf_llist t⟩" by simp
        with ‹x < (the_enat ⟨c #⇘enat n''⇙inf_llist t⟩)› and ‹x=⟨c #⇘i⇙ inf_llist t⟩› have
          "⟨c #⇘i⇙ inf_llist t⟩<⟨c #⇘n''⇙ inf_llist t⟩" by (metis enat_ord_simps(2))
        hence "i<n''" using nAct_strict_mono_back[of c i "inf_llist t" n''] by auto
        with ‹∥c∥⇘t i⇙› show ?thesis using lNact_notActive leI by blast
      qed
      ultimately obtain n'' where "eval c t t' n'' γ'" and "n''≥⟨c ⇐ t⟩⇘i⇙" and "n''≤⟨c → t⟩⇘i⇙"
        using a1 by auto
      moreover have "∃i'≥n''. ∥c∥⇘t i'⇙"
        using ‹∥c∥⇘t i⇙› ‹n''≤⟨c → t⟩⇘i⇙› less_or_eq_imp_le nxtAct_active by auto
      ultimately have "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘n''⇙ inf_llist t⟩))"
        using validCE_act[of n'' c t t' γ'] by blast
      moreover from ‹n''≥⟨c ⇐ t⟩⇘i⇙› and ‹n''≤⟨c → t⟩⇘i⇙›
        have "the_enat (⟨c #⇘n''⇙ inf_llist t⟩)=the_enat (⟨c #⇘i⇙ inf_llist t⟩)" using nAct_same by simp
      hence "the_enat (⟨c #⇘n''⇙ inf_llist t⟩) = x" by (simp add: ‹x = the_enat ⟨c #⇘enat i⇙inf_llist t⟩›)
      ultimately show "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x" by simp
    qed
  qed 
  ultimately have "eval c t t' n (λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n'))"
    using validCI_act[where γ="λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"] by blast
  thus ?thesis using until_def by simp
next
  assume "¬(∃i'≥n'. ∥c∥⇘t i'⇙)"
  with assms(4) have "eval c t t' n' γ" and a2: "∀n''≥⟨c → t⟩⇘n⇙. n''< 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'' γ')" by auto
  with ‹¬(∃i'≥n'. ∥c∥⇘t i'⇙)› ‹eval c t t' n' γ› ‹∃i≥n. ∥c∥⇘t i⇙› have
    "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(n'))" using validCE_cont by blast
  moreover have "⇘c⇙↓⇘t⇙(n') ≥ the_enat (⟨c #⇘n⇙ inf_llist t⟩)"
  proof -
    from ‹(∃i≥n. ∥c∥⇘t i⇙)› ‹¬(∃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 show ?thesis by simp
  qed
  moreover have "∀x≥the_enat ⟨c #⇘n⇙inf_llist t⟩. x < (⇘c⇙↓⇘t⇙(n'))
    ⟶ γ' (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
  proof
    fix x::nat show
      "x≥the_enat ⟨c #⇘n⇙inf_llist t⟩ ⟶ x < (⇘c⇙↓⇘t⇙(n')) ⟶ γ' (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
    proof (rule HOL.impI[OF HOL.impI])
      assume "x≥the_enat ⟨c #⇘n⇙inf_llist t⟩" and "x < (⇘c⇙↓⇘t⇙(n'))"
      show "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x"
      proof (cases)
        assume "(x ≥ llength (π⇘c⇙(inf_llist t)))"
        hence "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 have "∥c∥⇘t ⟨c → t⟩⇘n⇙⇙" by (simp add: ‹∃i≥n. ∥c∥⇘t i⇙› nxtActI)
        ultimately have "⟨c ∧ t⟩≥⟨c → t⟩⇘n⇙" using lActive_greatest[of c t "⟨c → t⟩⇘n⇙"] by blast
        moreover have "⇘c⇙↑⇘t⇙(x) ≥ ⟨c ∧ t⟩" by simp
        ultimately have "⇘c⇙↑⇘t⇙(x) ≥ ⟨c → t⟩⇘n⇙" by arith
        moreover have "¬ (∃i'≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i'⇙)"
        proof -
          from ‹lfinite (π⇘c⇙(inf_llist t))› ‹∃i≥n. ∥c∥⇘t i⇙›
            have "⇘c⇙↑⇘t⇙(the_enat (llength (π⇘c⇙(inf_llist t)))) = Suc (⟨c ∧ t⟩)"
            using bhv2cnf_lActive by blast
          moreover from ‹(x ≥ llength (π⇘c⇙(inf_llist t)))› have "x ≥ the_enat(llength (π⇘c⇙(inf_llist t)))"
            using the_enat_mono by fastforce
          hence "⇘c⇙↑⇘t⇙(x) ≥ ⇘c⇙↑⇘t⇙(the_enat (llength (π⇘c⇙(inf_llist t))))"
            using bhv2cnf_mono[of "the_enat (llength (π⇘c⇙(inf_llist t)))" x] by simp
          ultimately have "⇘c⇙↑⇘t⇙(x) ≥ Suc (⟨c ∧ t⟩)" by simp
          hence "⇘c⇙↑⇘t⇙(x) > ⟨c ∧ t⟩" by simp
          with ‹∀n''>z. ¬ ∥c∥⇘t n''⇙› show ?thesis using lActive_greater_active_all by simp
        qed
        moreover have "⇘c⇙↑⇘t⇙x < n'"
        proof -
          from ‹lfinite (π⇘c⇙(inf_llist t))› have "llength (π⇘c⇙inf_llist t) = the_enat (llength (π⇘c⇙inf_llist t))"
            by (simp add: enat_the_enat llength_eq_infty_conv_lfinite)
          with ‹x ≥ llength (π⇘c⇙(inf_llist t))› have "x≥the_enat (llength (π⇘c⇙inf_llist t))"
            using enat_ord_simps(1) by fastforce
          moreover from ‹∃i≥n. ∥c∥⇘t i⇙› have "llength (π⇘c⇙inf_llist t)≥1" using proj_one by force
          ultimately have "the_enat (llength (π⇘c⇙inf_llist t)) - 1 ≤ x" by simp
          with ‹x < (⇘c⇙↓⇘t⇙(n'))› show ?thesis using c2p_mono_p2c_strict by simp
        qed
        ultimately have "eval c t t' (⇘c⇙↑⇘t⇙(x)) γ'" using a2 by blast
        hence "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x)))"
          using validCE_cont[of c t "⇘c⇙↑⇘t⇙(x)" t' γ'] ‹∃i≥n. ∥c∥⇘t i⇙› ‹¬ (∃i'≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i'⇙)› by blast
        moreover from ‹(x ≥ llength (π⇘c⇙(inf_llist t)))›
          have "(enat x ≥ llength (π⇘c⇙(inf_llist t)))" by auto
        with ‹lfinite (π⇘c⇙(inf_llist t))› have "llength (π⇘c⇙(inf_llist t))≠∞"
          using llength_eq_infty_conv_lfinite by auto
        with ‹(x ≥ llength (π⇘c⇙(inf_llist t)))›
          have "the_enat(llength (π⇘c⇙(inf_llist t))) - 1 ≤ x" by auto
        ultimately show ?thesis using cnf2bhv_bhv2cnf[of c t x] by simp
      next
        assume "¬(x ≥ llength (π⇘c⇙(inf_llist t)))"
        hence "x<llength (π⇘c⇙(inf_llist t))" by simp
        then obtain n''::nat where "x=⟨c #⇘n''⇙ inf_llist t⟩" using nAct_exists by blast
        moreover from ‹enat x < llength (π⇘c⇙(inf_llist t))› ‹enat x = ⟨c #⇘enat n''⇙ inf_llist t⟩›
          have "∃i≥n''. ∥c∥⇘t i⇙" using nAct_less_llength_active by force
        then obtain i where "i≥n''" and "∥c∥⇘t i⇙" and "¬ (∃k≥n''. k < i ∧ ∥c∥⇘t k⇙)" 
          using nact_exists by blast
        moreover have "enat i - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
        ultimately have "x=⟨c #⇘i⇙ inf_llist t⟩" using one_enat_def nAct_not_active_same by simp
        moreover have "⟨c #⇘i⇙ inf_llist t⟩≠∞" by simp
        ultimately have "x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)" by fastforce
        from ‹x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)› ‹x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)›
        have "the_enat (⟨c #⇘i⇙ inf_llist t⟩)≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)" by simp
        with ‹∥c∥⇘t i⇙› have "i≥⟨c → t⟩⇘n⇙" using active_geq_nxtAct by simp
        moreover from ‹x=⟨c #⇘i⇙ inf_llist t⟩› ‹x < llength (π⇘c⇙(inf_llist t))›
          have "∃i'. i ≤ enat i' ∧ ∥c∥⇘t i'⇙" using nAct_less_llength_active[of x c "inf_llist t" i] by simp
        hence "∃i'≥i. ∥c∥⇘t i'⇙" by simp
        moreover have "i<n'"
        proof -
          from ‹∃i≥n. ∥c∥⇘t i⇙› ‹¬(∃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
          with ‹x<llength (π⇘c⇙(inf_llist t))› show ?thesis
            using ‹¬ (∃i'≥n'. ∥c∥⇘t i'⇙)› ‹∥c∥⇘t i⇙› le_neq_implies_less nat_le_linear by blast
        qed
        ultimately obtain n''' where "eval c t t' n''' γ'" and "n'''≥⟨c ⇐ t⟩⇘i⇙" and "n'''≤⟨c → t⟩⇘i⇙"
          using a2 by blast
        moreover from ‹∥c∥⇘t i⇙› have "∥c∥⇘t ⟨c → t⟩⇘i⇙⇙" using nxtActI by auto
        with ‹n'''≤⟨c → t⟩⇘i⇙› have "∃i'≥n'''. ∥c∥⇘t i'⇙" using less_or_eq_imp_le by blast
        ultimately have "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘n'''⇙ inf_llist t⟩))"
          using validCE_act[of n''' c t t' γ'] by blast
        moreover from ‹n'''≥⟨c ⇐ t⟩⇘i⇙› and ‹n'''≤⟨c → t⟩⇘i⇙›
          have "the_enat (⟨c #⇘n'''⇙ inf_llist t⟩)=the_enat (⟨c #⇘i⇙ inf_llist t⟩)" using nAct_same by simp
        hence "the_enat (⟨c #⇘n'''⇙ inf_llist t⟩) = x" by (simp add: ‹x = the_enat ⟨c #⇘enat i⇙inf_llist t⟩›)
        ultimately have "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat x)" by simp
        thus ?thesis by simp
      qed
    qed
  qed
  ultimately have "eval c t t' n (λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n'))"
    using ‹∃i≥n. ∥c∥⇘t i⇙› validCI_act[of n c t "λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')" t']
    by blast
  thus ?thesis using until_def by simp
qed
  
lemma untilIN[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' γ"
    and a1: "⋀n''. ⟦n≤n''; n''<n'⟧ ⟹ 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
  moreover have "∀x::nat≥ ⇘c⇙↓⇘t⇙(n). x<⇘c⇙↓⇘t⇙(n') ⟶ γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x"
  proof (rule HOL.allI[OF HOL.impI[OF HOL.impI]])
    fix x assume "x≥⇘c⇙↓⇘t⇙(n)" and "x<⇘c⇙↓⇘t⇙(n')"
  
    from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "⟨c ∧ t⟩ ≤ n" using ‹∃i. ∥c∥⇘t i⇙› lActive_less by auto
    with ‹x≥⇘c⇙↓⇘t⇙(n)› have "⇘c⇙↑⇘t⇙(x) ≥ n" using p2c_mono_c2p by simp
    moreover from ‹⟨c ∧ t⟩ ≤ n› ‹⇘c⇙↓⇘t⇙(n) ≤ x› have "x ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1"
      using cnf2bhv_ge_llength dual_order.trans by blast
    with ‹x<⇘c⇙↓⇘t⇙(n')› have "⇘c⇙↑⇘t⇙(x) < n'" using c2p_mono_p2c_strict[of c t x n'] by simp
    moreover from ‹¬ (∃i≥n. ∥c∥⇘t i⇙)› ‹⇘c⇙↑⇘t⇙(x) ≥ n› have "¬ (∃i''≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i''⇙)" by auto
    ultimately have "eval c t t' (⇘c⇙↑⇘t⇙(x)) γ'" using a1[of "⇘c⇙↑⇘t⇙(x)"] by simp
    with ‹¬ (∃i''≥⇘c⇙↑⇘t⇙x. ∥c∥⇘t i''⇙)›
      have "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x)))"
      using validCE_cont[of c t "⇘c⇙↑⇘t⇙(x)" t' γ'] ‹∃i. ∥c∥⇘t i⇙› by blast
    moreover have "x ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1"
      using ‹⇘c⇙↓⇘t⇙(n) ≤ x› cnf2bhv_def by auto
    ultimately show "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (x)"
      using cnf2bhv_bhv2cnf by simp
  qed   
  ultimately have "eval c t t' n (λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n'))"
    using validCI_cont[of c t n "λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')" t']
    ‹∃i. ∥c∥⇘t i⇙› ‹¬(∃i'≥n. ∥c∥⇘t i'⇙)› by blast
  thus ?thesis using until_def by simp
next
  assume "¬(∃i. ∥c∥⇘t i⇙)"
  with assms have "∃n''≥n. γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n'' ∧
    (∀n'≥n. n' < n'' ⟶ γ' (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'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n'))"
    using validCI_not_act[where γ="λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"] by blast
  thus ?thesis using until_def by simp
qed
  
lemma untilEA[elim]:
  fixes n::nat
    and n'::nat
    and t::"nat ⇒ cnf"
    and t'::"nat ⇒ 'cmp"
    and c::'id
  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'' γ)
      ∧ (∀n''≥⟨c ⇐ t⟩⇘n⇙. n'' < ⟨c ⇐ t⟩⇘n'⇙ ⟶ eval c t t' n'' γ') ∨
    (¬(∃i≥n'. ∥c∥⇘t i⇙)) ∧ eval c t t' n' γ ∧ (∀n''≥⟨c ⇐ t⟩⇘n⇙. n'' < n' ⟶ 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'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n'))" using until_def by simp
  with ‹∃i≥n. ∥c∥⇘t i⇙› obtain x
    where "x≥the_enat ⟨c #⇘enat n⇙inf_llist t⟩" and "γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x"
    and a1: "∀x'≥the_enat ⟨c #⇘enat n⇙inf_llist t⟩. x' < x ⟶ γ' (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) x'"
    using validCE_act[where γ="λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"] by blast
  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
    moreover have "∀n''≥⟨c ⇐ t⟩⇘n⇙. n'' < (⇘c⇙↑⇘t⇙x) ⟶ eval c t t' n'' γ'"
    proof
      fix n'' show "⟨c ⇐ t⟩⇘n⇙ ≤ n'' ⟶ n'' < ⇘c⇙↑⇘t⇙x ⟶ eval c t t' n'' γ'"
      proof (rule HOL.impI[OF HOL.impI])
        assume "⟨c ⇐ t⟩⇘n⇙ ≤ n''" and "n'' < ⇘c⇙↑⇘t⇙x"
        show "eval c t t' n'' γ'"
        proof cases
          assume "∃i≥n''. ∥c∥⇘t i⇙"
          with ‹n''≥⟨c ⇐ t⟩⇘n⇙› have "the_enat (⟨c #⇘n''⇙ inf_llist t⟩) ≥ the_enat (⟨c #⇘n⇙ inf_llist t⟩)"
            using nAct_mono_lNact ‹∃i≥n. ∥c∥⇘t i⇙› by simp
          moreover have "the_enat (⟨c #⇘n''⇙ inf_llist t⟩)<x"
          proof -
            from ‹∃i≥n''. ∥c∥⇘t i⇙› have "eSuc ⟨c #⇘enat n''⇙inf_llist t⟩ ≤ llength (π⇘c⇙inf_llist t)"
              using nAct_llength_proj by auto
            with ‹x ≥ llength (π⇘c⇙(inf_llist t))› have "eSuc ⟨c #⇘enat n''⇙inf_llist t⟩ ≤ x" by simp
            moreover have "⟨c #⇘enat n''⇙inf_llist t⟩≠∞" by simp
            ultimately have "Suc (the_enat(⟨c #⇘enat n''⇙inf_llist t⟩)) ≤ x"
              by (metis enat.distinct(2) the_enat.simps the_enat_eSuc the_enat_mono)
            thus ?thesis by simp
          qed
          ultimately have "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘n''⇙ inf_llist t⟩))"
            using a1 by auto
          with ‹∃i≥n''. ∥c∥⇘t i⇙› show ?thesis using validCI_act by blast      
        next
          assume "¬(∃i≥n''. ∥c∥⇘t i⇙)"
          moreover have "⇘c⇙↓⇘t⇙(n'') ≥ the_enat (⟨c #⇘n⇙ inf_llist t⟩)"
          proof -
            have "⟨c #⇘n⇙ inf_llist t⟩≤llength (π⇘c⇙(inf_llist t))" using nAct_le_proj by metis
            moreover from ‹¬ (∃i≥n''. ∥c∥⇘t i⇙)› have "llength (π⇘c⇙(inf_llist t))≠∞"
              by (metis llength_eq_infty_conv_lfinite lnth_inf_llist proj_finite2)
            ultimately have "the_enat(⟨c #⇘n⇙ inf_llist t⟩)≤the_enat(llength (π⇘c⇙(inf_llist t)))" by simp
            moreover from ‹∃i≥n. ∥c∥⇘t i⇙› ‹¬ (∃i≥n''. ∥c∥⇘t i⇙)› have "n''>⟨c ∧ t⟩"
              using lActive_active by (meson leI le_eq_less_or_eq)
            hence "⇘c⇙↓⇘t⇙(n'') > the_enat (llength (π⇘c⇙(inf_llist t))) - 1" using cnf2bhv_greater_llength by simp
            ultimately show ?thesis by simp
          qed
          moreover from ‹¬(∃i≥n''. ∥c∥⇘t i⇙)› have "⟨c ∧ t⟩ ≤ n''" using assms(1) lActive_less by auto
            with ‹n'' < ⇘c⇙↑⇘t⇙x› have "⇘c⇙↓⇘t⇙(n'')<x" using p2c_mono_c2p_strict by simp
          ultimately have "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(n''))"
            using a1 by auto
          with ‹∃i≥n. ∥c∥⇘t i⇙› ‹¬(∃i≥n''. ∥c∥⇘t i⇙)› show ?thesis using validCI_cont by blast              
        qed
      qed
    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 simp
    then obtain n'::nat where "x=⟨c #⇘n'⇙ inf_llist t⟩" using nAct_exists by blast
    with ‹enat x < llength (π⇘c⇙(inf_llist t))› have "∃i≥n'. ∥c∥⇘t i⇙" using nAct_less_llength_active by force
    then obtain i where "i≥n'" and "∥c∥⇘t i⇙" and "¬ (∃k≥n'. k < i ∧ ∥c∥⇘t k⇙)" using nact_exists by blast
    moreover have "(∀n''≥ ⟨c ⇐ t⟩⇘i⇙. n''≤⟨c → t⟩⇘i⇙ ⟶ eval c t t' n'' γ)"
    proof
      fix n'' show "⟨c ⇐ t⟩⇘i⇙ ≤ n'' ⟶ n'' ≤ ⟨c → t⟩⇘i⇙ ⟶ eval c t t' n'' γ"
      proof(rule HOL.impI[OF HOL.impI])
        assume "⟨c ⇐ t⟩⇘i⇙ ≤ n''" and "n'' ≤ ⟨c → t⟩⇘i⇙"
        hence "the_enat (⟨c #⇘enat i⇙ inf_llist t⟩) = the_enat (⟨c #⇘enat n''⇙ inf_llist t⟩)"
          using nAct_same by simp
        moreover from ‹∥c∥⇘t i⇙› have "∥c∥⇘t ⟨c → t⟩⇘i⇙⇙" using nxtActI by auto
        with ‹n'' ≤ ⟨c → t⟩⇘i⇙› have "∃i≥n''. ∥c∥⇘t i⇙" using dual_order.strict_implies_order by auto
        moreover have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘enat i⇙ inf_llist t⟩))"
        proof -
          have "enat i - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
          with ‹x=⟨c #⇘n'⇙ inf_llist t⟩› ‹i≥n'› ‹¬ (∃k≥n'. k < i ∧ ∥c∥⇘t k⇙)› have "x=⟨c #⇘i⇙ inf_llist t⟩"
            using one_enat_def nAct_not_active_same by simp
          moreover have "⟨c #⇘i⇙ inf_llist t⟩≠∞" by simp
          ultimately have "x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)" by fastforce        
          thus ?thesis using ‹γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x› by blast
        qed
        with ‹the_enat (⟨c #⇘enat i⇙ inf_llist t⟩) = the_enat (⟨c #⇘enat n''⇙ inf_llist t⟩)› have
          "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘enat n''⇙ inf_llist t⟩))" by simp
        ultimately show "eval c t t' n'' γ" using validCI_act by blast
      qed
    qed
    moreover have "i≥⟨c → t⟩⇘n⇙"
    proof -
      have "enat i - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
      with ‹x=⟨c #⇘n'⇙ inf_llist t⟩› ‹i≥n'› ‹¬ (∃k≥n'. k < i ∧ ∥c∥⇘t k⇙)› have "x=⟨c #⇘i⇙ inf_llist t⟩"
        using one_enat_def nAct_not_active_same by simp
      moreover have "⟨c #⇘i⇙ inf_llist t⟩≠∞" by simp
      ultimately have "x=the_enat(⟨c #⇘i⇙ inf_llist t⟩)" by fastforce        
      with ‹x≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)›
        have "the_enat (⟨c #⇘i⇙ inf_llist t⟩)≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)" by simp
      with ‹∥c∥⇘t i⇙› show ?thesis using active_geq_nxtAct by simp
    qed
    moreover have "∀n''≥⟨c ⇐ t⟩⇘n⇙. n'' < ⟨c ⇐ t⟩⇘i⇙ ⟶ eval c t t' n'' γ'"
    proof
      fix n'' show "⟨c ⇐ t⟩⇘n⇙ ≤ n'' ⟶ n'' < ⟨c ⇐ t⟩⇘i⇙ ⟶ eval c t t' n'' γ'"
      proof (rule HOL.impI[OF HOL.impI])
        assume "⟨c ⇐ t⟩⇘n⇙ ≤ n''" and "n'' < ⟨c ⇐ t⟩⇘i⇙"
        moreover have "⟨c ⇐ t⟩⇘i⇙≤i" by simp
        ultimately have "∃i≥n''. ∥c∥⇘t i⇙" using ‹∥c∥⇘t i⇙› by (meson less_le less_le_trans)
        with ‹n''≥⟨c ⇐ t⟩⇘n⇙› have "the_enat (⟨c #⇘n''⇙ inf_llist t⟩) ≥ the_enat (⟨c #⇘n⇙ inf_llist t⟩)"
          using nAct_mono_lNact ‹∃i≥n. ∥c∥⇘t i⇙› by simp
        moreover have "the_enat (⟨c #⇘n''⇙ inf_llist t⟩) < x"
        proof -
          from ‹n'' < ⟨c ⇐ t⟩⇘i⇙› ‹⟨c ⇐ t⟩⇘i⇙ ≤ i› have "n'' < i" using dual_order.strict_trans1 by arith
          with ‹n'' < ⟨c ⇐ t⟩⇘i⇙› have "∃i'≥n''. i' < i ∧ ∥c∥⇘t i'⇙" using lNact_least[of i n''] by fastforce
          hence "⟨c #⇘n''⇙ inf_llist t⟩ < ⟨c #⇘i⇙ inf_llist t⟩" using nAct_less by auto
          moreover have "enat i - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
          with ‹x=⟨c #⇘n'⇙ inf_llist t⟩› ‹i≥n'› ‹¬ (∃k≥n'. k < i ∧ ∥c∥⇘t k⇙)› have "x=⟨c #⇘i⇙ inf_llist t⟩"
            using one_enat_def nAct_not_active_same by simp    
          moreover have "⟨c #⇘n''⇙ inf_llist t⟩≠∞" by simp
          ultimately show ?thesis by (metis enat_ord_simps(2) enat_the_enat)
        qed
        ultimately have "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (the_enat (⟨c #⇘n''⇙ inf_llist t⟩))"
          using a1 by auto
        with ‹∃i≥n''. ∥c∥⇘t i⇙› show "eval c t t' n'' γ'" using validCI_act by blast
      qed
    qed
    ultimately show ?thesis using ‹∥c∥⇘t i⇙› by auto
  qed    
qed

lemma untilEN[elim]:
  fixes n::nat
    and n'::nat
    and t::"nat ⇒ cnf"
    and t'::"nat ⇒ 'cmp"
    and c::'id
  assumes "∄i. i≥n ∧ ∥c∥⇘t i⇙"
    and "eval c t t' n (γ' 𝔘⇩b γ)"
  shows "∃n'≥n. eval c t t' n' γ ∧
    (∀n''≥n. n'' < n' ⟶ eval c t t' n'' γ')"
proof cases
  assume "∃i. ∥c∥⇘t i⇙"
  moreover from ‹eval c t t' n (γ' 𝔘⇩b γ)›
    have "eval c t t' n (λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n'))" using until_def by simp
  ultimately have "∃n''≥⇘c⇙↓⇘t⇙(n). γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n'' ∧
    (∀n'≥⇘c⇙↓⇘t⇙(n). n' < n'' ⟶ γ' (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n')"
    using validCE_cont[where γ="λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"]
    ‹∄i. i≥n ∧ ∥c∥⇘t i⇙› by blast
  then obtain x where "x≥⇘c⇙↓⇘t⇙(n)" and "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x"
    and "∀x'≥⇘c⇙↓⇘t⇙(n). x'<x ⟶ γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x'" by auto
  moreover from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "the_enat (llength (π⇘c⇙(inf_llist t))) - 1 < x"
  proof -
    have "⟨c ∧ t⟩ < n"
    proof (rule ccontr)
      assume "¬⟨c ∧ t⟩ < n"
      hence "⟨c ∧ t⟩ ≥ n" by simp
      moreover from ‹∃i. ∥c∥⇘t i⇙› ‹¬ (∃i≥n. ∥c∥⇘t i⇙)› have "∥c∥⇘t ⟨c ∧ t⟩⇙"
        using lActive_active less_or_eq_imp_le by blast
      ultimately show False using ‹¬ (∃i≥n. ∥c∥⇘t i⇙)› by simp
    qed
    hence "the_enat (llength (π⇘c⇙(inf_llist t))) - 1 < ⇘c⇙↓⇘t⇙(n)" using cnf2bhv_greater_llength by simp
    with ‹x≥⇘c⇙↓⇘t⇙(n)› show ?thesis by simp
  qed
  hence "x = ⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x))" using cnf2bhv_bhv2cnf by simp
  ultimately have "γ (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x)))" by simp
  moreover from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "¬(∃i≥⇘c⇙↑⇘t⇙(x). ∥c∥⇘t i⇙)"
  proof -
    from ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "lfinite (π⇘c⇙(inf_llist t))" using proj_finite2 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 validCI_cont ‹∃i. ∥c∥⇘t i⇙› by blast
  moreover from ‹∃i. ∥c∥⇘t i⇙› ‹¬(∃i≥n. ∥c∥⇘t i⇙)› have "⟨c ∧ t⟩ ≤ n" using lActive_less[of c t _ n] by auto
  with ‹x≥⇘c⇙↓⇘t⇙(n)› have "n ≤ ⇘c⇙↑⇘t⇙(x)" using p2c_mono_c2p by blast
  moreover have "∀n''≥n. n'' < ⇘c⇙↑⇘t⇙(x) ⟶ eval c t t' n'' γ'"
  proof (rule HOL.allI[OF HOL.impI[OF HOL.impI]])
    fix n'' assume "n ≤ n''" and "n'' < ⇘c⇙↑⇘t⇙(x)"
    hence "⇘c⇙↓⇘t⇙(n'')≥⇘c⇙↓⇘t⇙(n)" using cnf2bhv_mono by simp
    moreover have "n''<⇘c⇙↑⇘t⇙(x)" by (simp add: ‹n'' < ⇘c⇙↑⇘t⇙x›)
    with ‹⟨c ∧ t⟩ ≤ n› ‹n ≤ n''› have "⇘c⇙↓⇘t⇙(n'')<⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x))" using cnf2bhv_mono_strict by simp
    with ‹x = ⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(x))› have "⇘c⇙↓⇘t⇙(n'')< x" by simp
    ultimately have "γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) (⇘c⇙↓⇘t⇙(n''))"
      using ‹∀x'≥⇘c⇙↓⇘t⇙(n). x'<x ⟶ γ' (lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t'))) x'› by simp
    moreover from ‹n ≤ n''› have "∄i. i≥n'' ∧ ∥c∥⇘t i⇙" using ‹∄i. i≥n ∧ ∥c∥⇘t i⇙› by simp
    ultimately show "eval c t t' n'' γ'" using validCI_cont using ‹∃i. ∥c∥⇘t i⇙› by blast
  qed
  ultimately show ?thesis by auto
next
  assume "¬(∃i. ∥c∥⇘t i⇙)"
  moreover from ‹eval c t t' n (γ' 𝔘⇩b γ)›
    have "eval c t t' n (λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n'))" using until_def by simp
  ultimately have "∃n''≥n. γ (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n''
    ∧ (∀n'≥n. n' < n'' ⟶ γ' (lnth (π⇘c⇙inf_llist t @⇩l inf_llist t')) n')" using ‹¬(∃i. ∥c∥⇘t i⇙)›
    validCE_not_act[where γ="λ t n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"] by blast
  with ‹¬(∃i. ∥c∥⇘t i⇙)› show ?thesis using validCI_not_act by blast
qed
  
subsubsection "Weak Until"

definition wuntil :: "('cmp bta) ⇒ ('cmp bta) ⇒ ('cmp bta)" (infixl ‹𝔚⇩b› 20)
  where "γ' 𝔚⇩b γ ≡ γ' 𝔘⇩b γ ∨⇧b □⇩b(γ')"

end
  
end