Theory Operational_SoundComplete

theory Operational_SoundComplete
imports Coinductive_Prop
chapter‹Main Theorems›

theory Operational_SoundComplete
imports
  Coinductive_Prop

begin
text ‹
  Using the properties we have shown about the interpretation of configurations 
  and the stepwise unfolding of the denotational semantics, we can now prove 
  several important results about the construction of runs from a specification.
›
section ‹Initial configuration›

text ‹
  The denotational semantics of a specification @{term ‹Ψ›} is the interpretation 
  at the first instant of a configuration which has @{term ‹Ψ›} as its present.
  This means that we can start to build a run that satisfies a specification by 
  starting from this configuration.
›
theorem solve_start:
  shows ‹⟦⟦ Ψ ⟧⟧TESL = ⟦ [], 0 ⊨ Ψ ▹ [] ⟧config
  proof -
    have ‹⟦⟦ Ψ ⟧⟧TESL = ⟦⟦ Ψ ⟧⟧TESL≥ 0
    by (simp add: TESL_interpretation_stepwise_zero')
    moreover have ‹⟦ [], 0 ⊨ Ψ ▹ [] ⟧config =
                      ⟦⟦ [] ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ 0 ∩ ⟦⟦ [] ⟧⟧TESL≥ Suc 0
    by simp
    ultimately show ?thesis by auto
  qed

section ‹Soundness›
text ‹
  The interpretation of a configuration @{term ‹𝒮2›} that is a refinement of a
  configuration @{term ‹𝒮1›} is contained in the interpretation of @{term ‹𝒮1›}.
  This means that by making successive choices in building the instants of a run,
  we preserve the soundness of the constructed run with regard to the original 
  specification.
›
lemma sound_reduction:
  assumes ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1)  ↪  (Γ2, n2 ⊨ Ψ2 ▹ Φ2)›
  shows ‹⟦⟦ Γ1 ⟧⟧prim ∩ ⟦⟦ Ψ1 ⟧⟧TESL≥ n1 ∩ ⟦⟦ Φ1 ⟧⟧TESL≥ Suc n1
          ⊇  ⟦⟦ Γ2 ⟧⟧prim ∩ ⟦⟦ Ψ2 ⟧⟧TESL≥ n2 ∩ ⟦⟦ Φ2 ⟧⟧TESL≥ Suc n2 (is ?P)
