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⇖›
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) # Φ))›
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 ⊢ Ψ ▹ Φ)›
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
[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 ψ)
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›
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)›
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) # Φ))›
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›

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 ⊢ Ψ ▹ Φ)›
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
‹ρ ∈ ⟦ Γ, 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) # Φ))›
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) # Φ))›
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) # Φ))›
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) # Φ))›
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) # Φ))›
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) # Φ))›
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) # Φ))›
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) # Φ))›
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) # Φ))›
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) # Φ))›
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) # Φ))›
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›
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))›
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
```