# Theory N_Omega_Binary_Iterings

```(* Title:      N-Omega Binary Iterings
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹N-Omega Binary Iterings›

theory N_Omega_Binary_Iterings

imports N_Omega_Algebras Binary_Iterings_Strict

begin

sublocale extended_binary_itering < left_zero_conway_semiring where circ = "(λx . x ⋆ 1)"
apply unfold_locales
using while_left_unfold apply force
apply (metis mult_1_right while_one_mult_below while_slide)

class binary_itering_apx = bounded_binary_itering + n_algebra_apx
begin

lemma C_while_import:
"C (x ⋆ z) = C (C x ⋆ z)"
proof -
have 1: "C x * (x ⋆ z) ≤ C x ⋆ (C x * z)"
using C_mult_propagate while_simulate by force
have "C (x ⋆ z) = C z ⊔ C x * (x ⋆ z)"
by (metis inf_sup_distrib1 n_L_T_meet_mult while_left_unfold)
also have "... ≤ C x ⋆ z"
using 1 by (metis C_decreasing sup_mono while_right_unfold)
finally have "C (x ⋆ z) ≤ C (C x ⋆ z)"
by simp
thus ?thesis
by (metis order.antisym inf.boundedI inf.cobounded1 inf.coboundedI2 inf.sup_monoid.add_commute while_absorb_2 while_increasing)
qed

lemma C_while_preserve:
"C (x ⋆ z) = C (x ⋆ C z)"
proof -
have "C x * (x ⋆ z) ≤ C x ⋆ (C x * z)"
using C_mult_propagate while_simulate by auto
also have "... ≤ x ⋆ (x * C z)"
using C_decreasing n_L_T_meet_mult_propagate while_isotone by blast
finally have 1: "C x * (x ⋆ z) ≤ x ⋆ (x * C z)"
.
have "C (x ⋆ z) = C z ⊔ C x * (x ⋆ z)"
by (metis inf_sup_distrib1 n_L_T_meet_mult while_left_unfold)
also have "... ≤ x ⋆ C z"
using 1 by (meson order.trans le_supI while_increasing while_right_plus_below)
finally have "C (x ⋆ z) ≤ C (x ⋆ C z)"
by simp
thus ?thesis
by (meson order.antisym inf.boundedI inf.cobounded1 inf.coboundedI2 inf.eq_refl while_isotone)
qed

lemma C_while_import_preserve:
"C (x ⋆ z) = C (C x ⋆ C z)"
using C_while_import C_while_preserve by auto

lemma while_L_L:
"L ⋆ L = L"
by (metis n_L_top_L while_mult_star_exchange while_right_top)

lemma while_L_below_sup:
"L ⋆ x ≤ x ⊔ L"
by (metis while_left_unfold sup_right_isotone n_L_below_L)

lemma while_L_split:
"x ⋆ L ≤ (x ⋆ y) ⊔ L"
proof -
have "x ⋆ L ≤ (x ⋆ bot) ⊔ L"
by (metis sup_commute sup_bot_left mult_1_right n_L_split_L while_right_unfold while_simulate_left_plus while_zero)
thus ?thesis
by (metis sup_commute sup_right_isotone order_trans while_right_isotone bot_least)
qed

lemma while_n_while_top_split:
"x ⋆ (n(x ⋆ y) * top) ≤ (x ⋆ bot) ⊔ n(x ⋆ y) * top"
proof -
have "x * n(x ⋆ y) * top ≤ x * bot ⊔ n(x * (x ⋆ y)) * top"
also have "... ≤ n(x ⋆ y) * top ⊔ x * bot"
by (metis sup_commute sup_right_isotone mult_left_isotone n_isotone while_left_plus_below)
finally have "x ⋆ (n(x ⋆ y) * top) ≤ n(x ⋆ y) * top ⊔ (x ⋆ (x * bot))"
by (metis mult_assoc mult_1_right while_simulate_left mult_left_zero while_left_top)
also have "... ≤ (x ⋆ bot) ⊔ n(x ⋆ y) * top"
using sup_left_isotone while_right_plus_below by auto
finally show ?thesis
.
qed

lemma circ_apx_right_isotone:
assumes "x ⊑ y"
shows "z ⋆ x ⊑ z ⋆ y"
proof -
have 1: "x ≤ y ⊔ L ∧ C y ≤ x ⊔ n(x) * top"
using assms apx_def by auto
hence "z ⋆ x ≤ (z ⋆ y) ⊔ (z ⋆ L)"
by (metis while_left_dist_sup while_right_isotone)
hence 2: "z ⋆ x ≤ (z ⋆ y) ⊔ L"
by (meson le_supI order_lesseq_imp sup.cobounded1 while_L_split)
have "z ⋆ (n(z ⋆ x) * top) ≤ (z ⋆ bot) ⊔ n(z ⋆ x) * top"
also have "... ≤ (z ⋆ x) ⊔ n(z ⋆ x) * top"
using sup_left_isotone while_right_isotone by force
finally have 3: "z ⋆ (n(x) * top) ≤ (z ⋆ x) ⊔ n(z ⋆ x) * top"
by (metis mult_left_isotone n_isotone order_trans while_increasing while_right_isotone)
have "C (z ⋆ y) ≤ z ⋆ C y"
by (metis C_while_preserve inf.cobounded2)
also have "... ≤ (z ⋆ x) ⊔ (z ⋆ (n(x) * top))"
using 1 by (metis while_left_dist_sup while_right_isotone)
also have "... ≤ (z ⋆ x) ⊔ n(z ⋆ x) * top"
using 3 by simp
finally show ?thesis
using 2 apx_def by auto
qed

end

class extended_binary_itering_apx = binary_itering_apx + bounded_extended_binary_itering +
assumes n_below_while_zero: "n(x) ≤ n(x ⋆ bot)"
begin

lemma circ_apx_right_isotone:
assumes "x ⊑ y"
shows "x ⋆ z ⊑ y ⋆ z"
proof -
have 1: "x ≤ y ⊔ L ∧ C y ≤ x ⊔ n(x) * top"
using assms apx_def by auto
hence "x ⋆ z ≤ ((y ⋆ 1) * L) ⋆ (y ⋆ z)"
by (metis while_left_isotone while_sumstar_3)
also have "... ≤ (y ⋆ z) ⊔ (y ⋆ 1) * L"
by (metis while_productstar sup_right_isotone mult_right_isotone n_L_below_L while_slide)
also have "... ≤ (y ⋆ z) ⊔ L"
by (meson order.trans le_supI sup.cobounded1 while_L_split while_one_mult_below)
finally have 2: "x ⋆ z ≤ (y ⋆ z) ⊔ L"
.
have "C (y ⋆ z) ≤ C y ⋆ z"
by (metis C_while_import inf.sup_right_divisibility)
also have "... ≤ ((x ⋆ 1) * n(x) * top) ⋆ (x ⋆ z)"
using 1 by (metis while_left_isotone mult_assoc while_sumstar_3)
also have "... ≤ (x ⋆ z) ⊔ (x ⋆ 1) * n(x) * top"
by (metis while_productstar sup_left_top sup_right_isotone mult_assoc mult_left_sub_dist_sup_right while_slide)
also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (n(x) * top))"
using sup_right_isotone while_one_mult_below mult_assoc by auto
also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (n(x ⋆ z) * top))"
by (metis n_below_while_zero bot_least while_right_isotone n_isotone mult_left_isotone sup_right_isotone order_trans)
also have "... ≤ (x ⋆ z) ⊔ n(x ⋆ z) * top"
by (metis sup_assoc sup_right_isotone while_n_while_top_split sup_bot_right while_left_dist_sup)
finally show ?thesis
using 2 apx_def by auto
qed

proposition while_top: "top ⋆ x = L ⊔ top * x" oops
proposition while_one_top: "1 ⋆ x = L ⊔ x" oops
proposition while_unfold_below_1: "x = y * x ⟹ x ≤ y ⋆ 1" oops

proposition while_square_1: "x ⋆ 1 = (x * x) ⋆ (x ⊔ 1)" oops
proposition while_absorb_below_one: "y * x ≤ x ⟹ y ⋆ x ≤ 1 ⋆ x" oops
proposition while_mult_L: "(x * L) ⋆ z = z ⊔ x * L" oops
proposition tarski_top_omega_below_2: "x * L ≤ (x * L) ⋆ bot" oops
proposition tarski_top_omega_2: "x * L = (x * L) ⋆ bot" oops
proposition while_separate_right_plus: "y * x ≤ x * (x ⋆ (1 ⊔ y)) ⊔ 1 ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)" oops
proposition "y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1) ⟹ (x ⊔ y) ⋆ 1 = x ⋆ (y ⋆ 1)" oops
proposition "y * x ≤ (1 ⊔ x) * (y ⋆ 1) ⟹ (x ⊔ y) ⋆ 1 = x ⋆ (y ⋆ 1)" oops

end

class n_omega_algebra_binary = n_omega_algebra + while +
assumes while_def: "x ⋆ y = n(x⇧ω) * L ⊔ x⇧⋆ * y"
begin

lemma while_omega_inf_L_star:
"x ⋆ y = (x⇧ω ⊓ L) ⊔ x⇧⋆ * y"
by (metis loop_semantics_kappa_mu_nu loop_semantics_kappa_mu_nu_2 while_def)

lemma while_one_mult_while_below_1:
"(y ⋆ 1) * (y ⋆ v) ≤ y ⋆ v"
proof -
have "(y ⋆ 1) * (y ⋆ v) ≤ y ⋆ (y ⋆ v)"
by (smt sup_left_isotone mult_assoc mult_right_dist_sup mult_right_isotone n_L_below_L while_def mult_left_one)
also have "... = n(y⇧ω) * L ⊔ y⇧⋆ * n(y⇧ω) * L ⊔ y⇧⋆ * y⇧⋆ * v"
by (simp add: mult_left_dist_sup sup_assoc while_def mult_assoc)
also have "... = n(y⇧ω) * L ⊔ (y⇧⋆ * y⇧⋆ * bot ⊔ y⇧⋆ * n(y⇧ω) * L) ⊔ y⇧⋆ * y⇧⋆ * v"
by (metis mult_left_dist_sup star.circ_transitive_equal sup_bot_left mult_assoc)
also have "... = n(y⇧ω) * L ⊔ (y⇧⋆ * y⇧⋆ * bot ⊔ n(y⇧⋆ * y⇧ω) * L) ⊔ y⇧⋆ * y⇧⋆ * v"
also have "... = n(y⇧ω) * L ⊔ n(y⇧⋆ * y⇧ω) * L ⊔ y⇧⋆ * y⇧⋆ * v"
by (smt (z3) mult_left_dist_sup sup.left_commute sup_bot_left sup_commute)
finally show ?thesis
by (simp add: star.circ_transitive_equal star_mult_omega while_def)
qed

lemma star_below_while:
"x⇧⋆ * y ≤ x ⋆ y"

subclass bounded_binary_itering
proof unfold_locales
fix x y z
have "z ⊔ x * ((y * x) ⋆ (y * z)) = x * (y * x)⇧⋆ * y * z ⊔ x * n((y * x)⇧ω) * L ⊔ z"
using mult_left_dist_sup sup_commute while_def mult_assoc by auto
also have "... = x * (y * x)⇧⋆ * y * z ⊔ n(x * (y * x)⇧ω) * L ⊔ z"
by (metis mult_assoc mult_right_isotone bot_least n_mult_omega_L_star_zero sup_relative_same_increasing)
also have "... = (x * y)⇧⋆ * z ⊔ n(x * (y * x)⇧ω) * L"
by (smt sup_assoc sup_commute mult_assoc star.circ_loop_fixpoint star_slide)
also have "... = (x * y) ⋆ z"
finally show "(x * y) ⋆ z = z ⊔ x * ((y * x) ⋆ (y * z))"
by simp
next
fix x y z
have "(x ⋆ y) ⋆ (x ⋆ z) = n((n(x⇧ω) * L ⊔ x⇧⋆ * y)⇧ω) * L ⊔ (n(x⇧ω) * L ⊔ x⇧⋆ * y)⇧⋆ * (x ⋆ z)"
also have "... = n((x⇧⋆ * y)⇧ω ⊔ (x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L) * L ⊔ ((x⇧⋆ * y)⇧⋆ ⊔ (x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L) * (x ⋆ z)"
using mult_L_sup_omega mult_L_sup_star by force
also have "... = n((x⇧⋆ * y)⇧ω) * L ⊔ n((x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L) * L ⊔ (x⇧⋆ * y)⇧⋆ * (x ⋆ z) ⊔ (x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L * (x ⋆ z)"
by (simp add: mult_right_dist_sup n_dist_omega_star sup_assoc mult_assoc)
also have "... = n((x⇧⋆ * y)⇧ω) * L ⊔ n((x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L) * L ⊔ (x⇧⋆ * y)⇧⋆ * bot ⊔ (x⇧⋆ * y)⇧⋆ * (x ⋆ z) ⊔ (x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L * (x ⋆ z)"
by (smt sup_assoc sup_bot_left mult_left_dist_sup)
also have "... = n((x⇧⋆ * y)⇧ω) * L ⊔ ((x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L * (x ⋆ z) ⊔ (x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L ⊔ (x⇧⋆ * y)⇧⋆ * (x ⋆ z))"
by (smt n_n_L_split_n_n_L_L sup_commute sup_assoc)
also have "... = n((x⇧⋆ * y)⇧ω) * L ⊔ ((x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L ⊔ (x⇧⋆ * y)⇧⋆ * (x ⋆ z))"
by (smt mult_L_omega omega_sub_vector le_iff_sup)
also have "... = n((x⇧⋆ * y)⇧ω) * L ⊔ (x⇧⋆ * y)⇧⋆ * (x ⋆ z)"
using mult_left_sub_dist_sup_left sup_absorb2 while_def mult_assoc by auto
also have "... = (x⇧⋆ * y)⇧⋆ * x⇧⋆ * z ⊔ (x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L ⊔ n((x⇧⋆ * y)⇧ω) * L"
by (simp add: mult_left_dist_sup sup_commute while_def mult_assoc)
also have "... = (x⇧⋆ * y)⇧⋆ * x⇧⋆ * z ⊔ n((x⇧⋆ * y)⇧⋆ * x⇧ω) * L ⊔ n((x⇧⋆ * y)⇧ω) * L"
by (metis sup_bot_right mult_left_dist_sup sup_assoc n_mult_omega_L_star_zero)
also have "... = (x ⊔ y) ⋆ z"
using n_dist_omega_star omega_decompose semiring.combine_common_factor star.circ_sup_9 sup_commute while_def by force
finally show "(x ⊔ y) ⋆ z = (x ⋆ y) ⋆ (x ⋆ z)"
by simp
next
fix x y z
show "x ⋆ (y ⊔ z) = (x ⋆ y) ⊔ (x ⋆ z)"
using semiring.distrib_left sup_assoc sup_commute while_def by force
next
fix x y z
show "(x ⋆ y) * z ≤ x ⋆ (y * z)"
by (smt sup_left_isotone mult_assoc mult_right_dist_sup mult_right_isotone n_L_below_L while_def)
next
fix v w x y z
show "x * z ≤ z * (y ⋆ 1) ⊔ w ⟶ x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ (w * (y ⋆ v)))"
proof
assume 1: "x * z ≤ z * (y ⋆ 1) ⊔ w"
have "z * v ⊔ x * (z * (y ⋆ v) ⊔ x⇧⋆ * (w * (y ⋆ v))) ≤ z * v ⊔ x * z * (y ⋆ v) ⊔ x⇧⋆ * (w * (y ⋆ v))"
by (metis sup_assoc sup_right_isotone mult_assoc mult_left_dist_sup mult_left_isotone star.left_plus_below_circ)
also have "... ≤ z * v ⊔ z * (y ⋆ 1) * (y ⋆ v) ⊔ w * (y ⋆ v) ⊔ x⇧⋆ * (w * (y ⋆ v))"
using 1 by (metis sup_assoc sup_left_isotone sup_right_isotone mult_left_isotone mult_right_dist_sup)
also have "... ≤ z * v ⊔ z * (y ⋆ v) ⊔ x⇧⋆ * (w * (y ⋆ v))"
by (smt (verit, ccfv_threshold) sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup star.circ_loop_fixpoint while_one_mult_while_below_1 le_supE le_supI)
also have "... = z * (y ⋆ v) ⊔ x⇧⋆ * (w * (y ⋆ v))"
by (metis le_iff_sup le_supE mult_right_isotone star.circ_loop_fixpoint star_below_while)
finally have "x⇧⋆ * z * v ≤ z * (y ⋆ v) ⊔ x⇧⋆ * (w * (y ⋆ v))"
using star_left_induct mult_assoc by auto
thus "x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ (w * (y ⋆ v)))"
by (smt sup_assoc sup_commute sup_right_isotone mult_assoc while_def)
qed
next
fix v w x y z
show "z * x ≤ y * (y ⋆ z) ⊔ w ⟶ z * (x ⋆ v) ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
proof
assume "z * x ≤ y * (y ⋆ z) ⊔ w"
hence 1: "z * x ≤ y * y⇧⋆ * z ⊔ (y * n(y⇧ω) * L ⊔ w)"
by (simp add: mult_left_dist_sup sup.left_commute sup_commute while_def mult_assoc)
hence "z * x⇧⋆ ≤ y⇧⋆ * (z ⊔ (y * n(y⇧ω) * L ⊔ w) * x⇧⋆)"
also have "... = y⇧⋆ * z ⊔ y⇧⋆ * y * n(y⇧ω) * L ⊔ y⇧⋆ * w * x⇧⋆"
also have "... = y⇧⋆ * z ⊔ n(y⇧⋆ * y * y⇧ω) * L ⊔ y⇧⋆ * w * x⇧⋆"
by (metis sup_relative_same_increasing mult_isotone n_mult_omega_L_star_zero star.left_plus_below_circ star.right_plus_circ bot_least)
also have "... = n(y⇧ω) * L ⊔ y⇧⋆ * z ⊔ y⇧⋆ * w * x⇧⋆"
using omega_unfold star_mult_omega sup_commute mult_assoc by force
finally have "z * x⇧⋆ * v ≤ n(y⇧ω) * L * v ⊔ y⇧⋆ * z * v ⊔ y⇧⋆ * w * x⇧⋆ * v"
by (smt le_iff_sup mult_right_dist_sup)
also have "... ≤ n(y⇧ω) * L ⊔ y⇧⋆ * (z * v ⊔ w * x⇧⋆ * v)"
by (metis n_L_below_L mult_assoc mult_right_isotone sup_left_isotone mult_left_dist_sup sup_assoc)
also have "... ≤ n(y⇧ω) * L ⊔ y⇧⋆ * (z * v ⊔ w * (x ⋆ v))"
using mult_right_isotone semiring.add_left_mono mult_assoc star_below_while by auto
finally have 2: "z * x⇧⋆ * v ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
have 3: "y⇧⋆ * y * y⇧⋆ * bot ≤ y⇧⋆ * w * x⇧ω"
by (metis sup_commute sup_bot_left mult_assoc mult_left_sub_dist_sup_left star.circ_loop_fixpoint star.circ_transitive_equal)
have "z * x⇧ω ≤ y * y⇧⋆ * z * x⇧ω ⊔ (y * n(y⇧ω) * L ⊔ w) * x⇧ω"
using 1 by (metis mult_assoc mult_left_isotone mult_right_dist_sup omega_unfold)
hence "z * x⇧ω ≤ y⇧ω ⊔ y⇧⋆ * y * n(y⇧ω) * L * x⇧ω ⊔ y⇧⋆ * w * x⇧ω"
by (smt sup_assoc sup_commute left_plus_omega mult_assoc mult_left_dist_sup mult_right_dist_sup omega_induct star.left_plus_circ)
also have "... ≤ y⇧ω ⊔ y⇧⋆ * y * n(y⇧ω) * L ⊔ y⇧⋆ * w * x⇧ω"
by (metis sup_left_isotone sup_right_isotone mult_assoc mult_right_isotone n_L_below_L)
also have "... = y⇧ω ⊔ n(y⇧⋆ * y * y⇧ω) * L ⊔ y⇧⋆ * w * x⇧ω"
using 3 by (smt sup_assoc sup_commute sup_relative_same_increasing n_mult_omega_L_star_zero)
also have "... = y⇧ω ⊔ y⇧⋆ * w * x⇧ω"
by (metis mult_assoc omega_unfold star_mult_omega sup_commute le_iff_sup n_L_decreasing)
finally have "n(z * x⇧ω) * L ≤ n(y⇧ω) * L ⊔ n(y⇧⋆ * w * x⇧ω) * L"
by (metis mult_assoc mult_left_isotone mult_right_dist_sup n_dist_omega_star n_isotone)
also have "... ≤ n(y⇧ω) * L ⊔ y⇧⋆ * (w * (n(x⇧ω) * L ⊔ x⇧⋆ * bot))"
by (smt sup_commute sup_right_isotone mult_assoc mult_left_dist_sup n_mult_omega_L_below_zero)
also have "... ≤ n(y⇧ω) * L ⊔ y⇧⋆ * (w * (n(x⇧ω) * L ⊔ x⇧⋆ * v))"
by (metis sup_right_isotone mult_right_isotone bot_least)
also have "... ≤ n(y⇧ω) * L ⊔ y⇧⋆ * (z * v ⊔ w * (n(x⇧ω) * L ⊔ x⇧⋆ * v))"
using mult_left_sub_dist_sup_right sup_right_isotone by auto
finally have 4: "n(z * x⇧ω) * L ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
using while_def by auto
have "z * (x ⋆ v) = z * n(x⇧ω) * L ⊔ z * x⇧⋆ * v"
by (simp add: mult_left_dist_sup while_def mult_assoc)
also have "... = n(z * x⇧ω) * L ⊔ z * x⇧⋆ * v"
by (metis sup_commute sup_relative_same_increasing mult_right_isotone n_mult_omega_L_star_zero bot_least)
finally show "z * (x ⋆ v) ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
using 2 4 by simp
qed
qed

lemma while_top:
"top ⋆ x = L ⊔ top * x"
by (metis n_top_L star.circ_top star_omega_top while_def)

lemma while_one_top:
"1 ⋆ x = L ⊔ x"
by (smt mult_left_one n_top_L omega_one star_one while_def)

lemma while_finite_associative:
"x⇧ω = bot ⟹ (x ⋆ y) * z = x ⋆ (y * z)"
by (metis sup_bot_left mult_assoc n_zero_L_zero while_def)

lemma while_while_one:
"y ⋆ (x ⋆ 1) = n(y⇧ω) * L ⊔ y⇧⋆ * n(x⇧ω) * L ⊔ y⇧⋆ * x⇧⋆"
by (simp add: mult_left_dist_sup sup_assoc while_def mult_assoc)

text ‹AACP Theorem 8.17›

subclass bounded_extended_binary_itering
proof unfold_locales
fix w x y z
have "w * (x ⋆ y * z) = n(w * n(x⇧ω) * L) * L ⊔ w * x⇧⋆ * y * z"
by (smt sup_assoc sup_commute sup_bot_left mult_assoc mult_left_dist_sup n_n_L_split_n_n_L_L while_def)
also have "... ≤ n((w * n(x⇧ω) * L)⇧ω) * L ⊔ w * x⇧⋆ * y * z"
also have "... ≤ n((w * (x ⋆ y))⇧ω) * L ⊔ w * x⇧⋆ * y * z"
by (smt sup_left_isotone sup_ge1 mult_assoc mult_left_isotone mult_right_isotone n_isotone omega_isotone while_def)
also have "... ≤ n((w * (x ⋆ y))⇧ω) * L ⊔ w * (x ⋆ y) * z"
by (metis star_below_while mult_assoc mult_left_isotone mult_right_isotone sup_right_isotone)
also have "... ≤ n((w * (x ⋆ y))⇧ω) * L ⊔ (w * (x ⋆ y))⇧⋆ * (w * (x ⋆ y) * z)"
using sup.boundedI sup.cobounded1 while_def while_increasing by auto
finally show "w * (x ⋆ y * z) ≤ (w * (x ⋆ y)) ⋆ (w * (x ⋆ y) * z)"
using while_def by auto
qed

subclass extended_binary_itering_apx
apply unfold_locales
by (metis n_below_n_omega n_left_upper_bound n_n_L order_trans while_def)

lemma while_simulate_4_plus:
assumes "y * x ≤ x * (x ⋆ (1 ⊔ y))"
shows "y * x * x⇧⋆ ≤ x * (x ⋆ (1 ⊔ y))"
proof -
have "x * (x ⋆ (1 ⊔ y)) = x * n(x⇧ω) * L ⊔ x * x⇧⋆ * (1 ⊔ y)"
by (simp add: mult_left_dist_sup while_def mult_assoc)
also have "... = n(x * x⇧ω) * L ⊔ x * x⇧⋆ * (1 ⊔ y)"
by (smt n_mult_omega_L_star_zero sup_relative_same_increasing sup_commute sup_bot_right mult_left_sub_dist_sup_right)
finally have 1: "x * (x ⋆ (1 ⊔ y)) = n(x⇧ω) * L ⊔ x * x⇧⋆ ⊔ x * x⇧⋆ * y"
using mult_left_dist_sup omega_unfold sup_assoc by force
hence "x * x⇧⋆ * y * x ≤ x * x⇧⋆ * n(x⇧ω) * L ⊔ x * x⇧⋆ * x⇧⋆ * x ⊔ x * x⇧⋆ * x * x⇧⋆ * y"
by (metis assms mult_assoc mult_right_isotone mult_left_dist_sup star_plus)
also have "... = n(x * x⇧⋆ * x⇧ω) * L ⊔ x * x⇧⋆ * x⇧⋆ * x ⊔ x * x⇧⋆ * x * x⇧⋆ * y"
by (smt (z3) sup_commute n_mult_omega_L_star omega_unfold semiring.distrib_left star_plus mult_assoc)
also have "... = n(x⇧ω) * L ⊔ x * x⇧⋆ * x ⊔ x * x * x⇧⋆ * y"
using omega_unfold star.circ_plus_same star.circ_transitive_equal star_mult_omega mult_assoc by auto
also have "... ≤ n(x⇧ω) * L ⊔ x * x⇧⋆ ⊔ x * x⇧⋆ * y"
by (smt sup_assoc sup_ge2 le_iff_sup mult_assoc mult_right_dist_sup star.circ_increasing star.circ_plus_same star.circ_transitive_equal)
finally have 2: "x * x⇧⋆ * y * x ≤ n(x⇧ω) * L ⊔ x * x⇧⋆ ⊔ x * x⇧⋆ * y"
.
have "(n(x⇧ω) * L ⊔ x * x⇧⋆ ⊔ x * x⇧⋆ * y) * x ≤ n(x⇧ω) * L ⊔ x * x⇧⋆ * x ⊔ x * x⇧⋆ * y * x"
by (metis mult_right_dist_sup n_L_below_L mult_assoc mult_right_isotone sup_left_isotone)
also have "... ≤ n(x⇧ω) * L ⊔ x * x⇧⋆ ⊔ x * x⇧⋆ * y * x"
by (smt sup_commute sup_left_isotone mult_assoc mult_right_isotone star.left_plus_below_circ star_plus)
also have "... ≤ n(x⇧ω) * L ⊔ x * x⇧⋆ ⊔ x * x⇧⋆ * y"
using 2 by simp
finally show ?thesis
using 1 assms star_right_induct by force
qed

lemma while_simulate_4_omega:
assumes "y * x ≤ x * (x ⋆ (1 ⊔ y))"
shows "y * x⇧ω ≤ x⇧ω"
proof -
have "x * (x ⋆ (1 ⊔ y)) = x * n(x⇧ω) * L ⊔ x * x⇧⋆ * (1 ⊔ y)"
using mult_left_dist_sup while_def mult_assoc by auto
also have "... = n(x * x⇧ω) * L ⊔ x * x⇧⋆ * (1 ⊔ y)"
by (smt (z3) mult_1_right mult_left_sub_dist_sup_left n_mult_omega_L_star sup_commute sup_relative_same_increasing)
finally have "x * (x ⋆ (1 ⊔ y)) = n(x⇧ω) * L ⊔ x * x⇧⋆ ⊔ x * x⇧⋆ * y"
using mult_left_dist_sup omega_unfold sup_assoc by force
hence "y * x⇧ω ≤ n(x⇧ω) * L * x⇧ω ⊔ x * x⇧⋆ * x⇧ω ⊔ x * x⇧⋆ * y * x⇧ω"
by (smt assms le_iff_sup mult_assoc mult_right_dist_sup omega_unfold)
also have "... ≤ x * x⇧⋆ * (y * x⇧ω) ⊔ x⇧ω"
by (metis sup_left_isotone mult_L_omega omega_sub_vector mult_assoc omega_unfold star_mult_omega n_L_decreasing le_iff_sup sup_commute)
finally have "y * x⇧ω ≤ (x * x⇧⋆)⇧ω ⊔ (x * x⇧⋆)⇧⋆ * x⇧ω"
thus ?thesis
by (metis sup_idem left_plus_omega star_mult_omega)
qed

lemma while_square_1:
"x ⋆ 1 = (x * x) ⋆ (x ⊔ 1)"
by (metis mult_1_right omega_square star_square_2 while_def)

lemma while_absorb_below_one:
"y * x ≤ x ⟹ y ⋆ x ≤ 1 ⋆ x"
by (metis star_left_induct_mult sup_mono n_galois n_sub_nL while_def while_one_top)

lemma while_mult_L:
"(x * L) ⋆ z = z ⊔ x * L"
by (metis sup_bot_right mult_left_zero while_denest_5 while_one_top while_productstar while_sumstar)

lemma tarski_top_omega_below_2:
"x * L ≤ (x * L) ⋆ bot"

lemma tarski_top_omega_2:
"x * L = (x * L) ⋆ bot"

proposition while_sub_mult_one: "x * (1 ⋆ y) ≤ 1 ⋆ x" nitpick [expect=genuine,card=3] oops
proposition while_unfold_below: "x = z ⊔ y * x ⟶ x ≤ y ⋆ z" nitpick [expect=genuine,card=2] oops
proposition while_loop_is_greatest_postfixpoint: "is_greatest_postfixpoint (λx . y * x ⊔ z) (y ⋆ z)" nitpick [expect=genuine,card=2] oops
proposition while_loop_is_greatest_fixpoint: "is_greatest_fixpoint (λx . y * x ⊔ z) (y ⋆ z)" nitpick [expect=genuine,card=2] oops
proposition while_denest_3: "(x ⋆ w) ⋆ x⇧ω = (x ⋆ w)⇧ω" nitpick [expect=genuine,card=2] oops
proposition while_mult_top: "(x * top) ⋆ z = z ⊔ x * top" nitpick [expect=genuine,card=2] oops
proposition tarski_below_top_omega: "x ≤ (x * L)⇧ω" nitpick [expect=genuine,card=2] oops
proposition tarski_mult_omega_omega: "(x * y⇧ω)⇧ω = x * y⇧ω" nitpick [expect=genuine,card=3] oops
proposition tarski_below_top_omega_2: "x ≤ (x * L) ⋆ bot" nitpick [expect=genuine,card=2] oops
proposition "1 = (x * bot) ⋆ 1" nitpick [expect=genuine,card=3] oops
proposition tarski: "x = bot ∨ top * x * top = top" nitpick [expect=genuine,card=3] oops
proposition "(x ⊔ y) ⋆ z = ((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z)" nitpick [expect=genuine,card=2] oops
proposition while_top_2: "top ⋆ z = top * z" nitpick [expect=genuine,card=2] oops
proposition while_mult_top_2: "(x * top) ⋆ z = z ⊔ x * top * z" nitpick [expect=genuine,card=2] oops
proposition while_one_mult: "(x ⋆ 1) * x = x ⋆ x" nitpick [expect=genuine,card=4] oops
proposition "(x ⋆ 1) * y = x ⋆ y" nitpick [expect=genuine,card=2] oops
proposition while_associative: "(x ⋆ y) * z = x ⋆ (y * z)" nitpick [expect=genuine,card=2] oops
proposition while_back_loop_is_fixpoint: "is_fixpoint (λx . x * y ⊔ z) (z * (y ⋆ 1))" nitpick [expect=genuine,card=4] oops
proposition "1 ⊔ x * bot = x ⋆ 1" nitpick [expect=genuine,card=3] oops
proposition "x = x * (x ⋆ 1)" nitpick [expect=genuine,card=3] oops
proposition "x * (x ⋆ 1) = x ⋆ 1" nitpick [expect=genuine,card=2] oops
proposition "x ⋆ 1 = x ⋆ (1 ⋆ 1)" nitpick [expect=genuine,card=3] oops
proposition "(x ⊔ y) ⋆ 1 = (x ⋆ (y ⋆ 1)) ⋆ 1" nitpick [expect=genuine,card=3] oops
proposition "z ⊔ y * x = x ⟹ y ⋆ z ≤ x" nitpick [expect=genuine,card=2] oops
proposition "y * x = x ⟹ y ⋆ x ≤ x" nitpick [expect=genuine,card=2] oops
proposition "z ⊔ x * y = x ⟹ z * (y ⋆ 1) ≤ x" nitpick [expect=genuine,card=3] oops
proposition "x * y = x ⟹ x * (y ⋆ 1) ≤ x" nitpick [expect=genuine,card=3] oops
proposition "x * z = z * y ⟹ x ⋆ z ≤ z * (y ⋆ 1)" nitpick [expect=genuine,card=2] oops

proposition while_unfold_below_1: "x = y * x ⟹ x ≤ y ⋆ 1" nitpick [expect=genuine,card=3] oops
proposition "x⇧ω ≤ x⇧ω * x⇧ω" oops
proposition tarski_omega_idempotent: "x⇧ω⇧ω = x⇧ω" oops

end

class n_omega_algebra_binary_strict = n_omega_algebra_binary + circ +
assumes L_left_zero: "L * x = L"
assumes circ_def: "x⇧∘ = n(x⇧ω) * L ⊔ x⇧⋆"
begin

subclass strict_binary_itering
apply unfold_locales
apply (metis while_def mult_assoc L_left_zero mult_right_dist_sup)
by (metis circ_def while_def mult_1_right)

end

end

```