proof -
  from assms consider
    (a) ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1)  ↪i2, n2 ⊨ Ψ2 ▹ Φ2)›
  | (b) ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1)  ↪e2, n2 ⊨ Ψ2 ▹ Φ2)›
    using operational_semantics_step.simps by blast
  thus ?thesis
  proof (cases)
    case a
      thus ?thesis by (simp add: operational_semantics_intro.simps)
  next
    case b thus ?thesis
    proof (rule operational_semantics_elim.cases)
      fix  Γ n C1 τ C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ (C1 sporadic τ on C2) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ))›
      thus ?P using configuration_interp_stepwise_sporadicon_cases
                    configuration_interpretation.simps by blast
    next
      fix  Γ n C1 τ C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ (C1 sporadic τ on C2) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ)›
      thus ?P using configuration_interp_stepwise_sporadicon_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 τexpr C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ (C1 sporadic♯ τexpr on C2) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ))›
      thus ?P using configuration_interp_stepwise_sporadicon_tvar_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 τexpr C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ (C1 sporadic♯ τexpr on C2) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ)›
      thus ?P using configuration_interp_stepwise_sporadicon_tvar_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 C2 R Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ (time-relation ⌊C1, C2⌋ ∈ R) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((⌊τvar (C1, n), τvar (C2, n)⌋ ∈ R) # Γ), n
                                      ⊨ Ψ ▹ ((time-relation ⌊C1, C2⌋ ∈ R) # Φ))›
      thus ?P using configuration_interp_stepwise_tagrel_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ (C1 implies C2) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ))›
      thus ?P using configuration_interp_stepwise_implies_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ ((C1 implies C2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((C1 ⇑ n) # (C2 ⇑ n) # Γ), n
                                   ⊨ Ψ ▹ ((C1 implies C2) # Φ))›
      thus ?P using configuration_interp_stepwise_implies_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ))›
      thus ?P using configuration_interp_stepwise_implies_not_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n
                                   ⊨ Ψ ▹ ((C1 implies not C2) # Φ))›
      thus ?P using configuration_interp_stepwise_implies_not_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 δτ C2 C3 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) =
                (Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) =
            (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))›
      thus ?P using configuration_interp_stepwise_timedelayed_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 δτ C2 C3 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) =
               (Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2)
            = (((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
                ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))›
      thus ?P using configuration_interp_stepwise_timedelayed_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 δτ C2 C3 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ (C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))›
      thus ?P using configuration_interp_stepwise_timedelayed_tvar_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 δτ C2 C3 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ (C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ ▹ Φ)›
         and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((C1 ⇑ n) # Γ), n ⊨ (C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2) #
               Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))›
      thus ?P using configuration_interp_stepwise_timedelayed_tvar_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ ((C1 weakly precedes C2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((⌈# C2 n, # C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊨ Ψ ▹ ((C1 weakly precedes C2) # Φ))›
      thus ?P using configuration_interp_stepwise_weakly_precedes_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ ((C1 strictly precedes C2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((⌈# C2 n, #< C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊨ Ψ ▹ ((C1 strictly precedes C2) # Φ))›
      thus ?P using configuration_interp_stepwise_strictly_precedes_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) = (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))›
      thus ?P using configuration_interp_stepwise_kills_cases
                    configuration_interpretation.simps by blast
    next
      fix Γ n C1 C2 Ψ Φ
      assume ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1) = (Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊨ Ψ2 ▹ Φ2) =
            (((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))›
      thus ?P using configuration_interp_stepwise_kills_cases
                    configuration_interpretation.simps by blast
    qed
  qed
qed

inductive_cases step_elim:‹𝒮1 ↪ 𝒮2

lemma sound_reduction':
  assumes ‹𝒮1 ↪ 𝒮2
  shows ‹⟦ 𝒮1config ⊇ ⟦ 𝒮2config
proof -
  have ‹∀s1 s2. (⟦ s2config ⊆ ⟦ s1config) ∨ ¬(s1 ↪ s2)›
    using sound_reduction by fastforce
  thus ?thesis using assms by blast
qed

lemma sound_reduction_generalized:
  assumes ‹𝒮1k 𝒮2
    shows ‹⟦ 𝒮1config ⊇ ⟦ 𝒮2config
proof -
  from assms show ?thesis
  proof (induction k arbitrary: 𝒮2)
    case 0
      hence *: ‹𝒮10 𝒮2 ⟹ 𝒮1 = 𝒮2 by auto
      moreover have ‹𝒮1 = 𝒮2 using * "0.prems" by linarith
      ultimately show ?case by auto
  next
    case (Suc k)
      thus ?case
      proof -
        fix k :: nat
        assume ff: ‹𝒮1Suc k 𝒮2
        assume hi: ‹⋀𝒮2. 𝒮1k 𝒮2 ⟹ ⟦ 𝒮2config ⊆ ⟦ 𝒮1config
        obtain 𝒮n where red_decomp: ‹(𝒮1k 𝒮n) ∧ (𝒮n ↪ 𝒮2)› using ff by auto
        hence ‹⟦ 𝒮1config ⊇ ⟦ 𝒮nconfig using hi by simp
        also have ‹⟦ 𝒮nconfig ⊇ ⟦ 𝒮2config by (simp add: red_decomp sound_reduction')
        ultimately show ‹⟦ 𝒮1config ⊇ ⟦ 𝒮2config by simp
      qed
  qed
qed

text ‹
  From the initial configuration, a configuration @{term ‹𝒮›} obtained after any 
  number @{term ‹k›} of reduction steps denotes runs from the 
  initial specification @{term ‹Ψ›}.
›
theorem soundness:
  assumes ‹([], 0 ⊨ Ψ ▹ []) ↪k 𝒮›
    shows ‹⟦⟦ Ψ ⟧⟧TESL ⊇ ⟦ 𝒮 ⟧config
  using assms sound_reduction_generalized solve_start by blast

section ‹Completeness›

text ‹
  We will now show that any run that satisfies a specification can be derived
  from the initial configuration, at any number of steps.

  We start by proving that any run that is denoted by a configuration @{term ‹𝒮›}
  is necessarily denoted by at least one of the configurations that can be reached
  from @{term ‹𝒮›}.
›
lemma complete_direct_successors:
  shows ‹⟦ Γ, n ⊨ Ψ ▹ Φ ⟧config ⊆ (⋃X∈𝒞next (Γ, n ⊨ Ψ ▹ Φ). ⟦ X ⟧config)›
  proof (induct Ψ)
    case Nil
    show ?case
      using configuration_interp_stepwise_instant_cases operational_semantics_step.simps
            operational_semantics_intro.instant_i
      by fastforce
  next
    case (Cons ψ Ψ)  thus ?case
      proof (cases ψ)
        case (SporadicOn K1 τ K2) thus ?thesis 
          using configuration_interp_stepwise_sporadicon_cases
                                      [of ‹Γ› ‹n› ‹K1› ‹τ› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_sporadicon[of ‹Γ› ‹n› ‹Ψ› ‹K1› ‹τ› ‹K2› ‹Φ›] by blast
      next
        case (SporadicOnTvar X1 X2 X3) thus ?thesis
          using configuration_interp_stepwise_sporadicon_tvar_cases
                                           [of ‹Γ› ‹n› ‹X1› ‹X2› ‹X3› ‹Ψ› ‹Φ›]
                Cnext_solve_sporadicon_tvar[of ‹Γ› ‹n› ‹Ψ› ‹X1› ‹X2› ‹X3› ‹Φ›] by blast
      next
        case (TagRelation C1 C2 R) thus ?thesis
          using configuration_interp_stepwise_tagrel_cases
                                  [of ‹Γ› ‹n› ‹C1 ‹C2 ‹R› ‹Ψ› ‹Φ›]
                Cnext_solve_tagrel[of ‹C1 ‹n› ‹C2 ‹R› ‹Γ› ‹Ψ› ‹Φ›] by blast
      next
        case (Implies K1 K2) thus ?thesis
          using configuration_interp_stepwise_implies_cases
                                   [of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_implies[of ‹K1› ‹n› ‹Γ› ‹Ψ› ‹K2› ‹Φ›] by blast
      next
        case (ImpliesNot K1 K2) thus ?thesis
          using configuration_interp_stepwise_implies_not_cases
                                       [of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_implies_not[of ‹K1› ‹n› ‹Γ› ‹Ψ› ‹K2› ‹Φ›] by blast
      next
        case (TimeDelayedBy Kmast τ Kmeas Kslave) thus ?thesis
          using configuration_interp_stepwise_timedelayed_cases
                          [of ‹Γ› ‹n› ‹Kmast› ‹τ› ‹Kmeas› ‹Kslave› ‹Ψ› ‹Φ›]
                Cnext_solve_timedelayed
                          [of ‹Kmast› ‹n› ‹Γ› ‹Ψ› ‹τ› ‹Kmeas› ‹Kslave› ‹Φ›] by blast
      next
        case (RelaxedTimeDelayed Kmast τ Kmeas Kslave) thus ?thesis
          using configuration_interp_stepwise_timedelayed_tvar_cases
                          [of ‹Γ› ‹n› ‹Kmast› ‹τ› ‹Kmeas› ‹Kslave› ‹Ψ› ‹Φ›]
                Cnext_solve_timedelayed_tvar
                          [of ‹Kmast› ‹n› ‹Γ› ‹Ψ› ‹τ› ‹Kmeas› ‹Kslave› ‹Φ›] by blast
      next
        case (WeaklyPrecedes K1 K2) thus ?thesis
          using configuration_interp_stepwise_weakly_precedes_cases
                                           [of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_weakly_precedes[of ‹K2› ‹n› ‹K1› ‹Γ› ‹Ψ›  ‹Φ›]
          by blast
      next
        case (StrictlyPrecedes K1 K2)  thus ?thesis
          using configuration_interp_stepwise_strictly_precedes_cases
                                             [of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_strictly_precedes[of ‹K2› ‹n› ‹K1› ‹Γ› ‹Ψ›  ‹Φ›]
          by blast
      next
        case (Kills K1 K2) thus ?thesis
          using configuration_interp_stepwise_kills_cases[of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_kills[of ‹K1› ‹n› ‹Γ› ‹Ψ› ‹K2› ‹Φ›] by blast
      qed
  qed

lemma complete_direct_successors':
  shows ‹⟦ 𝒮 ⟧config ⊆ (⋃X∈𝒞next 𝒮. ⟦ X ⟧config)›
proof -
  from configuration_interpretation.cases obtain Γ n Ψ Φ
    where ‹𝒮 = (Γ, n ⊨ Ψ ▹ Φ)› by blast
  with complete_direct_successors[of ‹Γ› ‹n› ‹Ψ› ‹Φ›] show ?thesis by simp
qed

text ‹
  Therefore, if a run belongs to a configuration, it necessarily belongs to a
  configuration derived from it.
›
lemma branch_existence:
  assumes ‹ρ ∈ ⟦ 𝒮1config
  shows ‹∃𝒮2. (𝒮1 ↪ 𝒮2) ∧ (ρ ∈ ⟦ 𝒮2config)›
proof -
  from assms complete_direct_successors' have ‹ρ ∈ (⋃X∈𝒞next 𝒮1. ⟦ X ⟧config)› by blast
  hence ‹∃s∈𝒞next 𝒮1. ρ ∈ ⟦ s ⟧config by simp
  thus ?thesis by blast
qed

lemma branch_existence':
  assumes ‹ρ ∈ ⟦ 𝒮1config
  shows ‹∃𝒮2. (𝒮1k 𝒮2) ∧ (ρ ∈ ⟦ 𝒮2config)›
proof (induct k)
  case 0
    thus ?case by (simp add: assms)
next
  case (Suc k)
    thus ?case
      using branch_existence relpowp_Suc_I[of ‹k› ‹operational_semantics_step›]
    by blast
qed

text‹
  Any run that belongs to the original specification @{term ‹Ψ›} has a corresponding 
  configuration @{term ‹𝒮›} at any number @{term ‹k›} of reduction steps
  from the initial configuration. Therefore, any run that satisfies a specification
  can be derived from the initial configuration at any level of reduction.
›
theorem completeness:
  assumes ‹ρ ∈ ⟦⟦ Ψ ⟧⟧TESL
  shows ‹∃𝒮. (([], 0 ⊨ Ψ ▹ [])  ↪k  𝒮)
           ∧ ρ ∈ ⟦ 𝒮 ⟧config
  using assms branch_existence' solve_start by blast

section ‹Progress›

text ‹
  Reduction steps do not guarantee that the construction of a run progresses in the
  sequence of instants. We need to show that it is always possible to reach the next 
  instant, and therefore any future instant, through a number of steps.
›
lemma instant_index_increase:
  assumes ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ Φ ⟧config
  shows   ‹∃Γk Ψk Φk k. ((Γ, n ⊨ Ψ ▹ Φ)  ↪kk, Suc n ⊨ Ψk ▹ Φk))
                         ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
proof (insert assms, induct Ψ arbitrary: Γ Φ)
  case (Nil Γ Φ)
    then show ?case
    proof -
      have ‹(Γ, n ⊨ [] ▹ Φ) ↪1 (Γ, Suc n ⊨ Φ ▹ [])›
        using instant_i intro_part by fastforce
      moreover have ‹⟦ Γ, n ⊨ [] ▹ Φ ⟧config = ⟦ Γ, Suc n ⊨ Φ ▹ [] ⟧config
        by auto
      moreover have ‹ρ ∈ ⟦ Γ, Suc n ⊨ Φ ▹ [] ⟧config
        using assms Nil.prems calculation(2) by blast
      ultimately show ?thesis by blast
    qed
next
  case (Cons ψ Ψ)
    then show ?case
    proof (induct ψ)
      case (SporadicOn C1 τ C2)
        have branches: ‹⟦ Γ, n ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ ⟧config
                      = ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ) ⟧config
                      ∪ ⟦ ((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧config
          using configuration_interp_stepwise_sporadicon_cases by simp
        have br1: ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ) ⟧config
                    ⟹ ∃Γk Ψk Φk k.
                      ((Γ, n ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ)
                          ↪kk, Suc n ⊨ Ψk ▹ Φk))
                      ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
        proof -
          assume h1: ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ) ⟧config
          hence ‹∃Γk Ψk Φk k. ((Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ))
                                      ↪kk, Suc n ⊨ Ψk ▹ Φk))
                                 ∧ (ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig)›
            using h1 SporadicOn.prems by simp
          from this obtain Γk Ψk Φk k where
              fp:‹((Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ))
                    ↪kk, Suc n ⊨ Ψk ▹ Φk))
                ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
          have
            ‹(Γ, n ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ)
              ↪ (Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ))›
            by (simp add: elims_part sporadic_on_e1)
          with fp relpowp_Suc_I2 have
            ‹((Γ, n ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ)
              ↪Suc kk, Suc n ⊨ Ψk ▹ Φk))› by auto
          thus ?thesis using fp by blast
        qed
        have br2: ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧config
                  ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ)
                                        ↪kk, Suc n ⊨ Ψk ▹ Φk))
                            ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
        proof -
          assume h2: ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧config
          hence ‹∃Γk Ψk Φk k. ((((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ)
                                    ↪kk, Suc n ⊨ Ψk ▹ Φk))
                             ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
            using h2 SporadicOn.prems by simp

            from this obtain Γk Ψk Φk k
            where fp:‹((((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ)
                            ↪kk, Suc n ⊨ Ψk ▹ Φk))›
              and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
            have pc:‹(Γ, n ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ)
              ↪ (((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ)›
            by (simp add: elims_part sporadic_on_e2)
            hence ‹(Γ, n ⊨ (C1 sporadic τ on C2) # Ψ ▹ Φ)
                    ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
                using fp relpowp_Suc_I2 by auto
            with rc show ?thesis by blast
        qed
        from branches SporadicOn.prems(2) have
          ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ) ⟧config
             ∪ ⟦ ((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧config
          by simp
        with br1 br2 show ?case by blast
    next
      case (SporadicOnTvar C1 τexpr C2)
        have branches: ‹⟦ Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ ⟧config
                      = ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ) ⟧config
                      ∪ ⟦ ((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ ⟧config
          using configuration_interp_stepwise_sporadicon_tvar_cases by simp
        have br1: ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ) ⟧config
                    ⟹ ∃Γk Ψk Φk k.
                      ((Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ)
                          ↪kk, Suc n ⊨ Ψk ▹ Φk))
                      ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
        proof -
          assume h:‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ) ⟧config
          hence ‹∃Γk Ψk Φk k.
                    ((Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ))
                        ↪kk, Suc n ⊨ Ψk ▹ Φk))
                    ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
            using Cons.hyps by blast
          from this obtain Γk Ψk Φk k where
               ‹((Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ)) ↪kk, Suc n ⊨ Ψk ▹ Φk))›
              and *:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
          moreover have ‹(Γ, n ⊨((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ)
                          ↪(Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ))›
            by (simp add: sporadic_on_tvar_e1 elims_part)
          ultimately have ‹((Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ)
                        ↪Suc kk, Suc n ⊨ Ψk ▹ Φk))›
            using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast
          with * have ‹((Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ)
                        ↪Suc kk, Suc n ⊨ Ψk ▹ Φk))
                      ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by simp
          thus ?thesis by blast
        qed
      moreover have br2: ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ ⟧config ⟹ ∃Γk Ψk Φk k.
                       ((Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ) ↪kk, Suc n ⊨ Ψk ▹ Φk))
                      ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
        proof -
          assume h:‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ ⟧config
          hence ‹∃Γk Ψk Φk k.
                    ((((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ)
                        ↪kk, Suc n ⊨ Ψk ▹ Φk))
                    ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
            using Cons.hyps by blast
          from this obtain Γk Ψk Φk k where
               ‹((((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ) ↪kk, Suc n ⊨ Ψk ▹ Φk))›
              and *:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
          moreover have ‹(Γ, n ⊨((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ)
                          ↪(((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ)›
            by (simp add: sporadic_on_tvar_e2 elims_part)
          ultimately have ‹((Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ)
                        ↪Suc kk, Suc n ⊨ Ψk ▹ Φk))›
            using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast
          with * have ‹((Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ)
                        ↪Suc kk, Suc n ⊨ Ψk ▹ Φk))
                      ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by simp
          thus ?thesis by blast
        qed
        ultimately show ?case
          using branches SporadicOnTvar.prems(2) by blast
  next
    case (TagRelation C1 C2 R)
      have branches: ‹⟦ Γ, n ⊨ ((time-relation ⌊C1, C2⌋ ∈ R) # Ψ) ▹ Φ ⟧config
          = ⟦ ((⌊τvar(C1, n), τvar(C2, n)⌋ ∈ R) # Γ), n
              ⊨ Ψ ▹ ((time-relation ⌊C1, C2⌋ ∈ R) # Φ) ⟧config
        using configuration_interp_stepwise_tagrel_cases by simp
      thus ?case
      proof -
        have ‹∃Γk Ψk Φk k.
            ((((⌊τvar(C1, n), τvar(C2, n)⌋ ∈ R) # Γ), n
                ⊨ Ψ ▹ ((time-relation ⌊C1, C2⌋ ∈ R) # Φ))
              ↪kk, Suc n ⊨ Ψk ▹ Φk)) ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using TagRelation.prems by simp

        from this obtain Γk Ψk Φk k
          where fp:‹((((⌊τvar(C1, n), τvar(C2, n)⌋ ∈ R) # Γ), n
                        ⊨ Ψ ▹ ((time-relation ⌊C1, C2⌋ ∈ R) # Φ))
                    ↪kk, Suc n ⊨ Ψk ▹ Φk))›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have pc:‹(Γ, n ⊨ ((time-relation ⌊C1, C2⌋ ∈ R) # Ψ) ▹ Φ)
            ↪ (((⌊τvar (C1, n), τvar (C2, n)⌋ ∈ R) # Γ), n
                  ⊨ Ψ ▹ ((time-relation ⌊C1, C2⌋ ∈ R) # Φ))›
          by (simp add: elims_part tagrel_e)
        hence ‹(Γ, n ⊨ (time-relation ⌊C1, C2⌋ ∈ R) # Ψ ▹ Φ)
                ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
  next
    case (Implies C1 C2)
      have branches: ‹⟦ Γ, n ⊨ ((C1 implies C2) # Ψ) ▹ Φ ⟧config
          = ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config
          ∪ ⟦ ((C1 ⇑ n) # (C2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config
        using configuration_interp_stepwise_implies_cases by simp
      moreover have br1: ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config
                ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊨ ((C1 implies C2) # Ψ) ▹ Φ)
                                    ↪kk, Suc n ⊨ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
      proof -
        assume h1: ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config
        then have ‹∃Γk Ψk Φk k.
                    ((((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ))
                        ↪kk, Suc n ⊨ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using h1 Implies.prems by simp
        from this obtain Γk Ψk Φk k where
          fp:‹((((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ))
            ↪kk, Suc n ⊨ Ψk ▹ Φk))›
          and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have pc:‹(Γ, n ⊨ (C1 implies C2) # Ψ ▹ Φ)
                  ↪ (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ))›
          by (simp add: elims_part implies_e1)
        hence ‹(Γ, n ⊨ (C1 implies C2) # Ψ ▹ Φ) ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2: ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 ⇑ n) # Γ), n
                                ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config
                            ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊨ ((C1 implies C2) # Ψ) ▹ Φ)
                                              ↪kk, Suc n ⊨ Ψk ▹ Φk))
                                  ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
      proof -
        assume h2: ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 ⇑ n) # Γ), n
                          ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config
        then have ‹∃Γk Ψk Φk k. (
                        (((C1 ⇑ n) # (C2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ))
                          ↪kk, Suc n ⊨ Ψk ▹ Φk)
                    ) ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using h2 Implies.prems by simp
        from this obtain Γk Ψk Φk k where
            fp:‹(((C1 ⇑ n) # (C2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ))
                ↪kk, Suc n ⊨ Ψk ▹ Φk)›
        and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have ‹(Γ, n ⊨ ((C1 implies C2) # Ψ) ▹ Φ)
              ↪ (((C1 ⇑ n) # (C2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ))›
          by (simp add: elims_part implies_e2)
        hence ‹(Γ, n ⊨ ((C1 implies C2) # Ψ) ▹ Φ) ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case using Implies.prems(2) by blast
  next
    case (ImpliesNot C1 C2)
      have branches: ‹⟦ Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ ⟧config
          = ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config
          ∪ ⟦ ((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config
        using configuration_interp_stepwise_implies_not_cases by simp
      moreover have br1: ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n
                            ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config
                ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ)
                                    ↪kk, Suc n ⊨ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
      proof -
        assume h1: ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config
        then have ‹∃Γk Ψk Φk k.
                    ((((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ))
                      ↪kk, Suc n ⊨ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using h1 ImpliesNot.prems by simp
        from this obtain Γk Ψk Φk k where
          fp:‹((((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ))
                ↪kk, Suc n ⊨ Ψk ▹ Φk))›
          and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have pc:‹(Γ, n ⊨ (C1 implies not C2) # Ψ ▹ Φ)
                  ↪ (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ))›
          by (simp add: elims_part implies_not_e1)
        hence ‹(Γ, n ⊨ (C1 implies not C2) # Ψ ▹ Φ) ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2: ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n
                            ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config
                            ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ)
                                              ↪kk, Suc n ⊨ Ψk ▹ Φk))
                                  ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
      proof -
        assume h2: ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n
                          ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config
        then have ‹∃Γk Ψk Φk k. (
                     (((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n
                       ⊨ Ψ ▹ ((C1 implies not C2) # Φ)) ↪kk, Suc n ⊨ Ψk ▹ Φk)
                    ) ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using h2 ImpliesNot.prems by simp
        from this obtain Γk Ψk Φk k where
            fp:‹(((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ))
                ↪kk, Suc n ⊨ Ψk ▹ Φk)›
        and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have ‹(Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ)
              ↪ (((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ))›
          by (simp add: elims_part implies_not_e2)
        hence ‹(Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ)
                ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case  using ImpliesNot.prems(2) by blast
  next
    case (TimeDelayedBy C1 δτ C2 C3)
      have branches:
        ‹⟦ Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ ⟧config
          = ⟦ ((C1 ¬⇑ n) # Γ), n
              ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config
          ∪ ⟦ ((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
              ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config
        using configuration_interp_stepwise_timedelayed_cases by simp
      moreover have br1:
        ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n
              ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config
          ⟹ ∃Γk Ψk Φk k.
            ((Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)
                ↪kk, Suc n ⊨ Ψk ▹ Φk))
            ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
      proof -
        assume h1: ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n
                         ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config
        then have ‹∃Γk Ψk Φk k.
          ((((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))
            ↪kk, Suc n ⊨ Ψk ▹ Φk))
          ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using h1 TimeDelayedBy.prems by simp
        from this obtain Γk Ψk Φk k
          where fp:‹(((C1 ¬⇑ n) # Γ), n
                      ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))
                    ↪kk, Suc n ⊨ Ψk ▹ Φk)›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have ‹(Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)
              ↪ (((C1 ¬⇑ n) # Γ), n
                    ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))›
          by (simp add: elims_part timedelayed_e1)
        hence ‹(Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)
                ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2:
        ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
              ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config
          ⟹ ∃Γk Ψk Φk k.
              ((Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)
                ↪kk, Suc n ⊨ Ψk ▹ Φk))
              ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
      proof -
        assume h2: ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
                    ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config
        then have ‹∃Γk Ψk Φk k. ((((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
                                 ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))
                                 ↪kk, Suc n ⊨ Ψk ▹ Φk))
                                ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using h2 TimeDelayedBy.prems by simp
        from this obtain Γk Ψk Φk k
          where fp:‹(((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
                         ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))
                       ↪kk, Suc n ⊨ Ψk ▹ Φk)›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have ‹(Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)
              ↪ (((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
                  ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))›
          by (simp add: elims_part timedelayed_e2)
        with fp relpowp_Suc_I2 have
          ‹(Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)
            ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case using TimeDelayedBy.prems(2) by blast
  next
    case (RelaxedTimeDelayed C1 δτ C2 C3)
      have branches:
        ‹⟦ Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ ⟧config
          = ⟦ ((C1 ¬⇑ n) # Γ), n
              ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
          ∪ ⟦ ((C1 ⇑ n) # Γ), n
              ⊨ (C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2) # Ψ
              ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
        using configuration_interp_stepwise_timedelayed_tvar_cases by simp
      have more_branches:
                ‹⟦ ((C1 ⇑ n) # Γ), n ⊨ ((C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2) # Ψ)
                                     ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
                = ⟦ ((C1 ⇑ n) # Γ), n ⊨ Ψ
                                      ▹ ((C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2)
                                       # (C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
                  ∪ ⟦ ((C3 ⇑ n) # (C2 ⇓ n @♯ ⦇τvar(C2, n) ⊕ δτ⦈) # (C1 ⇑ n) # Γ), n
                                 ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
            using configuration_interp_stepwise_sporadicon_tvar_cases by blast
      moreover have br1:
        ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n
              ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
          ⟹ ∃Γk Ψk Φk k.
            ((Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
                ↪kk, Suc n ⊨ Ψk ▹ Φk))
            ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
      proof -
        assume h1: ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n
                         ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
        then have ‹∃Γk Ψk Φk k.
          ((((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))
            ↪kk, Suc n ⊨ Ψk ▹ Φk))
          ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using h1 RelaxedTimeDelayed.prems by simp
        from this obtain Γk Ψk Φk k
          where fp:‹(((C1 ¬⇑ n) # Γ), n
                      ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))
                    ↪kk, Suc n ⊨ Ψk ▹ Φk)›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have ‹(Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
              ↪ (((C1 ¬⇑ n) # Γ), n
                    ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))›
          by (simp add: elims_part timedelayed_tvar_e1)
        hence ‹(Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
                ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2:
        ‹ρ ∈ ⟦ ((C1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2)
                                       # (C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
          ⟹ ∃Γk Ψk Φk k.
              ((Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
              ↪kk, Suc n ⊨ Ψk ▹ Φk)) ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
        proof -
          assume h2: ‹ρ ∈ ⟦ ((C1 ⇑ n) # Γ), n ⊨ Ψ
                                           ▹ ((C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2)
                                           # (C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
          then have ‹∃Γk Ψk Φk k. ((((C1 ⇑ n) # Γ), n ⊨ Ψ
                                                   ▹ ((C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2)
                                                   # (C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))
                              ↪kk, Suc n ⊨ Ψk ▹ Φk)) ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
            using h2 RelaxedTimeDelayed.prems by simp
          from this obtain Γk Ψk Φk k where ‹((((C1 ⇑ n) # Γ), n ⊨ Ψ
                                                   ▹ ((C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2)
                                                   # (C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))
                              ↪kk, Suc n ⊨ Ψk ▹ Φk))› and *:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
            by blast
          moreover have ‹( ((C1 ⇑ n) # Γ), n
                            ⊨ (C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2) # Ψ
                            ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))
                        ↪ ( ((C1 ⇑ n) # Γ), n
                            ⊨ Ψ
                            ▹ ((C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2)
                            # (C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))›
            by (simp add: elims_part sporadic_on_tvar_e1)
          ultimately have ‹( ((C1 ⇑ n) # Γ), n
                            ⊨ (C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2) # Ψ
                            ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))
                         ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
            using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast 
          moreover have ‹(Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
                      ↪ ( ((C1 ⇑ n) # Γ), n
                            ⊨ (C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2) # Ψ
                            ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))›
            by (simp add: elims_part timedelayed_tvar_e2)
          ultimately have ‹(Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
                      ↪Suc(Suc k)k, Suc n ⊨ Ψk ▹ Φk)›
            using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast
          with * show ?thesis by blast
        qed
      moreover have br2':
        ‹ρ ∈ ⟦ ((C3 ⇑ n) # (C2 ⇓ n @♯ ⦇τvar(C2, n) ⊕ δτ⦈) # (C1 ⇑ n) # Γ), n
              ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
          ⟹ ∃Γk Ψk Φk k.
           ((Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
              ↪kk, Suc n ⊨ Ψk ▹ Φk)) ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
        proof -
          assume h2: ‹ρ ∈ ⟦ ((C3 ⇑ n) # (C2 ⇓ n @♯ ⦇τvar(C2, n) ⊕ δτ⦈) # (C1 ⇑ n) # Γ), n
                                ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
          then have ‹∃Γk Ψk Φk k.
              ((((C3 ⇑ n) # (C2 ⇓ n @♯ ⦇τvar(C2, n) ⊕ δτ⦈) # (C1 ⇑ n) # Γ), n
                ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ)) ↪kk, Suc n ⊨ Ψk ▹ Φk))
                ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
            using h2 RelaxedTimeDelayed.prems by simp
          from this obtain Γk Ψk Φk k where ‹
              ( (((C3 ⇑ n) # (C2 ⇓ n @♯ ⦇τvar(C2, n) ⊕ δτ⦈) # (C1 ⇑ n) # Γ), n
                   ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))
               ↪kk, Suc n ⊨ Ψk ▹ Φk))›
           and *:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
          moreover have ‹(  ((C1 ⇑ n) # Γ), n ⊨ (C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2) # Ψ
                  ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))
                        ↪ (((C3 ⇑ n) # (C2 ⇓ n @♯ ⦇τvar(C2, n) ⊕ δτ⦈) # (C1 ⇑ n) # Γ), n
                   ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))›
            by (simp add: elims_part sporadic_on_tvar_e2)
          ultimately have ‹( ((C1 ⇑ n) # Γ), n
                            ⊨ (C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2) # Ψ
                            ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))
                         ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
            using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast
          moreover have ‹(Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
                      ↪ ( ((C1 ⇑ n) # Γ), n
                            ⊨ (C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2) # Ψ
                            ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))›
            by (simp add: elims_part timedelayed_tvar_e2)
          ultimately have ‹(Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
                      ↪Suc(Suc k)k, Suc n ⊨ Ψk ▹ Φk)›
            using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast
          with * show ?thesis by blast
        qed
        ultimately show ?case using RelaxedTimeDelayed.prems(2) branches more_branches by blast
  next
    case (WeaklyPrecedes C1 C2)
      have ‹⟦ Γ, n ⊨ ((C1 weakly precedes C2) # Ψ) ▹ Φ ⟧config =
        ⟦ ((⌈# C2 n, # C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
            ⊨ Ψ ▹ ((C1 weakly precedes C2) # Φ) ⟧config
        using configuration_interp_stepwise_weakly_precedes_cases by simp
      moreover have ‹ρ ∈ ⟦ ((⌈# C2 n, # C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                            ⊨ Ψ ▹ ((C1 weakly precedes C2) # Φ) ⟧config
            ⟹ (∃Γk Ψk Φk k. ((Γ, n ⊨ ((C1 weakly precedes C2) # Ψ) ▹ Φ)
                                  ↪kk, Suc n ⊨ Ψk ▹ Φk))
                ∧ (ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig))›
      proof -
        assume ‹ρ ∈ ⟦ ((⌈# C2 n, # C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                        ⊨ Ψ ▹ ((C1 weakly precedes C2) # Φ) ⟧config
        hence ‹∃Γk Ψk Φk k. ((((⌈# C2 n, # C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊨ Ψ ▹ ((C1 weakly precedes C2) # Φ))
                             ↪kk, Suc n ⊨ Ψk ▹ Φk))
                          ∧ (ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig)›
          using  WeaklyPrecedes.prems by simp
        from this obtain Γk Ψk Φk k
          where fp:‹(((⌈# C2 n, # C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊨ Ψ ▹ ((C1 weakly precedes C2) # Φ))
                             ↪kk, Suc n ⊨ Ψk ▹ Φk)›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have ‹(Γ, n ⊨ ((C1 weakly precedes C2) # Ψ) ▹ Φ)
                ↪ (((⌈# C2 n, # C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
              ⊨ Ψ ▹ ((C1 weakly precedes C2) # Φ))›
          by (simp add: elims_part weakly_precedes_e)
        with fp relpowp_Suc_I2 have ‹(Γ, n ⊨ ((C1 weakly precedes C2) # Ψ) ▹ Φ)
                                      ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case using WeaklyPrecedes.prems(2) by blast
  next
    case (StrictlyPrecedes C1 C2)
      have ‹⟦ Γ, n ⊨ ((C1 strictly precedes C2) # Ψ) ▹ Φ ⟧config =
        ⟦ ((⌈# C2 n, #< C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
          ⊨ Ψ ▹ ((C1 strictly precedes C2) # Φ) ⟧config
        using configuration_interp_stepwise_strictly_precedes_cases by simp
      moreover have ‹ρ ∈ ⟦ ((⌈# C2 n, #< C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                            ⊨ Ψ ▹ ((C1 strictly precedes C2) # Φ) ⟧config
            ⟹ (∃Γk Ψk Φk k. ((Γ, n ⊨ ((C1 strictly precedes C2) # Ψ) ▹ Φ)
                                  ↪kk, Suc n ⊨ Ψk ▹ Φk))
                ∧ (ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig))›
      proof -
        assume ‹ρ ∈ ⟦ ((⌈# C2 n, #< C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                        ⊨ Ψ ▹ ((C1 strictly precedes C2) # Φ) ⟧config
        hence ‹∃Γk Ψk Φk k. ((((⌈# C2 n, #< C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊨ Ψ ▹ ((C1 strictly precedes C2) # Φ))
                             ↪kk, Suc n ⊨ Ψk ▹ Φk))
                            ∧ (ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig)›
          using  StrictlyPrecedes.prems by simp
        from this obtain Γk Ψk Φk k
          where fp:‹(((⌈# C2 n, #< C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊨ Ψ ▹ ((C1 strictly precedes C2) # Φ))
                             ↪kk, Suc n ⊨ Ψk ▹ Φk)›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have ‹(Γ, n ⊨ ((C1 strictly precedes C2) # Ψ) ▹ Φ)
                ↪ (((⌈# C2 n, #< C1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
              ⊨ Ψ ▹ ((C1 strictly precedes C2) # Φ))›
          by (simp add: elims_part strictly_precedes_e)
        with fp relpowp_Suc_I2 have ‹(Γ, n ⊨ ((C1 strictly precedes C2) # Ψ) ▹ Φ)
                                      ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case using StrictlyPrecedes.prems(2) by blast
  next
    case (Kills C1 C2)
      have branches: ‹⟦ Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ ⟧config
          = ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) ⟧config
          ∪ ⟦ ((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) ⟧config
        using configuration_interp_stepwise_kills_cases by simp
      moreover have br1: ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) ⟧config
                ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ)
                                    ↪kk, Suc n ⊨ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
      proof -
        assume h1: ‹ρ ∈ ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) ⟧config
        then have ‹∃Γk Ψk Φk k.
                    ((((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))
                    ↪kk, Suc n ⊨ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using h1 Kills.prems by simp
        from this obtain Γk Ψk Φk k where
          fp:‹((((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))
                ↪kk, Suc n ⊨ Ψk ▹ Φk))›
          and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have pc:‹(Γ, n ⊨ (C1 kills C2) # Ψ ▹ Φ)
                  ↪ (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))›
          by (simp add: elims_part kills_e1)
        hence ‹(Γ, n ⊨ (C1 kills C2) # Ψ ▹ Φ) ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2:
        ‹ρ ∈ ⟦ ((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) ⟧config
          ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ)
                                ↪kk, Suc n ⊨ Ψk ▹ Φk))
                          ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
      proof -
        assume h2: ‹ρ ∈ ⟦((C1 ⇑ n)#(C2 ¬⇑ ≥ n)#Γ), n ⊨ Ψ ▹ ((C1 kills C2)#Φ)⟧config
        then have ‹∃Γk Ψk Φk k. (
                    (((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))
                      ↪kk, Suc n ⊨ Ψk ▹ Φk)
                    ) ∧ ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig
          using h2 Kills.prems by simp
        from this obtain Γk Ψk Φk k where
            fp:‹(((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))
                ↪kk, Suc n ⊨ Ψk ▹ Φk)›
        and rc:‹ρ ∈ ⟦ Γk, Suc n ⊨ Ψk ▹ Φkconfig by blast
        have ‹(Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ)
              ↪ (((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))›
          by (simp add: elims_part kills_e2)
        hence ‹(Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ) ↪Suc kk, Suc n ⊨ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case using Kills.prems(2) by blast
  qed
qed

lemma instant_index_increase_generalized:
  assumes ‹n < nk
  assumes ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ Φ ⟧config
  shows   ‹∃Γk Ψk Φk k. ((Γ, n ⊨ Ψ ▹ Φ) ↪kk, nk ⊨ Ψk ▹ Φk))
                         ∧ ρ ∈ ⟦ Γk, nk ⊨ Ψk ▹ Φkconfig
proof -
  obtain δk where diff: ‹nk = δk + Suc n›
    using add.commute assms(1) less_iff_Suc_add by auto
  show ?thesis
    proof (subst diff, subst diff, insert assms(2), induct δk)
      case 0  thus ?case
        using instant_index_increase assms(2) by simp
    next
      case (Suc δk)
        have f0: ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ Φ ⟧config ⟹ ∃Γk Ψk Φk k.
                  ((Γ, n ⊨ Ψ ▹ Φ) ↪kk, δk + Suc n ⊨ Ψk ▹ Φk))
                ∧ ρ ∈ ⟦ Γk, δk + Suc n ⊨ Ψk ▹ Φkconfig
          using Suc.hyps by blast
        obtain Γk Ψk Φk k
          where cont: ‹((Γ, n ⊨ Ψ ▹ Φ) ↪kk, δk + Suc n ⊨ Ψk ▹ Φk))
                      ∧ ρ ∈ ⟦ Γk, δk + Suc n ⊨ Ψk ▹ Φkconfig
          using f0 assms(1) Suc.prems by blast
        then have fcontinue: ‹∃Γk' Ψk' Φk' k'. ((Γk, δk + Suc n ⊨ Ψk ▹ Φk)
                                       ↪k'k', Suc (δk + Suc n) ⊨ Ψk' ▹ Φk'))
                                   ∧ ρ ∈ ⟦ Γk', Suc (δk + Suc n) ⊨ Ψk' ▹ Φk' ⟧config
          using f0 cont instant_index_increase by blast
        obtain Γk' Ψk' Φk' k'
          where cont2: ‹((Γk, δk + Suc n ⊨ Ψk ▹ Φk)
                        ↪k'k', Suc (δk + Suc n) ⊨ Ψk' ▹ Φk'))
                      ∧ ρ ∈ ⟦ Γk', Suc (δk + Suc n) ⊨ Ψk' ▹ Φk' ⟧config
          using Suc.prems using fcontinue cont by blast
        have trans: ‹(Γ, n ⊨ Ψ ▹ Φ) ↪k + k'k', Suc (δk + Suc n) ⊨ Ψk' ▹ Φk')›
          using operational_semantics_trans_generalized cont cont2 by blast
        moreover have suc_assoc: ‹Suc δk + Suc n = Suc (δk + Suc n)› by arith
        ultimately show ?case
          proof (subst suc_assoc)
            show ‹∃Γk Ψk Φk k.
                   ((Γ, n ⊨ Ψ ▹ Φ) ↪kk, Suc (δk + Suc n) ⊨ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc δk + Suc n ⊨ Ψk ▹ Φkconfig
            using cont2 local.trans by auto
          qed
    qed
qed

text‹
  Any run that belongs to a specification @{term ‹Ψ›} has a corresponding 
  configuration that develops it up to the @{term ‹n›}\textsuperscript{th} instant.
›
theorem progress:
  assumes ‹ρ ∈ ⟦⟦ Ψ ⟧⟧TESL
    shows ‹∃k Γk Ψk Φk. (([], 0 ⊨ Ψ ▹ [])  ↪kk, n ⊨ Ψk ▹ Φk))
                         ∧ ρ ∈ ⟦ Γk, n ⊨ Ψk ▹ Φkconfig
proof -
  have 1:‹∃Γk Ψk Φk k. (([], 0 ⊨ Ψ ▹ []) ↪kk, 0 ⊨ Ψk ▹ Φk))
                      ∧ ρ ∈ ⟦ Γk, 0 ⊨ Ψk ▹ Φkconfig
    using assms relpowp_0_I solve_start by fastforce
  show ?thesis
  proof (cases ‹n = 0›)
    case True
      thus ?thesis using assms relpowp_0_I solve_start by fastforce
  next
    case False hence pos:‹n > 0› by simp
      from assms solve_start have ‹ρ ∈ ⟦ [], 0 ⊨ Ψ ▹ [] ⟧config by blast
      from instant_index_increase_generalized[OF pos this] show ?thesis by blast
  qed
qed

section ‹Local termination›
text ‹
  Here, we prove that the computation of an instant in a run always terminates.
  Since this computation terminates when the list of constraints for the present
  instant becomes empty, we introduce a measure for this formula.
›
primrec measure_interpretation :: ‹'τ::linordered_field TESL_formula ⇒ nat› (‹μ›)
where
  ‹μ [] = (0::nat)›
| ‹μ (φ # Φ) = (case φ of
                      _ sporadic _ on _ ⇒ 1 + μ Φ
                    | _ sporadic♯ _ on _ ⇒ 1 + μ Φ
                    | _                 ⇒ 2 + μ Φ)›

fun measure_interpretation_config :: ‹'τ::linordered_field config ⇒ nat› (‹μconfig)
where
  ‹μconfig (Γ, n ⊨ Ψ ▹ Φ) = μ Ψ›

text ‹
  We then show that the elimination rules make this measure decrease.
›
lemma elimation_rules_strictly_decreasing:
  assumes ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1)  ↪e2, n2 ⊨ Ψ2 ▹ Φ2)›
    shows ‹μ Ψ1 > μ Ψ2
using assms by (auto elim: operational_semantics_elim.cases)

lemma elimation_rules_strictly_decreasing_meas:
  assumes ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1)  ↪e2, n2 ⊨ Ψ2 ▹ Φ2)›
    shows ‹(Ψ2, Ψ1) ∈ measure μ›
using assms by (auto elim: operational_semantics_elim.cases)

lemma elimation_rules_strictly_decreasing_meas':
  assumes ‹𝒮1e  𝒮2
  shows ‹(𝒮2, 𝒮1) ∈ measure μconfig
proof -
  from assms obtain Γ1 n1 Ψ1 Φ1 where p1:‹𝒮1 = (Γ1, n1 ⊨ Ψ1 ▹ Φ1)›
    using measure_interpretation_config.cases by blast
  from assms obtain Γ2 n2 Ψ2 Φ2 where p2:‹𝒮2 = (Γ2, n2 ⊨ Ψ2 ▹ Φ2)›
    using measure_interpretation_config.cases by blast
  from elimation_rules_strictly_decreasing_meas assms p1 p2
    have ‹(Ψ2, Ψ1) ∈ measure μ› by blast
  hence ‹μ Ψ2 < μ Ψ1 by simp
  hence ‹μconfig2, n2 ⊨ Ψ2 ▹ Φ2) < μconfig1, n1 ⊨ Ψ1 ▹ Φ1)› by simp
  with p1 p2 show ?thesis by simp
qed

text ‹
  Therefore, the relation made up of elimination rules is well-founded and the
  computation of an instant terminates.
›
theorem instant_computation_termination:
  ‹wfP (λ(𝒮1::'a::linordered_field config) 𝒮2. (𝒮1e  𝒮2))›
proof (simp add: wfP_def)
  show ‹wf {((𝒮1::'a::linordered_field config), 𝒮2). 𝒮1e 𝒮2}›
  proof (rule wf_subset)
    have ‹measure μconfig = {(𝒮2, (𝒮1::'a::linordered_field config)).
                               μconfig 𝒮2 < μconfig 𝒮1}›
      by (simp add: inv_image_def less_eq measure_def)
    thus ‹{((𝒮1::'a::linordered_field config), 𝒮2). 𝒮1e 𝒮2} ⊆ (measure μconfig)›
      using elimation_rules_strictly_decreasing_meas'
            operational_semantics_elim_inv_def by blast
  next
    show ‹wf (measure measure_interpretation_config)› by simp
  qed
qed


end