diff --git a/thys/Correctness_Algebras/Approximation.thy b/thys/Correctness_Algebras/Approximation.thy
--- a/thys/Correctness_Algebras/Approximation.thy
+++ b/thys/Correctness_Algebras/Approximation.thy
@@ -1,114 +1,116 @@
 (* Title:      Approximation
    Author:     Walter Guttmann
    Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
 *)
 
 section \<open>Approximation\<close>
 
 theory Approximation
 
 imports Stone_Kleene_Relation_Algebras.Iterings
 
 begin
 
+nitpick_params [timeout = 600]
+
 class apx =
   fixes apx :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
 
 class apx_order = apx +
   assumes apx_reflexive: "x \<sqsubseteq> x"
   assumes apx_antisymmetric: "x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> x = y"
   assumes apx_transitive: "x \<sqsubseteq> y \<and> y \<sqsubseteq> z \<longrightarrow> x \<sqsubseteq> z"
 
 sublocale apx_order < apx: order where less_eq = apx and less = "\<lambda>x y . x \<sqsubseteq> y \<and> \<not> y \<sqsubseteq> x"
   apply unfold_locales
   apply simp
   apply (rule apx_reflexive)
   using apx_transitive apply blast
   by (simp add: apx_antisymmetric)
 
 context apx_order
 begin
 
 abbreviation the_apx_least_fixpoint    :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("\<kappa> _" [201] 200)  where "\<kappa>  f \<equiv> apx.the_least_fixpoint f"
 abbreviation the_apx_least_prefixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("p\<kappa> _" [201] 200) where "p\<kappa> f \<equiv> apx.the_least_prefixpoint f"
 
 definition is_apx_meet  :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"          where "is_apx_meet x y z \<equiv> z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<and> (\<forall>w . w \<sqsubseteq> x \<and> w \<sqsubseteq> y \<longrightarrow> w \<sqsubseteq> z)"
 definition has_apx_meet :: "'a \<Rightarrow> 'a \<Rightarrow> bool"                where "has_apx_meet x y \<equiv> \<exists>z . is_apx_meet x y z"
 definition the_apx_meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<triangle>" 66) where "x \<triangle> y \<equiv> THE z . is_apx_meet x y z"
 
 lemma apx_meet_unique:
   "has_apx_meet x y \<Longrightarrow> \<exists>!z . is_apx_meet x y z"
   by (meson apx_antisymmetric has_apx_meet_def is_apx_meet_def)
 
 lemma apx_meet:
   assumes "has_apx_meet x y"
     shows "is_apx_meet x y (x \<triangle> y)"
 proof -
   have "is_apx_meet x y (THE z . is_apx_meet x y z)"
     by (metis apx_meet_unique assms theI)
   thus ?thesis
     by (simp add: the_apx_meet_def)
 qed
 
 lemma apx_greatest_lower_bound:
   "has_apx_meet x y \<Longrightarrow> (w \<sqsubseteq> x \<and> w \<sqsubseteq> y \<longleftrightarrow> w \<sqsubseteq> x \<triangle> y)"
   by (meson apx_meet apx_transitive is_apx_meet_def)
 
 lemma apx_meet_same:
   "is_apx_meet x y z \<Longrightarrow> z = x \<triangle> y"
   using apx_meet apx_meet_unique has_apx_meet_def by blast
 
 lemma apx_meet_char:
   "is_apx_meet x y z \<longleftrightarrow> has_apx_meet x y \<and> z = x \<triangle> y"
   using apx_meet_same has_apx_meet_def by auto
 
 end
 
 class apx_biorder = apx_order + order
 begin
 
 lemma mu_below_kappa:
   "has_least_fixpoint f \<Longrightarrow> apx.has_least_fixpoint f \<Longrightarrow> \<mu> f \<le> \<kappa> f"
   using apx.mu_unfold is_least_fixpoint_def least_fixpoint by auto
 
 lemma kappa_below_nu:
   "has_greatest_fixpoint f \<Longrightarrow> apx.has_least_fixpoint f \<Longrightarrow> \<kappa> f \<le> \<nu> f"
   by (meson apx.mu_unfold greatest_fixpoint is_greatest_fixpoint_def)
 
 lemma kappa_apx_below_mu:
   "has_least_fixpoint f \<Longrightarrow> apx.has_least_fixpoint f \<Longrightarrow> \<kappa> f \<sqsubseteq> \<mu> f"
   using apx.is_least_fixpoint_def apx.least_fixpoint mu_unfold by auto
 
 lemma kappa_apx_below_nu:
   "has_greatest_fixpoint f \<Longrightarrow> apx.has_least_fixpoint f \<Longrightarrow> \<kappa> f \<sqsubseteq> \<nu> f"
   by (metis apx.is_least_fixpoint_def apx.least_fixpoint nu_unfold)
 
 end
 
 class apx_semiring = apx_biorder + idempotent_left_semiring + L +
   assumes apx_L_least: "L \<sqsubseteq> x"
   assumes sup_apx_left_isotone: "x \<sqsubseteq> y \<longrightarrow> x \<squnion> z \<sqsubseteq> y \<squnion> z"
   assumes mult_apx_left_isotone: "x \<sqsubseteq> y \<longrightarrow> x * z \<sqsubseteq> y * z"
   assumes mult_apx_right_isotone: "x \<sqsubseteq> y \<longrightarrow> z * x \<sqsubseteq> z * y"
 begin
 
 lemma sup_apx_right_isotone:
   "x \<sqsubseteq> y \<Longrightarrow> z \<squnion> x \<sqsubseteq> z \<squnion> y"
   by (simp add: sup_apx_left_isotone sup_commute)
 
 lemma sup_apx_isotone:
   "w \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> w \<squnion> x \<sqsubseteq> y \<squnion> z"
   by (meson apx_transitive sup_apx_left_isotone sup_apx_right_isotone)
 
 lemma mult_apx_isotone:
   "w \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> w * x \<sqsubseteq> y * z"
   by (meson apx_transitive mult_apx_left_isotone mult_apx_right_isotone)
 
 lemma affine_apx_isotone:
   "apx.isotone (\<lambda>x . y * x \<squnion> z)"
   by (simp add: apx.isotone_def mult_apx_right_isotone sup_apx_left_isotone)
 
 end
 
 end
 
diff --git a/thys/Correctness_Algebras/Base.thy b/thys/Correctness_Algebras/Base.thy
--- a/thys/Correctness_Algebras/Base.thy
+++ b/thys/Correctness_Algebras/Base.thy
@@ -1,228 +1,230 @@
 (* Title:      Base
    Author:     Walter Guttmann
    Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
 *)
 
 section \<open>Base\<close>
 
 theory Base
 
 imports Stone_Relation_Algebras.Semirings
 
 begin
 
