# Theory Restricted_Master_Theorem

```(*
Author:   Salomon Sickert
Author:   Benedikt Seidl
*)

section ‹Master Theorem with Reduced Subformulas›

theory Restricted_Master_Theorem
imports
Master_Theorem
begin

subsection ‹Restricted Set of Subformulas›

fun restricted_subformulas_inner :: "'a ltln ⇒ 'a ltln set"
where
"restricted_subformulas_inner (φ and⇩n ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas_inner (φ or⇩n ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas_inner (X⇩n φ) = restricted_subformulas_inner φ"
| "restricted_subformulas_inner (φ U⇩n ψ) = subformulas⇩ν (φ U⇩n ψ) ∪ subformulas⇩μ (φ U⇩n ψ)"
| "restricted_subformulas_inner (φ R⇩n ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas_inner (φ W⇩n ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas_inner (φ M⇩n ψ) = subformulas⇩ν (φ M⇩n ψ) ∪ subformulas⇩μ (φ M⇩n ψ)"
| "restricted_subformulas_inner _ = {}"

fun restricted_subformulas :: "'a ltln ⇒ 'a ltln set"
where
"restricted_subformulas (φ and⇩n ψ) = restricted_subformulas φ ∪ restricted_subformulas ψ"
| "restricted_subformulas (φ or⇩n ψ) = restricted_subformulas φ ∪ restricted_subformulas ψ"
| "restricted_subformulas (X⇩n φ) = restricted_subformulas φ"
| "restricted_subformulas (φ U⇩n ψ) = restricted_subformulas φ ∪ restricted_subformulas ψ"
| "restricted_subformulas (φ R⇩n ψ) = restricted_subformulas φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas (φ W⇩n ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas ψ"
| "restricted_subformulas (φ M⇩n ψ) = restricted_subformulas φ ∪ restricted_subformulas ψ"
| "restricted_subformulas _ = {}"

"restricted_subformulas_inner (φ[X]⇩ν) = {}"
by (induction φ) simp_all

"restricted_subformulas (φ[X]⇩ν) = {}"

lemma restricted_subformulas_inner_subset:
"restricted_subformulas_inner φ ⊆ subformulas⇩ν φ ∪ subformulas⇩μ φ"
by (induction φ) auto

lemma restricted_subformulas_subset':
"restricted_subformulas φ ⊆ restricted_subformulas_inner φ"
by (induction φ) (insert restricted_subformulas_inner_subset, auto)

lemma restricted_subformulas_subset:
"restricted_subformulas φ ⊆ subformulas⇩ν φ ∪ subformulas⇩μ φ"
using restricted_subformulas_inner_subset restricted_subformulas_subset' by auto

lemma restricted_subformulas_size:
"ψ ∈ restricted_subformulas φ ⟹ size ψ < size φ"
proof -
have "⋀φ. restricted_subformulas_inner φ ⊆ subfrmlsn φ"
using restricted_subformulas_inner_subset subformulas⇩μ⇩ν_subfrmlsn by blast

then have inner: "⋀ψ φ. ψ ∈ restricted_subformulas_inner φ ⟹ size ψ ≤ size φ"
using subfrmlsn_size dual_order.strict_implies_order
by blast

show "ψ ∈ restricted_subformulas φ ⟹ size ψ < size φ"
by (induction φ arbitrary: ψ) (fastforce dest: inner)+
qed

lemma restricted_subformulas_notin:
"φ ∉ restricted_subformulas φ"
using restricted_subformulas_size by auto

lemma restricted_subformulas_superset:
"ψ ∈ restricted_subformulas φ ⟹ subformulas⇩ν ψ ∪ subformulas⇩μ ψ ⊆ restricted_subformulas φ"
proof -
assume "ψ ∈ restricted_subformulas φ"

then obtain χ x where
"ψ ∈ restricted_subformulas_inner χ" and "(x R⇩n χ) ∈ subformulas⇩ν φ ∨ (χ W⇩n x) ∈ subformulas⇩ν φ "
by (induction φ) auto

moreover

have "⋀ψ⇩1 ψ⇩2. (ψ⇩1 R⇩n ψ⇩2) ∈ subformulas⇩ν φ ⟹ restricted_subformulas_inner ψ⇩2 ⊆ restricted_subformulas φ"
"⋀ψ⇩1 ψ⇩2. (ψ⇩1 W⇩n ψ⇩2) ∈ subformulas⇩ν φ ⟹ restricted_subformulas_inner ψ⇩1 ⊆ restricted_subformulas φ"
by (induction φ) (simp_all; insert restricted_subformulas_subset', blast)+

moreover

have "subformulas⇩ν ψ ∪ subformulas⇩μ ψ ⊆  restricted_subformulas_inner χ"
using ‹ψ ∈ restricted_subformulas_inner χ›
proof (induction χ)
case (Until_ltln χ1 χ2)
then show ?case
apply (cases "ψ = χ1 U⇩n χ2")
apply auto[1]
apply simp
apply (cases "ψ ∈ subformulas⇩ν χ1")
apply (meson le_supI1 le_supI2 subformulas⇩μ_subset subformulas⇩ν_subfrmlsn subformulas⇩ν_subset subset_eq subset_insertI2)
apply (cases "ψ ∈ subformulas⇩ν χ2")
apply (meson le_supI1 le_supI2 subformulas⇩μ_subset subformulas⇩ν_subfrmlsn subformulas⇩ν_subset subset_eq subset_insertI2)
apply (cases "ψ ∈ subformulas⇩μ χ1")
apply (metis (no_types, opaque_lifting) Un_insert_right subformulas⇩μ_subfrmlsn subformulas⇩μ_subset subformulas⇩ν_subset subsetD sup.coboundedI2 sup_commute)
apply simp
by (metis (no_types, opaque_lifting) Un_insert_right subformulas⇩μ_subfrmlsn subformulas⇩μ_subset subformulas⇩ν_subset subsetD sup.coboundedI2 sup_commute)
next
case (Release_ltln χ1 χ2)
then show ?case by simp blast
next
case (WeakUntil_ltln χ1 χ2)
then show ?case by simp blast
next
case (StrongRelease_ltln χ1 χ2)
then show ?case
apply (cases "ψ = χ1 M⇩n χ2")
apply auto[1]
apply simp
apply (cases "ψ ∈ subformulas⇩ν χ1")
apply (meson le_supI1 le_supI2 subformulas⇩μ_subset subformulas⇩ν_subfrmlsn subformulas⇩ν_subset subset_eq subset_insertI2)
apply (cases "ψ ∈ subformulas⇩ν χ2")
apply (meson le_supI1 le_supI2 subformulas⇩μ_subset subformulas⇩ν_subfrmlsn subformulas⇩ν_subset subset_eq subset_insertI2)
apply (cases "ψ ∈ subformulas⇩μ χ1")
apply (metis (no_types, opaque_lifting) Un_insert_right subformulas⇩μ_subfrmlsn subformulas⇩μ_subset subformulas⇩ν_subset subsetD sup.coboundedI2 sup_commute)
apply simp
by (metis (no_types, opaque_lifting) Un_insert_right subformulas⇩μ_subfrmlsn subformulas⇩μ_subset subformulas⇩ν_subset subsetD sup.coboundedI2 sup_commute)
qed auto

ultimately

show "subformulas⇩ν ψ ∪ subformulas⇩μ ψ ⊆ restricted_subformulas φ"
by blast
qed

lemma restricted_subformulas_W_μ:
"subformulas⇩μ φ ⊆ restricted_subformulas (φ W⇩n ψ)"
by (induction φ) auto

lemma restricted_subformulas_R_μ:
"subformulas⇩μ ψ ⊆ restricted_subformulas (φ R⇩n ψ)"
by (induction ψ) auto

lemma restrict_af_letter:
"restricted_subformulas (af_letter φ σ) = restricted_subformulas φ"
proof (induction φ)
case (Release_ltln φ1 φ2)
then show ?case
using restricted_subformulas_subset' by simp blast
next
case (WeakUntil_ltln φ1 φ2)
then show ?case
using restricted_subformulas_subset' by simp blast
qed auto

lemma restrict_af:
"restricted_subformulas (af φ w) = restricted_subformulas φ"
by (induction w rule: rev_induct) (auto simp: restrict_af_letter)

subsection ‹Restricted Master Theorem / Lemmas›

lemma delay_2:
assumes "μ_stable φ w"
assumes "w ⊨⇩n φ"
shows "∃i. suffix i w ⊨⇩n af φ (prefix i w)[{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ]⇩ν"
using assms
proof (induction φ arbitrary: w)
case (Prop_ltln x)
then show ?case
next
case (Nprop_ltln x)
then show ?case
next
case (And_ltln φ1 φ2)

let ?X  = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas (φ1 and⇩n φ2)"
let ?X1 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ1"
let ?X2 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ2"

have "?X1 ⊆ ?X" and "?X2 ⊆ ?X"
by auto

moreover

obtain i j where "suffix i w ⊨⇩n af φ1 (prefix i w)[?X1]⇩ν"
and "suffix j w ⊨⇩n af φ2 (prefix j w)[?X2]⇩ν"
using μ_stable_subfrmlsn[OF ‹μ_stable (φ1 and⇩n φ2) w›] And_ltln by fastforce

ultimately

obtain k where "suffix k w ⊨⇩n af φ1 (prefix k w)[?X]⇩ν"
and "suffix k w ⊨⇩n af φ2 (prefix k w)[?X]⇩ν"

thus ?case
unfolding af_decompose semantics_ltln.simps(5) GF_advice.simps by blast
next
case (Or_ltln φ1 φ2)
let ?X  = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas (φ1 and⇩n φ2)"
let ?X1 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ1"
let ?X2 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ2"

have "?X1 ⊆ ?X" and "?X2 ⊆ ?X"
by auto

moreover

obtain i j where "suffix i w ⊨⇩n af φ1 (prefix i w)[?X1]⇩ν ∨ suffix j w ⊨⇩n af φ2 (prefix j w)[?X2]⇩ν"
using μ_stable_subfrmlsn[OF ‹μ_stable (φ1 or⇩n φ2) w›] Or_ltln by fastforce

ultimately

obtain k where "suffix k w ⊨⇩n af φ1 (prefix k w)[?X]⇩ν ∨ suffix k w ⊨⇩n af φ2 (prefix k w)[?X]⇩ν"

thus ?case
unfolding af_decompose semantics_ltln.simps(6) GF_advice.simps by auto
next
case (Next_ltln φ)
then have stable: "μ_stable φ (suffix 1 w)"
and suffix: "suffix 1 w ⊨⇩n φ"
using ℱ_suffix 𝒢ℱ_ℱ_subset 𝒢ℱ_suffix
show ?case
by (metis (no_types, lifting) Next_ltln.IH[OF stable suffix, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] One_nat_def add.commute af_simps(3) foldl_Nil foldl_append restricted_subformulas.simps(3) subsequence_append subsequence_singleton)
next
case (Until_ltln φ1 φ2)
let ?X  = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas (φ1 U⇩n φ2)"
let ?X1 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ1"
let ?X2 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ2"

have stable_1: "⋀i. μ_stable φ1 (suffix i w)"
and stable_2: "⋀i. μ_stable φ2 (suffix i w)"
using μ_stable_subfrmlsn[OF Until_ltln.prems(1)] by (simp add: μ_stable_suffix)+

obtain i where "⋀j. j < i ⟹ suffix j w ⊨⇩n φ1" and "suffix i w ⊨⇩n φ2"
using Until_ltln by auto

then have "⋀j. j < i ⟹ ∃k. suffix (j + k) w ⊨⇩n af φ1 (w [j → k + j])[?X1]⇩ν"
and "∃k. suffix (i + k) w ⊨⇩n af φ2 (w [i → k + i])[?X2]⇩ν"
using Until_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
using Until_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
by blast+

moreover

have "?X1 ⊆ ?X"
and "?X2 ⊆ ?X"
by auto

ultimately

obtain k where "k ≥ i"
and "suffix k w ⊨⇩n af φ2 (w [i → k])[?X]⇩ν"
and "⋀j. j < i ⟹ suffix k w ⊨⇩n af φ1 (w [j → k])[?X]⇩ν"
using GF_advice_sync_less[of i w φ1 ?X φ2] GF_advice_monotone[of _ ?X] by meson

hence "suffix (Suc k) w ⊨⇩n af (φ1 U⇩n φ2) (prefix (Suc k) w)[?X]⇩ν"

then show ?case
by blast
next
case (WeakUntil_ltln φ1 φ2)

let ?X  = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas (φ1 W⇩n φ2)"
let ?X1 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ1"
let ?X2 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ2"

have stable_1: "⋀i. μ_stable φ1 (suffix i w)"
and stable_2: "⋀i. μ_stable φ2 (suffix i w)"
using μ_stable_subfrmlsn[OF WeakUntil_ltln.prems(1)] by (simp add: μ_stable_suffix)+

{
assume Until_ltln: "w ⊨⇩n φ1 U⇩n φ2"
then obtain i where "⋀j. j < i ⟹ suffix j w ⊨⇩n φ1" and "suffix i w ⊨⇩n φ2"
by auto

then have "⋀j. j < i ⟹ ∃k. suffix (j + k) w ⊨⇩n af φ1 (w [j → k + j])[?X1]⇩ν"
and "∃k. suffix (i + k) w ⊨⇩n af φ2 (w [i → k + i])[?X2]⇩ν"
using WeakUntil_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
using WeakUntil_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
by blast+

moreover

have "?X1 ⊆ ?X"
and "?X2 ⊆ ?X"
using restricted_subformulas_subset' by force+

ultimately

obtain k where "k ≥ i"
and "suffix k w ⊨⇩n af φ2 (w [i → k])[?X]⇩ν"
and "⋀j. j < i ⟹ suffix k w ⊨⇩n af φ1 (w [j → k])[?X]⇩ν"
using GF_advice_sync_less[of i w φ1 ?X φ2] GF_advice_monotone[of _ ?X] by meson

hence "suffix (Suc k) w ⊨⇩n af (φ1 W⇩n φ2) (prefix (Suc k) w)[?X]⇩ν"
hence ?case
by blast
}
moreover
{
assume Globally_ltln: "w ⊨⇩n G⇩n φ1"

{
fix j
have "suffix j w ⊨⇩n φ1"
using Globally_ltln by simp
then have "suffix j w ⊨⇩n φ1[{ψ. w ⊨⇩n G⇩n (F⇩n ψ)}]⇩ν"
by (metis stable_1 GF_advice_a1 𝒢ℱ_suffix μ_stable_def 𝒢ℱ_elim mem_Collect_eq subsetI)
then have "suffix j w ⊨⇩n φ1[?X]⇩ν"
}

then have "w ⊨⇩n (φ1 W⇩n φ2)[?X]⇩ν"
by simp
then have ?case
}
ultimately
show ?case
using WeakUntil_ltln.prems(2) ltln_weak_to_strong(1) by blast
next
case (Release_ltln φ1 φ2)

let ?X  = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas (φ1 R⇩n φ2)"
let ?X1 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ1"
let ?X2 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ2"

have stable_1: "⋀i. μ_stable φ1 (suffix i w)"
and stable_2: "⋀i. μ_stable φ2 (suffix i w)"
using μ_stable_subfrmlsn[OF Release_ltln.prems(1)] by (simp add: μ_stable_suffix)+

{
assume Until_ltln: "w ⊨⇩n φ1 M⇩n φ2"
then obtain i where "⋀j. j ≤ i ⟹ suffix j w ⊨⇩n φ2" and "suffix i w ⊨⇩n φ1"
by auto

then have "⋀j. j ≤ i ⟹ ∃k. suffix (j + k) w ⊨⇩n af φ2 (w [j → k + j])[?X2]⇩ν"
and "∃k. suffix (i + k) w ⊨⇩n af φ1 (w [i → k + i])[?X1]⇩ν"
using Release_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
using Release_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
by blast+

moreover

have "?X1 ⊆ ?X"
and "?X2 ⊆ ?X"
using restricted_subformulas_subset' by force+

ultimately

obtain k where "k ≥ i"
and "suffix k w ⊨⇩n af φ1 (w [i → k])[?X]⇩ν"
and "⋀j. j ≤ i ⟹ suffix k w ⊨⇩n af φ2 (w [j → k])[?X]⇩ν"
using GF_advice_sync_lesseq[of i w φ2 ?X φ1] GF_advice_monotone[of _ ?X] by meson

hence "suffix (Suc k) w ⊨⇩n af (φ1 R⇩n φ2) (prefix (Suc k) w)[?X]⇩ν"
hence ?case
by blast
}
moreover
{
assume Globally_ltln: "w ⊨⇩n G⇩n φ2"

{
fix j
have "suffix j w ⊨⇩n φ2"
using Globally_ltln by simp
then have "suffix j w ⊨⇩n φ2[{ψ. w ⊨⇩n G⇩n (F⇩n ψ)}]⇩ν"
by (metis stable_2 GF_advice_a1 𝒢ℱ_suffix μ_stable_def 𝒢ℱ_elim mem_Collect_eq subsetI)
then have "suffix j w ⊨⇩n φ2[?X]⇩ν"
}

then have "w ⊨⇩n (φ1 R⇩n φ2)[?X]⇩ν"
by simp
then have ?case
}
ultimately
show ?case
using Release_ltln.prems(2) ltln_weak_to_strong(3) by blast
next
case (StrongRelease_ltln φ1 φ2)

let ?X  = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas (φ1 M⇩n φ2)"
let ?X1 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ1"
let ?X2 = "{ψ. w ⊨⇩n G⇩n (F⇩n ψ)} ∩ restricted_subformulas φ2"

have stable_1: "⋀i. μ_stable φ1 (suffix i w)"
and stable_2: "⋀i. μ_stable φ2 (suffix i w)"
using μ_stable_subfrmlsn[OF StrongRelease_ltln.prems(1)] by (simp add: μ_stable_suffix)+

obtain i where "⋀j. j ≤ i ⟹ suffix j w ⊨⇩n φ2" and "suffix i w ⊨⇩n φ1"
using StrongRelease_ltln by auto

then have "⋀j. j ≤ i ⟹ ∃k. suffix (j + k) w ⊨⇩n af φ2 (w [j → k + j])[?X2]⇩ν"
and "∃k. suffix (i + k) w ⊨⇩n af φ1 (w [i → k + i])[?X1]⇩ν"
using StrongRelease_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
using StrongRelease_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
by blast+

moreover

have "?X1 ⊆ ?X"
and "?X2 ⊆ ?X"
by auto

ultimately

obtain k where "k ≥ i"
and "suffix k w ⊨⇩n af φ1 (w [i → k])[?X]⇩ν"
and "⋀j. j ≤ i ⟹ suffix k w ⊨⇩n af φ2 (w [j → k])[?X]⇩ν"
using GF_advice_sync_lesseq[of i w φ2 ?X φ1] GF_advice_monotone[of _ ?X] by meson

hence "suffix (Suc k) w ⊨⇩n af (φ1 M⇩n φ2) (prefix (Suc k) w)[?X]⇩ν"

then show ?case
by blast
qed simp+

theorem master_theorem_restricted:
"w ⊨⇩n φ ⟷
(∃X ⊆ subformulas⇩μ φ ∩ restricted_subformulas φ.
(∃Y ⊆ subformulas⇩ν φ ∩ restricted_subformulas φ.
(∃i. (suffix i w ⊨⇩n af φ (prefix i w)[X]⇩ν)
∧ (∀ψ ∈ X. w ⊨⇩n G⇩n (F⇩n ψ[Y]⇩μ))
∧ (∀ψ ∈ Y. w ⊨⇩n F⇩n (G⇩n ψ[X]⇩ν)))))"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs

obtain i where "μ_stable φ (suffix i w)"
by (metis MOST_nat less_Suc_eq suffix_μ_stable)

hence stable: "μ_stable (af φ (prefix i w)) (suffix i w)"
by (simp add: ℱ_af 𝒢ℱ_af μ_stable_def)

let ?φ' = "af φ (prefix i w)"
let ?X' = "𝒢ℱ φ w ∩ restricted_subformulas φ"
let ?Y' = "ℱ𝒢 φ w ∩ restricted_subformulas φ"

have 1: "suffix i w ⊨⇩n ?φ'"
using ‹?lhs› af_ltl_continuation by force

have 2: "⋀j. af (af φ (prefix i w)) (prefix j (suffix i w)) = af φ (prefix (i + j) w)"

have 3: "𝒢ℱ φ w = 𝒢ℱ φ (suffix i w)"
using 𝒢ℱ_af 𝒢ℱ_suffix by blast

have "∃j. suffix (i + j) w ⊨⇩n af (?φ') (prefix j (suffix i w))[?X']⇩ν"
using delay_2[OF stable 1] unfolding suffix_suffix 2 restrict_af 3 unfolding 𝒢ℱ_semantics'
by (metis (no_types, lifting) GF_advice_inter_subformulas af_subformulas⇩μ inf_assoc inf_commute)

hence "∃i. suffix i w ⊨⇩n af φ (prefix i w)[?X']⇩ν"
using 2 by auto

moreover

{
fix ψ
have "⋀X. ψ ∈ restricted_subformulas φ ⟹ ψ[X ∩ restricted_subformulas φ]⇩μ = ψ[X]⇩μ"
by (metis le_supE restricted_subformulas_superset FG_advice_inter inf.coboundedI2)
hence "ψ ∈ ?X' ⟹  w ⊨⇩n G⇩n (F⇩n ψ[?Y']⇩μ)"
using 𝒢ℱ_implies_GF by force
}

moreover

{
fix ψ
have "⋀X. ψ ∈ restricted_subformulas φ ⟹ ψ[X ∩ restricted_subformulas φ]⇩ν = ψ[X]⇩ν"
by (metis le_supE restricted_subformulas_superset GF_advice_inter inf.coboundedI2)
hence "ψ ∈ ?Y' ⟹ w ⊨⇩n F⇩n (G⇩n ψ[?X']⇩ν)"
using ℱ𝒢_implies_FG by force
}

moreover

have "?X' ⊆ subformulas⇩μ φ ∩ restricted_subformulas φ"
using 𝒢ℱ_subformulas⇩μ by blast

moreover

have "?Y' ⊆ subformulas⇩ν φ ∩ restricted_subformulas φ"
using ℱ𝒢_subformulas⇩ν by blast

ultimately show ?rhs
by meson
qed (insert master_theorem, fast)

corollary master_theorem_restricted_language:
"language_ltln φ = ⋃ {L⇩1 φ X ∩ L⇩2 X Y ∩ L⇩3 X Y | X Y. X ⊆ subformulas⇩μ φ ∩ restricted_subformulas φ ∧ Y ⊆ subformulas⇩ν φ ∩ restricted_subformulas φ}"
proof safe
fix w
assume "w ∈ language_ltln φ"

then have "w ⊨⇩n φ"
unfolding language_ltln_def by simp

then obtain X Y where
1: "X ⊆ subformulas⇩μ φ ∩ restricted_subformulas φ"
and 2: "Y ⊆ subformulas⇩ν φ ∩ restricted_subformulas φ"
and "∃i. suffix i w ⊨⇩n af φ (prefix i w)[X]⇩ν"
and "∀ψ ∈ X. w ⊨⇩n G⇩n (F⇩n ψ[Y]⇩μ)"
and "∀ψ ∈ Y. w ⊨⇩n F⇩n (G⇩n ψ[X]⇩ν)"
using master_theorem_restricted by metis

then have "w ∈ L⇩1 φ X" and "w ∈ L⇩2 X Y" and "w ∈ L⇩3 X Y"
unfolding L⇩1_def L⇩2_def L⇩3_def by simp+

then show "w ∈ ⋃ {L⇩1 φ X ∩ L⇩2 X Y ∩ L⇩3 X Y | X Y. X ⊆ subformulas⇩μ φ ∩ restricted_subformulas φ ∧ Y ⊆ subformulas⇩ν φ ∩ restricted_subformulas φ}"
using 1 2 by blast
next
fix w X Y
assume "X ⊆ subformulas⇩μ φ ∩ restricted_subformulas φ" and "Y ⊆ subformulas⇩ν φ ∩ restricted_subformulas φ"
and "w ∈ L⇩1 φ X" and "w ∈ L⇩2 X Y" and "w ∈ L⇩3 X Y"

then show "w ∈ language_ltln φ"
unfolding language_ltln_def L⇩1_def L⇩2_def L⇩3_def
using master_theorem_restricted by blast
qed

subsection ‹Definitions with Lists for Code Export›

definition restricted_advice_sets :: "'a ltln ⇒ ('a ltln list × 'a ltln list) list"
where
"restricted_advice_sets φ = List.product (subseqs (List.filter (λx. x ∈ restricted_subformulas φ) (subformulas⇩μ_list φ))) (subseqs (List.filter (λx. x ∈ restricted_subformulas φ) (subformulas⇩ν_list φ)))"

lemma subseqs_subformulas⇩μ_restricted_list:
"X ⊆ subformulas⇩μ φ ∩ restricted_subformulas φ ⟷ (∃xs. X = set xs ∧ xs ∈ set (subseqs (List.filter (λx. x ∈ restricted_subformulas φ) (subformulas⇩μ_list φ))))"
by (metis in_set_subseqs inf_commute inter_set_filter subformulas⇩μ_list_set subset_subseq)

lemma subseqs_subformulas⇩ν_restricted_list:
"Y ⊆ subformulas⇩ν φ ∩ restricted_subformulas φ ⟷ (∃ys. Y = set ys ∧ ys ∈ set (subseqs (List.filter (λx. x ∈ restricted_subformulas φ) (subformulas⇩ν_list φ))))"
by (metis in_set_subseqs inf_commute inter_set_filter subformulas⇩ν_list_set subset_subseq)