diff --git a/thys/LTL_Normal_Form/Normal_Form.thy b/thys/LTL_Normal_Form/Normal_Form.thy
new file mode 100644
--- /dev/null
+++ b/thys/LTL_Normal_Form/Normal_Form.thy
@@ -0,0 +1,423 @@
+(*
+    Author:   Salomon Sickert
+    License:  BSD
+*)
+
+section \<open>A Normal Form for Linear Temporal Logic\<close>
+
+theory Normal_Form imports
+  LTL_Master_Theorem.Master_Theorem
+begin
+
+subsection \<open>LTL Equivalences\<close>
+
+text \<open>Several valid laws of LTL relating strong and weak operators that are useful later.\<close>
+
+lemma ltln_strong_weak_2:
+  "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>) W\<^sub>n \<psi>" (is "?thesis1")
+  "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)" (is "?thesis2")
+proof -
+  have "\<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n \<psi>"
+    if "suffix j w \<Turnstile>\<^sub>n \<psi>" and "\<forall>j\<le>i. \<not> suffix j w \<Turnstile>\<^sub>n \<psi>" for i j
+  proof
+    from that have "j > i"
+      by (cases "j > i") auto
+    thus "suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<psi>"
+      using that by auto
+  qed
+  thus ?thesis1
+    unfolding ltln_strong_weak by auto
+next 
+  have "\<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n \<phi>"
+    if "suffix j w \<Turnstile>\<^sub>n \<phi>" and "\<forall>j<i. \<not> suffix j w \<Turnstile>\<^sub>n \<phi>" for i j
+  proof
+    from that have "j \<ge> i"
+      by (cases "j \<ge> i") auto
+    thus "suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<phi>"
+      using that by auto
+  qed
+  thus ?thesis2
+    unfolding ltln_strong_weak by auto
+qed
+
+lemma ltln_weak_strong_2:
+  "w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>)" (is "?thesis1")
+  "w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>" (is "?thesis2")
+proof -
+  have "suffix j w \<Turnstile>\<^sub>n \<phi>"
+    if "\<And>j. j < i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<phi>" and "\<And>j. suffix (i + j) w \<Turnstile>\<^sub>n \<phi>" for i j
+    using that(1)[of j] that(2)[of "j - i"] by (cases "j < i") simp_all
+  thus ?thesis1
+    unfolding ltln_weak_strong unfolding semantics_ltln.simps suffix_suffix by blast
+next
+  have "suffix j w \<Turnstile>\<^sub>n \<psi>"
+    if "\<And>j. j \<le> i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<psi>" and "\<And>j. suffix (i + j) w \<Turnstile>\<^sub>n \<psi>" for i j
+    using that(1)[of j] that(2)[of "j - i"] by (cases "j \<le> i") simp_all
+  thus ?thesis2
+    unfolding ltln_weak_strong unfolding semantics_ltln.simps suffix_suffix by blast
+qed
+
+subsection \<open>$\evalnu{\psi}{M}$, $\evalmu{\psi}{N}$, $\flatten{\psi}{M}$, and $\flattentwo{\psi}{N}$\<close>
+
+text \<open>The following four functions use "promise sets", named $M$ or $N$, to rewrite arbitrary 
+  formulas into formulas from the class $\Sigma_1$-, $\Sigma_2$-, $\Pi_1$-, and $\Pi_2$, 
+  respectively. In general the obtained formulas are not  equivalent, but under some conditions 
+  (as outlined below) they are.\<close>
+
+no_notation FG_advice ("_[_]\<^sub>\<mu>" [90,60] 89)
+no_notation GF_advice ("_[_]\<^sub>\<nu>" [90,60] 89)
+
+notation FG_advice ("_[_]\<^sub>\<Sigma>\<^sub>1" [90,60] 89)
+notation GF_advice ("_[_]\<^sub>\<Pi>\<^sub>1" [90,60] 89)
+
+fun flatten_sigma_2:: "'a ltln \<Rightarrow> 'a ltln set \<Rightarrow> 'a ltln" ("_[_]\<^sub>\<Sigma>\<^sub>2")
+where
+  "(\<phi> U\<^sub>n \<psi>)[M]\<^sub>\<Sigma>\<^sub>2 = (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) U\<^sub>n (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)"
+| "(\<phi> W\<^sub>n \<psi>)[M]\<^sub>\<Sigma>\<^sub>2 = (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) U\<^sub>n ((\<psi>[M]\<^sub>\<Sigma>\<^sub>2) or\<^sub>n (G\<^sub>n \<phi>[M]\<^sub>\<Pi>\<^sub>1))"
+| "(\<phi> M\<^sub>n \<psi>)[M]\<^sub>\<Sigma>\<^sub>2 = (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) M\<^sub>n (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)"
+| "(\<phi> R\<^sub>n \<psi>)[M]\<^sub>\<Sigma>\<^sub>2 = ((\<phi>[M]\<^sub>\<Sigma>\<^sub>2) or\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) M\<^sub>n (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)"
+| "(\<phi> and\<^sub>n \<psi>)[M]\<^sub>\<Sigma>\<^sub>2 = (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) and\<^sub>n (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)"
+| "(\<phi> or\<^sub>n \<psi>)[M]\<^sub>\<Sigma>\<^sub>2 = (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) or\<^sub>n (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)"
+| "(X\<^sub>n \<phi>)[M]\<^sub>\<Sigma>\<^sub>2 = X\<^sub>n (\<phi>[M]\<^sub>\<Sigma>\<^sub>2)"
+| "\<phi>[M]\<^sub>\<Sigma>\<^sub>2 = \<phi>"
+
+fun flatten_pi_2 :: "'a ltln \<Rightarrow> 'a ltln set \<Rightarrow> 'a ltln" ("_[_]\<^sub>\<Pi>\<^sub>2")
+where
+  "(\<phi> W\<^sub>n \<psi>)[N]\<^sub>\<Pi>\<^sub>2 = (\<phi>[N]\<^sub>\<Pi>\<^sub>2) W\<^sub>n (\<psi>[N]\<^sub>\<Pi>\<^sub>2)"
+| "(\<phi> U\<^sub>n \<psi>)[N]\<^sub>\<Pi>\<^sub>2 = (\<phi>[N]\<^sub>\<Pi>\<^sub>2 and\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) W\<^sub>n (\<psi>[N]\<^sub>\<Pi>\<^sub>2)"
+| "(\<phi> R\<^sub>n \<psi>)[N]\<^sub>\<Pi>\<^sub>2 = (\<phi>[N]\<^sub>\<Pi>\<^sub>2) R\<^sub>n (\<psi>[N]\<^sub>\<Pi>\<^sub>2)"
+| "(\<phi> M\<^sub>n \<psi>)[N]\<^sub>\<Pi>\<^sub>2 = (\<phi>[N]\<^sub>\<Pi>\<^sub>2) R\<^sub>n ((\<psi>[N]\<^sub>\<Pi>\<^sub>2) and\<^sub>n (F\<^sub>n \<phi>[N]\<^sub>\<Sigma>\<^sub>1))"
+| "(\<phi> and\<^sub>n \<psi>)[N]\<^sub>\<Pi>\<^sub>2 = (\<phi>[N]\<^sub>\<Pi>\<^sub>2) and\<^sub>n (\<psi>[N]\<^sub>\<Pi>\<^sub>2)"
+| "(\<phi> or\<^sub>n \<psi>)[N]\<^sub>\<Pi>\<^sub>2 = (\<phi>[N]\<^sub>\<Pi>\<^sub>2) or\<^sub>n (\<psi>[N]\<^sub>\<Pi>\<^sub>2)"
+| "(X\<^sub>n \<phi>)[N]\<^sub>\<Pi>\<^sub>2 = X\<^sub>n (\<phi>[N]\<^sub>\<Pi>\<^sub>2)"
+| "\<phi>[N]\<^sub>\<Pi>\<^sub>2 = \<phi>"
+
+lemma GF_advice_restriction:
+  "\<phi>[\<G>\<F> (\<phi> W\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1 = \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1"
+  "\<psi>[\<G>\<F> (\<phi> R\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1 = \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1"
+  by (metis (no_types, lifting) \<G>\<F>_semantics' inf_commute inf_left_commute inf_sup_absorb subformulas\<^sub>\<mu>.simps(6) GF_advice_inter_subformulas) 
+     (metis (no_types, lifting) GF_advice_inter \<G>\<F>.simps(5) \<G>\<F>_semantics' \<G>\<F>_subformulas\<^sub>\<mu> inf.commute sup.boundedE)
+
+lemma FG_advice_restriction: 
+  "\<psi>[\<F>\<G> (\<phi> U\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1 = \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1"
+  "\<phi>[\<F>\<G> (\<phi> M\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1 = \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1"  
+  by (metis (no_types, lifting) FG_advice_inter \<F>\<G>.simps(4) \<F>\<G>_semantics' \<F>\<G>_subformulas\<^sub>\<nu> inf.commute sup.boundedE) 
+     (metis (no_types, lifting) FG_advice_inter \<F>\<G>.simps(7) \<F>\<G>_semantics' \<F>\<G>_subformulas\<^sub>\<nu> inf.right_idem inf_commute sup.cobounded1) 
+
+lemma flatten_sigma_2_intersection:
+  "M \<inter> subformulas\<^sub>\<mu> \<phi> \<subseteq> S \<Longrightarrow> \<phi>[M \<inter> S]\<^sub>\<Sigma>\<^sub>2 = \<phi>[M]\<^sub>\<Sigma>\<^sub>2"
+  by (induction \<phi>) (simp; blast intro: GF_advice_inter)+
+
+lemma flatten_sigma_2_intersection_eq:
+  "M \<inter> subformulas\<^sub>\<mu> \<phi> = M' \<Longrightarrow> \<phi>[M']\<^sub>\<Sigma>\<^sub>2 = \<phi>[M]\<^sub>\<Sigma>\<^sub>2"
+  using flatten_sigma_2_intersection by auto
+
+lemma flatten_sigma_2_monotone: 
+  "w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<Longrightarrow> M \<subseteq> M' \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[M']\<^sub>\<Sigma>\<^sub>2"
+  by (induction \<phi> arbitrary: w)
+     (simp; blast dest: GF_advice_monotone)+
+
+lemma flatten_pi_2_intersection:
+  "N \<inter> subformulas\<^sub>\<nu> \<phi> \<subseteq> S \<Longrightarrow> \<phi>[N \<inter> S]\<^sub>\<Pi>\<^sub>2 = \<phi>[N]\<^sub>\<Pi>\<^sub>2"
+  by (induction \<phi>) (simp; blast intro: FG_advice_inter)+
+
+lemma flatten_pi_2_intersection_eq:
+  "N \<inter> subformulas\<^sub>\<nu> \<phi> = N' \<Longrightarrow> \<phi>[N']\<^sub>\<Pi>\<^sub>2 = \<phi>[N]\<^sub>\<Pi>\<^sub>2"
+  using flatten_pi_2_intersection by auto
+
+lemma flatten_pi_2_monotone: 
+  "w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<Longrightarrow> N \<subseteq> N' \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[N']\<^sub>\<Pi>\<^sub>2"
+  by (induction \<phi> arbitrary: w)
+     (simp; blast dest: FG_advice_monotone)+
+
+lemma ltln_weak_strong_stable_words_1:
+  "w \<Turnstile>\<^sub>n (\<phi> W\<^sub>n \<psi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n (G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1))" (is "?lhs \<longleftrightarrow> ?rhs") 
+proof 
+  assume ?lhs
+  
+  moreover
+
+  {
+    assume assm: "w \<Turnstile>\<^sub>n G\<^sub>n \<phi>"
+    moreover
+    obtain i where "\<And>j. \<F> \<phi> (suffix i w) \<subseteq> \<G>\<F> \<phi> w"
+      by (metis MOST_nat_le \<G>\<F>_suffix \<mu>_stable_def order_refl suffix_\<mu>_stable)
+    hence "\<And>j. \<F> \<phi> (suffix i (suffix j w)) \<subseteq> \<G>\<F> \<phi> w"
+      by (metis \<F>_suffix \<G>\<F>_\<F>_subset \<G>\<F>_suffix semiring_normalization_rules(24) subset_Un_eq suffix_suffix sup.orderE)
+    ultimately
+    have "suffix i w \<Turnstile>\<^sub>n G\<^sub>n (\<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)"
+      using GF_advice_a1[OF \<open>\<And>j. \<F> \<phi> (suffix i (suffix j w)) \<subseteq> \<G>\<F> \<phi> w\<close>]
+      by (simp add: add.commute)
+    hence "?rhs"
+      using assm by auto 
+  }
+
+  moreover
+
+  have "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> ?rhs"
+    by auto
+  
+  ultimately
+
+  show ?rhs
+    using ltln_weak_to_strong(1) by blast
+next
+  assume ?rhs
+  thus ?lhs
+    unfolding ltln_weak_strong_2 unfolding semantics_ltln.simps
+    by (metis \<G>\<F>_suffix order_refl GF_advice_a2)
+qed
+
+lemma ltln_weak_strong_stable_words_2:
+  "w \<Turnstile>\<^sub>n (\<phi> R\<^sub>n \<psi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n (G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1)) M\<^sub>n \<psi>" (is "?lhs \<longleftrightarrow> ?rhs") 
+proof 
+  assume ?lhs
+  
+  moreover
+
+  {
+    assume assm: "w \<Turnstile>\<^sub>n G\<^sub>n \<psi>"
+    moreover
+    obtain i where "\<And>j. \<F> \<psi> (suffix i w) \<subseteq> \<G>\<F> \<psi> w"
+      by (metis MOST_nat_le \<G>\<F>_suffix \<mu>_stable_def order_refl suffix_\<mu>_stable)
+    hence "\<And>j. \<F> \<psi> (suffix i (suffix j w)) \<subseteq> \<G>\<F> \<psi> w"
+      by (metis \<F>_suffix \<G>\<F>_\<F>_subset \<G>\<F>_suffix semiring_normalization_rules(24) subset_Un_eq suffix_suffix sup.orderE)
+    ultimately
+    have "suffix i w \<Turnstile>\<^sub>n G\<^sub>n (\<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1)"
+      using GF_advice_a1[OF \<open>\<And>j. \<F> \<psi> (suffix i (suffix j w)) \<subseteq> \<G>\<F> \<psi> w\<close>]
+      by (simp add: add.commute)
+    hence "?rhs"
+      using assm by auto 
+  }
+
+  moreover
+
+  have "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> ?rhs"
+    by auto
+  
+  ultimately
+
+  show ?rhs
+    using ltln_weak_to_strong by blast
+next
+  assume ?rhs
+  thus ?lhs
+    unfolding ltln_weak_strong_2 unfolding semantics_ltln.simps
+    by (metis GF_advice_a2 \<G>\<F>_suffix order_refl)
+qed
+
+lemma ltln_weak_strong_stable_words:
+  "w \<Turnstile>\<^sub>n (\<phi> W\<^sub>n \<psi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n (G\<^sub>n \<phi>[\<G>\<F> (\<phi> W\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1))"
+  "w \<Turnstile>\<^sub>n (\<phi> R\<^sub>n \<psi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n (G\<^sub>n \<psi>[\<G>\<F> (\<phi> R\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1)) M\<^sub>n \<psi>"
+  unfolding ltln_weak_strong_stable_words_1 ltln_weak_strong_stable_words_2 GF_advice_restriction by simp+
+
+lemma flatten_sigma_2_IH_lifting: 
+  assumes "\<psi> \<in> subfrmlsn \<phi>"
+  assumes "suffix i w \<Turnstile>\<^sub>n \<psi>[\<G>\<F> \<psi> (suffix i w)]\<^sub>\<Sigma>\<^sub>2 = suffix i w \<Turnstile>\<^sub>n \<psi>"
+  shows "suffix i w \<Turnstile>\<^sub>n \<psi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = suffix i w \<Turnstile>\<^sub>n \<psi>" 
+  by (metis (no_types, lifting) inf.absorb_iff2 inf_assoc inf_commute assms(2) \<G>\<F>_suffix flatten_sigma_2_intersection_eq[of "\<G>\<F> \<phi> w" \<psi> "\<G>\<F> \<psi> w"] \<G>\<F>_semantics' subformulas\<^sub>\<mu>_subset[OF assms(1)])
+  
+lemma flatten_sigma_2_correct:
+  "w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
+proof (induction \<phi> arbitrary: w)
+  case (And_ltln \<phi>1 \<phi>2)
+  then show ?case 
+    using flatten_sigma_2_IH_lifting[of _ "\<phi>1 and\<^sub>n \<phi>2" 0] by simp
+next
+  case (Or_ltln \<phi>1 \<phi>2)
+  then show ?case 
+    using flatten_sigma_2_IH_lifting[of _ "\<phi>1 or\<^sub>n \<phi>2" 0] by simp
+next
+  case (Next_ltln \<phi>)
+  then show ?case 
+    using flatten_sigma_2_IH_lifting[of _ "X\<^sub>n \<phi>" 1] by fastforce
+next
+  case (Until_ltln \<phi>1 \<phi>2)
+  then show ?case
+    using flatten_sigma_2_IH_lifting[of _ "\<phi>1 U\<^sub>n \<phi>2"] by fastforce
+next
+  case (Release_ltln \<phi>1 \<phi>2)
+  then show ?case
+    unfolding ltln_weak_strong_stable_words
+    using flatten_sigma_2_IH_lifting[of _ "\<phi>1 R\<^sub>n \<phi>2"] by fastforce
+next
+  case (WeakUntil_ltln \<phi>1 \<phi>2)
+  then show ?case
+    unfolding ltln_weak_strong_stable_words
+    using flatten_sigma_2_IH_lifting[of _ "\<phi>1 W\<^sub>n \<phi>2"] by fastforce
+next
+case (StrongRelease_ltln \<phi>1 \<phi>2)
+  then show ?case
+    using flatten_sigma_2_IH_lifting[of _ "\<phi>1 M\<^sub>n \<phi>2"] by fastforce
+qed auto
+
+lemma ltln_strong_weak_stable_words_1:
+  "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n (F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1)) W\<^sub>n \<psi>" (is "?lhs \<longleftrightarrow> ?rhs") 
+proof 
+  assume ?rhs
+
+  moreover
+
+  obtain i where "\<nu>_stable \<psi> (suffix i w)"
+    by (metis MOST_nat less_Suc_eq suffix_\<nu>_stable)
+  hence "\<forall>\<psi> \<in> \<F>\<G> \<psi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>"
+    using \<F>\<G>_suffix \<G>_elim \<nu>_stable_def by blast
+
+  {
+    assume assm: "w \<Turnstile>\<^sub>n G\<^sub>n (\<phi> and\<^sub>n (F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1))"
+    hence "suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<psi>)[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1"
+      by simp
+    hence "suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<psi>"
+      by (blast dest: FG_advice_b2_helper[OF \<open>\<forall>\<psi> \<in> \<F>\<G> \<psi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>\<close>])
+    hence "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>"
+      using assm by auto
+  }
+
+  ultimately
+  
+  show ?lhs
+    by (meson ltln_weak_to_strong(1) semantics_ltln.simps(5) until_and_left_distrib)
+next 
+  assume ?lhs 
+
+  moreover
+
+  have "\<And>i. suffix i w \<Turnstile>\<^sub>n \<psi> \<Longrightarrow> suffix i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1"
+    using \<F>\<G>_suffix by (blast intro: FG_advice_b1)
+
+  ultimately
+
+  show "?rhs"
+    unfolding ltln_strong_weak_2 by fastforce
+qed
+
+lemma ltln_strong_weak_stable_words_2:
+  "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n (F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1))" (is "?lhs \<longleftrightarrow> ?rhs") 
+proof 
+  assume ?rhs
+
+  moreover
+
+  obtain i where "\<nu>_stable \<phi> (suffix i w)"
+    by (metis MOST_nat less_Suc_eq suffix_\<nu>_stable)
+  hence "\<forall>\<psi> \<in> \<F>\<G> \<phi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>"
+    using \<F>\<G>_suffix \<G>_elim \<nu>_stable_def by blast
+
+  {
+    assume assm: "w \<Turnstile>\<^sub>n G\<^sub>n (\<psi> and\<^sub>n (F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1))"
+    hence "suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<phi>)[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1"
+      by simp
+    hence "suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<phi>"
+      by (blast dest: FG_advice_b2_helper[OF \<open>\<forall>\<psi> \<in> \<F>\<G> \<phi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>\<close>])
+    hence "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>"
+      using assm by auto
+  }
+
+  ultimately
+  
+  show ?lhs
+    using ltln_weak_to_strong(3) semantics_ltln.simps(5) strong_release_and_right_distrib by blast
+next 
+  assume ?lhs 
+
+  moreover
+
+  have "\<And>i. suffix i w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> suffix i w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1"
+    using \<F>\<G>_suffix by (blast intro: FG_advice_b1)
+
+  ultimately
+
+  show "?rhs"
+    unfolding ltln_strong_weak_2 by fastforce
+qed
+
+lemma ltln_strong_weak_stable_words:
+  "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n (F\<^sub>n \<psi>[\<F>\<G> (\<phi> U\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1)) W\<^sub>n \<psi>"
+  "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n (F\<^sub>n \<phi>[\<F>\<G> (\<phi> M\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1))"
+  unfolding ltln_strong_weak_stable_words_1 ltln_strong_weak_stable_words_2 FG_advice_restriction by simp+
+
+lemma flatten_pi_2_IH_lifting: 
+  assumes "\<psi> \<in> subfrmlsn \<phi>"
+  assumes "suffix i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> (suffix i w)]\<^sub>\<Pi>\<^sub>2 = suffix i w \<Turnstile>\<^sub>n \<psi>"
+  shows "suffix i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = suffix i w \<Turnstile>\<^sub>n \<psi>" 
+  by (metis (no_types, lifting) inf.absorb_iff2 inf_assoc inf_commute assms(2) \<F>\<G>_suffix flatten_pi_2_intersection_eq[of "\<F>\<G> \<phi> w" \<psi> "\<F>\<G> \<psi> w"] \<F>\<G>_semantics' subformulas\<^sub>\<nu>_subset[OF assms(1)])
+
+lemma flatten_pi_2_correct:
+  "w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
+proof (induction \<phi> arbitrary: w)
+  case (And_ltln \<phi>1 \<phi>2)
+  then show ?case 
+    using flatten_pi_2_IH_lifting[of _ "\<phi>1 and\<^sub>n \<phi>2" 0] by simp
+next
+  case (Or_ltln \<phi>1 \<phi>2)
+  then show ?case 
+    using flatten_pi_2_IH_lifting[of _ "\<phi>1 or\<^sub>n \<phi>2" 0] by simp
+next
+  case (Next_ltln \<phi>)
+  then show ?case 
+    using flatten_pi_2_IH_lifting[of _ "X\<^sub>n \<phi>" 1] by fastforce
+next
+  case (Until_ltln \<phi>1 \<phi>2)
+  then show ?case
+    unfolding ltln_strong_weak_stable_words
+    using flatten_pi_2_IH_lifting[of _ "\<phi>1 U\<^sub>n \<phi>2"] by fastforce
+next
+  case (Release_ltln \<phi>1 \<phi>2)
+  then show ?case
+    using flatten_pi_2_IH_lifting[of _ "\<phi>1 R\<^sub>n \<phi>2"] by fastforce
+next
+  case (WeakUntil_ltln \<phi>1 \<phi>2)
+  then show ?case
+    using flatten_pi_2_IH_lifting[of _ "\<phi>1 W\<^sub>n \<phi>2"] by fastforce
+next
+case (StrongRelease_ltln \<phi>1 \<phi>2)
+  then show ?case
+    unfolding ltln_strong_weak_stable_words
+    using flatten_pi_2_IH_lifting[of _ "\<phi>1 M\<^sub>n \<phi>2"] by fastforce
+qed auto
+
+subsection \<open>Main Theorem\<close>
+
+text \<open>Using the four previously defined functions we obtain our normal form.\<close>
+
+theorem normal_form_with_flatten_sigma_2:
+  "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> 
+    (\<exists>M \<subseteq> subformulas\<^sub>\<mu> \<phi>. \<exists>N \<subseteq> subformulas\<^sub>\<nu> \<phi>.
+      w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi> \<in> M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi> \<in> N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)))" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs
+  then have "w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2"
+    using flatten_sigma_2_correct by blast
+  then show ?rhs
+    using \<G>\<F>_subformulas\<^sub>\<mu> \<F>\<G>_subformulas\<^sub>\<nu> \<G>\<F>_implies_GF \<F>\<G>_implies_FG by metis 
+next
+  assume ?rhs
+  then obtain M N where "w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2" and "M \<subseteq> \<G>\<F> \<phi> w" and "N \<subseteq> \<F>\<G> \<phi> w"
+    using X_\<G>\<F>_Y_\<F>\<G> by blast
+  then have "w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2"
+    using flatten_sigma_2_monotone by blast
+  then show ?lhs
+    using flatten_sigma_2_correct by blast
+qed
+
+theorem normal_form_with_flatten_pi_2:
+  "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> 
+    (\<exists>M \<subseteq> subformulas\<^sub>\<mu> \<phi>. \<exists>N \<subseteq> subformulas\<^sub>\<nu> \<phi>.
+      w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi> \<in> M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi> \<in> N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)))" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs
+  then have "w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2"
+    using flatten_pi_2_correct by blast
+  then show ?rhs
+    using \<G>\<F>_subformulas\<^sub>\<mu> \<F>\<G>_subformulas\<^sub>\<nu> \<G>\<F>_implies_GF \<F>\<G>_implies_FG by metis 
+next
+  assume ?rhs
+  then obtain M N where "w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2" and "M \<subseteq> \<G>\<F> \<phi> w" and "N \<subseteq> \<F>\<G> \<phi> w"
+    using X_\<G>\<F>_Y_\<F>\<G> by metis
+  then have "w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2"
+    using flatten_pi_2_monotone by metis
+  then show ?lhs
+    using flatten_pi_2_correct by blast
+qed
+
+end
\ No newline at end of file
diff --git a/thys/LTL_Normal_Form/Normal_Form_Code_Export.thy b/thys/LTL_Normal_Form/Normal_Form_Code_Export.thy
new file mode 100644
--- /dev/null
+++ b/thys/LTL_Normal_Form/Normal_Form_Code_Export.thy
@@ -0,0 +1,134 @@
+(*
+    Author:   Salomon Sickert
+    License:  BSD
+*)
+
+section \<open>Code Export\<close>
+
+theory Normal_Form_Code_Export imports
+  LTL.Code_Equations
+  LTL.Rewriting
+  LTL.Disjunctive_Normal_Form
+  HOL.String
+  Normal_Form
+begin
+
+fun flatten_pi_1_list :: "String.literal ltln \<Rightarrow> String.literal ltln list \<Rightarrow> String.literal ltln"
+  where
+  "flatten_pi_1_list (\<psi>\<^sub>1 U\<^sub>n \<psi>\<^sub>2) M = (if (\<psi>\<^sub>1 U\<^sub>n \<psi>\<^sub>2) \<in> set M then (flatten_pi_1_list \<psi>\<^sub>1 M) W\<^sub>n (flatten_pi_1_list \<psi>\<^sub>2 M) else false\<^sub>n)"
+| "flatten_pi_1_list (\<psi>\<^sub>1 W\<^sub>n \<psi>\<^sub>2) M = (flatten_pi_1_list \<psi>\<^sub>1 M) W\<^sub>n (flatten_pi_1_list \<psi>\<^sub>2 M)"
+| "flatten_pi_1_list (\<psi>\<^sub>1 M\<^sub>n \<psi>\<^sub>2) M = (if (\<psi>\<^sub>1 M\<^sub>n \<psi>\<^sub>2) \<in> set M then (flatten_pi_1_list \<psi>\<^sub>1 M) R\<^sub>n (flatten_pi_1_list \<psi>\<^sub>2 M) else false\<^sub>n)"
+| "flatten_pi_1_list (\<psi>\<^sub>1 R\<^sub>n \<psi>\<^sub>2) M = (flatten_pi_1_list \<psi>\<^sub>1 M) R\<^sub>n (flatten_pi_1_list \<psi>\<^sub>2 M)"
+| "flatten_pi_1_list (\<psi>\<^sub>1 and\<^sub>n \<psi>\<^sub>2) M = (flatten_pi_1_list \<psi>\<^sub>1 M) and\<^sub>n (flatten_pi_1_list \<psi>\<^sub>2 M)"
+| "flatten_pi_1_list (\<psi>\<^sub>1 or\<^sub>n \<psi>\<^sub>2) M = (flatten_pi_1_list \<psi>\<^sub>1 M) or\<^sub>n (flatten_pi_1_list \<psi>\<^sub>2 M)"
+| "flatten_pi_1_list (X\<^sub>n \<psi>) M = X\<^sub>n (flatten_pi_1_list \<psi> M)"
+| "flatten_pi_1_list \<phi> _ = \<phi>"
+
+fun flatten_sigma_1_list :: "String.literal ltln \<Rightarrow> String.literal ltln list \<Rightarrow> String.literal ltln"
+where
+  "flatten_sigma_1_list (\<psi>\<^sub>1 U\<^sub>n \<psi>\<^sub>2) N = (flatten_sigma_1_list \<psi>\<^sub>1 N) U\<^sub>n (flatten_sigma_1_list \<psi>\<^sub>2 N)"
+| "flatten_sigma_1_list (\<psi>\<^sub>1 W\<^sub>n \<psi>\<^sub>2) N = (if (\<psi>\<^sub>1 W\<^sub>n \<psi>\<^sub>2) \<in> set N then true\<^sub>n else (flatten_sigma_1_list \<psi>\<^sub>1 N) U\<^sub>n (flatten_sigma_1_list \<psi>\<^sub>2 N))"
+| "flatten_sigma_1_list (\<psi>\<^sub>1 M\<^sub>n \<psi>\<^sub>2) N = (flatten_sigma_1_list \<psi>\<^sub>1 N) M\<^sub>n (flatten_sigma_1_list \<psi>\<^sub>2 N)"
+| "flatten_sigma_1_list (\<psi>\<^sub>1 R\<^sub>n \<psi>\<^sub>2) N = (if (\<psi>\<^sub>1 R\<^sub>n \<psi>\<^sub>2) \<in> set N then true\<^sub>n else (flatten_sigma_1_list \<psi>\<^sub>1 N) M\<^sub>n (flatten_sigma_1_list \<psi>\<^sub>2 N))"
+| "flatten_sigma_1_list (\<psi>\<^sub>1 and\<^sub>n \<psi>\<^sub>2) N = (flatten_sigma_1_list \<psi>\<^sub>1 N) and\<^sub>n (flatten_sigma_1_list \<psi>\<^sub>2 N)"
+| "flatten_sigma_1_list (\<psi>\<^sub>1 or\<^sub>n \<psi>\<^sub>2) N = (flatten_sigma_1_list \<psi>\<^sub>1 N) or\<^sub>n (flatten_sigma_1_list \<psi>\<^sub>2 N)"
+| "flatten_sigma_1_list (X\<^sub>n \<psi>) N = X\<^sub>n (flatten_sigma_1_list \<psi> N)"
+| "flatten_sigma_1_list \<phi> _ = \<phi>"
+
+fun flatten_sigma_2_list :: "String.literal ltln \<Rightarrow> String.literal ltln list \<Rightarrow> String.literal ltln"
+where
+  "flatten_sigma_2_list (\<phi> U\<^sub>n \<psi>) M = (flatten_sigma_2_list \<phi> M) U\<^sub>n (flatten_sigma_2_list \<psi> M)"
+| "flatten_sigma_2_list (\<phi> W\<^sub>n \<psi>) M = (flatten_sigma_2_list \<phi> M) U\<^sub>n ((flatten_sigma_2_list \<psi> M) or\<^sub>n (G\<^sub>n (flatten_pi_1_list \<phi> M)))"
+| "flatten_sigma_2_list (\<phi> M\<^sub>n \<psi>) M = (flatten_sigma_2_list \<phi> M) M\<^sub>n (flatten_sigma_2_list \<psi> M)"
+| "flatten_sigma_2_list (\<phi> R\<^sub>n \<psi>) M = ((flatten_sigma_2_list \<phi> M) or\<^sub>n (G\<^sub>n (flatten_pi_1_list \<psi> M))) M\<^sub>n (flatten_sigma_2_list \<psi> M)"
+| "flatten_sigma_2_list (\<phi> and\<^sub>n \<psi>) M = (flatten_sigma_2_list \<phi> M) and\<^sub>n (flatten_sigma_2_list \<psi> M)"
+| "flatten_sigma_2_list (\<phi> or\<^sub>n \<psi>) M = (flatten_sigma_2_list \<phi> M) or\<^sub>n (flatten_sigma_2_list \<psi> M)"
+| "flatten_sigma_2_list (X\<^sub>n \<phi>) M = X\<^sub>n (flatten_sigma_2_list \<phi> M)"
+| "flatten_sigma_2_list \<phi> _ = \<phi>"
+
+lemma flatten_code_equations[simp]:
+  "\<phi>[set M]\<^sub>\<Pi>\<^sub>1 = flatten_pi_1_list \<phi> M"
+  "\<phi>[set M]\<^sub>\<Sigma>\<^sub>1 = flatten_sigma_1_list \<phi> M"
+  "\<phi>[set M]\<^sub>\<Sigma>\<^sub>2 = flatten_sigma_2_list \<phi> M"
+  by (induction \<phi>) auto
+
+abbreviation "and_list \<equiv> foldl And_ltln true\<^sub>n"
+
+abbreviation "or_list \<equiv> foldl Or_ltln false\<^sub>n"
+
+definition "normal_form_disjunct (\<phi> :: String.literal ltln) M N 
+  \<equiv> (flatten_sigma_2_list \<phi> M)
+      and\<^sub>n (and_list (map (\<lambda>\<psi>. G\<^sub>n (F\<^sub>n (flatten_sigma_1_list \<psi> N))) M) 
+      and\<^sub>n (and_list (map (\<lambda>\<psi>. F\<^sub>n (G\<^sub>n (flatten_pi_1_list    \<psi> M))) N)))"
+
+definition "normal_form (\<phi> :: String.literal ltln) 
+  \<equiv> or_list (map (\<lambda>(M, N). normal_form_disjunct \<phi> M N) (advice_sets \<phi>))" 
+
+lemma and_list_semantic: "w \<Turnstile>\<^sub>n and_list xs \<longleftrightarrow> (\<forall>x \<in> set xs. w \<Turnstile>\<^sub>n x)"
+  by (induction xs rule: rev_induct) auto 
+
+lemma or_list_semantic: "w \<Turnstile>\<^sub>n or_list xs \<longleftrightarrow> (\<exists>x \<in> set xs. w \<Turnstile>\<^sub>n x)"
+  by (induction xs rule: rev_induct) auto
+
+theorem normal_form_correct:
+  "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> w \<Turnstile>\<^sub>n normal_form \<phi>"
+proof 
+  assume "w \<Turnstile>\<^sub>n \<phi>"
+  then obtain M N where "M \<subseteq> subformulas\<^sub>\<mu> \<phi>" and "N \<subseteq> subformulas\<^sub>\<nu> \<phi>"
+    and c1: "w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2" and c2: "\<forall>\<psi> \<in> M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)" and c3: "\<forall>\<psi> \<in> N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)"
+    using normal_form_with_flatten_sigma_2 by metis
+  then obtain ms ns where "M = set ms" and "N = set ns" and ms_ns_in: "(ms, ns) \<in> set (advice_sets \<phi>)" 
+    by (meson advice_sets_subformulas)
+  then have "w \<Turnstile>\<^sub>n normal_form_disjunct \<phi> ms ns"
+    using c1 c2 c3 by (simp add: and_list_semantic normal_form_disjunct_def)
+  then show "w \<Turnstile>\<^sub>n normal_form \<phi>"
+    using normal_form_def or_list_semantic ms_ns_in by fastforce
+next
+  assume "w \<Turnstile>\<^sub>n normal_form \<phi>"
+  then obtain ms ns where "(ms, ns) \<in> set (advice_sets \<phi>)" 
+    and "w \<Turnstile>\<^sub>n normal_form_disjunct \<phi> ms ns"
+    unfolding normal_form_def or_list_semantic by force
+  then have "set ms \<subseteq> subformulas\<^sub>\<mu> \<phi>" and "set ns \<subseteq> subformulas\<^sub>\<nu> \<phi>"
+    and c1: "w \<Turnstile>\<^sub>n \<phi>[set ms]\<^sub>\<Sigma>\<^sub>2" and c2: "\<forall>\<psi> \<in> set ms. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[set ns]\<^sub>\<Sigma>\<^sub>1)" and c3: "\<forall>\<psi> \<in> set ns. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[set ms]\<^sub>\<Pi>\<^sub>1)"  
+    using advice_sets_element_subfrmlsn 
+    by (auto simp: and_list_semantic normal_form_disjunct_def) blast
+  then show "w \<Turnstile>\<^sub>n \<phi>"
+    using normal_form_with_flatten_sigma_2 by metis
+qed
+
+definition "normal_form_with_simplifier (\<phi> :: String.literal ltln) 
+  \<equiv> min_dnf (simplify Slow (normal_form (simplify Slow \<phi>)))" 
+
+lemma ltl_semantics_min_dnf:
+  "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> (\<exists>C \<in> min_dnf \<phi>. \<forall>\<psi>. \<psi> |\<in>| C \<longrightarrow> w \<Turnstile>\<^sub>n \<psi>)" (is "?lhs \<longleftrightarrow> ?rhs")
+proof 
+  let ?M = "{\<psi>. w \<Turnstile>\<^sub>n \<psi>}"
+  assume ?lhs
+  hence "?M \<Turnstile>\<^sub>P \<phi>"
+    using ltl_models_equiv_prop_entailment by blast
+  then obtain M' where "fset M' \<subseteq> ?M" and "M' \<in> min_dnf \<phi>"
+    using min_dnf_iff_prop_assignment_subset by blast
+  thus ?rhs
+    by (meson in_mono mem_Collect_eq notin_fset)
+next 
+  let ?M = "{\<psi>. w \<Turnstile>\<^sub>n \<psi>}"
+  assume ?rhs
+  then obtain M' where "fset M' \<subseteq> ?M" and "M' \<in> min_dnf \<phi>"
+    using notin_fset by fastforce
+  hence "?M \<Turnstile>\<^sub>P \<phi>"
+    using min_dnf_iff_prop_assignment_subset by blast
+  thus ?lhs
+    using ltl_models_equiv_prop_entailment by blast
+qed
+
+theorem 
+  "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> (\<exists>C \<in> (normal_form_with_simplifier \<phi>). \<forall>\<psi>. \<psi> |\<in>| C \<longrightarrow> w \<Turnstile>\<^sub>n \<psi>)" (is "?lhs \<longleftrightarrow> ?rhs")
+  unfolding normal_form_with_simplifier_def ltl_semantics_min_dnf[symmetric] 
+  using normal_form_correct by simp
+
+text \<open>In order to export the code run \texttt{isabelle build -D [PATH] -e}.\<close>
+
+export_code normal_form in SML
+export_code normal_form_with_simplifier in SML
+
+end
\ No newline at end of file
diff --git a/thys/LTL_Normal_Form/Normal_Form_Complexity.thy b/thys/LTL_Normal_Form/Normal_Form_Complexity.thy
new file mode 100644
--- /dev/null
+++ b/thys/LTL_Normal_Form/Normal_Form_Complexity.thy
@@ -0,0 +1,650 @@
+(*
+    Author:   Salomon Sickert
+    License:  BSD
+*)
+
+section \<open>Size Bounds\<close>
+
+text \<open>We prove an exponential upper bound for the normalisation procedure. Moreover, we show that 
+  the number of proper subformulas, which correspond to states very-weak alternating automata 
+  (A1W), is only linear for each disjunct.\<close>
+
+theory Normal_Form_Complexity imports
+  Normal_Form
+begin
+
+subsection \<open>Inequalities and Identities\<close>
+
+lemma inequality_1: 
+  "y > 0 \<Longrightarrow> y + 3 \<le> (2 :: nat) ^ (y + 1)"
+  by (induction y) (simp, fastforce)
+
+lemma inequality_2: 
+  "x > 0 \<Longrightarrow> y > 0 \<Longrightarrow> ((2 :: nat) ^ (x + 1)) + (2 ^ (y + 1)) \<le> (2 ^ (x + y + 1))"
+  by (induction x; simp; induction y; simp; fastforce)
+
+lemma size_gr_0: 
+  "size (\<phi> :: 'a ltln) > 0" 
+  by (cases \<phi>) simp_all
+
+lemma sum_associative:
+  "finite X \<Longrightarrow> (\<Sum>x \<in> X. f x + c) = (\<Sum>x \<in> X. f x) + card X * c"
+  by (induction rule: finite_induct) simp_all
+
+subsection \<open>Length\<close>
+
+text \<open>We prove that the length (size) of the resulting formula in normal form is at most exponential.\<close>
+
+lemma flatten_sigma_1_length: 
+  "size (\<phi>[N]\<^sub>\<Sigma>\<^sub>1) \<le> size \<phi>"
+  by (induction \<phi>) simp_all
+
+lemma flatten_pi_1_length: 
+  "size (\<phi>[M]\<^sub>\<Pi>\<^sub>1) \<le> size \<phi>"
+  by (induction \<phi>) simp_all
+
+lemma flatten_sigma_2_length: 
+  "size (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) \<le> 2 ^ (size \<phi> + 1)"
+proof (induction \<phi>)
+  case (And_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 and\<^sub>n \<phi>2)[M]\<^sub>\<Sigma>\<^sub>2  \<le> (2 ^ (size \<phi>1 + 1)) + (2 ^ (size \<phi>2 + 1)) + 1"
+    by simp
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + size \<phi>2 + 1) + 1 "
+    using inequality_2[OF size_gr_0 size_gr_0] by simp
+  also
+  have "\<dots> \<le> 2 ^ (size (\<phi>1 and\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (Or_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 or\<^sub>n \<phi>2)[M]\<^sub>\<Sigma>\<^sub>2  \<le> (2 ^ (size \<phi>1 + 1)) + (2 ^ (size \<phi>2 + 1)) + 1"
+    by simp
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + size \<phi>2 + 1) + 1 "
+    using inequality_2[OF size_gr_0 size_gr_0] by simp
+  also
+  have "\<dots> \<le> 2 ^ (size (\<phi>1 or\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (Next_ltln \<phi>)
+  then show ?case 
+    using le_Suc_eq by fastforce
+next
+  case (WeakUntil_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 W\<^sub>n \<phi>2)[M]\<^sub>\<Sigma>\<^sub>2 \<le> 2 ^ (size \<phi>1 + 1) + 2 ^ (size \<phi>2 + 1) + size \<phi>1 + 4"
+    by (simp, simp add: add.commute add_mono flatten_pi_1_length)
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>2 + 1) + 2 * 2 ^ (size \<phi>1 + 1) + 1"
+    using inequality_1[OF size_gr_0, of \<phi>1] by simp
+  also
+  have "\<dots> \<le> 2 * (2 ^ (size \<phi>1 + 1) + 2 ^ (size \<phi>2 + 1))"
+    by simp
+  also
+  have "\<dots> \<le> 2 * 2 ^ (size \<phi>1 + size \<phi>2 + 1)"
+    using inequality_2[OF size_gr_0 size_gr_0] mult_le_mono2 by blast 
+  also
+  have "\<dots> = 2 ^ (size (\<phi>1 W\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (StrongRelease_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 M\<^sub>n \<phi>2)[M]\<^sub>\<Sigma>\<^sub>2  \<le> (2 ^ (size \<phi>1 + 1)) + (2 ^ (size \<phi>2 + 1)) + 1"
+    by simp
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + size \<phi>2 + 1) + 1 "
+    using inequality_2[OF size_gr_0 size_gr_0] by simp
+  also
+  have "\<dots> \<le> 2 ^ (size (\<phi>1 M\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (Until_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 U\<^sub>n \<phi>2)[M]\<^sub>\<Sigma>\<^sub>2  \<le> (2 ^ (size \<phi>1 + 1)) + (2 ^ (size \<phi>2 + 1)) + 1"
+    by simp
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + size \<phi>2 + 1) + 1 "
+    using inequality_2[OF size_gr_0 size_gr_0] by simp
+  also
+  have "\<dots> \<le> 2 ^ (size (\<phi>1 U\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (Release_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 R\<^sub>n \<phi>2)[M]\<^sub>\<Sigma>\<^sub>2 \<le> 2 ^ (size \<phi>1 + 1) + 2 ^ (size \<phi>2 + 1) + size \<phi>2 + 4"
+    by (simp, simp add: add.commute add_mono flatten_pi_1_length)
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + 1) + 2 * 2 ^ (size \<phi>2 + 1) + 1"
+    using inequality_1[OF size_gr_0, of \<phi>2] by simp
+  also
+  have "\<dots> \<le> 2 * (2 ^ (size \<phi>1 + 1) + 2 ^ (size \<phi>2 + 1))"
+    by simp
+  also
+  have "\<dots> \<le> 2 * 2 ^ (size \<phi>1 + size \<phi>2 + 1)"
+    using inequality_2[OF size_gr_0 size_gr_0] mult_le_mono2 by blast 
+  also
+  have "\<dots> = 2 ^ (size (\<phi>1 R\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case .
+qed auto
+
+lemma flatten_pi_2_length: 
+  "size (\<phi>[N]\<^sub>\<Pi>\<^sub>2) \<le> 2 ^ (size \<phi> + 1)"
+proof (induction \<phi>)
+  case (And_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 and\<^sub>n \<phi>2)[N]\<^sub>\<Pi>\<^sub>2  \<le> (2 ^ (size \<phi>1 + 1)) + (2 ^ (size \<phi>2 + 1)) + 1"
+    by simp
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + size \<phi>2 + 1) + 1 "
+    using inequality_2[OF size_gr_0 size_gr_0] by simp
+  also
+  have "\<dots> \<le> 2 ^ (size (\<phi>1 and\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (Or_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 or\<^sub>n \<phi>2)[N]\<^sub>\<Pi>\<^sub>2  \<le> (2 ^ (size \<phi>1 + 1)) + (2 ^ (size \<phi>2 + 1)) + 1"
+    by simp
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + size \<phi>2 + 1) + 1 "
+    using inequality_2[OF size_gr_0 size_gr_0] by simp
+  also
+  have "\<dots> \<le> 2 ^ (size (\<phi>1 or\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (Next_ltln \<phi>)
+  then show ?case 
+    using le_Suc_eq by fastforce
+next
+  case (Until_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 U\<^sub>n \<phi>2)[N]\<^sub>\<Pi>\<^sub>2 \<le> 2 ^ (size \<phi>1 + 1) + 2 ^ (size \<phi>2 + 1) + size \<phi>2 + 4"
+    by (simp, simp add: add.commute add_mono flatten_sigma_1_length)
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + 1) + 2 * 2 ^ (size \<phi>2 + 1) + 1"
+    using inequality_1[OF size_gr_0, of \<phi>2] by simp
+  also
+  have "\<dots> \<le> 2 * (2 ^ (size \<phi>1 + 1) + 2 ^ (size \<phi>2 + 1))"
+    by simp
+  also
+  have "\<dots> \<le> 2 * 2 ^ (size \<phi>1 + size \<phi>2 + 1)"
+    using inequality_2[OF size_gr_0 size_gr_0] mult_le_mono2 by blast 
+  also
+  have "\<dots> = 2 ^ (size (\<phi>1 U\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (Release_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 R\<^sub>n \<phi>2)[N]\<^sub>\<Pi>\<^sub>2  \<le> (2 ^ (size \<phi>1 + 1)) + (2 ^ (size \<phi>2 + 1)) + 1"
+    by simp
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + size \<phi>2 + 1) + 1 "
+    using inequality_2[OF size_gr_0 size_gr_0] by simp
+  also
+  have "\<dots> \<le> 2 ^ (size (\<phi>1 R\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (WeakUntil_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 W\<^sub>n \<phi>2)[N]\<^sub>\<Pi>\<^sub>2  \<le> (2 ^ (size \<phi>1 + 1)) + (2 ^ (size \<phi>2 + 1)) + 1"
+    by simp
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>1 + size \<phi>2 + 1) + 1 "
+    using inequality_2[OF size_gr_0 size_gr_0] by simp
+  also
+  have "\<dots> \<le> 2 ^ (size (\<phi>1 W\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case.
+next
+  case (StrongRelease_ltln \<phi>1 \<phi>2)
+  hence "size (\<phi>1 M\<^sub>n \<phi>2)[N]\<^sub>\<Pi>\<^sub>2 \<le> 2 ^ (size \<phi>1 + 1) + 2 ^ (size \<phi>2 + 1) + size \<phi>1 + 4"
+    by (simp, simp add: add.commute add_mono flatten_sigma_1_length)
+  also
+  have "\<dots> \<le> 2 ^ (size \<phi>2 + 1) + 2 * 2 ^ (size \<phi>1 + 1) + 1"
+    using inequality_1[OF size_gr_0, of \<phi>1] by simp
+  also
+  have "\<dots> \<le> 2 * (2 ^ (size \<phi>1 + 1) + 2 ^ (size \<phi>2 + 1))"
+    by simp
+  also
+  have "\<dots> \<le> 2 * 2 ^ (size \<phi>1 + size \<phi>2 + 1)"
+    using inequality_2[OF size_gr_0 size_gr_0] mult_le_mono2 by blast 
+  also
+  have "\<dots> = 2 ^ (size (\<phi>1 M\<^sub>n \<phi>2) + 1)"
+    by simp
+  finally
+  show ?case .
+qed auto
+
+definition "normal_form_length_upper_bound"
+  where "normal_form_length_upper_bound \<phi>
+    \<equiv> (2 :: nat) ^ (size \<phi>) * (2 ^ (size \<phi> + 1) + 2 * (size \<phi> + 2) ^ 2)"
+
+definition "normal_form_disjunct_with_flatten_pi_2_length"
+  where "normal_form_disjunct_with_flatten_pi_2_length \<phi> M N
+    \<equiv> size (\<phi>[N]\<^sub>\<Pi>\<^sub>2) + (\<Sum>\<psi> \<in> M. size (\<psi>[N]\<^sub>\<Sigma>\<^sub>1) + 2) + (\<Sum>\<psi> \<in> N. size (\<psi>[M]\<^sub>\<Pi>\<^sub>1) + 2)" 
+
+definition "normal_form_with_flatten_pi_2_length"
+  where "normal_form_with_flatten_pi_2_length \<phi> 
+    \<equiv> \<Sum>(M, N) \<in> {(M, N) | M N. M \<subseteq> subformulas\<^sub>\<mu> \<phi> \<and> N \<subseteq> subformulas\<^sub>\<nu> \<phi>}. normal_form_disjunct_with_flatten_pi_2_length \<phi> M N"
+
+definition "normal_form_disjunct_with_flatten_sigma_2_length"
+  where "normal_form_disjunct_with_flatten_sigma_2_length \<phi> M N 
+    \<equiv> size (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) + (\<Sum>\<psi> \<in> M. size (\<psi>[N]\<^sub>\<Sigma>\<^sub>1) + 2) + (\<Sum>\<psi> \<in> N. size (\<psi>[M]\<^sub>\<Pi>\<^sub>1) + 2)" 
+
+definition "normal_form_with_flatten_sigma_2_length"
+  where "normal_form_with_flatten_sigma_2_length \<phi> 
+    \<equiv> \<Sum>(M, N) \<in> {(M, N) | M N. M \<subseteq> subformulas\<^sub>\<mu> \<phi> \<and> N \<subseteq> subformulas\<^sub>\<nu> \<phi>}. normal_form_disjunct_with_flatten_sigma_2_length \<phi> M N"
+
+lemma normal_form_disjunct_length_upper_bound:
+  assumes 
+    "M \<subseteq> subformulas\<^sub>\<mu> \<phi>" 
+    "N \<subseteq> subformulas\<^sub>\<nu> \<phi>"
+  shows 
+    "normal_form_disjunct_with_flatten_sigma_2_length \<phi> M N \<le> 2 ^ (size \<phi> + 1) + 2 * (size \<phi> + 2) ^ 2" (is "?thesis1")
+    "normal_form_disjunct_with_flatten_pi_2_length \<phi> M N \<le> 2 ^ (size \<phi> + 1) + 2 * (size \<phi> + 2) ^ 2" (is "?thesis2")
+proof -
+  let ?n = "size \<phi>"
+  let ?b = "2 ^ (?n + 1) + ?n * (?n + 2) + ?n * (?n + 2)"
+
+  have finite_M: "finite M" and card_M: "card M \<le> ?n"
+    by (metis assms(1) finite_subset subformulas\<^sub>\<mu>_finite)
+       (meson assms(1) card_mono order_trans subformulas\<^sub>\<mu>_subfrmlsn subfrmlsn_card subfrmlsn_finite) 
+
+  have finite_N: "finite N" and card_N: "card N \<le> ?n"
+    by (metis assms(2) finite_subset subformulas\<^sub>\<nu>_finite)
+       (meson assms(2) card_mono order_trans subformulas\<^sub>\<nu>_subfrmlsn subfrmlsn_card subfrmlsn_finite) 
+
+  have size_M: "\<And>\<psi>. \<psi> \<in> M \<Longrightarrow> size \<psi> \<le> size \<phi>"
+    and size_N: "\<And>\<psi>. \<psi> \<in> N \<Longrightarrow> size \<psi> \<le> size \<phi>"
+    by (metis assms(1) eq_iff in_mono less_imp_le subformulas\<^sub>\<mu>_subfrmlsn subfrmlsn_size)
+       (metis assms(2) eq_iff in_mono less_imp_le subformulas\<^sub>\<nu>_subfrmlsn subfrmlsn_size)
+
+  hence size_M': "\<And>\<psi>. \<psi> \<in> M \<Longrightarrow> size (\<psi>[N]\<^sub>\<Sigma>\<^sub>1) \<le> size \<phi>"
+    and size_N': "\<And>\<psi>. \<psi> \<in> N \<Longrightarrow> size (\<psi>[M]\<^sub>\<Pi>\<^sub>1) \<le> size \<phi>"
+    using flatten_sigma_1_length flatten_pi_1_length order_trans by blast+
+
+  have "(\<Sum>\<psi> \<in> M. size (\<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<le> ?n * ?n"
+    and "(\<Sum>\<psi> \<in> N. size (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<le> ?n * ?n"
+    using sum_bounded_above[of M, OF size_M'] sum_bounded_above[of N, OF size_N']
+    using mult_le_mono[OF card_M] mult_le_mono[OF card_N] by fastforce+
+     
+  hence "(\<Sum>\<psi> \<in> M. (size (\<psi>[N]\<^sub>\<Sigma>\<^sub>1) + 2)) \<le> ?n * (?n + 2)"
+    and "(\<Sum>\<psi> \<in> N. (size (\<psi>[M]\<^sub>\<Pi>\<^sub>1) + 2)) \<le> ?n * (?n + 2)"
+    unfolding sum_associative[OF finite_M] sum_associative[OF finite_N]
+    using card_M card_N by simp_all
+
+  hence "normal_form_disjunct_with_flatten_sigma_2_length \<phi> M N \<le> ?b"
+    and "normal_form_disjunct_with_flatten_pi_2_length \<phi> M N \<le> ?b"
+    unfolding normal_form_disjunct_with_flatten_sigma_2_length_def normal_form_disjunct_with_flatten_pi_2_length_def 
+    by (metis (no_types, lifting) flatten_sigma_2_length flatten_pi_2_length add_le_mono)+
+
+  thus ?thesis1 and ?thesis2
+    by (simp_all add: power2_eq_square)
+qed
+
+theorem normal_form_length_upper_bound:
+  "normal_form_with_flatten_sigma_2_length \<phi> \<le> normal_form_length_upper_bound \<phi>" (is "?thesis1")
+  "normal_form_with_flatten_pi_2_length \<phi> \<le> normal_form_length_upper_bound \<phi>" (is "?thesis2")
+proof -
+  let ?n = "size \<phi>"
+  let ?b = "2 ^ (size \<phi> + 1) + 2 * (size \<phi> + 2) ^ 2"
+
+  have "{(M, N) | M N. M \<subseteq> subformulas\<^sub>\<mu> \<phi> \<and> N \<subseteq> subformulas\<^sub>\<nu> \<phi>} = {M. M \<subseteq> subformulas\<^sub>\<mu> \<phi>} \<times> {N. N \<subseteq> subformulas\<^sub>\<nu> \<phi>}" (is "?choices = _")
+    by simp
+  
+  moreover
+  
+  have "card {M. M \<subseteq> subformulas\<^sub>\<mu> \<phi>} = (2 :: nat) ^ (card (subformulas\<^sub>\<mu> \<phi>))"
+    and "card {N. N \<subseteq> subformulas\<^sub>\<nu> \<phi>} = (2 :: nat) ^ (card (subformulas\<^sub>\<nu> \<phi>))"
+    using card_Pow unfolding Pow_def using subformulas\<^sub>\<mu>_finite subformulas\<^sub>\<nu>_finite by auto
+  
+  ultimately
+  
+  have "card ?choices \<le> 2 ^ (card (subfrmlsn \<phi>))" (is "?f \<le> _")
+    by (metis subformulas\<^sub>\<mu>\<^sub>\<nu>_card card_cartesian_product subformulas\<^sub>\<mu>\<^sub>\<nu>_subfrmlsn subfrmlsn_finite Suc_1 card_mono lessI power_add power_increasing_iff)
+  
+  moreover
+  
+  have "(2 :: nat) ^ (card (subfrmlsn \<phi>)) \<le> 2 ^ ?n"
+    using power_increasing[of _ _ "2 :: nat"] by (simp add: subfrmlsn_card)
+  
+  ultimately
+  
+  have bar: "of_nat (card ?choices) \<le> (2 :: nat) ^ ?n"
+    using of_nat_id by presburger
+
+  moreover
+
+  have "normal_form_with_flatten_sigma_2_length \<phi> \<le> of_nat (card ?choices) * ?b"
+    unfolding normal_form_with_flatten_sigma_2_length_def
+    by (rule sum_bounded_above) (insert normal_form_disjunct_length_upper_bound, auto)
+
+  moreover
+
+  have "normal_form_with_flatten_pi_2_length \<phi> \<le> of_nat (card ?choices) * ?b"
+    unfolding normal_form_with_flatten_pi_2_length_def
+    by (rule sum_bounded_above) (insert normal_form_disjunct_length_upper_bound, auto)
+
+  ultimately
+
+  show ?thesis1 and ?thesis2
+    unfolding normal_form_length_upper_bound_def 
+    using mult_le_mono1 order_trans by blast+
+qed
+
+subsection \<open>Proper Subformulas\<close>
+
+text \<open>We prove that the number of (proper) subformulas (sf) in a disjunct is linear and not exponential.\<close>
+
+fun sf :: "'a ltln \<Rightarrow> 'a ltln set"
+where
+  "sf (\<phi> and\<^sub>n \<psi>) = sf \<phi> \<union> sf \<psi>"
+| "sf (\<phi> or\<^sub>n \<psi>) = sf \<phi> \<union> sf \<psi>"
+| "sf (X\<^sub>n \<phi>) = {X\<^sub>n \<phi>} \<union> sf \<phi>"
+| "sf (\<phi> U\<^sub>n \<psi>) = {\<phi> U\<^sub>n \<psi>} \<union> sf \<phi> \<union> sf \<psi>"
+| "sf (\<phi> R\<^sub>n \<psi>) = {\<phi> R\<^sub>n \<psi>} \<union> sf \<phi> \<union> sf \<psi>"
+| "sf (\<phi> W\<^sub>n \<psi>) = {\<phi> W\<^sub>n \<psi>} \<union> sf \<phi> \<union> sf \<psi>"
+| "sf (\<phi> M\<^sub>n \<psi>) = {\<phi> M\<^sub>n \<psi>} \<union> sf \<phi> \<union> sf \<psi>"
+| "sf \<phi> = {}"
+
+lemma sf_finite: 
+  "finite (sf \<phi>)"
+  by (induction \<phi>) auto
+
+lemma sf_subset_subfrmlsn: 
+  "sf \<phi> \<subseteq> subfrmlsn \<phi>"
+  by (induction \<phi>) auto
+
+lemma sf_size:
+  "\<psi> \<in> sf \<phi> \<Longrightarrow> size \<psi> \<le> size \<phi>"
+  by (induction \<phi>) auto
+
+lemma sf_sf_subset: 
+  "\<psi> \<in> sf \<phi> \<Longrightarrow> sf \<psi> \<subseteq> sf \<phi>"
+  by (induction \<phi>) auto
+
+lemma subfrmlsn_sf_subset: 
+  "\<psi> \<in> subfrmlsn \<phi> \<Longrightarrow> sf \<psi> \<subseteq> sf \<phi>"
+  by (induction \<phi>) auto
+
+lemma sf_subset_insert:
+  assumes "sf \<phi> \<subseteq> insert \<phi> X"
+  assumes "\<psi> \<in> subfrmlsn \<phi>"
+  assumes "\<phi> \<noteq> \<psi>" 
+  shows "sf \<psi> \<subseteq> X" 
+proof -
+  have "sf \<psi> \<subseteq> sf \<phi> - {\<phi>}"
+    using assms(2,3) subfrmlsn_sf_subset sf_size subfrmlsn_size by fastforce
+  thus "?thesis"
+    using assms(1) by auto
+qed
+
+lemma flatten_pi_1_sf_subset: 
+  "sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1) \<subseteq> (\<Union>\<phi>\<in>sf \<phi>. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1))"
+  by (induction \<phi>) auto
+
+lemma flatten_sigma_1_sf_subset: 
+  "sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>1) \<subseteq> (\<Union>\<phi>\<in>sf \<phi>. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>1))"
+  by (induction \<phi>) auto
+
+lemma flatten_sigma_2_sf_subset: 
+  "sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) \<subseteq> (\<Union>\<psi>\<in>sf \<phi>. sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>2))"
+  by (induction \<phi>) auto
+
+lemma sf_set1: 
+  "sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1) \<subseteq> (\<Union>\<psi> \<in> (sf \<phi>). (sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>2) \<union> sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)))"
+  by (induction \<phi>) auto
+
+(* TODO: could be moved *)
+lemma ltln_not_idempotent [simp]:
+  "\<phi> and\<^sub>n \<psi> \<noteq> \<phi>" "\<psi> and\<^sub>n \<phi> \<noteq> \<phi>" "\<phi> \<noteq> \<phi> and\<^sub>n \<psi>" "\<phi> \<noteq> \<psi> and\<^sub>n \<phi>"
+  "\<phi> or\<^sub>n \<psi> \<noteq> \<phi>" "\<psi> or\<^sub>n \<phi> \<noteq> \<phi>" "\<phi> \<noteq> \<phi> or\<^sub>n \<psi>" "\<phi> \<noteq> \<psi> or\<^sub>n \<phi>"
+  "X\<^sub>n \<phi> \<noteq> \<phi>" "\<phi> \<noteq> X\<^sub>n \<phi>"
+  "\<phi> U\<^sub>n \<psi> \<noteq> \<phi>" "\<phi> \<noteq> \<phi> U\<^sub>n \<psi>" "\<psi> U\<^sub>n \<phi> \<noteq> \<phi>" "\<phi> \<noteq> \<psi> U\<^sub>n \<phi>"
+  "\<phi> R\<^sub>n \<psi> \<noteq> \<phi>" "\<phi> \<noteq> \<phi> R\<^sub>n \<psi>" "\<psi> R\<^sub>n \<phi> \<noteq> \<phi>" "\<phi> \<noteq> \<psi> R\<^sub>n \<phi>"
+  "\<phi> W\<^sub>n \<psi> \<noteq> \<phi>" "\<phi> \<noteq> \<phi> W\<^sub>n \<psi>" "\<psi> W\<^sub>n \<phi> \<noteq> \<phi>" "\<phi> \<noteq> \<psi> W\<^sub>n \<phi>"
+  "\<phi> M\<^sub>n \<psi> \<noteq> \<phi>" "\<phi> \<noteq> \<phi> M\<^sub>n \<psi>" "\<psi> M\<^sub>n \<phi> \<noteq> \<phi>" "\<phi> \<noteq> \<psi> M\<^sub>n \<phi>"
+  by (induction \<phi>; force)+
+
+lemma flatten_card_sf_induct:
+  assumes "finite X"
+  assumes "\<And>x. x \<in> X \<Longrightarrow> sf x \<subseteq> X"
+  shows "card (\<Union>\<phi>\<in>X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)) \<le> card X 
+   \<and> card (\<Union>\<phi>\<in>X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<le> card X 
+   \<and> card (\<Union>\<phi>\<in>X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<le> 3 * card X"
+  using assms(2)
+proof (induction rule: finite_ranking_induct[where f = size, OF \<open>finite X\<close>])
+  case (2 \<psi> X)
+    {
+      assume "\<psi> \<notin> X"
+      hence "\<And>\<chi>. \<chi> \<in> X \<Longrightarrow> sf \<chi> \<subseteq> X"
+        using 2(2,4) sf_subset_subfrmlsn subfrmlsn_size by fastforce
+      hence "card (\<Union>\<phi>\<in>X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)) \<le> card X"
+        and "card (\<Union>\<phi>\<in>X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<le> card X"        
+        and "card (\<Union>\<phi>\<in>X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<le> 3 * card X"
+        using 2(3) by simp+
+      
+      moreover
+
+      let ?lower1 = "\<Union>\<phi> \<in> insert \<psi> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)"
+      let ?upper1 = "(\<Union>\<phi> \<in> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)) \<union> {\<psi>[N]\<^sub>\<Sigma>\<^sub>1}"
+
+      let ?lower2 = "\<Union>\<phi> \<in> insert \<psi> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)"
+      let ?upper2 = "(\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}"
+
+      let ?lower3 = "\<Union>\<phi> \<in> insert \<psi> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)"
+      let ?upper3_cases = "{\<psi>[M]\<^sub>\<Sigma>\<^sub>2, \<psi>[M]\<^sub>\<Pi>\<^sub>1} \<union> (case \<psi> of (\<phi>1 W\<^sub>n \<phi>2) \<Rightarrow> {G\<^sub>n (\<phi>1[M]\<^sub>\<Pi>\<^sub>1)} | (\<phi>1 R\<^sub>n \<phi>2) \<Rightarrow> {G\<^sub>n (\<phi>2[M]\<^sub>\<Pi>\<^sub>1)} | _ \<Rightarrow> {})"
+      let ?upper3 = "(\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> ?upper3_cases"
+
+      have finite_upper1: "finite (?upper1)"
+        and finite_upper2: "finite (?upper2)" 
+        and finite_upper3: "finite (?upper3)" 
+        using 2(1) sf_finite by auto (cases \<psi>, auto)
+
+      have "\<And>x y. card {x, y} \<le> 3"
+        and "\<And>x y z. card {x, y, z} \<le> 3"
+        by (simp add: card_insert_if le_less)+
+      hence card_leq_3: "card (?upper3_cases) \<le> 3"
+        by (cases \<psi>) (simp_all, fast)
+
+      note card_subset_split_rule = le_trans[OF card_mono card_Un_le]
+
+      have sf_in_X: "sf \<psi> \<subseteq> insert \<psi> X"
+        using 2 by blast
+
+      have "?lower1 \<subseteq> ?upper1 \<and> ?lower2 \<subseteq> ?upper2 \<and> ?lower3 \<subseteq> ?upper3" 
+      proof (cases \<psi>)
+        case (And_ltln \<psi>\<^sub>1 \<psi>\<^sub>2)
+        have *: "sf \<psi>\<^sub>1 \<subseteq> X" "sf \<psi>\<^sub>2 \<subseteq> X" 
+          by (rule sf_subset_insert[OF sf_in_X, unfolded And_ltln]; simp)+
+
+        have "(sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2))"
+          and "(sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1))"
+          and "(sf (\<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1))"
+          subgoal
+            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: And_ltln)
+          subgoal
+            using flatten_pi_1_sf_subset[of _ M] * by (force simp: And_ltln)
+          subgoal 
+            using flatten_sigma_1_sf_subset * by (force simp: And_ltln)
+          done
+        
+        thus ?thesis 
+          by blast
+      next
+        case (Or_ltln \<psi>\<^sub>1 \<psi>\<^sub>2)
+        have *: "sf \<psi>\<^sub>1 \<subseteq> X" "sf \<psi>\<^sub>2 \<subseteq> X"
+          by (rule sf_subset_insert[OF sf_in_X, unfolded Or_ltln]; simp)+
+
+        have "(sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2))"
+          and "(sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1))"
+          and "(sf (\<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1))"
+          subgoal
+            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: Or_ltln)
+          subgoal
+            using flatten_pi_1_sf_subset[of _ M] * by (force simp: Or_ltln)
+          subgoal 
+            using flatten_sigma_1_sf_subset * by (force simp: Or_ltln)
+          done
+          
+        thus ?thesis 
+          by blast
+      next
+        case (Next_ltln \<psi>\<^sub>1)
+        have *: "sf \<psi>\<^sub>1 \<subseteq> X" 
+          by (rule sf_subset_insert[OF sf_in_X, unfolded Next_ltln]) simp_all
+  
+        have "(sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2)) \<union> {\<psi>[M]\<^sub>\<Sigma>\<^sub>2}"
+          and "(sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}"
+          and "(sf (\<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)) \<union> {\<psi>[N]\<^sub>\<Sigma>\<^sub>1}"
+          subgoal
+            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: Next_ltln)
+          subgoal
+            using flatten_pi_1_sf_subset[of _ M] * by (force simp: Next_ltln)
+          subgoal 
+            using flatten_sigma_1_sf_subset * by (force simp: Next_ltln)
+          done
+        
+        thus ?thesis
+          by blast
+      next
+        case (Until_ltln \<psi>\<^sub>1 \<psi>\<^sub>2)
+        have *: "sf \<psi>\<^sub>1 \<subseteq> X" "sf \<psi>\<^sub>2 \<subseteq> X"
+          by (rule sf_subset_insert[OF sf_in_X, unfolded Until_ltln]; simp)+
+  
+        hence "(sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2)) \<union> {\<psi>[M]\<^sub>\<Sigma>\<^sub>2}"
+          and "(sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}"
+          and "(sf (\<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)) \<union> {\<psi>[N]\<^sub>\<Sigma>\<^sub>1}"
+          subgoal
+            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: Until_ltln)
+          subgoal
+            using flatten_pi_1_sf_subset[of _ M] * by (force simp: Until_ltln)
+          subgoal 
+            using flatten_sigma_1_sf_subset * by (force simp: Until_ltln)
+          done
+  
+        thus ?thesis
+          by blast
+      next
+        case (Release_ltln \<psi>\<^sub>1 \<psi>\<^sub>2)
+        have *: "sf \<psi>\<^sub>1 \<subseteq> X" "sf \<psi>\<^sub>2 \<subseteq> X"
+          by (rule sf_subset_insert[OF sf_in_X, unfolded Release_ltln]; simp)+
+  
+        have "(sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2)) \<union> {\<psi>[M]\<^sub>\<Sigma>\<^sub>2, G\<^sub>n \<psi>\<^sub>2[M]\<^sub>\<Pi>\<^sub>1} \<union> sf (\<psi>\<^sub>2[M]\<^sub>\<Pi>\<^sub>1)"
+          and "(sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}"
+          and "(sf (\<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)) \<union> {\<psi>[N]\<^sub>\<Sigma>\<^sub>1}"
+          subgoal
+            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: Release_ltln)
+          subgoal
+            using flatten_pi_1_sf_subset[of _ M] * by (force simp: Release_ltln)
+          subgoal 
+            using flatten_sigma_1_sf_subset * by (force simp: Release_ltln)
+          done
+  
+        moreover 
+        have "sf (\<psi>\<^sub>2[M]\<^sub>\<Pi>\<^sub>1) \<subseteq> (\<Union>\<phi>\<in>X. sf \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}" 
+          using \<open>(sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}\<close> 
+          by (auto simp: Release_ltln)
+          
+        ultimately
+        show ?thesis
+          by (simp add: Release_ltln) blast 
+      next
+        case (WeakUntil_ltln \<psi>\<^sub>1 \<psi>\<^sub>2)
+        have *: "sf \<psi>\<^sub>1 \<subseteq> X" "sf \<psi>\<^sub>2 \<subseteq> X"
+          by (rule sf_subset_insert[OF sf_in_X, unfolded WeakUntil_ltln]; simp)+
+  
+        have "(sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2)) \<union> {\<psi>[M]\<^sub>\<Sigma>\<^sub>2, G\<^sub>n \<psi>\<^sub>1[M]\<^sub>\<Pi>\<^sub>1} \<union> sf (\<psi>\<^sub>1[M]\<^sub>\<Pi>\<^sub>1)"
+          and "(sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}"
+          and "(sf (\<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)) \<union> {\<psi>[N]\<^sub>\<Sigma>\<^sub>1}"
+          subgoal
+            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: WeakUntil_ltln)
+          subgoal
+            using flatten_pi_1_sf_subset[of _ M] * by (force simp: WeakUntil_ltln)
+          subgoal 
+            using flatten_sigma_1_sf_subset * by (force simp: WeakUntil_ltln)
+          done
+  
+        moreover 
+        have "sf (\<psi>\<^sub>1[M]\<^sub>\<Pi>\<^sub>1) \<subseteq> (\<Union>\<phi>\<in>X. sf \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}" 
+          using \<open>(sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}\<close> 
+          by (auto simp: WeakUntil_ltln)
+          
+        ultimately
+        show ?thesis
+          by (simp add: WeakUntil_ltln) blast 
+      next 
+        case (StrongRelease_ltln \<psi>\<^sub>1 \<psi>\<^sub>2)
+        have *: "sf \<psi>\<^sub>1 \<subseteq> X" "sf \<psi>\<^sub>2 \<subseteq> X"
+          by (rule sf_subset_insert[OF sf_in_X, unfolded StrongRelease_ltln]; simp)+
+          
+        hence "(sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>2)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2)) \<union> {\<psi>[M]\<^sub>\<Sigma>\<^sub>2}"
+          and "(sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<union> {\<psi>[M]\<^sub>\<Pi>\<^sub>1}"
+          and "(sf (\<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<subseteq> (\<Union>\<phi> \<in> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)) \<union> {\<psi>[N]\<^sub>\<Sigma>\<^sub>1}"
+          subgoal
+            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: StrongRelease_ltln)
+          subgoal
+            using flatten_pi_1_sf_subset[of _ M] * by (force simp: StrongRelease_ltln)
+          subgoal 
+            using flatten_sigma_1_sf_subset * by (force simp: StrongRelease_ltln)
+          done
+          
+        thus ?thesis 
+          by blast
+      qed auto
+
+      hence "card ?lower1 \<le> card (\<Union>\<phi> \<in> X. sf (\<phi>[N]\<^sub>\<Sigma>\<^sub>1)) + 1"
+        and "card ?lower2 \<le> card (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) + 1"
+        and "card ?lower3 \<le> card (\<Union>\<phi> \<in> X. sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) + 3" 
+        using card_subset_split_rule[OF finite_upper1, of ?lower1] 
+        using card_subset_split_rule[OF finite_upper2, of ?lower2]
+        using card_subset_split_rule[OF finite_upper3, of ?lower3]
+        using card_leq_3 by simp+
+  
+      moreover
+      have "card (insert \<psi> X) = card X + 1"
+        using \<open>\<psi> \<notin> X\<close> \<open>finite X\<close> by simp
+      ultimately
+      have ?case
+        by linarith
+    }
+  moreover
+  have "\<psi> \<in> X \<Longrightarrow> ?case"
+    using 2 by (simp add: insert_absorb)
+  ultimately
+  show ?case 
+    by meson
+qed simp
+      
+theorem flatten_card_sf: 
+  "card (\<Union>\<psi> \<in> sf \<phi>. sf (\<psi>[M]\<^sub>\<Sigma>\<^sub>1)) \<le> card (sf \<phi>)" (is "?t1") 
+  "card (\<Union>\<psi> \<in> sf \<phi>. sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<le> card (sf \<phi>)" (is "?t2")
+  "card (sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2) \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<le> 3 * card (sf \<phi>)" (is "?t3")
+proof -
+  have "card (\<Union>\<psi> \<in> sf \<phi>. sf \<psi>[M]\<^sub>\<Sigma>\<^sub>2 \<union> sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<le> 3 * card (sf \<phi>)"
+    using flatten_card_sf_induct[OF sf_finite sf_sf_subset] by auto
+  moreover
+  have "card (sf \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<union> sf (\<phi>[M]\<^sub>\<Pi>\<^sub>1)) \<le> card (\<Union>\<psi> \<in> sf \<phi>. sf \<psi>[M]\<^sub>\<Sigma>\<^sub>2 \<union> sf (\<psi>[M]\<^sub>\<Pi>\<^sub>1))"
+    using card_mono[OF _ sf_set1] sf_finite by blast
+  ultimately
+  show ?t1 ?t2 ?t3
+    using flatten_card_sf_induct[OF sf_finite sf_sf_subset] by auto
+qed
+
+corollary flatten_sigma_2_card_sf: 
+  "card (sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2)) \<le> 3 * (card (sf \<phi>))"
+  by (metis sf_finite order.trans[OF _ flatten_card_sf(3), of "card (sf (\<phi>[M]\<^sub>\<Sigma>\<^sub>2))", OF card_mono] finite_UnI Un_upper1)
+
+end
\ No newline at end of file
diff --git a/thys/LTL_Normal_Form/ROOT b/thys/LTL_Normal_Form/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/LTL_Normal_Form/ROOT
@@ -0,0 +1,15 @@
+chapter AFP
+
+session LTL_Normal_Form (AFP) = "LTL" +
+  options [timeout = 600]
+  sessions
+    LTL_Master_Theorem
+  theories
+    "Normal_Form"
+    "Normal_Form_Complexity"
+    "Normal_Form_Code_Export"
+  document_files
+    "root.tex"
+    "root.bib"
+  export_files (in ".") [1]
+    "LTL_Normal_Form.Normal_Form_Code_Export:**"
diff --git a/thys/LTL_Normal_Form/document/root.bib b/thys/LTL_Normal_Form/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/LTL_Normal_Form/document/root.bib
@@ -0,0 +1,91 @@
+@inproceedings{DBLP:conf/lop/LichtensteinPZ85,
+  author    = {Orna Lichtenstein and
+               Amir Pnueli and
+               Lenore D. Zuck},
+  editor    = {Rohit Parikh},
+  title     = {The Glory of the Past},
+  booktitle = {Logics of Programs, Conference, Brooklyn College, New York, NY, USA,
+               June 17-19, 1985, Proceedings},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {193},
+  pages     = {196--218},
+  publisher = {Springer},
+  year      = {1985},
+  _url       = {https://doi.org/10.1007/3-540-15648-8\_16},
+  doi       = {10.1007/3-540-15648-8_16},
+  timestamp = {Tue, 14 May 2019 10:00:52 +0200},
+  biburl    = {https://dblp.org/rec/bib/conf/lop/LichtensteinPZ85},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@phdthesis{XXXX:phd/Zuck86,
+  author    = {Lenore D. Zuck},
+  title     = {{Past Temporal Logic}},
+  school    = {The Weizmann Institute of Science, Israel},
+  year      = {1986},
+  month     = aug
+}
+
+@inproceedings{DBLP:conf/icalp/ChangMP92,
+  author    = {Edward Y. Chang and
+               Zohar Manna and
+               Amir Pnueli},
+  editor    = {Werner Kuich},
+  title     = {Characterization of Temporal Property Classes},
+  booktitle = {Automata, Languages and Programming, 19th International Colloquium,
+               ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {623},
+  pages     = {474--486},
+  publisher = {Springer},
+  year      = {1992},
+  _url       = {https://doi.org/10.1007/3-540-55719-9\_97},
+  doi       = {10.1007/3-540-55719-9_97},
+  timestamp = {Tue, 14 May 2019 10:00:44 +0200},
+  biburl    = {https://dblp.org/rec/bib/conf/icalp/ChangMP92},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/mfcs/CernaP03,
+  author    = {Ivana {\v{C}}ern{\'{a}} and
+               Radek Pel{\'{a}}nek},
+  editor    = {Branislav Rovan and
+               Peter Vojt{\'{a}}s},
+  title     = {Relating Hierarchy of Temporal Properties to Model Checking},
+  booktitle = {Mathematical Foundations of Computer Science 2003, 28th International
+               Symposium, {MFCS} 2003, Bratislava, Slovakia, August 25-29, 2003,
+               Proceedings},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {2747},
+  pages     = {318--327},
+  publisher = {Springer},
+  year      = {2003},
+  _url       = {https://doi.org/10.1007/978-3-540-45138-9\_26},
+  doi       = {10.1007/978-3-540-45138-9_26},
+  timestamp = {Tue, 14 May 2019 10:00:37 +0200},
+  biburl    = {https://dblp.org/rec/bib/conf/mfcs/CernaP03},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{XXXX:conf/lics/SickertE20,
+  author    = {Salomon Sickert and Javier Esparza},
+  title     = {An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata},
+  booktitle = {Proceedings of the 35th Annual {ACM/IEEE} Symposium on Logic in Computer
+               Science, {LICS} 2020, Saarbr\"ucken, Germany, July 8-11, 2020},
+  publisher = {{ACM}},
+  year      = {2020},
+  _url       = {https://doi.org/10.1145/3373718.3394743},
+  doi       = {10.1145/3373718.3394743}
+}
+
+@article{DBLP:journals/corr/abs-2005-00472,
+  author    = {Salomon Sickert and
+               Javier Esparza},
+  title     = {An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata},
+  journal   = {CoRR},
+  volume    = {abs/2005.00472},
+  year      = {2020},
+  _url       = {http://arxiv.org/abs/2005.00472},
+  archivePrefix = {arXiv},
+  eprint    = {2005.00472}
+}
diff --git a/thys/LTL_Normal_Form/document/root.tex b/thys/LTL_Normal_Form/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/LTL_Normal_Form/document/root.tex
@@ -0,0 +1,108 @@
+\documentclass[11pt,a4paper]{article}
+
+\usepackage[english]{babel}
+\usepackage[utf8]{inputenc}
+
+\usepackage{mathtools,amsthm,amssymb}
+\usepackage{isabelle,isabellesym}
+
+\usepackage[T1]{fontenc}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+\renewcommand{\isastyle}{\isastyleminor}
+
+% LTL Operators
+
+\newcommand{\true}{{\ensuremath{\mathbf{t\hspace{-0.5pt}t}}}}
+\newcommand{\false}{{\ensuremath{\mathbf{ff}}}}
+\newcommand{\F}{{\ensuremath{\mathbf{F}}}}
+\newcommand{\G}{{\ensuremath{\mathbf{G}}}}
+\newcommand{\X}{{\ensuremath{\mathbf{X}}}}
+\newcommand{\U}{{\ensuremath{\mathbf{U}}}}
+\newcommand{\W}{{\ensuremath{\mathbf{W}}}}
+\newcommand{\M}{{\ensuremath{\mathbf{M}}}}
+\newcommand{\R}{{\ensuremath{\mathbf{R}}}}
+
+% LTL Subformulas
+
+\newcommand{\subf}{\textit{sf}\,}
+
+\newcommand{\sfmu}{{\ensuremath{\mathbb{\mu}}}}
+\newcommand{\sfnu}{{\ensuremath{\mathbb{\nu}}}}
+\newcommand{\setmu}{\ensuremath{M}}
+\newcommand{\setnu}{\ensuremath{N}}
+\newcommand{\setF}{\ensuremath{\mathcal{F}}}
+\newcommand{\setG}{\ensuremath{\mathcal{G}}}
+\newcommand{\setFG}{\ensuremath{\mathcal{F\hspace{-0.1em}G}}}
+\newcommand{\setGF}{\ensuremath{\mathcal{G\hspace{-0.1em}F}\!}}
+
+% LTL Functions
+
+\newcommand{\evalnu}[2]{{#1[#2]^\Pi_1}}
+\newcommand{\evalmu}[2]{{#1[#2]^\Sigma_1}}
+\newcommand{\flatten}[2]{{#1[#2]^\Sigma_2}}
+\newcommand{\flattentwo}[2]{{#1[#2]^\Pi_2}}
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{definition}[theorem]{Definition}
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{corollary}[theorem]{Corollary}
+\newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{example}[theorem]{Example}
+\newtheorem{remark}[theorem]{Remark}
+
+\begin{document}
+
+\title{An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation}
+\author{Salomon Sickert}
+
+\maketitle
+
+\begin{abstract}
+In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \G\F \varphi_i \vee \F\G \psi_i $, where $\varphi_i$ and $\psi_i$ contain only past operators \cite{DBLP:conf/lop/LichtensteinPZ85,XXXX:phd/Zuck86}. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL \cite{DBLP:conf/icalp/ChangMP92}. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present an executable formalisation of a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up.
+\end{abstract}
+
+\tableofcontents
+
+\section{Overview}
+
+This document contains the formalisation of the central results appearing in \cite[Sections 4-6]{XXXX:conf/lics/SickertE20}. We refer the interested reader to \cite{XXXX:conf/lics/SickertE20} or to the extended version \cite{DBLP:journals/corr/abs-2005-00472} for an introduction to the topic, related work, intuitive explanations of the proofs, and an application of the normalisation procedure, namely, a translation from LTL to deterministic automata.
+
+The central result of this document is the following theorem: 
+
+\begin{theorem}
+Let $\varphi$ be an LTL formula and let $\Delta_2$, $\Sigma_1$, $\Sigma_2$, and $\Pi_1$ be the classes of LTL formulas from Definition \ref{def:future_hierarchy}. Then $\varphi$ is equivalent to the following formula from the class $\Delta_2$:
+\[
+\bigvee_{\substack{\setmu \subseteq \sfmu(\varphi)\\\setnu \subseteq \sfnu(\varphi)}} \left( \flatten{\varphi}{\setmu} \wedge \bigwedge_{\psi \in \setmu} \G\F(\evalmu{\psi}{\setnu}) \wedge \bigwedge_{\psi \in \setnu} \F\G(\evalnu{\psi}{\setmu}) \right)
+\]
+\noindent where $\flatten{\psi}{\setmu}$, $\evalmu{\psi}{\setnu}$, and $\evalnu{\psi}{\setmu}$ are functions mapping $\psi$ to a formula from $\Sigma_2$, $\Sigma_1$, and $\Pi_1$, respectively.
+\end{theorem}
+
+\begin{definition}[Adapted from \cite{DBLP:conf/mfcs/CernaP03}]
+\label{def:future_hierarchy}
+We define the following classes of LTL formulas:
+\begin{itemize}
+	\item The class $\Sigma_0 = \Pi_0 = \Delta_0$ is the least set containing all atomic propositions and their negations, and is closed under the application of conjunction and disjunction.
+	\item The class $\Sigma_{i+1}$ is the least set containing $\Pi_i$ and is closed under the application of conjunction, disjunction, and the $\X$, $\U$, and $\M$ operators.
+	\item The class $\Pi_{i+1}$ is the least set containing $\Sigma_i$ and is closed under the application of conjunction, disjunction, and the $\X$, $\R$, and $\W$ operators.
+	\item The class $\Delta_{i+1}$ is the least set containing $\Sigma_{i+1}$ and $\Pi_{i+1}$ and is closed under the application of conjunction and disjunction.
+\end{itemize}
+\end{definition}
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+\bibliographystyle{plainurl}
+\bibliography{root}
+
+\end{document}
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,536 +1,537 @@
 ADS_Functor
 AODV
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 AutoFocus-Stream
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BNF_Operations
 Banach_Steinhaus
 Bell_Numbers_Spivey
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BNF_CC
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CYK
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Completeness
 Complete_Non_Orders
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Consensus_Refined
 Constructive_Cryptography
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 DFS_Framework
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 Discrete_Summation
 DiscretePricing
 DiskPaxos
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Example-Submission
 Factored_Transition_System_Bounding
 Farkas
 FFT
 FLP
 FOL-Fitting
 FOL_Harrison
 FOL_Seq_Calc1
 Falling_Factorial_Sum
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite_Automata_HF
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_SSA
 Formula_Derivatives
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interval_Arithmetic_Word32
 Iptables_Semantics
 Irrationality_J_Hancl
 Isabelle_C
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knot_Theory
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_to_DRA
 LTL_to_GBA
 LTL_Master_Theorem
+LTL_Normal_Form
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Lambda_Free_EPO
 Launchbury
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MFMC_Countable
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Of_Medians_Selection
 Menger
 Mersenne_Primes
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MiniML
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multirelations
 Multi_Party_Computation
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 Open_Induction
 OpSets
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PCF
 PLM
 Pell
 POPLmark-deBruijn
 PSemigroupsConvolution
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Perfect-Number-Thm
 Perron_Frobenius
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Poincare_Bendixson
 Poincare_Disc
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Projective_Geometry
 Program-Conflict-Analysis
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 QHLProver
 QR_Decomposition
 Quantales
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Randomised_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Regular-Sets
 Regular_Algebras
 Relation_Algebra
 Relational-Incorrectness-Logic
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Root_Balanced_Tree
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_OCL
 Saturation_Framework
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Timed_Automata
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Universal_Turing_Machine
 UPF
 UPF_Firewall
 UpDown_Scheme
 UTP
 Valuation
 VectorSpace
 VeriComp
 Verified-Prover
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 VolpanoSmith
 WHATandWHERE_Security
 WebAssembly
 Weight_Balanced_Trees
 Well_Quasi_Orders
 Winding_Number_Eval
 WOOT_Strong_Eventual_Consistency
 Word_Lib
 WorkerWrapper
 XML
 Zeta_Function
 Zeta_3_Irrational
 ZFC_in_HOL
 pGCL