Theory Hygge_Theory

chapter‹Main Theorems›

theory Hygge_Theory
imports
  Corecursive_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 ‹⟦⟦ Ψ ⟧⟧⇩T⇩E⇩S⇩L = ⟦ [], 0 ⊢ Ψ ▹ [] ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
  proof -
    have ‹⟦⟦ Ψ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Ψ ⟧⟧⇩T⇩E⇩S⇩L⇗≥ 0⇖›
    by (simp add: TESL_interpretation_stepwise_zero')
    moreover have ‹⟦ [], 0 ⊢ Ψ ▹ [] ⟧⇩c⇩o⇩n⇩f⇩i⇩g =
                      ⟦⟦ [] ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Ψ ⟧⟧⇩T⇩E⇩S⇩L⇗≥ 0⇖ ∩ ⟦⟦ [] ⟧⟧⇩T⇩E⇩S⇩L⇗≥ 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, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)  ↪  (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)›
  shows ‹⟦⟦ Γ⇩1 ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Ψ⇩1 ⟧⟧⇩T⇩E⇩S⇩L⇗≥ n⇩1⇖ ∩ ⟦⟦ Φ⇩1 ⟧⟧⇩T⇩E⇩S⇩L⇗≥ Suc n⇩1⇖
          ⊇  ⟦⟦ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Ψ⇩2 ⟧⟧⇩T⇩E⇩S⇩L⇗≥ n⇩2⇖ ∩ ⟦⟦ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L⇗≥ Suc n⇩2⇖› (is ?P)