+nitpick_params [timeout = 600]
+
 class while =
   fixes while :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<star>" 59)
 
 class n =
   fixes n :: "'a \<Rightarrow> 'a"
 
 class diamond =
   fixes diamond :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("| _ > _" [50,90] 95)
 
 class box =
   fixes box :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("| _ ] _" [50,90] 95)
 
 context ord
 begin
 
 definition ascending_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
   where "ascending_chain f \<equiv> \<forall>n . f n \<le> f (Suc n)"
 
 definition descending_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
   where "descending_chain f \<equiv> \<forall>n . f (Suc n) \<le> f n"
 
 definition directed :: "'a set \<Rightarrow> bool"
   where "directed X \<equiv> X \<noteq> {} \<and> (\<forall>x\<in>X . \<forall>y\<in>X . \<exists>z\<in>X . x \<le> z \<and> y \<le> z)"
 
 definition co_directed :: "'a set \<Rightarrow> bool"
   where "co_directed X \<equiv> X \<noteq> {} \<and> (\<forall>x\<in>X . \<forall>y\<in>X . \<exists>z\<in>X . z \<le> x \<and> z \<le> y)"
 
 definition chain :: "'a set \<Rightarrow> bool"
   where "chain X \<equiv> \<forall>x\<in>X . \<forall>y\<in>X . x \<le> y \<or> y \<le> x"
 
 end
 
 context order
 begin
 
 lemma ascending_chain_k:
   "ascending_chain f \<Longrightarrow> f m \<le> f (m + k)"
   apply (induct k)
   apply simp
   using le_add1 lift_Suc_mono_le ord.ascending_chain_def by blast
 
 lemma ascending_chain_isotone:
   "ascending_chain f \<Longrightarrow> m \<le> k \<Longrightarrow> f m \<le> f k"
   using lift_Suc_mono_le ord.ascending_chain_def by blast
 
 lemma ascending_chain_comparable:
   "ascending_chain f \<Longrightarrow> f k \<le> f m \<or> f m \<le> f k"
   by (meson ascending_chain_isotone linear)
 
 lemma ascending_chain_chain:
   "ascending_chain f \<Longrightarrow> chain (range f)"
   by (simp add: ascending_chain_comparable chain_def)
 
 lemma chain_directed:
   "X \<noteq> {} \<Longrightarrow> chain X \<Longrightarrow> directed X"
   by (metis chain_def directed_def)
 
 lemma ascending_chain_directed:
   "ascending_chain f \<Longrightarrow> directed (range f)"
   by (simp add: ascending_chain_chain chain_directed)
 
 lemma descending_chain_k:
   "descending_chain f \<Longrightarrow> f (m + k) \<le> f m"
   apply (induct k)
   apply simp
   using le_add1 lift_Suc_antimono_le ord.descending_chain_def by blast
 
 lemma descending_chain_antitone:
   "descending_chain f \<Longrightarrow> m \<le> k \<Longrightarrow> f k \<le> f m"
   using descending_chain_def lift_Suc_antimono_le by blast
 
 lemma descending_chain_comparable:
   "descending_chain f \<Longrightarrow> f k \<le> f m \<or> f m \<le> f k"
   by (meson descending_chain_antitone nat_le_linear)
 
 lemma descending_chain_chain:
   "descending_chain f \<Longrightarrow> chain (range f)"
   by (simp add: descending_chain_comparable chain_def)
 
 lemma chain_co_directed:
   "X \<noteq> {} \<Longrightarrow> chain X \<Longrightarrow> co_directed X"
   by (metis chain_def co_directed_def)
 
 lemma descending_chain_codirected:
   "descending_chain f \<Longrightarrow> co_directed (range f)"
   by (simp add: chain_co_directed descending_chain_chain)
 
 end
 
 context semilattice_sup
 begin
 
 lemma ascending_chain_left_sup:
   "ascending_chain f \<Longrightarrow> ascending_chain (\<lambda>n . x \<squnion> f n)"
   using ascending_chain_def sup_right_isotone by blast
 
 lemma ascending_chain_right_sup:
   "ascending_chain f \<Longrightarrow> ascending_chain (\<lambda>n . f n \<squnion> x)"
   using ascending_chain_def sup_left_isotone by auto
 
 lemma descending_chain_left_add:
   "descending_chain f \<Longrightarrow> descending_chain (\<lambda>n . x \<squnion> f n)"
   using descending_chain_def sup_right_isotone by blast
 
 lemma descending_chain_right_add:
   "descending_chain f \<Longrightarrow> descending_chain (\<lambda>n . f n \<squnion> x)"
   using descending_chain_def sup_left_isotone by auto
 
 primrec pSum0 :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
   where "pSum0 f 0 = f 0"
       | "pSum0 f (Suc m) = pSum0 f m \<squnion> f m"
 
 lemma pSum0_below:
  "\<forall>i . f i \<le> x \<Longrightarrow> pSum0 f m \<le> x"
   apply (induct m)
   by auto
 
 end
 
 context non_associative_left_semiring
 begin
 
 lemma ascending_chain_left_mult:
   "ascending_chain f \<Longrightarrow> ascending_chain (\<lambda>n . x * f n)"
   by (simp add: mult_right_isotone ord.ascending_chain_def)
 
 lemma ascending_chain_right_mult:
   "ascending_chain f \<Longrightarrow> ascending_chain (\<lambda>n . f n * x)"
   by (simp add: mult_left_isotone ord.ascending_chain_def)
 
 lemma descending_chain_left_mult:
   "descending_chain f \<Longrightarrow> descending_chain (\<lambda>n . x * f n)"
   by (simp add: descending_chain_def mult_right_isotone)
 
 lemma descending_chain_right_mult:
   "descending_chain f \<Longrightarrow> descending_chain (\<lambda>n . f n * x)"
   by (simp add: descending_chain_def mult_left_isotone)
 
 end
 
 context complete_lattice
 begin
 
 lemma sup_Sup:
   "A \<noteq> {} \<Longrightarrow> sup x (Sup A) = Sup ((sup x) ` A)"
   apply (rule order.antisym)
   apply (meson ex_in_conv imageI SUP_upper2 Sup_mono sup.boundedI sup_left_divisibility sup_right_divisibility)
   by (meson SUP_least Sup_upper sup_right_isotone)
 
 lemma sup_SUP:
   "Y \<noteq> {} \<Longrightarrow> sup x (SUP y\<in>Y . f y) = (SUP y\<in>Y. sup x (f y))"
   apply (subst sup_Sup)
   by (simp_all add: image_image)
 
 lemma inf_Inf:
   "A \<noteq> {} \<Longrightarrow> inf x (Inf A) = Inf ((inf x) ` A)"
   apply (rule order.antisym)
   apply (meson INF_greatest Inf_lower inf.sup_right_isotone)
   by (simp add: INF_inf_const1)
 
 lemma inf_INF:
   "Y \<noteq> {} \<Longrightarrow> inf x (INF y\<in>Y . f y) = (INF y\<in>Y. inf x (f y))"
   apply (subst inf_Inf)
   by (simp_all add: image_image)
 
 lemma SUP_image_id[simp]:
   "(SUP x\<in>f`A . x) = (SUP x\<in>A . f x)"
   by simp
 
 lemma INF_image_id[simp]:
   "(INF x\<in>f`A . x) = (INF x\<in>A . f x)"
   by simp
 
 end
 
 lemma image_Collect_2:
   "f ` { g x | x . P x } = { f (g x) | x . P x }"
   by auto
 
 text \<open>The following instantiation and four lemmas are from Jose Divason Mallagaray.\<close>
 
 instantiation "fun" :: (type, type) power
 begin
 
 definition one_fun :: "'a \<Rightarrow> 'a"
   where one_fun_def: "one_fun \<equiv> id"
 
 definition times_fun :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
   where times_fun_def: "times_fun \<equiv> comp"
 
 instance
   by intro_classes
 
 end
 
 lemma id_power:
   "id^m = id"
   apply (induct m)
   apply (simp add: one_fun_def)
   by (simp add: times_fun_def)
 
 lemma power_zero_id:
   "f^0 = id"
   by (simp add: one_fun_def)
 
 lemma power_succ_unfold:
   "f^Suc m = f \<circ> f^m"
   by (simp add: times_fun_def)
 
 lemma power_succ_unfold_ext:
   "(f^Suc m) x = f ((f^m) x)"
   by (simp add: times_fun_def)
 
 end
 
diff --git a/thys/Correctness_Algebras/Lattice_Ordered_Semirings.thy b/thys/Correctness_Algebras/Lattice_Ordered_Semirings.thy
--- a/thys/Correctness_Algebras/Lattice_Ordered_Semirings.thy
+++ b/thys/Correctness_Algebras/Lattice_Ordered_Semirings.thy
@@ -1,902 +1,904 @@
 (* Title:      Lattice-Ordered Semirings
    Author:     Walter Guttmann
    Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
 *)
 
 section \<open>Lattice-Ordered Semirings\<close>
 
 theory Lattice_Ordered_Semirings
 
 imports Stone_Relation_Algebras.Semirings
 
 begin
 
