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 ‹⟦⟦ Ψ ⟧⟧⇩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 C⇩1 τ C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ (C⇩1 sporadic τ on C⇩2) # Ψ ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic τ on C⇩2) # Φ))› thus ?P using configuration_interp_stepwise_sporadicon_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 τ C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ (C⇩1 sporadic τ on C⇩2) # Ψ ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ⇑ n) # (C⇩2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ)› thus ?P using configuration_interp_stepwise_sporadicon_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 τ⇩e⇩x⇩p⇩r C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ (C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Φ))› thus ?P using configuration_interp_stepwise_sporadicon_tvar_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 τ⇩e⇩x⇩p⇩r C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ (C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ⇑ n) # (C⇩2 ⇓ n @♯ τ⇩e⇩x⇩p⇩r) # Γ), n ⊨ Ψ ▹ Φ)› thus ?P using configuration_interp_stepwise_sporadicon_tvar_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 C⇩2 R Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ (time-relation ⌊C⇩1, C⇩2⌋ ∈ R) # Ψ ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((⌊τ⇩v⇩a⇩r (C⇩1, n), τ⇩v⇩a⇩r (C⇩2, n)⌋ ∈ R) # Γ), n ⊨ Ψ ▹ ((time-relation ⌊C⇩1, C⇩2⌋ ∈ R) # Φ))› thus ?P using configuration_interp_stepwise_tagrel_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ (C⇩1 implies C⇩2) # Ψ ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ))› thus ?P using configuration_interp_stepwise_implies_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ ((C⇩1 implies C⇩2) # Ψ) ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ⇑ n) # (C⇩2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ))› thus ?P using configuration_interp_stepwise_implies_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ ((C⇩1 implies not C⇩2) # Ψ) ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ))› thus ?P using configuration_interp_stepwise_implies_not_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ ((C⇩1 implies not C⇩2) # Ψ) ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ⇑ n) # (C⇩2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ))› thus ?P using configuration_interp_stepwise_implies_not_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 δτ C⇩2 C⇩3 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ))› thus ?P using configuration_interp_stepwise_timedelayed_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 δτ C⇩2 C⇩3 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ⇑ n) # (C⇩2 @ n ⊕ δτ ⇒ C⇩3) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ))› thus ?P using configuration_interp_stepwise_timedelayed_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 δτ C⇩2 C⇩3 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ (C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ))› thus ?P using configuration_interp_stepwise_timedelayed_tvar_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 δτ C⇩2 C⇩3 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ (C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ⇑ n) # Γ), n ⊨ (C⇩3 sporadic♯ ⦇ τ⇩v⇩a⇩r (C⇩2, n) ⊕ δτ ⦈ on C⇩2) # Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ))› thus ?P using configuration_interp_stepwise_timedelayed_tvar_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ ((C⇩1 weakly precedes C⇩2) # Ψ) ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((⌈#⇧≤ C⇩2 n, #⇧≤ C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 weakly precedes C⇩2) # Φ))› thus ?P using configuration_interp_stepwise_weakly_precedes_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ ((C⇩1 strictly precedes C⇩2) # Ψ) ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((⌈#⇧≤ C⇩2 n, #⇧< C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 strictly precedes C⇩2) # Φ))› thus ?P using configuration_interp_stepwise_strictly_precedes_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ ((C⇩1 kills C⇩2) # Ψ) ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ))› thus ?P using configuration_interp_stepwise_kills_cases configuration_interpretation.simps by blast next fix Γ n C⇩1 C⇩2 Ψ Φ assume ‹(Γ⇩1, n⇩1 ⊨ Ψ⇩1 ▹ Φ⇩1) = (Γ, n ⊨ ((C⇩1 kills C⇩2) # Ψ) ▹ Φ)› and ‹(Γ⇩2, n⇩2 ⊨ Ψ⇩2 ▹ Φ⇩2) = (((C⇩1 ⇑ n) # (C⇩2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ))› 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 ‹⟦ 𝒮⇩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 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 C⇩1 C⇩2 R) thus ?thesis using configuration_interp_stepwise_tagrel_cases [of ‹Γ› ‹n› ‹C⇩1› ‹C⇩2› ‹R› ‹Ψ› ‹Φ›] Cnext_solve_tagrel[of ‹C⇩1› ‹n› ‹C⇩2› ‹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 ‹⟦ 𝒮 ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⊆ (⋃X∈𝒞⇩n⇩e⇩x⇩t 𝒮. ⟦ X ⟧⇩c⇩o⇩n⇩f⇩i⇩g)› 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 ‹ρ ∈ ⟦ 𝒮⇩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 C⇩1 τ C⇩2) have branches: ‹⟦ Γ, n ⊨ ((C⇩1 sporadic τ on C⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic τ on C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ∪ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_sporadicon_cases by simp have br1: ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic τ on C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 sporadic τ on C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h1: ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic τ on C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic τ on C⇩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 ⊨ Ψ ▹ ((C⇩1 sporadic τ on C⇩2) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast have ‹(Γ, n ⊨ ((C⇩1 sporadic τ on C⇩2) # Ψ) ▹ Φ) ↪ (Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic τ on C⇩2) # Φ))› by (simp add: elims_part sporadic_on_e1) with fp relpowp_Suc_I2 have ‹((Γ, n ⊨ ((C⇩1 sporadic τ on C⇩2) # Ψ) ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k))› by auto thus ?thesis using fp by blast qed have br2: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 sporadic τ on C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h2: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g› hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩1 ⇑ n) # (C⇩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:‹((((C⇩1 ⇑ n) # (C⇩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 ⊨ ((C⇩1 sporadic τ on C⇩2) # Ψ) ▹ Φ) ↪ (((C⇩1 ⇑ n) # (C⇩2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ)› by (simp add: elims_part sporadic_on_e2) hence ‹(Γ, n ⊨ (C⇩1 sporadic τ on C⇩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 ⊨ Ψ ▹ ((C⇩1 sporadic τ on C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ∪ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by simp with br1 br2 show ?case by blast next case (SporadicOnTvar C⇩1 τ⇩e⇩x⇩p⇩r C⇩2) have branches: ‹⟦ Γ, n ⊨ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ∪ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇓ n @♯ τ⇩e⇩x⇩p⇩r) # Γ), n ⊨ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_sporadicon_tvar_cases by simp have br1: ‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h:‹ρ ∈ ⟦ Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using Cons.hyps by blast from this obtain Γ⇩k Ψ⇩k Φ⇩k k where ‹((Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k))› and *:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast moreover have ‹(Γ, n ⊨((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ) ▹ Φ) ↪(Γ, n ⊨ Ψ ▹ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Φ))› by (simp add: sporadic_on_tvar_e1 elims_part) ultimately have ‹((Γ, n ⊨ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ) ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k))› using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast with * have ‹((Γ, n ⊨ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ) ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by simp thus ?thesis by blast qed moreover have br2: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇓ n @♯ τ⇩e⇩x⇩p⇩r) # Γ), n ⊨ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h:‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇓ n @♯ τ⇩e⇩x⇩p⇩r) # Γ), n ⊨ Ψ ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g› hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩1 ⇑ n) # (C⇩2 ⇓ n @♯ τ⇩e⇩x⇩p⇩r) # Γ), n ⊨ Ψ ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using Cons.hyps by blast from this obtain Γ⇩k Ψ⇩k Φ⇩k k where ‹((((C⇩1 ⇑ n) # (C⇩2 ⇓ n @♯ τ⇩e⇩x⇩p⇩r) # Γ), n ⊨ Ψ ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k))› and *:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast moreover have ‹(Γ, n ⊨((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ) ▹ Φ) ↪(((C⇩1 ⇑ n) # (C⇩2 ⇓ n @♯ τ⇩e⇩x⇩p⇩r) # Γ), n ⊨ Ψ ▹ Φ)› by (simp add: sporadic_on_tvar_e2 elims_part) ultimately have ‹((Γ, n ⊨ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ) ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k))› using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast with * have ‹((Γ, n ⊨ ((C⇩1 sporadic♯ τ⇩e⇩x⇩p⇩r on C⇩2) # Ψ) ▹ Φ) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by simp thus ?thesis by blast qed ultimately show ?case using branches SporadicOnTvar.prems(2) by blast next case (TagRelation C⇩1 C⇩2 R) have branches: ‹⟦ Γ, n ⊨ ((time-relation ⌊C⇩1, C⇩2⌋ ∈ R) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ ((⌊τ⇩v⇩a⇩r(C⇩1, n), τ⇩v⇩a⇩r(C⇩2, n)⌋ ∈ R) # Γ), n ⊨ Ψ ▹ ((time-relation ⌊C⇩1, C⇩2⌋ ∈ R) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_tagrel_cases by simp thus ?case proof - have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((⌊τ⇩v⇩a⇩r(C⇩1, n), τ⇩v⇩a⇩r(C⇩2, n)⌋ ∈ R) # Γ), n ⊨ Ψ ▹ ((time-relation ⌊C⇩1, C⇩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(C⇩1, n), τ⇩v⇩a⇩r(C⇩2, n)⌋ ∈ R) # Γ), n ⊨ Ψ ▹ ((time-relation ⌊C⇩1, C⇩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 ⌊C⇩1, C⇩2⌋ ∈ R) # Ψ) ▹ Φ) ↪ (((⌊τ⇩v⇩a⇩r (C⇩1, n), τ⇩v⇩a⇩r (C⇩2, n)⌋ ∈ R) # Γ), n ⊨ Ψ ▹ ((time-relation ⌊C⇩1, C⇩2⌋ ∈ R) # Φ))› by (simp add: elims_part tagrel_e) hence ‹(Γ, n ⊨ (time-relation ⌊C⇩1, C⇩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 C⇩1 C⇩2) have branches: ‹⟦ Γ, n ⊨ ((C⇩1 implies C⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ∪ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_implies_cases by simp moreover have br1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 implies C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩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:‹((((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩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 ⊨ (C⇩1 implies C⇩2) # Ψ ▹ Φ) ↪ (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ))› by (simp add: elims_part implies_e1) hence ‹(Γ, n ⊨ (C⇩1 implies C⇩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: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 implies C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h2: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ( (((C⇩1 ⇑ n) # (C⇩2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩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:‹(((C⇩1 ⇑ n) # (C⇩2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast have ‹(Γ, n ⊨ ((C⇩1 implies C⇩2) # Ψ) ▹ Φ) ↪ (((C⇩1 ⇑ n) # (C⇩2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies C⇩2) # Φ))› by (simp add: elims_part implies_e2) hence ‹(Γ, n ⊨ ((C⇩1 implies C⇩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 C⇩1 C⇩2) have branches: ‹⟦ Γ, n ⊨ ((C⇩1 implies not C⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ∪ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_implies_not_cases by simp moreover have br1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 implies not C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩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:‹((((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩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 ⊨ (C⇩1 implies not C⇩2) # Ψ ▹ Φ) ↪ (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ))› by (simp add: elims_part implies_not_e1) hence ‹(Γ, n ⊨ (C⇩1 implies not C⇩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: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 implies not C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h2: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ( (((C⇩1 ⇑ n) # (C⇩2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩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:‹(((C⇩1 ⇑ n) # (C⇩2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast have ‹(Γ, n ⊨ ((C⇩1 implies not C⇩2) # Ψ) ▹ Φ) ↪ (((C⇩1 ⇑ n) # (C⇩2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 implies not C⇩2) # Φ))› by (simp add: elims_part implies_not_e2) hence ‹(Γ, n ⊨ ((C⇩1 implies not C⇩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 C⇩1 δτ C⇩2 C⇩3) have branches: ‹⟦ Γ, n ⊨ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ∪ ⟦ ((C⇩1 ⇑ n) # (C⇩2 @ n ⊕ δτ ⇒ C⇩3) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_timedelayed_cases by simp moreover have br1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩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:‹(((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast have ‹(Γ, n ⊨ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪ (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ))› by (simp add: elims_part timedelayed_e1) hence ‹(Γ, n ⊨ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩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: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 @ n ⊕ δτ ⇒ C⇩3) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h2: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 @ n ⊕ δτ ⇒ C⇩3) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩1 ⇑ n) # (C⇩2 @ n ⊕ δτ ⇒ C⇩3) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩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:‹(((C⇩1 ⇑ n) # (C⇩2 @ n ⊕ δτ ⇒ C⇩3) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast have ‹(Γ, n ⊨ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪ (((C⇩1 ⇑ n) # (C⇩2 @ n ⊕ δτ ⇒ C⇩3) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩3) # Φ))› by (simp add: elims_part timedelayed_e2) with fp relpowp_Suc_I2 have ‹(Γ, n ⊨ ((C⇩1 time-delayed by δτ on C⇩2 implies C⇩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 (RelaxedTimeDelayed C⇩1 δτ C⇩2 C⇩3) have branches: ‹⟦ Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ∪ ⟦ ((C⇩1 ⇑ n) # Γ), n ⊨ (C⇩3 sporadic♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈ on C⇩2) # Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_timedelayed_tvar_cases by simp have more_branches: ‹⟦ ((C⇩1 ⇑ n) # Γ), n ⊨ ((C⇩3 sporadic♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈ on C⇩2) # Ψ) ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ ((C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩3 sporadic♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈ on C⇩2) # (C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ∪ ⟦ ((C⇩3 ⇑ n) # (C⇩2 ⇓ n @♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈) # (C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_sporadicon_tvar_cases by blast moreover have br1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using h1 RelaxedTimeDelayed.prems by simp from this obtain Γ⇩k Ψ⇩k Φ⇩k k where fp:‹(((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast have ‹(Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪ (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ))› by (simp add: elims_part timedelayed_tvar_e1) hence ‹(Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩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: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩3 sporadic♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈ on C⇩2) # (C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h2: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩3 sporadic♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈ on C⇩2) # (C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩3 sporadic♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈ on C⇩2) # (C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using h2 RelaxedTimeDelayed.prems by simp from this obtain Γ⇩k Ψ⇩k Φ⇩k k where ‹((((C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩3 sporadic♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈ on C⇩2) # (C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k))› and *:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast moreover have ‹( ((C⇩1 ⇑ n) # Γ), n ⊨ (C⇩3 sporadic♯ ⦇ τ⇩v⇩a⇩r (C⇩2, n) ⊕ δτ ⦈ on C⇩2) # Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪ ( ((C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩3 sporadic♯ ⦇ τ⇩v⇩a⇩r (C⇩2, n) ⊕ δτ ⦈ on C⇩2) # (C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ))› by (simp add: elims_part sporadic_on_tvar_e1) ultimately have ‹( ((C⇩1 ⇑ n) # Γ), n ⊨ (C⇩3 sporadic♯ ⦇ τ⇩v⇩a⇩r (C⇩2, n) ⊕ δτ ⦈ on C⇩2) # Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast moreover have ‹(Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪ ( ((C⇩1 ⇑ n) # Γ), n ⊨ (C⇩3 sporadic♯ ⦇ τ⇩v⇩a⇩r (C⇩2, n) ⊕ δτ ⦈ on C⇩2) # Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ))› by (simp add: elims_part timedelayed_tvar_e2) ultimately have ‹(Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪⇗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': ‹ρ ∈ ⟦ ((C⇩3 ⇑ n) # (C⇩2 ⇓ n @♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈) # (C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h2: ‹ρ ∈ ⟦ ((C⇩3 ⇑ n) # (C⇩2 ⇓ n @♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈) # (C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩3 ⇑ n) # (C⇩2 ⇓ n @♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈) # (C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using h2 RelaxedTimeDelayed.prems by simp from this obtain Γ⇩k Ψ⇩k Φ⇩k k where ‹ ( (((C⇩3 ⇑ n) # (C⇩2 ⇓ n @♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈) # (C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k))› and *:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast moreover have ‹( ((C⇩1 ⇑ n) # Γ), n ⊨ (C⇩3 sporadic♯ ⦇ τ⇩v⇩a⇩r (C⇩2, n) ⊕ δτ ⦈ on C⇩2) # Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪ (((C⇩3 ⇑ n) # (C⇩2 ⇓ n @♯ ⦇τ⇩v⇩a⇩r(C⇩2, n) ⊕ δτ⦈) # (C⇩1 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ))› by (simp add: elims_part sporadic_on_tvar_e2) ultimately have ‹( ((C⇩1 ⇑ n) # Γ), n ⊨ (C⇩3 sporadic♯ ⦇ τ⇩v⇩a⇩r (C⇩2, n) ⊕ δτ ⦈ on C⇩2) # Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ)) ↪⇗Suc k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› using relpowp_Suc_I2[of ‹operational_semantics_step›] by blast moreover have ‹(Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪ ( ((C⇩1 ⇑ n) # Γ), n ⊨ (C⇩3 sporadic♯ ⦇ τ⇩v⇩a⇩r (C⇩2, n) ⊕ δτ ⦈ on C⇩2) # Ψ ▹ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Φ))› by (simp add: elims_part timedelayed_tvar_e2) ultimately have ‹(Γ, n ⊨ ((C⇩1 time-delayed⨝ by δτ on C⇩2 implies C⇩3) # Ψ) ▹ Φ) ↪⇗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 C⇩1 C⇩2) have ‹⟦ Γ, n ⊨ ((C⇩1 weakly precedes C⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ ((⌈#⇧≤ C⇩2 n, #⇧≤ C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 weakly precedes C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_weakly_precedes_cases by simp moreover have ‹ρ ∈ ⟦ ((⌈#⇧≤ C⇩2 n, #⇧≤ C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 weakly precedes C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ (∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 weakly precedes C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ (ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g))› proof - assume ‹ρ ∈ ⟦ ((⌈#⇧≤ C⇩2 n, #⇧≤ C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 weakly precedes C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((⌈#⇧≤ C⇩2 n, #⇧≤ C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 weakly precedes C⇩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:‹(((⌈#⇧≤ C⇩2 n, #⇧≤ C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 weakly precedes C⇩2) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast have ‹(Γ, n ⊨ ((C⇩1 weakly precedes C⇩2) # Ψ) ▹ Φ) ↪ (((⌈#⇧≤ C⇩2 n, #⇧≤ C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 weakly precedes C⇩2) # Φ))› by (simp add: elims_part weakly_precedes_e) with fp relpowp_Suc_I2 have ‹(Γ, n ⊨ ((C⇩1 weakly precedes C⇩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 C⇩1 C⇩2) have ‹⟦ Γ, n ⊨ ((C⇩1 strictly precedes C⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ ((⌈#⇧≤ C⇩2 n, #⇧< C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 strictly precedes C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_strictly_precedes_cases by simp moreover have ‹ρ ∈ ⟦ ((⌈#⇧≤ C⇩2 n, #⇧< C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 strictly precedes C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ (∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 strictly precedes C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ (ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g))› proof - assume ‹ρ ∈ ⟦ ((⌈#⇧≤ C⇩2 n, #⇧< C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 strictly precedes C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› hence ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((⌈#⇧≤ C⇩2 n, #⇧< C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 strictly precedes C⇩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:‹(((⌈#⇧≤ C⇩2 n, #⇧< C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 strictly precedes C⇩2) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast have ‹(Γ, n ⊨ ((C⇩1 strictly precedes C⇩2) # Ψ) ▹ Φ) ↪ (((⌈#⇧≤ C⇩2 n, #⇧< C⇩1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n ⊨ Ψ ▹ ((C⇩1 strictly precedes C⇩2) # Φ))› by (simp add: elims_part strictly_precedes_e) with fp relpowp_Suc_I2 have ‹(Γ, n ⊨ ((C⇩1 strictly precedes C⇩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 C⇩1 C⇩2) have branches: ‹⟦ Γ, n ⊨ ((C⇩1 kills C⇩2) # Ψ) ▹ Φ ⟧⇩c⇩o⇩n⇩f⇩i⇩g = ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ∪ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› using configuration_interp_stepwise_kills_cases by simp moreover have br1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 kills C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h1: ‹ρ ∈ ⟦ ((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ((((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩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:‹((((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩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 ⊨ (C⇩1 kills C⇩2) # Ψ ▹ Φ) ↪ (((C⇩1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ))› by (simp add: elims_part kills_e1) hence ‹(Γ, n ⊨ (C⇩1 kills C⇩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: ‹ρ ∈ ⟦ ((C⇩1 ⇑ n) # (C⇩2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ) ⟧⇩c⇩o⇩n⇩f⇩i⇩g ⟹ ∃Γ⇩k Ψ⇩k Φ⇩k k. ((Γ, n ⊨ ((C⇩1 kills C⇩2) # Ψ) ▹ Φ) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)) ∧ ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› proof - assume h2: ‹ρ ∈ ⟦((C⇩1 ⇑ n)#(C⇩2 ¬⇑ ≥ n)#Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2)#Φ)⟧⇩c⇩o⇩n⇩f⇩i⇩g› then have ‹∃Γ⇩k Ψ⇩k Φ⇩k k. ( (((C⇩1 ⇑ n) # (C⇩2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩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:‹(((C⇩1 ⇑ n) # (C⇩2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ)) ↪⇗k⇖ (Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k)› and rc:‹ρ ∈ ⟦ Γ⇩k, Suc n ⊨ Ψ⇩k ▹ Φ⇩k ⟧⇩c⇩o⇩n⇩f⇩i⇩g› by blast have ‹(Γ, n ⊨ ((C⇩1 kills C⇩2) # Ψ) ▹ Φ) ↪ (((C⇩1 ⇑ n) # (C⇩2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C⇩1 kills C⇩2) # Φ))› by (simp add: elims_part kills_e2) hence ‹(Γ, n ⊨ ((C⇩1 kills C⇩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 + μ Φ | _ 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