proof -
  from assms consider
    (a) ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)  ↪⇩i  (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)›
  | (b) ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)  ↪⇩e  (Γ⇩2, n⇩2 ⊢ Ψ⇩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 K⇩1 τ K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ (K⇩1 sporadic τ on K⇩2) # Ψ ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (Γ, n ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_sporadicon_cases
                    HeronConf_interpretation.simps by blast
    next
      fix  Γ n K⇩1 τ K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ (K⇩1 sporadic τ on K⇩2) # Ψ ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)›
      thus ?P using HeronConf_interp_stepwise_sporadicon_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 K⇩2 R Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ (time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Ψ ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (((⌊τ⇩v⇩a⇩r (K⇩1, n), τ⇩v⇩a⇩r (K⇩2, n)⌋ ∈ R) # Γ), n
                                      ⊢ Ψ ▹ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Φ))›
      thus ?P using HeronConf_interp_stepwise_tagrel_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ (K⇩1 implies K⇩2) # Ψ ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_implies_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ ((K⇩1 implies K⇩2) # Ψ) ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (((K⇩1 ⇑ n) # (K⇩2 ⇑ n) # Γ), n
                                   ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_implies_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_implies_not_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (((K⇩1 ⇑ n) # (K⇩2 ¬⇑ n) # Γ), n
                                   ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_implies_not_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 δτ K⇩2 K⇩3 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) =
                (Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) =
            (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))›
      thus ?P using HeronConf_interp_stepwise_timedelayed_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 δτ K⇩2 K⇩3 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) =
               (Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)
            = (((K⇩1 ⇑ n) # (K⇩2 @ n ⊕ δτ ⇒ K⇩3) # Γ), n
                ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))›
      thus ?P using HeronConf_interp_stepwise_timedelayed_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ ((K⇩1 weakly precedes K⇩2) # Ψ) ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (((⌈#⇧≤ K⇩2 n, #⇧≤ K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K⇩1 weakly precedes K⇩2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_weakly_precedes_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ ((K⇩1 strictly precedes K⇩2) # Ψ) ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (((⌈#⇧≤ K⇩2 n, #⇧< K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K⇩1 strictly precedes K⇩2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_strictly_precedes_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) = (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_kills_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K⇩1 K⇩2 Ψ Φ
      assume ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ)›
      and ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) =
            (((K⇩1 ⇑ n) # (K⇩2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_kills_cases
                    HeronConf_interpretation.simps by blast
    qed
  qed
qed

inductive_cases step_elim:‹𝒮⇩1 ↪ 𝒮⇩2›

lemma sound_reduction':
  assumes ‹𝒮⇩1 ↪ 𝒮⇩2›
  shows ‹⟦ 𝒮⇩1 ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊇ ⟦ 𝒮⇩2 ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
proof -
  have ‹∀s⇩1 s⇩2. (⟦ s⇩2 ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊆ ⟦ s⇩1 ⟧⇩c⇩o⇩n⇩f⇩i⇩g) ∨ ¬(s⇩1 ↪ s⇩2)›
    using sound_reduction by fastforce
  thus ?thesis using assms by blast
qed

lemma sound_reduction_generalized:
  assumes ‹𝒮⇩1 ↪⇗k⇖ 𝒮⇩2›
    shows ‹⟦ 𝒮⇩1 ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊇ ⟦ 𝒮⇩2 ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
proof -
  from assms show ?thesis
  proof (induction k arbitrary: 𝒮⇩2)
    case 0
      hence *: ‹𝒮⇩1 ↪⇗0⇖ 𝒮⇩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: ‹𝒮⇩1 ↪⇗Suc k⇖ 𝒮⇩2›
        assume hi: ‹⋀𝒮⇩2. 𝒮⇩1 ↪⇗k⇖ 𝒮⇩2 ⟹ ⟦ 𝒮⇩2 ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊆ ⟦ 𝒮⇩1 ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        obtain 𝒮⇩n where red_decomp: ‹(𝒮⇩1 ↪⇗k⇖ 𝒮⇩n) ∧ (𝒮⇩n ↪ 𝒮⇩2)› using ff by auto
        hence ‹⟦ 𝒮⇩1 ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊇ ⟦ 𝒮⇩n ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using hi by simp
        also have ‹⟦ 𝒮⇩n ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊇ ⟦ 𝒮⇩2 ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by (simp add: red_decomp sound_reduction')
        ultimately show ‹⟦ 𝒮⇩1 ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊇ ⟦ 𝒮⇩2 ⟧⇩c⇩o⇩n⇩f⇩i⇩g› 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 ‹⟦⟦ Ψ ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦ 𝒮 ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
  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 ⊢ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊆ (⋃X∈𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ Ψ ▹ Φ). ⟦ X ⟧⇩c⇩o⇩n⇩f⇩i⇩g)›
  proof (induct Ψ)
    case Nil
    show ?case
      using HeronConf_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 HeronConf_interp_stepwise_sporadicon_cases
                                      [of ‹Γ› ‹n› ‹K1› ‹τ› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_sporadicon[of ‹Γ› ‹n› ‹Ψ› ‹K1› ‹τ› ‹K2› ‹Φ›] by blast
      next
        case (TagRelation K⇩1 K⇩2 R) thus ?thesis
          using HeronConf_interp_stepwise_tagrel_cases
                                  [of ‹Γ› ‹n› ‹K⇩1› ‹K⇩2› ‹R› ‹Ψ› ‹Φ›]
                Cnext_solve_tagrel[of ‹K⇩1› ‹n› ‹K⇩2› ‹R› ‹Γ› ‹Ψ› ‹Φ›] by blast
      next
        case (Implies K1 K2) thus ?thesis
          using HeronConf_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 HeronConf_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 HeronConf_interp_stepwise_timedelayed_cases
                          [of ‹Γ› ‹n› ‹Kmast› ‹τ› ‹Kmeas› ‹Kslave› ‹Ψ› ‹Φ›]
                Cnext_solve_timedelayed
                          [of ‹Kmast› ‹n› ‹Γ› ‹Ψ› ‹τ› ‹Kmeas› ‹Kslave› ‹Φ›] by blast
      next
        case (WeaklyPrecedes K1 K2) thus ?thesis
          using HeronConf_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 HeronConf_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 HeronConf_interp_stepwise_kills_cases[of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_kills[of ‹K1› ‹n› ‹Γ› ‹Ψ› ‹K2› ‹Φ›] by blast
      qed
  qed

lemma complete_direct_successors':
  shows ‹⟦ 𝒮 ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊆ (⋃X∈𝒞⇩n⇩e⇩x⇩t 𝒮. ⟦ X ⟧⇩c⇩o⇩n⇩f⇩i⇩g)›
proof -
  from HeronConf_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 ‹ρ ∈ ⟦ 𝒮⇩1 ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
  shows ‹∃𝒮⇩2. (𝒮⇩1 ↪ 𝒮⇩2) ∧ (ρ ∈ ⟦ 𝒮⇩2 ⟧⇩c⇩o⇩n⇩f⇩i⇩g)›
proof -
  from assms complete_direct_successors' have ‹ρ ∈ (⋃X∈𝒞⇩n⇩e⇩x⇩t 𝒮⇩1. ⟦ X ⟧⇩c⇩o⇩n⇩f⇩i⇩g)› by blast
  hence ‹∃s∈𝒞⇩n⇩e⇩x⇩t 𝒮⇩1. ρ ∈ ⟦ s ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by simp
  thus ?thesis by blast
qed

lemma branch_existence':
  assumes ‹ρ ∈ ⟦ 𝒮⇩1 ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
  shows ‹∃𝒮⇩2. (𝒮⇩1 ↪⇗k⇖ 𝒮⇩2) ∧ (ρ ∈ ⟦ 𝒮⇩2 ⟧⇩c⇩o⇩n⇩f⇩i⇩g)›
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 ‹ρ ∈ ⟦⟦ Ψ ⟧⟧⇩T⇩E⇩S⇩L›
  shows ‹∃𝒮. (([], 0 ⊢ Ψ ▹ [])  ↪⇗k⇖  𝒮)
           ∧ ρ ∈ ⟦ 𝒮 ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
  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 ⊢ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
  shows   ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ Ψ ▹ Φ)  ↪⇗k⇖  (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                         ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
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 ⊢ [] ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ Γ, Suc n ⊢ Φ ▹ [] ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        by auto
      moreover have ‹ρ ∈ ⟦ Γ, Suc n ⊢ Φ ▹ [] ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        using assms Nil.prems calculation(2) by blast
      ultimately show ?thesis by blast
    qed
next
  case (Cons ψ Ψ)
    then show ?case
    proof (induct ψ)
      case (SporadicOn K⇩1 τ K⇩2)
        have branches: ‹⟦ Γ, n ⊢ ((K⇩1 sporadic τ on K⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g
                      = ⟦ Γ, n ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
                      ∪ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using HeronConf_interp_stepwise_sporadicon_cases by simp
        have br1: ‹ρ ∈ ⟦ Γ, n ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
                    ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k.
                      ((Γ, n ⊢ ((K⇩1 sporadic τ on K⇩2) # Ψ) ▹ Φ)
                          ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                      ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        proof -
          assume h1: ‹ρ ∈ ⟦ Γ, n ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ))
                                      ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                                 ∧ (ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g)›
            using h1 SporadicOn.prems by simp
          from this obtain Γ⇩k Ψ⇩k Φ⇩k k where
              fp:‹((Γ, n ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ))
                    ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
          have
            ‹(Γ, n ⊢ ((K⇩1 sporadic τ on K⇩2) # Ψ) ▹ Φ)
              ↪ (Γ, n ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ))›
            by (simp add: elims_part sporadic_on_e1)
          with fp relpowp_Suc_I2 have
            ‹((Γ, n ⊢ ((K⇩1 sporadic τ on K⇩2) # Ψ) ▹ Φ)
              ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))› by auto
          thus ?thesis using fp by blast
        qed
        have br2: ‹ρ ∈ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g
                  ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ ((K⇩1 sporadic τ on K⇩2) # Ψ) ▹ Φ)
                                        ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                            ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        proof -
          assume h2: ‹ρ ∈ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)
                                    ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                             ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
            using h2 SporadicOn.prems by simp

            from this obtain Γ⇩k Ψ⇩k Φ⇩k k
            where fp:‹((((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)
                            ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))›
              and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
            have pc:‹(Γ, n ⊢ ((K⇩1 sporadic τ on K⇩2) # Ψ) ▹ Φ)
              ↪ (((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)›
            by (simp add: elims_part sporadic_on_e2)
            hence ‹(Γ, n ⊢ (K⇩1 sporadic τ on K⇩2) # Ψ ▹ Φ)
                    ↪⇗Suc k⇖ (Γ⇩k, 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 ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
             ∪ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          by simp
        with br1 br2 show ?case by blast
  next
    case (TagRelation K⇩1 K⇩2 R)
      have branches: ‹⟦ Γ, n ⊢ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          = ⟦ ((⌊τ⇩v⇩a⇩r(K⇩1, n), τ⇩v⇩a⇩r(K⇩2, n)⌋ ∈ R) # Γ), n
              ⊢ Ψ ▹ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        using HeronConf_interp_stepwise_tagrel_cases by simp
      thus ?case
      proof -
        have ‹∃Γ⇩k Ψ⇩k Φ⇩k k.
            ((((⌊τ⇩v⇩a⇩r(K⇩1, n), τ⇩v⇩a⇩r(K⇩2, n)⌋ ∈ R) # Γ), n
                ⊢ Ψ ▹ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Φ))
              ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using TagRelation.prems by simp

        from this obtain Γ⇩k Ψ⇩k Φ⇩k k
          where fp:‹((((⌊τ⇩v⇩a⇩r(K⇩1, n), τ⇩v⇩a⇩r(K⇩2, n)⌋ ∈ R) # Γ), n
                        ⊢ Ψ ▹ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Φ))
                    ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))›
            and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have pc:‹(Γ, n ⊢ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Ψ) ▹ Φ)
            ↪ (((⌊τ⇩v⇩a⇩r (K⇩1, n), τ⇩v⇩a⇩r (K⇩2, n)⌋ ∈ R) # Γ), n
                  ⊢ Ψ ▹ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Φ))›
          by (simp add: elims_part tagrel_e)
        hence ‹(Γ, n ⊢ (time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Ψ ▹ Φ)
                ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
  next
    case (Implies K⇩1 K⇩2)
      have branches: ‹⟦ Γ, n ⊢ ((K⇩1 implies K⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          = ⟦ ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          ∪ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        using HeronConf_interp_stepwise_implies_cases by simp
      moreover have br1: ‹ρ ∈ ⟦ ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
                ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ ((K⇩1 implies K⇩2) # Ψ) ▹ Φ)
                                    ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                  ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
      proof -
        assume h1: ‹ρ ∈ ⟦ ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k.
                    ((((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))
                        ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                  ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using h1 Implies.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k where
          fp:‹((((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))
            ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))›
          and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have pc:‹(Γ, n ⊢ (K⇩1 implies K⇩2) # Ψ ▹ Φ)
                  ↪ (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))›
          by (simp add: elims_part implies_e1)
        hence ‹(Γ, n ⊢ (K⇩1 implies K⇩2) # Ψ ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2: ‹ρ ∈ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ⇑ n) # Γ), n
                                ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
                            ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ ((K⇩1 implies K⇩2) # Ψ) ▹ Φ)
                                              ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                                  ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
      proof -
        assume h2: ‹ρ ∈ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ⇑ n) # Γ), n
                          ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. (
                        (((K⇩1 ⇑ n) # (K⇩2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))
                          ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)
                    ) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using h2 Implies.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k where
            fp:‹(((K⇩1 ⇑ n) # (K⇩2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))
                ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
        and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have ‹(Γ, n ⊢ ((K⇩1 implies K⇩2) # Ψ) ▹ Φ)
              ↪ (((K⇩1 ⇑ n) # (K⇩2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))›
          by (simp add: elims_part implies_e2)
        hence ‹(Γ, n ⊢ ((K⇩1 implies K⇩2) # Ψ) ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, 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 K⇩1 K⇩2)
      have branches: ‹⟦ Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          = ⟦ ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          ∪ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        using HeronConf_interp_stepwise_implies_not_cases by simp
      moreover have br1: ‹ρ ∈ ⟦ ((K⇩1 ¬⇑ n) # Γ), n
                            ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
                ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ)
                                    ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                  ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
      proof -
        assume h1: ‹ρ ∈ ⟦ ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k.
                    ((((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ))
                      ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                  ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using h1 ImpliesNot.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k where
          fp:‹((((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ))
                ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))›
          and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have pc:‹(Γ, n ⊢ (K⇩1 implies not K⇩2) # Ψ ▹ Φ)
                  ↪ (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ))›
          by (simp add: elims_part implies_not_e1)
        hence ‹(Γ, n ⊢ (K⇩1 implies not K⇩2) # Ψ ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2: ‹ρ ∈ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ¬⇑ n) # Γ), n
                            ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
                            ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ)
                                              ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                                  ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
      proof -
        assume h2: ‹ρ ∈ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ¬⇑ n) # Γ), n
                          ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. (
                     (((K⇩1 ⇑ n) # (K⇩2 ¬⇑ n) # Γ), n
                       ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)
                    ) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using h2 ImpliesNot.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k where
            fp:‹(((K⇩1 ⇑ n) # (K⇩2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ))
                ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
        and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have ‹(Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ)
              ↪ (((K⇩1 ⇑ n) # (K⇩2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ))›
          by (simp add: elims_part implies_not_e2)
        hence ‹(Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ)
                ↪⇗Suc k⇖ (Γ⇩k, 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 K⇩1 δτ K⇩2 K⇩3)
      have branches:
        ‹⟦ Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          = ⟦ ((K⇩1 ¬⇑ n) # Γ), n
              ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          ∪ ⟦ ((K⇩1 ⇑ n) # (K⇩2 @ n ⊕ δτ ⇒ K⇩3) # Γ), n
              ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        using HeronConf_interp_stepwise_timedelayed_cases by simp
      moreover have br1:
        ‹ρ ∈ ⟦ ((K⇩1 ¬⇑ n) # Γ), n
              ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k.
            ((Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)
                ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
            ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
      proof -
        assume h1: ‹ρ ∈ ⟦ ((K⇩1 ¬⇑ n) # Γ), n
                         ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k.
          ((((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))
            ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
          ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using h1 TimeDelayedBy.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k
          where fp:‹(((K⇩1 ¬⇑ n) # Γ), n
                      ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))
                    ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
            and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have ‹(Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)
              ↪ (((K⇩1 ¬⇑ n) # Γ), n
                    ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))›
          by (simp add: elims_part timedelayed_e1)
        hence ‹(Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)
                ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2:
        ‹ρ ∈ ⟦ ((K⇩1 ⇑ n) # (K⇩2 @ n ⊕ δτ ⇒ K⇩3) # Γ), n
              ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k.
              ((Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)
                ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
              ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
      proof -
        assume h2: ‹ρ ∈ ⟦ ((K⇩1 ⇑ n) # (K⇩2 @ n ⊕ δτ ⇒ K⇩3) # Γ), n
                    ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((K⇩1 ⇑ n) # (K⇩2 @ n ⊕ δτ ⇒ K⇩3) # Γ), n
                                 ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))
                                 ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                                ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using h2 TimeDelayedBy.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k
          where fp:‹(((K⇩1 ⇑ n) # (K⇩2 @ n ⊕ δτ ⇒ K⇩3) # Γ), n
                         ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))
                       ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
            and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have ‹(Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)
              ↪ (((K⇩1 ⇑ n) # (K⇩2 @ n ⊕ δτ ⇒ K⇩3) # Γ), n
                  ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))›
          by (simp add: elims_part timedelayed_e2)
        with fp relpowp_Suc_I2 have
          ‹(Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)
            ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
          by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case using TimeDelayedBy.prems(2) by blast
  next
    case (WeaklyPrecedes K⇩1 K⇩2)
      have ‹⟦ Γ, n ⊢ ((K⇩1 weakly precedes K⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g =
        ⟦ ((⌈#⇧≤ K⇩2 n, #⇧≤ K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
            ⊢ Ψ ▹ ((K⇩1 weakly precedes K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        using HeronConf_interp_stepwise_weakly_precedes_cases by simp
      moreover have ‹ρ ∈ ⟦ ((⌈#⇧≤ K⇩2 n, #⇧≤ K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                            ⊢ Ψ ▹ ((K⇩1 weakly precedes K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
            ⟹ (∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ ((K⇩1 weakly precedes K⇩2) # Ψ) ▹ Φ)
                                  ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                ∧ (ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g))›
      proof -
        assume ‹ρ ∈ ⟦ ((⌈#⇧≤ K⇩2 n, #⇧≤ K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                        ⊢ Ψ ▹ ((K⇩1 weakly precedes K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((⌈#⇧≤ K⇩2 n, #⇧≤ K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K⇩1 weakly precedes K⇩2) # Φ))
                             ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                          ∧ (ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g)›
          using  WeaklyPrecedes.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k
          where fp:‹(((⌈#⇧≤ K⇩2 n, #⇧≤ K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K⇩1 weakly precedes K⇩2) # Φ))
                             ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
            and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have ‹(Γ, n ⊢ ((K⇩1 weakly precedes K⇩2) # Ψ) ▹ Φ)
                ↪ (((⌈#⇧≤ K⇩2 n, #⇧≤ K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
              ⊢ Ψ ▹ ((K⇩1 weakly precedes K⇩2) # Φ))›
          by (simp add: elims_part weakly_precedes_e)
        with fp relpowp_Suc_I2 have ‹(Γ, n ⊢ ((K⇩1 weakly precedes K⇩2) # Ψ) ▹ Φ)
                                      ↪⇗Suc k⇖ (Γ⇩k, 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 K⇩1 K⇩2)
      have ‹⟦ Γ, n ⊢ ((K⇩1 strictly precedes K⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g =
        ⟦ ((⌈#⇧≤ K⇩2 n, #⇧< K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
          ⊢ Ψ ▹ ((K⇩1 strictly precedes K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        using HeronConf_interp_stepwise_strictly_precedes_cases by simp
      moreover have ‹ρ ∈ ⟦ ((⌈#⇧≤ K⇩2 n, #⇧< K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                            ⊢ Ψ ▹ ((K⇩1 strictly precedes K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
            ⟹ (∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ ((K⇩1 strictly precedes K⇩2) # Ψ) ▹ Φ)
                                  ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                ∧ (ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g))›
      proof -
        assume ‹ρ ∈ ⟦ ((⌈#⇧≤ K⇩2 n, #⇧< K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                        ⊢ Ψ ▹ ((K⇩1 strictly precedes K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((⌈#⇧≤ K⇩2 n, #⇧< K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K⇩1 strictly precedes K⇩2) # Φ))
                             ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                            ∧ (ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g)›
          using  StrictlyPrecedes.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k
          where fp:‹(((⌈#⇧≤ K⇩2 n, #⇧< K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K⇩1 strictly precedes K⇩2) # Φ))
                             ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
            and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have ‹(Γ, n ⊢ ((K⇩1 strictly precedes K⇩2) # Ψ) ▹ Φ)
                ↪ (((⌈#⇧≤ K⇩2 n, #⇧< K⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
              ⊢ Ψ ▹ ((K⇩1 strictly precedes K⇩2) # Φ))›
          by (simp add: elims_part strictly_precedes_e)
        with fp relpowp_Suc_I2 have ‹(Γ, n ⊢ ((K⇩1 strictly precedes K⇩2) # Ψ) ▹ Φ)
                                      ↪⇗Suc k⇖ (Γ⇩k, 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 K⇩1 K⇩2)
      have branches: ‹⟦ Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          = ⟦ ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          ∪ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        using HeronConf_interp_stepwise_kills_cases by simp
      moreover have br1: ‹ρ ∈ ⟦ ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
                ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ)
                                    ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                  ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
      proof -
        assume h1: ‹ρ ∈ ⟦ ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k.
                    ((((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))
                    ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                  ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using h1 Kills.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k where
          fp:‹((((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))
                ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))›
          and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have pc:‹(Γ, n ⊢ (K⇩1 kills K⇩2) # Ψ ▹ Φ)
                  ↪ (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))›
          by (simp add: elims_part kills_e1)
        hence ‹(Γ, n ⊢ (K⇩1 kills K⇩2) # Ψ ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2:
        ‹ρ ∈ ⟦ ((K⇩1 ⇑ n) # (K⇩2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g
          ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ)
                                ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                          ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
      proof -
        assume h2: ‹ρ ∈ ⟦((K⇩1 ⇑ n)#(K⇩2 ¬⇑ ≥ n)#Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2)#Φ)⟧⇩c⇩o⇩n⇩f⇩i⇩g›
        then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. (
                    (((K⇩1 ⇑ n) # (K⇩2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))
                      ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)
                    ) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using h2 Kills.prems by simp
        from this obtain Γ⇩k Ψ⇩k Φ⇩k k where
            fp:‹(((K⇩1 ⇑ n) # (K⇩2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))
                ↪⇗k⇖ (Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k)›
        and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast
        have ‹(Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ)
              ↪ (((K⇩1 ⇑ n) # (K⇩2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))›
          by (simp add: elims_part kills_e2)
        hence ‹(Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, 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 < n⇩k›
  assumes ‹ρ ∈ ⟦ Γ, n ⊢ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
  shows   ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊢ Ψ ▹ Φ) ↪⇗k⇖ (Γ⇩k, n⇩k ⊢ Ψ⇩k ▹ Φ⇩k))
                         ∧ ρ ∈ ⟦ Γ⇩k, n⇩k ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
proof -
  obtain δk where diff: ‹n⇩k = δ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 ⊢ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k.
                  ((Γ, n ⊢ Ψ ▹ Φ) ↪⇗k⇖ (Γ⇩k, δk + Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                ∧ ρ ∈ ⟦ Γ⇩k, δk + Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          using Suc.hyps by blast
        obtain Γ⇩k Ψ⇩k Φ⇩k k
          where cont: ‹((Γ, n ⊢ Ψ ▹ Φ) ↪⇗k⇖ (Γ⇩k, δk + Suc n ⊢ Ψ⇩k ▹ Φ⇩k))
                      ∧ ρ ∈ ⟦ Γ⇩k, δk + Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          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' ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          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' ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
          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 ⊢ Ψ ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc (δk + Suc n) ⊢ Ψ⇩k ▹ Φ⇩k))
                  ∧ ρ ∈ ⟦ Γ⇩k, Suc δk + Suc n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
            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 ‹ρ ∈ ⟦⟦ Ψ ⟧⟧⇩T⇩E⇩S⇩L›
    shows ‹∃k Γ⇩k Ψ⇩k Φ⇩k. (([], 0 ⊢ Ψ ▹ [])  ↪⇗k⇖ (Γ⇩k, n ⊢ Ψ⇩k ▹ Φ⇩k))
                         ∧ ρ ∈ ⟦ Γ⇩k, n ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
proof -
  have 1:‹∃Γ⇩k Ψ⇩k Φ⇩k k. (([], 0 ⊢ Ψ ▹ []) ↪⇗k⇖ (Γ⇩k, 0 ⊢ Ψ⇩k ▹ Φ⇩k))
                      ∧ ρ ∈ ⟦ Γ⇩k, 0 ⊢ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g›
    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 ⊢ Ψ ▹ [] ⟧⇩c⇩o⇩n⇩f⇩i⇩g › 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 + μ Φ
                    | _                 ⇒ 2 + μ Φ)›

fun measure_interpretation_config :: ‹'τ::linordered_field config ⇒ nat› (‹μ⇩c⇩o⇩n⇩f⇩i⇩g›)
where
  ‹μ⇩c⇩o⇩n⇩f⇩i⇩g (Γ, n ⊢ Ψ ▹ Φ) = μ Ψ›

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

lemma elimation_rules_strictly_decreasing_meas:
  assumes ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)  ↪⇩e  (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)›
    shows ‹(Ψ⇩2, Ψ⇩1) ∈ measure μ›
using assms by (auto elim: operational_semantics_elim.cases)

lemma elimation_rules_strictly_decreasing_meas':
  assumes ‹𝒮⇩1  ↪⇩e  𝒮⇩2›
  shows ‹(𝒮⇩2, 𝒮⇩1) ∈ measure μ⇩c⇩o⇩n⇩f⇩i⇩g›
proof -
  from assms obtain Γ⇩1 n⇩1 Ψ⇩1 Φ⇩1 where p1:‹𝒮⇩1 = (Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)›
    using measure_interpretation_config.cases by blast
  from assms obtain Γ⇩2 n⇩2 Ψ⇩2 Φ⇩2 where p2:‹𝒮⇩2 = (Γ⇩2, n⇩2 ⊢ Ψ⇩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 ‹μ⇩c⇩o⇩n⇩f⇩i⇩g (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) < μ⇩c⇩o⇩n⇩f⇩i⇩g (Γ⇩1, n⇩1 ⊢ Ψ⇩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. (𝒮⇩1  ↪⇩e⇧←  𝒮⇩2))›
proof (simp add: wfp_def)
  show ‹wf {((𝒮⇩1::'a::linordered_field config), 𝒮⇩2). 𝒮⇩1 ↪⇩e⇧← 𝒮⇩2}›
  proof (rule wf_subset)
    have ‹measure μ⇩c⇩o⇩n⇩f⇩i⇩g = {(𝒮⇩2, (𝒮⇩1::'a::linordered_field config)).
                               μ⇩c⇩o⇩n⇩f⇩i⇩g 𝒮⇩2 < μ⇩c⇩o⇩n⇩f⇩i⇩g 𝒮⇩1}›
      by (simp add: inv_image_def less_eq measure_def)
    thus ‹{((𝒮⇩1::'a::linordered_field config), 𝒮⇩2). 𝒮⇩1 ↪⇩e⇧← 𝒮⇩2} ⊆ (measure μ⇩c⇩o⇩n⇩f⇩i⇩g)›
      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