Theory Configuration_Traces

(*
  Title:      Configuration_Traces.thy
  Author:     Diego Marmsoler
*)
section "A Theory of Dynamic Architectures"
text ‹
  The following theory formalizes configuration traces~\<^cite>‹"Marmsoler2016a" and "Marmsoler2016"› as a model for dynamic architectures.
  Since configuration traces may be finite as well as infinite, the theory depends on Lochbihler's theory of co-inductive lists~\<^cite>‹"Lochbihler2010"›.
›
theory Configuration_Traces
  imports Coinductive.Coinductive_List
begin
text ‹
  In the following we first provide some preliminary results for natural numbers, extended natural numbers, and lazy lists.
  Then, we introduce a locale @text{dynamic\_architectures} which introduces basic definitions and corresponding properties for dynamic architectures.
›
  
subsection "Natural Numbers"
text ‹
  We provide one additional property for natural numbers.
›
lemma boundedGreatest:
  assumes "P (i::nat)"
    and "∀n' > n. ¬ P n'"
  shows "∃i'≤n. P i' ∧ (∀n'. P n' ⟶ n'≤i')"
proof -
  have "P (i::nat) ⟹ n≥i ⟹ ∀n' > n. ¬ P n' ⟹ (∃i'≤n. P i' ∧ (∀n'≤n. P n' ⟶ n'≤i'))"
  proof (induction n)
    case 0
    then show ?case by auto
  next
    case (Suc n)
    then show ?case
    proof cases
      assume "i = Suc n"
      then show ?thesis using Suc.prems by auto
    next
      assume "¬(i = Suc n)"
      thus ?thesis
      proof cases
        assume "P (Suc n)"
        thus ?thesis by auto
      next
        assume "¬ P (Suc n)"
        with Suc.prems have "∀n' > n. ¬ P n'" using Suc_lessI by blast
        moreover from ‹¬(i = Suc n)› have "i ≤ n" and "P i" using Suc.prems by auto
        ultimately obtain i' where "i'≤n ∧ P i' ∧ (∀n'≤n. P n' ⟶ n' ≤ i')" using Suc.IH by blast
        hence "i' ≤ n" and "P i'" and "(∀n'≤n. P n' ⟶ n' ≤ i')" by auto
        thus ?thesis by (metis le_SucI le_Suc_eq)
      qed
    qed
  qed
  moreover have "n≥i"
  proof (rule ccontr)
    assume "¬ (n ≥ i)"
    hence "n < i" by arith
    thus False using assms by blast
  qed
  ultimately obtain i' where "i'≤n" and "P i'" and "∀n'≤n. P n' ⟶ n' ≤ i'" using assms by blast
  with assms have "∀n'. P n' ⟶ n' ≤ i'" using not_le_imp_less by blast
  with ‹i' ≤ n› and ‹P i'› show ?thesis by auto
qed

subsection "Extended Natural Numbers"
text ‹
  We provide one simple property for the \emph{strict} order over extended natural numbers.
›
lemma enat_min:
  assumes "m ≥ enat n'"
    and "enat n < m - enat n'"
  shows "enat n + enat n' < m" 
  using assms by (metis add.commute enat.simps(3) enat_add_mono enat_add_sub_same le_iff_add)

subsection "Lazy Lists"
text ‹
  In the following we provide some additional notation and properties for lazy lists.