+nitpick_params [timeout = 600]
+
 text \<open>Many results in this theory are taken from a joint paper with Rudolf Berghammer.\<close>
 
 text \<open>M0-algebra\<close>
 
 class lattice_ordered_pre_left_semiring = pre_left_semiring + bounded_distrib_lattice
 begin
 
 subclass bounded_pre_left_semiring
   apply unfold_locales
   by simp
 
 lemma top_mult_right_one:
   "x * top = x * top * 1"
   by (metis order.antisym mult_sub_right_one mult_sup_associative_one surjective_one_closed)
 
 lemma mult_left_sub_dist_inf_left:
   "x * (y \<sqinter> z) \<le> x * y"
   by (simp add: mult_right_isotone)
 
 lemma mult_left_sub_dist_inf_right:
   "x * (y \<sqinter> z) \<le> x * z"
   by (simp add: mult_right_isotone)
 
 lemma mult_right_sub_dist_inf_left:
   "(x \<sqinter> y) * z \<le> x * z"
   by (simp add: mult_left_isotone)
 
 lemma mult_right_sub_dist_inf_right:
   "(x \<sqinter> y) * z \<le> y * z"
   by (simp add: mult_left_isotone)
 
 lemma mult_right_sub_dist_inf:
   "(x \<sqinter> y) * z \<le> x * z \<sqinter> y * z"
   by (simp add: mult_right_sub_dist_inf_left mult_right_sub_dist_inf_right)
 
 text \<open>Figure 1: fundamental properties\<close>
 
 definition co_total          :: "'a \<Rightarrow> bool" where "co_total x \<equiv> x * bot = bot"
 definition up_closed         :: "'a \<Rightarrow> bool" where "up_closed x \<equiv> x * 1 = x"
 definition sup_distributive  :: "'a \<Rightarrow> bool" where "sup_distributive x \<equiv> (\<forall>y z . x * (y \<squnion> z) = x * y \<squnion> x * z)"
 definition inf_distributive  :: "'a \<Rightarrow> bool" where "inf_distributive x \<equiv> (\<forall>y z . x * (y \<sqinter> z) = x * y \<sqinter> x * z)"
 definition contact           :: "'a \<Rightarrow> bool" where "contact x \<equiv> x * x \<squnion> 1 = x"
 definition kernel            :: "'a \<Rightarrow> bool" where "kernel x \<equiv> x * x \<sqinter> 1 = x * 1"
 definition sup_dist_contact  :: "'a \<Rightarrow> bool" where "sup_dist_contact x \<equiv> sup_distributive x \<and> contact x"
 definition inf_dist_kernel   :: "'a \<Rightarrow> bool" where "inf_dist_kernel x \<equiv> inf_distributive x \<and> kernel x"
 definition test              :: "'a \<Rightarrow> bool" where "test x \<equiv> x * top \<sqinter> 1 = x"
 definition co_test           :: "'a \<Rightarrow> bool" where "co_test x \<equiv> x * bot \<squnion> 1 = x"
 definition co_vector         :: "'a \<Rightarrow> bool" where "co_vector x \<equiv> x * bot = x"
 
 text \<open>AAMP Theorem 6 / Figure 2: relations between properties\<close>
 
 lemma reflexive_total:
   "reflexive x \<Longrightarrow> total x"
   using sup_left_divisibility total_sup_closed by force
 
 lemma reflexive_dense:
   "reflexive x \<Longrightarrow> dense_rel x"
   using mult_left_isotone by fastforce
 
 lemma reflexive_transitive_up_closed:
   "reflexive x \<Longrightarrow> transitive x \<Longrightarrow> up_closed x"
   by (metis antisym_conv mult_isotone mult_sub_right_one reflexive_dense up_closed_def)
 
 lemma coreflexive_co_total:
   "coreflexive x \<Longrightarrow> co_total x"
   by (metis co_total_def order.eq_iff mult_left_isotone mult_left_one bot_least)
 
 lemma coreflexive_transitive:
   "coreflexive x \<Longrightarrow> transitive x"
   by (simp add: coreflexive_transitive)
 
 lemma idempotent_transitive_dense:
   "idempotent x \<longleftrightarrow> transitive x \<and> dense_rel x"
   by (simp add: order.eq_iff)
 
 lemma contact_reflexive:
   "contact x \<Longrightarrow> reflexive x"
   using contact_def sup_right_divisibility by auto
 
 lemma contact_transitive:
   "contact x \<Longrightarrow> transitive x"
   using contact_def sup_left_divisibility by blast
 
 lemma contact_dense:
   "contact x \<Longrightarrow> dense_rel x"
   by (simp add: contact_reflexive reflexive_dense)
 
 lemma contact_idempotent:
   "contact x \<Longrightarrow> idempotent x"
   by (simp add: contact_dense contact_transitive idempotent_transitive_dense)
 
 lemma contact_up_closed:
   "contact x \<Longrightarrow> up_closed x"
   by (simp add: contact_reflexive contact_transitive reflexive_transitive_up_closed)
 
 lemma contact_reflexive_idempotent_up_closed:
   "contact x \<longleftrightarrow> reflexive x \<and> idempotent x \<and> up_closed x"
   by (metis contact_def contact_idempotent contact_reflexive contact_up_closed sup_absorb2 sup_monoid.add_commute)
 
 lemma kernel_coreflexive:
   "kernel x \<Longrightarrow> coreflexive x"
   by (metis kernel_def inf.boundedE mult_sub_right_one)
 
 lemma kernel_transitive:
   "kernel x \<Longrightarrow> transitive x"
   by (simp add: coreflexive_transitive kernel_coreflexive)
 
 lemma kernel_dense:
   "kernel x \<Longrightarrow> dense_rel x"
   by (metis kernel_def inf.boundedE mult_sub_right_one)
 
 lemma kernel_idempotent:
   "kernel x \<Longrightarrow> idempotent x"
   by (simp add: idempotent_transitive_dense kernel_dense kernel_transitive)
 
 lemma kernel_up_closed:
   "kernel x \<Longrightarrow> up_closed x"
   by (metis kernel_coreflexive kernel_def kernel_idempotent inf.absorb1 up_closed_def)
 
 lemma kernel_coreflexive_idempotent_up_closed:
   "kernel x \<longleftrightarrow> coreflexive x \<and> idempotent x \<and> up_closed x"
   by (metis kernel_coreflexive kernel_def kernel_idempotent inf.absorb1 up_closed_def)
 
 lemma test_coreflexive:
   "test x \<Longrightarrow> coreflexive x"
   using inf.sup_right_divisibility test_def by blast
 
 lemma test_up_closed:
   "test x \<Longrightarrow> up_closed x"
   by (metis order.eq_iff mult_left_one mult_sub_right_one mult_right_sub_dist_inf test_def top_mult_right_one up_closed_def)
 
 lemma co_test_reflexive:
   "co_test x \<Longrightarrow> reflexive x"
   using co_test_def sup_right_divisibility by blast
 
 lemma co_test_transitive:
   "co_test x \<Longrightarrow> transitive x"
   by (smt co_test_def sup_assoc le_iff_sup mult_left_one mult_left_zero mult_right_dist_sup mult_semi_associative)
 
 lemma co_test_idempotent:
   "co_test x \<Longrightarrow> idempotent x"
   by (simp add: co_test_reflexive co_test_transitive idempotent_transitive_dense reflexive_dense)
 
 lemma co_test_up_closed:
   "co_test x \<Longrightarrow> up_closed x"
   by (simp add: co_test_reflexive co_test_transitive reflexive_transitive_up_closed)
 
 lemma co_test_contact:
   "co_test x \<Longrightarrow> contact x"
   by (simp add: co_test_idempotent co_test_reflexive co_test_up_closed contact_reflexive_idempotent_up_closed)
 
 lemma vector_transitive:
   "vector x \<Longrightarrow> transitive x"
   by (metis mult_right_isotone top.extremum)
 
 lemma vector_up_closed:
   "vector x \<Longrightarrow> up_closed x"
   by (metis top_mult_right_one up_closed_def)
 
 text \<open>AAMP Theorem 10 / Figure 3: closure properties\<close>
 
 text \<open>total\<close>
 
 lemma one_total:
   "total 1"
   by simp
 
 lemma top_total:
   "total top"
   by simp
 
 lemma sup_total:
   "total x \<Longrightarrow> total y \<Longrightarrow> total (x \<squnion> y)"
   by (simp add: total_sup_closed)
 
 text \<open>co-total\<close>
 
 lemma zero_co_total:
   "co_total bot"
   by (simp add: co_total_def)
 
 lemma one_co_total:
   "co_total 1"
   by (simp add: co_total_def)
 
 lemma sup_co_total:
   "co_total x \<Longrightarrow> co_total y \<Longrightarrow> co_total (x \<squnion> y)"
   by (simp add: co_total_def mult_right_dist_sup)
 
 lemma inf_co_total:
   "co_total x \<Longrightarrow> co_total y \<Longrightarrow> co_total (x \<sqinter> y)"
   by (metis co_total_def order.antisym bot_least mult_right_sub_dist_inf_right)
 
 lemma comp_co_total:
   "co_total x \<Longrightarrow> co_total y \<Longrightarrow> co_total (x * y)"
   by (metis co_total_def order.eq_iff mult_semi_associative bot_least)
 
 text \<open>sub-transitive\<close>
 
 lemma zero_transitive:
   "transitive bot"
   by (simp add: vector_transitive)
 
 lemma one_transitive:
   "transitive 1"
   by simp
 
 lemma top_transitive:
   "transitive top"
   by simp
 
 lemma inf_transitive:
   "transitive x \<Longrightarrow> transitive y \<Longrightarrow> transitive (x \<sqinter> y)"
   by (meson inf_mono order_trans mult_left_sub_dist_inf_left mult_left_sub_dist_inf_right mult_right_sub_dist_inf)
 
 text \<open>dense\<close>
 
 lemma zero_dense:
   "dense_rel bot"
   by simp
 
 lemma one_dense:
   "dense_rel 1"
   by simp
 
 lemma top_dense:
   "dense_rel top"
   by simp
 
 lemma sup_dense:
   assumes "dense_rel x"
       and "dense_rel y"
     shows "dense_rel (x \<squnion> y)"
 proof -
   have "x \<le> x * x \<and> y \<le> y * y"
     using assms by auto
   hence "x \<le> (x \<squnion> y) * (x \<squnion> y) \<and> y \<le> (x \<squnion> y) * (x \<squnion> y)"
     by (meson dense_sup_closed order_trans sup.cobounded1 sup.cobounded2)
   hence "x \<squnion> y \<le> (x \<squnion> y) * (x \<squnion> y)"
     by simp
   thus "dense_rel (x \<squnion> y)"
     by simp
 qed
 
 text \<open>reflexive\<close>
 
 lemma one_reflexive:
   "reflexive 1"
   by simp
 
 lemma top_reflexive:
   "reflexive top"
   by simp
 
 lemma sup_reflexive:
   "reflexive x \<Longrightarrow> reflexive y \<Longrightarrow> reflexive (x \<squnion> y)"
   by (simp add: reflexive_sup_closed)
 
 lemma inf_reflexive:
   "reflexive x \<Longrightarrow> reflexive y \<Longrightarrow> reflexive (x \<sqinter> y)"
   by simp
 
 lemma comp_reflexive:
   "reflexive x \<Longrightarrow> reflexive y \<Longrightarrow> reflexive (x * y)"
   using reflexive_mult_closed by auto
 
 text \<open>co-reflexive\<close>
 
 lemma zero_coreflexive:
   "coreflexive bot"
   by simp
 
 lemma one_coreflexive:
   "coreflexive 1"
   by simp
 
 lemma sup_coreflexive:
   "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> coreflexive (x \<squnion> y)"
   by simp
 
 lemma inf_coreflexive:
   "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> coreflexive (x \<sqinter> y)"
   by (simp add: le_infI1)
 
 lemma comp_coreflexive:
   "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> coreflexive (x * y)"
   by (simp add: coreflexive_mult_closed)
 
 text \<open>idempotent\<close>
 
 lemma zero_idempotent:
   "idempotent bot"
   by simp
 
 lemma one_idempotent:
   "idempotent 1"
   by simp
 
 lemma top_idempotent:
   "idempotent top"
   by simp
 
 text \<open>up-closed\<close>
 
 lemma zero_up_closed:
   "up_closed bot"
   by (simp add: up_closed_def)
 
 lemma one_up_closed:
   "up_closed 1"
   by (simp add: up_closed_def)
 
 lemma top_up_closed:
   "up_closed top"
   by (simp add: vector_up_closed)
 
 lemma sup_up_closed:
   "up_closed x \<Longrightarrow> up_closed y \<Longrightarrow> up_closed (x \<squnion> y)"
   by (simp add: mult_right_dist_sup up_closed_def)
 
 lemma inf_up_closed:
   "up_closed x \<Longrightarrow> up_closed y \<Longrightarrow> up_closed (x \<sqinter> y)"
   by (metis order.antisym mult_sub_right_one mult_right_sub_dist_inf up_closed_def)
 
 lemma comp_up_closed:
   "up_closed x \<Longrightarrow> up_closed y \<Longrightarrow> up_closed (x * y)"
   by (metis order.antisym mult_semi_associative mult_sub_right_one up_closed_def)
 
 text \<open>add-distributive\<close>
 
 lemma zero_sup_distributive:
   "sup_distributive bot"
   by (simp add: sup_distributive_def)
 
 lemma one_sup_distributive:
   "sup_distributive 1"
   by (simp add: sup_distributive_def)
 
 lemma sup_sup_distributive:
   "sup_distributive x \<Longrightarrow> sup_distributive y \<Longrightarrow> sup_distributive (x \<squnion> y)"
   using sup_distributive_def mult_right_dist_sup sup_monoid.add_assoc sup_monoid.add_commute by auto
 
 text \<open>inf-distributive\<close>
 
 lemma zero_inf_distributive:
   "inf_distributive bot"
   by (simp add: inf_distributive_def)
 
 lemma one_inf_distributive:
   "inf_distributive 1"
   by (simp add: inf_distributive_def)
 
 text \<open>contact\<close>
 
 lemma one_contact:
   "contact 1"
   by (simp add: contact_def)
 
 lemma top_contact:
   "contact top"
   by (simp add: contact_def)
 
 lemma inf_contact:
   "contact x \<Longrightarrow> contact y \<Longrightarrow> contact (x \<sqinter> y)"
   by (meson contact_reflexive_idempotent_up_closed contact_transitive inf_reflexive inf_transitive inf_up_closed preorder_idempotent)
 
 text \<open>kernel\<close>
 
 lemma zero_kernel:
   "kernel bot"
   by (simp add: kernel_def)
 
 lemma one_kernel:
   "kernel 1"
   by (simp add: kernel_def)
 
 lemma sup_kernel:
   "kernel x \<Longrightarrow> kernel y \<Longrightarrow> kernel (x \<squnion> y)"
   using kernel_coreflexive_idempotent_up_closed order.antisym coreflexive_transitive sup_dense sup_up_closed by force
 
 text \<open>add-distributive contact\<close>
 
 lemma one_sup_dist_contact:
   "sup_dist_contact 1"
   by (simp add: sup_dist_contact_def one_sup_distributive one_contact)
 
 text \<open>inf-distributive kernel\<close>
 
 lemma zero_inf_dist_kernel:
   "inf_dist_kernel bot"
   by (simp add: inf_dist_kernel_def zero_kernel zero_inf_distributive)
 
 lemma one_inf_dist_kernel:
   "inf_dist_kernel 1"
   by (simp add: inf_dist_kernel_def one_kernel one_inf_distributive)
 
 text \<open>test\<close>
 
 lemma zero_test:
   "test bot"
   by (simp add: test_def)
 
 lemma one_test:
   "test 1"
   by (simp add: test_def)
 
 lemma sup_test:
   "test x \<Longrightarrow> test y \<Longrightarrow> test (x \<squnion> y)"
   by (simp add: inf_sup_distrib2 mult_right_dist_sup test_def)
 
 lemma inf_test:
   "test x \<Longrightarrow> test y \<Longrightarrow> test (x \<sqinter> y)"
   by (smt (z3) inf.left_commute idempotent_one_closed inf.le_iff_sup inf_top.right_neutral mult_right_isotone mult_sub_right_one mult_right_sub_dist_inf test_def top_mult_right_one)
 
 text \<open>co-test\<close>
 
 lemma one_co_test:
   "co_test 1"
   by (simp add: co_test_def)
 
 lemma sup_co_test:
   "co_test x \<Longrightarrow> co_test y \<Longrightarrow> co_test (x \<squnion> y)"
   by (smt (z3) co_test_def mult_right_dist_sup sup.left_idem sup_assoc sup_commute)
 
 text \<open>vector\<close>
 
 lemma zero_vector:
   "vector bot"
   by simp
 
 lemma top_vector:
   "vector top"
   by simp
 
 lemma sup_vector:
   "vector x \<Longrightarrow> vector y \<Longrightarrow> vector (x \<squnion> y)"
   by (simp add: vector_sup_closed)
 
 lemma inf_vector:
   "vector x \<Longrightarrow> vector y \<Longrightarrow> vector (x \<sqinter> y)"
   by (metis order.antisym top_right_mult_increasing mult_right_sub_dist_inf)
 
 lemma comp_vector:
   "vector y \<Longrightarrow> vector (x * y)"
   by (simp add: vector_mult_closed)
 
 end
 
 class lattice_ordered_pre_left_semiring_1 = non_associative_left_semiring + bounded_distrib_lattice +
   assumes mult_associative_one: "x * (y * z) = (x * (y * 1)) * z"
   assumes mult_right_dist_inf_one: "(x * 1 \<sqinter> y * 1) * z = x * z \<sqinter> y * z"
 begin
 
 subclass pre_left_semiring
   apply unfold_locales
   by (metis mult_associative_one mult_left_isotone mult_right_isotone mult_sub_right_one)
 
 subclass lattice_ordered_pre_left_semiring ..
 
 lemma mult_zero_associative:
   "x * bot * y = x * bot"
   by (metis mult_associative_one mult_left_zero)
 
 lemma mult_zero_sup_one_dist:
   "(x * bot \<squnion> 1) * z = x * bot \<squnion> z"
   by (simp add: mult_right_dist_sup mult_zero_associative)
 
 lemma mult_zero_sup_dist:
   "(x * bot \<squnion> y) * z = x * bot \<squnion> y * z"
   by (simp add: mult_right_dist_sup mult_zero_associative)
 
 lemma vector_zero_inf_one_comp:
   "(x * bot \<sqinter> 1) * y = x * bot \<sqinter> y"
   by (metis mult_left_one mult_right_dist_inf_one mult_zero_associative)
 
 text \<open>AAMP Theorem 6 / Figure 2: relations between properties\<close>
 
 lemma co_test_inf_distributive:
   "co_test x \<Longrightarrow> inf_distributive x"
   by (metis co_test_def distrib_imp1 inf_sup_distrib1 inf_distributive_def mult_zero_sup_one_dist)
 
 lemma co_test_sup_distributive:
   "co_test x \<Longrightarrow> sup_distributive x"
   by (metis sup_sup_distributive sup_distributive_def co_test_def one_sup_distributive sup.idem mult_zero_associative)
 
 lemma co_test_sup_dist_contact:
   "co_test x \<Longrightarrow> sup_dist_contact x"
   by (simp add: co_test_sup_distributive sup_dist_contact_def co_test_contact)
 
 text \<open>AAMP Theorem 10 / Figure 3: closure properties\<close>
 
 text \<open>co-test\<close>
 
 lemma inf_co_test:
   "co_test x \<Longrightarrow> co_test y \<Longrightarrow> co_test (x \<sqinter> y)"
   by (smt (z3) co_test_def co_test_up_closed mult_right_dist_inf_one sup_commute sup_inf_distrib1 up_closed_def)
 
 lemma comp_co_test:
   "co_test x \<Longrightarrow> co_test y \<Longrightarrow> co_test (x * y)"
   by (metis co_test_def mult_associative_one sup_assoc mult_zero_sup_one_dist)
 
 end
 
 class lattice_ordered_pre_left_semiring_2 = lattice_ordered_pre_left_semiring +
   assumes mult_sub_associative_one: "x * (y * z) \<le> (x * (y * 1)) * z"
   assumes mult_right_dist_inf_one_sub: "x * z \<sqinter> y * z \<le> (x * 1 \<sqinter> y * 1) * z"
 begin
 
 subclass lattice_ordered_pre_left_semiring_1
   apply unfold_locales
   apply (simp add: order.antisym mult_sub_associative_one mult_sup_associative_one)
   by (metis order.eq_iff mult_one_associative mult_right_dist_inf_one_sub mult_right_sub_dist_inf)
 
 end
 
 class multirelation_algebra_1 = lattice_ordered_pre_left_semiring +
   assumes mult_left_top: "top * x = top"
 begin
 
 text \<open>AAMP Theorem 10 / Figure 3: closure properties\<close>
 
 lemma top_sup_distributive:
   "sup_distributive top"
   by (simp add: sup_distributive_def mult_left_top)
 
 lemma top_inf_distributive:
   "inf_distributive top"
   by (simp add: inf_distributive_def mult_left_top)
 
 lemma top_sup_dist_contact:
   "sup_dist_contact top"
   by (simp add: sup_dist_contact_def top_contact top_sup_distributive)
 
 lemma top_co_test:
   "co_test top"
   by (simp add: co_test_def mult_left_top)
 
 end
 
 text \<open>M1-algebra\<close>
 
 class multirelation_algebra_2 = multirelation_algebra_1 + lattice_ordered_pre_left_semiring_2
 begin
 
 lemma mult_top_associative:
   "x * top * y = x * top"
   by (metis mult_left_top mult_associative_one)
 
 lemma vector_inf_one_comp:
   "(x * top \<sqinter> 1) * y = x * top \<sqinter> y"
   by (metis vector_zero_inf_one_comp mult_top_associative)
 
 lemma vector_left_annihilator:
   "vector x \<Longrightarrow> x * y = x"
   by (metis mult_top_associative)
 
 text \<open>properties\<close>
 
 lemma test_comp_inf:
   "test x \<Longrightarrow> test y \<Longrightarrow> x * y = x \<sqinter> y"
   by (metis inf.absorb1 inf.left_commute test_coreflexive test_def vector_inf_one_comp)
 
 text \<open>AAMP Theorem 6 / Figure 2: relations between properties\<close>
 
 lemma test_sup_distributive:
   "test x \<Longrightarrow> sup_distributive x"
   by (metis sup_distributive_def inf_sup_distrib1 test_def vector_inf_one_comp)
 
 lemma test_inf_distributive:
   "test x \<Longrightarrow> inf_distributive x"
   by (smt (verit, ccfv_SIG) inf.commute inf.sup_monoid.add_assoc inf_distributive_def test_def inf.idem vector_inf_one_comp)
 
 lemma test_inf_dist_kernel:
   "test x \<Longrightarrow> inf_dist_kernel x"
   by (simp add: kernel_def inf_dist_kernel_def one_test test_comp_inf test_inf_distributive)
 
 lemma vector_idempotent:
   "vector x \<Longrightarrow> idempotent x"
   using vector_left_annihilator by blast
 
 lemma vector_sup_distributive:
   "vector x \<Longrightarrow> sup_distributive x"
   by (simp add: sup_distributive_def vector_left_annihilator)
 
 lemma vector_inf_distributive:
   "vector x \<Longrightarrow> inf_distributive x"
   by (simp add: inf_distributive_def vector_left_annihilator)
 
 lemma vector_co_vector:
   "vector x \<longleftrightarrow> co_vector x"
   by (metis co_vector_def mult_zero_associative mult_top_associative)
 
 text \<open>AAMP Theorem 10 / Figure 3: closure properties\<close>
 
 text \<open>test\<close>
 
 lemma comp_test:
   "test x \<Longrightarrow> test y \<Longrightarrow> test (x * y)"
   by (simp add: inf_test test_comp_inf)
 
 end
 
 class dual =
   fixes dual :: "'a \<Rightarrow> 'a" ("_\<^sup>d" [100] 100)
 
 class multirelation_algebra_3 = lattice_ordered_pre_left_semiring + dual +
   assumes dual_involutive: "x\<^sup>d\<^sup>d = x"
   assumes dual_dist_sup: "(x \<squnion> y)\<^sup>d = x\<^sup>d \<sqinter> y\<^sup>d"
   assumes dual_one: "1\<^sup>d = 1"
 begin
 
 lemma dual_dist_inf:
   "(x \<sqinter> y)\<^sup>d = x\<^sup>d \<squnion> y\<^sup>d"
   by (metis dual_dist_sup dual_involutive)
 
 lemma dual_antitone:
   "x \<le> y \<Longrightarrow> y\<^sup>d \<le> x\<^sup>d"
   using dual_dist_sup sup_right_divisibility by fastforce
 
 lemma dual_zero:
   "bot\<^sup>d = top"
   by (metis dual_antitone bot_least dual_involutive top_le)
 
 lemma dual_top:
   "top\<^sup>d = bot"
   using dual_zero dual_involutive by auto
 
 text \<open>AAMP Theorem 10 / Figure 3: closure properties\<close>
 
 lemma reflexive_coreflexive_dual:
   "reflexive x \<longleftrightarrow> coreflexive (x\<^sup>d)"
   using dual_antitone dual_involutive dual_one by fastforce
 
 end
 
 class multirelation_algebra_4 = multirelation_algebra_3 +
   assumes dual_sub_dist_comp: "(x * y)\<^sup>d \<le> x\<^sup>d * y\<^sup>d"
 begin
 
 subclass multirelation_algebra_1
   apply unfold_locales
   by (metis order.antisym top.extremum dual_zero dual_sub_dist_comp dual_involutive mult_left_zero)
 
 lemma dual_sub_dist_comp_one:
   "(x * y)\<^sup>d \<le> (x * 1)\<^sup>d * y\<^sup>d"
   by (metis dual_sub_dist_comp mult_one_associative)
 
 text \<open>AAMP Theorem 10 / Figure 3: closure properties\<close>
 
 lemma co_total_total_dual:
   "co_total x \<Longrightarrow> total (x\<^sup>d)"
   by (metis co_total_def dual_sub_dist_comp dual_zero top_le)
 
 lemma transitive_dense_dual:
   "transitive x \<Longrightarrow> dense_rel (x\<^sup>d)"
   using dual_antitone dual_sub_dist_comp inf.order_lesseq_imp by blast
 
 end
 
 text \<open>M2-algebra\<close>
 
 class multirelation_algebra_5 = multirelation_algebra_3 +
   assumes dual_dist_comp_one: "(x * y)\<^sup>d = (x * 1)\<^sup>d * y\<^sup>d"
 begin
 
 subclass multirelation_algebra_4
   apply unfold_locales
   by (metis dual_antitone mult_sub_right_one mult_left_isotone dual_dist_comp_one)
 
 lemma strong_up_closed:
   "x * 1 \<le> x \<Longrightarrow> x\<^sup>d * y\<^sup>d \<le> (x * y)\<^sup>d"
   by (simp add: dual_dist_comp_one antisym_conv mult_sub_right_one)
 
 lemma strong_up_closed_2:
   "up_closed x \<Longrightarrow> (x * y)\<^sup>d = x\<^sup>d * y\<^sup>d"
   by (simp add: dual_dist_comp_one up_closed_def)
 
 subclass lattice_ordered_pre_left_semiring_2
   apply unfold_locales
   apply (smt comp_up_closed dual_antitone dual_dist_comp_one dual_involutive dual_one mult_left_one mult_one_associative mult_semi_associative up_closed_def strong_up_closed_2)
   by (smt dual_dist_comp_one dual_dist_inf dual_involutive eq_refl mult_one_associative mult_right_dist_sup)
 
 text \<open>AAMP Theorem 8\<close>
 
 subclass multirelation_algebra_2 ..
 
 text \<open>AAMP Theorem 10 / Figure 3: closure properties\<close>
 
 text \<open>up-closed\<close>
 
 lemma dual_up_closed:
   "up_closed x \<longleftrightarrow> up_closed (x\<^sup>d)"
   by (metis dual_involutive dual_one up_closed_def strong_up_closed_2)
 
 text \<open>contact\<close>
 
 lemma contact_kernel_dual:
   "contact x \<longleftrightarrow> kernel (x\<^sup>d)"
   by (metis contact_def contact_up_closed dual_dist_sup dual_involutive dual_one kernel_def kernel_up_closed up_closed_def strong_up_closed_2)
 
 text \<open>add-distributive contact\<close>
 
 lemma sup_dist_contact_inf_dist_kernel_dual:
   "sup_dist_contact x \<longleftrightarrow> inf_dist_kernel (x\<^sup>d)"
 proof
   assume 1: "sup_dist_contact x"
   hence 2: "up_closed x"
     using sup_dist_contact_def contact_up_closed by auto
   have "sup_distributive x"
     using 1 sup_dist_contact_def by auto
   hence "inf_distributive (x\<^sup>d)"
     using 2 by (smt sup_distributive_def dual_dist_comp_one dual_dist_inf dual_involutive inf_distributive_def up_closed_def)
   thus "inf_dist_kernel (x\<^sup>d)"
     using 1 contact_kernel_dual sup_dist_contact_def inf_dist_kernel_def by blast
 next
   assume 3: "inf_dist_kernel (x\<^sup>d)"
   hence 4: "up_closed (x\<^sup>d)"
     using kernel_up_closed inf_dist_kernel_def by auto
   have "inf_distributive (x\<^sup>d)"
     using 3 inf_dist_kernel_def by auto
   hence "sup_distributive (x\<^sup>d\<^sup>d)"
     using 4 by (smt inf_distributive_def sup_distributive_def dual_dist_sup dual_involutive strong_up_closed_2)
   thus "sup_dist_contact x"
     using 3 contact_kernel_dual sup_dist_contact_def dual_involutive inf_dist_kernel_def by auto
 qed
 
 text \<open>test\<close>
 
 lemma test_co_test_dual:
   "test x \<longleftrightarrow> co_test (x\<^sup>d)"
   by (smt (z3) co_test_def co_test_up_closed dual_dist_comp_one dual_dist_inf dual_involutive dual_one dual_top test_def test_up_closed up_closed_def)
 
 text \<open>vector\<close>
 
 lemma vector_dual:
   "vector x \<longleftrightarrow> vector (x\<^sup>d)"
   by (metis dual_dist_comp_one dual_involutive mult_top_associative)
 
 end
 
 class multirelation_algebra_6 = multirelation_algebra_4 +
   assumes dual_sub_dist_comp_one: "(x * 1)\<^sup>d * y\<^sup>d \<le> (x * y)\<^sup>d"
 begin
 
 subclass multirelation_algebra_5
   apply unfold_locales
   by (metis dual_sub_dist_comp dual_sub_dist_comp_one order.eq_iff mult_one_associative)
 
 proposition "dense_rel x \<and> coreflexive x \<longrightarrow> up_closed x" nitpick [expect=genuine,card=5] oops
 proposition "x * top \<sqinter> y * z \<le> (x * top \<sqinter> y) * z" nitpick [expect=genuine,card=8] oops
 
 end
 
 text \<open>M3-algebra\<close>
 
 class up_closed_multirelation_algebra = multirelation_algebra_3 +
   assumes dual_dist_comp: "(x * y)\<^sup>d = x\<^sup>d * y\<^sup>d"
 begin
 
 lemma mult_right_dist_inf:
   "(x \<sqinter> y) * z = x * z \<sqinter> y * z"
   by (metis dual_dist_sup dual_dist_comp dual_involutive mult_right_dist_sup)
 
 text \<open>AAMP Theorem 9\<close>
 
 subclass idempotent_left_semiring
   apply unfold_locales
   apply (metis order.antisym dual_antitone dual_dist_comp dual_involutive mult_semi_associative)
   apply simp
   by (metis order.antisym dual_antitone dual_dist_comp dual_involutive dual_one mult_sub_right_one)
 
 subclass multirelation_algebra_6
   apply unfold_locales
   by (simp_all add: dual_dist_comp)
 
 lemma vector_inf_comp:
   "(x * top \<sqinter> y) * z = x * top \<sqinter> y * z"
   by (simp add: vector_left_annihilator mult_right_dist_inf mult.assoc)
 
 lemma vector_zero_inf_comp:
   "(x * bot \<sqinter> y) * z = x * bot \<sqinter> y * z"
   by (simp add: mult_right_dist_inf mult.assoc)
 
 text \<open>AAMP Theorem 10 / Figure 3: closure properties\<close>
 
 text \<open>total\<close>
 
 lemma inf_total:
   "total x \<Longrightarrow> total y \<Longrightarrow> total (x \<sqinter> y)"
   by (simp add: mult_right_dist_inf)
 
 lemma comp_total:
   "total x \<Longrightarrow> total y \<Longrightarrow> total (x * y)"
   by (simp add: mult_assoc)
 
 lemma total_co_total_dual:
   "total x \<longleftrightarrow> co_total (x\<^sup>d)"
   by (metis co_total_def dual_dist_comp dual_involutive dual_top)
 
 text \<open>dense\<close>
 
 lemma transitive_iff_dense_dual:
   "transitive x \<longleftrightarrow> dense_rel (x\<^sup>d)"
   by (metis dual_antitone dual_dist_comp dual_involutive)
 
 text \<open>idempotent\<close>
 
 lemma idempotent_dual:
   "idempotent x \<longleftrightarrow> idempotent (x\<^sup>d)"
   using dual_involutive idempotent_transitive_dense transitive_iff_dense_dual by auto
 
 text \<open>add-distributive\<close>
 
 lemma comp_sup_distributive:
   "sup_distributive x \<Longrightarrow> sup_distributive y \<Longrightarrow> sup_distributive (x * y)"
   by (simp add: sup_distributive_def mult.assoc)
 
 lemma sup_inf_distributive_dual:
   "sup_distributive x \<longleftrightarrow> inf_distributive (x\<^sup>d)"
   by (smt (verit, ccfv_threshold) sup_distributive_def dual_dist_sup dual_dist_comp dual_dist_inf dual_involutive inf_distributive_def)
 
 text \<open>inf-distributive\<close>
 
 lemma inf_inf_distributive:
   "inf_distributive x \<Longrightarrow> inf_distributive y \<Longrightarrow> inf_distributive (x \<sqinter> y)"
   by (metis sup_inf_distributive_dual sup_sup_distributive dual_dist_inf dual_involutive)
 
 lemma comp_inf_distributive:
   "inf_distributive x \<Longrightarrow> inf_distributive y \<Longrightarrow> inf_distributive (x * y)"
   by (simp add: inf_distributive_def mult.assoc)
 
 proposition "co_total x \<and> transitive x \<and> up_closed x \<longrightarrow> coreflexive x" nitpick [expect=genuine,card=5] oops
 proposition "total x \<and> dense_rel x \<and> up_closed x \<longrightarrow> reflexive x" nitpick [expect=genuine,card=5] oops
 proposition "x * top \<sqinter> x\<^sup>d * bot = bot" nitpick [expect=genuine,card=6] oops
 
 end
 
 class multirelation_algebra_7 = multirelation_algebra_4 +
   assumes vector_inf_comp: "(x * top \<sqinter> y) * z = x * top \<sqinter> y * z"
 begin
 
 lemma vector_zero_inf_comp:
   "(x * bot \<sqinter> y) * z = x * bot \<sqinter> y * z"
   by (metis vector_inf_comp vector_mult_closed zero_vector)
 
 lemma test_sup_distributive:
   "test x \<Longrightarrow> sup_distributive x"
   by (metis sup_distributive_def inf_sup_distrib1 mult_left_one test_def vector_inf_comp)
 
 lemma test_inf_distributive:
   "test x \<Longrightarrow> inf_distributive x"
   by (smt (z3) inf.right_idem inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_distributive_def mult_left_one test_def vector_inf_comp)
 
 lemma test_inf_dist_kernel:
   "test x \<Longrightarrow> inf_dist_kernel x"
   by (metis inf.idem inf.sup_monoid.add_assoc kernel_def inf_dist_kernel_def mult_left_one test_def test_inf_distributive vector_inf_comp)
 
 lemma co_test_inf_distributive:
   assumes "co_test x"
     shows "inf_distributive x"
 proof -
   have "x = x * bot \<squnion> 1"
     using assms co_test_def by auto
   hence "\<forall>y z . x * y \<sqinter> x * z = x * (y \<sqinter> z)"
     by (metis distrib_imp1 inf_sup_absorb inf_sup_distrib1 mult_left_one mult_left_top mult_right_dist_sup sup_top_right vector_zero_inf_comp)
   thus "inf_distributive x"
     by (simp add: inf_distributive_def)
 qed
 
 lemma co_test_sup_distributive:
   assumes "co_test x"
     shows "sup_distributive x"
 proof -
   have "x = x * bot \<squnion> 1"
     using assms co_test_def by auto
   hence "\<forall>y z . x * (y \<squnion> z) = x * y \<squnion> x * z"
     by (metis sup_sup_distributive sup_distributive_def inf_sup_absorb mult_left_top one_sup_distributive sup.idem sup_top_right vector_zero_inf_comp)
   thus "sup_distributive x"
     by (simp add: sup_distributive_def)
 qed
 
 lemma co_test_sup_dist_contact:
   "co_test x \<Longrightarrow> sup_dist_contact x"
   by (simp add: sup_dist_contact_def co_test_sup_distributive co_test_contact)
 
 end
 
 end
 
