diff --git a/thys/LTL_Master_Theorem/Code_Export.thy b/thys/LTL_Master_Theorem/Code_Export.thy
--- a/thys/LTL_Master_Theorem/Code_Export.thy
+++ b/thys/LTL_Master_Theorem/Code_Export.thy
@@ -1,68 +1,78 @@
 (*
     Author:   Benedikt Seidl
     License:  BSD
 *)
 
 section \<open>Code export to Standard ML\<close>
 
 theory Code_Export
 imports
-  "LTL_to_DRA/DRA_Implementation"
+  "LTL_to_DRA/DRA_Instantiation"
   LTL.Code_Equations
   "HOL-Library.Code_Target_Numeral"
 begin
 
 subsection \<open>Hashing Sets\<close>
 
 global_interpretation comp_fun_commute "plus o cube o hashcode :: ('a :: hashable) \<Rightarrow> hashcode \<Rightarrow> hashcode"
   by unfold_locales (auto simp: cube_def)
 
 lemma [code]:
   "hashcode (set xs) = fold (plus o cube o hashcode) (remdups xs) (uint32_of_nat (length (remdups xs)))"
   by (simp add: fold_set_fold_remdups length_remdups_card_conv)
 
 lemma [code]:
   "hashcode (abs_ltln\<^sub>P \<phi>) = hashcode (min_dnf \<phi>)"
   by simp
 
+lemma min_dnf_rep_abs[simp]:
+  "min_dnf (Unf (rep_ltln\<^sub>Q (abs_ltln\<^sub>Q \<phi>))) = min_dnf (Unf \<phi>)"
+  using Quotient3_ltln\<^sub>Q ltl_prop_equiv_min_dnf ltl_prop_unfold_equiv_def rep_abs_rsp by fastforce
+
+lemma [code]:
+  "hashcode (abs_ltln\<^sub>Q \<phi>) = hashcode (min_dnf (Unf \<phi>))"
+  by simp
+
 
 subsection \<open>LTL to DRA\<close>
 
-export_code ltlc_to_draei checking
+declare ltl_to_dra\<^sub>P.af_letter\<^sub>F_lifted_semantics [code]
+declare ltl_to_dra\<^sub>P.af_letter\<^sub>G_lifted_semantics [code]
+declare ltl_to_dra\<^sub>P.af_letter\<^sub>\<nu>_lifted_semantics [code]
 
-declare ltl_to_dra.af_letter\<^sub>F_lifted_semantics [code]
-declare ltl_to_dra.af_letter\<^sub>G_lifted_semantics [code]
-declare ltl_to_dra.af_letter\<^sub>\<nu>_lifted_semantics [code]
+declare ltl_to_dra\<^sub>Q.af_letter\<^sub>F_lifted_semantics [code]
+declare ltl_to_dra\<^sub>Q.af_letter\<^sub>G_lifted_semantics [code]
+declare ltl_to_dra\<^sub>Q.af_letter\<^sub>\<nu>_lifted_semantics [code]
 
 definition atoms_ltlc_list_literals :: "String.literal ltlc \<Rightarrow> String.literal list"
 where
   "atoms_ltlc_list_literals = atoms_ltlc_list"
 
-definition ltlc_to_draei_literals :: "String.literal ltlc \<Rightarrow> (String.literal set, nat) draei"
+definition ltlc_to_draei_literals :: "equiv \<Rightarrow> String.literal ltlc \<Rightarrow> (String.literal set, nat) draei"
 where
   "ltlc_to_draei_literals = ltlc_to_draei"
 
 definition sort_transitions :: "(nat \<times> String.literal set \<times> nat) list \<Rightarrow> (nat \<times> String.literal set \<times> nat) list"
 where
   "sort_transitions = sort_key fst"
 
-export_code True_ltlc Iff_ltlc ltlc_to_draei_literals
+export_code True_ltlc Iff_ltlc ltlc_to_draei_literals Prop PropUnfold
   alphabetei initialei transitionei conditionei
   integer_of_nat atoms_ltlc_list_literals sort_transitions set
   in SML module_name LTL file_prefix LTL_to_DRA
 
 
 
 subsection \<open>LTL to NBA\<close>
 
 (* TODO *)
 
 
 
 subsection \<open>LTL to LDBA\<close>
 
 (* TODO *)
 
 
 
 end
diff --git a/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy b/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy
--- a/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy
+++ b/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy
@@ -1,436 +1,906 @@
 (*
     Author:   Benedikt Seidl
     License:  BSD
 *)
 
 section \<open>Constructing DRAs for LTL Formulas\<close>
 
 theory DRA_Construction
   imports
     Transition_Functions
 
     "../Quotient_Type"
     "../Omega_Words_Fun_Stream"
 
+    "HOL-Library.Log_Nat"
+
     "../Logical_Characterization/Master_Theorem"
+    "../Logical_Characterization/Restricted_Master_Theorem"
 
     Transition_Systems_and_Automata.DBA_Combine
     Transition_Systems_and_Automata.DCA_Combine
     Transition_Systems_and_Automata.DRA_Combine
 begin
 
 \<comment> \<open>We use prefix and suffix on infinite words.\<close>
 hide_const Sublist.prefix Sublist.suffix
 
-locale dra_construction = transition_functions eq + quotient eq Rep Abs
+locale dra_construction = transition_functions eq normalise + quotient eq Rep Abs
   for
     eq :: "'a ltln \<Rightarrow> 'a ltln \<Rightarrow> bool" (infix "\<sim>" 75)
   and
+    normalise :: "'a ltln \<Rightarrow> 'a ltln"
+  and
     Rep :: "'ltlq \<Rightarrow> 'a ltln"
   and
     Abs :: "'a ltln \<Rightarrow> 'ltlq"
 begin
 
 subsection \<open>Lifting Setup\<close>
 
 abbreviation true\<^sub>n_lifted :: "'ltlq" ("\<up>true\<^sub>n") where
   "\<up>true\<^sub>n \<equiv> Abs true\<^sub>n"
 
 abbreviation false\<^sub>n_lifted :: "'ltlq" ("\<up>false\<^sub>n") where
   "\<up>false\<^sub>n \<equiv> Abs false\<^sub>n"
 
 abbreviation af_letter_lifted :: "'a set \<Rightarrow> 'ltlq \<Rightarrow> 'ltlq" ("\<up>afletter") where
   "\<up>afletter \<nu> \<phi> \<equiv> Abs (af_letter (Rep \<phi>) \<nu>)"
 
 abbreviation af_lifted :: "'ltlq \<Rightarrow> 'a set list \<Rightarrow> 'ltlq" ("\<up>af") where
   "\<up>af \<phi> w \<equiv> fold \<up>afletter w \<phi>"
 
 abbreviation GF_advice_lifted :: "'ltlq \<Rightarrow> 'a ltln set \<Rightarrow> 'ltlq" ("_\<up>[_]\<^sub>\<nu>" [90,60] 89) where
   "\<phi>\<up>[X]\<^sub>\<nu> \<equiv> Abs ((Rep \<phi>)[X]\<^sub>\<nu>)"
 
 
 lemma af_letter_lifted_semantics:
   "\<up>afletter \<nu> (Abs \<phi>) = Abs (af_letter \<phi> \<nu>)"
   by (metis Rep_Abs_eq af_letter_congruent Abs_eq)
 
 lemma af_lifted_semantics:
   "\<up>af (Abs \<phi>) w = Abs (af \<phi> w)"
   by (induction w rule: rev_induct) (auto simp: Abs_eq, insert Rep_Abs_eq af_letter_congruent eq_sym, blast)
 
 lemma af_lifted_range:
   "range (\<up>af (Abs \<phi>)) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
   using af_lifted_semantics af_nested_prop_atoms by blast
 
 
 definition af_letter\<^sub>F_lifted :: "'a ltln \<Rightarrow> 'a set \<Rightarrow> 'ltlq \<Rightarrow> 'ltlq" ("\<up>afletter\<^sub>F")
 where
   "\<up>afletter\<^sub>F \<phi> \<nu> \<psi> \<equiv> Abs (af_letter\<^sub>F \<phi> (Rep \<psi>) \<nu>)"
 
 definition af_letter\<^sub>G_lifted :: "'a ltln \<Rightarrow> 'a set \<Rightarrow> 'ltlq \<Rightarrow> 'ltlq" ("\<up>afletter\<^sub>G")
 where
   "\<up>afletter\<^sub>G \<phi> \<nu> \<psi> \<equiv> Abs (af_letter\<^sub>G \<phi> (Rep \<psi>) \<nu>)"
 
 lemma af_letter\<^sub>F_lifted_semantics:
   "\<up>afletter\<^sub>F \<phi> \<nu> (Abs \<psi>) = Abs (af_letter\<^sub>F \<phi> \<psi> \<nu>)"
   by (metis af_letter\<^sub>F_lifted_def Rep_inverse af_letter\<^sub>F_def af_letter_congruent Abs_eq)
 
 lemma af_letter\<^sub>G_lifted_semantics:
   "\<up>afletter\<^sub>G \<phi> \<nu> (Abs \<psi>) = Abs (af_letter\<^sub>G \<phi> \<psi> \<nu>)"
   by (metis af_letter\<^sub>G_lifted_def Rep_inverse af_letter\<^sub>G_def af_letter_congruent Abs_eq)
 
 abbreviation af\<^sub>F_lifted :: "'a ltln \<Rightarrow> 'ltlq \<Rightarrow> 'a set list \<Rightarrow> 'ltlq" ("\<up>af\<^sub>F")
 where
   "\<up>af\<^sub>F \<phi> \<psi> w \<equiv> fold (\<up>afletter\<^sub>F \<phi>) w \<psi>"
 
 abbreviation af\<^sub>G_lifted :: "'a ltln \<Rightarrow> 'ltlq \<Rightarrow> 'a set list \<Rightarrow> 'ltlq" ("\<up>af\<^sub>G")
 where
   "\<up>af\<^sub>G \<phi> \<psi> w \<equiv> fold (\<up>afletter\<^sub>G \<phi>) w \<psi>"
 
 lemma af\<^sub>F_lifted_semantics:
   "\<up>af\<^sub>F \<phi> (Abs \<psi>) w = Abs (af\<^sub>F \<phi> \<psi> w)"
   by (induction w rule: rev_induct) (auto simp: af_letter\<^sub>F_lifted_semantics)
 
 lemma af\<^sub>G_lifted_semantics:
   "\<up>af\<^sub>G \<phi> (Abs \<psi>) w = Abs (af\<^sub>G \<phi> \<psi> w)"
   by (induction w rule: rev_induct) (auto simp: af_letter\<^sub>G_lifted_semantics)
 