›
notation LNil (‹[]⇩l›)
notation LCons (infixl ‹#⇩l› 60)
notation lappend (infixl ‹@⇩l› 60)

lemma lnth_lappend[simp]:
  assumes "lfinite xs"
    and "¬ lnull ys"
  shows "lnth (xs @⇩l ys) (the_enat (llength xs)) = lhd ys"
proof -
  from assms have "∃k. llength xs = enat k" using lfinite_conv_llength_enat by auto
  then obtain k where "llength xs = enat k" by blast
  hence "lnth (xs @⇩l ys) (the_enat (llength xs)) = lnth ys 0"
    using lnth_lappend2[of xs k k ys] by simp
  with assms show ?thesis using lnth_0_conv_lhd by simp
qed

lemma lfilter_ltake:
  assumes "∀(n::nat)≤llength xs. n≥i ⟶ (¬ P (lnth xs n))"
  shows "lfilter P xs = lfilter P (ltake i xs)"
proof -
  have "lfilter P xs = lfilter P ((ltake i xs) @⇩l (ldrop i xs))"
    using lappend_ltake_ldrop[of "(enat i)" xs] by simp
  hence "lfilter P xs = (lfilter P ((ltake i) xs)) @⇩l (lfilter P (ldrop i xs))" by simp
  show ?thesis
  proof cases
    assume "enat i ≤ llength xs"
  
    have "∀x<llength (ldrop i xs). ¬ P (lnth (ldrop i xs) x)"
    proof (rule allI)
      fix x show "enat x < llength (ldrop (enat i) xs) ⟶ ¬ P (lnth (ldrop (enat i) xs) x)"
      proof
        assume "enat x < llength (ldrop (enat i) xs)"
        moreover have "llength (ldrop (enat i) xs) = llength xs - enat i"
          using llength_ldrop[of "enat i"] by simp
        ultimately have "enat x < llength xs - enat i" by simp
        with ‹enat i ≤ llength xs› have "enat x + enat i < llength xs"
          using enat_min[of i "llength xs" x] by simp
        moreover have "enat i + enat x = enat x + enat i" by simp
        ultimately have "enat i + enat x < llength xs" by arith
        hence "i + x < llength xs" by simp
        hence "lnth (ldrop i xs) x = lnth xs (x + the_enat i)" using lnth_ldrop[of "enat i" "x" xs] by simp
        moreover have "x + i ≥ i" by simp
        with assms ‹i + x < llength xs› have "¬ P (lnth xs (x + the_enat i))"
          by (simp add: assms(1) add.commute)
        ultimately show "¬ P (lnth (ldrop i xs) x)" using assms by simp
      qed
    qed
    hence "lfilter P (ldrop i xs) = []⇩l" by (metis diverge_lfilter_LNil in_lset_conv_lnth)
    with ‹lfilter P xs = (lfilter P ((ltake i) xs)) @⇩l (lfilter P (ldrop i xs))›
      show "lfilter P xs = lfilter P (ltake i xs)" by simp
  next
    assume "¬ enat i ≤ llength xs"
    hence "enat i > llength xs" by simp
    hence "ldrop i xs = []⇩l" by simp
    hence "lfilter P (ldrop i xs) = []⇩l" using lfilter_LNil[of P] by arith
    with ‹lfilter P xs = (lfilter P ((ltake i) xs)) @⇩l (lfilter P (ldrop i xs))›
      show "lfilter P xs = lfilter P (ltake i xs)" by simp        
  qed
qed

lemma lfilter_lfinite[simp]:
  assumes "lfinite (lfilter P t)"
    and "¬ lfinite t"
  shows "∃n. ∀n'>n. ¬ P (lnth t n')"
proof -
  from assms have "finite {n. enat n < llength t ∧ P (lnth t n)}" using lfinite_lfilter by auto
  then obtain k
    where sset: "{n. enat n < llength t ∧ P (lnth t n)} ⊆ {n. n<k ∧ enat n < llength t ∧ P (lnth t n)}"
    using finite_nat_bounded[of "{n. enat n < llength t ∧ P (lnth t n)}"] by auto
  show ?thesis
  proof (rule ccontr)
    assume "¬(∃n. ∀n'>n. ¬ P (lnth t n'))"
    hence "∀n. ∃n'>n. P (lnth t n')" by simp
    then obtain n' where "n'>k" and "P (lnth t n')" by auto
    moreover from ‹¬ lfinite t› have "n' < llength t" by (simp add: not_lfinite_llength)
    ultimately have "n' ∉ {n. n<k ∧ enat n < llength t ∧ P (lnth t n)}" and
      "n'∈{n. enat n < llength t ∧ P (lnth t n)}" by auto
    with sset show False by auto
  qed
qed

subsection "Specifying Dynamic Architectures"
text ‹
  In the following we formalize dynamic architectures in terms of configuration traces, i.e., sequences of architecture configurations.
  Moreover, we introduce definitions for operations to support the specification of configuration traces.
›
typedecl cnf
type_synonym trace = "nat ⇒ cnf"
consts arch:: "trace set"

type_synonym cta = "trace ⇒ nat ⇒ bool"

subsubsection "Implication"

definition imp :: "cta ⇒ cta ⇒ cta" (infixl ‹⟶⇧c› 10)
  where "γ ⟶⇧c γ' ≡ λ t n. γ t n ⟶ γ' t n"

declare imp_def[simp]

lemma impI[intro!]:
  fixes t n
  assumes "γ t n ⟹ γ' t n"
  shows "(γ ⟶⇧c γ') t n" using assms by simp

lemma impE[elim!]:
  fixes t n
  assumes "(γ ⟶⇧c γ') t n" and "γ t n" and "γ' t n ⟹ γ'' t n"
  shows "γ'' t n" using assms by simp

subsubsection "Disjunction"  
    
definition disj :: "cta ⇒ cta ⇒ cta" (infixl ‹∨⇧c› 15)
  where "γ ∨⇧c γ' ≡ λ t n. γ t n ∨ γ' t n"

declare disj_def[simp]

lemma disjI1[intro]:
  assumes "γ t n"
  shows "(γ ∨⇧c γ') t n" using assms by simp

lemma disjI2[intro]:
  assumes "γ' t n"
  shows "(γ ∨⇧c γ') t n" using assms by simp

lemma disjE[elim!]:
  assumes "(γ ∨⇧c γ') t n"
    and "γ t n ⟹ γ'' t n"
    and "γ' t n ⟹ γ'' t n"
  shows "γ'' t n" using assms by auto

subsubsection "Conjunction"
  
definition conj :: "cta ⇒ cta ⇒ cta" (infixl ‹∧⇧c› 20)
  where "γ ∧⇧c γ' ≡ λ t n. γ t n ∧ γ' t n"

declare conj_def[simp]

lemma conjI[intro!]:
  fixes n
  assumes "γ t n" and "γ' t n"
  shows "(γ ∧⇧c γ') t n" using assms by simp

lemma conjE[elim!]:
  fixes n
  assumes "(γ ∧⇧c γ') t n" and "γ t n ⟹ γ' t n ⟹ γ'' t n"
  shows "γ'' t n" using assms by simp

subsubsection "Negation"
  
definition neg :: "cta ⇒ cta" (‹¬⇧c _› [19] 19)
  where "¬⇧c γ ≡ λ t n. ¬ γ t n"

declare neg_def[simp]

lemma negI[intro!]:
  assumes "γ t n ⟹ False"
  shows "(¬⇧c γ) t n" using assms by auto

lemma negE[elim!]:
  assumes "(¬⇧c γ) t n"
    and "γ t n"
  shows "γ' t n" using assms by simp

subsubsection "Quantifiers"

definition all :: "('a ⇒ cta)
  ⇒ cta" (binder ‹∀⇩c› 10)
  where "all P ≡ λt n. (∀y. (P y t n))"

declare all_def[simp]

lemma allI[intro!]:
  assumes "⋀x. γ x t n"
  shows "(∀⇩cx. γ x) t n" using assms by simp

lemma allE[elim!]:
  fixes n
  assumes "(∀⇩cx. γ x) t n" and "γ x t n ⟹ γ' t n"
  shows "γ' t n" using assms by simp

definition ex :: "('a ⇒ cta)
  ⇒ cta" (binder ‹∃⇩c› 10)
  where "ex P ≡ λt n. (∃y. (P y t n))"

declare ex_def[simp]

lemma exI[intro!]:
  assumes "γ x t n"
  shows "(∃⇩cx. γ x) t n" using assms HOL.exI by simp

lemma exE[elim!]:
  assumes "(∃⇩cx. γ x) t n" and "⋀x. γ x t n ⟹ γ' t n"
  shows "γ' t n" using assms HOL.exE by auto

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

definition ca :: "(cnf ⇒ bool) ⇒ cta"
  where "ca φ ≡ λ t n. φ (t n)"

lemma caI[intro]:
  fixes n
  assumes "φ (t n)"
  shows "(ca φ) t n" using assms ca_def by simp

lemma caE[elim]:
  fixes n
  assumes "(ca φ) t n"
  shows "φ (t n)" using assms ca_def by simp

subsubsection "Next Operator"

definition nxt :: "cta ⇒ cta" (‹○⇩c(_)› 24)
  where "○⇩c(γ) ≡ λ(t::(nat ⇒ cnf)) n. γ t (Suc n)"

subsubsection "Eventually Operator"  

definition evt :: "cta ⇒ cta" (‹◇⇩c(_)› 23)
  where "◇⇩c(γ) ≡ λ(t::(nat ⇒ cnf)) n. ∃n'≥n. γ t n'"

subsubsection "Globally Operator"

definition glob :: "cta ⇒ cta" (‹□⇩c(_)› 22)
  where "□⇩c(γ) ≡ λ(t::(nat ⇒ cnf)) n. ∀n'≥n. γ t n'"

lemma globI[intro!]:
  fixes n'
  assumes "∀n≥n'. γ t n"
  shows "(□⇩c(γ)) t n'" using assms glob_def by simp

lemma globE[elim!]:
  fixes n n'
  assumes "(□⇩c(γ)) t n" and "n'≥n"
  shows "γ t n'" using assms glob_def by simp

subsubsection "Until Operator"

definition until :: "cta ⇒ cta ⇒ cta" (infixl ‹𝔘⇩c› 21)
  where "γ' 𝔘⇩c γ ≡ λ(t::(nat ⇒ cnf)) n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"

lemma untilI[intro]:
  fixes n
  assumes "∃n''≥n. γ t n'' ∧ (∀n'≥n. n'<n'' ⟶ γ' t n')"
  shows "(γ' 𝔘⇩c γ) t n" using assms until_def by simp

lemma untilE[elim]:
  fixes n
  assumes "(γ' 𝔘⇩c γ) t n"
  shows "∃n''≥n. γ t n'' ∧ (∀n'≥n. n'<n'' ⟶ γ' t n')" using assms until_def by simp

subsubsection "Weak Until"

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

lemma wUntilI[intro]:
  fixes n
  assumes "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n'<n'' ⟶ γ' t n')) ∨ (∀n'≥n. γ' t n')"
  shows "(γ' 𝔚⇩c γ) t n" using assms wuntil_def by auto

lemma wUntilE[elim]:
  fixes n n'
  assumes "(γ' 𝔚⇩c γ) t n"
  shows "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n'<n'' ⟶ γ' t n')) ∨ (∀n'≥n. γ' t n')"
proof -
  from assms have "(γ' 𝔘⇩c γ ∨⇧c □⇩c(γ')) t n" using wuntil_def by simp
  hence "(γ' 𝔘⇩c γ) t n ∨ (□⇩c(γ')) t n" by simp
  thus ?thesis
  proof
    assume "(γ' 𝔘⇩c γ) t n"
    hence "∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')" by auto
    thus ?thesis by auto
  next
    assume "(□⇩cγ') t n"
    hence "∀n'≥n. γ' t n'" by auto
    thus ?thesis by auto
  qed
qed

lemma wUntil_Glob:
  assumes "(γ' 𝔚⇩c γ) t n"
    and "(□⇩c(γ' ⟶⇧c γ'')) t n"
  shows "(γ'' 𝔚⇩c γ) t n"
proof
  from assms(1) have "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')) ∨ (∀n'≥n. γ' t n')" using wUntilE by simp
  thus "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ'' t n')) ∨ (∀n'≥n. γ'' t n')"
  proof
    assume "∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"
    show "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ'' t n')) ∨ (∀n'≥n. γ'' t n')"
    proof -
      from ‹∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')› obtain n'' where "n''≥n" and "γ t n''" and a1: "∀n'≥n. n' < n'' ⟶ γ' t n'" by auto
      moreover have "∀n'≥n. n' < n'' ⟶ γ'' t n'"
      proof
        fix n'
        show "n'≥n ⟶ n'< n'' ⟶ γ'' t n'"
        proof (rule HOL.impI[OF HOL.impI])
          assume "n'≥n" and "n'<n''"
          with assms(2) have "(γ' ⟶⇧c γ'') t n'" using globE by simp
          hence "γ' t n' ⟶ γ'' t n'" using impE by auto
          moreover from a1 ‹n'≥n› ‹n'<n''› have "γ' t n'" by simp
          ultimately show "γ'' t n'" by simp
        qed
      qed
      ultimately show ?thesis by auto
    qed
  next
    assume a1: "∀n'≥n. γ' t n'"
    have "∀n'≥n. γ'' t n'"
    proof
      fix n'
      show "n'≥n ⟶ γ'' t n'"
      proof
        assume "n'≥n"
        with assms(2) have "(γ' ⟶⇧c γ'') t n'" using globE by simp
        hence "γ' t n' ⟶ γ'' t n'" using impE by auto
        moreover from a1 ‹n'≥n› have "γ' t n'" by simp
        ultimately show "γ'' t n'" by simp
      qed
    qed
    thus "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ'' t n')) ∨ (∀n'≥n. γ'' t n')" by simp
  qed
qed

subsection "Dynamic Components"
text ‹
  To support the specification of patterns over dynamic architectures we provide a locale for dynamic components.
  It takes the following type parameters:
  \begin{itemize}
    \item id: a type for component identifiers
    \item cmp: a type for components
    \item cnf: a type for architecture configurations
  \end{itemize}
›
locale dynamic_component =
  fixes tCMP :: "'id ⇒ cnf ⇒ 'cmp" (‹σ⇘_⇙(_)› [0,110]60)
    and active :: "'id ⇒ cnf ⇒ bool" (‹∥_∥⇘_⇙› [0,110]60)
begin
  
text ‹
  The locale requires two parameters:
  \begin{itemize}
    \item @{term tCMP} is an operator to obtain a component with a certain identifier from an architecture configuration.
    \item @{term active} is a predicate to assert whether a certain component is activated within an architecture configuration.
  \end{itemize}
›

text ‹
  The locale provides some general properties about its parameters and introduces six important operators over configuration traces:
  \begin{itemize}
    \item An operator to extract the behavior of a certain component out of a given configuration trace.
    \item An operator to obtain the number of activations of a certain component within a given configuration trace.
    \item An operator to obtain the least point in time (before a certain point in time) from which on a certain component is not activated anymore.
    \item An operator to obtain the latest point in time where a certain component was activated.
    \item Two operators to map time-points between configuration traces and behavior traces.
  \end{itemize}
  Moreover, the locale provides several properties about the operators and their relationships.
›

lemma nact_active:
  fixes t::"nat ⇒ cnf"
    and n::nat
    and n''
    and id
  assumes "∥id∥⇘t n⇙"
    and "n'' ≥ n"    
    and "¬ (∃n'≥n. n' < n'' ∧ ∥id∥⇘t n'⇙)"    
  shows "n=n''"
  using assms le_eq_less_or_eq by auto

lemma nact_exists:
  fixes t::"nat ⇒ cnf"
  assumes "∃i≥n. ∥c∥⇘t i⇙"
  shows "∃i≥n. ∥c∥⇘t i⇙ ∧ (∄k. n≤k ∧ k<i ∧ ∥c∥⇘t k⇙)"
proof -
  let ?L = "LEAST i. (i≥n ∧ ∥c∥⇘t i⇙)"
  from assms have "?L≥n ∧ ∥c∥⇘t ?L⇙" using LeastI[of "λx::nat. (x≥n ∧ ∥c∥⇘t x⇙)"] by auto
  moreover have "∄k. n≤k ∧ k<?L ∧ ∥c∥⇘t k⇙" using not_less_Least by auto
  ultimately show ?thesis by blast
qed

lemma lActive_least:
  assumes "∃i≥n. i < llength t ∧ ∥c∥⇘lnth t i⇙"
  shows "∃i≥n. (i < llength t ∧ ∥c∥⇘lnth t i⇙ ∧ (∄k. n≤k ∧ k<i ∧ k<llength t ∧ ∥c∥⇘lnth t k⇙))"
proof -
  let ?L = "LEAST i. (i≥n ∧ i < llength t ∧ ∥c∥⇘lnth t i⇙)"
  from assms have "?L≥n ∧ ?L < llength t ∧ ∥c∥⇘lnth t ?L⇙"
    using LeastI[of "λx::nat.(x≥n ∧ x<llength t ∧ ∥c∥⇘lnth t x⇙)"] by auto
  moreover have "∄k. n≤k ∧ k<llength t ∧ k<?L ∧ ∥c∥⇘lnth t k⇙" using not_less_Least by auto
  ultimately show ?thesis by blast
qed

subsection "Projection"
text ‹
  In the following we introduce an operator which extracts the behavior of a certain component out of a given configuration trace.
›

definition proj:: "'id ⇒ (cnf llist) ⇒ ('cmp llist)" (‹π⇘_⇙(_)› [0,110]60) 
  where "proj c = lmap (λcnf. (σ⇘c⇙(cnf))) ∘ (lfilter (active c))"

lemma proj_lnil [simp,intro]:
  "π⇘c⇙([]⇩l) = []⇩l" using proj_def by simp

lemma proj_lnull [simp]:
  "π⇘c⇙(t) = []⇩l ⟷ (∀k ∈ lset t. ¬ ∥c∥⇘k⇙)"
proof
  assume "π⇘c⇙(t) = []⇩l"
  hence "lfilter (active c) t = []⇩l" using proj_def lmap_eq_LNil by auto
  thus "∀k ∈ lset t. ¬ ∥c∥⇘k⇙" using lfilter_eq_LNil[of "active c"] by simp
next
  assume "∀k∈lset t. ¬ ∥c∥⇘k⇙"
  hence "lfilter (active c) t = []⇩l" by simp
  thus "π⇘c⇙(t) = []⇩l" using proj_def by simp
qed
  
lemma proj_LCons [simp]:
  "π⇘i⇙(x #⇩l xs) = (if ∥i∥⇘x⇙ then (σ⇘i⇙(x)) #⇩l (π⇘i⇙(xs)) else π⇘i⇙(xs))"
  using proj_def by simp
    
lemma proj_llength[simp]:
  "llength (π⇘c⇙(t)) ≤ llength t"
  using llength_lfilter_ile proj_def by simp

lemma proj_ltake:
  assumes "∀(n'::nat)≤llength t. n'≥n ⟶ (¬ ∥c∥⇘lnth t n'⇙)"
  shows "π⇘c⇙(t) = π⇘c⇙(ltake n t)" using lfilter_ltake proj_def assms by (metis comp_apply)
    
lemma proj_finite_bound:
  assumes "lfinite (π⇘c⇙(inf_llist t))"
  shows "∃n. ∀n'>n. ¬ ∥c∥⇘t n'⇙"
  using assms lfilter_lfinite[of "active c" "inf_llist t"] proj_def by simp

subsubsection "Monotonicity and Continuity"

lemma proj_mcont:
  shows "mcont lSup lprefix lSup lprefix (proj c)"
proof -
  have "mcont lSup lprefix lSup lprefix (λx. lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) x))"
    by simp
  moreover have "(λx. lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) x)) =
    lmap (λcnf. σ⇘c⇙(cnf)) ∘ lfilter (active c)" by auto
  ultimately show ?thesis using proj_def by simp
qed

lemma proj_mcont2mcont:
  assumes "mcont lub ord lSup lprefix f"
  shows "mcont lub ord lSup lprefix (λx. π⇘c⇙(f x))"
proof -
  have "mcont lSup lprefix lSup lprefix (proj c)" using proj_mcont by simp
  with assms show ?thesis using llist.mcont2mcont[of lSup lprefix "proj c"] by simp
qed
    
lemma proj_mono_prefix[simp]:
  assumes "lprefix t t'"
  shows "lprefix (π⇘c⇙(t)) (π⇘c⇙(t'))"
proof -
  from assms have "lprefix (lfilter (active c) t) (lfilter (active c) t')" using lprefix_lfilterI by simp
  hence "lprefix (lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) t))
    (lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) t'))" using lmap_lprefix by simp
  thus ?thesis using proj_def by simp
qed
 
subsubsection "Finiteness"
    
lemma proj_finite[simp]:
  assumes "lfinite t"
  shows "lfinite (π⇘c⇙(t))"
  using assms proj_def by simp

lemma proj_finite2:
  assumes "∀(n'::nat)≤llength t. n'≥n ⟶ (¬ ∥c∥⇘lnth t n'⇙)"
  shows "lfinite (π⇘c⇙(t))" using assms proj_ltake proj_finite by simp

lemma proj_append_lfinite[simp]:
  fixes t t'
  assumes "lfinite t"
  shows "π⇘c⇙(t @⇩l t') = (π⇘c⇙(t)) @⇩l (π⇘c⇙(t'))" (is "?lhs=?rhs")
proof -
  have "?lhs = (lmap (λcnf. σ⇘c⇙(cnf)) ∘ (lfilter (active c))) (t @⇩l t')" using proj_def by simp
  also have "… = lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) (t @⇩l t'))" by simp
  also from assms have "… = lmap (λcnf. σ⇘c⇙(cnf))
    ((lfilter (active c) t) @⇩l (lfilter (active c) t'))" by simp
  also have "… = (@⇩l) (lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) t))
    (lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) t'))" using lmap_lappend_distrib by simp
  also have "… = ?rhs" using proj_def by simp
  finally show ?thesis .
qed
  
lemma proj_one:
  assumes "∃i. i < llength t ∧ ∥c∥⇘lnth t i⇙"
  shows "llength (π⇘c⇙(t)) ≥ 1"
proof -
  from assms have "∃x∈lset t. ∥c∥⇘x⇙" using lset_conv_lnth by force
  hence "¬ lfilter (λk. ∥c∥⇘k⇙) t = []⇩l" using lfilter_eq_LNil[of "(λk. ∥c∥⇘k⇙)"] by blast
  hence "¬ π⇘c⇙(t) = []⇩l" using proj_def by fastforce
  thus ?thesis by (simp add: ileI1 lnull_def one_eSuc)
qed

subsubsection "Projection not Active"
  
lemma proj_not_active[simp]:
  assumes "enat n < llength t"
    and "¬ ∥c∥⇘lnth t n⇙"
  shows "π⇘c⇙(ltake (Suc n) t) = π⇘c⇙(ltake n t)" (is "?lhs = ?rhs")
proof -
  from assms have "ltake (enat (Suc n)) t = (ltake (enat n) t) @⇩l ((lnth t n) #⇩l []⇩l)"
    using ltake_Suc_conv_snoc_lnth by blast
  hence "?lhs = π⇘c⇙((ltake (enat n) t) @⇩l ((lnth t n) #⇩l []⇩l))" by simp
  moreover have "… = (π⇘c⇙(ltake (enat n) t)) @⇩l (π⇘c⇙((lnth t n) #⇩l []⇩l))" by simp
  moreover from assms have "π⇘c⇙((lnth t n) #⇩l []⇩l) = []⇩l" by simp
  ultimately show ?thesis by simp
qed

lemma proj_not_active_same:
  assumes "enat n ≤ (n'::enat)"
      and "¬ lfinite t ∨ n'-1 < llength t"
      and "∄k. k≥n ∧ k<n' ∧ k < llength t ∧ ∥c∥⇘lnth t k⇙"
    shows "π⇘c⇙(ltake n' t) = π⇘c⇙(ltake n t)"
proof -
  have "π⇘c⇙(ltake (n + (n' - n)) t) = π⇘c⇙((ltake n t) @⇩l (ltake (n'-n) (ldrop n t)))"
    by (simp add: ltake_plus_conv_lappend)
  hence "π⇘c⇙(ltake (n + (n' - n)) t) =
    (π⇘c⇙(ltake n t)) @⇩l (π⇘c⇙(ltake (n'-n) (ldrop n t)))" by simp
  moreover have "π⇘c⇙(ltake (n'-n) (ldrop n t)) = []⇩l"
  proof -
    have "∀k∈{lnth (ltake (n' - enat n) (ldrop (enat n) t)) na |
      na. enat na < llength (ltake (n' - enat n) (ldrop (enat n) t))}. ¬ ∥c∥⇘k⇙"
    proof
      fix k assume "k∈{lnth (ltake (n' - enat n) (ldrop (enat n) t)) na |
        na. enat na < llength (ltake (n' - enat n) (ldrop (enat n) t))}"
      then obtain k' where "enat k' < llength (ltake (n' - enat n) (ldrop (enat n) t))"
        and "k=lnth (ltake (n' - enat n) (ldrop (enat n) t)) k'" by auto
      have "enat (k' + n) < llength t"
      proof -
        from ‹enat k' < llength (ltake (n' - enat n) (ldrop (enat n) t))› have "enat k' < n'-n" by simp
        hence "enat k' + n < n'" using assms(1) enat_min by auto
        show ?thesis
        proof cases
          assume "lfinite t"
          with ‹¬ lfinite t ∨ n'-1 < llength t› have "n'-1<llength t" by simp
          hence "n'< eSuc (llength t)" by (metis eSuc_minus_1 enat_minus_mono1 leD leI)
          hence "n'≤ llength t" using eSuc_ile_mono ileI1 by blast
          with ‹enat k' + n < n'› show ?thesis by (simp add: add.commute)
        next
          assume "¬ lfinite t"
          hence "llength t = ∞" using not_lfinite_llength by auto
          thus ?thesis by simp
        qed
      qed
      moreover have "k = lnth t (k' + n)"
      proof -
        from ‹enat k' < llength (ltake (n' - enat n) (ldrop (enat n) t))›
          have "enat k'<n' - enat n" by auto
        hence "lnth (ltake (n' - enat n) (ldrop (enat n) t)) k' = lnth (ldrop (enat n) t) k'"
          using lnth_ltake[of k' "n' - enat n"] by simp
        with ‹enat (k' + n) < llength t› show ?thesis using lnth_ldrop[of n k' t ]
          using ‹k = lnth (ltake (n' - enat n) (ldrop (enat n) t)) k'› by (simp add: add.commute)
      qed
      moreover from ‹enat n ≤ (n'::enat)› have "k' + the_enat n≥n" by auto
      moreover from ‹enat k' < llength (ltake (n' - enat n) (ldrop (enat n) t))› have "k' + n<n'"
        using assms(1) enat_min by auto
      ultimately show "¬ ∥c∥⇘k⇙" using ‹∄k. k≥n ∧ k<n' ∧ k < llength t ∧ ∥c∥⇘lnth t k⇙› by simp
    qed
    hence "∀k∈lset (ltake (n'-n) (ldrop n t)). ¬ ∥c∥⇘k⇙"
      using lset_conv_lnth[of "(ltake (n' - enat n) (ldrop (enat n) t))"] by simp
    thus ?thesis using proj_lnull by auto
  qed
  moreover from assms have "n + (n' - n) = n'"
    by (meson enat.distinct(1) enat_add_sub_same enat_diff_cancel_left enat_le_plus_same(1) less_imp_le)
  ultimately show ?thesis by simp
qed
  
subsubsection "Projection Active"

lemma proj_active[simp]:
  assumes "enat i < llength t" "∥c∥⇘lnth t i⇙"
  shows "π⇘c⇙(ltake (Suc i) t) = (π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" (is "?lhs = ?rhs")
proof -
  from assms have "ltake (enat (Suc i)) t = (ltake (enat i) t) @⇩l ((lnth t i) #⇩l []⇩l)"
    using ltake_Suc_conv_snoc_lnth by blast
  hence "?lhs = π⇘c⇙((ltake (enat i) t) @⇩l ((lnth t i) #⇩l []⇩l))" by simp
  moreover have "… = (π⇘c⇙(ltake (enat i) t)) @⇩l (π⇘c⇙((lnth t i) #⇩l []⇩l))" by simp
  moreover from assms have "π⇘c⇙((lnth t i) #⇩l []⇩l) = (σ⇘c⇙(lnth t i)) #⇩l []⇩l" by simp
  ultimately show ?thesis by simp
qed
  
lemma proj_active_append:
  assumes a1: "(n::nat) ≤ i"
      and a2: "enat i < (n'::enat)"
      and a3: "¬ lfinite t ∨ n'-1 < llength t"
      and a4: "∥c∥⇘lnth t i⇙"
      and "∀i'. (n ≤ i' ∧ enat i'<n' ∧ i' < llength t ∧ ∥c∥⇘lnth t i'⇙) ⟶ (i' = i)"
    shows "π⇘c⇙(ltake n' t) = (π⇘c⇙(ltake n t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" (is "?lhs = ?rhs")
proof -
  have "?lhs = π⇘c⇙(ltake (Suc i) t)"
  proof -
    from a2 have "Suc i ≤ n'" by (simp add: Suc_ile_eq)
    moreover from a3 have "¬ lfinite t ∨ n'-1 < llength t" by simp
    moreover have "∄k. enat k≥enat (Suc i) ∧ k<n' ∧ k < llength t ∧ ∥c∥⇘lnth t k⇙"
    proof
      assume "∃k. enat k≥enat (Suc i) ∧ k<n' ∧ k < llength t ∧ ∥c∥⇘lnth t k⇙"
      then obtain k where "enat k≥enat (Suc i)" and "k<n'" and "k < llength t" and "∥c∥⇘lnth t k⇙" by blast
      moreover from ‹enat k≥enat (Suc i)› have "enat k≥n"
        using assms by (meson dual_order.trans enat_ord_simps(1) le_SucI)
      ultimately have "enat k=enat i" using assms using enat_ord_simps(1) by blast
      with ‹enat k≥enat (Suc i)› show False by simp
    qed
    ultimately show ?thesis using proj_not_active_same[of "Suc i" n' t c] by simp
  qed
  also have "… = (π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)"
  proof -
    have "i < llength t"
    proof cases
      assume "lfinite t"
      with a3 have "n'-1 < llength t" by simp
      hence "n' ≤ llength t" by (metis eSuc_minus_1 enat_minus_mono1 ileI1 not_le)
      with a2 show "enat i < llength t" by simp
    next
      assume "¬ lfinite t"
      thus ?thesis by (metis enat_ord_code(4) llength_eq_infty_conv_lfinite)
    qed
    with a4 show ?thesis by simp
  qed
  also have "… = ?rhs"
  proof -
    from a1 have "enat n ≤ enat i" by simp
    moreover from a2 a3 have "¬ lfinite t ∨ enat i-1 < llength t"
      using enat_minus_mono1 less_imp_le order.strict_trans1 by blast
    moreover have "∄k. k≥n ∧ enat k<enat i ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙"
    proof
      assume "∃k. k≥n ∧ enat k<enat i ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙"
      then obtain k where "k≥n" and "enat k<enat i" and "enat k < llength t" and "∥c∥⇘lnth t k⇙" by blast
      moreover from ‹enat k<enat i› have "enat k<n'" using assms dual_order.strict_trans by blast
      ultimately have "enat k=enat i" using assms by simp
      with ‹enat k<enat i› show False by simp
    qed
    ultimately show ?thesis using proj_not_active_same[of n i t c] by simp
  qed    
  finally show ?thesis by simp
qed
  
subsubsection "Same and not Same"

lemma proj_same_not_active:
  assumes "n ≤ n'"
    and "enat (n'-1) < llength t"
    and "π⇘c⇙(ltake n' t) = π⇘c⇙(ltake n t)"
  shows "∄k. k≥n ∧ k<n' ∧ ∥c∥⇘lnth t k⇙"
proof
  assume "∃k. k≥n ∧ k<n' ∧ ∥c∥⇘lnth t k⇙"
  then obtain i where "i≥n" and "i<n'" and "∥c∥⇘lnth t i⇙" by blast
  moreover from ‹enat (n'-1)<llength t› and ‹i<n'› have "i<llength t"
    by (metis diff_Suc_1 dual_order.strict_trans enat_ord_simps(2) lessE)
  ultimately have "π⇘c⇙(ltake (Suc i) t) =
    (π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
  moreover from ‹i<n'› have "Suc i ≤ n'" by simp
    hence "lprefix(π⇘c⇙(ltake (Suc i) t)) (π⇘c⇙(ltake n' t))" by simp
    then obtain "tl" where "π⇘c⇙(ltake n' t) = (π⇘c⇙(ltake (Suc i) t)) @⇩l tl"
      using lprefix_conv_lappend by auto
  moreover from ‹n≤i› have "lprefix(π⇘c⇙(ltake n t)) (π⇘c⇙(ltake i t))" by simp
    hence "lprefix(π⇘c⇙(ltake n t)) (π⇘c⇙(ltake i t))" by simp
    then obtain "hd" where "π⇘c⇙(ltake i t) = (π⇘c⇙(ltake n t)) @⇩l hd"
      using lprefix_conv_lappend by auto
  ultimately have "π⇘c⇙(ltake n' t) =
    (((π⇘c⇙(ltake n t)) @⇩l hd) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)) @⇩l tl" by simp
  also have "… = ((π⇘c⇙(ltake n t)) @⇩l hd) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl)"
    using lappend_snocL1_conv_LCons2[of "(π⇘c⇙(ltake n t)) @⇩l hd" "σ⇘c⇙(lnth t i)"] by simp
  also have "… = (π⇘c⇙(ltake n t)) @⇩l (hd @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl))"
    using lappend_assoc by auto
  also have "π⇘c⇙(ltake n' t) = (π⇘c⇙(ltake n' t)) @⇩l []⇩l" by simp
  finally have "(π⇘c⇙(ltake n' t)) @⇩l []⇩l = (π⇘c⇙(ltake n t)) @⇩l (hd @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl))" .
  moreover from assms(3) have "llength (π⇘c⇙(ltake n' t)) = llength (π⇘c⇙(ltake n t))" by simp
  ultimately have "lfinite (π⇘c⇙(ltake n' t)) ⟶ []⇩l = hd @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl)"
    using assms(3) lappend_eq_lappend_conv[of "π⇘c⇙(ltake n' t)" "π⇘c⇙(ltake n t)" "[]⇩l"] by simp
  moreover have "lfinite (π⇘c⇙(ltake n' t))" by simp
  ultimately have "[]⇩l = hd @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl)" by simp
  hence "(σ⇘c⇙(lnth t i)) #⇩l tl = []⇩l" using LNil_eq_lappend_iff by auto
  thus False by simp
qed

lemma proj_not_same_active:
  assumes "enat n ≤ (n'::enat)"
    and "(¬ lfinite t) ∨ n'-1 < llength t"
    and "¬(π⇘c⇙(ltake n' t) = π⇘c⇙(ltake n t))"
  shows "∃k. k≥n ∧ k<n' ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙"
proof (rule ccontr)
  assume "¬(∃k. k≥n ∧ k<n' ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙)"
  have "π⇘c⇙(ltake n' t) = π⇘c⇙(ltake (enat n) t)"
  proof cases
    assume "lfinite t"
    hence "llength t≠∞" by (simp add: lfinite_llength_enat) 
    hence "enat (the_enat (llength t)) = llength t" by auto
    with assms ‹¬ (∃k≥n. k < n' ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙)›
      show ?thesis using proj_not_active_same[of n n' t c] by simp
  next
    assume "¬ lfinite t"
    with assms ‹¬ (∃k≥n. k < n' ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙)›
      show ?thesis using proj_not_active_same[of n n' t c] by simp
  qed
  with assms show False by simp
qed

subsection "Activations"
text ‹
  We also introduce an operator to obtain the number of activations of a certain component within a given configuration trace.
›

definition nAct :: "'id ⇒ enat ⇒ (cnf llist) ⇒ enat" (‹⟨_ #⇘_⇙_⟩›) where
"⟨c #⇘n⇙ t⟩ ≡ llength (π⇘c⇙(ltake n t))"

lemma nAct_0[simp]:
  "⟨c #⇘0⇙ t⟩ = 0" by (simp add: nAct_def)

lemma nAct_NIL[simp]:
  "⟨c #⇘n⇙ []⇩l⟩ = 0" by (simp add: nAct_def)    

lemma nAct_Null:
  assumes "llength t ≥ n"
      and "⟨c #⇘n⇙ t⟩ = 0"
    shows "∀i<n. ¬ ∥c∥⇘lnth t i⇙"
proof -
  from assms have "lnull (π⇘c⇙(ltake n t))" using nAct_def lnull_def by simp
  hence "π⇘c⇙(ltake n t) = []⇩l" using lnull_def by blast
  hence "(∀k∈lset (ltake n t). ¬ ∥c∥⇘k⇙)" by simp
  show ?thesis
  proof (rule ccontr)
    assume "¬ (∀i<n. ¬ ∥c∥⇘lnth t i⇙)"
    then obtain i where "i<n" and "∥c∥⇘lnth t i⇙" by blast
    moreover have "enat i < llength (ltake n t)  ∧ lnth (ltake n t) i = (lnth t i)"
    proof
      from ‹llength t ≥ n› have "n = min n (llength t)" using min.orderE by auto
      hence "llength (ltake n t) = n" by simp
      with ‹i<n› show "enat i < llength (ltake n t)" by auto
      from ‹i<n› show "lnth (ltake n t) i = (lnth t i)" using lnth_ltake by auto
    qed
    hence "(lnth t i ∈ lset (ltake n t))" using in_lset_conv_lnth[of "lnth t i" "ltake n t"] by blast
    ultimately show False using ‹(∀k∈lset (ltake n t). ¬ ∥c∥⇘k⇙)› by simp
  qed
qed

lemma nAct_ge_one[simp]:
  assumes "llength t ≥ n"
      and "i < n"
      and "∥c∥⇘lnth t i⇙"
    shows "⟨c #⇘n⇙ t⟩ ≥ enat 1"
proof (rule ccontr)
  assume "¬ (⟨c #⇘n⇙ t⟩ ≥ enat 1)"
  hence "⟨c #⇘n⇙ t⟩ < enat 1" by simp
  hence "⟨c #⇘n⇙ t⟩ < 1" using enat_1 by simp
  hence "⟨c #⇘n⇙ t⟩ = 0" using Suc_ile_eq ‹¬ enat 1 ≤ ⟨c #⇘n⇙ t⟩› zero_enat_def by auto
  with ‹llength t ≥ n› have "∀i<n. ¬ ∥c∥⇘lnth t i⇙" using nAct_Null by simp
  with assms show False by simp
qed
    
lemma nAct_finite[simp]:
  assumes "n ≠ ∞"
  shows "∃n'. ⟨c #⇘n⇙ t⟩ = enat n'"
proof -
  from assms have "lfinite (ltake n t)" by simp
  hence "lfinite (π⇘c⇙(ltake n t))" by simp
  hence "∃n'. llength (π⇘c⇙(ltake n t)) = enat n'" using lfinite_llength_enat[of "π⇘c⇙(ltake n t)"] by simp
  thus ?thesis using nAct_def by simp
qed

lemma nAct_enat_the_nat[simp]:
  assumes "n ≠ ∞"
  shows "enat (the_enat (⟨c #⇘n⇙ t⟩)) = ⟨c #⇘n⇙ t⟩"
proof -
  from assms have "⟨c #⇘n⇙ t⟩ ≠ ∞" by simp
  thus ?thesis using enat_the_enat by simp
qed
  
subsubsection "Monotonicity and Continuity"
  
lemma nAct_mcont:
  shows "mcont lSup lprefix Sup (≤) (nAct c n)"
proof -
  have "mcont lSup lprefix lSup lprefix (ltake n)" by simp
  hence "mcont lSup lprefix lSup lprefix (λt. π⇘c⇙(ltake n t))"
    using proj_mcont2mcont[of lSup lprefix "(ltake n)"] by simp
  hence "mcont lSup lprefix Sup (≤) (λt. llength (π⇘c⇙(ltake n t)))" by simp
  moreover have "nAct c n = (λt. llength (π⇘c⇙(ltake n t)))" using nAct_def by auto
  ultimately show ?thesis by simp
qed
  
lemma nAct_mono:
  assumes "n ≤ n'"
    shows "⟨c #⇘n⇙ t⟩ ≤ ⟨c #⇘n'⇙ t⟩"
proof -
  from assms have "lprefix (ltake n t) (ltake n' t)" by simp
  hence "lprefix (π⇘c⇙(ltake n t)) (π⇘c⇙(ltake n' t))" by simp
  hence "llength (π⇘c⇙(ltake n t)) ≤ llength (π⇘c⇙(ltake n' t))"
    using lprefix_llength_le[of "(π⇘c⇙(ltake n t))"] by simp
  thus ?thesis using nAct_def by simp
qed
  
lemma nAct_strict_mono_back:
  assumes "⟨c #⇘n⇙ t⟩ < ⟨c #⇘n'⇙ t⟩"
    shows "n < n'"
proof (rule ccontr)
  assume "¬ n<n'"
  hence "n≥n'" by simp
  hence "⟨c #⇘n⇙ t⟩ ≥ ⟨c #⇘n'⇙ t⟩" using nAct_mono by simp
  thus False using assms by simp
qed

subsubsection "Not Active"

lemma nAct_not_active[simp]:
  fixes n::nat
    and n'::nat
    and t::"(cnf llist)"
    and c::'id
  assumes "enat i < llength t"
    and "¬ ∥c∥⇘lnth t i⇙"
  shows "⟨c #⇘Suc i⇙ t⟩ = ⟨c #⇘i⇙ t⟩"
proof -
  from assms have "π⇘c⇙(ltake (Suc i) t) = π⇘c⇙(ltake i t)" by simp
  hence "llength (π⇘c⇙(ltake (enat (Suc i)) t)) = llength (π⇘c⇙(ltake i t))" by simp
  moreover have "llength (π⇘c⇙(ltake i t)) ≠ ∞"
    using llength_eq_infty_conv_lfinite[of "π⇘c⇙(ltake (enat i) t)"] by simp
  ultimately have "llength (π⇘c⇙(ltake (Suc i) t)) = llength (π⇘c⇙(ltake i t))"
    using the_enat_eSuc by simp
  with nAct_def show ?thesis by simp
qed
  
lemma nAct_not_active_same:
  assumes "enat n ≤ (n'::enat)"
      and "n'-1 < llength t"
      and "∄k. enat k≥n ∧ k<n' ∧ ∥c∥⇘lnth t k⇙"
    shows "⟨c #⇘n'⇙ t⟩ = ⟨c #⇘n⇙ t⟩"
  using assms proj_not_active_same nAct_def by simp
    
subsubsection "Active"
  
lemma nAct_active[simp]:
  fixes n::nat
    and n'::nat
    and t::"(cnf llist)"
    and c::'id
  assumes "enat i < llength t"
    and "∥c∥⇘lnth t i⇙"
  shows "⟨c #⇘Suc i⇙ t⟩ = eSuc (⟨c #⇘i⇙ t⟩)"
proof -
  from assms have "π⇘c⇙(ltake (Suc i) t) =
    (π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
  hence "llength (π⇘c⇙(ltake (enat (Suc i)) t)) = eSuc (llength (π⇘c⇙(ltake i t)))"
    using plus_1_eSuc one_eSuc by simp
  moreover have "llength (π⇘c⇙(ltake i t)) ≠ ∞"
    using llength_eq_infty_conv_lfinite[of "π⇘c⇙(ltake (enat i) t)"] by simp
  ultimately have "llength (π⇘c⇙(ltake (Suc i) t)) = eSuc (llength (π⇘c⇙(ltake i t)))"
    using the_enat_eSuc by simp
  with nAct_def show ?thesis by simp
qed

lemma nAct_active_suc:
  fixes n::nat
    and n'::enat
    and t::"(cnf llist)"
    and c::'id
  assumes "¬ lfinite t ∨ n'-1 < llength t"
    and "n ≤ i"
    and "enat i < n'"
    and "∥c∥⇘lnth t i⇙"
    and "∀i'. (n ≤ i' ∧ enat i'<n' ∧ i' < llength t ∧ ∥c∥⇘lnth t i'⇙) ⟶ (i' = i)"
  shows "⟨c #⇘n'⇙ t⟩ = eSuc (⟨c #⇘n⇙ t⟩)"
proof -
  from assms have "π⇘c⇙(ltake n' t) = (π⇘c⇙(ltake (enat n) t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)"
    using proj_active_append[of n i n' t c] by blast
  moreover have "llength ((π⇘c⇙(ltake (enat n) t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)) =
    eSuc (llength (π⇘c⇙(ltake (enat n) t)))" using one_eSuc eSuc_plus_1 by simp
  ultimately show ?thesis using nAct_def by simp
qed
  
lemma nAct_less:
  assumes "enat k < llength t"
    and "n ≤ k"
    and "k < (n'::enat)"
    and "∥c∥⇘lnth t k⇙"
  shows "⟨c #⇘n⇙ t⟩ < ⟨c #⇘n'⇙ t⟩"
proof -
  have "⟨c #⇘k⇙ t⟩ ≠ ∞" by simp
  then obtain en where en_def: "⟨c #⇘k⇙ t⟩ = enat en" by blast  
  moreover have "eSuc (enat en) ≤ ⟨c #⇘n'⇙ t⟩"
  proof -
    from assms have "Suc k ≤ n'" using Suc_ile_eq by simp
    hence "⟨c #⇘Suc k⇙ t⟩ ≤ ⟨c #⇘n'⇙ t⟩" using nAct_mono by simp
    moreover from assms have "⟨c #⇘Suc k⇙ t⟩ = eSuc (⟨c #⇘k⇙ t⟩)" by simp
    ultimately have "eSuc (⟨c #⇘k⇙ t⟩) ≤ ⟨c #⇘n'⇙ t⟩" by simp
    thus ?thesis using en_def by simp
  qed
  moreover have "enat en < eSuc (enat en)" by simp
  ultimately have "enat en < ⟨c #⇘n'⇙ t⟩" using less_le_trans[of "enat en" "eSuc (enat en)"] by simp
  moreover have "⟨c #⇘n⇙ t⟩ ≤ enat en"
  proof -
    from assms have "⟨c #⇘n⇙ t⟩ ≤ ⟨c #⇘k⇙ t⟩" using nAct_mono by simp
    thus ?thesis using en_def by simp
  qed
  ultimately show ?thesis using le_less_trans[of "⟨c #⇘n⇙ t⟩"] by simp
qed
  
lemma nAct_less_active:
  assumes "n' - 1 < llength t"
      and "⟨c #⇘enat n⇙ t⟩ < ⟨c #⇘n'⇙ t⟩"
  shows "∃i≥n. i<n' ∧ ∥c∥⇘lnth t i⇙"
proof (rule ccontr)
  assume "¬ (∃i≥n. i<n' ∧ ∥c∥⇘lnth t i⇙)"
  moreover have "enat n ≤ n'" using assms(2) less_imp_le nAct_strict_mono_back by blast
  ultimately have "⟨c #⇘n⇙ t⟩ = ⟨c #⇘n'⇙ t⟩" using ‹n' - 1 < llength t› nAct_not_active_same by simp
  thus False using assms by simp
qed

subsubsection "Same and Not Same"
  
lemma nAct_same_not_active:
  assumes "⟨c #⇘n'⇙ inf_llist t⟩ = ⟨c #⇘n⇙ inf_llist t⟩"
  shows "∀k≥n. k<n' ⟶ ¬ ∥c∥⇘t k⇙"
proof (rule ccontr)
  assume "¬(∀k≥n. k<n' ⟶ ¬ ∥c∥⇘t k⇙)"
  then obtain k where "k≥n" and "k<n'" and "∥c∥⇘t k⇙" by blast
  hence "⟨c #⇘Suc k⇙ inf_llist t⟩ = eSuc (⟨c #⇘k⇙ inf_llist t⟩)" by simp
  moreover have "⟨c #⇘k⇙ inf_llist t⟩≠∞" by simp
  ultimately have "⟨c #⇘k⇙ inf_llist t⟩ < ⟨c #⇘Suc k⇙ inf_llist t⟩" by fastforce
  moreover from ‹n≤k› have "⟨c #⇘n⇙ inf_llist t⟩ ≤ ⟨c #⇘k⇙ inf_llist t⟩" using nAct_mono by simp
  moreover from ‹k<n'› have "Suc k ≤ n'" by (simp add: Suc_ile_eq)
  hence "⟨c #⇘Suc k⇙ inf_llist t⟩ ≤ ⟨c #⇘n'⇙ inf_llist t⟩" using nAct_mono by simp
  ultimately show False using assms by simp
qed
  
lemma nAct_not_same_active:
  assumes "⟨c #⇘enat n⇙ t⟩ < ⟨c #⇘n'⇙ t⟩"
    and "¬ lfinite t ∨ n' - 1 < llength t"
  shows "∃(i::nat)≥n. enat i< n' ∧ i<llength t ∧ ∥c∥⇘lnth t i⇙"
proof -
  from assms have "llength(π⇘c⇙(ltake n t)) < llength (π⇘c⇙(ltake n' t))" using nAct_def by simp
  hence "π⇘c⇙(ltake n' t) ≠ π⇘c⇙(ltake n t)" by auto
  moreover from assms have "enat n < n'" using nAct_strict_mono_back[of c "enat n" t n'] by simp
  ultimately show ?thesis using proj_not_same_active[of n n' t c] assms by simp
qed
  
lemma nAct_less_llength_active:
  assumes "x < llength (π⇘c⇙(t))"
    and "enat x = ⟨c #⇘enat n'⇙ t⟩"
  shows "∃(i::nat)≥n'. i<llength t ∧ ∥c∥⇘lnth t i⇙"
proof -
  have "llength(π⇘c⇙(ltake n' t)) < llength (π⇘c⇙(t))" using assms(1) assms(2) nAct_def by auto
  hence "llength(π⇘c⇙(ltake n' t)) < llength (π⇘c⇙(ltake (llength t) t))" by (simp add: ltake_all)
  hence "⟨c #⇘enat n'⇙ t⟩ < ⟨c #⇘llength t⇙ t⟩" using nAct_def by simp
  moreover have "¬ lfinite t ∨ llength t - 1 < llength t"
  proof (rule Meson.imp_to_disjD[OF HOL.impI])
    assume "lfinite t"
    hence "llength t ≠ ∞" by (simp add: llength_eq_infty_conv_lfinite)
    moreover have "llength t>0"
    proof -
      from ‹x < llength (π⇘c⇙(t))› have "llength (π⇘c⇙(t))>0" by auto
      thus ?thesis using proj_llength order.strict_trans2 by blast
    qed
    ultimately show "llength t - 1 < llength t" by (metis One_nat_def ‹lfinite t› diff_Suc_less
      enat_ord_simps(2) idiff_enat_enat lfinite_conv_llength_enat one_enat_def zero_enat_def)
  qed
  ultimately show ?thesis using nAct_not_same_active[of c n' t "llength t"] by simp
qed

lemma nAct_exists:
  assumes "x < llength (π⇘c⇙(t))"
  shows "∃(n'::nat). enat x = ⟨c #⇘n'⇙ t⟩"
proof -
  have "x < llength (π⇘c⇙(t)) ⟶ (∃(n'::nat). enat x = ⟨c #⇘n'⇙ t⟩)"
  proof (induction x)
    case 0
    thus ?case by (metis nAct_0 zero_enat_def)
  next
    case (Suc x)
    show ?case
    proof
      assume "Suc x < llength (π⇘c⇙(t))"
      hence "x < llength (π⇘c⇙(t))" using Suc_ile_eq less_imp_le by auto
      with Suc.IH obtain n' where "enat x = ⟨c #⇘enat n'⇙ t⟩" by blast
      with ‹x < llength (π⇘c⇙(t))› have "∃i≥n'. i < llength t ∧ ∥c∥⇘lnth t i⇙"
        using nAct_less_llength_active[of x c t n'] by simp
      then obtain i where "i≥n'" and "i<llength t" and "∥c∥⇘lnth t i⇙"
        and "∄k. n'≤k ∧ k<i ∧ k<llength t ∧ ∥c∥⇘lnth t k⇙" using lActive_least[of n' t c] by auto
      moreover from ‹i<llength t› have "¬ lfinite t ∨ enat (Suc i) - 1 < llength t"
        by (simp add: one_enat_def)
      moreover have "enat i < enat (Suc i)" by simp
      moreover have "∀i'. (n' ≤ i' ∧ enat i'<enat (Suc i) ∧ i'<llength t ∧ ∥c∥⇘lnth t i'⇙) ⟶ (i' = i)"
      proof (rule HOL.impI[THEN HOL.allI])
        fix i' assume "n' ≤ i' ∧ enat i'<enat (Suc i) ∧ i'<llength t ∧ ∥c∥⇘lnth t i'⇙"
        with ‹∄k. n'≤k ∧ k<i ∧ k<llength t ∧ ∥c∥⇘lnth t k⇙› show "i'=i" by fastforce
      qed
      ultimately have "⟨c #⇘Suc i⇙ t⟩ = eSuc (⟨c #⇘n'⇙ t⟩)" using nAct_active_suc[of t "Suc i" n' i c] by simp
      with ‹enat x = ⟨c #⇘enat n'⇙ t⟩› have "⟨c #⇘Suc i⇙ t⟩ = eSuc (enat x)" by simp
      thus "∃n'. enat (Suc x) = ⟨c #⇘enat n'⇙ t⟩" by (metis eSuc_enat)
    qed
  qed
  with assms show ?thesis by simp
qed
  
subsection "Projection and Activation"
text ‹
  In the following we provide some properties about the relationship between the projection and activations operator.
›
  
lemma nAct_le_proj:
  "⟨c #⇘n⇙ t⟩ ≤ llength (π⇘c⇙(t))"
proof -
  from nAct_def have "⟨c #⇘n⇙ t⟩ = llength (π⇘c⇙(ltake n t))" by simp
  moreover have "llength (π⇘c⇙(ltake n t)) ≤ llength (π⇘c⇙(t))"
  proof -
    have "lprefix (ltake n t) t" by simp
    hence "lprefix (π⇘c⇙(ltake n t)) (π⇘c⇙(t))" by simp
    hence "llength (π⇘c⇙(ltake n t)) ≤ llength (π⇘c⇙(t))" using lprefix_llength_le by blast
    thus ?thesis by auto
  qed
  thus ?thesis using nAct_def by simp
qed
  
lemma proj_nAct:
  assumes "(enat n < llength t)"
  shows "π⇘c⇙(ltake n t) = ltake (⟨c #⇘n⇙ t⟩) (π⇘c⇙(t))" (is "?lhs = ?rhs")
proof -
  have "?lhs = ltake (llength (π⇘c⇙(ltake n t))) (π⇘c⇙(ltake n t))"
    using ltake_all[of "π⇘c⇙(ltake n t)" "llength (π⇘c⇙(ltake n t))"] by simp
  also have "… = ltake (llength (π⇘c⇙(ltake n t))) ((π⇘c⇙(ltake n t)) @⇩l (π⇘c⇙(ldrop n t)))"
    using ltake_lappend1[of "llength (π⇘c⇙(ltake (enat n) t))" "π⇘c⇙(ltake n t)" "(π⇘c⇙(ldrop n t))"] by simp
  also have "… = ltake (⟨c #⇘n⇙ t⟩) ((π⇘c⇙(ltake n t)) @⇩l (π⇘c⇙(ldrop n t)))" using nAct_def by simp      
  also have "… = ltake (⟨c #⇘n⇙ t⟩) (π⇘c⇙((ltake (enat n) t) @⇩l (ldrop n t)))" by simp
  also have "… = ltake (⟨c #⇘n⇙ t⟩) (π⇘c⇙(t))" using lappend_ltake_ldrop[of n t] by simp
  finally show ?thesis by simp
qed

lemma proj_active_nth:
  assumes "enat (Suc i) < llength t" "∥c∥⇘lnth t i⇙"
  shows "lnth (π⇘c⇙(t)) (the_enat (⟨c #⇘i⇙ t⟩)) = σ⇘c⇙(lnth t i)"
proof -
  from assms have "enat i < llength t" using Suc_ile_eq[of i "llength t"] by auto
  with assms have "π⇘c⇙(ltake (Suc i) t) = (π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
  moreover have "lnth ((π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l))
    (the_enat (llength (π⇘c⇙(ltake i t)))) = σ⇘c⇙(lnth t i)"
  proof -
    have "¬ lnull ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
    moreover have "lfinite (π⇘c⇙(ltake i t))" by simp
    ultimately have "lnth ((π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l))
      (the_enat (llength (π⇘c⇙(ltake i t)))) = lhd ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
    also have "… = σ⇘c⇙(lnth t i)" by simp
    finally show "lnth ((π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l))
      (the_enat (llength (π⇘c⇙(ltake i t)))) = σ⇘c⇙(lnth t i)" by simp
  qed
  ultimately have "σ⇘c⇙(lnth t i) = lnth (π⇘c⇙(ltake (Suc i) t))
    (the_enat (llength (π⇘c⇙(ltake i t))))" by simp
  also have "… = lnth (π⇘c⇙(ltake (Suc i) t)) (the_enat (⟨c #⇘i⇙ t⟩))" using nAct_def by simp
  also have "… = lnth (ltake (⟨c #⇘Suc i⇙ t⟩) (π⇘c⇙(t))) (the_enat (⟨c #⇘i⇙ t⟩))"
    using proj_nAct[of "Suc i" t c] assms by simp
  also have "… = lnth (π⇘c⇙(t)) (the_enat (⟨c #⇘i⇙ t⟩))"
  proof -
    from assms have "⟨c #⇘Suc i⇙ t⟩ = eSuc (⟨c #⇘i⇙ t⟩)" using ‹enat i < llength t› by simp
    moreover have "⟨c #⇘i⇙ t⟩ < eSuc (⟨c #⇘i⇙ t⟩)" using iless_Suc_eq[of "the_enat (⟨c #⇘enat i⇙ t⟩)"] by simp
    ultimately have "⟨c #⇘i⇙ t⟩ < (⟨c #⇘Suc i⇙ t⟩)" by simp
    hence "enat (the_enat (⟨c #⇘Suc i⇙ t⟩)) > enat (the_enat (⟨c #⇘i⇙ t⟩))" by simp
    thus ?thesis using lnth_ltake[of "the_enat (⟨c #⇘i⇙ t⟩)" "the_enat (⟨c #⇘enat (Suc i)⇙ t⟩)" "π⇘c⇙(t)"] by simp
  qed
  finally show ?thesis ..
qed

lemma nAct_eq_proj:
  assumes "¬(∃i≥n. ∥c∥⇘lnth t i⇙)"
  shows "⟨c #⇘n⇙ t⟩ = llength (π⇘c⇙(t))" (is "?lhs = ?rhs")
proof -
  from nAct_def have "?lhs = llength (π⇘c⇙(ltake n t))" by simp
  moreover from assms have "∀(n'::nat)≤llength t. n'≥n ⟶ (¬ ∥c∥⇘lnth t n'⇙)" by simp
  hence "π⇘c⇙(t) = π⇘c⇙(ltake n t)" using proj_ltake by simp
  ultimately show ?thesis by simp
qed

lemma nAct_llength_proj:
  assumes "∃i≥n. ∥c∥⇘t i⇙"
  shows "llength (π⇘c⇙(inf_llist t)) ≥ eSuc (⟨c #⇘n⇙ inf_llist t⟩)"
proof -
  from ‹∃i≥n. ∥c∥⇘t i⇙› obtain i where "i≥n" and "∥c∥⇘t i⇙"
    and "¬ (∃k≥n. k < i ∧ k < llength (inf_llist t) ∧ ∥c∥⇘t k⇙)"
    using lActive_least[of n "inf_llist t" c] by auto
  moreover have "llength (π⇘c⇙(inf_llist t)) ≥ ⟨c #⇘Suc i⇙ inf_llist t⟩" using nAct_le_proj by simp
  moreover have "eSuc (⟨c #⇘n⇙ inf_llist t⟩) = ⟨c #⇘Suc i⇙ inf_llist t⟩"
  proof -
    have "enat (Suc i) < llength (inf_llist t)" by simp
    moreover have "i < Suc i" by simp
    moreover from ‹¬ (∃k≥n. k < i ∧ k < llength (inf_llist t) ∧ ∥c∥⇘t k⇙)›
      have "∀i'. n ≤ i' ∧ i' < Suc i ∧ ∥c∥⇘lnth (inf_llist t) i'⇙ ⟶ i' = i" by fastforce
    ultimately show ?thesis using nAct_active_suc ‹i≥n› ‹∥c∥⇘t i⇙› by simp
  qed
  ultimately show ?thesis by simp
qed
  
subsection "Least not Active"
text ‹
  In the following, we introduce an operator to obtain the least point in time before a certain point in time where a component was deactivated.
›

definition lNAct :: "'id ⇒ (nat ⇒ cnf) ⇒ nat ⇒ nat" (‹⟨_ ⇐ _⟩⇘_⇙›)
  where "⟨c ⇐ t⟩⇘n⇙ ≡ (LEAST n'. n=n' ∨ (n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙)))"

lemma lNact0[simp]:
  "⟨c ⇐ t⟩⇘0⇙ = 0"
  by (simp add: lNAct_def)
    
lemma lNact_least:
  assumes "n=n' ∨ n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙)"
  shows "⟨c ⇐ t⟩⇘n⇙ ≤ n'"
using Least_le[of "λn'. n=n' ∨ (n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙))" n'] lNAct_def using assms by auto
    
lemma lNAct_ex: "⟨c ⇐ t⟩⇘n⇙=n ∨ ⟨c ⇐ t⟩⇘n⇙<n ∧ (∄k. k≥⟨c ⇐ t⟩⇘n⇙ ∧ k<n ∧ ∥c∥⇘t k⇙)"
proof -
  let ?P="λn'. n=n' ∨ n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙)"
  from lNAct_def have "⟨c ⇐ t⟩⇘n⇙ = (LEAST n'. ?P n')" by simp
  moreover have "?P n" by simp
  with LeastI have "?P (LEAST n'. ?P n')" .
  ultimately show ?thesis by auto
qed
    
lemma lNact_notActive:
  fixes c t n k
  assumes "k≥⟨c ⇐ t⟩⇘n⇙"
    and "k<n"
  shows "¬∥c∥⇘t k⇙"
  by (metis assms lNAct_ex leD)
    
lemma lNactGe:
  fixes c t n n'
  assumes "n' ≥ ⟨c ⇐ t⟩⇘n⇙" 
    and "∥c∥⇘t n'⇙"
  shows "n' ≥ n"
  using assms lNact_notActive leI by blast

lemma lNactLe[simp]:
  fixes n n'
  shows "⟨c ⇐ t⟩⇘n⇙ ≤ n"
  using lNAct_ex less_or_eq_imp_le by blast
    
lemma lNactLe_nact:
  fixes n n'
  assumes "n'=n ∨ (n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙))"
  shows "⟨c ⇐ t⟩⇘n⇙ ≤ n'"
  using assms lNAct_def Least_le[of "λn'. n=n' ∨ (n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙))"] by auto
    
lemma lNact_active:
  fixes cid t n
  assumes "∀k<n. ∥cid∥⇘t k⇙"
  shows "⟨cid ⇐ t⟩⇘n⇙ = n"
  using assms lNAct_ex by blast
    
lemma nAct_mono_back:
  fixes c t and n and n'
  assumes "⟨c #⇘n'⇙ inf_llist t⟩ ≥ ⟨c #⇘n⇙ inf_llist t⟩"
  shows "n'≥⟨c ⇐ t⟩⇘n⇙"
proof cases
  assume "⟨c #⇘n'⇙ inf_llist t⟩ = ⟨c #⇘n⇙ inf_llist t⟩"
  thus ?thesis
  proof cases
    assume "n'≥n"
    thus ?thesis
      by (rule order_trans[OF lNactLe])
  next
    assume "¬ n'≥n"
    hence "n'<n" by simp
    with ‹⟨c #⇘n'⇙ inf_llist t⟩ = ⟨c #⇘n⇙ inf_llist t⟩› have "∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙"
      by (metis enat_ord_simps(1) enat_ord_simps(2) nAct_same_not_active)
    thus ?thesis using lNactLe_nact by (simp add: ‹n' < n›)
  qed
next
  assume "¬⟨c #⇘n'⇙ inf_llist t⟩ = ⟨c #⇘n⇙ inf_llist t⟩"
  with assms have "⟨c #⇘enat n'⇙ inf_llist t⟩ > ⟨c #⇘enat n⇙ inf_llist t⟩" by simp
  hence "n' > n" using nAct_strict_mono_back[of c "enat n" "inf_llist t" "enat n'"] by simp
  thus ?thesis by (meson dual_order.strict_implies_order lNactLe le_trans)
qed
  
lemma nAct_mono_lNact:
  assumes "⟨c ⇐ t⟩⇘n⇙ ≤ n'"
  shows "⟨c #⇘n⇙ inf_llist t⟩ ≤ ⟨c #⇘n'⇙ inf_llist t⟩"
proof -
  have "∄k. k≥⟨c ⇐ t⟩⇘n⇙ ∧ k<n ∧ ∥c∥⇘t k⇙" using lNact_notActive by auto
  moreover have "enat n - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
  moreover from ‹⟨c ⇐ t⟩⇘n⇙ ≤ n'› have "enat ⟨c ⇐ t⟩⇘n⇙ ≤ enat n" by simp
  ultimately have "⟨c #⇘n⇙ inf_llist t⟩=⟨c #⇘⟨c ⇐ t⟩⇘n⇙⇙ inf_llist t⟩" using nAct_not_active_same by simp
  thus ?thesis using nAct_mono assms by simp
qed
 
subsection "Next Active"
text ‹
  In the following, we introduce an operator to obtain the next point in time when a component is activated.
›
  
definition nxtAct :: "'id ⇒ (nat ⇒ cnf) ⇒ nat ⇒ nat" (‹⟨_ → _⟩⇘_⇙›)
  where "⟨c → t⟩⇘n⇙ ≡ (THE n'. n'≥n ∧ ∥c∥⇘t n'⇙ ∧ (∄k. k≥n ∧ k<n' ∧ ∥c∥⇘t k⇙))"

lemma nxtActI:
  fixes n::nat
    and t::"nat ⇒ cnf"
    and c::'id
  assumes "∃i≥n. ∥c∥⇘t i⇙"
  shows "⟨c → t⟩⇘n⇙ ≥ n ∧ ∥c∥⇘t ⟨c → t⟩⇘n⇙⇙ ∧ (∄k. k≥n ∧ k<⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘t k⇙)"
proof -
  let ?P = "THE n'. n'≥n ∧ ∥c∥⇘t n'⇙ ∧ (∄k. k≥n ∧ k<n' ∧ ∥c∥⇘t k⇙)"
  from assms obtain i where "i≥n ∧ ∥c∥⇘t i⇙ ∧ (∄k. k≥n ∧ k<i ∧ ∥c∥⇘t k⇙)"
    using lActive_least[of n "inf_llist t" c] by auto
  moreover have "(⋀x. n ≤ x ∧ ∥c∥⇘t x⇙ ∧ ¬ (∃k≥n. k < x ∧ ∥c∥⇘t k⇙) ⟹ x = i)"
  proof -
    fix x assume "n ≤ x ∧ ∥c∥⇘t x⇙ ∧ ¬ (∃k≥n. k < x ∧ ∥c∥⇘t k⇙)"
    show "x = i"
    proof (rule ccontr)
      assume "¬ (x = i)"
      thus False using ‹i≥n ∧ ∥c∥⇘t i⇙ ∧ (∄k. k≥n ∧ k<i ∧ ∥c∥⇘t k⇙)›
        ‹n ≤ x ∧ ∥c∥⇘t x⇙ ∧ ¬ (∃k≥n. k < x ∧ ∥c∥⇘t k⇙)› by fastforce
    qed
  qed
  ultimately have "(?P) ≥ n ∧ ∥c∥⇘t (?P)⇙ ∧ (∄k. k≥n ∧ k<?P ∧ ∥c∥⇘t k⇙)"
    using theI[of "λn'. n'≥n ∧ ∥c∥⇘t n'⇙ ∧ (∄k. k≥n ∧ k<n' ∧ ∥c∥⇘t k⇙)"] by blast
  thus ?thesis using nxtAct_def[of c t n] by metis
qed
  
lemma nxtActLe:
  fixes n n'
  assumes "∃i≥n. ∥c∥⇘t i⇙"
  shows "n ≤ ⟨c → t⟩⇘n⇙"
  by (simp add: assms nxtActI)

lemma nxtAct_eq:
  assumes "n'≥n"
    and "∥c∥⇘t n'⇙"
    and "∀n''≥n. n''<n' ⟶ ¬ ∥c∥⇘t n''⇙"
  shows "n' = ⟨c → t⟩⇘n⇙"
  by (metis assms(1) assms(2) assms(3) nxtActI linorder_neqE_nat nxtActLe)

lemma nxtAct_active:
  fixes i::nat
    and t::"nat ⇒ cnf"
    and c::'id
  assumes "∥c∥⇘t i⇙"
  shows "⟨c → t⟩⇘i⇙ = i" by (metis assms le_eq_less_or_eq nxtActI)
    
lemma nxtActive_no_active:
  assumes "∃!i. i≥n ∧ ∥c∥⇘t i⇙"
  shows "¬ (∃i'≥Suc ⟨c → t⟩⇘n⇙. ∥c∥⇘t i'⇙)"
proof
  assume "∃i'≥Suc ⟨c → t⟩⇘n⇙. ∥c∥⇘t i'⇙"
  then obtain i' where "i'≥Suc ⟨c → t⟩⇘n⇙" and "∥c∥⇘t i'⇙" by auto
  moreover from assms(1) have "⟨c → t⟩⇘n⇙≥n" using nxtActI by auto
  ultimately have "i'≥n" and "∥c∥⇘t i'⇙" and "i'≠⟨c → t⟩⇘n⇙" by auto
  moreover from assms(1) have "∥c∥⇘t ⟨c → t⟩⇘n⇙⇙" and "⟨c → t⟩⇘n⇙≥n" using nxtActI by auto
  ultimately show False using assms(1) by auto
qed
  
lemma nxt_geq_lNact[simp]:
  assumes "∃i≥n. ∥c∥⇘t i⇙"
  shows "⟨c → t⟩⇘n⇙≥⟨c ⇐ t⟩⇘n⇙"
proof -
  from assms have "n ≤ ⟨c → t⟩⇘n⇙" using nxtActLe by simp
  moreover have "⟨c ⇐ t⟩⇘n⇙≤n" by simp
  ultimately show ?thesis by arith
qed
  
lemma active_geq_nxtAct:
  assumes "∥c∥⇘t i⇙"
    and "the_enat (⟨c #⇘i⇙ inf_llist t⟩)≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)"
  shows "i≥⟨c → t⟩⇘n⇙"
proof cases
  assume "⟨c #⇘i⇙ inf_llist t⟩=⟨c #⇘n⇙ inf_llist t⟩"
  show ?thesis
  proof (rule ccontr)
    assume "¬ i≥⟨c → t⟩⇘n⇙"
    hence "i<⟨c → t⟩⇘n⇙" by simp
    with ‹⟨c #⇘i⇙ inf_llist t⟩=⟨c #⇘n⇙ inf_llist t⟩› have "¬ (∃k≥i. k < n ∧ ∥c∥⇘t k⇙)"
      by (metis enat_ord_simps(1) leD leI nAct_same_not_active)
    moreover have "¬ (∃k≥n. k <⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘t k⇙)" using nxtActI by blast
    ultimately have "¬ (∃k≥i. k <⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘t k⇙)" by auto
    with ‹i<⟨c → t⟩⇘n⇙› show False using ‹∥c∥⇘t i⇙› by simp
  qed
next
  assume "¬⟨c #⇘i⇙ inf_llist t⟩=⟨c #⇘n⇙ inf_llist t⟩"
  moreover from ‹the_enat (⟨c #⇘i⇙ inf_llist t⟩)≥the_enat (⟨c #⇘n⇙ inf_llist t⟩)›
  have "⟨c #⇘i⇙ inf_llist t⟩≥⟨c #⇘n⇙ inf_llist t⟩"
    by (metis enat.distinct(2) enat_ord_simps(1) nAct_enat_the_nat)
  ultimately have "⟨c #⇘i⇙ inf_llist t⟩>⟨c #⇘n⇙ inf_llist t⟩" by simp
  hence "i>n" using nAct_strict_mono_back[of c n "inf_llist t" i] by simp
  with ‹∥c∥⇘t i⇙› show ?thesis by (meson dual_order.strict_implies_order leI nxtActI)
qed

lemma nAct_same:
  assumes "⟨c ⇐ t⟩⇘n⇙ ≤ n'" and "n' ≤ ⟨c → t⟩⇘n⇙"
  shows "the_enat (⟨c #⇘enat n'⇙ inf_llist t⟩) = the_enat (⟨c #⇘enat n⇙ inf_llist t⟩)"
proof cases
  assume "n ≤ n'"
  moreover have "n' - 1 < llength (inf_llist t)" by simp
  moreover have "¬ (∃i≥n. i <n' ∧ ∥c∥⇘t i⇙)" by (meson assms(2) less_le_trans nxtActI)
  ultimately show ?thesis using nAct_not_active_same by (simp add: one_enat_def)
next
  assume "¬ n ≤ n'"
  hence "n' < n" by simp
  moreover have "n - 1 < llength (inf_llist t)" by simp
  moreover have "¬ (∃i≥n'. i < n ∧ ∥c∥⇘t i⇙)" by (metis ‹¬ n ≤ n'› assms(1) dual_order.trans lNAct_ex)
  ultimately show ?thesis using nAct_not_active_same[of n' n] by (simp add: one_enat_def)
qed
  
lemma nAct_mono_nxtAct:
  assumes "∃i≥n. ∥c∥⇘t i⇙"
    and "⟨c → t⟩⇘n⇙ ≤ n'"
  shows "⟨c #⇘n⇙ inf_llist t⟩ ≤ ⟨c #⇘n'⇙ inf_llist t⟩"
proof -
  from assms have "⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩ ≤ ⟨c #⇘n'⇙ inf_llist t⟩" using nAct_mono assms by simp
  moreover have "⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩=⟨c #⇘n⇙ inf_llist t⟩"
  proof -
    from assms have "∄k. k≥n ∧ k<⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘t k⇙" and "n ≤ ⟨c → t⟩⇘n⇙" using nxtActI by auto
    moreover have "enat ⟨c → t⟩⇘n⇙ - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
    ultimately show ?thesis using nAct_not_active_same[of n "⟨c → t⟩⇘n⇙"] by auto
  qed
  ultimately show ?thesis by simp
qed

subsection "Latest Activation"
text ‹
  In the following, we introduce an operator to obtain the latest point in time when a component is activated.
›

abbreviation latestAct_cond:: "'id ⇒ trace ⇒ nat ⇒ nat ⇒ bool"
  where "latestAct_cond c t n n' ≡ n'<n ∧ ∥c∥⇘t n'⇙"

definition latestAct:: "'id ⇒ trace ⇒ nat ⇒ nat" (‹⟨_ ← _⟩⇘_⇙›)
  where "latestAct c t n = (GREATEST n'. latestAct_cond c t n n')"

lemma latestActEx:
  assumes "∃n'<n. ∥nid∥⇘t n'⇙"
  shows "∃n'. latestAct_cond nid t n n' ∧ (∀n''. latestAct_cond nid t n n'' ⟶ n'' ≤ n')"
proof -
  from assms obtain n' where "latestAct_cond nid t n n'" by auto
  moreover have "∀n''>n. ¬ latestAct_cond nid t n n''" by simp
  ultimately obtain n' where "latestAct_cond nid t n n' ∧ (∀n''. latestAct_cond nid t n n'' ⟶ n'' ≤ n')"
    using boundedGreatest[of "latestAct_cond nid t n" n'] by blast
  thus ?thesis ..
qed

lemma latestAct_prop:
  assumes "∃n'<n. ∥nid∥⇘t n'⇙"
  shows "∥nid∥⇘t (latestAct nid t n)⇙" and "latestAct nid t n<n"
proof -
  from assms latestActEx have "latestAct_cond nid t n (GREATEST x. latestAct_cond nid t n x)"
    using GreatestI_ex_nat[of "latestAct_cond nid t n"] by blast
  thus "∥nid∥⇘t ⟨nid ← t⟩⇘n⇙⇙" and "latestAct nid t n<n" using latestAct_def by auto
qed

lemma latestAct_less:
  assumes "latestAct_cond nid t n n'"
  shows "n' ≤ ⟨nid ← t⟩⇘n⇙"
proof -
  from assms latestActEx have "n' ≤ (GREATEST x. latestAct_cond nid t n x)"
    using Greatest_le_nat[of "latestAct_cond nid t n"] by blast
  thus ?thesis using latestAct_def by auto
qed

lemma latestActNxt:
  assumes "∃n'<n. ∥nid∥⇘t n'⇙"
  shows "⟨nid → t⟩⇘⟨nid ← t⟩⇘n⇙⇙=⟨nid ← t⟩⇘n⇙"
  using assms latestAct_prop(1) nxtAct_active by auto

lemma latestActNxtAct:
  assumes "∃n'≥n. ∥tid∥⇘t n'⇙"
    and "∃n'<n. ∥tid∥⇘t n'⇙"
  shows "⟨tid → t⟩⇘n⇙ > ⟨tid ← t⟩⇘n⇙"
  by (meson assms latestAct_prop(2) less_le_trans nxtActI zero_le)

lemma latestActless:
  assumes "∃n'≥n⇩s. n'<n ∧ ∥nid∥⇘t n'⇙"
  shows "⟨nid ← t⟩⇘n⇙≥n⇩s"
  by (meson assms dual_order.trans latestAct_less)

lemma latestActEq:
  fixes nid::'id
  assumes "∥nid∥⇘t n'⇙" and "¬(∃n''>n'. n''<n ∧ ∥nid∥⇘t n'⇙)" and "n'<n"
  shows "⟨nid ← t⟩⇘n⇙ = n'"
  using latestAct_def
proof
  have "(GREATEST n'. latestAct_cond nid t n n') = n'"
  proof (rule Greatest_equality[of "latestAct_cond nid t n" n'])
    from assms(1) assms (3) show "latestAct_cond nid t n n'" by simp
  next
    fix y assume "latestAct_cond nid t n y"
    hence "∥nid∥⇘t y⇙" and "y<n" by auto
    thus "y ≤ n'" using assms(1) assms (2) leI by blast
  qed
  thus "n' = (GREATEST n'. latestAct_cond nid t n n')" by simp
qed
  
subsection "Last Activation"
text ‹
  In the following we introduce an operator to obtain the latest point in time where a certain component was activated within a certain configuration trace.
›

definition lActive :: "'id ⇒ (nat ⇒ cnf) ⇒ nat" (‹⟨_ ∧ _⟩›)
  where "⟨c ∧ t⟩ ≡ (GREATEST i. ∥c∥⇘t i⇙)"

lemma lActive_active:
  assumes "∥c∥⇘t i⇙"
    and "∀n' > n. ¬ (∥c∥⇘t n'⇙)"
  shows "∥c∥⇘t (⟨c ∧ t⟩)⇙"
proof -
  from assms obtain i' where "∥c∥⇘t i'⇙" and "⋀y. ∥c∥⇘t y⇙ ⟹ y ≤ i'"
    using boundedGreatest[of "λi'. ∥c∥⇘t i'⇙" i n] by blast
  thus ?thesis using lActive_def Nat.GreatestI_nat[of "λi'. ∥c∥⇘t i'⇙"] by metis
qed

lemma lActive_less:
  assumes "∥c∥⇘t i⇙"
    and "∀n' > n. ¬ (∥c∥⇘t n'⇙)"
  shows "⟨c ∧ t⟩ ≤ n"
proof (rule ccontr)
  assume "¬ ⟨c ∧ t⟩ ≤ n"
  hence "⟨c ∧ t⟩ > n" by simp
  moreover from assms have "∥c∥⇘t (⟨c ∧ t⟩)⇙" using lActive_active by simp
  ultimately show False using assms by simp
qed

lemma lActive_greatest:
  assumes "∥c∥⇘t i⇙"
    and "∀n' > n. ¬ (∥c∥⇘t n'⇙)"
  shows "i ≤ ⟨c ∧ t⟩"
proof -
  from assms obtain i' where "∥c∥⇘t i'⇙" and "⋀y. ∥c∥⇘t y⇙ ⟹ y ≤ i'"
    using boundedGreatest[of "λi'. ∥c∥⇘t i'⇙" i n] by blast
  with assms show ?thesis using lActive_def Nat.Greatest_le_nat[of "λi'. ∥c∥⇘t i'⇙" i] by metis
qed
  
lemma lActive_greater_active:
  assumes "n > ⟨c ∧ t⟩"
    and "∀n'' > n'. ¬ ∥c∥⇘t n''⇙"
  shows "¬ ∥c∥⇘t n⇙"
proof (rule ccontr)
  assume "¬ ¬ ∥c∥⇘t n⇙"
  with ‹∀n'' > n'. ¬ ∥c∥⇘t n''⇙› have "n ≤ ⟨c ∧ t⟩" using lActive_greatest by simp
  thus False using assms by simp
qed
  
lemma lActive_greater_active_all:
  assumes "∀n'' > n'. ¬ ∥c∥⇘t n''⇙"
  shows "¬(∃n > ⟨c ∧ t⟩. ∥c∥⇘t n⇙)" 
proof (rule ccontr)
  assume "¬¬(∃n > ⟨c ∧ t⟩. ∥c∥⇘t n⇙)"
  then obtain "n" where "n>⟨c ∧ t⟩" and "∥c∥⇘t n⇙" by blast
  with ‹∀n'' > n'. ¬ (∥c∥⇘t n''⇙)› have "¬ ∥c∥⇘t n⇙" using lActive_greater_active by simp
  with ‹∥c∥⇘t n⇙› show False by simp
qed

lemma lActive_equality:
  assumes "∥c∥⇘t i⇙"
    and "(⋀x. ∥c∥⇘t x⇙ ⟹ x ≤ i)"
  shows "⟨c ∧ t⟩ = i" unfolding lActive_def using assms Greatest_equality[of "λi'. ∥c∥⇘t i'⇙"] by simp
    
lemma nxtActive_lactive:
  assumes "∃i≥n. ∥c∥⇘t i⇙"
    and "¬ (∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙)"
  shows "⟨c → t⟩⇘n⇙=⟨c ∧ t⟩"
proof -
  from assms(1) have "∥c∥⇘t ⟨c → t⟩⇘n⇙⇙" using nxtActI by auto
  moreover from assms have "¬ (∃i'≥Suc ⟨c → t⟩⇘n⇙. ∥c∥⇘t i'⇙)" using nxtActive_no_active by simp
  hence "(⋀x. ∥c∥⇘t x⇙ ⟹ x ≤ ⟨c → t⟩⇘n⇙)" using not_less_eq_eq by auto
  ultimately show ?thesis using ‹¬ (∃i'≥Suc ⟨c → t⟩⇘n⇙. ∥c∥⇘t i'⇙)› lActive_equality by simp
qed
    
subsection "Mapping Time Points"
text ‹
  In the following we introduce two operators to map time-points between configuration traces and behavior traces.
›

subsubsection "Configuration Trace to Behavior Trace"
text ‹
  First we provide an operator which maps a point in time of a configuration trace to the corresponding point in time of a behavior trace.
›
  
definition cnf2bhv :: "'id ⇒ (nat ⇒ cnf) ⇒ nat ⇒ nat" (‹⇘_⇙↓⇘_⇙(_)› [150,150,150] 110)
  where "⇘c⇙↓⇘t⇙(n) ≡ the_enat(llength (π⇘c⇙(inf_llist t))) - 1 + (n - ⟨c ∧ t⟩)"

lemma cnf2bhv_mono:
  assumes "n'≥n"
  shows "⇘c⇙↓⇘t⇙(n') ≥ ⇘c⇙↓⇘t⇙(n)"
  by (simp add: assms cnf2bhv_def diff_le_mono)

lemma cnf2bhv_mono_strict:
  assumes "n≥⟨c ∧ t⟩" and "n'>n"
  shows "⇘c⇙↓⇘t⇙(n') > ⇘c⇙↓⇘t⇙(n)"
  using assms cnf2bhv_def by auto

text "Note that the functions are nat, that means that also in the case the difference is negative they will return a 0!"
lemma cnf2bhv_ge_llength[simp]:
  assumes "n≥⟨c ∧ t⟩"
  shows "⇘c⇙↓⇘t⇙(n) ≥ the_enat(llength (π⇘c⇙(inf_llist t))) - 1"
  using assms cnf2bhv_def by simp

lemma cnf2bhv_greater_llength[simp]:
  assumes "n>⟨c ∧ t⟩"
  shows "⇘c⇙↓⇘t⇙(n) > the_enat(llength (π⇘c⇙(inf_llist t))) - 1"
  using assms cnf2bhv_def by simp

lemma cnf2bhv_suc[simp]:
  assumes "n≥⟨c ∧ t⟩"
  shows "⇘c⇙↓⇘t⇙(Suc n) = Suc (⇘c⇙↓⇘t⇙(n))"
  using assms cnf2bhv_def by simp

lemma cnf2bhv_lActive[simp]:
  shows "⇘c⇙↓⇘t⇙(⟨c ∧ t⟩) = the_enat(llength (π⇘c⇙(inf_llist t))) - 1"
  using cnf2bhv_def by simp
    
lemma cnf2bhv_lnth_lappend:
  assumes act: "∃i. ∥c∥⇘t i⇙"
    and nAct: "∄i. i≥n ∧ ∥c∥⇘t i⇙"
  shows "lnth ((π⇘c⇙(inf_llist t)) @⇩l (inf_llist t')) (⇘c⇙↓⇘t⇙(n)) = lnth (inf_llist t') (n - ⟨c ∧ t⟩ - 1)"
    (is "?lhs = ?rhs")
proof -
  from nAct have "lfinite (π⇘c⇙(inf_llist t))" using proj_finite2 by auto
  then obtain k where k_def: "llength (π⇘c⇙(inf_llist t)) = enat k" using lfinite_llength_enat by blast
  moreover have "k ≤ ⇘c⇙↓⇘t⇙(n)"
  proof -
    from nAct have "∄i. i>n-1 ∧ ∥c∥⇘t i⇙" by simp
    with act have "⟨c ∧ t⟩ ≤ n-1" using lActive_less by auto
    moreover have "n>0" using act nAct by auto
    ultimately have "⟨c ∧ t⟩ < n" by simp
    hence "the_enat (llength (π⇘c⇙inf_llist t)) - 1 < ⇘c⇙↓⇘t⇙(n)" using cnf2bhv_greater_llength by simp
    with k_def show ?thesis by simp
  qed
  ultimately have "?lhs = lnth (inf_llist t') (⇘c⇙↓⇘t⇙(n) - k)" using lnth_lappend2 by blast
  moreover have "⇘c⇙↓⇘t⇙(n) - k = n - ⟨c ∧ t⟩ - 1"
  proof -
    from cnf2bhv_def have "⇘c⇙↓⇘t⇙(n) - k = the_enat (llength (π⇘c⇙inf_llist t)) - 1 + (n - ⟨c ∧ t⟩) - k"
      by simp
    also have "… = the_enat (llength (π⇘c⇙inf_llist t)) - 1 + (n - ⟨c ∧ t⟩) -
      the_enat (llength (π⇘c⇙(inf_llist t)))" using k_def by simp
    also have "… = the_enat (llength (π⇘c⇙inf_llist t)) + (n - ⟨c ∧ t⟩) - 1 -
      the_enat (llength (π⇘c⇙(inf_llist t)))"
    proof -
      have "∃i. enat i < llength (inf_llist t) ∧ ∥c∥⇘lnth (inf_llist t) i⇙" by (simp add: act)
      hence "llength (π⇘c⇙inf_llist t) ≥ 1" using proj_one by simp
      moreover from k_def have "llength (π⇘c⇙inf_llist t) ≠ ∞" by simp
      ultimately have "the_enat (llength (π⇘c⇙inf_llist t)) ≥ 1" by (simp add: k_def one_enat_def)
      thus ?thesis by simp
    qed
    also have "… = the_enat (llength (π⇘c⇙inf_llist t)) + (n - ⟨c ∧ t⟩) -
      the_enat (llength (π⇘c⇙(inf_llist t))) - 1" by simp
    also have "… = n - ⟨c ∧ t⟩ - 1" by simp
    finally show ?thesis .
  qed
  ultimately show ?thesis by simp
qed

lemma nAct_cnf2proj_Suc_dist:
  assumes "∃i≥n. ∥c∥⇘t i⇙"
    and "¬(∃i>⟨c → t⟩⇘n⇙. ∥c∥⇘t i⇙)"
  shows "Suc (the_enat ⟨c #⇘enat n⇙inf_llist t⟩)=⇘c⇙↓⇘t⇙(Suc ⟨c → t⟩⇘n⇙)"
proof -
  have "the_enat ⟨c #⇘enat n⇙inf_llist t⟩ = ⇘c⇙↓⇘t⇙(⟨c → t⟩⇘n⇙)" (is "?LHS = ?RHS")
  proof -
    from assms have "?RHS = the_enat(llength (π⇘c⇙(inf_llist t))) - 1"
      using nxtActive_lactive[of n c t] by simp
    also have "llength (π⇘c⇙(inf_llist t)) = eSuc (⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩)"
    proof -
      from assms have "¬ (∃i'≥ Suc (⟨c → t⟩⇘n⇙). ∥c∥⇘t i'⇙)" using nxtActive_no_active by simp
      hence "⟨c #⇘Suc (⟨c → t⟩⇘n⇙)⇙ inf_llist t⟩ = llength (π⇘c⇙(inf_llist t))"
        using nAct_eq_proj[of "Suc (⟨c → t⟩⇘n⇙)" c "inf_llist t"] by simp
      moreover from assms(1) have "∥c∥⇘t (⟨c → t⟩⇘n⇙)⇙" using nxtActI by blast
      hence "⟨c #⇘Suc (⟨c → t⟩⇘n⇙)⇙ inf_llist t⟩ = eSuc (⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩)" by simp
      ultimately show ?thesis by simp
    qed
    also have "the_enat(eSuc (⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩)) - 1 = (⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩)"
    proof -
      have "⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩ ≠ ∞" by simp
      hence "the_enat(eSuc (⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩)) = Suc(the_enat(⟨c #⇘⟨c → t⟩⇘n⇙⇙ inf_llist t⟩))"
        using the_enat_eSuc by simp
      thus ?thesis by simp
    qed
    also have "… = ?LHS"
    proof -
      have "enat ⟨c → t⟩⇘n⇙ - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
      moreover from assms(1) have "⟨c → t⟩⇘n⇙≥n" and
        "∄k. enat n ≤ enat k ∧ enat k < enat ⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘lnth (inf_llist t) k⇙" using nxtActI by auto
      ultimately have "⟨c #⇘enat ⟨c → t⟩⇘n⇙⇙inf_llist t⟩ = ⟨c #⇘enat n⇙inf_llist t⟩"
        using nAct_not_active_same[of n "⟨c → t⟩⇘n⇙" "inf_llist t" c] by simp
      moreover have "⟨c #⇘enat n⇙inf_llist t⟩≠∞" by simp
      ultimately show ?thesis by auto
    qed
    finally show ?thesis by fastforce
  qed      
  moreover from assms have "⟨c → t⟩⇘n⇙=⟨c ∧ t⟩" using nxtActive_lactive by simp
  hence "Suc (⇘c⇙↓⇘t⇙(⟨c → t⟩⇘n⇙)) = ⇘c⇙↓⇘t⇙(Suc ⟨c → t⟩⇘n⇙)" using cnf2bhv_suc[where n="⟨c → t⟩⇘n⇙"] by simp
  ultimately show ?thesis by simp
qed

subsubsection "Behavior Trace to Configuration Trace"
text ‹
  Next we define an operator to map a point in time of a behavior trace back to a corresponding point in time for a configuration trace.
›

definition bhv2cnf :: "'id ⇒ (nat ⇒ cnf) ⇒ nat ⇒ nat" (‹⇘_⇙↑⇘_⇙(_)› [150,150,150] 110)
  where "⇘c⇙↑⇘t⇙(n) ≡ ⟨c ∧ t⟩ + (n - (the_enat(llength (π⇘c⇙(inf_llist t))) - 1))"

lemma bhv2cnf_mono:
  assumes "n'≥n"
  shows "⇘c⇙↑⇘t⇙(n') ≥ ⇘c⇙↑⇘t⇙(n)"
  by (simp add: assms bhv2cnf_def diff_le_mono)    

lemma bhv2cnf_mono_strict:
  assumes "n'>n"
    and "n ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1"
  shows "⇘c⇙↑⇘t⇙(n') > ⇘c⇙↑⇘t⇙(n)"
  using assms bhv2cnf_def by auto

text "Note that the functions are nat, that means that also in the case the difference is negative they will return a 0!"
lemma bhv2cnf_ge_lActive[simp]:
  shows "⇘c⇙↑⇘t⇙(n) ≥ ⟨c ∧ t⟩"
  using bhv2cnf_def by simp

lemma bhv2cnf_greater_lActive[simp]:
  assumes "n>the_enat(llength (π⇘c⇙(inf_llist t))) - 1"
  shows "⇘c⇙↑⇘t⇙(n) > ⟨c ∧ t⟩"
  using assms bhv2cnf_def by simp
    
lemma bhv2cnf_lActive[simp]:
  assumes "∃i. ∥c∥⇘t i⇙"
    and "lfinite (π⇘c⇙(inf_llist t))"
  shows "⇘c⇙↑⇘t⇙(the_enat(llength (π⇘c⇙(inf_llist t)))) = Suc (⟨c ∧ t⟩)"
proof -
  from assms have "π⇘c⇙(inf_llist t)≠ []⇩l" by simp
  hence "llength (π⇘c⇙(inf_llist t)) > 0" by (simp add: lnull_def)
  moreover from ‹lfinite (π⇘c⇙(inf_llist t))› have "llength (π⇘c⇙(inf_llist t)) ≠ ∞"
    using llength_eq_infty_conv_lfinite by auto
  ultimately have "the_enat(llength (π⇘c⇙(inf_llist t))) > 0" using enat_0_iff(1) by fastforce
  hence "the_enat(llength (π⇘c⇙(inf_llist t))) - (the_enat(llength (π⇘c⇙(inf_llist t))) - 1) = 1" by simp
  thus ?thesis using bhv2cnf_def by simp
qed
  
subsubsection "Relating the Mappings"
text ‹
  In the following we provide some properties about the relationship between the two mapping operators.
›
  
lemma bhv2cnf_cnf2bhv:
  assumes "n ≥ ⟨c ∧ t⟩"
  shows "⇘c⇙↑⇘t⇙(⇘c⇙↓⇘t⇙(n)) = n" (is "?lhs = ?rhs")
proof -
  have "?lhs = ⟨c ∧ t⟩ + ((⇘c⇙↓⇘t⇙(n)) - (the_enat(llength (π⇘c⇙(inf_llist t))) - 1))"
    using bhv2cnf_def by simp
  also have "… = ⟨c ∧ t⟩ + (((the_enat (llength (π⇘c⇙(inf_llist t)))) - 1 + (n - ⟨c ∧ t⟩)) -
    (the_enat (llength (π⇘c⇙(inf_llist t))) - 1))" using cnf2bhv_def by simp
  also have "(the_enat(llength (π⇘c⇙(inf_llist t)))) - 1 + (n - (⟨c ∧ t⟩)) -
    (the_enat (llength (π⇘c⇙(inf_llist t))) - 1) = (the_enat(llength (π⇘c⇙(inf_llist t)))) - 1 -
    ((the_enat (llength (π⇘c⇙(inf_llist t)))) - 1) + (n - (⟨c ∧ t⟩))" by simp
  also have "… = n - (⟨c ∧ t⟩)" by simp
  also have "(⟨c ∧ t⟩) + (n - (⟨c ∧ t⟩)) = (⟨c ∧ t⟩) + n - ⟨c ∧ t⟩" using assms by simp
  also have "… = ?rhs" by simp
  finally show ?thesis .
qed
    
lemma cnf2bhv_bhv2cnf:
  assumes "n ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1"
  shows "⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(n)) = n" (is "?lhs = ?rhs")
proof -
  have "?lhs = the_enat(llength (π⇘c⇙(inf_llist t))) - 1 + ((⇘c⇙↑⇘t⇙(n)) - (⟨c ∧ t⟩))"
    using cnf2bhv_def by simp
  also have "… = the_enat(llength (π⇘c⇙(inf_llist t))) - 1 + (⟨c ∧ t⟩ +
    (n - (the_enat(llength (π⇘c⇙(inf_llist t))) - 1)) - (⟨c ∧ t⟩))" using bhv2cnf_def by simp
  also have "⟨c ∧ t⟩ + (n - (the_enat(llength (π⇘c⇙(inf_llist t))) - 1)) - (⟨c ∧ t⟩) =
    ⟨c ∧ t⟩ - (⟨c ∧ t⟩) + (n - (the_enat(llength (π⇘c⇙(inf_llist t))) - 1))" by simp
  also have "… = n - (the_enat(llength (π⇘c⇙(inf_llist t))) - 1)" by simp      
  also have "the_enat (llength (π⇘c⇙(inf_llist t))) - 1 + (n - (the_enat (llength (π⇘c⇙(inf_llist t))) - 1)) =
    n - (the_enat (llength (π⇘c⇙(inf_llist t))) - 1) + (the_enat (llength (π⇘c⇙(inf_llist t))) - 1)" by simp
  also have "… = n + ((the_enat (llength (π⇘c⇙(inf_llist t))) - 1) -
    (the_enat (llength (π⇘c⇙(inf_llist t))) - 1))" using assms by simp
  also have "… = ?rhs" by simp
  finally show ?thesis .
qed
  
lemma p2c_mono_c2p:
  assumes "n ≥ ⟨c ∧ t⟩"
      and "n' ≥ ⇘c⇙↓⇘t⇙(n)"
    shows "⇘c⇙↑⇘t⇙(n') ≥ n"
proof -
  from ‹n' ≥ ⇘c⇙↓⇘t⇙(n)› have "⇘c⇙↑⇘t⇙(n') ≥ ⇘c⇙↑⇘t⇙(⇘c⇙↓⇘t⇙(n))" using bhv2cnf_mono by simp
  thus ?thesis using bhv2cnf_cnf2bhv ‹n ≥ ⟨c ∧ t⟩› by simp
qed
  
lemma p2c_mono_c2p_strict:
  assumes "n ≥ ⟨c ∧ t⟩"
      and "n<⇘c⇙↑⇘t⇙(n')"
  shows "⇘c⇙↓⇘t⇙(n) < n'"
proof (rule ccontr)
  assume "¬ (⇘c⇙↓⇘t⇙(n) < n')"
  hence "⇘c⇙↓⇘t⇙(n) ≥ n'" by simp
  with ‹n ≥ ⟨c ∧ t⟩› have "⇘c⇙↑⇘t⇙(nat (⇘c⇙↓⇘t⇙(n))) ≥ ⇘c⇙↑⇘t⇙(n')"
    using bhv2cnf_mono by simp
  hence "¬(⇘c⇙↑⇘t⇙(nat (⇘c⇙↓⇘t⇙(n))) < ⇘c⇙↑⇘t⇙(n'))" by simp
  with ‹n ≥ ⟨c ∧ t⟩› have  "¬(n < ⇘c⇙↑⇘t⇙(n'))"
    using "bhv2cnf_cnf2bhv" by simp
  with assms show False by simp
qed
  
lemma c2p_mono_p2c:
  assumes "n ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1"
      and "n' ≥ ⇘c⇙↑⇘t⇙(n)"
    shows "⇘c⇙↓⇘t⇙(n') ≥ n"
proof -
  from ‹n' ≥ ⇘c⇙↑⇘t⇙(n)› have "⇘c⇙↓⇘t⇙(n') ≥ ⇘c⇙↓⇘t⇙(⇘c⇙↑⇘t⇙(n))" using cnf2bhv_mono by simp
  thus ?thesis using cnf2bhv_bhv2cnf ‹n ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1› by simp
qed

lemma c2p_mono_p2c_strict:
  assumes "n ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1"
      and "n<⇘c⇙↓⇘t⇙(n')"
  shows "⇘c⇙↑⇘t⇙(n) < n'"
proof (rule ccontr)
  assume "¬ (⇘c⇙↑⇘t⇙(n) < n')"
  hence "⇘c⇙↑⇘t⇙(n) ≥ n'" by simp
  with ‹n ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1› have "⇘c⇙↓⇘t⇙(nat (⇘c⇙↑⇘t⇙(n))) ≥ ⇘c⇙↓⇘t⇙(n')"
    using cnf2bhv_mono by simp
  hence "¬(⇘c⇙↓⇘t⇙(nat (⇘c⇙↑⇘t⇙(n))) < ⇘c⇙↓⇘t⇙(n'))" by simp
  with ‹n ≥ the_enat (llength (π⇘c⇙(inf_llist t))) - 1› have  "¬(n < ⇘c⇙↓⇘t⇙(n'))"
    using "cnf2bhv_bhv2cnf" by simp
  with assms show False by simp
qed

end

end