diff --git a/thys/Correctness_Algebras/Omega_Algebras.thy b/thys/Correctness_Algebras/Omega_Algebras.thy
--- a/thys/Correctness_Algebras/Omega_Algebras.thy
+++ b/thys/Correctness_Algebras/Omega_Algebras.thy
@@ -1,497 +1,499 @@
 (* Title:      Omega Algebras
    Author:     Walter Guttmann
    Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
 *)
 
 section \<open>Omega Algebras\<close>
 
 theory Omega_Algebras
 
 imports Stone_Kleene_Relation_Algebras.Kleene_Algebras
 
 begin
 
+nitpick_params [timeout = 600]
+
 class omega =
   fixes omega :: "'a \<Rightarrow> 'a" ("_\<^sup>\<omega>" [100] 100)
 
 class left_omega_algebra = left_kleene_algebra + omega +
   assumes omega_unfold: "y\<^sup>\<omega> = y * y\<^sup>\<omega>"
   assumes omega_induct: "x \<le> z \<squnion> y * x \<longrightarrow> x \<le> y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * z"
 begin
 
 text \<open>Many lemmas in this class are taken from Georg Struth's Isabelle theories.\<close>
 
 lemma star_bot_below_omega:
   "x\<^sup>\<star> * bot \<le> x\<^sup>\<omega>"
   using omega_unfold star_left_induct_equal by auto
 
 lemma star_bot_below_omega_bot:
   "x\<^sup>\<star> * bot \<le> x\<^sup>\<omega> * bot"
   by (metis omega_unfold star_left_induct_equal sup_monoid.add_0_left mult_assoc)
 
 lemma omega_induct_mult:
   "y \<le> x * y \<Longrightarrow> y \<le> x\<^sup>\<omega>"
   by (metis bot_least omega_induct sup.absorb1 sup.absorb2 star_bot_below_omega)
 
 lemma omega_sub_dist:
   "x\<^sup>\<omega> \<le> (x \<squnion> y)\<^sup>\<omega>"
   by (metis eq_refl mult_isotone omega_unfold sup.cobounded1 omega_induct_mult)
 
 lemma omega_isotone:
   "x \<le> y \<Longrightarrow> x\<^sup>\<omega> \<le> y\<^sup>\<omega>"
   using sup_left_divisibility omega_sub_dist by fastforce
 
 lemma omega_induct_equal:
   "y = z \<squnion> x * y \<Longrightarrow> y \<le> x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * z"
   by (simp add: omega_induct)
 
 lemma omega_bot:
   "bot\<^sup>\<omega> = bot"
   by (metis mult_left_zero omega_unfold)
 
 lemma omega_one_greatest:
   "x \<le> 1\<^sup>\<omega>"
   by (simp add: omega_induct_mult)
 
 lemma star_mult_omega:
   "x\<^sup>\<star> * x\<^sup>\<omega> = x\<^sup>\<omega>"
   by (metis order.antisym omega_unfold star.circ_loop_fixpoint star_left_induct_mult_equal sup.cobounded2)
 
 lemma omega_sub_vector:
   "x\<^sup>\<omega> * y \<le> x\<^sup>\<omega>"
   by (metis mult_semi_associative omega_unfold omega_induct_mult)
 
 lemma omega_simulation:
   "z * x \<le> y * z \<Longrightarrow> z * x\<^sup>\<omega> \<le> y\<^sup>\<omega>"
   by (smt (verit, ccfv_threshold) mult_isotone omega_unfold order_lesseq_imp mult_assoc omega_induct_mult)
 
 lemma omega_omega:
   "x\<^sup>\<omega>\<^sup>\<omega> \<le> x\<^sup>\<omega>"
   by (metis omega_unfold omega_sub_vector)
 
 lemma left_plus_omega:
   "(x * x\<^sup>\<star>)\<^sup>\<omega> = x\<^sup>\<omega>"
   by (metis order.antisym mult_assoc omega_induct_mult omega_unfold order_refl star.left_plus_circ star_mult_omega)
 
 lemma omega_slide:
   "x * (y * x)\<^sup>\<omega> = (x * y)\<^sup>\<omega>"
   by (metis order.antisym mult_assoc mult_right_isotone omega_simulation omega_unfold order_refl)
 
 lemma omega_simulation_2:
   "y * x \<le> x * y \<Longrightarrow> (x * y)\<^sup>\<omega> \<le> x\<^sup>\<omega>"
   by (metis mult_right_isotone sup.absorb2 omega_induct_mult omega_slide omega_sub_dist)
 
 lemma wagner:
   "(x \<squnion> y)\<^sup>\<omega> = x * (x \<squnion> y)\<^sup>\<omega> \<squnion> z \<Longrightarrow> (x \<squnion> y)\<^sup>\<omega> = x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * z"
   by (smt (verit, ccfv_SIG) order.refl star_left_induct sup.absorb2 sup_assoc sup_commute omega_induct_equal omega_sub_dist)
 
 lemma right_plus_omega:
   "(x\<^sup>\<star> * x)\<^sup>\<omega> = x\<^sup>\<omega>"
   by (metis left_plus_omega omega_slide star_mult_omega)
 
 lemma omega_sub_dist_1:
   "(x * y\<^sup>\<star>)\<^sup>\<omega> \<le> (x \<squnion> y)\<^sup>\<omega>"
   by (metis left_plus_omega mult_isotone star.circ_sub_dist sup.cobounded1 sup_monoid.add_commute omega_isotone)
 
 lemma omega_sub_dist_2:
   "(x\<^sup>\<star> * y)\<^sup>\<omega> \<le> (x \<squnion> y)\<^sup>\<omega>"
   by (metis mult_isotone star.circ_sub_dist sup.cobounded2 omega_isotone right_plus_omega)
 
 lemma omega_star:
   "(x\<^sup>\<omega>)\<^sup>\<star> = 1 \<squnion> x\<^sup>\<omega>"
   by (metis antisym_conv star.circ_mult_increasing star_left_unfold_equal omega_sub_vector)
 
 lemma omega_mult_omega_star:
   "x\<^sup>\<omega> * x\<^sup>\<omega>\<^sup>\<star> = x\<^sup>\<omega>"
   by (simp add: order.antisym star.circ_mult_increasing omega_sub_vector)
 
 lemma omega_sum_unfold_1:
   "(x \<squnion> y)\<^sup>\<omega> = x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * (x \<squnion> y)\<^sup>\<omega>"
   by (metis mult_right_dist_sup omega_unfold mult_assoc wagner)
 
 lemma omega_sum_unfold_2:
   "(x \<squnion> y)\<^sup>\<omega> \<le> (x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>"
   using omega_induct_equal omega_sum_unfold_1 by auto
 
 lemma omega_sum_unfold_3:
   "(x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega> \<le> (x \<squnion> y)\<^sup>\<omega>"
   using star_left_induct_equal omega_sum_unfold_1 by auto
 
 lemma omega_decompose:
   "(x \<squnion> y)\<^sup>\<omega> = (x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>"
   by (metis sup.absorb1 sup_same_context omega_sub_dist_2 omega_sum_unfold_2 omega_sum_unfold_3)
 
 lemma omega_loop_fixpoint:
   "y * (y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * z) \<squnion> z = y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * z"
   apply (rule order.antisym)
   apply (smt (verit, ccfv_threshold) eq_refl mult_isotone mult_left_sub_dist_sup omega_induct omega_unfold star.circ_loop_fixpoint sup_assoc sup_commute sup_right_isotone)
   by (smt (z3) mult_left_sub_dist_sup omega_unfold star.circ_loop_fixpoint sup.left_commute sup_commute sup_right_isotone)
 
 lemma omega_loop_greatest_fixpoint:
   "y * x \<squnion> z = x \<Longrightarrow> x \<le> y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * z"
   by (simp add: sup_commute omega_induct_equal)
 
 lemma omega_square:
   "x\<^sup>\<omega> = (x * x)\<^sup>\<omega>"
   using order.antisym omega_unfold order_refl mult_assoc omega_induct_mult omega_simulation_2 by auto
 
 lemma mult_bot_omega:
   "(x * bot)\<^sup>\<omega> = x * bot"
   by (metis mult_left_zero omega_slide)
 
 lemma mult_bot_add_omega:
   "(x \<squnion> y * bot)\<^sup>\<omega> = x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * bot"
   by (metis mult_left_zero sup_commute mult_assoc mult_bot_omega omega_decompose omega_loop_fixpoint)
 
 lemma omega_mult_star:
   "x\<^sup>\<omega> * x\<^sup>\<star> = x\<^sup>\<omega>"
   by (meson antisym_conv star.circ_back_loop_prefixpoint sup.boundedE omega_sub_vector)
 
 lemma omega_loop_is_greatest_fixpoint:
   "is_greatest_fixpoint (\<lambda>x . y * x \<squnion> z) (y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * z)"
   by (simp add: is_greatest_fixpoint_def omega_loop_fixpoint omega_loop_greatest_fixpoint)
 
 lemma omega_loop_nu:
   "\<nu> (\<lambda>x . y * x \<squnion> z) = y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * z"
   by (metis greatest_fixpoint_same omega_loop_is_greatest_fixpoint)
 
 lemma omega_loop_bot_is_greatest_fixpoint:
   "is_greatest_fixpoint (\<lambda>x . y * x) (y\<^sup>\<omega>)"
   using is_greatest_fixpoint_def omega_unfold omega_induct_mult by auto
 
 lemma omega_loop_bot_nu:
   "\<nu> (\<lambda>x . y * x) = y\<^sup>\<omega>"
   by (metis greatest_fixpoint_same omega_loop_bot_is_greatest_fixpoint)
 
 lemma affine_has_greatest_fixpoint:
   "has_greatest_fixpoint (\<lambda>x . y * x \<squnion> z)"
   using has_greatest_fixpoint_def omega_loop_is_greatest_fixpoint by blast
 
 lemma omega_separate_unfold:
   "(x\<^sup>\<star> * y)\<^sup>\<omega> = y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * x * (x\<^sup>\<star> * y)\<^sup>\<omega>"
   by (metis star.circ_loop_fixpoint sup_commute mult_assoc omega_slide omega_sum_unfold_1)
 
 lemma omega_bot_left_slide:
   "(x * y)\<^sup>\<star> * ((x * y)\<^sup>\<omega> * bot \<squnion> 1) * x \<le> x * (y * x)\<^sup>\<star> * ((y * x)\<^sup>\<omega> * bot \<squnion> 1)"
 proof -
   have "x \<squnion> x * (y * x) * (y * x)\<^sup>\<star> * ((y * x)\<^sup>\<omega> * bot \<squnion> 1) \<le> x * (y * x)\<^sup>\<star> * ((y * x)\<^sup>\<omega> * bot \<squnion> 1)"
     by (metis sup_commute mult_assoc mult_right_isotone star.circ_back_loop_prefixpoint star.mult_zero_sup_circ star.mult_zero_circ le_supE le_supI order.refl star.circ_increasing star.circ_mult_upper_bound)
   hence "((x * y)\<^sup>\<omega> * bot \<squnion> 1) * x \<squnion> x * y * (x * (y * x)\<^sup>\<star> * ((y * x)\<^sup>\<omega> * bot \<squnion> 1)) \<le> x * (y * x)\<^sup>\<star> * ((y * x)\<^sup>\<omega> * bot \<squnion> 1)"
     by (smt (z3) sup.absorb_iff2 sup_assoc mult_assoc mult_left_one mult_left_sub_dist_sup_left mult_left_zero mult_right_dist_sup omega_slide star_mult_omega)
   thus ?thesis
     by (simp add: star_left_induct mult_assoc)
 qed
 
 lemma omega_bot_add_1:
   "(x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1) = x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1)"
 proof (rule order.antisym)
   have 1: "(x \<squnion> y) * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1) \<le> x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1)"
     by (smt (z3) eq_refl star.circ_mult_upper_bound star.circ_sub_dist_1 star.mult_zero_circ star.mult_zero_sup_circ star_sup_1 sup_assoc sup_commute mult_assoc)
   have 2: "1 \<le> x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1)"
     using reflexive_mult_closed star.circ_reflexive sup_ge2 by auto
   have "(y * x\<^sup>\<star>)\<^sup>\<omega> * bot \<le> (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot"
     by (metis mult_1_right mult_left_isotone mult_left_sub_dist_sup_right omega_isotone)
   also have 3: "... \<le> (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1)"
     by (metis mult_isotone mult_left_one star.circ_reflexive sup_commute sup_ge2)
   finally have 4: "(x\<^sup>\<star> * y)\<^sup>\<omega> * bot \<le> x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1)"
     by (smt mult_assoc mult_right_isotone omega_slide)
   have "y * (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega> * bot \<le> y * (x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> y))\<^sup>\<star> * x\<^sup>\<star> * x\<^sup>\<omega> * bot * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot"
     using mult_isotone mult_left_sub_dist_sup_left mult_left_zero order.refl star_isotone sup_commute mult_assoc star_mult_omega by auto
   also have "... \<le> y * (x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> y))\<^sup>\<star> * (x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * y)\<^sup>\<omega> * bot"
     by (smt mult_assoc mult_left_isotone mult_left_sub_dist_sup_left omega_slide)
   also have "... = y * (x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * y)\<^sup>\<omega> * bot"
     using mult_left_one mult_left_zero mult_right_dist_sup mult_assoc star_mult_omega by auto
   finally have "x\<^sup>\<star> * y * (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega> * bot \<le> x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1)"
     using 3 by (smt mult_assoc mult_right_isotone omega_slide order_trans)
   hence "(x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega> * bot \<le> x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1)"
     by (smt (verit, ccfv_threshold) sup_assoc sup_commute le_iff_sup mult_assoc mult_isotone mult_left_one mult_1_right mult_right_sub_dist_sup_left order_trans star.circ_loop_fixpoint star.circ_reflexive star.mult_zero_circ)
   hence "(x \<squnion> y)\<^sup>\<omega> * bot \<le> x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1)"
     using 4 by (smt (z3) mult_right_dist_sup sup.orderE sup_assoc sup_right_divisibility omega_decompose)
   thus "(x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1) \<le> x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1)"
     using 1 2 star_left_induct mult_assoc by force
 next
   have 5: "x\<^sup>\<omega> * bot \<le> (x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1)"
     by (metis bot_least le_supI1 le_supI2 mult_isotone star.circ_loop_fixpoint sup.cobounded1 omega_isotone)
   have 6: "(y * x\<^sup>\<star>)\<^sup>\<omega> * bot \<le> (x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1)"
     by (metis sup_commute mult_left_isotone omega_sub_dist_1 mult_assoc mult_left_sub_dist_sup_left order_trans star_mult_omega)
   have 7: "(y * x\<^sup>\<star>)\<^sup>\<star> \<le> (x \<squnion> y)\<^sup>\<star>"
     by (metis mult_left_one mult_right_sub_dist_sup_left star.circ_sup_1 star.circ_plus_one)
   hence "(y * x\<^sup>\<star>)\<^sup>\<star> * x\<^sup>\<omega> * bot \<le> (x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1)"
     by (smt sup_assoc le_iff_sup mult_assoc mult_isotone mult_right_dist_sup omega_sub_dist)
   hence "(x\<^sup>\<omega> * bot \<squnion> y * x\<^sup>\<star>)\<^sup>\<omega> * bot \<le> (x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1)"
     using 6 by (smt sup_commute sup.bounded_iff mult_assoc mult_right_dist_sup mult_bot_add_omega omega_unfold omega_bot)
   hence "(y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<le> y * x\<^sup>\<star> * (x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1)"
     by (smt mult_assoc mult_left_one mult_left_zero mult_right_dist_sup mult_right_isotone omega_slide)
   also have "... \<le> (x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1)"
     using 7 by (metis mult_left_isotone order_refl star.circ_mult_upper_bound star_left_induct_mult_iff)
   finally have "(y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1) \<le> (x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1)"
     using 5 by (smt (z3) le_supE star.circ_mult_upper_bound star.circ_sub_dist_1 star.mult_zero_circ star.mult_zero_sup_circ star_involutive star_isotone sup_commute)
   hence "(x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1) \<le> (x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1)"
     using 5 by (metis sup_commute mult_assoc star.circ_isotone star.circ_mult_upper_bound star.mult_zero_sup_circ star.mult_zero_circ star_involutive)
   thus "x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) * (y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<star> * ((y * x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))\<^sup>\<omega> * bot \<squnion> 1) \<le> (x \<squnion> y)\<^sup>\<star> * ((x \<squnion> y)\<^sup>\<omega> * bot \<squnion> 1)"
     by (smt sup_assoc sup_commute mult_assoc star.circ_mult_upper_bound star.circ_sub_dist star.mult_zero_sup_circ star.mult_zero_circ)
 qed
 
 lemma star_omega_greatest:
   "x\<^sup>\<star>\<^sup>\<omega> = 1\<^sup>\<omega>"
   by (metis sup_commute le_iff_sup omega_one_greatest omega_sub_dist star.circ_plus_one)
 
 lemma omega_vector_greatest:
   "x\<^sup>\<omega> * 1\<^sup>\<omega> = x\<^sup>\<omega>"
   by (metis order.antisym mult_isotone omega_mult_omega_star omega_one_greatest omega_sub_vector)
 
 lemma mult_greatest_omega:
   "(x * 1\<^sup>\<omega>)\<^sup>\<omega> \<le> x * 1\<^sup>\<omega>"
   by (metis mult_right_isotone omega_slide omega_sub_vector)
 
 lemma omega_mult_star_2:
   "x\<^sup>\<omega> * y\<^sup>\<star> = x\<^sup>\<omega>"
   by (meson order.antisym le_supE star.circ_back_loop_prefixpoint omega_sub_vector)
 
 lemma omega_import:
   assumes "p \<le> p * p"
       and "p * x \<le> x * p"
     shows "p * x\<^sup>\<omega> = p * (p * x)\<^sup>\<omega>"
 proof -
   have "p * x\<^sup>\<omega> \<le> p * (p * x) * x\<^sup>\<omega>"
     by (metis assms(1) mult_assoc mult_left_isotone omega_unfold)
   also have "... \<le> p * x * p * x\<^sup>\<omega>"
     by (metis assms(2) mult_assoc mult_left_isotone mult_right_isotone)
   finally have "p * x\<^sup>\<omega> \<le> (p * x)\<^sup>\<omega>"
     by (simp add: mult_assoc omega_induct_mult)
   hence "p * x\<^sup>\<omega> \<le> p * (p * x)\<^sup>\<omega>"
     by (metis assms(1) mult_assoc mult_left_isotone mult_right_isotone order_trans)
   thus "p * x\<^sup>\<omega> = p * (p * x)\<^sup>\<omega>"
     by (metis assms(2) sup_left_divisibility order.antisym mult_right_isotone omega_induct_mult omega_slide omega_sub_dist)
 qed
 
 proposition omega_circ_simulate_right_plus: "z * x \<le> y * (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) * z \<squnion> w \<longrightarrow> z * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) \<le> (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) * (z \<squnion> w * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>))" nitpick [expect=genuine,card=4] oops
 proposition omega_circ_simulate_left_plus: "x * z \<le> z * (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) \<squnion> w \<longrightarrow> (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) * z \<le> (z \<squnion> (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) * w) * (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>)" nitpick [expect=genuine,card=5] oops
 
 end
 
 text \<open>Theorem 50.2\<close>
 
 sublocale left_omega_algebra < comb0: left_conway_semiring where circ = "(\<lambda>x . x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))"
   apply unfold_locales
   apply (smt sup_assoc sup_commute le_iff_sup mult_assoc mult_left_sub_dist_sup_left omega_unfold star.circ_loop_fixpoint star_mult_omega)
   using omega_bot_left_slide mult_assoc apply fastforce
   using omega_bot_add_1 mult_assoc by simp
 
 class left_zero_omega_algebra = left_zero_kleene_algebra + left_omega_algebra
 begin
 
 lemma star_omega_absorb:
   "y\<^sup>\<star> * (y\<^sup>\<star> * x)\<^sup>\<star> * y\<^sup>\<omega> = (y\<^sup>\<star> * x)\<^sup>\<star> * y\<^sup>\<omega>"
 proof -
   have "y\<^sup>\<star> * (y\<^sup>\<star> * x)\<^sup>\<star> * y\<^sup>\<omega> = y\<^sup>\<star> * y\<^sup>\<star> * x * (y\<^sup>\<star> * x)\<^sup>\<star> * y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * y\<^sup>\<omega>"
     by (metis sup_commute mult_assoc mult_right_dist_sup star.circ_back_loop_fixpoint star.circ_plus_same)
   thus ?thesis
     by (metis mult_assoc star.circ_loop_fixpoint star.circ_transitive_equal star_mult_omega)
 qed
 
 lemma omega_circ_simulate_right_plus: 
   assumes "z * x \<le> y * (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) * z \<squnion> w"
     shows "z * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) \<le> (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) * (z \<squnion> w * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>))"
 proof -
   have 1: "z * x \<le> y\<^sup>\<omega> * bot \<squnion> y * y\<^sup>\<star> * z \<squnion> w"
     by (metis assms mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup omega_unfold)
   hence "(y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>) * x \<le> y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * (y\<^sup>\<omega> * bot \<squnion> y * y\<^sup>\<star> * z \<squnion> w) \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
     by (smt sup_assoc sup_ge1 sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup star.circ_back_loop_fixpoint)
   also have "... = y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
     by (smt sup_assoc sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup star.circ_back_loop_fixpoint star_mult_omega)
   also have "... \<le> y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
     by (smt sup_commute sup_left_isotone mult_left_isotone star.circ_increasing star.circ_plus_same star.circ_transitive_equal)
   finally have "z \<squnion> (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>) * x \<le> y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
     by (metis (no_types, lifting) le_supE le_supI star.circ_loop_fixpoint sup.cobounded1)
   hence 2: "z * x\<^sup>\<star> \<le> y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
     by (simp add: star_right_induct)
   have "z * x\<^sup>\<omega> * bot \<le> (y\<^sup>\<omega> * bot \<squnion> y * y\<^sup>\<star> * z \<squnion> w) * x\<^sup>\<omega> * bot"
     using 1 by (smt sup_left_divisibility mult_assoc mult_right_sub_dist_sup_left omega_unfold)
   hence "z * x\<^sup>\<omega> * bot \<le> y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * (y\<^sup>\<omega> * bot \<squnion> w * x\<^sup>\<omega> * bot)"
     by (smt sup_assoc sup_commute left_plus_omega mult_assoc mult_left_zero mult_right_dist_sup omega_induct star.left_plus_circ)
   thus "z * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) \<le> (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) * (z \<squnion> w * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>))"
     using 2 by (smt sup_assoc sup_commute le_iff_sup mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup omega_unfold omega_bot star_mult_omega zero_right_mult_decreasing)
 qed
 
 lemma omega_circ_simulate_left_plus:
   assumes "x * z \<le> z * (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) \<squnion> w"
     shows "(x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) * z \<le> (z \<squnion> (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) * w) * (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>)"
 proof -
   have "x * (z * y\<^sup>\<omega> * bot \<squnion> z * y\<^sup>\<star> \<squnion> x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) = x * z * y\<^sup>\<omega> * bot \<squnion> x * z * y\<^sup>\<star> \<squnion> x\<^sup>\<omega> * bot \<squnion> x * x\<^sup>\<star> * w * y\<^sup>\<omega> * bot \<squnion> x * x\<^sup>\<star> * w * y\<^sup>\<star>"
     by (smt mult_assoc mult_left_dist_sup omega_unfold)
   also have "... \<le> x * z * y\<^sup>\<omega> * bot \<squnion> x * z * y\<^sup>\<star> \<squnion> x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
     by (metis sup_mono sup_right_isotone mult_left_isotone star.left_plus_below_circ)
   also have "... \<le> (z * y\<^sup>\<omega> * bot \<squnion> z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<omega> * bot \<squnion> (z * y\<^sup>\<omega> * bot \<squnion> z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<star> \<squnion> x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
     by (metis assms sup_left_isotone mult_assoc mult_left_dist_sup mult_left_isotone)
   also have "... = z * y\<^sup>\<omega> * bot \<squnion> z * y\<^sup>\<star> * y\<^sup>\<omega> * bot \<squnion> w * y\<^sup>\<omega> * bot \<squnion> z * y\<^sup>\<omega> * bot \<squnion> z * y\<^sup>\<star> * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
     by (smt sup_assoc mult_assoc mult_left_zero mult_right_dist_sup)
   also have "... = z * y\<^sup>\<omega> * bot \<squnion> z * y\<^sup>\<star> \<squnion> x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
     by (smt (verit, ccfv_threshold) sup_assoc sup_commute sup_idem mult_assoc mult_right_dist_sup star.circ_loop_fixpoint star.circ_transitive_equal star_mult_omega)
   finally have "x\<^sup>\<star> * z \<le> z * y\<^sup>\<omega> * bot \<squnion> z * y\<^sup>\<star> \<squnion> x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
     by (smt (z3) le_supE sup_least sup_ge1 star.circ_back_loop_fixpoint star_left_induct)
   hence "(x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) * z \<le> z * y\<^sup>\<omega> * bot \<squnion> z * y\<^sup>\<star> \<squnion> x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
     by (smt (z3) sup.left_commute sup_commute sup_least sup_ge1 mult_assoc mult_left_zero mult_right_dist_sup)
   thus "(x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) * z \<le> (z \<squnion> (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) * w) * (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>)"
     by (smt sup_assoc mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup)
 qed
 
 lemma omega_translate:
   "x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) = x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>"
   by (metis mult_assoc mult_left_dist_sup mult_1_right star_mult_omega)
 
 lemma omega_circ_simulate_right:
   assumes "z * x \<le> y * z \<squnion> w"
     shows "z * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) \<le> (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) * (z \<squnion> w * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>))"
 proof -
   have "... \<le> y * (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) * z \<squnion> w"
     using comb0.circ_mult_increasing mult_isotone sup_left_isotone omega_translate by auto
   thus "z * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>) \<le> (y\<^sup>\<omega> * bot \<squnion> y\<^sup>\<star>) * (z \<squnion> w * (x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>))"
     using assms order_trans omega_circ_simulate_right_plus by blast
 qed
 
 end
 
 sublocale left_zero_omega_algebra < comb1: left_conway_semiring_1 where circ = "(\<lambda>x . x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))"
   apply unfold_locales
   by (smt order.eq_iff mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup mult_1_right omega_slide star_slide)
 
 sublocale left_zero_omega_algebra < comb0: itering where circ = "(\<lambda>x . x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))"
   apply unfold_locales
   using comb1.circ_sup_9 apply blast
   using comb1.circ_mult_1 apply blast
   apply (metis omega_circ_simulate_right_plus omega_translate)
   using omega_circ_simulate_left_plus omega_translate by auto
 
 text \<open>Theorem 2.2\<close>
 
 sublocale left_zero_omega_algebra < comb2: itering where circ = "(\<lambda>x . x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star>)"
   apply unfold_locales
   using comb1.circ_sup_9 omega_translate apply force
   apply (metis comb1.circ_mult_1 omega_translate)
   using omega_circ_simulate_right_plus apply blast
   by (simp add: omega_circ_simulate_left_plus)
 
 class omega_algebra = kleene_algebra + left_zero_omega_algebra
 
 class left_omega_conway_semiring = left_omega_algebra + left_conway_semiring
 begin
 
 subclass left_kleene_conway_semiring ..
 
 lemma circ_below_omega_star:
   "x\<^sup>\<circ> \<le> x\<^sup>\<omega> \<squnion> x\<^sup>\<star>"
   by (metis circ_left_unfold mult_1_right omega_induct order_refl)
 
 lemma omega_mult_circ:
   "x\<^sup>\<omega> * x\<^sup>\<circ> = x\<^sup>\<omega>"
   by (metis circ_star omega_mult_star_2)
 
 lemma circ_mult_omega:
   "x\<^sup>\<circ> * x\<^sup>\<omega> = x\<^sup>\<omega>"
   by (metis order.antisym sup_right_divisibility circ_loop_fixpoint circ_plus_sub omega_simulation)
 
 lemma circ_omega_greatest:
   "x\<^sup>\<circ>\<^sup>\<omega> = 1\<^sup>\<omega>"
   by (metis circ_star star_omega_greatest)
 
 lemma omega_circ:
   "x\<^sup>\<omega>\<^sup>\<circ> = 1 \<squnion> x\<^sup>\<omega>"
   by (metis order.antisym circ_left_unfold mult_left_sub_dist_sup_left mult_1_right omega_sub_vector)
 
 end
 
 class bounded_left_omega_algebra = bounded_left_kleene_algebra + left_omega_algebra
 begin
 
 lemma omega_one:
   "1\<^sup>\<omega> = top"
   by (simp add: order.antisym omega_one_greatest)
 
 lemma star_omega_top:
   "x\<^sup>\<star>\<^sup>\<omega> = top"
   by (simp add: star_omega_greatest omega_one)
 
 lemma omega_vector:
   "x\<^sup>\<omega> * top = x\<^sup>\<omega>"
   by (simp add: order.antisym omega_sub_vector top_right_mult_increasing)
 
 lemma mult_top_omega:
   "(x * top)\<^sup>\<omega> \<le> x * top"
   using mult_greatest_omega omega_one by auto
 
 end
 
 sublocale bounded_left_omega_algebra < comb0: bounded_left_conway_semiring where circ = "(\<lambda>x . x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))" ..
 
 class bounded_left_zero_omega_algebra = bounded_left_zero_kleene_algebra + left_zero_omega_algebra
 begin
 
 subclass bounded_left_omega_algebra ..
 
 end
 
 sublocale bounded_left_zero_omega_algebra < comb0: bounded_itering where circ = "(\<lambda>x . x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1))" ..
 
 class bounded_omega_algebra = bounded_kleene_algebra + omega_algebra
 begin
 
 subclass bounded_left_zero_omega_algebra ..
 
 end
 
 class bounded_left_omega_conway_semiring = bounded_left_omega_algebra + left_omega_conway_semiring
 begin
 
 subclass left_kleene_conway_semiring ..
 
 subclass bounded_left_conway_semiring ..
 
 lemma circ_omega:
   "x\<^sup>\<circ>\<^sup>\<omega> = top"
   by (simp add: circ_omega_greatest omega_one)
 
 end
 
 class top_left_omega_algebra = bounded_left_omega_algebra +
   assumes top_left_bot: "top * x = top"
 begin
 
 lemma omega_translate_3:
   "x\<^sup>\<star> * (x\<^sup>\<omega> * bot \<squnion> 1) = x\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> 1)"
   by (metis omega_one omega_vector_greatest top_left_bot mult_assoc)
 
 end
 
 text \<open>Theorem 50.2\<close>
 
 sublocale top_left_omega_algebra < comb4: left_conway_semiring where circ = "(\<lambda>x . x\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> 1))"
   apply unfold_locales
   using comb0.circ_left_unfold omega_translate_3 apply force
   using omega_bot_left_slide omega_translate_3 mult_assoc apply force
   using comb0.circ_sup_1 omega_translate_3 by auto
 
 class top_left_bot_omega_algebra = bounded_left_zero_omega_algebra +
   assumes top_left_bot: "top * x = top"
 begin
 
 lemma omega_translate_2:
   "x\<^sup>\<omega> * bot \<squnion> x\<^sup>\<star> = x\<^sup>\<omega> \<squnion> x\<^sup>\<star>"
   by (metis mult_assoc omega_mult_star_2 star.circ_top top_left_bot)
 
 end
 
 text \<open>Theorem 2.3\<close>
 
 sublocale top_left_bot_omega_algebra < comb3: itering where circ = "(\<lambda>x . x\<^sup>\<omega> \<squnion> x\<^sup>\<star>)"
   apply unfold_locales
   using comb2.circ_slide_1 comb2.circ_sup_1 omega_translate_2 apply force
   apply (metis comb2.circ_mult_1 omega_translate_2)
   using omega_circ_simulate_right_plus omega_translate_2 apply force
   using omega_circ_simulate_left_plus omega_translate_2 by auto
 
 class Omega =
   fixes Omega :: "'a \<Rightarrow> 'a" ("_\<^sup>\<Omega>" [100] 100)
 
 end