-lemma af\<^sub>F_lifted_range:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> range (\<up>af\<^sub>F \<phi> (Abs \<psi>)) \<subseteq>  {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
-  using af\<^sub>F_lifted_semantics af\<^sub>F_nested_prop_atoms by blast
-
-lemma af\<^sub>G_lifted_range:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> range (\<up>af\<^sub>G \<phi> (Abs \<psi>)) \<subseteq>  {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
-  using af\<^sub>G_lifted_semantics af\<^sub>G_nested_prop_atoms by blast
-
 
 definition af_letter\<^sub>\<nu>_lifted :: "'a ltln set \<Rightarrow> 'a set \<Rightarrow> 'ltlq \<times> 'ltlq \<Rightarrow> 'ltlq \<times> 'ltlq" ("\<up>afletter\<^sub>\<nu>")
 where
   "\<up>afletter\<^sub>\<nu> X \<nu> p \<equiv>
     (Abs (fst (af_letter\<^sub>\<nu> X (Rep (fst p), Rep (snd p)) \<nu>)),
      Abs (snd (af_letter\<^sub>\<nu> X (Rep (fst p), Rep (snd p)) \<nu>)))"
 
 abbreviation af\<^sub>\<nu>_lifted :: "'a ltln set \<Rightarrow> 'ltlq \<times> 'ltlq \<Rightarrow> 'a set list \<Rightarrow> 'ltlq \<times> 'ltlq" ("\<up>af\<^sub>\<nu>")
 where
   "\<up>af\<^sub>\<nu> X p w \<equiv> fold (\<up>afletter\<^sub>\<nu> X) w p"
 
 lemma af_letter\<^sub>\<nu>_lifted_semantics:
   "\<up>afletter\<^sub>\<nu> X \<nu> (Abs x, Abs y) = (Abs (fst (af_letter\<^sub>\<nu> X (x, y) \<nu>)), Abs (snd (af_letter\<^sub>\<nu> X (x, y) \<nu>)))"
   by (simp add: af_letter\<^sub>\<nu>_def af_letter\<^sub>\<nu>_lifted_def) (insert GF_advice_congruent Rep_Abs_eq Rep_inverse af_letter_lifted_semantics eq_trans Abs_eq, blast)
 
 lemma af\<^sub>\<nu>_lifted_semantics:
   "\<up>af\<^sub>\<nu> X (Abs \<xi>, Abs \<zeta>) w = (Abs (fst (af\<^sub>\<nu> X (\<xi>, \<zeta>) w)), Abs (snd (af\<^sub>\<nu> X (\<xi>, \<zeta>) w)))"
   apply (induction w rule: rev_induct) 
    apply (auto simp: af_letter\<^sub>\<nu>_lifted_def af_letter\<^sub>\<nu>_lifted_semantics af_letter_lifted_semantics)
   by (metis (no_types, hide_lams) af_letter\<^sub>\<nu>_lifted_def af\<^sub>\<nu>_fst af_letter\<^sub>\<nu>_lifted_semantics eq_fst_iff prod.sel(2))
 
 
 
 subsection \<open>Büchi automata for basic languages\<close>
 
 definition \<AA>\<^sub>\<mu> :: "'a ltln \<Rightarrow> ('a set, 'ltlq) dba" where
   "\<AA>\<^sub>\<mu> \<phi> = dba UNIV (Abs \<phi>) \<up>afletter (\<lambda>\<psi>. \<psi> = \<up>true\<^sub>n)"
 
 definition \<AA>\<^sub>\<mu>_GF :: "'a ltln \<Rightarrow> ('a set, 'ltlq) dba" where
   "\<AA>\<^sub>\<mu>_GF \<phi> = dba UNIV (Abs (F\<^sub>n \<phi>)) (\<up>afletter\<^sub>F \<phi>) (\<lambda>\<psi>. \<psi> = \<up>true\<^sub>n)"
 
 definition \<AA>\<^sub>\<nu> :: "'a ltln \<Rightarrow> ('a set, 'ltlq) dca" where
   "\<AA>\<^sub>\<nu> \<phi> = dca UNIV (Abs \<phi>) \<up>afletter (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n)"
 
 definition \<AA>\<^sub>\<nu>_FG :: "'a ltln \<Rightarrow> ('a set, 'ltlq) dca" where
   "\<AA>\<^sub>\<nu>_FG \<phi> = dca UNIV (Abs (G\<^sub>n \<phi>)) (\<up>afletter\<^sub>G \<phi>) (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n)"
 
 
 lemma dba_run:
   "DBA.run (dba UNIV p \<delta> \<alpha>) (to_stream w) p" unfolding dba.run_alt_def by simp
 
 lemma dca_run:
   "DCA.run (dca UNIV p \<delta> \<alpha>) (to_stream w) p" unfolding dca.run_alt_def by simp
 
 
 lemma \<AA>\<^sub>\<mu>_language:
   "\<phi> \<in> \<mu>LTL \<Longrightarrow> to_stream w \<in> DBA.language (\<AA>\<^sub>\<mu> \<phi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
 proof -
   assume "\<phi> \<in> \<mu>LTL"
 
   then have "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> (\<forall>n. \<exists>k\<ge>n. af \<phi> (w[0 \<rightarrow> k]) \<sim> true\<^sub>n)"
     by (meson af_\<mu>LTL af_prefix_true le_cases)
 
   also have "\<dots> \<longleftrightarrow> (\<forall>n. \<exists>k\<ge>n. af \<phi> (w[0 \<rightarrow> Suc k]) \<sim> true\<^sub>n)"
     by (meson af_prefix_true le_SucI order_refl)
 
   also have "\<dots> \<longleftrightarrow> infs (\<lambda>\<psi>. \<psi> = \<up>true\<^sub>n) (DBA.trace (\<AA>\<^sub>\<mu> \<phi>) (to_stream w) (Abs \<phi>))"
     by (simp add: infs_snth \<AA>\<^sub>\<mu>_def DBA.transition_def af_lifted_semantics Abs_eq[symmetric] af_letter_lifted_semantics)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DBA.language (\<AA>\<^sub>\<mu> \<phi>)"
     unfolding \<AA>\<^sub>\<mu>_def dba.initial_def dba.accepting_def by (auto simp: dba_run)
 
   finally show ?thesis
     by simp
 qed
 
 lemma \<AA>\<^sub>\<mu>_GF_language:
   "\<phi> \<in> \<mu>LTL \<Longrightarrow> to_stream w \<in> DBA.language (\<AA>\<^sub>\<mu>_GF \<phi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<phi>)"
 proof -
   assume "\<phi> \<in> \<mu>LTL"
 
   then have "w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<phi>) \<longleftrightarrow> (\<forall>n. \<exists>k. af (F\<^sub>n \<phi>) (w[n \<rightarrow> k]) \<sim>\<^sub>L true\<^sub>n)"
     using ltl_lang_equivalence.af_\<mu>LTL_GF by blast
 
   also have "\<dots> \<longleftrightarrow> (\<forall>n. \<exists>k>n. af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w[0 \<rightarrow> k]) \<sim> true\<^sub>n)"
     using af\<^sub>F_semantics_ltr af\<^sub>F_semantics_rtl
     using \<open>\<phi> \<in> \<mu>LTL\<close> af_\<mu>LTL_GF calculation by blast
 
   also have "\<dots> \<longleftrightarrow> (\<forall>n. \<exists>k\<ge>n. af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w[0 \<rightarrow> Suc k]) \<sim> true\<^sub>n)"
     by (metis less_Suc_eq_le less_imp_Suc_add)
 
   also have "\<dots> \<longleftrightarrow> infs (\<lambda>\<psi>. \<psi> = \<up>true\<^sub>n) (DBA.trace (\<AA>\<^sub>\<mu>_GF \<phi>) (to_stream w) (Abs (F\<^sub>n \<phi>)))"
     by (simp add: infs_snth \<AA>\<^sub>\<mu>_GF_def DBA.transition_def af\<^sub>F_lifted_semantics Abs_eq[symmetric] af_letter\<^sub>F_lifted_semantics)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DBA.language (\<AA>\<^sub>\<mu>_GF \<phi>)"
     unfolding \<AA>\<^sub>\<mu>_GF_def dba.initial_def dba.accepting_def by (auto simp: dba_run)
 
   finally show ?thesis
     by simp
 qed
 
 lemma \<AA>\<^sub>\<nu>_language:
   "\<phi> \<in> \<nu>LTL \<Longrightarrow> to_stream w \<in> DCA.language (\<AA>\<^sub>\<nu> \<phi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
 proof -
   assume "\<phi> \<in> \<nu>LTL"
 
   then have "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> (\<exists>n. \<forall>k\<ge>n. \<not> af \<phi> (w[0 \<rightarrow> k]) \<sim> false\<^sub>n)"
     by (meson af_\<nu>LTL af_prefix_false le_cases order_refl)
 
   also have "\<dots> \<longleftrightarrow> (\<exists>n. \<forall>k\<ge>n. \<not> af \<phi> (w[0 \<rightarrow> Suc k]) \<sim> false\<^sub>n)"
     by (meson af_prefix_false le_SucI order_refl)
 
   also have "\<dots> \<longleftrightarrow> fins (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n) (DCA.trace (\<AA>\<^sub>\<nu> \<phi>) (to_stream w) (Abs \<phi>))"
     by (simp add: infs_snth \<AA>\<^sub>\<nu>_def DBA.transition_def af_lifted_semantics Abs_eq[symmetric] af_letter_lifted_semantics)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DCA.language (\<AA>\<^sub>\<nu> \<phi>)"
     unfolding \<AA>\<^sub>\<nu>_def dca.initial_def dca.rejecting_def by (auto simp: dca_run)
 
   finally show ?thesis
     by simp
 qed
 
 lemma \<AA>\<^sub>\<nu>_FG_language:
   "\<phi> \<in> \<nu>LTL \<Longrightarrow> to_stream w \<in> DCA.language (\<AA>\<^sub>\<nu>_FG \<phi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<phi>)"
 proof -
   assume "\<phi> \<in> \<nu>LTL"
 
   then have "w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<phi>) \<longleftrightarrow> (\<exists>k. \<forall>j. \<not> af (G\<^sub>n \<phi>) (w[k \<rightarrow> j]) \<sim>\<^sub>L false\<^sub>n)"
     using ltl_lang_equivalence.af_\<nu>LTL_FG by blast
 
   also have "\<dots> \<longleftrightarrow> (\<exists>n. \<forall>k>n. \<not> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w[0 \<rightarrow> k]) \<sim> false\<^sub>n)"
     using af\<^sub>G_semantics_ltr af\<^sub>G_semantics_rtl
     using \<open>\<phi> \<in> \<nu>LTL\<close> af_\<nu>LTL_FG calculation by blast
 
   also have "\<dots> \<longleftrightarrow> (\<exists>n. \<forall>k\<ge>n. \<not> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w[0 \<rightarrow> Suc k]) \<sim> false\<^sub>n)"
     by (metis less_Suc_eq_le less_imp_Suc_add)
 
   also have "\<dots> \<longleftrightarrow> fins (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n) (DCA.trace (\<AA>\<^sub>\<nu>_FG \<phi>) (to_stream w) (Abs (G\<^sub>n \<phi>)))"
     by (simp add: infs_snth \<AA>\<^sub>\<nu>_FG_def DBA.transition_def af\<^sub>G_lifted_semantics Abs_eq[symmetric] af_letter\<^sub>G_lifted_semantics)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DCA.language (\<AA>\<^sub>\<nu>_FG \<phi>)"
     unfolding \<AA>\<^sub>\<nu>_FG_def dca.initial_def dca.rejecting_def by (auto simp: dca_run)
 
   finally show ?thesis
     by simp
 qed
 
 
-lemma \<AA>\<^sub>\<mu>_nodes:
-  "DBA.nodes (\<AA>\<^sub>\<mu> \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
-  unfolding \<AA>\<^sub>\<mu>_def
-  using af_lifted_semantics af_nested_prop_atoms by fastforce
-
-lemma \<AA>\<^sub>\<mu>_GF_nodes:
-  "DBA.nodes (\<AA>\<^sub>\<mu>_GF \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
-  unfolding \<AA>\<^sub>\<mu>_GF_def dba.nodes_alt_def dba.reachable_alt_def
-  using af\<^sub>F_nested_prop_atoms[of "F\<^sub>n \<phi>"] by (auto simp: af\<^sub>F_lifted_semantics)
-
-lemma \<AA>\<^sub>\<nu>_nodes:
-  "DCA.nodes (\<AA>\<^sub>\<nu> \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
-  unfolding \<AA>\<^sub>\<nu>_def
-  using af_lifted_semantics af_nested_prop_atoms by fastforce
-
-lemma \<AA>\<^sub>\<nu>_FG_nodes:
-  "DCA.nodes (\<AA>\<^sub>\<nu>_FG \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
-  unfolding \<AA>\<^sub>\<nu>_FG_def dca.nodes_alt_def dca.reachable_alt_def
-  using af\<^sub>G_nested_prop_atoms[of "G\<^sub>n \<phi>"] by (auto simp: af\<^sub>G_lifted_semantics)
-
-
-
 subsection \<open>A DCA checking the GF-advice Function\<close>
 
 definition \<CC> :: "'a ltln \<Rightarrow> 'a ltln set \<Rightarrow> ('a set, 'ltlq \<times> 'ltlq) dca" where
-  "\<CC> \<phi> X = dca UNIV (Abs \<phi>, Abs (\<phi>[X]\<^sub>\<nu>)) (\<up>afletter\<^sub>\<nu> X) (\<lambda>p. snd p = \<up>false\<^sub>n)"
+  "\<CC> \<phi> X = dca UNIV (Abs \<phi>, Abs ((normalise \<phi>)[X]\<^sub>\<nu>)) (\<up>afletter\<^sub>\<nu> X) (\<lambda>p. snd p = \<up>false\<^sub>n)"
 
 lemma \<CC>_language:
   "to_stream w \<in> DCA.language (\<CC> \<phi> X) \<longleftrightarrow> (\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>)"
 proof -
 
   have "(\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>)
-        \<longleftrightarrow> (\<exists>m. \<forall>k\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n)"
+        \<longleftrightarrow> (\<exists>m. \<forall>k\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n)"
     using af\<^sub>\<nu>_semantics_ltr af\<^sub>\<nu>_semantics_rtl by blast
 
-  also have "\<dots> \<longleftrightarrow> fins (\<lambda>p. snd p = \<up>false\<^sub>n) (DCA.trace (\<CC> \<phi> X) (to_stream w) (Abs \<phi>, Abs (\<phi>[X]\<^sub>\<nu>)))"
+  also have "\<dots> \<longleftrightarrow> fins (\<lambda>p. snd p = \<up>false\<^sub>n) (DCA.trace (\<CC> \<phi> X) (to_stream w) (Abs \<phi>, Abs ((normalise \<phi>)[X]\<^sub>\<nu>)))"
     by(simp add: infs_snth \<CC>_def DCA.transition_def af\<^sub>\<nu>_lifted_semantics af_letter\<^sub>\<nu>_lifted_semantics Abs_eq)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DCA.language (\<CC> \<phi> X)"
     by (simp add: \<CC>_def dca.initial_def dca.rejecting_def dca.language_def dca_run)
 
   finally show ?thesis
     by blast
 qed
 
 
-lemma \<CC>_nodes:
-  "DCA.nodes (\<CC> \<phi> X) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>} \<times> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X}"
-  unfolding \<CC>_def dca.nodes_alt_def dca.reachable_alt_def
-  apply (auto simp add: af\<^sub>\<nu>_lifted_semantics af_letter\<^sub>\<nu>_lifted_semantics)
-  using af\<^sub>\<nu>_fst_nested_prop_atoms apply force
-  using GF_advice_nested_prop_atoms\<^sub>\<nu> af\<^sub>\<nu>_snd_nested_prop_atoms dra_construction_axioms by fastforce
-
-
-
 subsection \<open>A DRA for each combination of sets X and Y\<close>
 
 lemma dba_language:
   "(\<And>w. to_stream w \<in> DBA.language \<AA> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> DBA.language \<AA> = {w. to_omega w \<Turnstile>\<^sub>n \<phi>}"
   by (metis (mono_tags, lifting) Collect_cong dba.language_def mem_Collect_eq to_stream_to_omega)
 
 lemma dca_language:
   "(\<And>w. to_stream w \<in> DCA.language \<AA> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> DCA.language \<AA> = {w. to_omega w \<Turnstile>\<^sub>n \<phi>}"
   by (metis (mono_tags, lifting) Collect_cong dca.language_def mem_Collect_eq to_stream_to_omega)
 
 
 definition \<AA>\<^sub>1 :: "'a ltln \<Rightarrow> 'a ltln list \<Rightarrow> ('a set, 'ltlq \<times> 'ltlq) dca" where
   "\<AA>\<^sub>1 \<phi> xs = \<CC> \<phi> (set xs)"
 
 lemma \<AA>\<^sub>1_language:
   "to_omega ` DCA.language (\<AA>\<^sub>1 \<phi> xs) = L\<^sub>1 \<phi> (set xs)"
   by (simp add: \<AA>\<^sub>1_def L\<^sub>1_def set_eq_iff \<CC>_language)
 
 lemma \<AA>\<^sub>1_alphabet:
   "DCA.alphabet (\<AA>\<^sub>1 \<phi> xs) = UNIV"
   unfolding \<AA>\<^sub>1_def \<CC>_def by simp
 
 
 definition \<AA>\<^sub>2 :: "'a ltln list \<Rightarrow> 'a ltln list \<Rightarrow> ('a set, 'ltlq list degen) dba" where
   "\<AA>\<^sub>2 xs ys = DBA_Combine.intersect_list (map (\<lambda>\<psi>. \<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>)) xs)"
 
 lemma \<AA>\<^sub>2_language:
   "to_omega ` DBA.language (\<AA>\<^sub>2 xs ys) = L\<^sub>2 (set xs) (set ys)"
   by (simp add: \<AA>\<^sub>2_def L\<^sub>2_def set_eq_iff dba_language[OF \<AA>\<^sub>\<mu>_GF_language[OF FG_advice_\<mu>LTL(1)]])
 
 lemma \<AA>\<^sub>2_alphabet:
   "DBA.alphabet (\<AA>\<^sub>2 xs ys) = UNIV"
   by (simp add: \<AA>\<^sub>2_def \<AA>\<^sub>\<mu>_GF_def)
 
 
 definition \<AA>\<^sub>3 :: "'a ltln list \<Rightarrow> 'a ltln list \<Rightarrow> ('a set, 'ltlq list) dca" where
   "\<AA>\<^sub>3 xs ys = DCA_Combine.intersect_list (map (\<lambda>\<psi>. \<AA>\<^sub>\<nu>_FG (\<psi>[set xs]\<^sub>\<nu>)) ys)"
 
 lemma \<AA>\<^sub>3_language:
   "to_omega ` DCA.language (\<AA>\<^sub>3 xs ys) = L\<^sub>3 (set xs) (set ys)"
   by (simp add: \<AA>\<^sub>3_def L\<^sub>3_def set_eq_iff dca_language[OF \<AA>\<^sub>\<nu>_FG_language[OF GF_advice_\<nu>LTL(1)]])
 
 lemma \<AA>\<^sub>3_alphabet:
   "DCA.alphabet (\<AA>\<^sub>3 xs ys) = UNIV"
   by (simp add: \<AA>\<^sub>3_def \<AA>\<^sub>\<nu>_FG_def)
 
 
 definition "\<AA>' \<phi> xs ys = intersect_bc (\<AA>\<^sub>2 xs ys) (DCA_Combine.intersect (\<AA>\<^sub>1 \<phi> xs) (\<AA>\<^sub>3 xs ys))"
 
 lemma \<AA>'_language:
   "to_omega ` DRA.language (\<AA>' \<phi> xs ys) = (L\<^sub>1 \<phi> (set xs) \<inter> L\<^sub>2 (set xs) (set ys) \<inter> L\<^sub>3 (set xs) (set ys))"
   by (simp add: \<AA>'_def \<AA>\<^sub>1_language \<AA>\<^sub>2_language \<AA>\<^sub>3_language) fastforce
 
 lemma \<AA>'_alphabet:
   "DRA.alphabet (\<AA>' \<phi> xs ys) = UNIV"
   by (simp add: \<AA>'_def \<AA>\<^sub>1_alphabet \<AA>\<^sub>2_alphabet \<AA>\<^sub>3_alphabet)
 
 
 
 subsection \<open>A DRA for @{term "L(\<phi>)"}\<close>
 
+text \<open>
+  This is the final constant constructing a deterministic Rabin automaton
+  using the pure version of the  @{thm master_theorem}.
+\<close>
+
 definition "ltl_to_dra \<phi> = DRA_Combine.union_list (map (\<lambda>(xs, ys). \<AA>' \<phi> xs ys) (advice_sets \<phi>))"
 
 lemma ltl_to_dra_language:
   "to_omega ` DRA.language (ltl_to_dra \<phi>) = language_ltln \<phi>"
 proof -
   have "(\<Inter>(a, b)\<in>set (advice_sets \<phi>). dra.alphabet (\<AA>' \<phi> a b)) =
     (\<Union>(a, b)\<in>set (advice_sets \<phi>). dra.alphabet (\<AA>' \<phi> a b))"
     using advice_sets_not_empty by (simp add: \<AA>'_alphabet)
   then have *: "DRA.language (DRA_Combine.union_list (map (\<lambda>(x, y). \<AA>' \<phi> x y) (advice_sets \<phi>))) =
     \<Union> (DRA.language ` set (map (\<lambda>(x, y). \<AA>' \<phi> x y) (advice_sets \<phi>)))"
     by (simp add: split_def)
   have "language_ltln \<phi> = \<Union> {(L\<^sub>1 \<phi> X \<inter> L\<^sub>2 X Y \<inter> L\<^sub>3 X Y) | X Y. X \<subseteq> subformulas\<^sub>\<mu> \<phi> \<and> Y \<subseteq> subformulas\<^sub>\<nu> \<phi>}"
     unfolding master_theorem_language by auto
   also have "\<dots> = \<Union> {L\<^sub>1 \<phi> (set xs) \<inter> L\<^sub>2 (set xs) (set ys) \<inter> L\<^sub>3 (set xs) (set ys) | xs ys. (xs, ys) \<in> set (advice_sets \<phi>)}"
     unfolding advice_sets_subformulas by (metis (no_types, lifting))
   also have "\<dots> = \<Union> {to_omega ` DRA.language (\<AA>' \<phi> xs ys) | xs ys. (xs, ys) \<in> set (advice_sets \<phi>)}"
     by (simp add: \<AA>'_language)
   finally show ?thesis
     using * by (auto simp add: ltl_to_dra_def)
 qed
 
 lemma ltl_to_dra_alphabet:
   "alphabet (ltl_to_dra \<phi>) = UNIV"
   by (auto simp: ltl_to_dra_def \<AA>'_alphabet)
 
 
+subsection \<open>A DRA for @{term "L(\<phi>)"} with Restricted Advice Sets\<close>
 
-subsection \<open>Setting the Alphabet of a DRA\<close>
+text \<open>
+  The following constant uses the @{thm master_theorem_restricted} to reduce
+  the size of the resulting automaton.
+\<close>
+
+definition "ltl_to_dra_restricted \<phi> = DRA_Combine.union_list (map (\<lambda>(xs, ys). \<AA>' \<phi> xs ys) (restricted_advice_sets \<phi>))"
+
+lemma ltl_to_dra_restricted_language:
+  "to_omega ` DRA.language (ltl_to_dra_restricted \<phi>) = language_ltln \<phi>"
+proof -
+  have "(\<Inter>(a, b)\<in>set (restricted_advice_sets \<phi>). dra.alphabet (\<AA>' \<phi> a b)) =
+    (\<Union>(a, b)\<in>set (restricted_advice_sets \<phi>). dra.alphabet (\<AA>' \<phi> a b))"
+    using restricted_advice_sets_not_empty by (simp add: \<AA>'_alphabet)
+  then have *: "DRA.language (DRA_Combine.union_list (map (\<lambda>(x, y). \<AA>' \<phi> x y) (restricted_advice_sets \<phi>))) =
+    \<Union> (DRA.language ` set (map (\<lambda>(x, y). \<AA>' \<phi> x y) (restricted_advice_sets \<phi>)))"
+    by (simp add: split_def)
+  have "language_ltln \<phi> = \<Union> {(L\<^sub>1 \<phi> X \<inter> L\<^sub>2 X Y \<inter> L\<^sub>3 X Y) | X Y. X \<subseteq> subformulas\<^sub>\<mu> \<phi> \<inter> restricted_subformulas \<phi> \<and> Y \<subseteq> subformulas\<^sub>\<nu> \<phi> \<inter> restricted_subformulas \<phi>}"
+    unfolding master_theorem_restricted_language by auto
+  also have "\<dots> = \<Union> {L\<^sub>1 \<phi> (set xs) \<inter> L\<^sub>2 (set xs) (set ys) \<inter> L\<^sub>3 (set xs) (set ys) | xs ys. (xs, ys) \<in> set (restricted_advice_sets \<phi>)}"
+    unfolding restricted_advice_sets_subformulas by (metis (no_types, lifting))
+  also have "\<dots> = \<Union> {to_omega ` DRA.language (\<AA>' \<phi> xs ys) | xs ys. (xs, ys) \<in> set (restricted_advice_sets \<phi>)}"
+    by (simp add: \<AA>'_language)
+  finally show ?thesis
+    using * by (auto simp add: ltl_to_dra_restricted_def)
+qed
+
+lemma ltl_to_dra_restricted_alphabet:
+  "alphabet (ltl_to_dra_restricted \<phi>) = UNIV"
+  by (auto simp: ltl_to_dra_restricted_def \<AA>'_alphabet)
+
+
+subsection \<open>A DRA for @{term "L(\<phi>)"} with a finite alphabet\<close>
+
+text \<open>
+  Until this point, we use @{term UNIV} as the alphabet in all places.
+  To explore the automaton, however, we need a way to fix the alphabet
+  to some finite set.
+\<close>
 
 definition dra_set_alphabet :: "('a set, 'b) dra \<Rightarrow> 'a set set \<Rightarrow> ('a set, 'b) dra"
 where
   "dra_set_alphabet \<AA> \<Sigma> = dra \<Sigma> (initial \<AA>) (transition \<AA>) (condition \<AA>)"
 
 lemma dra_set_alphabet_language:
   "\<Sigma> \<subseteq> alphabet \<AA> \<Longrightarrow> language (dra_set_alphabet \<AA> \<Sigma>) = language \<AA> \<inter> {s. sset s \<subseteq> \<Sigma>}"
   by (auto simp add: dra_set_alphabet_def dra.language_def set_eq_iff dra.run_alt_def)
 
 lemma dra_set_alphabet_alphabet[simp]:
   "alphabet (dra_set_alphabet \<AA> \<Sigma>) = \<Sigma>"
   unfolding dra_set_alphabet_def by simp
 
 lemma dra_set_alphabet_nodes:
   "\<Sigma> \<subseteq> alphabet \<AA> \<Longrightarrow> DRA.nodes (dra_set_alphabet \<AA> \<Sigma>) \<subseteq> DRA.nodes \<AA>"
   unfolding dra_set_alphabet_def dra.nodes_alt_def dra.reachable_alt_def dra.path_alt_def
   by auto
 
 
-
-subsection \<open>A DRA for @{term "L(\<phi>)"} with a finite alphabet\<close>
-
-definition "ltl_to_dra_alphabet \<phi> Ap = dra_set_alphabet (ltl_to_dra \<phi>) (Pow Ap)"
+definition "ltl_to_dra_alphabet \<phi> Ap = dra_set_alphabet (ltl_to_dra_restricted \<phi>) (Pow Ap)"
 
 lemma ltl_to_dra_alphabet_language:
   assumes
     "atoms_ltln \<phi> \<subseteq> Ap"
   shows
     "to_omega ` language (ltl_to_dra_alphabet \<phi> Ap) = language_ltln \<phi> \<inter> {w. range w \<subseteq> Pow Ap}"
 proof -
-  have 1: "Pow Ap \<subseteq> alphabet (ltl_to_dra \<phi>)"
-    unfolding ltl_to_dra_alphabet by simp
+  have 1: "Pow Ap \<subseteq> alphabet (ltl_to_dra_restricted \<phi>)"
+    unfolding ltl_to_dra_restricted_alphabet by simp
 
   show ?thesis
     unfolding ltl_to_dra_alphabet_def dra_set_alphabet_language[OF 1]
-    by (simp add: ltl_to_dra_language sset_range) force
+    by (simp add: ltl_to_dra_restricted_language sset_range) force
 qed
 
 lemma ltl_to_dra_alphabet_alphabet[simp]:
   "alphabet (ltl_to_dra_alphabet \<phi> Ap) = Pow Ap"
   unfolding ltl_to_dra_alphabet_def by simp
 
 lemma ltl_to_dra_alphabet_nodes:
-  "DRA.nodes (ltl_to_dra_alphabet \<phi> Ap) \<subseteq> DRA.nodes (ltl_to_dra \<phi>)"
+  "DRA.nodes (ltl_to_dra_alphabet \<phi> Ap) \<subseteq> DRA.nodes (ltl_to_dra_restricted \<phi>)"
   unfolding ltl_to_dra_alphabet_def
-  by (rule dra_set_alphabet_nodes) (simp add: ltl_to_dra_alphabet)
+  by (rule dra_set_alphabet_nodes) (simp add: ltl_to_dra_restricted_alphabet)
+
+end
+
+
+subsection \<open>Verified Bounds for Number of Nodes\<close>
+
+text \<open>
+  Using two additional assumptions, we can show a double-exponential size bound
+  for the constructed automaton.
+\<close>
+
+(* TODO add to HOL/Groups_List.thy *)
+lemma list_prod_mono:
+  "f \<le> g \<Longrightarrow> (\<Prod>x\<leftarrow>xs. f x) \<le> (\<Prod>x\<leftarrow>xs. g x)" for f g :: "'a \<Rightarrow> nat"
+  by (induction xs) (auto simp: le_funD mult_le_mono)
+
+(* TODO add to HOL/Groups_List.thy *)
+lemma list_prod_const:
+  "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> c) \<Longrightarrow> (\<Prod>x\<leftarrow>xs. f x) \<le> c ^ length xs" for f :: "'a \<Rightarrow> nat"
+  by (induction xs) (auto simp: mult_le_mono)
+
+(* TODO add to HOL/Finite_Set.thy *)
+lemma card_insert_Suc:
+  "card (insert x S) \<le> Suc (card S)"
+  by (metis Suc_n_not_le_n card.infinite card_insert_if finite_insert linear)
+
+(* TODO add to HOL/Power.thy *)
+lemma nat_power_le_imp_le:
+  "0 < a \<Longrightarrow> a \<le> b \<Longrightarrow> x ^ a \<le> x ^ b" for x :: nat
+  by (metis leD linorder_le_less_linear nat_power_less_imp_less neq0_conv power_eq_0_iff)
+
+(* TODO add to HOL/Power.thy *)
+lemma const_less_power:
+  "n < x ^ n" if "x > 1"
+  using that by (induction n) (auto simp: less_trans_Suc)
+
+(* TODO add to HOL-Library/Log_Nat.thy *)
+lemma floorlog_le_const:
+  "floorlog x n \<le> n"
+  by (induction n) (simp add: floorlog_eq_zero_iff, metis Suc_lessI floorlog_le_iff le_SucI power_inject_exp)
+
+
+locale dra_construction_size = dra_construction + transition_functions_size +
+  assumes
+    equiv_finite: "finite P \<Longrightarrow> finite {Abs \<psi> | \<psi>. prop_atoms \<psi> \<subseteq> P}"
+  assumes
+    equiv_card: "finite P \<Longrightarrow> card {Abs \<psi> | \<psi>. prop_atoms \<psi> \<subseteq> P} \<le> 2 ^ 2 ^ card P"
+begin
+
+lemma af\<^sub>F_lifted_range:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> range (\<up>af\<^sub>F \<phi> (Abs \<psi>)) \<subseteq>  {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
+  using af\<^sub>F_lifted_semantics af\<^sub>F_nested_prop_atoms by blast
+
+lemma af\<^sub>G_lifted_range:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> range (\<up>af\<^sub>G \<phi> (Abs \<psi>)) \<subseteq>  {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
+  using af\<^sub>G_lifted_semantics af\<^sub>G_nested_prop_atoms by blast
+
+
+lemma \<AA>\<^sub>\<mu>_nodes:
+  "DBA.nodes (\<AA>\<^sub>\<mu> \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
+  unfolding \<AA>\<^sub>\<mu>_def
+  using af_lifted_semantics af_nested_prop_atoms by fastforce
+
+lemma \<AA>\<^sub>\<mu>_GF_nodes:
+  "DBA.nodes (\<AA>\<^sub>\<mu>_GF \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
+  unfolding \<AA>\<^sub>\<mu>_GF_def dba.nodes_alt_def dba.reachable_alt_def
+  using af\<^sub>F_nested_prop_atoms[of "F\<^sub>n \<phi>"] by (auto simp: af\<^sub>F_lifted_semantics)
+
+lemma \<AA>\<^sub>\<nu>_nodes:
+  "DCA.nodes (\<AA>\<^sub>\<nu> \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
+  unfolding \<AA>\<^sub>\<nu>_def
+  using af_lifted_semantics af_nested_prop_atoms by fastforce
+
+lemma \<AA>\<^sub>\<nu>_FG_nodes:
+  "DCA.nodes (\<AA>\<^sub>\<nu>_FG \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
+  unfolding \<AA>\<^sub>\<nu>_FG_def dca.nodes_alt_def dca.reachable_alt_def
+  using af\<^sub>G_nested_prop_atoms[of "G\<^sub>n \<phi>"] by (auto simp: af\<^sub>G_lifted_semantics)
+
+lemma \<CC>_nodes_normalise:
+  "DCA.nodes (\<CC> \<phi> X) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>} \<times> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> (normalise \<phi>) X}"
+  unfolding \<CC>_def dca.nodes_alt_def dca.reachable_alt_def
+  apply (auto simp add: af\<^sub>\<nu>_lifted_semantics af_letter\<^sub>\<nu>_lifted_semantics)
+  using af\<^sub>\<nu>_fst_nested_prop_atoms apply force
+  by (metis GF_advice_nested_prop_atoms\<^sub>\<nu> af\<^sub>\<nu>_snd_nested_prop_atoms Abs_eq af\<^sub>\<nu>_lifted_semantics fst_conv normalise_eq snd_conv sup.absorb_iff1)
+
+lemma \<CC>_nodes:
+  "DCA.nodes (\<CC> \<phi> X) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>} \<times> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X}"
+  unfolding \<CC>_def dca.nodes_alt_def dca.reachable_alt_def
+  apply (auto simp add: af\<^sub>\<nu>_lifted_semantics af_letter\<^sub>\<nu>_lifted_semantics)
+  using af\<^sub>\<nu>_fst_nested_prop_atoms apply force
+  by (metis (no_types, hide_lams) GF_advice_nested_prop_atoms\<^sub>\<nu> af\<^sub>\<nu>_snd_nested_prop_atoms fst_eqD nested_prop_atoms\<^sub>\<nu>_subset normalise_nested_propos order_refl order_trans snd_eqD sup.order_iff)
+
+
+
+lemma equiv_subset:
+  "{Abs \<psi> |\<psi>. nested_prop_atoms \<psi> \<subseteq> P} \<subseteq> {Abs \<psi> |\<psi>. prop_atoms \<psi> \<subseteq> P}"
+  using prop_atoms_nested_prop_atoms by blast
+
+lemma equiv_finite':
+  "finite P \<Longrightarrow> finite {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> P}"
+  using equiv_finite equiv_subset finite_subset by fast
+
+lemma equiv_card':
+  "finite P \<Longrightarrow> card {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> P} \<le> 2 ^ 2 ^ card P"
+  by (metis (mono_tags, lifting) equiv_card equiv_subset equiv_finite card_mono le_trans)
+
+
+lemma nested_prop_atoms_finite:
+  "finite {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
+  using equiv_finite'[OF Equivalence_Relations.nested_prop_atoms_finite] .
+
+lemma nested_prop_atoms_card:
+  "card {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>} \<le> 2 ^ 2 ^ card (nested_prop_atoms \<phi>)"
+  using equiv_card'[OF Equivalence_Relations.nested_prop_atoms_finite] .
+
+lemma nested_prop_atoms\<^sub>\<nu>_finite:
+  "finite {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X}"
+  using equiv_finite'[OF nested_prop_atoms\<^sub>\<nu>_finite] by fast
+
+lemma nested_prop_atoms\<^sub>\<nu>_card:
+  "card {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X} \<le> 2 ^ 2 ^ card (nested_prop_atoms \<phi>)" (is "?lhs \<le> ?rhs")
+proof -
+  have "finite {Abs \<psi> | \<psi>. prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X}"
+    by (simp add: nested_prop_atoms\<^sub>\<nu>_finite Advice.nested_prop_atoms\<^sub>\<nu>_finite equiv_finite)
+
+  then have "?lhs \<le> card {Abs \<psi> | \<psi>. prop_atoms \<psi> \<subseteq> (nested_prop_atoms\<^sub>\<nu> \<phi> X)}"
+    using card_mono equiv_subset by blast
+
+  also have "\<dots> \<le> 2 ^ 2 ^ card (nested_prop_atoms\<^sub>\<nu> \<phi> X)"
+    using equiv_card[OF Advice.nested_prop_atoms\<^sub>\<nu>_finite] by fast
+
+  also have "\<dots> \<le> ?rhs"
+    using nested_prop_atoms\<^sub>\<nu>_card by auto
+
+  finally show ?thesis .
+qed
+
+
+lemma \<AA>\<^sub>\<mu>_GF_nodes_finite:
+  "finite (DBA.nodes (\<AA>\<^sub>\<mu>_GF \<phi>))"
+  using finite_subset[OF \<AA>\<^sub>\<mu>_GF_nodes nested_prop_atoms_finite] .
+
+lemma \<AA>\<^sub>\<nu>_FG_nodes_finite:
+  "finite (DCA.nodes (\<AA>\<^sub>\<nu>_FG \<phi>))"
+  using finite_subset[OF \<AA>\<^sub>\<nu>_FG_nodes nested_prop_atoms_finite] .
+
+lemma \<AA>\<^sub>\<mu>_GF_nodes_card:
+  "card (DBA.nodes (\<AA>\<^sub>\<mu>_GF \<phi>)) \<le> 2 ^ 2 ^ card (nested_prop_atoms (F\<^sub>n \<phi>))"
+  using le_trans[OF card_mono[OF nested_prop_atoms_finite \<AA>\<^sub>\<mu>_GF_nodes] nested_prop_atoms_card] .
+
+lemma \<AA>\<^sub>\<nu>_FG_nodes_card:
+  "card (DCA.nodes (\<AA>\<^sub>\<nu>_FG \<phi>)) \<le> 2 ^ 2 ^ card (nested_prop_atoms (G\<^sub>n \<phi>))"
+  using le_trans[OF card_mono[OF nested_prop_atoms_finite \<AA>\<^sub>\<nu>_FG_nodes] nested_prop_atoms_card] .
+
+
+lemma \<AA>\<^sub>2_nodes_finite_helper:
+  "list_all (finite \<circ> DBA.nodes) (map (\<lambda>\<psi>. \<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>)) xs)"
+  by (auto simp: list.pred_map list_all_iff \<AA>\<^sub>\<mu>_GF_nodes_finite)
+
+lemma \<AA>\<^sub>2_nodes_finite:
+  "finite (DBA.nodes (\<AA>\<^sub>2 xs ys))"
+  unfolding \<AA>\<^sub>2_def using DBA_Combine.intersect_list_nodes_finite \<AA>\<^sub>2_nodes_finite_helper .
+
+lemma \<AA>\<^sub>3_nodes_finite_helper:
+  "list_all (finite \<circ> DCA.nodes) (map (\<lambda>\<psi>. \<AA>\<^sub>\<nu>_FG (\<psi>[set xs]\<^sub>\<nu>)) ys)"
+  by (auto simp: list.pred_map list_all_iff \<AA>\<^sub>\<nu>_FG_nodes_finite)
+
+lemma \<AA>\<^sub>3_nodes_finite:
+  "finite (DCA.nodes (\<AA>\<^sub>3 xs ys))"
+  unfolding \<AA>\<^sub>3_def using DCA_Combine.intersect_list_nodes_finite \<AA>\<^sub>3_nodes_finite_helper .
+
+lemma \<AA>\<^sub>2_nodes_card:
+  assumes
+    "length xs \<le> n"
+  and
+    "\<And>\<psi>. \<psi> \<in> set xs \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
+  shows
+    "card (DBA.nodes (\<AA>\<^sub>2 xs ys)) \<le> 2 ^ 2 ^ (n + floorlog 2 n + 2)"
+proof -
+  have 1: "\<And>\<psi>. \<psi> \<in> set xs \<Longrightarrow> card (nested_prop_atoms (F\<^sub>n \<psi>[set ys]\<^sub>\<mu>)) \<le> Suc n"
+  proof -
+    fix \<psi>
+    assume "\<psi> \<in> set xs"
+
+    have "card (nested_prop_atoms (F\<^sub>n (\<psi>[set ys]\<^sub>\<mu>)))
+          \<le> Suc (card (nested_prop_atoms (\<psi>[set ys]\<^sub>\<mu>)))"
+      by (simp add: card_insert_Suc)
+
+    also have "\<dots> \<le> Suc (card (nested_prop_atoms \<psi>))"
+      by (simp add: FG_advice_nested_prop_atoms_card)
+
+    also have "\<dots> \<le> Suc n"
+      by (simp add: assms(2) \<open>\<psi> \<in> set xs\<close>)
+
+    finally show "card (nested_prop_atoms (F\<^sub>n (\<psi>[set ys]\<^sub>\<mu>))) \<le> Suc n" .
+  qed
+
+  have "(\<Prod>\<psi>\<leftarrow>xs. card (DBA.nodes (\<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>))))
+        \<le> (\<Prod>\<psi>\<leftarrow>xs. 2 ^ 2 ^ card (nested_prop_atoms (F\<^sub>n (\<psi>[set ys]\<^sub>\<mu>))))"
+    by (rule list_prod_mono) (insert \<AA>\<^sub>\<mu>_GF_nodes_card le_fun_def, blast)
+
+  also have "\<dots> \<le> (2 ^ 2 ^ Suc n) ^ length xs"
+    by (rule list_prod_const) (metis 1 Suc_leI nat_power_le_imp_le nat_power_eq_Suc_0_iff neq0_conv pos2 zero_less_power)
+
+  also have "\<dots> \<le> (2 ^ 2 ^ Suc n) ^ n"
+    using assms(1) nat_power_le_imp_le by fastforce
+
+  also have "\<dots> = 2 ^ (n * 2 ^ Suc n)"
+    by (metis Groups.mult_ac(2) power_mult)
+
+  also have "\<dots> \<le> 2 ^ (2 ^ floorlog 2 n * 2 ^ Suc n)"
+    by (cases "n = 0") (auto simp: floorlog_bounds less_imp_le_nat)
+
+  also have "\<dots> = 2 ^ 2 ^ (Suc n + floorlog 2 n)"
+    by (simp add: power_add)
+
+  finally have 2: "(\<Prod>\<psi>\<leftarrow>xs. card (DBA.nodes (\<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>)))) \<le> 2 ^ 2 ^ (Suc n + floorlog 2 n)" .
+
+  have "card (DBA.nodes (\<AA>\<^sub>2 xs ys)) \<le> max 1 (length xs) * (\<Prod>\<psi>\<leftarrow>xs. card (DBA.nodes (\<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>))))"
+    using DBA_Combine.intersect_list_nodes_card[OF \<AA>\<^sub>2_nodes_finite_helper]
+    by (auto simp: \<AA>\<^sub>2_def comp_def)
+
+  also have "\<dots> \<le> max 1 n * 2 ^ 2 ^ (Suc n + floorlog 2 n)"
+    using assms(1) 2 by (simp add: mult_le_mono)
+
+  also have "\<dots> \<le> 2 ^ (floorlog 2 n) * 2 ^ 2 ^ (Suc n + floorlog 2 n)"
+    by (cases "n = 0") (auto simp: floorlog_bounds less_imp_le_nat)
+
+  also have "\<dots> = 2 ^ (floorlog 2 n + 2 ^ (Suc n + floorlog 2 n))"
+    by (simp add: power_add)
+
+  also have "\<dots> \<le> 2 ^ (n + 2 ^ (Suc n + floorlog 2 n))"
+    by (simp add: floorlog_le_const)
+
+  also have "\<dots> \<le> 2 ^ 2 ^ (n + floorlog 2 n + 2)"
+    by simp (metis const_less_power Suc_1 add_Suc_right add_leE lessI less_imp_le_nat power_Suc)
+
+  finally show ?thesis .
+qed
+
+
+lemma \<AA>\<^sub>3_nodes_card:
+  assumes
+    "length ys \<le> n"
+  and
+    "\<And>\<psi>. \<psi> \<in> set ys \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
+  shows
+    "card (DCA.nodes (\<AA>\<^sub>3 xs ys)) \<le> 2 ^ 2 ^ (n + floorlog 2 n + 1)"
+proof -
+  have 1: "\<And>\<psi>. \<psi> \<in> set ys \<Longrightarrow> card (DCA.nodes (\<AA>\<^sub>\<nu>_FG (\<psi>[set xs]\<^sub>\<nu>))) \<le> 2 ^ 2 ^ Suc n"
+  proof -
+    fix \<psi>
+    assume "\<psi> \<in> set ys"
+
+    have "card (nested_prop_atoms (G\<^sub>n \<psi>[set xs]\<^sub>\<nu>))
+          \<le> Suc (card (nested_prop_atoms (\<psi>[set xs]\<^sub>\<nu>)))"
+      by (simp add: card_insert_Suc)
+
+    also have "\<dots> \<le> Suc (card (nested_prop_atoms \<psi>))"
+      by (simp add: GF_advice_nested_prop_atoms_card)
+
+    also have "\<dots> \<le> Suc n"
+      by (simp add: assms(2) \<open>\<psi> \<in> set ys\<close>)
+
+    finally have 2: "card (nested_prop_atoms (G\<^sub>n \<psi>[set xs]\<^sub>\<nu>)) \<le> Suc n" .
+
+    then show "?thesis \<psi>"
+      by (intro le_trans[OF \<AA>\<^sub>\<nu>_FG_nodes_card]) (meson one_le_numeral power_increasing)
+  qed
+
+
+  have "card (DCA.nodes (\<AA>\<^sub>3 xs ys)) \<le> (\<Prod>\<psi>\<leftarrow>ys. card (DCA.nodes (\<AA>\<^sub>\<nu>_FG (\<psi>[set xs]\<^sub>\<nu>))))"
+    unfolding \<AA>\<^sub>3_def using DCA_Combine.intersect_list_nodes_card[OF \<AA>\<^sub>3_nodes_finite_helper]
+    by (auto simp: comp_def)
+
+  also have "\<dots> \<le> (2 ^ 2 ^ Suc n) ^ length ys"
+    by (rule list_prod_const) (rule 1)
+
+  also have "\<dots> \<le> (2 ^ 2 ^ Suc n) ^ n"
+    by (simp add: assms(1) power_increasing)
+
+  also have "\<dots> \<le> 2 ^ (n * 2 ^ Suc n)"
+    by (metis le_refl mult.commute power_mult)
+
+  also have "\<dots> \<le> 2 ^ (2 ^ floorlog 2 n * 2 ^ Suc n)"
+    by (cases \<open>n > 0\<close>) (simp_all add: floorlog_bounds less_imp_le_nat)
+
+  also have "\<dots> = 2 ^ 2 ^ (n + floorlog 2 n + 1)"
+    by (simp add: power_add)
+
+  finally show ?thesis .
+qed
+
+
+lemma \<AA>\<^sub>1_nodes_finite:
+  "finite (DCA.nodes (\<AA>\<^sub>1 \<phi> xs))"
+  unfolding \<AA>\<^sub>1_def
+  by (metis (no_types, lifting) finite_subset \<CC>_nodes finite_SigmaI nested_prop_atoms\<^sub>\<nu>_finite nested_prop_atoms_finite)
+
+lemma \<AA>\<^sub>1_nodes_card:
+  assumes
+    "card (subfrmlsn \<phi>) \<le> n"
+  shows
+    "card (DCA.nodes (\<AA>\<^sub>1 \<phi> xs)) \<le> 2 ^ 2 ^ (n + 1)"
+proof -
+  let ?fst = "{Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
+  let ?snd = "{Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> (set xs)}"
+
+  have 1: "card (nested_prop_atoms \<phi>) \<le> n"
+    by (meson card_mono[OF subfrmlsn_finite nested_prop_atoms_subfrmlsn] assms le_trans)
+
+
+  have "card (DCA.nodes (\<AA>\<^sub>1 \<phi> xs)) \<le> card (?fst \<times> ?snd)"
+    unfolding \<AA>\<^sub>1_def
+    by (rule card_mono) (simp_all add: \<CC>_nodes nested_prop_atoms\<^sub>\<nu>_finite nested_prop_atoms_finite)
+
+  also have "\<dots> = card ?fst * card ?snd"
+    using nested_prop_atoms\<^sub>\<nu>_finite card_cartesian_product by blast
+
+  also have "\<dots> \<le> 2 ^ 2 ^ card (nested_prop_atoms \<phi>) * 2 ^ 2 ^ card (nested_prop_atoms \<phi>)"
+    using nested_prop_atoms\<^sub>\<nu>_card nested_prop_atoms_card mult_le_mono by blast
+
+  also have "\<dots> = 2 ^ 2 ^ (card (nested_prop_atoms \<phi>) + 1)"
+    by (simp add: semiring_normalization_rules(36))
+
+  also have "\<dots> \<le> 2 ^ 2 ^ (n + 1)"
+    using assms 1 by simp
+
+  finally show ?thesis .
+qed
+
+
+lemma \<AA>'_nodes_finite:
+  "finite (DRA.nodes (\<AA>' \<phi> xs ys))"
+  unfolding \<AA>'_def
+  using intersect_nodes_finite intersect_bc_nodes_finite
+  using \<AA>\<^sub>1_nodes_finite \<AA>\<^sub>2_nodes_finite \<AA>\<^sub>3_nodes_finite
+  by fast
+
+lemma \<AA>'_nodes_card:
+  assumes
+    "length xs \<le> n"
+  and
+    "\<And>\<psi>. \<psi> \<in> set xs \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
+  and
+    "length ys \<le> n"
+  and
+    "\<And>\<psi>. \<psi> \<in> set ys \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
+  and
+    "card (subfrmlsn \<phi>) \<le> n"
+  shows
+    "card (DRA.nodes (\<AA>' \<phi> xs ys)) \<le> 2 ^ 2 ^ (n + floorlog 2 n + 4)"
+proof -
+  have "n + 1 \<le> n + floorlog 2 n + 2"
+    by auto
+
+  then have 1: "(2::nat) ^ (n + 1) \<le> 2 ^ (n + floorlog 2 n + 2)"
+    using one_le_numeral power_increasing by blast
+
+
+  have "card (DRA.nodes (\<AA>' \<phi> xs ys)) \<le> card (DCA.nodes (\<AA>\<^sub>1 \<phi> xs)) * card (DBA.nodes (\<AA>\<^sub>2 xs ys)) * card (DCA.nodes (\<AA>\<^sub>3 xs ys))" (is "?lhs \<le> ?rhs")
+  proof (unfold \<AA>'_def)
+    have "card (DBA.nodes (\<AA>\<^sub>2 xs ys)) * card (DCA.nodes (DCA_Combine.intersect (\<AA>\<^sub>1 \<phi> xs) (\<AA>\<^sub>3 xs ys))) \<le> ?rhs"
+      by (simp add: intersect_nodes_card[OF \<AA>\<^sub>1_nodes_finite \<AA>\<^sub>3_nodes_finite])
+    then show "card (DRA.nodes (intersect_bc (\<AA>\<^sub>2 xs ys) (DCA_Combine.intersect (\<AA>\<^sub>1 \<phi> xs) (\<AA>\<^sub>3 xs ys)))) \<le> ?rhs"
+      by (meson intersect_bc_nodes_card[OF \<AA>\<^sub>2_nodes_finite intersect_nodes_finite[OF \<AA>\<^sub>1_nodes_finite \<AA>\<^sub>3_nodes_finite]] basic_trans_rules(23))
+  qed
+
+  also have "\<dots> \<le> 2 ^ 2 ^ (n + 1) * 2 ^ 2 ^ (n + floorlog 2 n + 2) * 2 ^ 2 ^ (n + floorlog 2 n + 1)"
+    using \<AA>\<^sub>1_nodes_card[OF assms(5)] \<AA>\<^sub>2_nodes_card[OF assms(1,2)] \<AA>\<^sub>3_nodes_card[OF assms(3,4)]
+    by (metis mult_le_mono)
+
+  also have "\<dots> = 2 ^ (2 ^ (n + 1) + 2 ^ (n + floorlog 2 n + 2) + 2 ^ (n + floorlog 2 n + 1))"
+    by (metis power_add)
+
+  also have "\<dots> \<le> 2 ^ (4 * 2 ^ (n + floorlog 2 n + 2))"
+    using 1 by auto
+
+  finally show ?thesis
+    by (simp add: numeral.simps(2) power_add)
+qed
+
+lemma subformula_nested_prop_atoms_subfrmlsn:
+  "\<psi> \<in> subfrmlsn \<phi> \<Longrightarrow> nested_prop_atoms \<psi> \<subseteq> subfrmlsn \<phi>"
+  using nested_prop_atoms_subfrmlsn subfrmlsn_subset by blast
+
+
+lemma ltl_to_dra_nodes_finite:
+  "finite (DRA.nodes (ltl_to_dra \<phi>))"
+  unfolding ltl_to_dra_def
+  apply (rule DRA_Combine.union_list_nodes_finite)
+  apply (simp add: split_def \<AA>'_alphabet advice_sets_not_empty)
+  apply (simp add: list.pred_set split_def \<AA>'_nodes_finite)
+  done
+
+lemma ltl_to_dra_restricted_nodes_finite:
+  "finite (DRA.nodes (ltl_to_dra_restricted \<phi>))"
+  unfolding ltl_to_dra_restricted_def
+  apply (rule DRA_Combine.union_list_nodes_finite)
+  apply (simp add: split_def \<AA>'_alphabet advice_sets_not_empty)
+  apply (simp add: list.pred_set split_def \<AA>'_nodes_finite)
+  done
+
+lemma ltl_to_dra_alphabet_nodes_finite:
+  "finite (DRA.nodes (ltl_to_dra_alphabet \<phi> AP))"
+  using ltl_to_dra_alphabet_nodes ltl_to_dra_restricted_nodes_finite finite_subset by fast
+
+
+lemma ltl_to_dra_nodes_card:
+  assumes
+    "card (subfrmlsn \<phi>) \<le> n"
+  shows
+    "card (DRA.nodes (ltl_to_dra \<phi>)) \<le> 2 ^ 2 ^ (2 * n + floorlog 2 n + 4)"
+proof -
+  let ?map = "map (\<lambda>(x, y). \<AA>' \<phi> x y) (advice_sets \<phi>)"
+
+  have 1: "\<And>x::nat. x > 0 \<Longrightarrow> x ^ length (advice_sets \<phi>) \<le> x ^ 2 ^ card (subfrmlsn \<phi>)"
+    by (metis advice_sets_length linorder_not_less nat_power_less_imp_less)
+
+  have "card (DRA.nodes (ltl_to_dra \<phi>)) \<le> prod_list (map (card \<circ> DRA.nodes) ?map)"
+    unfolding ltl_to_dra_def
+    apply (rule DRA_Combine.union_list_nodes_card)
+    unfolding list.pred_set using \<AA>'_nodes_finite by auto
+
+  also have "\<dots> = (\<Prod>(x, y)\<leftarrow>advice_sets \<phi>. card (DRA.nodes (\<AA>' \<phi> x y)))"
+    by (induction "advice_sets \<phi>") (auto, metis (no_types, lifting) comp_apply split_def)
+
+  also have "\<dots> \<le> (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ length (advice_sets \<phi>)"
+  proof (rule list_prod_const, unfold split_def, rule \<AA>'_nodes_card)
+    show "\<And>x. x \<in> set (advice_sets \<phi>) \<Longrightarrow> length (fst x) \<le> n"
+      using advice_sets_element_length assms by fastforce
+
+    show "\<And>x \<psi>. \<lbrakk>x \<in> set (advice_sets \<phi>); \<psi> \<in> set (fst x)\<rbrakk> \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
+      using advice_sets_element_subfrmlsn(1) assms subformula_nested_prop_atoms_subfrmlsn subformulas\<^sub>\<mu>_subfrmlsn
+      by (metis (no_types, lifting) card_mono subfrmlsn_finite subset_iff sup.absorb_iff2 sup.coboundedI1 surjective_pairing)
+
+    show "\<And>x. x \<in> set (advice_sets \<phi>) \<Longrightarrow> length (snd x) \<le> n"
+      using advice_sets_element_length assms by fastforce
+
+    show "\<And>x \<psi>. \<lbrakk>x \<in> set (advice_sets \<phi>); \<psi> \<in> set (snd x)\<rbrakk> \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
+      using advice_sets_element_subfrmlsn(2) assms subformula_nested_prop_atoms_subfrmlsn subformulas\<^sub>\<nu>_subfrmlsn
+      by (metis (no_types, lifting) card_mono subfrmlsn_finite subset_iff sup.absorb_iff2 sup.coboundedI1 surjective_pairing)
+  qed (insert assms, blast)
+
+  also have "\<dots> \<le> (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ (2 ^ card (subfrmlsn \<phi>))"
+    by (simp add: 1)
+
+  also have "\<dots> \<le> (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ (2 ^ n)"
+    by (simp add: assms power_increasing)
+
+  also have "\<dots> = 2 ^ (2 ^ n * 2 ^ (n + floorlog 2 n + 4))"
+    by (simp add: ac_simps power_mult [symmetric])
+
+  also have "\<dots> = 2 ^ 2 ^ (2 * n + floorlog 2 n + 4)"
+    by (simp add: power_add) (simp add: mult_2 power_add)
+
+  finally show ?thesis .
+qed
+
+text \<open>We verify the size bound of the automaton to be double exponential.\<close>
+
+theorem ltl_to_dra_size:
+  "card (DRA.nodes (ltl_to_dra \<phi>)) \<le> 2 ^ 2 ^ (2 * size \<phi> + floorlog 2 (size \<phi>) + 4)"
+  using ltl_to_dra_nodes_card subfrmlsn_card by blast
 
 end
 
 end
diff --git a/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Implementation.thy b/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Implementation.thy
--- a/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Implementation.thy
+++ b/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Implementation.thy
@@ -1,203 +1,157 @@
 (*
     Author:   Benedikt Seidl
     License:  BSD
 *)
 
 section \<open>Implementation of the DRA Construction\<close>
 
 theory DRA_Implementation
 imports
-  DRA_Instantiation
+  DRA_Construction
   LTL.Rewriting
-  LTL.Disjunctive_Normal_Form
   Transition_Systems_and_Automata.DRA_Translate
-  Deriving.Derive
-begin
-
-subsection \<open>Hash functions for LTL\<close>
-
-derive hashable ltln
-
-definition cube :: "'a :: times \<Rightarrow> 'a"
-where
-  "cube a = a * a * a"
-
-instantiation set :: (hashable) hashable
 begin
 
-definition [simp]: "hashcode (x :: 'a set) = Finite_Set.fold (plus o cube o hashcode) (uint32_of_nat (card x)) x"
-definition "def_hashmap_size = (\<lambda>_ :: 'a set itself. 2 * def_hashmap_size TYPE('a))"
-
-instance
-proof
-  from def_hashmap_size[where ?'a = "'a"]
-  show "1 < def_hashmap_size TYPE('a set)"
-    by (simp add: def_hashmap_size_set_def)
-qed
-
-end
-
-instantiation fset :: (hashable) hashable
-begin
-
-definition [simp]: "hashcode (x :: 'a fset) = hashcode (fset x)"
-definition "def_hashmap_size = (\<lambda>_ :: 'a fset itself. 2 * def_hashmap_size TYPE('a))"
-
-instance
-proof
-  from def_hashmap_size[where ?'a = "'a"]
-  show "1 < def_hashmap_size TYPE('a fset)"
-    by (simp add: def_hashmap_size_fset_def)
-qed
-
-end
-
-instantiation ltln\<^sub>P :: (hashable) hashable
-begin
-
-definition [simp]: "hashcode (\<phi> :: 'a ltln\<^sub>P) = hashcode (min_dnf (rep_ltln\<^sub>P \<phi>))"
-definition "def_hashmap_size = (\<lambda>_ :: 'a ltln\<^sub>P itself. def_hashmap_size TYPE('a ltln))"
-
-instance
-proof
-  from def_hashmap_size[where ?'a = "'a"]
-  show "1 < def_hashmap_size TYPE('a ltln\<^sub>P)"
-    by (simp add: def_hashmap_size_ltln\<^sub>P_def def_hashmap_size_ltln_def)
-qed
-
-end
-
-
 subsection \<open>Generating the Explicit Automaton\<close>
 
 text \<open>
   We convert the implicit automaton to its explicit representation
   and afterwards proof the final correctness theorem and the overall
   size bound.
 \<close>
 
 definition dra_to_drai :: "('a, 'b) dra \<Rightarrow> 'a list \<Rightarrow> ('a, 'b) drai"
 where
   "dra_to_drai \<AA> \<Sigma> = drai \<Sigma> (initial \<AA>) (transition \<AA>) (condition \<AA>)"
 
 lemma dra_to_drai_language:
   "set \<Sigma> = alphabet \<AA> \<Longrightarrow> language (drai_dra (dra_to_drai \<AA> \<Sigma>)) = language \<AA>"
   by (simp add: dra_to_drai_def drai_dra_def)
 
 definition drai_to_draei :: "nat \<Rightarrow> ('a, 'b :: hashable) drai \<Rightarrow> ('a, nat) draei"
 where
   "drai_to_draei hms = to_draei_impl (=) bounded_hashcode_nat hms"
 
+
+lemma dra_to_drai_rel:
+  assumes
+    "(\<Sigma>, alphabet A) \<in> \<langle>Id\<rangle> list_set_rel"
+  shows
+    "(dra_to_drai A \<Sigma>, A) \<in> \<langle>Id, Id\<rangle>drai_dra_rel"
+proof -
+  have "(A, A) \<in> \<langle>Id, Id\<rangle>dra_rel"
+    by simp
+
+  then have "(dra_to_drai A \<Sigma>, dra (alphabet A) (initial A) (transition A) (condition A)) \<in> \<langle>Id, Id\<rangle>drai_dra_rel"
+    unfolding dra_to_drai_def using assms by parametricity
+
+  then show ?thesis
+    by simp
+qed
+
+lemma draei_language_rel:
+  fixes
+    A :: "('label, 'state :: hashable) dra"
+  assumes
+    "(\<Sigma>, alphabet A) \<in> \<langle>Id\<rangle> list_set_rel"
+  and
+    "finite (DRA.nodes A)"
+  and
+    "is_valid_def_hm_size TYPE('state) hms"
+  shows
+    "DRA.language (drae_dra (draei_drae (drai_to_draei hms (dra_to_drai A \<Sigma>)))) = DRA.language A"
+proof -
+  have "(dra_to_drai A \<Sigma>, A) \<in> \<langle>Id, Id\<rangle>drai_dra_rel"
+    using dra_to_drai_rel assms by fast
+
+  then have "(drai_to_draei hms (dra_to_drai A \<Sigma>), to_draei A) \<in> \<langle>Id_on (dra.alphabet A), rel (dra_to_drai A \<Sigma>) A (=) bounded_hashcode_nat hms\<rangle> draei_dra_rel"
+    unfolding drai_to_draei_def
+    using to_draei_impl_refine[unfolded autoref_tag_defs]
+    by parametricity (simp_all add: assms is_bounded_hashcode_def bounded_hashcode_nat_bounds)
+
+  then have "(DRA.language ((drae_dra \<circ> draei_drae) (drai_to_draei hms (dra_to_drai A \<Sigma>))), DRA.language (id (to_draei A))) \<in> \<langle>\<langle>Id_on (dra.alphabet A)\<rangle> stream_rel\<rangle> set_rel"
+    by parametricity
+
+  then show ?thesis
+    by (simp add: to_draei_def)
+qed
+
+
+subsection \<open>Defining the Alphabet\<close>
+
 fun atoms_ltlc_list :: "'a ltlc \<Rightarrow> 'a list"
 where
   "atoms_ltlc_list true\<^sub>c = []"
 | "atoms_ltlc_list false\<^sub>c = []"
 | "atoms_ltlc_list prop\<^sub>c(q) = [q]"
 | "atoms_ltlc_list (not\<^sub>c \<phi>) = atoms_ltlc_list \<phi>"
 | "atoms_ltlc_list (\<phi> and\<^sub>c \<psi>) = List.union (atoms_ltlc_list \<phi>) (atoms_ltlc_list \<psi>)"
 | "atoms_ltlc_list (\<phi> or\<^sub>c \<psi>) = List.union (atoms_ltlc_list \<phi>) (atoms_ltlc_list \<psi>)"
 | "atoms_ltlc_list (\<phi> implies\<^sub>c \<psi>) = List.union (atoms_ltlc_list \<phi>) (atoms_ltlc_list \<psi>)"
 | "atoms_ltlc_list (X\<^sub>c \<phi>) = atoms_ltlc_list \<phi>"
 | "atoms_ltlc_list (F\<^sub>c \<phi>) = atoms_ltlc_list \<phi>"
 | "atoms_ltlc_list (G\<^sub>c \<phi>) = atoms_ltlc_list \<phi>"
 | "atoms_ltlc_list (\<phi> U\<^sub>c \<psi>) = List.union (atoms_ltlc_list \<phi>) (atoms_ltlc_list \<psi>)"
 | "atoms_ltlc_list (\<phi> R\<^sub>c \<psi>) = List.union (atoms_ltlc_list \<phi>) (atoms_ltlc_list \<psi>)"
 | "atoms_ltlc_list (\<phi> W\<^sub>c \<psi>) = List.union (atoms_ltlc_list \<phi>) (atoms_ltlc_list \<psi>)"
 | "atoms_ltlc_list (\<phi> M\<^sub>c \<psi>) = List.union (atoms_ltlc_list \<phi>) (atoms_ltlc_list \<psi>)"
 
 lemma atoms_ltlc_list_set:
   "set (atoms_ltlc_list \<phi>) = atoms_ltlc \<phi>"
   by (induction \<phi>) simp_all
 
 lemma atoms_ltlc_list_distinct:
   "distinct (atoms_ltlc_list \<phi>)"
   by (induction \<phi>) simp_all
 
 definition ltl_alphabet :: "'a list \<Rightarrow> 'a set list"
 where
   "ltl_alphabet AP = map set (subseqs AP)"
 
-definition ltln_to_draei :: "'a list \<Rightarrow> ('a :: hashable) ltln \<Rightarrow> ('a set, nat) draei"
+
+subsection \<open>The Final Constant\<close>
+
+text \<open>
+  We require the quotient type to be hashable in order to efficiently explore the automaton.
+\<close>
+
+locale dra_implementation = dra_construction_size _ _ _ Abs
+  for
+    Abs :: "'a ltln \<Rightarrow> 'ltlq :: hashable"
+begin
+
+definition ltln_to_draei :: "'a list \<Rightarrow> 'a ltln \<Rightarrow> ('a set, nat) draei"
 where
   "ltln_to_draei AP \<phi> = drai_to_draei (Suc (size \<phi>)) (dra_to_drai (ltl_to_dra_alphabet \<phi> (set AP)) (ltl_alphabet AP))"
 
-definition ltlc_to_draei :: "('a :: hashable) ltlc \<Rightarrow> ('a set, nat) draei"
+definition ltlc_to_draei :: "'a ltlc \<Rightarrow> ('a set, nat) draei"
 where
   "ltlc_to_draei \<phi> = ltln_to_draei (atoms_ltlc_list \<phi>) (simplify Slow (ltlc_to_ltln \<phi>))"
 
 
-
-subsection \<open>Final Proof of Correctness\<close>
-
-lemma dra_to_drai_rel:
-  assumes
-    "(\<Sigma>, alphabet A) \<in> \<langle>Id\<rangle> list_set_rel"
-  shows
-    "(dra_to_drai A \<Sigma>, A) \<in> \<langle>Id, Id\<rangle>drai_dra_rel"
-proof -
-  have "(A, A) \<in> \<langle>Id, Id\<rangle>dra_rel"
-    by simp
-
-  then have "(dra_to_drai A \<Sigma>, dra (alphabet A) (initial A) (transition A) (condition A)) \<in> \<langle>Id, Id\<rangle>drai_dra_rel"
-    unfolding dra_to_drai_def using assms by parametricity
-
-  then show ?thesis
-    by simp
-qed
-
-lemma draei_language:
-  fixes
-    A :: "('label, 'state :: hashable) dra"
-  assumes
-    "(\<Sigma>, alphabet A) \<in> \<langle>Id\<rangle> list_set_rel"
-  and
-    "finite (DRA.nodes A)"
-  and
-    "is_valid_def_hm_size TYPE('state) hms"
-  shows
-    "DRA.language (drae_dra (draei_drae (drai_to_draei hms (dra_to_drai A \<Sigma>)))) = DRA.language A"
-proof -
-  have "(dra_to_drai A \<Sigma>, A) \<in> \<langle>Id, Id\<rangle>drai_dra_rel"
-    using dra_to_drai_rel assms by fast
-
-  then have "(drai_to_draei hms (dra_to_drai A \<Sigma>), to_draei A) \<in> \<langle>Id_on (dra.alphabet A), rel (dra_to_drai A \<Sigma>) A (=) bounded_hashcode_nat hms\<rangle> draei_dra_rel"
-    unfolding drai_to_draei_def
-    using to_draei_impl_refine[unfolded autoref_tag_defs]
-    by parametricity (simp_all add: assms is_bounded_hashcode_def bounded_hashcode_nat_bounds)
-
-  then have "(DRA.language ((drae_dra \<circ> draei_drae) (drai_to_draei hms (dra_to_drai A \<Sigma>))), DRA.language (id (to_draei A))) \<in> \<langle>\<langle>Id_on (dra.alphabet A)\<rangle> stream_rel\<rangle> set_rel"
-    by parametricity
-
-  then show ?thesis
-    by (simp add: to_draei_def)
-qed
-
-
 lemma ltl_to_dra_alphabet_rel:
   "distinct AP \<Longrightarrow> (ltl_alphabet AP, alphabet (ltl_to_dra_alphabet \<psi> (set AP))) \<in> \<langle>Id\<rangle> list_set_rel"
-  unfolding ltl_to_dra.ltl_to_dra_alphabet_alphabet ltl_alphabet_def
+  unfolding ltl_to_dra_alphabet_alphabet ltl_alphabet_def
   by (simp add: list_set_rel_def in_br_conv subseqs_powset distinct_set_subseqs)
 
-lemma ltl_to_dra_alphabet_nodes_finite:
-  "finite (DRA.nodes (ltl_to_dra_alphabet \<phi> AP))"
-  using ltl_to_dra.ltl_to_dra_alphabet_nodes ltl_to_dra_nodes_finite finite_subset by fast
-
 lemma ltlc_to_ltln_simplify_atoms:
   "atoms_ltln (simplify Slow (ltlc_to_ltln \<phi>)) \<subseteq> atoms_ltlc \<phi>"
   using ltlc_to_ltln_atoms simplify_atoms by fast
 
 lemma valid_def_hm_size:
   "is_valid_def_hm_size TYPE('state) (Suc (size \<phi>))" for \<phi> :: "'a ltln"
   unfolding is_valid_def_hm_size_def
   using ltln.size_neq by auto
 
 theorem final_correctness:
   "to_omega ` language (drae_dra (draei_drae (ltlc_to_draei \<phi>)))
     = language_ltlc \<phi> \<inter> {w. range w \<subseteq> Pow (atoms_ltlc \<phi>)}"
   unfolding ltlc_to_draei_def ltln_to_draei_def
-  unfolding draei_language[OF ltl_to_dra_alphabet_rel[OF atoms_ltlc_list_distinct] ltl_to_dra_alphabet_nodes_finite valid_def_hm_size]
+  unfolding draei_language_rel[OF ltl_to_dra_alphabet_rel[OF atoms_ltlc_list_distinct] ltl_to_dra_alphabet_nodes_finite valid_def_hm_size]
   unfolding atoms_ltlc_list_set
-  unfolding ltl_to_dra.ltl_to_dra_alphabet_language[OF ltlc_to_ltln_simplify_atoms]
+  unfolding ltl_to_dra_alphabet_language[OF ltlc_to_ltln_simplify_atoms]
   unfolding ltlc_to_ltln_atoms language_ltln_def language_ltlc_def ltlc_to_ltln_semantics simplify_correct ..
 
 end
+
+end
diff --git a/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Instantiation.thy b/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Instantiation.thy
--- a/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Instantiation.thy
+++ b/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Instantiation.thy
@@ -1,417 +1,163 @@
 (*
     Author:   Benedikt Seidl
     License:  BSD
 *)
 
 section \<open>Instantiation of the LTL to DRA construction\<close>
 
 theory DRA_Instantiation
 imports
-  DRA_Construction
+  DRA_Implementation
   LTL.Equivalence_Relations
+  LTL.Disjunctive_Normal_Form
+  "../Logical_Characterization/Extra_Equivalence_Relations"
   "HOL-Library.Log_Nat"
+  Deriving.Derive
 begin
 
-text \<open>We instantiate the construction locale with propositional equivalence
-      and obtain a function converting a formula into an abstract automaton.\<close>
-
-global_interpretation ltl_to_dra: dra_construction "(\<sim>\<^sub>P)" rep_ltln\<^sub>P abs_ltln\<^sub>P
-  defines ltl_to_dra = ltl_to_dra.ltl_to_dra
-    and ltl_to_dra_alphabet = ltl_to_dra.ltl_to_dra_alphabet
-    and \<AA>' = ltl_to_dra.\<AA>'
-    and \<AA>\<^sub>1 = ltl_to_dra.\<AA>\<^sub>1
-    and \<AA>\<^sub>2 = ltl_to_dra.\<AA>\<^sub>2
-    and \<AA>\<^sub>3 = ltl_to_dra.\<AA>\<^sub>3
-    and \<AA>\<^sub>\<nu>_FG = ltl_to_dra.\<AA>\<^sub>\<nu>_FG
-    and \<AA>\<^sub>\<mu>_GF = ltl_to_dra.\<AA>\<^sub>\<mu>_GF
-    and af_letter\<^sub>G = ltl_to_dra.af_letter\<^sub>G
-    and af_letter\<^sub>F = ltl_to_dra.af_letter\<^sub>F
-    and af_letter\<^sub>G_lifted = ltl_to_dra.af_letter\<^sub>G_lifted
-    and af_letter\<^sub>F_lifted = ltl_to_dra.af_letter\<^sub>F_lifted
-    and af_letter\<^sub>\<nu>_lifted = ltl_to_dra.af_letter\<^sub>\<nu>_lifted
-    and \<CC> = ltl_to_dra.\<CC>
-    and af_letter\<^sub>\<nu> = ltl_to_dra.af_letter\<^sub>\<nu>
-  by unfold_locales (meson Quotient_abs_rep Quotient_ltln\<^sub>P, simp add: Quotient_abs_rep Quotient_ltln\<^sub>P ltln\<^sub>P.abs_eq_iff)
-
-text \<open>We obtain the following theorem:\<close>
-
-thm ltl_to_dra.ltl_to_dra_language
-
-
-text \<open>Furthermore, we verify the size bound of the automaton to be double-exponential.\<close>
-
-lemma prop_equiv_nested_prop_atoms_finite:
-  "finite {abs_ltln\<^sub>P \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
-  using prop_equiv_finite'[OF nested_prop_atoms_finite] .
-
-lemma prop_equiv_nested_prop_atoms_card:
-  "card {abs_ltln\<^sub>P \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>} \<le> 2 ^ 2 ^ card (nested_prop_atoms \<phi>)"
-  using prop_equiv_card'[OF nested_prop_atoms_finite] .
-
-
-lemma prop_equiv_nested_prop_atoms\<^sub>\<nu>_finite:
-  "finite {abs_ltln\<^sub>P \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X}"
-  using prop_equiv_finite'[OF nested_prop_atoms\<^sub>\<nu>_finite] by fast
-
-lemma prop_equiv_nested_prop_atoms\<^sub>\<nu>_card:
-  "card {abs_ltln\<^sub>P \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X} \<le> 2 ^ 2 ^ card (nested_prop_atoms \<phi>)" (is "?lhs \<le> ?rhs")
-proof -
-  have "finite {abs_ltln\<^sub>P \<psi> | \<psi>. prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X}"
-    by (simp add: prop_equiv_nested_prop_atoms\<^sub>\<nu>_finite nested_prop_atoms\<^sub>\<nu>_finite prop_equiv_finite)
-
-  then have "?lhs \<le> card {abs_ltln\<^sub>P \<psi> | \<psi>. prop_atoms \<psi> \<subseteq> (nested_prop_atoms\<^sub>\<nu> \<phi> X)}"
-    using card_mono prop_equiv_subset by blast
-
-  also have "\<dots> \<le> 2 ^ 2 ^ card (nested_prop_atoms\<^sub>\<nu> \<phi> X)"
-    using prop_equiv_card[OF nested_prop_atoms\<^sub>\<nu>_finite] by fast
-
-  also have "\<dots> \<le> ?rhs"
-    using nested_prop_atoms\<^sub>\<nu>_card by auto
-
-  finally show ?thesis .
-qed
-
-
-lemma \<AA>\<^sub>\<mu>_GF_nodes_finite:
-  "finite (DBA.nodes (\<AA>\<^sub>\<mu>_GF \<phi>))"
-  using finite_subset[OF ltl_to_dra.\<AA>\<^sub>\<mu>_GF_nodes prop_equiv_nested_prop_atoms_finite] .
-
-lemma \<AA>\<^sub>\<nu>_FG_nodes_finite:
-  "finite (DCA.nodes (\<AA>\<^sub>\<nu>_FG \<phi>))"
-  using finite_subset[OF ltl_to_dra.\<AA>\<^sub>\<nu>_FG_nodes prop_equiv_nested_prop_atoms_finite] .
-
-lemma \<AA>\<^sub>\<mu>_GF_nodes_card:
-  "card (DBA.nodes (\<AA>\<^sub>\<mu>_GF \<phi>)) \<le> 2 ^ 2 ^ card (nested_prop_atoms (F\<^sub>n \<phi>))"
-  using le_trans[OF card_mono[OF prop_equiv_nested_prop_atoms_finite ltl_to_dra.\<AA>\<^sub>\<mu>_GF_nodes] prop_equiv_nested_prop_atoms_card] .
-
-lemma \<AA>\<^sub>\<nu>_FG_nodes_card:
-  "card (DCA.nodes (\<AA>\<^sub>\<nu>_FG \<phi>)) \<le> 2 ^ 2 ^ card (nested_prop_atoms (G\<^sub>n \<phi>))"
-  using le_trans[OF card_mono[OF prop_equiv_nested_prop_atoms_finite ltl_to_dra.\<AA>\<^sub>\<nu>_FG_nodes] prop_equiv_nested_prop_atoms_card] .
-
-
-lemma \<AA>\<^sub>2_nodes_finite_helper:
-  "list_all (finite \<circ> DBA.nodes) (map (\<lambda>\<psi>. \<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>)) xs)"
-  by (auto simp: list.pred_map list_all_iff \<AA>\<^sub>\<mu>_GF_nodes_finite)
-
-lemma \<AA>\<^sub>2_nodes_finite:
-  "finite (DBA.nodes (\<AA>\<^sub>2 xs ys))"
-  unfolding ltl_to_dra.\<AA>\<^sub>2_def using DBA_Combine.intersect_list_nodes_finite \<AA>\<^sub>2_nodes_finite_helper .
-
-lemma \<AA>\<^sub>3_nodes_finite_helper:
-  "list_all (finite \<circ> DCA.nodes) (map (\<lambda>\<psi>. \<AA>\<^sub>\<nu>_FG (\<psi>[set xs]\<^sub>\<nu>)) ys)"
-  by (auto simp: list.pred_map list_all_iff \<AA>\<^sub>\<nu>_FG_nodes_finite)
-
-lemma \<AA>\<^sub>3_nodes_finite:
-  "finite (DCA.nodes (\<AA>\<^sub>3 xs ys))"
-  unfolding ltl_to_dra.\<AA>\<^sub>3_def using DCA_Combine.intersect_list_nodes_finite \<AA>\<^sub>3_nodes_finite_helper .
+subsection \<open>Hash Functions for Quotient Types\<close>
 
-(* TODO add to HOL/Groups_List.thy *)
-lemma list_prod_mono:
-  "f \<le> g \<Longrightarrow> (\<Prod>x\<leftarrow>xs. f x) \<le> (\<Prod>x\<leftarrow>xs. g x)" for f g :: "'a \<Rightarrow> nat"
-  by (induction xs) (auto simp: le_funD mult_le_mono)
-
-(* TODO add to HOL/Groups_List.thy *)
-lemma list_prod_const:
-  "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> c) \<Longrightarrow> (\<Prod>x\<leftarrow>xs. f x) \<le> c ^ length xs" for f :: "'a \<Rightarrow> nat"
-  by (induction xs) (auto simp: mult_le_mono)
-
-(* TODO add to HOL/Finite_Set.thy *)
-lemma card_insert_Suc:
-  "card (insert x S) \<le> Suc (card S)"
-  by (metis Suc_n_not_le_n card.infinite card_insert_if finite_insert linear)
-
-(* TODO add to HOL/Power.thy *)
-lemma nat_power_le_imp_le:
-  "0 < a \<Longrightarrow> a \<le> b \<Longrightarrow> x ^ a \<le> x ^ b" for x :: nat
-  by (metis leD linorder_le_less_linear nat_power_less_imp_less neq0_conv power_eq_0_iff)
-
-(* TODO add to HOL/Power.thy *)
-lemma const_less_power:
-  "n < x ^ n" if "x > 1"
-  using that by (induction n) (auto simp: less_trans_Suc)
-
-(* TODO add to HOL-Library/Log_Nat.thy *)
-lemma floorlog_le_const:
-  "floorlog x n \<le> n"
-  by (induction n) (simp add: floorlog_eq_zero_iff, metis Suc_lessI floorlog_le_iff le_SucI power_inject_exp)
-
-lemma \<AA>\<^sub>2_nodes_card:
-  assumes
-    "length xs \<le> n"
-  and
-    "\<And>\<psi>. \<psi> \<in> set xs \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
-  shows
-    "card (DBA.nodes (\<AA>\<^sub>2 xs ys)) \<le> 2 ^ 2 ^ (n + floorlog 2 n + 2)"
-proof -
-  have 1: "\<And>\<psi>. \<psi> \<in> set xs \<Longrightarrow> card (nested_prop_atoms (F\<^sub>n \<psi>[set ys]\<^sub>\<mu>)) \<le> Suc n"
-  proof -
-    fix \<psi>
-    assume "\<psi> \<in> set xs"
-
-    have "card (nested_prop_atoms (F\<^sub>n (\<psi>[set ys]\<^sub>\<mu>)))
-          \<le> Suc (card (nested_prop_atoms (\<psi>[set ys]\<^sub>\<mu>)))"
-      by (simp add: card_insert_Suc)
+derive hashable ltln
 
-    also have "\<dots> \<le> Suc (card (nested_prop_atoms \<psi>))"
-      by (simp add: FG_advice_nested_prop_atoms_card)
-
-    also have "\<dots> \<le> Suc n"
-      by (simp add: assms(2) \<open>\<psi> \<in> set xs\<close>)
-
-    finally show "card (nested_prop_atoms (F\<^sub>n (\<psi>[set ys]\<^sub>\<mu>))) \<le> Suc n" .
-  qed
-
-  have "(\<Prod>\<psi>\<leftarrow>xs. card (DBA.nodes (\<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>))))
-        \<le> (\<Prod>\<psi>\<leftarrow>xs. 2 ^ 2 ^ card (nested_prop_atoms (F\<^sub>n (\<psi>[set ys]\<^sub>\<mu>))))"
-    by (rule list_prod_mono) (insert \<AA>\<^sub>\<mu>_GF_nodes_card le_fun_def, blast)
-
-  also have "\<dots> \<le> (2 ^ 2 ^ Suc n) ^ length xs"
-    by (rule list_prod_const) (metis 1 Suc_leI nat_power_le_imp_le nat_power_eq_Suc_0_iff neq0_conv pos2 zero_less_power)
-
-  also have "\<dots> \<le> (2 ^ 2 ^ Suc n) ^ n"
-    using assms(1) nat_power_le_imp_le by fastforce
-
-  also have "\<dots> = 2 ^ (n * 2 ^ Suc n)"
-    by (metis Groups.mult_ac(2) power_mult)
-
-  also have "\<dots> \<le> 2 ^ (2 ^ floorlog 2 n * 2 ^ Suc n)"
-    by (cases "n = 0") (auto simp: floorlog_bounds less_imp_le_nat)
-
-  also have "\<dots> = 2 ^ 2 ^ (Suc n + floorlog 2 n)"
-    by (simp add: power_add)
-
-  finally have 2: "(\<Prod>\<psi>\<leftarrow>xs. card (DBA.nodes (\<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>)))) \<le> 2 ^ 2 ^ (Suc n + floorlog 2 n)" .
-
-  have "card (DBA.nodes (\<AA>\<^sub>2 xs ys)) \<le> max 1 (length xs) * (\<Prod>\<psi>\<leftarrow>xs. card (DBA.nodes (\<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>))))"
-    using DBA_Combine.intersect_list_nodes_card[OF \<AA>\<^sub>2_nodes_finite_helper]
-    by (auto simp: ltl_to_dra.\<AA>\<^sub>2_def comp_def)
-
-  also have "\<dots> \<le> max 1 n * 2 ^ 2 ^ (Suc n + floorlog 2 n)"
-    using assms(1) 2 by (simp add: mult_le_mono)
-
-  also have "\<dots> \<le> 2 ^ (floorlog 2 n) * 2 ^ 2 ^ (Suc n + floorlog 2 n)"
-    by (cases "n = 0") (auto simp: floorlog_bounds less_imp_le_nat)
-
-  also have "\<dots> = 2 ^ (floorlog 2 n + 2 ^ (Suc n + floorlog 2 n))"
-    by (simp add: power_add)
-
-  also have "\<dots> \<le> 2 ^ (n + 2 ^ (Suc n + floorlog 2 n))"
-    by (simp add: floorlog_le_const)
-
-  also have "\<dots> \<le> 2 ^ 2 ^ (n + floorlog 2 n + 2)"
-    by simp (metis const_less_power Suc_1 add_Suc_right add_leE lessI less_imp_le_nat power_Suc)
-
-  finally show ?thesis .
-qed
+definition "cube a = a * a * a"
 
 
-lemma \<AA>\<^sub>3_nodes_card:
-  assumes
-    "length ys \<le> n"
-  and
-    "\<And>\<psi>. \<psi> \<in> set ys \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
-  shows
-    "card (DCA.nodes (\<AA>\<^sub>3 xs ys)) \<le> 2 ^ 2 ^ (n + floorlog 2 n + 1)"
-proof -
-  have 1: "\<And>\<psi>. \<psi> \<in> set ys \<Longrightarrow> card (DCA.nodes (\<AA>\<^sub>\<nu>_FG (\<psi>[set xs]\<^sub>\<nu>))) \<le> 2 ^ 2 ^ Suc n"
-  proof -
-    fix \<psi>
-    assume "\<psi> \<in> set ys"
-
-    have "card (nested_prop_atoms (G\<^sub>n \<psi>[set xs]\<^sub>\<nu>))
-          \<le> Suc (card (nested_prop_atoms (\<psi>[set xs]\<^sub>\<nu>)))"
-      by (simp add: card_insert_Suc)
-
-    also have "\<dots> \<le> Suc (card (nested_prop_atoms \<psi>))"
-      by (simp add: GF_advice_nested_prop_atoms_card)
-
-    also have "\<dots> \<le> Suc n"
-      by (simp add: assms(2) \<open>\<psi> \<in> set ys\<close>)
-
-    finally have 2: "card (nested_prop_atoms (G\<^sub>n \<psi>[set xs]\<^sub>\<nu>)) \<le> Suc n" .
+instantiation set :: (hashable) hashable
+begin
 
-    then show "?thesis \<psi>"
-      by (intro le_trans[OF \<AA>\<^sub>\<nu>_FG_nodes_card]) (meson one_le_numeral power_increasing)
-  qed
-
-
-  have "card (DCA.nodes (\<AA>\<^sub>3 xs ys)) \<le> (\<Prod>\<psi>\<leftarrow>ys. card (DCA.nodes (\<AA>\<^sub>\<nu>_FG (\<psi>[set xs]\<^sub>\<nu>))))"
-    unfolding ltl_to_dra.\<AA>\<^sub>3_def using DCA_Combine.intersect_list_nodes_card[OF \<AA>\<^sub>3_nodes_finite_helper]
-    by (auto simp: comp_def)
-
-  also have "\<dots> \<le> (2 ^ 2 ^ Suc n) ^ length ys"
-    by (rule list_prod_const) (rule 1)
+definition [simp]: "hashcode (x :: 'a set) = Finite_Set.fold (plus o cube o hashcode) (uint32_of_nat (card x)) x"
+definition "def_hashmap_size = (\<lambda>_ :: 'a set itself. 2 * def_hashmap_size TYPE('a))"
 
-  also have "\<dots> \<le> (2 ^ 2 ^ Suc n) ^ n"
-    by (simp add: assms(1) power_increasing)
-
-  also have "\<dots> \<le> 2 ^ (n * 2 ^ Suc n)"
-    by (metis le_refl mult.commute power_mult)
-
-  also have "\<dots> \<le> 2 ^ (2 ^ floorlog 2 n * 2 ^ Suc n)"
-    by (cases \<open>n > 0\<close>) (simp_all add: floorlog_bounds less_imp_le_nat)
-
-  also have "\<dots> = 2 ^ 2 ^ (n + floorlog 2 n + 1)"
-    by (simp add: power_add)
-
-  finally show ?thesis .
+instance
+proof
+  from def_hashmap_size[where ?'a = "'a"]
+  show "1 < def_hashmap_size TYPE('a set)"
+    by (simp add: def_hashmap_size_set_def)
 qed
 
-
-lemma \<AA>\<^sub>1_nodes_finite:
-  "finite (DCA.nodes (\<AA>\<^sub>1 \<phi> xs))"
-  unfolding ltl_to_dra.\<AA>\<^sub>1_def
-  by (metis (no_types, lifting) finite_subset ltl_to_dra.\<CC>_nodes finite_SigmaI prop_equiv_nested_prop_atoms\<^sub>\<nu>_finite prop_equiv_nested_prop_atoms_finite)
-
-lemma \<AA>\<^sub>1_nodes_card:
-  assumes
-    "card (subfrmlsn \<phi>) \<le> n"
-  shows
-    "card (DCA.nodes (\<AA>\<^sub>1 \<phi> xs)) \<le> 2 ^ 2 ^ (n + 1)"
-proof -
-  let ?fst = "{abs_ltln\<^sub>P \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
-  let ?snd = "{abs_ltln\<^sub>P \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> (set xs)}"
-
-  have 1: "card (nested_prop_atoms \<phi>) \<le> n"
-    by (meson card_mono[OF subfrmlsn_finite nested_prop_atoms_subfrmlsn] assms le_trans)
-
-
-  have "card (DCA.nodes (\<AA>\<^sub>1 \<phi> xs)) \<le> card (?fst \<times> ?snd)"
-    unfolding ltl_to_dra.\<AA>\<^sub>1_def
-    by (rule card_mono) (simp_all add: ltl_to_dra.\<CC>_nodes prop_equiv_nested_prop_atoms\<^sub>\<nu>_finite prop_equiv_nested_prop_atoms_finite)
-
-  also have "\<dots> = card ?fst * card ?snd"
-    using prop_equiv_nested_prop_atoms\<^sub>\<nu>_finite card_cartesian_product by blast
-
-  also have "\<dots> \<le> 2 ^ 2 ^ card (nested_prop_atoms \<phi>) * 2 ^ 2 ^ card (nested_prop_atoms \<phi>)"
-    using prop_equiv_nested_prop_atoms\<^sub>\<nu>_card prop_equiv_nested_prop_atoms_card mult_le_mono by blast
-
-  also have "\<dots> = 2 ^ 2 ^ (card (nested_prop_atoms \<phi>) + 1)"
-    by (simp add: semiring_normalization_rules(36))
-
-  also have "\<dots> \<le> 2 ^ 2 ^ (n + 1)"
-    using assms 1 by simp
-
-  finally show ?thesis .
-qed
+end
 
 
-lemma \<AA>'_nodes_finite:
-  "finite (DRA.nodes (\<AA>' \<phi> xs ys))"
-  unfolding ltl_to_dra.\<AA>'_def
-  using intersect_nodes_finite intersect_bc_nodes_finite
-  using \<AA>\<^sub>1_nodes_finite \<AA>\<^sub>2_nodes_finite \<AA>\<^sub>3_nodes_finite
-  by fast
-
-lemma \<AA>'_nodes_card:
-  assumes
-    "length xs \<le> n"
-  and
-    "\<And>\<psi>. \<psi> \<in> set xs \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
-  and
-    "length ys \<le> n"
-  and
-    "\<And>\<psi>. \<psi> \<in> set ys \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
-  and
-    "card (subfrmlsn \<phi>) \<le> n"
-  shows
-    "card (DRA.nodes (\<AA>' \<phi> xs ys)) \<le> 2 ^ 2 ^ (n + floorlog 2 n + 4)"
-proof -
-  have "n + 1 \<le> n + floorlog 2 n + 2"
-    by auto
+instantiation fset :: (hashable) hashable
+begin
 
-  then have 1: "(2::nat) ^ (n + 1) \<le> 2 ^ (n + floorlog 2 n + 2)"
-    using one_le_numeral power_increasing by blast
-
-
-  have "card (DRA.nodes (\<AA>' \<phi> xs ys)) \<le> card (DCA.nodes (\<AA>\<^sub>1 \<phi> xs)) * card (DBA.nodes (\<AA>\<^sub>2 xs ys)) * card (DCA.nodes (\<AA>\<^sub>3 xs ys))" (is "?lhs \<le> ?rhs")
-  proof (unfold ltl_to_dra.\<AA>'_def)
-    have "card (DBA.nodes (\<AA>\<^sub>2 xs ys)) * card (DCA.nodes (DCA_Combine.intersect (\<AA>\<^sub>1 \<phi> xs) (\<AA>\<^sub>3 xs ys))) \<le> ?rhs"
-      by (simp add: intersect_nodes_card[OF \<AA>\<^sub>1_nodes_finite \<AA>\<^sub>3_nodes_finite])
-    then show "card (DRA.nodes (intersect_bc (\<AA>\<^sub>2 xs ys) (DCA_Combine.intersect (\<AA>\<^sub>1 \<phi> xs) (\<AA>\<^sub>3 xs ys)))) \<le> ?rhs"
-      by (meson intersect_bc_nodes_card[OF \<AA>\<^sub>2_nodes_finite intersect_nodes_finite[OF \<AA>\<^sub>1_nodes_finite \<AA>\<^sub>3_nodes_finite]] basic_trans_rules(23))
-  qed
+definition [simp]: "hashcode (x :: 'a fset) = hashcode (fset x)"
+definition "def_hashmap_size = (\<lambda>_ :: 'a fset itself. 2 * def_hashmap_size TYPE('a))"
 
-  also have "\<dots> \<le> 2 ^ 2 ^ (n + 1) * 2 ^ 2 ^ (n + floorlog 2 n + 2) * 2 ^ 2 ^ (n + floorlog 2 n + 1)"
-    using \<AA>\<^sub>1_nodes_card[OF assms(5)] \<AA>\<^sub>2_nodes_card[OF assms(1,2)] \<AA>\<^sub>3_nodes_card[OF assms(3,4)]
-    by (metis mult_le_mono)
-
-  also have "\<dots> = 2 ^ (2 ^ (n + 1) + 2 ^ (n + floorlog 2 n + 2) + 2 ^ (n + floorlog 2 n + 1))"
-    by (metis power_add)
-
-  also have "\<dots> \<le> 2 ^ (4 * 2 ^ (n + floorlog 2 n + 2))"
-    using 1 by auto
-
-  finally show ?thesis
-    by (simp add: numeral.simps(2) power_add)
+instance
+proof
+  from def_hashmap_size[where ?'a = "'a"]
+  show "1 < def_hashmap_size TYPE('a fset)"
+    by (simp add: def_hashmap_size_fset_def)
 qed
 
-lemma subformula_nested_prop_atoms_subfrmlsn:
-  "\<psi> \<in> subfrmlsn \<phi> \<Longrightarrow> nested_prop_atoms \<psi> \<subseteq> subfrmlsn \<phi>"
-  using nested_prop_atoms_subfrmlsn subfrmlsn_subset by blast
+end
 
 
-lemma ltl_to_dra_nodes_finite:
-  "finite (DRA.nodes (ltl_to_dra \<phi>))"
-  unfolding ltl_to_dra.ltl_to_dra_def
-  apply (rule DRA_Combine.union_list_nodes_finite)
-  apply (simp add: split_def ltl_to_dra.\<AA>'_alphabet advice_sets_not_empty)
-  apply (simp add: list.pred_set split_def \<AA>'_nodes_finite)
-  done
-
-lemma ltl_to_dra_nodes_card:
-  assumes
-    "card (subfrmlsn \<phi>) \<le> n"
-  shows
-    "card (DRA.nodes (ltl_to_dra \<phi>)) \<le> 2 ^ 2 ^ (2 * n + floorlog 2 n + 4)"
-proof -
-  let ?map = "map (\<lambda>(x, y). \<AA>' \<phi> x y) (advice_sets \<phi>)"
-
-  have 1: "\<And>x::nat. x > 0 \<Longrightarrow> x ^ length (advice_sets \<phi>) \<le> x ^ 2 ^ card (subfrmlsn \<phi>)"
-    by (metis advice_sets_length linorder_not_less nat_power_less_imp_less)
-
-  have "card (DRA.nodes (ltl_to_dra \<phi>)) \<le> prod_list (map (card \<circ> DRA.nodes) ?map)"
-    unfolding ltl_to_dra.ltl_to_dra_def
-    apply (rule DRA_Combine.union_list_nodes_card)
-    unfolding list.pred_set using \<AA>'_nodes_finite by auto
-
-  also have "\<dots> = (\<Prod>(x, y)\<leftarrow>advice_sets \<phi>. card (DRA.nodes (\<AA>' \<phi> x y)))"
-    by (induction "advice_sets \<phi>") (auto, metis (no_types, lifting) comp_apply split_def)
+instantiation ltln\<^sub>P:: (hashable) hashable
+begin
 
-  also have "\<dots> \<le> (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ length (advice_sets \<phi>)"
-  proof (rule list_prod_const, unfold split_def, rule \<AA>'_nodes_card)
-    show "\<And>x. x \<in> set (advice_sets \<phi>) \<Longrightarrow> length (fst x) \<le> n"
-      using advice_sets_element_length assms by fastforce
-
-    show "\<And>x \<psi>. \<lbrakk>x \<in> set (advice_sets \<phi>); \<psi> \<in> set (fst x)\<rbrakk> \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
-      using advice_sets_element_subfrmlsn(1) assms subformula_nested_prop_atoms_subfrmlsn subformulas\<^sub>\<mu>_subfrmlsn
-      by (metis (no_types, lifting) card_mono subfrmlsn_finite subset_iff sup.absorb_iff2 sup.coboundedI1 surjective_pairing)
-
-    show "\<And>x. x \<in> set (advice_sets \<phi>) \<Longrightarrow> length (snd x) \<le> n"
-      using advice_sets_element_length assms by fastforce
+definition [simp]: "hashcode (\<phi> :: 'a ltln\<^sub>P) = hashcode (min_dnf (rep_ltln\<^sub>P \<phi>))"
+definition "def_hashmap_size = (\<lambda>_ :: 'a ltln\<^sub>P itself. def_hashmap_size TYPE('a ltln))"
 
-    show "\<And>x \<psi>. \<lbrakk>x \<in> set (advice_sets \<phi>); \<psi> \<in> set (snd x)\<rbrakk> \<Longrightarrow> card (nested_prop_atoms \<psi>) \<le> n"
-      using advice_sets_element_subfrmlsn(2) assms subformula_nested_prop_atoms_subfrmlsn subformulas\<^sub>\<nu>_subfrmlsn
-      by (metis (no_types, lifting) card_mono subfrmlsn_finite subset_iff sup.absorb_iff2 sup.coboundedI1 surjective_pairing)
-  qed (insert assms, blast)
-
-  also have "\<dots> \<le> (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ (2 ^ card (subfrmlsn \<phi>))"
-    by (simp add: 1)
-
-  also have "\<dots> \<le> (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ (2 ^ n)"
-    by (simp add: assms power_increasing)
-
-  also have "\<dots> = 2 ^ (2 ^ n * 2 ^ (n + floorlog 2 n + 4))"
-    by (simp add: ac_simps power_mult [symmetric])
-
-  also have "\<dots> = 2 ^ 2 ^ (2 * n + floorlog 2 n + 4)"
-    by (simp add: power_add) (simp add: mult_2 power_add)
-
-  finally show ?thesis .
+instance
+proof
+  from def_hashmap_size[where ?'a = "'a"]
+  show "1 < def_hashmap_size TYPE('a ltln\<^sub>P)"
+    by (simp add: def_hashmap_size_ltln\<^sub>P_def def_hashmap_size_ltln_def)
 qed
 
-theorem ltl_to_dra_size:
-  "card (DRA.nodes (ltl_to_dra \<phi>)) \<le> 2 ^ 2 ^ (2 * size \<phi> + floorlog 2 (size \<phi>) + 4)"
-  using ltl_to_dra_nodes_card subfrmlsn_card by blast
+end
+
+
+instantiation ltln\<^sub>Q :: (hashable) hashable
+begin
+
+definition [simp]: "hashcode (\<phi> :: 'a ltln\<^sub>Q) = hashcode (min_dnf (Unf (rep_ltln\<^sub>Q \<phi>)))"
+definition "def_hashmap_size = (\<lambda>_ :: 'a ltln\<^sub>Q itself. def_hashmap_size TYPE('a ltln))"
+
+instance
+proof
+  from def_hashmap_size[where ?'a = "'a"]
+  show "1 < def_hashmap_size TYPE('a ltln\<^sub>Q)"
+    by (simp add: def_hashmap_size_ltln\<^sub>Q_def def_hashmap_size_ltln_def)
+qed
 
 end
+
+
+subsection \<open>Interpretations with Equivalence Relations\<close>
+
+text \<open>
+  We instantiate the construction locale with propositional equivalence
+  and obtain a function converting a formula into an abstract automaton.
+\<close>
+
+global_interpretation ltl_to_dra\<^sub>P: dra_implementation "(\<sim>\<^sub>P)" id rep_ltln\<^sub>P abs_ltln\<^sub>P
+  defines ltl_to_dra\<^sub>P = ltl_to_dra\<^sub>P.ltl_to_dra
+    and ltl_to_dra_restricted\<^sub>P = ltl_to_dra\<^sub>P.ltl_to_dra_restricted
+    and ltl_to_dra_alphabet\<^sub>P = ltl_to_dra\<^sub>P.ltl_to_dra_alphabet
+    and \<AA>'\<^sub>P = ltl_to_dra\<^sub>P.\<AA>'
+    and \<AA>\<^sub>1\<^sub>P = ltl_to_dra\<^sub>P.\<AA>\<^sub>1
+    and \<AA>\<^sub>2\<^sub>P = ltl_to_dra\<^sub>P.\<AA>\<^sub>2
+    and \<AA>\<^sub>3\<^sub>P = ltl_to_dra\<^sub>P.\<AA>\<^sub>3
+    and \<AA>\<^sub>\<nu>_FG\<^sub>P = ltl_to_dra\<^sub>P.\<AA>\<^sub>\<nu>_FG
+    and \<AA>\<^sub>\<mu>_GF\<^sub>P = ltl_to_dra\<^sub>P.\<AA>\<^sub>\<mu>_GF
+    and af_letter\<^sub>G\<^sub>P = ltl_to_dra\<^sub>P.af_letter\<^sub>G
+    and af_letter\<^sub>F\<^sub>P = ltl_to_dra\<^sub>P.af_letter\<^sub>F
+    and af_letter\<^sub>G_lifted\<^sub>P = ltl_to_dra\<^sub>P.af_letter\<^sub>G_lifted
+    and af_letter\<^sub>F_lifted\<^sub>P = ltl_to_dra\<^sub>P.af_letter\<^sub>F_lifted
+    and af_letter\<^sub>\<nu>_lifted\<^sub>P = ltl_to_dra\<^sub>P.af_letter\<^sub>\<nu>_lifted
+    and \<CC>\<^sub>P = ltl_to_dra\<^sub>P.\<CC>
+    and af_letter\<^sub>\<nu>\<^sub>P = ltl_to_dra\<^sub>P.af_letter\<^sub>\<nu>
+    and ltln_to_draei\<^sub>P = ltl_to_dra\<^sub>P.ltln_to_draei
+    and ltlc_to_draei\<^sub>P = ltl_to_dra\<^sub>P.ltlc_to_draei
+  by unfold_locales (meson Quotient_abs_rep Quotient_ltln\<^sub>P, simp_all add: Quotient_abs_rep Quotient_ltln\<^sub>P ltln\<^sub>P.abs_eq_iff prop_equiv_card prop_equiv_finite)
+
+thm ltl_to_dra\<^sub>P.ltl_to_dra_language
+thm ltl_to_dra\<^sub>P.ltl_to_dra_size
+thm ltl_to_dra\<^sub>P.final_correctness
+
+text \<open>
+  Similarly, we instantiate the locale with a different equivalence relation and obtain another
+  constant for translation of LTL to deterministic Rabin automata.
+\<close>
+
+global_interpretation ltl_to_dra\<^sub>Q: dra_implementation "(\<sim>\<^sub>Q)" Unf rep_ltln\<^sub>Q abs_ltln\<^sub>Q
+  defines ltl_to_dra\<^sub>Q = ltl_to_dra\<^sub>Q.ltl_to_dra
+    and ltl_to_dra_restricted\<^sub>Q = ltl_to_dra\<^sub>Q.ltl_to_dra_restricted
+    and ltl_to_dra_alphabet\<^sub>Q = ltl_to_dra\<^sub>Q.ltl_to_dra_alphabet
+    and \<AA>'\<^sub>Q = ltl_to_dra\<^sub>Q.\<AA>'
+    and \<AA>\<^sub>1\<^sub>Q = ltl_to_dra\<^sub>Q.\<AA>\<^sub>1
+    and \<AA>\<^sub>2\<^sub>Q = ltl_to_dra\<^sub>Q.\<AA>\<^sub>2
+    and \<AA>\<^sub>3\<^sub>Q = ltl_to_dra\<^sub>Q.\<AA>\<^sub>3
+    and \<AA>\<^sub>\<nu>_FG\<^sub>Q = ltl_to_dra\<^sub>Q.\<AA>\<^sub>\<nu>_FG
+    and \<AA>\<^sub>\<mu>_GF\<^sub>Q = ltl_to_dra\<^sub>Q.\<AA>\<^sub>\<mu>_GF
+    and af_letter\<^sub>G\<^sub>Q = ltl_to_dra\<^sub>Q.af_letter\<^sub>G
+    and af_letter\<^sub>F\<^sub>Q = ltl_to_dra\<^sub>Q.af_letter\<^sub>F
+    and af_letter\<^sub>G_lifted\<^sub>Q = ltl_to_dra\<^sub>Q.af_letter\<^sub>G_lifted
+    and af_letter\<^sub>F_lifted\<^sub>Q = ltl_to_dra\<^sub>Q.af_letter\<^sub>F_lifted
+    and af_letter\<^sub>\<nu>_lifted\<^sub>Q = ltl_to_dra\<^sub>Q.af_letter\<^sub>\<nu>_lifted
+    and \<CC>\<^sub>Q = ltl_to_dra\<^sub>Q.\<CC>
+    and af_letter\<^sub>\<nu>\<^sub>Q = ltl_to_dra\<^sub>Q.af_letter\<^sub>\<nu>
+    and ltln_to_draei\<^sub>Q = ltl_to_dra\<^sub>Q.ltln_to_draei
+    and ltlc_to_draei\<^sub>Q = ltl_to_dra\<^sub>Q.ltlc_to_draei
+  by unfold_locales (meson Quotient_abs_rep Quotient_ltln\<^sub>Q, simp_all add: Quotient_abs_rep Quotient_ltln\<^sub>Q ltln\<^sub>Q.abs_eq_iff nested_prop_atoms_Unf prop_unfold_equiv_finite prop_unfold_equiv_card)
+
+thm ltl_to_dra\<^sub>Q.ltl_to_dra_language
+thm ltl_to_dra\<^sub>Q.ltl_to_dra_size
+thm ltl_to_dra\<^sub>Q.final_correctness
+
+
+text \<open>
+  We allow the user to choose one of the two equivalence relations.
+\<close>
+
+datatype equiv = Prop | PropUnfold
+
+fun ltlc_to_draei :: "equiv \<Rightarrow> ('a :: hashable) ltlc \<Rightarrow> ('a set, nat) draei"
+where
+  "ltlc_to_draei Prop = ltlc_to_draei\<^sub>P"
+| "ltlc_to_draei PropUnfold = ltlc_to_draei\<^sub>Q"
+
+end
diff --git a/thys/LTL_Master_Theorem/LTL_to_DRA/Transition_Functions.thy b/thys/LTL_Master_Theorem/LTL_to_DRA/Transition_Functions.thy
--- a/thys/LTL_Master_Theorem/LTL_to_DRA/Transition_Functions.thy
+++ b/thys/LTL_Master_Theorem/LTL_to_DRA/Transition_Functions.thy
@@ -1,592 +1,609 @@
 (*
     Author:   Benedikt Seidl
     License:  BSD
 *)
 
 section \<open>Transition Functions for Deterministic Automata\<close>
 
 theory Transition_Functions
 imports
   "../Logical_Characterization/After"
   "../Logical_Characterization/Advice"
 begin
 
-text \<open>This theory defines three functions based on the ``after''-function
-      which we use as transition functions for deterministic automata.\<close>
+text \<open>
+  This theory defines three functions based on the ``after''-function
+  which we use as transition functions for deterministic automata.
+\<close>
 
 locale transition_functions =
   af_congruent + GF_advice_congruent
 begin
 
 subsection \<open>After Functions with Resets for @{term "GF(\<mu>LTL)"} and @{term "FG(\<nu>LTL)"}\<close>
 
 definition af_letter\<^sub>F :: "'a ltln \<Rightarrow> 'a ltln \<Rightarrow> 'a set \<Rightarrow> 'a ltln"
 where
   "af_letter\<^sub>F \<phi> \<psi> \<nu> = (if \<psi> \<sim> true\<^sub>n then F\<^sub>n \<phi> else af_letter \<psi> \<nu>)"
 
 definition af_letter\<^sub>G :: "'a ltln \<Rightarrow> 'a ltln \<Rightarrow> 'a set \<Rightarrow> 'a ltln"
 where
   "af_letter\<^sub>G \<phi> \<psi> \<nu> = (if \<psi> \<sim> false\<^sub>n then G\<^sub>n \<phi> else af_letter \<psi> \<nu>)"
 
 abbreviation af\<^sub>F :: "'a ltln \<Rightarrow> 'a ltln \<Rightarrow> 'a set list \<Rightarrow> 'a ltln"
 where
   "af\<^sub>F \<phi> \<psi> w \<equiv> foldl (af_letter\<^sub>F \<phi>) \<psi> w"
 
 abbreviation af\<^sub>G :: "'a ltln \<Rightarrow> 'a ltln \<Rightarrow> 'a set list \<Rightarrow> 'a ltln"
 where
   "af\<^sub>G \<phi> \<psi> w \<equiv> foldl (af_letter\<^sub>G \<phi>) \<psi> w"
 
 
-lemma af_letter\<^sub>F_nested_prop_atoms:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> nested_prop_atoms (af_letter\<^sub>F \<phi> \<psi> \<nu>) \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)"
-  by (induction \<psi>) (auto simp: af_letter\<^sub>F_def, insert af_letter_nested_prop_atoms, blast+)
-
-lemma af\<^sub>F_nested_prop_atoms:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> nested_prop_atoms (af\<^sub>F \<phi> \<psi> w) \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)"
-  by (induction w rule: rev_induct) (insert af_letter\<^sub>F_nested_prop_atoms, auto)
-
-lemma af_letter\<^sub>F_range:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> range (af_letter\<^sub>F \<phi> \<psi>) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
-  using af_letter\<^sub>F_nested_prop_atoms by blast
-
-lemma af\<^sub>F_range:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> range (af\<^sub>F \<phi> \<psi>) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
-  using af\<^sub>F_nested_prop_atoms by blast
-
-
-lemma af_letter\<^sub>G_nested_prop_atoms:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> nested_prop_atoms (af_letter\<^sub>G \<phi> \<psi> \<nu>) \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)"
-  by (induction \<psi>) (auto simp: af_letter\<^sub>G_def, insert af_letter_nested_prop_atoms, blast+)
-
-lemma af\<^sub>G_nested_prop_atoms:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> nested_prop_atoms (af\<^sub>G \<phi> \<psi> w) \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)"
-  by (induction w rule: rev_induct) (insert af_letter\<^sub>G_nested_prop_atoms, auto)
-
-lemma af_letter\<^sub>G_range:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> range (af_letter\<^sub>G \<phi> \<psi>) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
-  using af_letter\<^sub>G_nested_prop_atoms by blast
-
-lemma af\<^sub>G_range:
-  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> range (af\<^sub>G \<phi> \<psi>) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
-  using af\<^sub>G_nested_prop_atoms by blast
-
-
 lemma af\<^sub>F_step:
   "af\<^sub>F \<phi> \<psi> w \<sim> true\<^sub>n \<Longrightarrow> af\<^sub>F \<phi> \<psi> (w @ [\<nu>]) = F\<^sub>n \<phi>"
   by (induction w rule: rev_induct) (auto simp: af_letter\<^sub>F_def)
 
 lemma af\<^sub>G_step:
   "af\<^sub>G \<phi> \<psi> w \<sim> false\<^sub>n \<Longrightarrow> af\<^sub>G \<phi> \<psi> (w @ [\<nu>]) = G\<^sub>n \<phi>"
   by (induction w rule: rev_induct) (auto simp: af_letter\<^sub>G_def)
 
 lemma af\<^sub>F_segments:
   "af\<^sub>F \<phi> \<psi> w = F\<^sub>n \<phi> \<Longrightarrow> af\<^sub>F \<phi> \<psi> (w @ w') = af\<^sub>F \<phi> (F\<^sub>n \<phi>) w'"
   by simp
 
 lemma af\<^sub>G_segments:
   "af\<^sub>G \<phi> \<psi> w = G\<^sub>n \<phi> \<Longrightarrow> af\<^sub>G \<phi> \<psi> (w @ w') = af\<^sub>G \<phi> (G\<^sub>n \<phi>) w'"
   by simp
 
 
 lemma af_not_true_implies_af_equals_af\<^sub>F:
   "(\<And>xs ys. w = xs @ ys \<Longrightarrow> \<not> af \<psi> xs \<sim> true\<^sub>n) \<Longrightarrow> af\<^sub>F \<phi> \<psi> w = af \<psi> w"
 proof (induction w rule: rev_induct)
   case (snoc x xs)
 
   then have "af\<^sub>F \<phi> \<psi> xs = af \<psi> xs"
     by simp
 
   moreover
 
   have "\<not> af \<psi> xs \<sim> true\<^sub>n"
     using snoc.prems by blast
 
   ultimately show ?case
     by (metis af_letter\<^sub>F_def foldl_Cons foldl_Nil foldl_append)
 qed simp
 
 lemma af_not_false_implies_af_equals_af\<^sub>G:
   "(\<And>xs ys. w = xs @ ys \<Longrightarrow> \<not> af \<psi> xs \<sim> false\<^sub>n) \<Longrightarrow> af\<^sub>G \<phi> \<psi> w = af \<psi> w"
 proof (induction w rule: rev_induct)
   case (snoc x xs)
 
   then have "af\<^sub>G \<phi> \<psi> xs = af \<psi> xs"
     by simp
 
   moreover
 
   have "\<not> af \<psi> xs \<sim> false\<^sub>n"
     using snoc.prems by blast
 
   ultimately show ?case
     by (metis af_letter\<^sub>G_def foldl_Cons foldl_Nil foldl_append)
 qed simp
 
 
 lemma af\<^sub>F_not_true_implies_af_equals_af\<^sub>F:
   "(\<And>xs ys. w = xs @ ys \<Longrightarrow> \<not> af\<^sub>F \<phi> \<psi> xs \<sim> true\<^sub>n) \<Longrightarrow> af\<^sub>F \<phi> \<psi> w = af \<psi> w"
 proof (induction w rule: rev_induct)
   case (snoc x xs)
 
   then have "af\<^sub>F \<phi> \<psi> xs = af \<psi> xs"
     by simp
 
   moreover
 
   have "\<not> af\<^sub>F \<phi> \<psi> xs \<sim> true\<^sub>n"
     using snoc.prems by blast
 
   ultimately show ?case
     by (metis af_letter\<^sub>F_def foldl_Cons foldl_Nil foldl_append)
 qed simp
 
 lemma af\<^sub>G_not_false_implies_af_equals_af\<^sub>G:
   "(\<And>xs ys. w = xs @ ys \<Longrightarrow> \<not> af\<^sub>G \<phi> \<psi> xs \<sim> false\<^sub>n) \<Longrightarrow> af\<^sub>G \<phi> \<psi> w = af \<psi> w"
 proof (induction w rule: rev_induct)
   case (snoc x xs)
 
   then have "af\<^sub>G \<phi> \<psi> xs = af \<psi> xs"
     by simp
 
   moreover
 
   have "\<not> af\<^sub>G \<phi> \<psi> xs \<sim> false\<^sub>n"
     using snoc.prems by blast
 
   ultimately show ?case
     by (metis af_letter\<^sub>G_def foldl_Cons foldl_Nil foldl_append)
 qed simp
 
 
 lemma af\<^sub>F_true_implies_af_true:
   "af\<^sub>F \<phi> \<psi> w \<sim> true\<^sub>n \<Longrightarrow> af \<psi> w \<sim> true\<^sub>n"
   by (metis af_append_true af_not_true_implies_af_equals_af\<^sub>F)
 
 lemma af\<^sub>G_false_implies_af_false:
   "af\<^sub>G \<phi> \<psi> w \<sim> false\<^sub>n \<Longrightarrow> af \<psi> w \<sim> false\<^sub>n"
   by (metis af_append_false af_not_false_implies_af_equals_af\<^sub>G)
 
 
 lemma af_equiv_true_af\<^sub>F_prefix_true:
   "af \<psi> w \<sim> true\<^sub>n \<Longrightarrow> \<exists>xs ys. w = xs @ ys \<and> af\<^sub>F \<phi> \<psi> xs \<sim> true\<^sub>n"
 proof (induction w rule: rev_induct)
   case (snoc a w)
   then show ?case
   proof (cases "af \<psi> w \<sim> true\<^sub>n")
     case False
 
     then have "\<And>xs ys. w = xs @ ys \<Longrightarrow> \<not> af \<psi> xs \<sim> true\<^sub>n"
       using af_append_true by blast
 
     then have "af\<^sub>F \<phi> \<psi> w = af \<psi> w"
       using af_not_true_implies_af_equals_af\<^sub>F by auto
 
     then have "af\<^sub>F \<phi> \<psi> (w @ [a]) = af \<psi> (w @ [a])"
       by (simp add: False af_letter\<^sub>F_def)
 
     then show ?thesis
       by (metis append_Nil2 snoc.prems)
   qed (insert snoc, force)
 qed (simp add: const_implies_eq)
 
 lemma af_equiv_false_af\<^sub>G_prefix_false:
   "af \<psi> w \<sim> false\<^sub>n \<Longrightarrow> \<exists>xs ys. w = xs @ ys \<and> af\<^sub>G \<phi> \<psi> xs \<sim> false\<^sub>n"
 proof (induction w rule: rev_induct)
   case (snoc a w)
   then show ?case
   proof (cases "af \<psi> w \<sim> false\<^sub>n")
     case False
 
     then have "\<And>xs ys. w = xs @ ys \<Longrightarrow> \<not> af \<psi> xs \<sim> false\<^sub>n"
       using af_append_false by blast
 
     then have "af\<^sub>G \<phi> \<psi> w = af \<psi> w"
       using af_not_false_implies_af_equals_af\<^sub>G by auto
 
     then have "af\<^sub>G \<phi> \<psi> (w @ [a]) = af \<psi> (w @ [a])"
       by (simp add: False af_letter\<^sub>G_def)
 
     then show ?thesis
       by (metis append_Nil2 snoc.prems)
   qed (insert snoc, force)
 qed (simp add: const_implies_eq)
 
 
 lemma append_take_drop:
   "w = xs @ ys \<longleftrightarrow> xs = take (length xs) w \<and> ys = drop (length xs) w"
   by (metis append_eq_conv_conj)
 
 lemma subsequence_split:
   "(w [i \<rightarrow> j]) = xs @ ys \<Longrightarrow> xs = (w [i \<rightarrow> i + length xs])"
   by (simp add: append_take_drop) (metis add_diff_cancel_left' subsequence_length subsequence_prefix_suffix)
 
 lemma subsequence_append_general:
   "i \<le> k \<Longrightarrow> k \<le> j \<Longrightarrow> (w [i \<rightarrow> j]) = (w [i \<rightarrow> k]) @ (w [k \<rightarrow> j])"
   by (metis le_Suc_ex map_append subsequence_def upt_add_eq_append)
 
 
 lemma af\<^sub>F_semantics_rtl:
   assumes
     "\<forall>i. \<exists>j>i. af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> j]) \<sim> true\<^sub>n"
   shows
     "\<forall>i. \<exists>j. af (F\<^sub>n \<phi>) (w [i \<rightarrow> j]) \<sim>\<^sub>L true\<^sub>n"
 proof
   fix i
   from assms obtain j where "j > i" and "af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> j]) \<sim> true\<^sub>n"
     by blast
   then have X: "af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> Suc j]) = F\<^sub>n \<phi>"
     using af\<^sub>F_step by auto
 
-  obtain k where "k > j" and "af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> k]) \<sim> true\<^sub>n" 
+  obtain k where "k > j" and "af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> k]) \<sim> true\<^sub>n"
     using assms using Suc_le_eq by blast
   then have "af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [Suc j \<rightarrow> k]) \<sim> true\<^sub>n"
     using af\<^sub>F_segments[OF X] by (metis le_Suc_ex le_simps(3) subsequence_append)
   then have "af (F\<^sub>n \<phi>) (w [Suc j \<rightarrow> k]) \<sim> true\<^sub>n"
     using af\<^sub>F_true_implies_af_true by blast
   then show "\<exists>k. af (F\<^sub>n \<phi>) (w [i \<rightarrow> k]) \<sim>\<^sub>L true\<^sub>n"
     by (metis (full_types) af_F_prefix_lang_equiv_true eq_implies_lang subsequence_append_general Suc_le_eq \<open>i < j\<close> \<open>j < k\<close> less_SucI order.order_iff_strict)
 qed
 
 lemma af\<^sub>F_semantics_ltr:
   assumes
     "\<forall>i. \<exists>j. af (F\<^sub>n \<phi>) (w [i \<rightarrow> j]) \<sim> true\<^sub>n"
   shows
     "\<forall>i. \<exists>j>i. af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> j]) \<sim> true\<^sub>n"
 proof (rule ccontr)
   define resets where "resets = {i. af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> i]) \<sim> true\<^sub>n}"
   define m where "m = (if resets = {} then 0 else Suc (Max resets))"
 
   assume "\<not> (\<forall>i. \<exists>j>i. af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> j]) \<sim> true\<^sub>n)"
 
   then have "finite resets"
     using infinite_nat_iff_unbounded resets_def by force
   then have "resets \<noteq> {} \<Longrightarrow> af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> Max resets]) \<sim> true\<^sub>n"
     unfolding resets_def using Max_in by blast
   then have m_reset: "af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> m]) = F\<^sub>n \<phi>"
     unfolding m_def using af\<^sub>F_step by auto
 
   {
     fix i
     assume "i \<ge> m"
 
     with m_reset have "\<not> af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [0 \<rightarrow> i]) \<sim> true\<^sub>n"
       by (metis (mono_tags, lifting) Max_ge_iff Suc_n_not_le_n \<open>finite resets\<close> empty_Collect_eq m_def mem_Collect_eq resets_def)
     with m_reset have "\<not> af\<^sub>F \<phi>  (F\<^sub>n \<phi>)(w [m \<rightarrow> i]) \<sim> true\<^sub>n"
       by (metis (mono_tags, hide_lams) \<open>m \<le> i\<close> af\<^sub>F_segments bot_nat_def le0 subsequence_append_general)
   }
 
   then have "\<nexists>j. af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w [m \<rightarrow> j]) \<sim> true\<^sub>n"
     by (metis le_cases subseq_to_smaller)
   then have "\<nexists>j. af (F\<^sub>n \<phi>) (w [m \<rightarrow> j]) \<sim> true\<^sub>n"
     by (metis af_equiv_true_af\<^sub>F_prefix_true subsequence_split)
   then show False
     using assms by blast
 qed
 
 
 lemma af\<^sub>G_semantics_rtl:
   assumes
     "\<exists>i. \<forall>j>i. \<not> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> j]) \<sim> false\<^sub>n"
   shows
     "\<exists>i. \<forall>j. \<not> af (G\<^sub>n \<phi>) (w [i \<rightarrow> j]) \<sim> false\<^sub>n"
 proof
   define resets where "resets = {i. af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> i]) \<sim> false\<^sub>n}"
   define m where "m = (if resets = {} then 0 else Suc (Max resets))"
 
   from assms have "finite resets"
     by (metis (mono_tags, lifting) infinite_nat_iff_unbounded mem_Collect_eq resets_def)
   then have "resets \<noteq> {} \<Longrightarrow> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> Max resets]) \<sim> false\<^sub>n"
     unfolding resets_def using Max_in by blast
   then have m_reset: "af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> m]) = G\<^sub>n \<phi>"
     unfolding m_def using af\<^sub>G_step by auto
 
   {
     fix i
     assume "i \<ge> m"
 
     with m_reset have "\<not> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> i]) \<sim> false\<^sub>n"
       by (metis (mono_tags, lifting) Max_ge_iff Suc_n_not_le_n \<open>finite resets\<close> empty_Collect_eq m_def mem_Collect_eq resets_def)
     with m_reset have "\<not> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [m \<rightarrow> i]) \<sim> false\<^sub>n"
       by (metis (mono_tags, hide_lams) \<open>m \<le> i\<close> af\<^sub>G_segments bot_nat_def le0 subsequence_append_general)
   }
 
   then have "\<forall>j. \<not> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [m \<rightarrow> j]) \<sim> false\<^sub>n"
     by (metis le_cases subseq_to_smaller)
   then show "\<forall>j. \<not> af (G\<^sub>n \<phi>) (w [m \<rightarrow> j]) \<sim> false\<^sub>n"
     by (metis af_equiv_false_af\<^sub>G_prefix_false subsequence_split)
 qed
 
 lemma af\<^sub>G_semantics_ltr:
   assumes
     "\<exists>i. \<forall>j. \<not> af (G\<^sub>n \<phi>) (w [i \<rightarrow> j]) \<sim>\<^sub>L false\<^sub>n"
   shows
     "\<exists>i. \<forall>j>i. \<not> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> j]) \<sim> false\<^sub>n"
 proof (rule ccontr, auto)
   assume 1: "\<forall>i. \<exists>j>i. af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> j]) \<sim> false\<^sub>n"
 
   {
     fix i
     obtain j where "j > i" and "af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> j]) \<sim> false\<^sub>n"
       using 1 by blast
     then have X: "af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> Suc j]) = G\<^sub>n \<phi>"
       using af\<^sub>G_step by auto
 
     obtain k where "k > j" and "af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [0 \<rightarrow> k]) \<sim> false\<^sub>n"
       using 1 using Suc_le_eq by blast
     then have "af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w [Suc j \<rightarrow> k]) \<sim> false\<^sub>n"
       using af\<^sub>G_segments[OF X] by (metis le_Suc_ex le_simps(3) subsequence_append)
     then have "af (G\<^sub>n \<phi>) (w [Suc j \<rightarrow> k]) \<sim> false\<^sub>n"
       using af\<^sub>G_false_implies_af_false by fastforce
     then have "af (G\<^sub>n \<phi>) (w [Suc j \<rightarrow> k]) \<sim>\<^sub>L false\<^sub>n"
       using eq_implies_lang by fastforce
     then have "af (G\<^sub>n \<phi>) (w [i \<rightarrow> k]) \<sim>\<^sub>L false\<^sub>n"
       by (metis (full_types) af_G_prefix_lang_equiv_false subsequence_append_general Suc_le_eq \<open>i < j\<close> \<open>j < k\<close> less_SucI order.order_iff_strict)
     then have "\<exists>j. af (G\<^sub>n \<phi>) (w [i \<rightarrow> j]) \<sim>\<^sub>L false\<^sub>n"
       by fast
   }
 
   then show False
     using assms by blast
 qed
 
 
 
 subsection \<open>After Function using GF-advice\<close>
 
 definition af_letter\<^sub>\<nu> :: "'a ltln set \<Rightarrow> 'a ltln \<times> 'a ltln \<Rightarrow> 'a set \<Rightarrow> 'a ltln \<times> 'a ltln"
 where
   "af_letter\<^sub>\<nu> X p \<nu> = (if snd p \<sim> false\<^sub>n
-    then (af_letter (fst p) \<nu>, (af_letter (fst p) \<nu>)[X]\<^sub>\<nu>)
+    then (af_letter (fst p) \<nu>, (normalise (af_letter (fst p) \<nu>))[X]\<^sub>\<nu>)
     else (af_letter (fst p) \<nu>, af_letter (snd p) \<nu>))"
 
 abbreviation af\<^sub>\<nu> :: "'a ltln set \<Rightarrow> 'a ltln \<times> 'a ltln \<Rightarrow> 'a set list \<Rightarrow> 'a ltln \<times> 'a ltln"
 where
   "af\<^sub>\<nu> X p w \<equiv> foldl (af_letter\<^sub>\<nu> X) p w"
 
 lemma af_letter\<^sub>\<nu>_fst[simp]:
   "fst (af_letter\<^sub>\<nu> X p \<nu>) = af_letter (fst p) \<nu>"
   by (simp add: af_letter\<^sub>\<nu>_def)
 
 lemma af_letter\<^sub>\<nu>_snd[simp]:
-  "snd p \<sim> false\<^sub>n \<Longrightarrow> snd (af_letter\<^sub>\<nu> X p \<nu>) = (af_letter (fst p) \<nu>)[X]\<^sub>\<nu>"
+  "snd p \<sim> false\<^sub>n \<Longrightarrow> snd (af_letter\<^sub>\<nu> X p \<nu>) = (normalise (af_letter (fst p) \<nu>))[X]\<^sub>\<nu>"
   "\<not> (snd p) \<sim> false\<^sub>n \<Longrightarrow> snd (af_letter\<^sub>\<nu> X p \<nu>) = af_letter (snd p) \<nu>"
   by (simp_all add: af_letter\<^sub>\<nu>_def)
 
+lemma af\<^sub>\<nu>_fst:
+  "fst (af\<^sub>\<nu> X p w) = af (fst p) w"
+  by (induction w rule: rev_induct) simp+
+
+lemma af\<^sub>\<nu>_snd:
+  "\<not> af (snd p) w \<sim> false\<^sub>n \<Longrightarrow> snd (af\<^sub>\<nu> X p w) = af (snd p) w"
+  by (induction w rule: rev_induct) (simp_all, metis af_letter\<^sub>\<nu>_snd(2) af_letter.simps(2) af_letter_congruent)
+
+lemma af\<^sub>\<nu>_snd':
+  "\<forall>i. \<not> snd (af\<^sub>\<nu> X p (take i w)) \<sim> false\<^sub>n \<Longrightarrow> snd (af\<^sub>\<nu> X p w) = af (snd p) w"
+  by (induction w rule: rev_induct) (simp_all, metis af_letter\<^sub>\<nu>_snd(2) diff_is_0_eq foldl_Nil le_cases take_all take_eq_Nil)
+
+lemma af\<^sub>\<nu>_step:
+  "snd (af\<^sub>\<nu> X (\<xi>, \<zeta>) w) \<sim> false\<^sub>n \<Longrightarrow> snd (af\<^sub>\<nu> X (\<xi>, \<zeta>) (w @ [\<nu>])) = (normalise (af \<xi> (w @ [\<nu>])))[X]\<^sub>\<nu>"
+  by (simp add: af\<^sub>\<nu>_fst)
+
+lemma af\<^sub>\<nu>_segments:
+  "af\<^sub>\<nu> X (\<xi>, \<zeta>) w = (af \<xi> w, (af \<xi> w)[X]\<^sub>\<nu>) \<Longrightarrow> af\<^sub>\<nu> X (\<xi>, \<zeta>) (w @ w') = af\<^sub>\<nu> X (af \<xi> w, (af \<xi> w)[X]\<^sub>\<nu>) w'"
+  by (induction w' rule: rev_induct) fastforce+
+
+
+lemma af\<^sub>\<nu>_semantics_ltr:
+  assumes
+    "\<exists>i. suffix i w \<Turnstile>\<^sub>n (af \<phi> (prefix i w))[X]\<^sub>\<nu>"
+  shows
+    "\<exists>m. \<forall>k\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n"
+proof
+  define resets where "resets = {i. snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix i w)) \<sim> false\<^sub>n}"
+  define m where "m = (if resets = {} then 0 else Suc (Max resets))"
+
+  from assms obtain i where 1: "suffix i w \<Turnstile>\<^sub>n (af \<phi> (prefix i w))[X]\<^sub>\<nu>"
+    by blast
+
+  {
+    fix j
+    assume "i \<le> j" and "j \<in> resets"
+
+    let ?\<phi> = "af \<phi> (prefix (Suc j) w)"
+
+    from 1 have "\<forall>n. suffix n (suffix i w) \<Turnstile>\<^sub>n (normalise (af \<phi> (prefix i w @ prefix n (suffix i w))))[X]\<^sub>\<nu>"
+      using normalise_monotonic by (simp add: GF_advice_af)
+
+    then have "suffix (Suc j) w \<Turnstile>\<^sub>n (normalise (af \<phi> (prefix (Suc j) w)))[X]\<^sub>\<nu>"
+      by (metis (no_types) \<open>i \<le> j\<close> add.right_neutral le_SucI le_Suc_ex subsequence_append subsequence_shift suffix_suffix)
+
+    then have "\<forall>k>j. \<not> af ((normalise (af \<phi> (prefix (Suc j) w)))[X]\<^sub>\<nu>) (w [Suc j \<rightarrow> k]) \<sim> false\<^sub>n"
+      by (metis ltl_implies_satisfiable_prefix subsequence_prefix_suffix)
+
+    then have "\<forall>k>j. \<not> snd (af\<^sub>\<nu> X (?\<phi>, (normalise ?\<phi>)[X]\<^sub>\<nu>) (w [Suc j \<rightarrow> k])) \<sim> false\<^sub>n"
+      by (metis af\<^sub>\<nu>_snd snd_eqD)
+
+    moreover
+
+    {
+      have "fst (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix (Suc j) w)) = ?\<phi>"
+        by (simp add: af\<^sub>\<nu>_fst)
+
+      moreover
+
+      have "snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix j w)) \<sim> false\<^sub>n"
+        using \<open>j \<in> resets\<close> resets_def by blast
+
+      ultimately have "af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix (Suc j) w) = (?\<phi>, (normalise ?\<phi>)[X]\<^sub>\<nu>)"
+        by (metis (no_types) af\<^sub>\<nu>_step prod.collapse subseq_to_Suc zero_le)
+    }
+
+    ultimately have "\<forall>k>j. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) ((w [0 \<rightarrow> Suc j]) @ (w [Suc j \<rightarrow> k]))) \<sim> false\<^sub>n"
+      by (simp add: af\<^sub>\<nu>_segments)
+
+    then have "\<forall>k>j. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix k w)) \<sim> false\<^sub>n"
+      by (metis Suc_leI le0 subsequence_append_general)
+
+    then have "\<forall>k \<in> resets. k \<le> j"
+      using \<open>j \<in> resets\<close> resets_def le_less_linear by blast
+  }
+
+  then have "finite resets"
+    by (meson finite_nat_set_iff_bounded_le infinite_nat_iff_unbounded_le)
+
+  then have "resets \<noteq> {} \<Longrightarrow> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix (Max resets) w)) \<sim> false\<^sub>n"
+    using Max_in resets_def by blast
+
+  then have "\<forall>k\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix k w)) \<sim> false\<^sub>n"
+    by (metis (mono_tags, lifting) Max_ge Suc_n_not_le_n \<open>finite resets\<close> empty_Collect_eq m_def mem_Collect_eq order.trans resets_def)
+
+  then show "\<forall>k\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n"
+    using le_SucI by blast
+qed
+
+lemma af\<^sub>\<nu>_semantics_rtl:
+  assumes
+    "\<exists>n. \<forall>k\<ge>n. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n"
+  shows
+    "\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>"
+proof -
+  define resets where "resets = {i. snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix i w)) \<sim> false\<^sub>n}"
+  define m where "m = (if resets = {} then 0 else Suc (Max resets))"
+
+  from assms obtain n where "\<forall>k\<ge>n. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n"
+    by blast
+
+  then have "\<forall>k>n. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix k w)) \<sim> false\<^sub>n"
+    by (metis le_SucE lessE less_imp_le_nat)
+
+  then have "finite resets"
+    by (metis (mono_tags, lifting) infinite_nat_iff_unbounded mem_Collect_eq resets_def)
+
+  then have "\<forall>i\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix i w)) \<sim> false\<^sub>n"
+    unfolding resets_def m_def using Max_ge not_less_eq_eq by auto
+
+  then have "\<forall>i. \<not> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) ((w [0 \<rightarrow> m]) @ (w [m \<rightarrow> i]))) \<sim> false\<^sub>n"
+    by (metis le0 nat_le_linear subseq_to_smaller subsequence_append_general)
+
+  moreover
+
+  let ?\<phi> = "af \<phi> (prefix m w)"
+
+  have "resets \<noteq> {} \<Longrightarrow> snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix (Max resets) w)) \<sim> false\<^sub>n"
+    using Max_in \<open>finite resets\<close> resets_def by blast
+
+  then have prefix_\<phi>': "snd (af\<^sub>\<nu> X (\<phi>, (normalise \<phi>)[X]\<^sub>\<nu>) (prefix m w)) = (normalise ?\<phi>)[X]\<^sub>\<nu>"
+    by (auto simp: GF_advice_congruent m_def af\<^sub>\<nu>_fst)
+
+  ultimately have "\<forall>i. \<not> snd (af\<^sub>\<nu> X (?\<phi>, (normalise ?\<phi>)[X]\<^sub>\<nu>) (w [m \<rightarrow> i])) \<sim> false\<^sub>n"
+    by (metis af\<^sub>\<nu>_fst foldl_append fst_conv prod.collapse)
+
+  then have "\<forall>i. \<not> af ((normalise ?\<phi>)[X]\<^sub>\<nu>) (w [m \<rightarrow> i]) \<sim> false\<^sub>n"
+    by (metis prefix_\<phi>' af\<^sub>\<nu>_fst af\<^sub>\<nu>_snd' fst_conv prod.collapse subsequence_take)
+
+  then have "suffix m w \<Turnstile>\<^sub>n (normalise (af \<phi> (prefix m w)))[X]\<^sub>\<nu>"
+    by (metis GF_advice_\<nu>LTL(1) satisfiable_prefix_implies_\<nu>LTL add.right_neutral subsequence_shift)
+
+  from this[THEN normalise_eventually_equivalent]
+    show "\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>"
+    by (metis add.commute af_subsequence_append le_add1 le_add_same_cancel1 prefix_suffix_subsequence suffix_suffix)
+qed
+
+end
+
+
+subsection \<open>Reachability Bounds\<close>
+
+text \<open>
+  We show that the reach of each after-function is bounded by the atomic
+  propositions of the input formula.
+\<close>
+
+locale transition_functions_size = transition_functions +
+  assumes
+    normalise_nested_propos: "nested_prop_atoms \<phi> \<supseteq> nested_prop_atoms (normalise \<phi>)"
+begin
+
+lemma af_letter\<^sub>F_nested_prop_atoms:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> nested_prop_atoms (af_letter\<^sub>F \<phi> \<psi> \<nu>) \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)"
+  by (induction \<psi>) (auto simp: af_letter\<^sub>F_def, insert af_letter_nested_prop_atoms, blast+)
+
+lemma af\<^sub>F_nested_prop_atoms:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> nested_prop_atoms (af\<^sub>F \<phi> \<psi> w) \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)"
+  by (induction w rule: rev_induct) (insert af_letter\<^sub>F_nested_prop_atoms, auto)
+
+lemma af_letter\<^sub>F_range:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> range (af_letter\<^sub>F \<phi> \<psi>) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
+  using af_letter\<^sub>F_nested_prop_atoms by blast
+
+lemma af\<^sub>F_range:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> range (af\<^sub>F \<phi> \<psi>) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
+  using af\<^sub>F_nested_prop_atoms by blast
+
+lemma af_letter\<^sub>G_nested_prop_atoms:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> nested_prop_atoms (af_letter\<^sub>G \<phi> \<psi> \<nu>) \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)"
+  by (induction \<psi>) (auto simp: af_letter\<^sub>G_def, insert af_letter_nested_prop_atoms, blast+)
+
+lemma af\<^sub>G_nested_prop_atoms:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> nested_prop_atoms (af\<^sub>G \<phi> \<psi> w) \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)"
+  by (induction w rule: rev_induct) (insert af_letter\<^sub>G_nested_prop_atoms, auto)
+
+lemma af_letter\<^sub>G_range:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> range (af_letter\<^sub>G \<phi> \<psi>) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
+  using af_letter\<^sub>G_nested_prop_atoms by blast
+
+lemma af\<^sub>G_range:
+  "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> range (af\<^sub>G \<phi> \<psi>) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
+  using af\<^sub>G_nested_prop_atoms by blast
+
+lemma af_letter\<^sub>\<nu>_snd_nested_prop_atoms_helper:
+  "snd p \<sim> false\<^sub>n \<Longrightarrow> nested_prop_atoms (snd (af_letter\<^sub>\<nu> X p \<nu>)) \<subseteq> nested_prop_atoms\<^sub>\<nu> (fst p) X"
+  "\<not> snd p \<sim> false\<^sub>n \<Longrightarrow> nested_prop_atoms (snd (af_letter\<^sub>\<nu> X p \<nu>)) \<subseteq> nested_prop_atoms (snd p)"
+  by (simp_all add: af_letter_nested_prop_atoms nested_prop_atoms\<^sub>\<nu>_def)
+     (metis GF_advice_nested_prop_atoms\<^sub>\<nu> af_letter_nested_prop_atoms nested_prop_atoms\<^sub>\<nu>_subset dual_order.trans nested_prop_atoms\<^sub>\<nu>_def normalise_nested_propos)
+
 lemma af_letter\<^sub>\<nu>_fst_nested_prop_atoms:
   "nested_prop_atoms (fst (af_letter\<^sub>\<nu> X p \<nu>)) \<subseteq> nested_prop_atoms (fst p)"
   by (simp add: af_letter_nested_prop_atoms)
 
-lemma af_letter\<^sub>\<nu>_snd_nested_prop_atoms_helper:
-  "snd p \<sim> false\<^sub>n \<Longrightarrow> nested_prop_atoms (snd (af_letter\<^sub>\<nu> X p \<nu>)) \<subseteq> nested_prop_atoms\<^sub>\<nu> (fst p) X"
-  "\<not> snd p \<sim> false\<^sub>n \<Longrightarrow> nested_prop_atoms (snd (af_letter\<^sub>\<nu> X p \<nu>)) \<subseteq> nested_prop_atoms (snd p)"
-  by simp_all (insert GF_advice_nested_prop_atoms\<^sub>\<nu> af_letter_nested_prop_atoms nested_prop_atoms\<^sub>\<nu>_def, blast)
-
 lemma af_letter\<^sub>\<nu>_snd_nested_prop_atoms:
   "nested_prop_atoms (snd (af_letter\<^sub>\<nu> X p \<nu>)) \<subseteq> (nested_prop_atoms\<^sub>\<nu> (fst p) X) \<union> (nested_prop_atoms (snd p))"
   using af_letter\<^sub>\<nu>_snd_nested_prop_atoms_helper by blast
 
 lemma af_letter\<^sub>\<nu>_fst_range:
   "range (fst \<circ> af_letter\<^sub>\<nu> X p) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (fst p)}"
   using af_letter\<^sub>\<nu>_fst_nested_prop_atoms by force
 
 lemma af_letter\<^sub>\<nu>_snd_range:
   "range (snd \<circ> af_letter\<^sub>\<nu> X p) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> (nested_prop_atoms\<^sub>\<nu> (fst p) X) \<union> nested_prop_atoms (snd p)}"
   using af_letter\<^sub>\<nu>_snd_nested_prop_atoms by force
 
 lemma af_letter\<^sub>\<nu>_range:
   "range (af_letter\<^sub>\<nu> X p) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (fst p)} \<times> {\<psi>. nested_prop_atoms \<psi> \<subseteq> (nested_prop_atoms\<^sub>\<nu> (fst p) X) \<union> nested_prop_atoms (snd p)}"
 proof -
   have "range (af_letter\<^sub>\<nu> X p) \<subseteq> range (fst \<circ> af_letter\<^sub>\<nu> X p) \<times> range (snd \<circ> af_letter\<^sub>\<nu> X p)"
     by (simp add: image_subset_iff mem_Times_iff)
 
   also have "\<dots> \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (fst p)} \<times> {\<psi>. nested_prop_atoms \<psi> \<subseteq> (nested_prop_atoms\<^sub>\<nu> (fst p) X) \<union> nested_prop_atoms (snd p)}"
     using af_letter\<^sub>\<nu>_fst_range af_letter\<^sub>\<nu>_snd_range by blast
 
   finally show ?thesis .
 qed
 
-
 lemma af\<^sub>\<nu>_fst_nested_prop_atoms:
   "nested_prop_atoms (fst (af\<^sub>\<nu> X p w)) \<subseteq> nested_prop_atoms (fst p)"
   by (induction w rule: rev_induct) (auto, insert af_letter_nested_prop_atoms, blast)
 
 lemma af_letter_nested_prop_atoms\<^sub>\<nu>:
   "nested_prop_atoms\<^sub>\<nu> (af_letter \<phi> \<nu>) X \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X"
   by (induction \<phi>) (simp_all add: nested_prop_atoms\<^sub>\<nu>_def, blast+)
 
 lemma af\<^sub>\<nu>_fst_nested_prop_atoms\<^sub>\<nu>:
   "nested_prop_atoms\<^sub>\<nu> (fst (af\<^sub>\<nu> X p w)) X \<subseteq> nested_prop_atoms\<^sub>\<nu> (fst p) X"
   by (induction w rule: rev_induct) (auto, insert af_letter_nested_prop_atoms\<^sub>\<nu>, blast)
 
+lemma af\<^sub>\<nu>_fst_range:
+  "range (fst \<circ> af\<^sub>\<nu> X p) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (fst p)}"
+  using af\<^sub>\<nu>_fst_nested_prop_atoms by fastforce
+
 lemma af\<^sub>\<nu>_snd_nested_prop_atoms:
   "nested_prop_atoms (snd (af\<^sub>\<nu> X p w)) \<subseteq> (nested_prop_atoms\<^sub>\<nu> (fst p) X) \<union> (nested_prop_atoms (snd p))"
 proof (induction w arbitrary: p rule: rev_induct)
   case (snoc x xs)
 
   let ?p = "af\<^sub>\<nu> X p xs"
 
   have "nested_prop_atoms (snd (af\<^sub>\<nu> X p (xs @ [x]))) \<subseteq> (nested_prop_atoms\<^sub>\<nu> (fst ?p) X) \<union> (nested_prop_atoms (snd ?p))"
     by (simp add: af_letter\<^sub>\<nu>_snd_nested_prop_atoms)
 
   then show ?case
     using snoc af\<^sub>\<nu>_fst_nested_prop_atoms\<^sub>\<nu> by blast
 qed (simp add: nested_prop_atoms\<^sub>\<nu>_def)
 
-
-lemma af\<^sub>\<nu>_fst_range:
-  "range (fst \<circ> af\<^sub>\<nu> X p) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (fst p)}"
-  using af\<^sub>\<nu>_fst_nested_prop_atoms by fastforce
-
 lemma af\<^sub>\<nu>_snd_range:
   "range (snd \<circ> af\<^sub>\<nu> X p) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> (nested_prop_atoms\<^sub>\<nu> (fst p) X) \<union> nested_prop_atoms (snd p)}"
   using af\<^sub>\<nu>_snd_nested_prop_atoms by fastforce
 
 lemma af\<^sub>\<nu>_range:
   "range (af\<^sub>\<nu> X p) \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (fst p)} \<times> {\<psi>. nested_prop_atoms \<psi> \<subseteq> (nested_prop_atoms\<^sub>\<nu> (fst p) X) \<union> nested_prop_atoms (snd p)}"
 proof -
   have "range (af\<^sub>\<nu> X p) \<subseteq> range (fst \<circ> af\<^sub>\<nu> X p) \<times> range (snd \<circ> af\<^sub>\<nu> X p)"
     by (simp add: image_subset_iff mem_Times_iff)
 
   also have "\<dots> \<subseteq> {\<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (fst p)} \<times> {\<psi>. nested_prop_atoms \<psi> \<subseteq> (nested_prop_atoms\<^sub>\<nu> (fst p) X) \<union> nested_prop_atoms (snd p)}"
     using af\<^sub>\<nu>_fst_range af\<^sub>\<nu>_snd_range by blast
 
   finally show ?thesis .
 qed
 
-
-lemma af\<^sub>\<nu>_fst:
-  "fst (af\<^sub>\<nu> X p w) = af (fst p) w"
-  by (induction w rule: rev_induct) simp+
-
-lemma af\<^sub>\<nu>_snd:
-  "\<not> af (snd p) w \<sim> false\<^sub>n \<Longrightarrow> snd (af\<^sub>\<nu> X p w) = af (snd p) w"
-  by (induction w rule: rev_induct) (simp_all, metis af_letter\<^sub>\<nu>_snd(2) af_letter.simps(2) af_letter_congruent)
-
-lemma af\<^sub>\<nu>_snd':
-  "\<forall>i. \<not> snd (af\<^sub>\<nu> X p (take i w)) \<sim> false\<^sub>n \<Longrightarrow> snd (af\<^sub>\<nu> X p w) = af (snd p) w"
-  by (induction w rule: rev_induct) (simp_all, metis af_letter\<^sub>\<nu>_snd(2) diff_is_0_eq foldl_Nil le_cases take_all take_eq_Nil)
-
-lemma af\<^sub>\<nu>_step:
-  "snd (af\<^sub>\<nu> X (\<xi>, \<zeta>) w) \<sim> false\<^sub>n \<Longrightarrow> snd (af\<^sub>\<nu> X (\<xi>, \<zeta>) (w @ [\<nu>])) = (af \<xi> (w @ [\<nu>]))[X]\<^sub>\<nu>"
-  by (simp add: af\<^sub>\<nu>_fst)
-
-lemma af\<^sub>\<nu>_segments:
-  "af\<^sub>\<nu> X (\<xi>, \<zeta>) w = (af \<xi> w, (af \<xi> w)[X]\<^sub>\<nu>) \<Longrightarrow> af\<^sub>\<nu> X (\<xi>, \<zeta>) (w @ w') = af\<^sub>\<nu> X (af \<xi> w, (af \<xi> w)[X]\<^sub>\<nu>) w'"
-  by (induction w' rule: rev_induct) fastforce+
-
-
-lemma af\<^sub>\<nu>_semantics_ltr:
-  assumes
-    "\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>"
-  shows
-    "\<exists>m. \<forall>k\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n"
-proof
-  define resets where "resets = {i. snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix i w)) \<sim> false\<^sub>n}"
-  define m where "m = (if resets = {} then 0 else Suc (Max resets))"
-
-  from assms obtain i where 1: "suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>"
-    by blast
-
-  {
-    fix j
-    assume "i \<le> j" and "j \<in> resets"
-    
-    let ?\<phi> = "af \<phi> (prefix (Suc j) w)"
-
-    from 1 have "\<forall>n. suffix n (suffix i w) \<Turnstile>\<^sub>n af \<phi> (prefix i w @ prefix n (suffix i w))[X]\<^sub>\<nu>"
-      by (simp add: GF_advice_af)
-
-    then have "suffix (Suc j) w \<Turnstile>\<^sub>n af \<phi> (prefix (Suc j) w)[X]\<^sub>\<nu>"
-      by (metis (no_types) \<open>i \<le> j\<close> add.right_neutral le_SucI le_Suc_ex subsequence_append subsequence_shift suffix_suffix)
-
-    then have "\<forall>k>j. \<not> af (af \<phi> (prefix (Suc j) w)[X]\<^sub>\<nu>) (w [Suc j \<rightarrow> k]) \<sim> false\<^sub>n"
-      by (metis ltl_implies_satisfiable_prefix subsequence_prefix_suffix)
-
-    then have "\<forall>k>j. \<not> snd (af\<^sub>\<nu> X (?\<phi>, ?\<phi>[X]\<^sub>\<nu>) (w [Suc j \<rightarrow> k])) \<sim> false\<^sub>n"
-      by (metis af\<^sub>\<nu>_snd snd_eqD)
-
-    moreover
-
-    {
-      have "fst (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Suc j) w)) = ?\<phi>"
-        by (simp add: af\<^sub>\<nu>_fst)
-
-      moreover
-
-      have "snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix j w)) \<sim> false\<^sub>n"
-        using \<open>j \<in> resets\<close> resets_def by blast
-
-      ultimately have "af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Suc j) w) = (?\<phi>, ?\<phi>[X]\<^sub>\<nu>)"
-        by (metis (no_types) af\<^sub>\<nu>_step prod.collapse subseq_to_Suc zero_le)
-    }
-
-    ultimately have "\<forall>k>j. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) ((w [0 \<rightarrow> Suc j]) @ (w [Suc j \<rightarrow> k]))) \<sim> false\<^sub>n"
-      by (simp add: af\<^sub>\<nu>_segments)
-
-    then have "\<forall>k>j. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix k w)) \<sim> false\<^sub>n"
-      by (metis Suc_leI le0 subsequence_append_general)
-
-    then have "\<forall>k \<in> resets. k \<le> j"
-      using \<open>j \<in> resets\<close> resets_def le_less_linear by blast
-  }
-
-  then have "finite resets"
-    by (meson finite_nat_set_iff_bounded_le infinite_nat_iff_unbounded_le)
-
-  then have "resets \<noteq> {} \<Longrightarrow> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Max resets) w)) \<sim> false\<^sub>n"
-    using Max_in resets_def by blast
-
-  then have "\<forall>k\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix k w)) \<sim> false\<^sub>n"
-    by (metis (mono_tags, lifting) Max_ge Suc_n_not_le_n \<open>finite resets\<close> empty_Collect_eq m_def mem_Collect_eq order.trans resets_def)
-
-  then show "\<forall>k\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n"
-    using le_SucI by blast
-qed
-
-lemma af\<^sub>\<nu>_semantics_rtl:
-  assumes
-    "\<exists>n. \<forall>k\<ge>n. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n"
-  shows
-    "\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>"
-proof
-  define resets where "resets = {i. snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix i w)) \<sim> false\<^sub>n}"
-  define m where "m = (if resets = {} then 0 else Suc (Max resets))"
-
-  from assms obtain n where "\<forall>k\<ge>n. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n"
-    by blast
-
-  then have "\<forall>k>n. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix k w)) \<sim> false\<^sub>n"
-    by (metis le_SucE lessE less_imp_le_nat)
-
-  then have "finite resets"
-    by (metis (mono_tags, lifting) infinite_nat_iff_unbounded mem_Collect_eq resets_def)
-
-  then have "\<forall>i\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix i w)) \<sim> false\<^sub>n"
-    unfolding resets_def m_def using Max_ge not_less_eq_eq by auto
-
-  then have "\<forall>i. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) ((w [0 \<rightarrow> m]) @ (w [m \<rightarrow> i]))) \<sim> false\<^sub>n"
-    by (metis le0 nat_le_linear subseq_to_smaller subsequence_append_general)
-
-  moreover
-
-  let ?\<phi> = "af \<phi> (prefix m w)"
-
-  have "resets \<noteq> {} \<Longrightarrow> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Max resets) w)) \<sim> false\<^sub>n"
-    using Max_in \<open>finite resets\<close> resets_def by blast
-
-  then have prefix_\<phi>': "snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix m w)) = ?\<phi>[X]\<^sub>\<nu>"
-    by (auto simp: GF_advice_congruent m_def af\<^sub>\<nu>_fst)
-
-  ultimately have "\<forall>i. \<not> snd (af\<^sub>\<nu> X (?\<phi>, ?\<phi>[X]\<^sub>\<nu>) (w [m \<rightarrow> i])) \<sim> false\<^sub>n"
-    by (metis af\<^sub>\<nu>_fst foldl_append fst_conv prod.collapse)
-
-  then have "\<forall>i. \<not> af (?\<phi>[X]\<^sub>\<nu>) (w [m \<rightarrow> i]) \<sim> false\<^sub>n"
-    by (metis prefix_\<phi>' af\<^sub>\<nu>_fst af\<^sub>\<nu>_snd' fst_conv prod.collapse subsequence_take)
-
-  then show "suffix m w \<Turnstile>\<^sub>n af \<phi> (prefix m w)[X]\<^sub>\<nu>"
-    by (metis GF_advice_\<nu>LTL(1) satisfiable_prefix_implies_\<nu>LTL add.right_neutral subsequence_shift)
-qed
+end
 
 end
-
-end
\ No newline at end of file
diff --git a/thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy b/thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy
--- a/thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy
+++ b/thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy
@@ -1,996 +1,1012 @@
 (*
     Author:   Benedikt Seidl
     Author:   Salomon Sickert
     License:  BSD
 *)
 
 section \<open>Advice functions\<close>
 
 theory Advice
 imports
   LTL.LTL LTL.Equivalence_Relations
   Syntactic_Fragments_and_Stability After
 begin
 
 subsection \<open>The GF and FG Advice Functions\<close>
 
 fun GF_advice :: "'a ltln \<Rightarrow> 'a ltln set \<Rightarrow> 'a ltln" ("_[_]\<^sub>\<nu>" [90,60] 89)
   where
   "(X\<^sub>n \<psi>)[X]\<^sub>\<nu> = X\<^sub>n (\<psi>[X]\<^sub>\<nu>)"
 | "(\<psi>\<^sub>1 and\<^sub>n \<psi>\<^sub>2)[X]\<^sub>\<nu> = (\<psi>\<^sub>1[X]\<^sub>\<nu>) and\<^sub>n (\<psi>\<^sub>2[X]\<^sub>\<nu>)"
 | "(\<psi>\<^sub>1 or\<^sub>n \<psi>\<^sub>2)[X]\<^sub>\<nu> = (\<psi>\<^sub>1[X]\<^sub>\<nu>) or\<^sub>n (\<psi>\<^sub>2[X]\<^sub>\<nu>)"
 | "(\<psi>\<^sub>1 W\<^sub>n \<psi>\<^sub>2)[X]\<^sub>\<nu> = (\<psi>\<^sub>1[X]\<^sub>\<nu>) W\<^sub>n (\<psi>\<^sub>2[X]\<^sub>\<nu>)"
 | "(\<psi>\<^sub>1 R\<^sub>n \<psi>\<^sub>2)[X]\<^sub>\<nu> = (\<psi>\<^sub>1[X]\<^sub>\<nu>) R\<^sub>n (\<psi>\<^sub>2[X]\<^sub>\<nu>)"
 | "(\<psi>\<^sub>1 U\<^sub>n \<psi>\<^sub>2)[X]\<^sub>\<nu> = (if (\<psi>\<^sub>1 U\<^sub>n \<psi>\<^sub>2) \<in> X then (\<psi>\<^sub>1[X]\<^sub>\<nu>) W\<^sub>n (\<psi>\<^sub>2[X]\<^sub>\<nu>) else false\<^sub>n)"
 | "(\<psi>\<^sub>1 M\<^sub>n \<psi>\<^sub>2)[X]\<^sub>\<nu> = (if (\<psi>\<^sub>1 M\<^sub>n \<psi>\<^sub>2) \<in> X then (\<psi>\<^sub>1[X]\<^sub>\<nu>) R\<^sub>n (\<psi>\<^sub>2[X]\<^sub>\<nu>) else false\<^sub>n)"
 | "\<phi>[_]\<^sub>\<nu> = \<phi>"
 
 fun FG_advice :: "'a ltln \<Rightarrow> 'a ltln set \<Rightarrow> 'a ltln" ("_[_]\<^sub>\<mu>" [90,60] 89)
 where
   "(X\<^sub>n \<psi>)[Y]\<^sub>\<mu> = X\<^sub>n (\<psi>[Y]\<^sub>\<mu>)"
 | "(\<psi>\<^sub>1 and\<^sub>n \<psi>\<^sub>2)[Y]\<^sub>\<mu> = (\<psi>\<^sub>1[Y]\<^sub>\<mu>) and\<^sub>n (\<psi>\<^sub>2[Y]\<^sub>\<mu>)"
 | "(\<psi>\<^sub>1 or\<^sub>n \<psi>\<^sub>2)[Y]\<^sub>\<mu> = (\<psi>\<^sub>1[Y]\<^sub>\<mu>) or\<^sub>n (\<psi>\<^sub>2[Y]\<^sub>\<mu>)"
 | "(\<psi>\<^sub>1 U\<^sub>n \<psi>\<^sub>2)[Y]\<^sub>\<mu> = (\<psi>\<^sub>1[Y]\<^sub>\<mu>) U\<^sub>n (\<psi>\<^sub>2[Y]\<^sub>\<mu>)"
 | "(\<psi>\<^sub>1 M\<^sub>n \<psi>\<^sub>2)[Y]\<^sub>\<mu> = (\<psi>\<^sub>1[Y]\<^sub>\<mu>) M\<^sub>n (\<psi>\<^sub>2[Y]\<^sub>\<mu>)"
 | "(\<psi>\<^sub>1 W\<^sub>n \<psi>\<^sub>2)[Y]\<^sub>\<mu> = (if (\<psi>\<^sub>1 W\<^sub>n \<psi>\<^sub>2) \<in> Y then true\<^sub>n else (\<psi>\<^sub>1[Y]\<^sub>\<mu>) U\<^sub>n (\<psi>\<^sub>2[Y]\<^sub>\<mu>))"
 | "(\<psi>\<^sub>1 R\<^sub>n \<psi>\<^sub>2)[Y]\<^sub>\<mu> = (if (\<psi>\<^sub>1 R\<^sub>n \<psi>\<^sub>2) \<in> Y then true\<^sub>n else (\<psi>\<^sub>1[Y]\<^sub>\<mu>) M\<^sub>n (\<psi>\<^sub>2[Y]\<^sub>\<mu>))"
 | "\<phi>[_]\<^sub>\<mu> = \<phi>"
 
 lemma GF_advice_\<nu>LTL:
   "\<phi>[X]\<^sub>\<nu> \<in> \<nu>LTL"
   "\<phi> \<in> \<nu>LTL \<Longrightarrow> \<phi>[X]\<^sub>\<nu> = \<phi>"
   by (induction \<phi>) auto
 
 lemma FG_advice_\<mu>LTL:
   "\<phi>[X]\<^sub>\<mu> \<in> \<mu>LTL"
   "\<phi> \<in> \<mu>LTL \<Longrightarrow> \<phi>[X]\<^sub>\<mu> = \<phi>"
   by (induction \<phi>) auto
 
 
 lemma GF_advice_subfrmlsn:
   "subfrmlsn (\<phi>[X]\<^sub>\<nu>) \<subseteq> {\<psi>[X]\<^sub>\<nu> | \<psi>. \<psi> \<in> subfrmlsn \<phi>}"
   by (induction \<phi>) force+
 
 lemma FG_advice_subfrmlsn:
   "subfrmlsn (\<phi>[Y]\<^sub>\<mu>) \<subseteq> {\<psi>[Y]\<^sub>\<mu> | \<psi>. \<psi> \<in> subfrmlsn \<phi>}"
   by (induction \<phi>) force+
 
 lemma GF_advice_subfrmlsn_card:
   "card (subfrmlsn (\<phi>[X]\<^sub>\<nu>)) \<le> card (subfrmlsn \<phi>)"
 proof -
   have "card (subfrmlsn (\<phi>[X]\<^sub>\<nu>)) \<le> card {\<psi>[X]\<^sub>\<nu> | \<psi>. \<psi> \<in> subfrmlsn \<phi>}"
     by (simp add: subfrmlsn_finite GF_advice_subfrmlsn card_mono)
 
   also have "\<dots> \<le> card (subfrmlsn \<phi>)"
     by (metis Collect_mem_eq card_image_le image_Collect subfrmlsn_finite)
 
   finally show ?thesis .
 qed
 
 lemma FG_advice_subfrmlsn_card:
   "card (subfrmlsn (\<phi>[Y]\<^sub>\<mu>)) \<le> card (subfrmlsn \<phi>)"
 proof -
   have "card (subfrmlsn (\<phi>[Y]\<^sub>\<mu>)) \<le> card {\<psi>[Y]\<^sub>\<mu> | \<psi>. \<psi> \<in> subfrmlsn \<phi>}"
     by (simp add: subfrmlsn_finite FG_advice_subfrmlsn card_mono)
 
   also have "\<dots> \<le> card (subfrmlsn \<phi>)"
     by (metis Collect_mem_eq card_image_le image_Collect subfrmlsn_finite)
 
   finally show ?thesis .
 qed
 
 lemma GF_advice_monotone:
   "X \<subseteq> Y \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[Y]\<^sub>\<nu>"
 proof (induction \<phi> arbitrary: w)
   case (Until_ltln \<phi> \<psi>)
   then show ?case
     by (cases "\<phi> U\<^sub>n \<psi> \<in> X") (simp_all, blast)
 next
   case (Release_ltln \<phi> \<psi>)
   then show ?case by (simp, blast)
 next
   case (WeakUntil_ltln \<phi> \<psi>)
   then show ?case by (simp, blast)
 next
   case (StrongRelease_ltln \<phi> \<psi>)
   then show ?case
     by (cases "\<phi> M\<^sub>n \<psi> \<in> X") (simp_all, blast)
 qed auto
 
 lemma FG_advice_monotone:
   "X \<subseteq> Y \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<mu> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[Y]\<^sub>\<mu>"
 proof (induction \<phi> arbitrary: w)
   case (Until_ltln \<phi> \<psi>)
   then show ?case by (simp, blast)
 next
   case (Release_ltln \<phi> \<psi>)
   then show ?case
     by (cases "\<phi> R\<^sub>n \<psi> \<in> X") (auto, blast)
 next
   case (WeakUntil_ltln \<phi> \<psi>)
   then show ?case
     by (cases "\<phi> W\<^sub>n \<psi> \<in> X") (auto, blast)
 next
   case (StrongRelease_ltln \<phi> \<psi>)
   then show ?case by (simp, blast)
 qed auto
 
 lemma GF_advice_ite_simps[simp]:
   "(if P then true\<^sub>n else false\<^sub>n)[X]\<^sub>\<nu> = (if P then true\<^sub>n else false\<^sub>n)"
   "(if P then false\<^sub>n else true\<^sub>n)[X]\<^sub>\<nu> = (if P then false\<^sub>n else true\<^sub>n)"
   by simp_all
 
 lemma FG_advice_ite_simps[simp]:
   "(if P then true\<^sub>n else false\<^sub>n)[Y]\<^sub>\<mu> = (if P then true\<^sub>n else false\<^sub>n)"
   "(if P then false\<^sub>n else true\<^sub>n)[Y]\<^sub>\<mu> = (if P then false\<^sub>n else true\<^sub>n)"
   by simp_all
 
 subsection \<open>Advice Functions on Nested Propositions\<close>
 
 definition nested_prop_atoms\<^sub>\<nu> :: "'a ltln \<Rightarrow> 'a ltln set \<Rightarrow> 'a ltln set"
 where
   "nested_prop_atoms\<^sub>\<nu> \<phi> X = {\<psi>[X]\<^sub>\<nu> | \<psi>. \<psi> \<in> nested_prop_atoms \<phi>}"
 
 definition nested_prop_atoms\<^sub>\<mu> :: "'a ltln \<Rightarrow> 'a ltln set \<Rightarrow> 'a ltln set"
 where
   "nested_prop_atoms\<^sub>\<mu> \<phi> X = {\<psi>[X]\<^sub>\<mu> | \<psi>. \<psi> \<in> nested_prop_atoms \<phi>}"
 
 lemma nested_prop_atoms\<^sub>\<nu>_finite:
   "finite (nested_prop_atoms\<^sub>\<nu> \<phi> X)"
   by (simp add: nested_prop_atoms\<^sub>\<nu>_def nested_prop_atoms_finite)
 
 lemma nested_prop_atoms\<^sub>\<mu>_finite:
   "finite (nested_prop_atoms\<^sub>\<mu> \<phi> X)"
   by (simp add: nested_prop_atoms\<^sub>\<mu>_def nested_prop_atoms_finite)
 
 lemma nested_prop_atoms\<^sub>\<nu>_card:
   "card (nested_prop_atoms\<^sub>\<nu> \<phi> X) \<le> card (nested_prop_atoms \<phi>)"
   unfolding nested_prop_atoms\<^sub>\<nu>_def
   by (metis Collect_mem_eq card_image_le image_Collect nested_prop_atoms_finite)
 
 lemma nested_prop_atoms\<^sub>\<mu>_card:
   "card (nested_prop_atoms\<^sub>\<mu> \<phi> X) \<le> card (nested_prop_atoms \<phi>)"
   unfolding nested_prop_atoms\<^sub>\<mu>_def
   by (metis Collect_mem_eq card_image_le image_Collect nested_prop_atoms_finite)
 
 lemma GF_advice_nested_prop_atoms\<^sub>\<nu>:
   "nested_prop_atoms (\<phi>[X]\<^sub>\<nu>) \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X"
   by (induction \<phi>) (unfold nested_prop_atoms\<^sub>\<nu>_def, force+)
 
 lemma FG_advice_nested_prop_atoms\<^sub>\<mu>:
   "nested_prop_atoms (\<phi>[Y]\<^sub>\<mu>) \<subseteq> nested_prop_atoms\<^sub>\<mu> \<phi> Y"
   by (induction \<phi>) (unfold nested_prop_atoms\<^sub>\<mu>_def, force+)
 
 lemma nested_prop_atoms\<^sub>\<nu>_subset:
   "nested_prop_atoms \<phi> \<subseteq> nested_prop_atoms \<psi> \<Longrightarrow> nested_prop_atoms\<^sub>\<nu> \<phi> X \<subseteq> nested_prop_atoms\<^sub>\<nu> \<psi> X"
   unfolding nested_prop_atoms\<^sub>\<nu>_def by blast
 
 lemma nested_prop_atoms\<^sub>\<mu>_subset:
   "nested_prop_atoms \<phi> \<subseteq> nested_prop_atoms \<psi> \<Longrightarrow> nested_prop_atoms\<^sub>\<mu> \<phi> Y \<subseteq> nested_prop_atoms\<^sub>\<mu> \<psi> Y"
   unfolding nested_prop_atoms\<^sub>\<mu>_def by blast
 
 lemma GF_advice_nested_prop_atoms_card:
   "card (nested_prop_atoms (\<phi>[X]\<^sub>\<nu>)) \<le> card (nested_prop_atoms \<phi>)"
 proof -
   have "card (nested_prop_atoms (\<phi>[X]\<^sub>\<nu>)) \<le> card (nested_prop_atoms\<^sub>\<nu> \<phi> X)"
     by (simp add: nested_prop_atoms\<^sub>\<nu>_finite GF_advice_nested_prop_atoms\<^sub>\<nu> card_mono)
 
   then show ?thesis
     using nested_prop_atoms\<^sub>\<nu>_card le_trans by blast
 qed
 
 lemma FG_advice_nested_prop_atoms_card:
   "card (nested_prop_atoms (\<phi>[Y]\<^sub>\<mu>)) \<le> card (nested_prop_atoms \<phi>)"
 proof -
   have "card (nested_prop_atoms (\<phi>[Y]\<^sub>\<mu>)) \<le> card (nested_prop_atoms\<^sub>\<mu> \<phi> Y)"
     by (simp add: nested_prop_atoms\<^sub>\<mu>_finite FG_advice_nested_prop_atoms\<^sub>\<mu> card_mono)
 
   then show ?thesis
     using nested_prop_atoms\<^sub>\<mu>_card le_trans by blast
 qed
 
 
 
 subsection \<open>Intersecting the Advice Set\<close>
 
 lemma GF_advice_inter:
   "X \<inter> subformulas\<^sub>\<mu> \<phi> \<subseteq> S \<Longrightarrow> \<phi>[X \<inter> S]\<^sub>\<nu> = \<phi>[X]\<^sub>\<nu>"
   by (induction \<phi>) auto
 
 lemma GF_advice_inter_subformulas:
   "\<phi>[X \<inter> subformulas\<^sub>\<mu> \<phi>]\<^sub>\<nu> = \<phi>[X]\<^sub>\<nu>"
   using GF_advice_inter by blast
 
 lemma GF_advice_minus_subformulas:
   "\<psi> \<notin> subformulas\<^sub>\<mu> \<phi> \<Longrightarrow> \<phi>[X - {\<psi>}]\<^sub>\<nu> = \<phi>[X]\<^sub>\<nu>"
 proof -
   assume "\<psi> \<notin> subformulas\<^sub>\<mu> \<phi>"
   then have "subformulas\<^sub>\<mu> \<phi> \<inter> X \<subseteq> X - {\<psi>}"
     by blast
   then show "\<phi>[X - {\<psi>}]\<^sub>\<nu> = \<phi>[X]\<^sub>\<nu>"
     by (metis GF_advice_inter Diff_subset Int_absorb1 inf.commute)
 qed
 
 lemma GF_advice_minus_size:
   "\<lbrakk>size \<phi> \<le> size \<psi>; \<phi> \<noteq> \<psi>\<rbrakk> \<Longrightarrow> \<phi>[X - {\<psi>}]\<^sub>\<nu> = \<phi>[X]\<^sub>\<nu>"
   using subfrmlsn_size subformulas\<^sub>\<mu>_subfrmlsn GF_advice_minus_subformulas
   by fastforce
 
 
 lemma FG_advice_inter:
   "Y \<inter> subformulas\<^sub>\<nu> \<phi> \<subseteq> S \<Longrightarrow> \<phi>[Y \<inter> S]\<^sub>\<mu> = \<phi>[Y]\<^sub>\<mu>"
   by (induction \<phi>) auto
 
 lemma FG_advice_inter_subformulas:
   "\<phi>[Y \<inter> subformulas\<^sub>\<nu> \<phi>]\<^sub>\<mu> = \<phi>[Y]\<^sub>\<mu>"
   using FG_advice_inter by blast
 
 lemma FG_advice_minus_subformulas:
   "\<psi> \<notin> subformulas\<^sub>\<nu> \<phi> \<Longrightarrow> \<phi>[Y - {\<psi>}]\<^sub>\<mu> = \<phi>[Y]\<^sub>\<mu>"
 proof -
   assume "\<psi> \<notin> subformulas\<^sub>\<nu> \<phi>"
   then have "subformulas\<^sub>\<nu> \<phi> \<inter> Y \<subseteq> Y - {\<psi>}"
     by blast
   then show "\<phi>[Y - {\<psi>}]\<^sub>\<mu>  = \<phi>[Y]\<^sub>\<mu>"
     by (metis FG_advice_inter Diff_subset Int_absorb1 inf.commute)
 qed
 
 lemma FG_advice_minus_size:
   "\<lbrakk>size \<phi> \<le> size \<psi>; \<phi> \<noteq> \<psi>\<rbrakk> \<Longrightarrow> \<phi>[Y - {\<psi>}]\<^sub>\<mu> = \<phi>[Y]\<^sub>\<mu>"
   using subfrmlsn_size subformulas\<^sub>\<nu>_subfrmlsn FG_advice_minus_subformulas
   by fastforce
 
 lemma FG_advice_insert:
   "\<lbrakk>\<psi> \<notin> Y; size \<phi> < size \<psi>\<rbrakk> \<Longrightarrow> \<phi>[insert \<psi> Y]\<^sub>\<mu> = \<phi>[Y]\<^sub>\<mu>"
   by (metis FG_advice_minus_size Diff_insert_absorb less_imp_le neq_iff)
 
 
 
 subsection \<open>Correctness GF-advice function\<close>
 
 lemma GF_advice_a1:
   "\<lbrakk>\<F> \<phi> w \<subseteq> X; w \<Turnstile>\<^sub>n \<phi>\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu>"
 proof (induction \<phi> arbitrary: w)
   case (Next_ltln \<phi>)
   then show ?case
     using \<F>_suffix by simp blast
 next
   case (Until_ltln \<phi>1 \<phi>2)
 
   have "\<F> (\<phi>1 W\<^sub>n \<phi>2) w \<subseteq> \<F> (\<phi>1 U\<^sub>n \<phi>2) w"
     by fastforce
   then have "\<F> (\<phi>1 W\<^sub>n \<phi>2) w \<subseteq> X" and "w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2"
     using Until_ltln.prems ltln_strong_to_weak by blast+
   then have "w \<Turnstile>\<^sub>n \<phi>1[X]\<^sub>\<nu> W\<^sub>n \<phi>2[X]\<^sub>\<nu>"
     using Until_ltln.IH
     by simp (meson \<F>_suffix subset_trans sup.boundedE)
 
   moreover
 
   have "w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2"
     using Until_ltln.prems by simp
   then have "\<phi>1 U\<^sub>n \<phi>2 \<in> \<F> (\<phi>1 U\<^sub>n \<phi>2) w"
     by force
   then have "\<phi>1 U\<^sub>n \<phi>2 \<in> X"
     using Until_ltln.prems by fast
 
   ultimately show ?case
     by auto
 next
   case (Release_ltln \<phi>1 \<phi>2)
   then show ?case
     by simp (meson \<F>_suffix subset_trans sup.boundedE)
 next
   case (WeakUntil_ltln \<phi>1 \<phi>2)
   then show ?case
     by simp (meson \<F>_suffix subset_trans sup.boundedE)
 next
   case (StrongRelease_ltln \<phi>1 \<phi>2)
 
   have "\<F> (\<phi>1 R\<^sub>n \<phi>2) w \<subseteq> \<F> (\<phi>1 M\<^sub>n \<phi>2) w"
     by fastforce
   then have "\<F> (\<phi>1 R\<^sub>n \<phi>2) w \<subseteq> X" and "w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2"
     using StrongRelease_ltln.prems ltln_strong_to_weak by blast+
   then have "w \<Turnstile>\<^sub>n \<phi>1[X]\<^sub>\<nu> R\<^sub>n \<phi>2[X]\<^sub>\<nu>"
     using StrongRelease_ltln.IH
     by simp (meson \<F>_suffix subset_trans sup.boundedE)
 
   moreover
 
   have "w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2"
     using StrongRelease_ltln.prems by simp
   then have "\<phi>1 M\<^sub>n \<phi>2 \<in> \<F> (\<phi>1 M\<^sub>n \<phi>2) w"
     by force
   then have "\<phi>1 M\<^sub>n \<phi>2 \<in> X"
     using StrongRelease_ltln.prems by fast
 
   ultimately show ?case
     by auto
 qed auto
 
 lemma GF_advice_a2_helper:
   "\<lbrakk>\<forall>\<psi> \<in> X. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>); w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu>\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>"
 proof (induction \<phi> arbitrary: w)
   case (Next_ltln \<phi>)
   then show ?case
     unfolding GF_advice.simps semantics_ltln.simps(7)
     using GF_suffix by blast
 next
   case (Until_ltln \<phi>1 \<phi>2)
 
   then have "\<phi>1 U\<^sub>n \<phi>2 \<in> X"
     using ccontr[of "\<phi>1 U\<^sub>n \<phi>2 \<in> X"] by force
   then have "w \<Turnstile>\<^sub>n F\<^sub>n \<phi>2"
     using Until_ltln.prems by fastforce
 
   moreover
 
   have "w \<Turnstile>\<^sub>n (\<phi>1 U\<^sub>n \<phi>2)[X]\<^sub>\<nu>"
     using Until_ltln.prems by simp
   then have "w \<Turnstile>\<^sub>n (\<phi>1[X]\<^sub>\<nu>) W\<^sub>n (\<phi>2[X]\<^sub>\<nu>)"
     unfolding GF_advice.simps using `\<phi>1 U\<^sub>n \<phi>2 \<in> X` by simp
   then have "w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2"
     unfolding GF_advice.simps semantics_ltln.simps(10)
     by (metis GF_suffix Until_ltln.IH Until_ltln.prems(1))
 
   ultimately show ?case
     using ltln_weak_to_strong by blast
 next
   case (Release_ltln \<phi>1 \<phi>2)
   then show ?case
     unfolding GF_advice.simps semantics_ltln.simps(9)
     by (metis GF_suffix Release_ltln.IH Release_ltln.prems(1))
 next
   case (WeakUntil_ltln \<phi>1 \<phi>2)
   then show ?case
     unfolding GF_advice.simps semantics_ltln.simps(10)
     by (metis GF_suffix)
 next
   case (StrongRelease_ltln \<phi>1 \<phi>2)
 
   then have "\<phi>1 M\<^sub>n \<phi>2 \<in> X"
     using ccontr[of "\<phi>1 M\<^sub>n \<phi>2 \<in> X"] by force
   then have "w \<Turnstile>\<^sub>n F\<^sub>n \<phi>1"
     using StrongRelease_ltln.prems by fastforce
 
   moreover
 
   have "w \<Turnstile>\<^sub>n (\<phi>1 M\<^sub>n \<phi>2)[X]\<^sub>\<nu>"
     using StrongRelease_ltln.prems by simp
   then have "w \<Turnstile>\<^sub>n (\<phi>1[X]\<^sub>\<nu>) R\<^sub>n (\<phi>2[X]\<^sub>\<nu>)"
     unfolding GF_advice.simps using `\<phi>1 M\<^sub>n \<phi>2 \<in> X` by simp
   then have "w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2"
     unfolding GF_advice.simps semantics_ltln.simps(9)
     by (metis GF_suffix StrongRelease_ltln.IH StrongRelease_ltln.prems(1))
 
   ultimately show ?case
     using ltln_weak_to_strong by blast
 qed auto
 
 lemma GF_advice_a2:
   "\<lbrakk>X \<subseteq> \<G>\<F> \<phi> w; w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu>\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>"
   by (metis GF_advice_a2_helper \<G>\<F>_elim subset_eq)
 
 lemma GF_advice_a3:
   "\<lbrakk>X = \<F> \<phi> w; X = \<G>\<F> \<phi> w\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu>"
   using GF_advice_a1 GF_advice_a2 by fastforce
 
 
 
 subsection \<open>Correctness FG-advice function\<close>
 
 lemma FG_advice_b1:
   "\<lbrakk>\<F>\<G> \<phi> w \<subseteq> Y; w \<Turnstile>\<^sub>n \<phi>\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[Y]\<^sub>\<mu>"
 proof (induction \<phi> arbitrary: w)
   case (Next_ltln \<phi>)
   then show ?case
     using \<F>\<G>_suffix by simp blast
 next
   case (Until_ltln \<phi>1 \<phi>2)
   then show ?case
     by simp (metis \<F>\<G>_suffix)
 next
   case (Release_ltln \<phi>1 \<phi>2)
 
   show ?case
   proof (cases "\<phi>1 R\<^sub>n \<phi>2 \<in> Y")
     case False
     then have "\<phi>1 R\<^sub>n \<phi>2 \<notin> \<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w"
       using Release_ltln.prems by blast
     then have "\<not> w \<Turnstile>\<^sub>n G\<^sub>n \<phi>2"
       by fastforce
     then have "w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2"
       using Release_ltln.prems ltln_weak_to_strong by blast
 
     moreover
 
     have "\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w \<subseteq> \<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w"
       by fastforce
     then have "\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w \<subseteq> Y"
       using Release_ltln.prems by blast
 
     ultimately show ?thesis
       using Release_ltln.IH by simp (metis \<F>\<G>_suffix)
   qed simp
 next
   case (WeakUntil_ltln \<phi>1 \<phi>2)
 
   show ?case
   proof (cases "\<phi>1 W\<^sub>n \<phi>2 \<in> Y")
     case False
     then have "\<phi>1 W\<^sub>n \<phi>2 \<notin> \<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w"
       using WeakUntil_ltln.prems by blast
     then have "\<not> w \<Turnstile>\<^sub>n G\<^sub>n \<phi>1"
       by fastforce
     then have "w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2"
       using WeakUntil_ltln.prems ltln_weak_to_strong by blast
 
     moreover
 
     have "\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w \<subseteq> \<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w"
       by fastforce
     then have "\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w \<subseteq> Y"
       using WeakUntil_ltln.prems by blast
 
     ultimately show ?thesis
       using WeakUntil_ltln.IH by simp (metis \<F>\<G>_suffix)
   qed simp
 next
   case (StrongRelease_ltln \<phi>1 \<phi>2)
   then show ?case
     by simp (metis \<F>\<G>_suffix)
 qed auto
 
 lemma FG_advice_b2_helper:
   "\<lbrakk>\<forall>\<psi> \<in> Y. w \<Turnstile>\<^sub>n G\<^sub>n \<psi>; w \<Turnstile>\<^sub>n \<phi>[Y]\<^sub>\<mu>\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>"
 proof (induction \<phi> arbitrary: w)
   case (Until_ltln \<phi>1 \<phi>2)
   then show ?case
     by simp (metis (no_types, lifting) suffix_suffix)
 next
   case (Release_ltln \<phi>1 \<phi>2)
   then show ?case
   proof (cases "\<phi>1 R\<^sub>n \<phi>2 \<in> Y")
     case True
     then show ?thesis
       using Release_ltln.prems by force
   next
     case False
     then have "w \<Turnstile>\<^sub>n (\<phi>1[Y]\<^sub>\<mu>) M\<^sub>n (\<phi>2[Y]\<^sub>\<mu>)"
       using Release_ltln.prems by simp
     then have "w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2"
       using Release_ltln
       by simp (metis (no_types, lifting) suffix_suffix)
     then show ?thesis
       using ltln_strong_to_weak by fast
   qed
 next
   case (WeakUntil_ltln \<phi>1 \<phi>2)
   then show ?case
   proof (cases "\<phi>1 W\<^sub>n \<phi>2 \<in> Y")
     case True
     then show ?thesis
       using WeakUntil_ltln.prems by force
   next
     case False
     then have "w \<Turnstile>\<^sub>n (\<phi>1[Y]\<^sub>\<mu>) U\<^sub>n (\<phi>2[Y]\<^sub>\<mu>)"
       using WeakUntil_ltln.prems by simp
     then have "w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2"
       using WeakUntil_ltln
       by simp (metis (no_types, lifting) suffix_suffix)
     then show ?thesis
       using ltln_strong_to_weak by fast
   qed
 next
   case (StrongRelease_ltln \<phi>1 \<phi>2)
   then show ?case
     by simp (metis (no_types, lifting) suffix_suffix)
 qed auto
 
 lemma FG_advice_b2:
   "\<lbrakk>Y \<subseteq> \<G> \<phi> w; w \<Turnstile>\<^sub>n \<phi>[Y]\<^sub>\<mu>\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>"
   by (metis FG_advice_b2_helper \<G>_elim subset_eq)
 
 lemma FG_advice_b3:
   "\<lbrakk>Y = \<F>\<G> \<phi> w; Y = \<G> \<phi> w\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>[Y]\<^sub>\<mu>"
   using FG_advice_b1 FG_advice_b2 by fastforce
 
 
 
 subsection \<open>Advice Functions and the ``after'' Function\<close>
 
 lemma GF_advice_af_letter:
   "(x ## w) \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu> \<Longrightarrow> w \<Turnstile>\<^sub>n (af_letter \<phi> x)[X]\<^sub>\<nu>"
 proof (induction \<phi>)
   case (Until_ltln \<phi>1 \<phi>2)
 
   then have "w \<Turnstile>\<^sub>n af_letter ((\<phi>1 U\<^sub>n \<phi>2)[X]\<^sub>\<nu>) x"
     using af_letter_build by blast
 
   then show ?case
     using Until_ltln.IH af_letter_build by fastforce
 next
   case (Release_ltln \<phi>1 \<phi>2)
 
   then have "w \<Turnstile>\<^sub>n af_letter ((\<phi>1 R\<^sub>n \<phi>2)[X]\<^sub>\<nu>) x"
     using af_letter_build by blast
 
   then show ?case
     using Release_ltln.IH af_letter_build by auto
 next
   case (WeakUntil_ltln \<phi>1 \<phi>2)
 
   then have "w \<Turnstile>\<^sub>n af_letter ((\<phi>1 W\<^sub>n \<phi>2)[X]\<^sub>\<nu>) x"
     using af_letter_build by blast
 
   then show ?case
     using WeakUntil_ltln.IH af_letter_build by auto
 next
   case (StrongRelease_ltln \<phi>1 \<phi>2)
 
   then have "w \<Turnstile>\<^sub>n af_letter ((\<phi>1 M\<^sub>n \<phi>2)[X]\<^sub>\<nu>) x"
     using af_letter_build by blast
 
   then show ?case
     using StrongRelease_ltln.IH af_letter_build by force
 qed auto
 
 lemma FG_advice_af_letter:
   "w \<Turnstile>\<^sub>n (af_letter \<phi> x)[Y]\<^sub>\<mu> \<Longrightarrow> (x ## w) \<Turnstile>\<^sub>n \<phi>[Y]\<^sub>\<mu>"
 proof (induction \<phi>)
   case (Prop_ltln a)
   then show ?case
     using semantics_ltln.simps(3) by fastforce
 next
   case (Until_ltln \<phi>1 \<phi>2)
   then show ?case
     unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6)
     using af_letter_build apply (cases "w \<Turnstile>\<^sub>n af_letter \<phi>2 x[Y]\<^sub>\<mu>") apply force
     by (metis af_letter.simps(8) semantics_ltln.simps(5) semantics_ltln.simps(6))
 next
   case (Release_ltln \<phi>1 \<phi>2)
   then show ?case
     apply (cases "\<phi>1 R\<^sub>n \<phi>2 \<in> Y")
     apply simp
     unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6)
     using af_letter_build  apply (cases "w \<Turnstile>\<^sub>n af_letter \<phi>1 x[Y]\<^sub>\<mu>") apply force
     by (metis (full_types) af_letter.simps(11) semantics_ltln.simps(5) semantics_ltln.simps(6))
 next
   case (WeakUntil_ltln \<phi>1 \<phi>2)
   then show ?case
     apply (cases "\<phi>1 W\<^sub>n \<phi>2 \<in> Y")
     apply simp
     unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6)
     using af_letter_build  apply (cases "w \<Turnstile>\<^sub>n af_letter \<phi>2 x[Y]\<^sub>\<mu>") apply force
     by (metis (full_types) af_letter.simps(8) semantics_ltln.simps(5) semantics_ltln.simps(6))
 next
   case (StrongRelease_ltln \<phi>1 \<phi>2)
   then show ?case
     unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6)
     using af_letter_build apply (cases "w \<Turnstile>\<^sub>n af_letter \<phi>1 x[Y]\<^sub>\<mu>") apply force
     by (metis af_letter.simps(11) semantics_ltln.simps(5) semantics_ltln.simps(6))
 qed auto
 
 lemma GF_advice_af:
   "(w \<frown> w') \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu> \<Longrightarrow> w' \<Turnstile>\<^sub>n (af \<phi> w)[X]\<^sub>\<nu>"
   by (induction w arbitrary: \<phi>) (simp, insert GF_advice_af_letter, fastforce)
 
 lemma FG_advice_af:
   "w' \<Turnstile>\<^sub>n (af \<phi> w)[X]\<^sub>\<mu> \<Longrightarrow> (w \<frown> w') \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<mu>"
   by (induction w arbitrary: \<phi>) (simp, insert FG_advice_af_letter, fastforce)
 
 lemma GF_advice_af_2:
   "w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu> \<Longrightarrow> suffix i w \<Turnstile>\<^sub>n (af \<phi> (prefix i w))[X]\<^sub>\<nu>"
   using GF_advice_af by force
 
 lemma FG_advice_af_2:
   "suffix i w \<Turnstile>\<^sub>n (af \<phi> (prefix i w))[X]\<^sub>\<mu> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<mu>"
   using FG_advice_af by force
 
 (* TODO move to Omega_Words_Fun.thy ?? *)
 lemma prefix_suffix_subsequence: "prefix i (suffix j w) = (w [j \<rightarrow> i + j])"
   by (simp add: add.commute)
 
 text \<open>We show this generic lemma to prove the following theorems:\<close>
 
 lemma GF_advice_sync:
   fixes index :: "nat \<Rightarrow> nat"
   fixes formula :: "nat \<Rightarrow> 'a ltln"
   assumes "\<And>i. i < n \<Longrightarrow> \<exists>j. suffix ((index i) + j) w \<Turnstile>\<^sub>n af (formula i) (w [index i \<rightarrow> (index i) + j])[X]\<^sub>\<nu>"
   shows "\<exists>k. (\<forall>i < n. k \<ge> index i \<and> suffix k w \<Turnstile>\<^sub>n af (formula i) (w [index i \<rightarrow> k])[X]\<^sub>\<nu>)"
   using assms
 proof (induction n)
   case (Suc n)
 
   obtain k1 where leq1: "\<And>i. i < n \<Longrightarrow> k1 \<ge> index i"
     and suffix1: "\<And>i. i < n \<Longrightarrow> suffix k1 w \<Turnstile>\<^sub>n af (formula i) (w [(index i) \<rightarrow> k1])[X]\<^sub>\<nu>"
     using Suc less_SucI by blast
 
   obtain k2 where leq2: "k2 \<ge> index n"
     and suffix2: "suffix k2 w \<Turnstile>\<^sub>n af (formula n) (w [index n \<rightarrow> k2])[X]\<^sub>\<nu>"
     using le_add1 Suc.prems by blast
 
   define k where "k \<equiv> k1 + k2"
 
   have "\<And>i. i < Suc n \<Longrightarrow> k \<ge> index i"
     unfolding k_def by (metis leq1 leq2 less_SucE trans_le_add1 trans_le_add2)
 
   moreover
 
   {
     have "\<And>i. i < n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (formula i) (w [(index i) \<rightarrow> k])[X]\<^sub>\<nu>"
       unfolding k_def
       by (metis GF_advice_af_2[OF suffix1, unfolded suffix_suffix prefix_suffix_subsequence] af_subsequence_append leq1 add.commute le_add1)
 
     moreover
 
     have "suffix k w \<Turnstile>\<^sub>n af (formula n) (w [index n \<rightarrow> k])[X]\<^sub>\<nu>"
       unfolding k_def
       by (metis GF_advice_af_2[OF suffix2, unfolded suffix_suffix prefix_suffix_subsequence] af_subsequence_append leq2 add.commute le_add1)
 
     ultimately
 
     have "\<And>i. i \<le> n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (formula i) (w [(index i) \<rightarrow> k])[X]\<^sub>\<nu>"
       using nat_less_le by blast
   }
 
   ultimately
 
   show ?case
     by (meson less_Suc_eq_le)
 qed simp
 
 lemma GF_advice_sync_and:
   assumes "\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>"
   assumes "\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<psi> (prefix i w)[X]\<^sub>\<nu>"
   shows "\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu> \<and> suffix i w \<Turnstile>\<^sub>n af \<psi> (prefix i w)[X]\<^sub>\<nu>"
 proof -
   let ?formula = "\<lambda>i :: nat. (if (i = 0) then \<phi> else \<psi>)"
 
   have assms: "\<And>i. i < 2 \<Longrightarrow> \<exists>j. suffix j w \<Turnstile>\<^sub>n af (?formula i) (w [0 \<rightarrow> j])[X]\<^sub>\<nu>"
     using assms by simp
   obtain k where k_def: "\<And>i :: nat. i < 2 \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if i = 0 then \<phi> else \<psi>) (prefix k w)[X]\<^sub>\<nu>"
     using GF_advice_sync[of "2" "\<lambda>i. 0" w ?formula, simplified, OF assms, simplified] by blast
   show ?thesis
     using k_def[of 0] k_def[of 1] by auto
 qed
 
 lemma GF_advice_sync_less:
   assumes "\<And>i. i < n \<Longrightarrow> \<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n af \<phi> (w [i \<rightarrow> j + i])[X]\<^sub>\<nu>"
   assumes "\<exists>j. suffix (n + j) w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> j + n])[X]\<^sub>\<nu>"
   shows "\<exists>k \<ge> n. (\<forall>j < n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>"
 proof -
   let ?index = "\<lambda>i. min i n"
   let ?formula = "\<lambda>i. if (i < n) then \<phi> else \<psi>"
 
   {
     fix i
     assume "i < Suc n"
     then have min_def: "min i n = i"
       by simp
     have "\<exists>j. suffix ((?index i) + j) w \<Turnstile>\<^sub>n af (?formula i) (w [?index i \<rightarrow> (?index i) + j])[X]\<^sub>\<nu>"
       unfolding min_def
       by (cases "i < n")
          (metis (full_types) assms(1) add.commute, metis (full_types) assms(2) \<open>i < Suc n\<close> add.commute  less_SucE)
   }
 
   then obtain k where leq: "(\<And>i. i < Suc n \<Longrightarrow> min i n \<le> k)"
     and suffix: "\<And>i. i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>"
     using GF_advice_sync[of "Suc n" ?index w ?formula X] by metis
 
   have "\<forall>j < n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>"
     using suffix by (metis (full_types) less_SucI min.strict_order_iff)
 
   moreover
 
   have "suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>"
     using suffix[of n, simplified] by blast
 
   moreover
 
   have "k \<ge> n"
     using leq by presburger
 
   ultimately
   show ?thesis
     by auto
 qed
 
 lemma GF_advice_sync_lesseq:
   assumes "\<And>i. i \<le> n \<Longrightarrow> \<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n af \<phi> (w [i \<rightarrow> j + i])[X]\<^sub>\<nu>"
   assumes "\<exists>j. suffix (n + j) w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> j + n])[X]\<^sub>\<nu>"
   shows "\<exists>k \<ge> n. (\<forall>j \<le> n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>"
 proof -
   let ?index = "\<lambda>i. min i n"
   let ?formula = "\<lambda>i. if (i \<le> n) then \<phi> else \<psi>"
 
   {
     fix i
     assume "i < Suc (Suc n)"
     hence "\<exists>j. suffix ((?index i) + j) w \<Turnstile>\<^sub>n af (?formula i) (w [?index i \<rightarrow> (?index i) + j])[X]\<^sub>\<nu>"
     proof (cases "i < Suc n")
       case True
       then have min_def: "min i n = i"
         by simp
       show ?thesis
         unfolding min_def by (metis (full_types) assms(1) Suc_leI Suc_le_mono True add.commute)
     next
       case False
       then have i_def: "i = Suc n"
         using \<open>i < Suc (Suc n)\<close> less_antisym by blast
       have min_def: "min i n = n"
         unfolding i_def by simp
       show ?thesis
         using assms(2) False
         by (simp add: min_def add.commute)
     qed
   }
 
   then obtain k where leq: "(\<And>i. i \<le> Suc n \<Longrightarrow> min i n \<le> k)"
     and suffix: "\<And>i :: nat. i < Suc (Suc n) \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if i \<le> n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>"
     using GF_advice_sync[of "Suc (Suc n)" ?index w ?formula X]
     by (metis (no_types, hide_lams) less_Suc_eq min_le_iff_disj)
 
   have "\<forall>j \<le> n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>"
     using suffix by (metis (full_types) le_SucI less_Suc_eq_le min.orderE)
 
   moreover
 
   have "suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>"
     using suffix[of "Suc n", simplified] by linarith
 
   moreover
 
   have "k \<ge> n"
     using leq by presburger
 
   ultimately
   show ?thesis
     by auto
 qed
 
 lemma af_subsequence_U_GF_advice:
   assumes "i \<le> n"
   assumes "suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [i \<rightarrow> n]))[X]\<^sub>\<nu>)"
   assumes "\<And>j. j < i \<Longrightarrow> suffix n w \<Turnstile>\<^sub>n ((af \<phi> (w [j \<rightarrow> n]))[X]\<^sub>\<nu>)"
   shows "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> U\<^sub>n \<psi>) (prefix (Suc n) w))[X]\<^sub>\<nu>"
   using assms
 proof (induction i arbitrary: w n)
   case 0
   then have A: "suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [0 \<rightarrow> n]))[X]\<^sub>\<nu>)"
     by blast
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<psi> (w [0 \<rightarrow> Suc n]))[X]\<^sub>\<nu>"
     using GF_advice_af_2[OF A, of 1] by simp
   then show ?case
     unfolding GF_advice.simps af_subsequence_U semantics_ltln.simps by blast
 next
   case (Suc i)
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<phi> (prefix (Suc n) w))[X]\<^sub>\<nu>"
     using Suc.prems(3)[OF zero_less_Suc, THEN GF_advice_af_2, unfolded suffix_suffix, of 1]
     by simp
   moreover
   have B: "(Suc (n - 1)) = n"
     using Suc by simp
   note Suc.IH[of "n - 1" "suffix 1 w", unfolded suffix_suffix] Suc.prems
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> U\<^sub>n \<psi>) (w [1 \<rightarrow> (Suc n)]))[X]\<^sub>\<nu>"
     by (metis B One_nat_def Suc_le_mono Suc_mono plus_1_eq_Suc subsequence_shift)
   ultimately
   show ?case
     unfolding af_subsequence_U semantics_ltln.simps GF_advice.simps by blast
 qed
 
 lemma af_subsequence_M_GF_advice:
   assumes "i \<le> n"
   assumes "suffix n w \<Turnstile>\<^sub>n ((af \<phi> (w [i \<rightarrow> n]))[X]\<^sub>\<nu>)"
   assumes "\<And>j. j \<le> i \<Longrightarrow> suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [j \<rightarrow> n]))[X]\<^sub>\<nu>)"
   shows "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> M\<^sub>n \<psi>) (prefix (Suc n) w))[X]\<^sub>\<nu>"
   using assms
 proof (induction i arbitrary: w n)
   case 0
   then have A: "suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [0 \<rightarrow> n]))[X]\<^sub>\<nu>)"
     by blast
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<psi> (w [0 \<rightarrow> Suc n]))[X]\<^sub>\<nu>"
     using GF_advice_af_2[OF A, of 1] by simp
   moreover
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<phi> (w [0 \<rightarrow> Suc n]))[X]\<^sub>\<nu>"
     using GF_advice_af_2[OF "0.prems"(2), of 1, unfolded suffix_suffix] by auto
   ultimately
   show ?case
     unfolding af_subsequence_M GF_advice.simps semantics_ltln.simps by blast
 next
   case (Suc i)
   have "suffix 1 (suffix n w) \<Turnstile>\<^sub>n af (af \<psi> (prefix n w)) [suffix n w 0][X]\<^sub>\<nu>"
     by (metis (no_types) GF_advice_af_2 Suc.prems(3) plus_1_eq_Suc subsequence_singleton suffix_0 suffix_suffix zero_le)
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<psi> (prefix (Suc n) w))[X]\<^sub>\<nu>"
     using Suc.prems(3)[THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp
   moreover
   have B: "(Suc (n - 1)) = n"
     using Suc by simp
   note Suc.IH[of _ "suffix 1 w", unfolded subsequence_shift suffix_suffix]
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> M\<^sub>n \<psi>) (w [1 \<rightarrow> (Suc n)]))[X]\<^sub>\<nu>"
     by (metis B One_nat_def Suc_le_mono plus_1_eq_Suc Suc.prems)
   ultimately
   show ?case
     unfolding af_subsequence_M semantics_ltln.simps GF_advice.simps by blast
 qed
 
 lemma af_subsequence_R_GF_advice:
   assumes "i \<le> n"
   assumes "suffix n w \<Turnstile>\<^sub>n ((af \<phi> (w [i \<rightarrow> n]))[X]\<^sub>\<nu>)"
   assumes "\<And>j. j \<le> i \<Longrightarrow> suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [j \<rightarrow> n]))[X]\<^sub>\<nu>)"
   shows "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> R\<^sub>n \<psi>) (prefix (Suc n) w))[X]\<^sub>\<nu>"
   using assms
 proof (induction i arbitrary: w n)
   case 0
   then have A: "suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [0 \<rightarrow> n]))[X]\<^sub>\<nu>)"
     by blast
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<psi> (w [0 \<rightarrow> Suc n]))[X]\<^sub>\<nu>"
     using GF_advice_af_2[OF A, of 1] by simp
   moreover
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<phi> (w [0 \<rightarrow> Suc n]))[X]\<^sub>\<nu>"
     using GF_advice_af_2[OF "0.prems"(2), of 1, unfolded suffix_suffix] by auto
   ultimately
   show ?case
     unfolding af_subsequence_R GF_advice.simps semantics_ltln.simps by blast
 next
   case (Suc i)
   have "suffix 1 (suffix n w) \<Turnstile>\<^sub>n af (af \<psi> (prefix n w)) [suffix n w 0][X]\<^sub>\<nu>"
     by (metis (no_types) GF_advice_af_2 Suc.prems(3) plus_1_eq_Suc subsequence_singleton suffix_0 suffix_suffix zero_le)
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<psi> (prefix (Suc n) w))[X]\<^sub>\<nu>"
     using Suc.prems(3)[THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp
   moreover
   have B: "(Suc (n - 1)) = n"
     using Suc by simp
   note Suc.IH[of _ "suffix 1 w", unfolded subsequence_shift suffix_suffix]
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> R\<^sub>n \<psi>) (w [1 \<rightarrow> (Suc n)]))[X]\<^sub>\<nu>"
     by (metis B One_nat_def Suc_le_mono plus_1_eq_Suc Suc.prems)
   ultimately
   show ?case
     unfolding af_subsequence_R semantics_ltln.simps GF_advice.simps by blast
 qed
 
 lemma af_subsequence_W_GF_advice:
   assumes "i \<le> n"
   assumes "suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [i \<rightarrow> n]))[X]\<^sub>\<nu>)"
   assumes "\<And>j. j < i \<Longrightarrow> suffix n w \<Turnstile>\<^sub>n ((af \<phi> (w [j \<rightarrow> n]))[X]\<^sub>\<nu>)"
   shows "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> W\<^sub>n \<psi>) (prefix (Suc n) w))[X]\<^sub>\<nu>"
   using assms
 proof (induction i arbitrary: w n)
   case 0
   then have A: "suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [0 \<rightarrow> n]))[X]\<^sub>\<nu>)"
     by blast
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<psi> (w [0 \<rightarrow> Suc n]))[X]\<^sub>\<nu>"
     using GF_advice_af_2[OF A, of 1] by simp
   then show ?case
     unfolding af_subsequence_W GF_advice.simps semantics_ltln.simps by blast
 next
   case (Suc i)
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<phi> (prefix (Suc n) w))[X]\<^sub>\<nu>"
     using Suc.prems(3)[OF zero_less_Suc, THEN GF_advice_af_2, unfolded suffix_suffix, of 1]
     by simp
   moreover
   have B: "(Suc (n - 1)) = n"
     using Suc by simp
   note Suc.IH[of "n - 1" "suffix 1 w", unfolded suffix_suffix] Suc.prems
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> W\<^sub>n \<psi>) (w [1 \<rightarrow> (Suc n)]))[X]\<^sub>\<nu>"
     by (metis B One_nat_def Suc_le_mono Suc_mono plus_1_eq_Suc subsequence_shift)
   ultimately
   show ?case
     unfolding af_subsequence_W unfolding semantics_ltln.simps GF_advice.simps by simp
 qed
 
 lemma af_subsequence_R_GF_advice_connect:
   assumes "i \<le> n"
   assumes "suffix n w \<Turnstile>\<^sub>n af (\<phi> R\<^sub>n \<psi>) (w [i \<rightarrow> n])[X]\<^sub>\<nu>"
   assumes "\<And>j. j \<le> i \<Longrightarrow> suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [j \<rightarrow> n]))[X]\<^sub>\<nu>)"
   shows "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> R\<^sub>n \<psi>) (prefix (Suc n) w))[X]\<^sub>\<nu>"
   using assms
 proof (induction i arbitrary: w n)
   case 0
   then have A: "suffix n w \<Turnstile>\<^sub>n ((af \<psi> (w [0 \<rightarrow> n]))[X]\<^sub>\<nu>)"
     by blast
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<psi> (w [0 \<rightarrow> Suc n]))[X]\<^sub>\<nu>"
     using GF_advice_af_2[OF A, of 1] by simp
   moreover
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> R\<^sub>n \<psi>) (w [0 \<rightarrow> Suc n]))[X]\<^sub>\<nu>"
     using GF_advice_af_2[OF "0.prems"(2), of 1, unfolded suffix_suffix] by simp
   ultimately
   show ?case
     unfolding af_subsequence_R GF_advice.simps semantics_ltln.simps by blast
 next
   case (Suc i)
   have "suffix 1 (suffix n w) \<Turnstile>\<^sub>n af (af \<psi> (prefix n w)) [suffix n w 0][X]\<^sub>\<nu>"
     by (metis (no_types) GF_advice_af_2 Suc.prems(3) plus_1_eq_Suc subsequence_singleton suffix_0 suffix_suffix zero_le)
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<psi> (prefix (Suc n) w))[X]\<^sub>\<nu>"
     using Suc.prems(3)[THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp
   moreover
   have B: "(Suc (n - 1)) = n"
     using Suc by simp
   note Suc.IH[of _ "suffix 1 w", unfolded subsequence_shift suffix_suffix]
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> R\<^sub>n \<psi>) (w [1 \<rightarrow> (Suc n)]))[X]\<^sub>\<nu>"
     by (metis B One_nat_def Suc_le_mono plus_1_eq_Suc Suc.prems)
   ultimately
   show ?case
     unfolding af_subsequence_R semantics_ltln.simps GF_advice.simps by blast
 qed
 
 lemma af_subsequence_W_GF_advice_connect:
   assumes "i \<le> n"
   assumes "suffix n w \<Turnstile>\<^sub>n af (\<phi> W\<^sub>n \<psi>) (w [i \<rightarrow> n])[X]\<^sub>\<nu>"
   assumes "\<And>j. j < i \<Longrightarrow> suffix n w \<Turnstile>\<^sub>n ((af \<phi> (w [j \<rightarrow> n]))[X]\<^sub>\<nu>)"
   shows "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> W\<^sub>n \<psi>) (prefix (Suc n) w))[X]\<^sub>\<nu>"
   using assms
 proof (induction i arbitrary: w n)
   case 0
   have "suffix (Suc n) w \<Turnstile>\<^sub>n af_letter (af (\<phi> W\<^sub>n \<psi>) (prefix n w)) (w n)[X]\<^sub>\<nu>"
     by (simp add: "0.prems"(2) GF_advice_af_letter)
   moreover
   have "prefix (Suc n) w = prefix n w @ [w n]"
     using subseq_to_Suc by blast
   ultimately show ?case
     by (metis (no_types) foldl.simps(1) foldl.simps(2) foldl_append)
 next
   case (Suc i)
   have "suffix (Suc n) w \<Turnstile>\<^sub>n (af \<phi> (prefix (Suc n) w))[X]\<^sub>\<nu>"
     using Suc.prems(3)[OF zero_less_Suc, THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp
   moreover
   have "n > 0" and B: "(Suc (n - 1)) = n"
     using Suc by simp+
   note Suc.IH[of "n - 1" "suffix 1 w", unfolded suffix_suffix] Suc.prems
   then have "suffix (Suc n) w \<Turnstile>\<^sub>n (af (\<phi> W\<^sub>n \<psi>) (w [1 \<rightarrow> (Suc n)]))[X]\<^sub>\<nu>"
     by (metis B One_nat_def Suc_le_mono Suc_mono plus_1_eq_Suc subsequence_shift)
   ultimately
   show ?case
     unfolding af_subsequence_W unfolding semantics_ltln.simps GF_advice.simps by simp
 qed
 
 
 subsection \<open>Advice Functions and Propositional Entailment\<close>
 
 lemma GF_advice_prop_entailment:
   "\<A> \<Turnstile>\<^sub>P \<phi>[X]\<^sub>\<nu> \<Longrightarrow> {\<psi>. \<psi>[X]\<^sub>\<nu> \<in> \<A>} \<Turnstile>\<^sub>P \<phi>"
   "false\<^sub>n \<notin> \<A> \<Longrightarrow> {\<psi>. \<psi>[X]\<^sub>\<nu> \<in> \<A>} \<Turnstile>\<^sub>P \<phi> \<Longrightarrow> \<A> \<Turnstile>\<^sub>P \<phi>[X]\<^sub>\<nu>"
   by (induction \<phi>) (auto, meson, meson)
 
 lemma GF_advice_iff_prop_entailment:
   "false\<^sub>n \<notin> \<A> \<Longrightarrow> \<A> \<Turnstile>\<^sub>P \<phi>[X]\<^sub>\<nu> \<longleftrightarrow> {\<psi>. \<psi>[X]\<^sub>\<nu> \<in> \<A>} \<Turnstile>\<^sub>P \<phi>"
   by (metis GF_advice_prop_entailment)
 
 lemma FG_advice_prop_entailment:
   "true\<^sub>n \<in> \<A> \<Longrightarrow> \<A> \<Turnstile>\<^sub>P \<phi>[Y]\<^sub>\<mu> \<Longrightarrow> {\<psi>. \<psi>[Y]\<^sub>\<mu> \<in> \<A>} \<Turnstile>\<^sub>P \<phi>"
   "{\<psi>. \<psi>[Y]\<^sub>\<mu> \<in> \<A>} \<Turnstile>\<^sub>P \<phi> \<Longrightarrow> \<A> \<Turnstile>\<^sub>P \<phi>[Y]\<^sub>\<mu>"
   by (induction \<phi>) auto
 
 lemma FG_advice_iff_prop_entailment:
   "true\<^sub>n \<in> \<A> \<Longrightarrow> \<A> \<Turnstile>\<^sub>P \<phi>[X]\<^sub>\<mu> \<longleftrightarrow> {\<psi>. \<psi>[X]\<^sub>\<mu> \<in> \<A>} \<Turnstile>\<^sub>P \<phi>"
   by (metis FG_advice_prop_entailment)
 
 lemma GF_advice_subst:
   "\<phi>[X]\<^sub>\<nu> = subst \<phi> (\<lambda>\<psi>. Some (\<psi>[X]\<^sub>\<nu>))"
   by (induction \<phi>) auto
 
 lemma FG_advice_subst:
   "\<phi>[X]\<^sub>\<mu> = subst \<phi> (\<lambda>\<psi>. Some (\<psi>[X]\<^sub>\<mu>))"
   by (induction \<phi>) auto
 
 lemma GF_advice_prop_congruent:
   "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> \<phi>[X]\<^sub>\<nu> \<longrightarrow>\<^sub>P \<psi>[X]\<^sub>\<nu>"
   "\<phi> \<sim>\<^sub>P \<psi> \<Longrightarrow> \<phi>[X]\<^sub>\<nu> \<sim>\<^sub>P \<psi>[X]\<^sub>\<nu>"
   by (metis GF_advice_subst subst_respects_ltl_prop_entailment)+
 
 lemma FG_advice_prop_congruent:
   "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> \<phi>[X]\<^sub>\<mu> \<longrightarrow>\<^sub>P \<psi>[X]\<^sub>\<mu>"
   "\<phi> \<sim>\<^sub>P \<psi> \<Longrightarrow> \<phi>[X]\<^sub>\<mu> \<sim>\<^sub>P \<psi>[X]\<^sub>\<mu>"
   by (metis FG_advice_subst subst_respects_ltl_prop_entailment)+
 
+
+subsection \<open>GF-advice with Equivalence Relations\<close>
+
 locale GF_advice_congruent = ltl_equivalence +
+  fixes
+    normalise :: "'a ltln \<Rightarrow> 'a ltln"
   assumes
-    GF_advice_congruent: "\<phi> \<sim> \<psi> \<Longrightarrow> \<phi>[X]\<^sub>\<nu> \<sim> \<psi>[X]\<^sub>\<nu>"
+    normalise_eq: "\<phi> \<sim> normalise \<phi>"
+  assumes
+    normalise_monotonic: "w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu> \<Longrightarrow> w \<Turnstile>\<^sub>n (normalise \<phi>)[X]\<^sub>\<nu>"
+  assumes
+    normalise_eventually_equivalent:
+      "w \<Turnstile>\<^sub>n (normalise \<phi>)[X]\<^sub>\<nu> \<Longrightarrow> (\<exists>i. suffix i w \<Turnstile>\<^sub>n (af \<phi> (prefix i w))[X]\<^sub>\<nu>)"
+  assumes
+    GF_advice_congruent: "\<phi> \<sim> \<psi> \<Longrightarrow> (normalise \<phi>)[X]\<^sub>\<nu> \<sim> (normalise \<psi>)[X]\<^sub>\<nu>"
 begin
 
+lemma normalise_language_equivalent[simp]:
+  "w \<Turnstile>\<^sub>n normalise \<phi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
+  using normalise_eq ltl_lang_equiv_def eq_implies_lang by blast
+
 end
 
-interpretation prop_GF_advice_compatible: GF_advice_congruent "(\<sim>\<^sub>P)"
-  by unfold_locales (simp add: GF_advice_prop_congruent(2))
+interpretation prop_GF_advice_compatible: GF_advice_congruent "(\<sim>\<^sub>P)" "id"
+  by unfold_locales (simp add: GF_advice_af GF_advice_prop_congruent(2))+
 
 end
diff --git a/thys/LTL_Master_Theorem/Logical_Characterization/Extra_Equivalence_Relations.thy b/thys/LTL_Master_Theorem/Logical_Characterization/Extra_Equivalence_Relations.thy
new file mode 100644
--- /dev/null
+++ b/thys/LTL_Master_Theorem/Logical_Characterization/Extra_Equivalence_Relations.thy
@@ -0,0 +1,247 @@
+(*
+    Author:   Salomon Sickert
+    License:  BSD
+*)
+
+section \<open>Additional Equivalence Relations\<close>
+
+theory Extra_Equivalence_Relations
+imports
+  LTL.LTL LTL.Equivalence_Relations After Advice
+begin
+
+subsection \<open>Propositional Equivalence with Implicit LTL Unfolding\<close>
+
+fun Unf :: "'a ltln \<Rightarrow> 'a ltln"
+where
+  "Unf (\<phi> U\<^sub>n \<psi>) = ((\<phi> U\<^sub>n \<psi>) and\<^sub>n Unf \<phi>) or\<^sub>n Unf \<psi>"
+| "Unf (\<phi> W\<^sub>n \<psi>) = ((\<phi> W\<^sub>n \<psi>) and\<^sub>n Unf \<phi>) or\<^sub>n Unf \<psi>"
+| "Unf (\<phi> M\<^sub>n \<psi>) = ((\<phi> M\<^sub>n \<psi>) or\<^sub>n Unf \<phi>) and\<^sub>n Unf \<psi>"
+| "Unf (\<phi> R\<^sub>n \<psi>) = ((\<phi> R\<^sub>n \<psi>) or\<^sub>n Unf \<phi>) and\<^sub>n Unf \<psi>"
+| "Unf (\<phi> and\<^sub>n \<psi>) = Unf \<phi> and\<^sub>n Unf \<psi>"
+| "Unf (\<phi> or\<^sub>n \<psi>) = Unf \<phi> or\<^sub>n Unf \<psi>"
+| "Unf \<phi> = \<phi>"
+
+lemma Unf_sound:
+  "w \<Turnstile>\<^sub>n Unf \<phi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
+proof (induction \<phi> arbitrary: w)
+  case (Until_ltln \<phi>1 \<phi>2)
+  then show ?case
+    by (simp, metis less_linear not_less0 suffix_0)
+next
+  case (Release_ltln \<phi>1 \<phi>2)
+  then show ?case
+    by (simp, metis less_linear not_less0 suffix_0)
+next
+  case (WeakUntil_ltln \<phi>1 \<phi>2)
+  then show ?case
+    by (simp, metis bot.extremum_unique bot_nat_def less_eq_nat.simps(1) suffix_0)
+qed (simp_all, fastforce)
+
+lemma Unf_lang_equiv:
+  "\<phi> \<sim>\<^sub>L Unf \<phi>"
+  by (simp add: Unf_sound ltl_lang_equiv_def)
+
+lemma Unf_idem:
+  "Unf (Unf \<phi>) \<sim>\<^sub>P Unf \<phi>"
+  by (induction \<phi>) (auto simp: ltl_prop_equiv_def)
+
+definition ltl_prop_unfold_equiv :: "'a ltln \<Rightarrow> 'a ltln \<Rightarrow> bool" (infix "\<sim>\<^sub>Q" 75)
+where
+  "\<phi> \<sim>\<^sub>Q \<psi> \<equiv> (Unf \<phi>) \<sim>\<^sub>P (Unf \<psi>)"
+
+lemma ltl_prop_unfold_equiv_equivp:
+  "equivp (\<sim>\<^sub>Q)"
+  by (metis ltl_prop_equiv_equivp ltl_prop_unfold_equiv_def equivpI equivp_def reflpI sympI transpI)
+
+lemma unfolding_prop_unfold_idem:
+  "Unf \<phi> \<sim>\<^sub>Q \<phi>"
+  unfolding ltl_prop_unfold_equiv_def by (rule Unf_idem)
+
+lemma unfolding_is_subst: "Unf \<phi> = subst \<phi> (\<lambda>\<psi>. Some (Unf \<psi>))"
+  by (induction \<phi>) auto
+
+lemma ltl_prop_equiv_implies_ltl_prop_unfold_equiv:
+  "\<phi> \<sim>\<^sub>P \<psi> \<Longrightarrow> \<phi> \<sim>\<^sub>Q \<psi>"
+  by (metis ltl_prop_unfold_equiv_def unfolding_is_subst subst_respects_ltl_prop_entailment(2))
+
+lemma ltl_prop_unfold_equiv_implies_ltl_lang_equiv:
+  "\<phi> \<sim>\<^sub>Q \<psi> \<Longrightarrow> \<phi> \<sim>\<^sub>L \<psi>"
+  by (metis ltl_prop_equiv_implies_ltl_lang_equiv ltl_lang_equiv_def Unf_sound ltl_prop_unfold_equiv_def)
+
+lemma ltl_prop_unfold_equiv_gt_and_lt:
+  "(\<sim>\<^sub>C) \<le> (\<sim>\<^sub>Q)" "(\<sim>\<^sub>P) \<le> (\<sim>\<^sub>Q)" "(\<sim>\<^sub>Q) \<le> (\<sim>\<^sub>L)"
+  using ltl_prop_equiv_implies_ltl_prop_unfold_equiv ltl_prop_equivalence.ge_const_equiv ltl_prop_unfold_equiv_implies_ltl_lang_equiv
+  by blast+
+
+quotient_type 'a ltln\<^sub>Q = "'a ltln" / "(\<sim>\<^sub>Q)"
+  by (rule ltl_prop_unfold_equiv_equivp)
+
+instantiation ltln\<^sub>Q :: (type) equal
+begin
+
+lift_definition ltln\<^sub>Q_eq_test :: "'a ltln\<^sub>Q \<Rightarrow> 'a ltln\<^sub>Q \<Rightarrow> bool" is "\<lambda>x y. x \<sim>\<^sub>Q y"
+  by (metis ltln\<^sub>Q.abs_eq_iff)
+
+definition
+  eq\<^sub>Q: "equal_class.equal \<equiv> ltln\<^sub>Q_eq_test"
+
+instance
+  by (standard; simp add: eq\<^sub>Q ltln\<^sub>Q_eq_test.rep_eq, metis Quotient_ltln\<^sub>Q Quotient_rel_rep)
+
+end
+
+lemma af_letter_unfolding:
+  "af_letter (Unf \<phi>) \<nu> \<sim>\<^sub>P af_letter \<phi> \<nu>"
+  by (induction \<phi>) (simp_all add: ltl_prop_equiv_def, blast+)
+
+lemma af_letter_prop_unfold_congruent:
+  assumes "\<phi> \<sim>\<^sub>Q \<psi>"
+  shows "af_letter \<phi> \<nu> \<sim>\<^sub>Q af_letter \<psi> \<nu>"
+proof -
+  have "Unf \<phi> \<sim>\<^sub>P Unf \<psi>"
+    using assms by (simp add: ltl_prop_unfold_equiv_def ltl_prop_equiv_def)
+  then have "af_letter (Unf \<phi>) \<nu> \<sim>\<^sub>P af_letter (Unf \<psi>) \<nu>"
+    by (simp add: prop_af_congruent.af_letter_congruent)
+  then have "af_letter \<phi> \<nu> \<sim>\<^sub>P af_letter \<psi> \<nu>"
+    by (metis af_letter_unfolding ltl_prop_equivalence.eq_sym ltl_prop_equivalence.eq_trans)
+  then show "af_letter \<phi> \<nu> \<sim>\<^sub>Q af_letter \<psi> \<nu>"
+    by (rule ltl_prop_equiv_implies_ltl_prop_unfold_equiv)
+qed
+
+lemma GF_advice_prop_unfold_congruent:
+  assumes "\<phi> \<sim>\<^sub>Q \<psi>"
+  shows "(Unf \<phi>)[X]\<^sub>\<nu> \<sim>\<^sub>Q (Unf \<psi>)[X]\<^sub>\<nu>"
+proof -
+  have "Unf \<phi> \<sim>\<^sub>P Unf \<psi>"
+    using assms
+    by (simp add: ltl_prop_unfold_equiv_def ltl_prop_equiv_def)
+  then have "(Unf \<phi>)[X]\<^sub>\<nu> \<sim>\<^sub>P (Unf \<psi>)[X]\<^sub>\<nu>"
+    by (simp add: GF_advice_prop_congruent(2))
+  then show "(Unf \<phi>)[X]\<^sub>\<nu> \<sim>\<^sub>Q (Unf \<psi>)[X]\<^sub>\<nu>"
+    by (simp add: ltl_prop_equiv_implies_ltl_prop_unfold_equiv)
+qed
+
+interpretation prop_unfold_equivalence: ltl_equivalence "(\<sim>\<^sub>Q)"
+  by unfold_locales (metis ltl_prop_unfold_equiv_equivp ltl_prop_unfold_equiv_gt_and_lt)+
+
+interpretation af_congruent "(\<sim>\<^sub>Q)"
+  by unfold_locales (rule af_letter_prop_unfold_congruent)
+
+lemma unfolding_monotonic:
+  "w \<Turnstile>\<^sub>n \<phi>[X]\<^sub>\<nu> \<Longrightarrow> w \<Turnstile>\<^sub>n (Unf \<phi>)[X]\<^sub>\<nu>"
+proof (induction \<phi>)
+  case (Until_ltln \<phi>1 \<phi>2)
+  then show ?case
+    by (cases "(\<phi>1 U\<^sub>n \<phi>2) \<in> X") force+
+next
+  case (Release_ltln \<phi>1 \<phi>2)
+  then show ?case
+    using ltln_expand_Release by auto
+next
+  case (WeakUntil_ltln \<phi>1 \<phi>2)
+  then show ?case
+    using ltln_expand_WeakUntil by auto
+next
+  case (StrongRelease_ltln \<phi>1 \<phi>2)
+  then show ?case
+    by (cases "(\<phi>1 M\<^sub>n \<phi>2) \<in> X") force+
+qed auto
+
+lemma unfolding_next_step_equivalent:
+  "w \<Turnstile>\<^sub>n (Unf \<phi>)[X]\<^sub>\<nu> \<Longrightarrow> suffix 1 w \<Turnstile>\<^sub>n (af_letter \<phi> (w 0))[X]\<^sub>\<nu>"
+proof (induction \<phi>)
+  case (Next_ltln \<phi>)
+  then show ?case
+    unfolding Unf.simps by (metis GF_advice_af_letter build_split)
+next
+  case (Until_ltln \<phi>1 \<phi>2)
+  then show ?case
+    unfolding Unf.simps
+    by (metis GF_advice.simps(2) GF_advice.simps(3) GF_advice_af_letter af_letter.simps(8) build_split semantics_ltln.simps(5) semantics_ltln.simps(6))
+next
+  case (Release_ltln \<phi>1 \<phi>2)
+  then show ?case
+    unfolding Unf.simps
+    by (metis GF_advice.simps(2) GF_advice.simps(3) GF_advice_af_letter One_nat_def af_letter.simps(9) build_first semantics_ltln.simps(5) semantics_ltln.simps(6))
+next
+  case (WeakUntil_ltln \<phi>1 \<phi>2)
+  then show ?case
+    unfolding Unf.simps
+    by (metis GF_advice.simps(2) GF_advice.simps(3) GF_advice_af_letter af_letter.simps(10) build_split semantics_ltln.simps(5) semantics_ltln.simps(6))
+next
+  case (StrongRelease_ltln \<phi>1 \<phi>2)
+  then show ?case
+    unfolding Unf.simps
+    by (metis GF_advice.simps(2) GF_advice.simps(3) GF_advice_af_letter af_letter.simps(11) build_split semantics_ltln.simps(5) semantics_ltln.simps(6))
+qed auto
+
+lemma nested_prop_atoms_Unf:
+  "nested_prop_atoms (Unf \<phi>) \<subseteq> nested_prop_atoms \<phi>"
+  by (induction \<phi>) auto
+
+(* TODO move somewhere?? *)
+lemma refine_image:
+  assumes "\<And>x y. f x = f y \<longrightarrow> g x = g y"
+  assumes "finite (f ` X)"
+  shows "finite (g ` X)"
+  and "card (f ` X) \<ge> card (g ` X)"
+proof -
+  obtain Y where "Y \<subseteq> X" and "finite Y" and Y_def: "f ` X = f ` Y"
+    using assms by (meson finite_subset_image subset_refl)
+  moreover
+  {
+    fix x
+    assume "x \<in> X"
+    then have "g x \<in> g ` Y"
+      by (metis (no_types, hide_lams) \<open>x \<in> X\<close> assms(1) Y_def image_iff)
+  }
+  then have "g ` X = g ` Y"
+    using assms `Y \<subseteq> X` by blast
+  ultimately
+  show "finite (g ` X)"
+    by simp
+
+  from \<open>finite Y\<close> have "card (f ` Y) \<ge> card (g ` Y)"
+  proof (induction Y rule: finite_induct)
+    case (insert x F)
+
+    then have 1: "finite (g ` F)" and 2: "finite (f ` F)"
+      by simp_all
+
+    have "f x \<in> f ` F \<Longrightarrow> g x \<in> g ` F"
+      using assms(1) by blast
+
+    then show ?case
+      using insert by (simp add: card_insert_if[OF 1] card_insert_if[OF 2])
+  qed simp
+
+  then show "card (f ` X) \<ge> card (g ` X)"
+    by (simp add: Y_def \<open>g ` X = g ` Y\<close>)
+qed
+
+lemma abs_ltln\<^sub>P_implies_abs_ltln\<^sub>Q:
+  "abs_ltln\<^sub>P \<phi> = abs_ltln\<^sub>P \<psi> \<longrightarrow> abs_ltln\<^sub>Q \<phi> = abs_ltln\<^sub>Q \<psi>"
+  by (simp add: ltl_prop_equiv_implies_ltl_prop_unfold_equiv ltln\<^sub>P.abs_eq_iff ltln\<^sub>Q.abs_eq_iff)
+
+lemmas prop_unfold_equiv_helper = refine_image[of abs_ltln\<^sub>P abs_ltln\<^sub>Q, OF abs_ltln\<^sub>P_implies_abs_ltln\<^sub>Q]
+
+lemma prop_unfold_equiv_finite:
+  "finite P \<Longrightarrow> finite {abs_ltln\<^sub>Q \<psi> |\<psi>. prop_atoms \<psi> \<subseteq> P}"
+  using prop_unfold_equiv_helper(1)[OF prop_equiv_finite[unfolded image_Collect[symmetric]]]
+  unfolding image_Collect[symmetric] .
+
+lemma prop_unfold_equiv_card:
+  "finite P \<Longrightarrow> card {abs_ltln\<^sub>Q \<psi> |\<psi>. prop_atoms \<psi> \<subseteq> P} \<le> 2 ^ 2 ^ card P"
+  using prop_unfold_equiv_helper(2)[OF prop_equiv_finite[unfolded image_Collect[symmetric]]] prop_equiv_card
+  unfolding image_Collect[symmetric]
+  by fastforce
+
+lemma Unf_eventually_equivalent:
+  "w \<Turnstile>\<^sub>n Unf \<phi>[X]\<^sub>\<nu> \<Longrightarrow> \<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>"
+  by (metis (full_types) One_nat_def foldl.simps(1) foldl.simps(2) subsequence_singleton unfolding_next_step_equivalent)
+
+interpretation prop_unfold_GF_advice_compatible: GF_advice_congruent "(\<sim>\<^sub>Q)" Unf
+  by unfold_locales (simp_all add: unfolding_prop_unfold_idem prop_unfold_equivalence.eq_sym unfolding_monotonic Unf_eventually_equivalent GF_advice_prop_unfold_congruent)
+
+end
\ No newline at end of file
diff --git a/thys/LTL_Master_Theorem/code/ltl_to_dra_cli.sml b/thys/LTL_Master_Theorem/code/ltl_to_dra_cli.sml
--- a/thys/LTL_Master_Theorem/code/ltl_to_dra_cli.sml
+++ b/thys/LTL_Master_Theorem/code/ltl_to_dra_cli.sml
@@ -1,20 +1,20 @@
 (* Initialise Parser *)
 structure LtlParser = Ltl(PropLtl)
 
 (* Printers *)
 fun println x = print (x ^ "\n")
 fun println_err x = (TextIO.output (TextIO.stdErr, x ^ "\n"); TextIO.flushOut TextIO.stdErr)
 
 (* Main *)
 fun usage () = println ("Usage: " ^ CommandLine.name () ^ " ltlformula");
 
 fun main () =
   let 
     val e = fn () => OS.Process.exit (OS.Process.failure)
     val u = fn () => (usage(); e())
     val input = case CommandLine.arguments () of [] => valOf (TextIO.inputLine TextIO.stdIn) | x :: _ => x
     val phi = LtlParser.compile_from_string input handle LtlParser.LtlError msg => (println_err ("LTL Error: " ^ msg); usage (); e ())
-    val aut = LTL.ltlc_to_draei_literals phi
+    val aut = LTL.ltlc_to_draei_literals LTL.PropUnfold phi
   in 
     println (HOA.serialize phi aut)
   end