# Theory Binary_Iterings

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

section ‹Binary Iterings›

theory Binary_Iterings

imports Base

begin

class binary_itering = idempotent_left_zero_semiring + while +
assumes while_productstar: "(x * y) ⋆ z = z ⊔ x * ((y * x) ⋆ (y * z))"
assumes while_sumstar: "(x ⊔ y) ⋆ z = (x ⋆ y) ⋆ (x ⋆ z)"
assumes while_left_dist_sup: "x ⋆ (y ⊔ z) = (x ⋆ y) ⊔ (x ⋆ z)"
assumes while_sub_associative: "(x ⋆ y) * z ≤ x ⋆ (y * z)"
assumes while_simulate_left_plus: "x * z ≤ z * (y ⋆ 1) ⊔ w ⟶ x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ (w * (y ⋆ v)))"
assumes while_simulate_right_plus: "z * x ≤ y * (y ⋆ z) ⊔ w ⟶ z * (x ⋆ v) ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
begin

text ‹Theorem 9.1›

lemma while_zero:
"bot ⋆ x = x"
by (metis sup_bot_right mult_left_zero while_productstar)

text ‹Theorem 9.4›

lemma while_mult_increasing:
"x * y ≤ x ⋆ y"
by (metis le_supI2 mult.left_neutral mult_left_sub_dist_sup_left while_productstar)

text ‹Theorem 9.2›

lemma while_one_increasing:
"x ≤ x ⋆ 1"
by (metis mult.right_neutral while_mult_increasing)

text ‹Theorem 9.3›

lemma while_increasing:
"y ≤ x ⋆ y"
by (metis sup_left_divisibility mult_left_one while_productstar)

text ‹Theorem 9.42›

lemma while_right_isotone:
"y ≤ z ⟹ x ⋆ y ≤ x ⋆ z"
by (metis le_iff_sup while_left_dist_sup)

text ‹Theorem 9.41›

lemma while_left_isotone:
"x ≤ y ⟹ x ⋆ z ≤ y ⋆ z"
using sup_left_divisibility while_sumstar while_increasing by auto

lemma while_isotone:
"w ≤ x ⟹ y ≤ z ⟹ w ⋆ y ≤ x ⋆ z"
by (meson order_lesseq_imp while_left_isotone while_right_isotone)

text ‹Theorem 9.17›

lemma while_left_unfold:
"x ⋆ y = y ⊔ x * (x ⋆ y)"
by (metis mult_1_left mult_1_right while_productstar)

lemma while_simulate_left_plus_1:
"x * z ≤ z * (y ⋆ 1) ⟹ x ⋆ (z * w) ≤ z * (y ⋆ w) ⊔ (x ⋆ bot)"
by (metis sup_bot_right mult_left_zero while_simulate_left_plus)

text ‹Theorem 11.1›

lemma while_simulate_absorb:
"y * x ≤ x ⟹ y ⋆ x ≤ x ⊔ (y ⋆ bot)"
by (metis while_simulate_left_plus_1 while_zero mult_1_right)

text ‹Theorem 9.10›

lemma while_transitive:
"x ⋆ (x ⋆ y) = x ⋆ y"
by (metis order.eq_iff sup_bot_right sup_ge2 while_left_dist_sup while_increasing while_left_unfold while_simulate_absorb)

text ‹Theorem 9.25›

lemma while_slide:
"(x * y) ⋆ (x * z) = x * ((y * x) ⋆ z)"
by (metis mult_left_dist_sup while_productstar mult_assoc while_left_unfold)

text ‹Theorem 9.21›

lemma while_zero_2:
"(x * bot) ⋆ y = x * bot ⊔ y"
by (metis mult_left_zero sup_commute mult_assoc while_left_unfold)

text ‹Theorem 9.5›

lemma while_mult_star_exchange:
"x * (x ⋆ y) = x ⋆ (x * y)"
by (metis mult_left_one while_slide)

text ‹Theorem 9.18›

lemma while_right_unfold:
"x ⋆ y = y ⊔ (x ⋆ (x * y))"
by (metis while_left_unfold while_mult_star_exchange)

text ‹Theorem 9.7›

lemma while_one_mult_below:
"(x ⋆ 1) * y ≤ x ⋆ y"
by (metis mult_left_one while_sub_associative)

lemma while_plus_one:
"x ⋆ y = y ⊔ (x ⋆ y)"

text ‹Theorem 9.19›

lemma while_rtc_2:
"y ⊔ x * y ⊔ (x ⋆ (x ⋆ y)) = x ⋆ y"
by (simp add: sup_absorb2 while_increasing while_mult_increasing while_transitive)

text ‹Theorem 9.6›

lemma while_left_plus_below:
"x * (x ⋆ y) ≤ x ⋆ y"
by (metis sup_right_divisibility while_left_unfold)

lemma while_right_plus_below:
"x ⋆ (x * y) ≤ x ⋆ y"
using while_left_plus_below while_mult_star_exchange by auto

lemma while_right_plus_below_2:
"(x ⋆ x) * y ≤ x ⋆ y"
by (smt order_trans while_right_plus_below while_sub_associative)

text ‹Theorem 9.47›

lemma while_mult_transitive:
"x ≤ z ⋆ y ⟹ y ≤ z ⋆ w ⟹ x ≤ z ⋆ w"
by (smt order_trans while_right_isotone while_transitive)

text ‹Theorem 9.48›

lemma while_mult_upper_bound:
"x ≤ z ⋆ 1 ⟹ y ≤ z ⋆ w ⟹ x * y ≤ z ⋆ w"
by (metis order.trans mult_isotone while_one_mult_below while_transitive)

lemma while_one_mult_while_below:
"(y ⋆ 1) * (y ⋆ v) ≤ y ⋆ v"

text ‹Theorem 9.34›

lemma while_sub_dist:
"x ⋆ z ≤ (x ⊔ y) ⋆ z"

lemma while_sub_dist_1:
"x * z ≤ (x ⊔ y) ⋆ z"
using order.trans while_mult_increasing while_sub_dist by blast

lemma while_sub_dist_2:
"x * y * z ≤ (x ⊔ y) ⋆ z"
by (metis sup_commute mult_assoc while_mult_transitive while_sub_dist_1)

text ‹Theorem 9.36›

lemma while_sub_dist_3:
"x ⋆ (y ⋆ z) ≤ (x ⊔ y) ⋆ z"
by (metis sup_commute while_mult_transitive while_sub_dist)

text ‹Theorem 9.44›

lemma while_absorb_2:
"x ≤ y ⟹ y ⋆ (x ⋆ z) = y ⋆ z"
using sup_left_divisibility while_sumstar while_transitive by auto

lemma while_simulate_right_plus_1:
"z * x ≤ y * (y ⋆ z) ⟹ z * (x ⋆ w) ≤ y ⋆ (z * w)"
by (metis sup_bot_right mult_left_zero while_simulate_right_plus)

text ‹Theorem 9.39›

lemma while_sumstar_1_below:
"x ⋆ ((y * (x ⋆ 1)) ⋆ z) ≤ ((x ⋆ 1) * y) ⋆ (x ⋆ z)"
proof -
have 1: "x * (((x ⋆ 1) * y) ⋆ (x ⋆ z)) ≤ ((x ⋆ 1) * y) ⋆ (x ⋆ z)"
by (smt sup_mono sup_ge2 mult_assoc mult_left_dist_sup mult_right_sub_dist_sup_right while_left_unfold)
have "x ⋆ ((y * (x ⋆ 1)) ⋆ z) ≤ (x ⋆ z) ⊔ (x ⋆ (y * (((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z))))"
by (metis eq_refl while_left_dist_sup while_productstar)
also have "... ≤ (x ⋆ z) ⊔ (x ⋆ ((x ⋆ 1) * y * (((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z))))"
by (metis sup_right_isotone mult_assoc mult_left_one mult_right_sub_dist_sup_left while_left_unfold while_right_isotone)
also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z)))"
using semiring.add_left_mono while_left_plus_below while_right_isotone by blast
also have "... ≤ x ⋆ (((x ⋆ 1) * y) ⋆ (x ⋆ z))"
by (meson order.trans le_supI while_increasing while_one_mult_below while_right_isotone)
also have "... ≤ (((x ⋆ 1) * y) ⋆ (x ⋆ z)) ⊔ (x ⋆ bot)"
using 1 while_simulate_absorb by auto
also have "... = ((x ⋆ 1) * y) ⋆ (x ⋆ z)"
by (smt sup_assoc sup_commute sup_bot_left while_left_dist_sup while_left_unfold)
finally show ?thesis
.
qed

lemma while_sumstar_2_below:
"((x ⋆ 1) * y) ⋆ (x ⋆ z) ≤ (x ⋆ y) ⋆ (x ⋆ z)"

text ‹Theorem 9.38›

lemma while_sup_1_below:
"x ⋆ ((y * (x ⋆ 1)) ⋆ z) ≤ (x ⊔ y) ⋆ z"
proof -
have "((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z) ≤ (x ⊔ y) ⋆ z"
using while_sumstar while_isotone while_one_mult_below by auto
hence "(y * (x ⋆ 1)) ⋆ z ≤ z ⊔ y * ((x ⊔ y) ⋆ z)"
by (metis sup_right_isotone mult_right_isotone while_productstar)
also have "... ≤ (x ⊔ y) ⋆ z"
by (metis sup_right_isotone sup_ge2 mult_left_isotone while_left_unfold)
finally show ?thesis
using while_mult_transitive while_sub_dist by blast
qed

text ‹Theorem 9.16›

lemma while_while_while:
"((x ⋆ 1) ⋆ 1) ⋆ y = (x ⋆ 1) ⋆ y"
by (smt (z3) sup.absorb1 while_sumstar while_absorb_2 while_increasing while_one_increasing)

lemma while_one:
"(1 ⋆ 1) ⋆ y = 1 ⋆ y"
by (metis while_while_while while_zero)

text ‹Theorem 9.22›

lemma while_sup_below:
"x ⊔ y ≤ x ⋆ (y ⋆ 1)"
by (metis le_supI le_supI1 while_left_dist_sup while_left_unfold while_one_increasing)

text ‹Theorem 9.32›

lemma while_sup_2:
"(x ⊔ y) ⋆ z ≤ (x ⋆ (y ⋆ 1)) ⋆ z"
using while_left_isotone while_sup_below by auto

text ‹Theorem 9.45›

lemma while_sup_one_left_unfold:
"1 ≤ x ⟹ x * (x ⋆ y) = x ⋆ y"
by (metis order.antisym mult_1_left mult_left_isotone while_left_plus_below)

lemma while_sup_one_right_unfold:
"1 ≤ x ⟹ x ⋆ (x * y) = x ⋆ y"
using while_mult_star_exchange while_sup_one_left_unfold by auto

text ‹Theorem 9.30›

lemma while_decompose_7:
"(x ⊔ y) ⋆ z = x ⋆ (y ⋆ ((x ⊔ y) ⋆ z))"
by (metis order.eq_iff order_trans while_increasing while_sub_dist_3 while_transitive)

text ‹Theorem 9.31›

lemma while_decompose_8:
"(x ⊔ y) ⋆ z = (x ⊔ y) ⋆ (x ⋆ (y ⋆ z))"
using while_absorb_2 by auto

text ‹Theorem 9.27›

lemma while_decompose_9:
"(x ⋆ (y ⋆ 1)) ⋆ z = x ⋆ (y ⋆ ((x ⋆ (y ⋆ 1)) ⋆ z))"
by (smt sup_commute le_iff_sup order_trans while_sup_below while_increasing while_sub_dist_3)

lemma while_decompose_10:
"(x ⋆ (y ⋆ 1)) ⋆ z = (x ⋆ (y ⋆ 1)) ⋆ (x ⋆ (y ⋆ z))"
proof -
have 1: "(x ⋆ (y ⋆ 1)) ⋆ z ≤ (x ⋆ (y ⋆ 1)) ⋆ (x ⋆ (y ⋆ z))"
by (meson order.trans while_increasing while_right_isotone)
have "x ⊔ (y ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
using while_increasing while_sup_below by auto
hence "(x ⋆ (y ⋆ 1)) ⋆ (x ⋆ (y ⋆ z)) ≤ (x ⋆ (y ⋆ 1)) ⋆ z"
using while_absorb_2 while_sup_below by force
thus ?thesis
using 1 order.antisym by blast
qed

lemma while_back_loop_fixpoint:
"z * (y ⋆ (y * x)) ⊔ z * x = z * (y ⋆ x)"
by (metis sup_commute mult_left_dist_sup while_right_unfold)

lemma while_back_loop_prefixpoint:
"z * (y ⋆ 1) * y ⊔ z ≤ z * (y ⋆ 1)"
by (metis le_supI le_supI2 mult_1_right mult_right_isotone mult_assoc while_increasing while_one_mult_below while_right_unfold)

text ‹Theorem 9›

lemma while_loop_is_fixpoint:
"is_fixpoint (λx . y * x ⊔ z) (y ⋆ z)"
using is_fixpoint_def sup_commute while_left_unfold by auto

text ‹Theorem 9›

lemma while_back_loop_is_prefixpoint:
"is_prefixpoint (λx . x * y ⊔ z) (z * (y ⋆ 1))"
using is_prefixpoint_def while_back_loop_prefixpoint by auto

text ‹Theorem 9.20›

lemma while_while_sup:
"(1 ⊔ x) ⋆ y = (x ⋆ 1) ⋆ y"
by (metis sup_commute while_decompose_10 while_sumstar while_zero)

lemma while_while_mult_sub:
"x ⋆ (1 ⋆ y) ≤ (x ⋆ 1) ⋆ y"
by (metis sup_commute while_sub_dist_3 while_while_sup)

text ‹Theorem 9.11›

lemma while_right_plus:
"(x ⋆ x) ⋆ y = x ⋆ y"
by (metis sup_idem while_plus_one while_sumstar while_transitive)

text ‹Theorem 9.12›

lemma while_left_plus:
"(x * (x ⋆ 1)) ⋆ y = x ⋆ y"

text ‹Theorem 9.9›

lemma while_below_while_one:
"x ⋆ x ≤ x ⋆ 1"
by (meson eq_refl while_mult_transitive while_one_increasing)

lemma while_below_while_one_mult:
"x * (x ⋆ x) ≤ x * (x ⋆ 1)"

text ‹Theorem 9.23›

lemma while_sup_sub_sup_one:
"x ⋆ (x ⊔ y) ≤ x ⋆ (1 ⊔ y)"
using semiring.add_right_mono while_left_dist_sup while_below_while_one by auto

lemma while_sup_sub_sup_one_mult:
"x * (x ⋆ (x ⊔ y)) ≤ x * (x ⋆ (1 ⊔ y))"

lemma while_elimination:
"x * y = bot ⟹ x * (y ⋆ z) = x * z"
by (metis sup_bot_right mult_assoc mult_left_dist_sup mult_left_zero while_left_unfold)

text ‹Theorem 9.8›

lemma while_square:
"(x * x) ⋆ y ≤ x ⋆ y"
by (metis while_left_isotone while_mult_increasing while_right_plus)

text ‹Theorem 9.35›

lemma while_mult_sub_sup:
"(x * y) ⋆ z ≤ (x ⊔ y) ⋆ z"
by (metis while_increasing while_isotone while_mult_increasing while_sumstar)

text ‹Theorem 9.43›

lemma while_absorb_1:
"x ≤ y ⟹ x ⋆ (y ⋆ z) = y ⋆ z"
by (metis order.antisym le_iff_sup while_increasing while_sub_dist_3)

lemma while_absorb_3:
"x ≤ y ⟹ x ⋆ (y ⋆ z) = y ⋆ (x ⋆ z)"

text ‹Theorem 9.24›

lemma while_square_2:
"(x * x) ⋆ ((x ⊔ 1) * y) ≤ x ⋆ y"
by (metis le_supI while_increasing while_mult_transitive while_mult_upper_bound while_one_increasing while_square)

lemma while_separate_unfold_below:
"(y * (x ⋆ 1)) ⋆ z ≤ (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z))))"
proof -
have "(y * (x ⋆ 1)) ⋆ z = (y ⋆ (y * x * (x ⋆ 1))) ⋆ (y ⋆ z)"
by (metis mult_assoc mult_left_dist_sup mult_1_right while_left_unfold while_sumstar)
hence "(y * (x ⋆ 1)) ⋆ z = (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ 1))) * ((y * (x ⋆ 1)) ⋆ z)"
using while_left_unfold by auto
also have "... ≤ (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ 1)) * ((y * (x ⋆ 1)) ⋆ z))"
using sup_right_isotone while_sub_associative by auto
also have "... ≤ (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z))))"
by (smt sup_right_isotone mult_assoc mult_right_isotone while_one_mult_below while_right_isotone)
finally show ?thesis
.
qed

text ‹Theorem 9.33›

lemma while_mult_zero_sup:
"(x ⊔ y * bot) ⋆ z = x ⋆ ((y * bot) ⋆ z)"
proof -
have "(x ⊔ y * bot) ⋆ z = (x ⋆ (y * bot)) ⋆ (x ⋆ z)"
also have "... = (x ⋆ z) ⊔ (x ⋆ (y * bot)) * ((x ⋆ (y * bot)) ⋆ (x ⋆ z))"
using while_left_unfold by auto
also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (y * bot))"
by (metis sup_right_isotone mult_assoc mult_left_zero while_sub_associative)
also have "... = x ⋆ ((y * bot) ⋆ z)"
by (simp add: sup_commute while_left_dist_sup while_zero_2)
finally show ?thesis
qed

lemma while_sup_mult_zero:
"(x ⊔ y * bot) ⋆ y = x ⋆ y"
by (simp add: sup_absorb2 zero_right_mult_decreasing while_mult_zero_sup while_zero_2)

lemma while_mult_zero_sup_2:
"(x ⊔ y * bot) ⋆ z = (x ⋆ z) ⊔ (x ⋆ (y * bot))"
by (simp add: sup_commute while_left_dist_sup while_mult_zero_sup while_zero_2)

lemma while_sup_zero_star:
"(x ⊔ y * bot) ⋆ z = x ⋆ (y * bot ⊔ z)"

lemma while_unfold_sum:
"(x ⊔ y) ⋆ z = (x ⋆ z) ⊔ (x ⋆ (y * ((x ⊔ y) ⋆ z)))"
apply (rule order.antisym)
apply (metis semiring.add_left_mono while_sub_associative while_sumstar while_left_unfold)
by (metis le_supI while_decompose_7 while_mult_increasing while_right_isotone while_sub_dist)

lemma while_simulate_left:
"x * z ≤ z * y ⊔ w ⟹ x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ (w * (y ⋆ v)))"
by (metis sup_left_isotone mult_right_isotone order_trans while_one_increasing while_simulate_left_plus)

lemma while_simulate_right:
assumes "z * x ≤ y * z ⊔ w"
shows "z * (x ⋆ v) ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
proof -
have "y * z ⊔ w ≤ y * (y ⋆ z) ⊔ w"
using sup_left_isotone while_increasing while_mult_star_exchange by force
thus ?thesis
by (meson assms order.trans while_simulate_right_plus)
qed

lemma while_simulate:
"z * x ≤ y * z ⟹ z * (x ⋆ v) ≤ y ⋆ (z * v)"
by (metis sup_bot_right mult_left_zero while_simulate_right)

text ‹Theorem 9.14›

lemma while_while_mult:
"1 ⋆ (x ⋆ y) = (x ⋆ 1) ⋆ y"
proof -
have "(x ⋆ 1) ⋆ y ≤ (x ⋆ 1) * ((x ⋆ 1) ⋆ y)"
also have "... ≤ 1 ⋆ ((x ⋆ 1) * y)"
also have "... ≤ 1 ⋆ (x ⋆ y)"
finally show ?thesis
by (metis order.antisym while_sub_dist_3 while_while_sup)
qed

lemma while_simulate_left_1:
"x * z ≤ z * y ⟹ x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ bot)"
by (meson order.trans mult_right_isotone while_one_increasing while_simulate_left_plus_1)

text ‹Theorem 9.46›

lemma while_associative_1:
assumes "1 ≤ z"
shows "x ⋆ (y * z) = (x ⋆ y) * z"
proof -
have "x ⋆ (y * z) ≤ x ⋆ ((x ⋆ y) * z)"
by (simp add: mult_isotone while_increasing while_right_isotone)
also have "... ≤ (x ⋆ y) * (bot ⋆ z) ⊔ (x ⋆ bot)"
by (metis mult_assoc mult_right_sub_dist_sup_right while_left_unfold while_simulate_absorb while_zero)
also have "... ≤ (x ⋆ y) * z ⊔ (x ⋆ bot) * z"
by (metis assms le_supI sup_ge1 sup_ge2 case_split_right while_plus_one while_zero)
also have "... = (x ⋆ y) * z"
by (metis sup_bot_right mult_right_dist_sup while_left_dist_sup)
finally show ?thesis
qed

text ‹Theorem 9.29›

lemma while_associative_while_1:
"x ⋆ (y * (z ⋆ 1)) = (x ⋆ y) * (z ⋆ 1)"

text ‹Theorem 9.13›

lemma while_one_while:
"(x ⋆ 1) * (y ⋆ 1) = x ⋆ (y ⋆ 1)"
by (metis mult_left_one while_associative_while_1)

lemma while_decompose_5_below:
"(x ⋆ (y ⋆ 1)) ⋆ z ≤ (y ⋆ (x ⋆ 1)) ⋆ z"
by (smt (z3) while_left_dist_sup while_sumstar while_absorb_2 while_one_increasing while_plus_one while_sub_dist)

text ‹Theorem 9.26›

lemma while_decompose_5:
"(x ⋆ (y ⋆ 1)) ⋆ z = (y ⋆ (x ⋆ 1)) ⋆ z"

lemma while_decompose_4:
"(x ⋆ (y ⋆ 1)) ⋆ z = x ⋆ ((y ⋆ (x ⋆ 1)) ⋆ z)"
using while_absorb_1 while_decompose_5 while_sup_below by auto

text ‹Theorem 11.7›

lemma while_simulate_2:
"y * (x ⋆ 1) ≤ x ⋆ (y ⋆ 1) ⟷ y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
proof
assume "y * (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
hence "y * (x ⋆ 1) ≤ (x ⋆ 1) * (y ⋆ 1)"
hence "y ⋆ ((x ⋆ 1) * 1) ≤ (x ⋆ 1) * (y ⋆ 1) ⊔ (y ⋆ bot)"
using while_simulate_left_plus_1 by blast
hence "y ⋆ (x ⋆ 1) ≤ (x ⋆ (y ⋆ 1)) ⊔ (y ⋆ bot)"
also have "... = x ⋆ (y ⋆ 1)"
by (metis sup_commute le_iff_sup order_trans while_increasing while_right_isotone bot_least)
finally show "y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
.
next
assume "y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
thus "y * (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
using order_trans while_mult_increasing by blast
qed

lemma while_simulate_1:
"y * x ≤ x * y ⟹ y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
by (metis order_trans while_mult_increasing while_right_isotone while_simulate while_simulate_2)

lemma while_simulate_3:
"y * (x ⋆ 1) ≤ x ⋆ 1 ⟹ y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
by (meson order.trans while_increasing while_right_isotone while_simulate_2)

text ‹Theorem 9.28›

lemma while_extra_while:
"(y * (x ⋆ 1)) ⋆ z = (y * (y ⋆ (x ⋆ 1))) ⋆ z"
proof -
have "y * (y ⋆ (x ⋆ 1)) ≤ y * (x ⋆ 1) * (y * (x ⋆ 1) ⋆ 1)"
using while_back_loop_prefixpoint while_left_isotone while_mult_star_exchange by auto
hence 1: "(y * (y ⋆ (x ⋆ 1))) ⋆ z ≤ (y * (x ⋆ 1)) ⋆ z"
by (metis while_simulate_right_plus_1 mult_left_one)
have "(y * (x ⋆ 1)) ⋆ z ≤ (y * (y ⋆ (x ⋆ 1))) ⋆ z"
by (simp add: while_increasing while_left_isotone while_mult_star_exchange)
thus ?thesis
using 1 order.antisym by auto
qed

text ‹Theorem 11.6›

lemma while_separate_4:
assumes "y * x ≤ x * (x ⋆ (1 ⊔ y))"
shows "(x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
proof -
have "(1 ⊔ y) * x ≤ x * (x ⋆ (1 ⊔ y))"
by (smt assms sup_assoc le_supI mult_left_one mult_left_sub_dist_sup_left mult_right_dist_sup mult_1_right while_left_unfold)
hence 1: "(1 ⊔ y) * (x ⋆ 1) ≤ x ⋆ (1 ⊔ y)"
by (metis mult_1_right while_simulate_right_plus_1)
have "y * x * (x ⋆ 1) ≤ x * (x ⋆ ((1 ⊔ y) * (x ⋆ 1)))"
by (smt assms le_iff_sup mult_assoc mult_right_dist_sup while_associative_1 while_increasing)
also have "... ≤ x * (x ⋆ (1 ⊔ y))"
using 1 mult_right_isotone while_mult_transitive by blast
also have "... ≤ x * (x ⋆ 1) * (y ⋆ 1)"
by (simp add: mult_right_isotone mult_assoc while_increasing while_one_increasing while_one_while while_right_isotone)
finally have "y ⋆ (x * (x ⋆ 1)) ≤ x * (x ⋆ 1) * (y ⋆ 1) ⊔ (y ⋆ bot)"
by (metis mult_assoc mult_1_right while_simulate_left_plus_1)
hence "(y ⋆ 1) * (y ⋆ x) ≤ x * (x ⋆ y ⋆ 1) ⊔ (y ⋆ bot)"
by (smt le_iff_sup mult_assoc mult_1_right order_refl order_trans while_absorb_2 while_left_dist_sup while_mult_star_exchange while_one_mult_below while_one_while while_plus_one)
hence "(y ⋆ 1) * ((y ⋆ x) ⋆ (y ⋆ z)) ≤ x ⋆ ((y ⋆ 1) * (y ⋆ z) ⊔ (y ⋆ bot) * ((y ⋆ x) ⋆ (y ⋆ z)))"
also have "... ≤ x ⋆ ((y ⋆ z) ⊔ (y ⋆ bot))"
by (metis sup_mono mult_left_zero order_refl while_absorb_2 while_one_mult_below while_right_isotone while_sub_associative)
also have "... = x ⋆ y ⋆ z"
using sup.absorb_iff1 while_right_isotone by auto
finally show ?thesis
by (smt sup_commute le_iff_sup mult_left_one mult_right_dist_sup while_plus_one while_sub_associative while_sumstar)
qed

lemma while_separate_5:
"y * x ≤ x * (x ⋆ (x ⊔ y)) ⟹ (x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
using order_lesseq_imp while_separate_4 while_sup_sub_sup_one_mult by blast

lemma while_separate_6:
"y * x ≤ x * (x ⊔ y) ⟹ (x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
by (smt order_trans while_increasing while_mult_star_exchange while_separate_5)

text ‹Theorem 11.4›

lemma while_separate_1:
"y * x ≤ x * y ⟹ (x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
using mult_left_sub_dist_sup_right order_lesseq_imp while_separate_6 by blast

text ‹Theorem 11.2›

lemma while_separate_mult_1:
"y * x ≤ x * y ⟹ (x * y) ⋆ z ≤ x ⋆ (y ⋆ z)"
by (metis while_mult_sub_sup while_separate_1)

text ‹Theorem 11.5›

lemma separation:
assumes "y * x ≤ x * (y ⋆ 1)"
shows "(x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
proof -
have "y ⋆ x ≤ x * (y ⋆ 1) ⊔ (y ⋆ bot)"
by (metis assms mult_1_right while_simulate_left_plus_1)
also have "... ≤ x * (x ⋆ y ⋆ 1) ⊔ (y ⋆ bot)"
using sup_left_isotone while_increasing while_mult_star_exchange by force
finally have "(y ⋆ 1) * (y ⋆ x) ≤ x * (x ⋆ y ⋆ 1) ⊔ (y ⋆ bot)"
using order.trans while_one_mult_while_below by blast
hence "(y ⋆ 1) * ((y ⋆ x) ⋆ (y ⋆ z)) ≤ x ⋆ ((y ⋆ 1) * (y ⋆ z) ⊔ (y ⋆ bot) * ((y ⋆ x) ⋆ (y ⋆ z)))"
also have "... ≤ x ⋆ ((y ⋆ z) ⊔ (y ⋆ bot))"
by (metis sup_mono mult_left_zero order_refl while_absorb_2 while_one_mult_below while_right_isotone while_sub_associative)
also have "... = x ⋆ y ⋆ z"
using sup.absorb_iff1 while_right_isotone by auto
finally show ?thesis
by (smt sup_commute le_iff_sup mult_left_one mult_right_dist_sup while_plus_one while_sub_associative while_sumstar)
qed

text ‹Theorem 11.5›

lemma while_separate_left:
"y * x ≤ x * (y ⋆ 1) ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
by (metis sup_commute separation while_sub_dist_3)

text ‹Theorem 11.6›

lemma while_simulate_4:
"y * x ≤ x * (x ⋆ (1 ⊔ y)) ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
by (metis sup_commute while_separate_4 while_sub_dist_3)

lemma while_simulate_5:
"y * x ≤ x * (x ⋆ (x ⊔ y)) ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
by (smt order_trans while_sup_sub_sup_one_mult while_simulate_4)

lemma while_simulate_6:
"y * x ≤ x * (x ⊔ y) ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
by (smt order_trans while_increasing while_mult_star_exchange while_simulate_5)

text ‹Theorem 11.3›

lemma while_simulate_7:
"y * x ≤ x * y ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
using mult_left_sub_dist_sup_right order_lesseq_imp while_simulate_6 by blast

lemma while_while_mult_1:
"x ⋆ (1 ⋆ y) = 1 ⋆ (x ⋆ y)"
by (metis sup_commute mult_left_one mult_1_right order_refl while_separate_1)

text ‹Theorem 9.15›

lemma while_while_mult_2:
"x ⋆ (1 ⋆ y) = (x ⋆ 1) ⋆ y"

text ‹Theorem 11.8›

lemma while_import:
assumes "p ≤ p * p ∧ p ≤ 1 ∧ p * x ≤ x * p"
shows "p * (x ⋆ y) = p * ((p * x) ⋆ y)"
proof -
have "p * (x ⋆ y) ≤ (p * x) ⋆ (p * y)"
using assms test_preserves_equation while_simulate by auto
also have "... ≤ (p * x) ⋆ y"
by (metis assms le_iff_sup mult_left_one mult_right_dist_sup while_right_isotone)
finally have 2: "p * (x ⋆ y) ≤ p * ((p * x) ⋆ y)"
by (smt assms sup_commute le_iff_sup mult_assoc mult_left_dist_sup mult_1_right)
have "p * ((p * x) ⋆ y) ≤ p * (x ⋆ y)"
by (metis assms mult_left_isotone mult_left_one mult_right_isotone while_left_isotone)
thus ?thesis
using 2 order.antisym by auto
qed

text ‹Theorem 11.8›

lemma while_preserve:
assumes "p ≤ p * p"
and "p ≤ 1"
and "p * x ≤ x * p"
shows "p * (x ⋆ y) = p * (x ⋆ (p * y))"
proof (rule order.antisym)
show "p * (x ⋆ y) ≤ p * (x ⋆ (p * y))"
by (metis assms order.antisym coreflexive_transitive mult_right_isotone mult_assoc while_simulate)
show "p * (x ⋆ (p * y)) ≤ p * (x ⋆ y)"
by (metis assms(2) mult_left_isotone mult_left_one mult_right_isotone while_right_isotone)
qed

lemma while_plus_below_while:
"(x ⋆ 1) * x ≤ x ⋆ 1"

text ‹Theorem 9.40›

lemma while_01:
"(w * (x ⋆ 1)) ⋆ (y * z) ≤ (x ⋆ w) ⋆ ((x ⋆ y) * z)"
proof -
have "(w * (x ⋆ 1)) ⋆ (y * z) = y * z ⊔ w * (((x ⋆ 1) * w) ⋆ ((x ⋆ 1) * y * z))"
by (metis mult_assoc while_productstar)
also have "... ≤ y * z ⊔ w * ((x ⋆ w) ⋆ ((x ⋆ y) * z))"
by (metis sup_right_isotone mult_left_isotone mult_right_isotone while_isotone while_one_mult_below)
also have "... ≤ (x ⋆ y) * z ⊔ (x ⋆ w) * ((x ⋆ w) ⋆ ((x ⋆ y) * z))"
finally show ?thesis
using while_left_unfold by auto
qed

text ‹Theorem 9.37›

lemma while_while_sub_associative:
"x ⋆ (y ⋆ z) ≤ ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
proof -
have 1: "x * (x ⋆ 1) ≤ (x ⋆ 1) * ((x ⋆ y) ⋆ 1)"
by (metis le_supE while_back_loop_prefixpoint while_mult_increasing while_mult_transitive while_one_while)
have "x ⋆ (y ⋆ z) ≤ x ⋆ ((x ⋆ 1) * (y ⋆ z))"
by (metis mult_left_isotone mult_left_one while_increasing while_right_isotone)
also have "... ≤ (x ⋆ 1) * ((x ⋆ y) ⋆ (y ⋆ z)) ⊔ (x ⋆ bot)"
using 1 while_simulate_left_plus_1 by auto
also have "... ≤ (x ⋆ 1) * ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
by (simp add: le_supI1 sup_commute while_absorb_2 while_increasing while_right_isotone)
also have "... = (x ⋆ 1) * z ⊔ (x ⋆ 1) * (x ⋆ y) * ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
by (metis mult_assoc mult_left_dist_sup while_left_unfold)
also have "... = (x ⋆ y) * ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
by (smt sup_assoc sup_commute le_iff_sup mult_left_one mult_right_dist_sup order_refl while_absorb_1 while_plus_one while_sub_associative)
also have "... ≤ ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
using sup_left_isotone while_left_plus_below by auto
finally show ?thesis
.
qed

lemma while_induct:
"x * z ≤ z ∧ y ≤ z ∧ x ⋆ 1 ≤ z ⟹ x ⋆ y ≤ z"
by (metis le_supI1 sup_commute sup_bot_left le_iff_sup while_right_isotone while_simulate_absorb)

proposition while_sumstar_4_below: "(x ⋆ y) ⋆ ((x ⋆ 1) * z) ≤ x ⋆ ((y * (x ⋆ 1)) ⋆ z)" oops
proposition while_sumstar_2: "(x ⊔ y) ⋆ z = x ⋆ ((y * (x ⋆ 1)) ⋆ z)" oops
proposition while_sumstar_3: "(x ⊔ y) ⋆ z = ((x ⋆ 1) * y) ⋆ (x ⋆ z)" oops
proposition while_decompose_6: "x ⋆ ((y * (x ⋆ 1)) ⋆ z) = y ⋆ ((x * (y ⋆ 1)) ⋆ z)" oops
proposition while_finite_associative: "x ⋆ bot = bot ⟹ (x ⋆ y) * z = x ⋆ (y * z)" oops
proposition atomicity_refinement: "s = s * q ⟹ x = q * x ⟹ q * b = bot ⟹ r * b ≤ b * r ⟹ r * l ≤ l * r ⟹ x * l ≤ l * x ⟹ b * l ≤ l * b ⟹ q * l ≤ l * q ⟹ r ⋆ q ≤ q * (r ⋆ 1) ⟹ q ≤ 1 ⟹ s * ((x ⊔ b ⊔ r ⊔ l) ⋆ (q * z)) ≤ s * ((x * (b ⋆ q) ⊔ r ⊔ l) ⋆ z)" oops

proposition while_separate_right_plus: "y * x ≤ x * (x ⋆ (1 ⊔ y)) ⊔ 1 ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)" 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 "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 bounded_binary_itering = bounded_idempotent_left_zero_semiring + binary_itering
begin

text ‹Theorem 9›

lemma while_right_top:
"x ⋆ top = top"
by (metis sup_left_top while_left_unfold)

text ‹Theorem 9›

lemma while_left_top:
"top * (x ⋆ 1) = top"
by (meson order.antisym le_supE top_greatest while_back_loop_prefixpoint)

end

class extended_binary_itering = binary_itering +
assumes while_denest_0: "w * (x ⋆ (y * z)) ≤ (w * (x ⋆ y)) ⋆ (w * (x ⋆ y) * z)"
begin

text ‹Theorem 10.2›

lemma while_denest_1:
"w * (x ⋆ (y * z)) ≤ (w * (x ⋆ y)) ⋆ z"
using while_denest_0 while_mult_increasing while_mult_transitive by blast

lemma while_mult_sub_while_while:
"x ⋆ (y * z) ≤ (x ⋆ y) ⋆ z"
by (metis mult_left_one while_denest_1)

lemma while_zero_zero:
"(x ⋆ bot) ⋆ bot = x ⋆ bot"
by (metis order.antisym mult_left_zero sup_bot_left while_left_unfold while_sub_associative while_mult_sub_while_while)

text ‹Theorem 10.11›

lemma while_mult_zero_zero:
"(x * (y ⋆ bot)) ⋆ bot = x * (y ⋆ bot)"
apply (rule order.antisym)
apply (metis sup_bot_left while_left_unfold mult_assoc le_supI1 mult_left_zero mult_right_isotone while_left_dist_sup while_sub_associative)
by (metis mult_left_zero while_denest_1)

text ‹Theorem 10.3›

lemma while_denest_2:
"w * ((x ⋆ (y * w)) ⋆ z) = w * (((x ⋆ y) * w) ⋆ z)"
apply (rule order.antisym)
apply (metis mult_assoc while_denest_0 while_simulate_right_plus_1 while_slide)
by (simp add: mult_isotone while_left_isotone while_sub_associative)

text ‹Theorem 10.12›

lemma while_denest_3:
"(x ⋆ w) ⋆ (x ⋆ bot) = (x ⋆ w) ⋆ bot"
by (metis while_absorb_2 while_right_isotone while_zero_zero bot_least)

text ‹Theorem 10.15›

lemma while_02:
"x ⋆ ((x ⋆ w) ⋆ ((x ⋆ y) * z)) = (x ⋆ w) ⋆ ((x ⋆ y) * z)"
proof -
have "x * ((x ⋆ w) ⋆ ((x ⋆ y) * z)) = x * (x ⋆ y) * z ⊔ x * (x ⋆ w) * ((x ⋆ w) ⋆ ((x ⋆ y) * z))"
by (metis mult_assoc mult_left_dist_sup while_left_unfold)
also have "... ≤ (x ⋆ w) ⋆ ((x ⋆ y) * z)"
by (metis sup_mono mult_right_sub_dist_sup_right while_left_unfold)
finally have "x ⋆ ((x ⋆ w) ⋆ ((x ⋆ y) * z)) ≤ ((x ⋆ w) ⋆ ((x ⋆ y) * z)) ⊔ (x ⋆ bot)"
using while_simulate_absorb by auto
also have "... = (x ⋆ w) ⋆ ((x ⋆ y) * z)"
by (metis sup_commute le_iff_sup order_trans while_mult_sub_while_while while_right_isotone bot_least)
finally show ?thesis
qed

lemma while_sumstar_3_below:
"(x ⋆ y) ⋆ (x ⋆ z) ≤ (x ⋆ y) ⋆ ((x ⋆ 1) * z)"
proof -
have "(x ⋆ y) ⋆ (x ⋆ z) = (x ⋆ z) ⊔ ((x ⋆ y) ⋆ ((x ⋆ y) * (x ⋆ z)))"
using while_right_unfold by blast
also have "... ≤ (x ⋆ z) ⊔ ((x ⋆ y) ⋆ (x ⋆ (y * (x ⋆ z))))"
by (meson sup_right_isotone while_right_isotone while_sub_associative)
also have "... ≤ (x ⋆ z) ⊔ ((x ⋆ y) ⋆ (x ⋆ ((x ⋆ y) ⋆ (x ⋆ z))))"
by (smt sup_right_isotone order_trans while_increasing while_mult_upper_bound while_one_increasing while_right_isotone)
also have "... ≤ (x ⋆ z) ⊔ ((x ⋆ y) ⋆ (x ⋆ ((x ⋆ y) ⋆ ((x ⋆ 1) * z))))"
by (metis sup_right_isotone mult_left_isotone mult_left_one order_trans while_increasing while_right_isotone while_sumstar while_transitive)
also have "... = (x ⋆ z) ⊔ ((x ⋆ y) ⋆ ((x ⋆ 1) * z))"
also have "... = (x ⋆ y) ⋆ ((x ⋆ 1) * z)"
by (smt sup_assoc mult_left_one mult_right_dist_sup while_02 while_left_dist_sup while_plus_one)
finally show ?thesis
.
qed

lemma while_sumstar_4_below:
"(x ⋆ y) ⋆ ((x ⋆ 1) * z) ≤ x ⋆ ((y * (x ⋆ 1)) ⋆ z)"
proof -
have "(x ⋆ y) ⋆ ((x ⋆ 1) * z) = (x ⋆ 1) * z ⊔ (x ⋆ y) * ((x ⋆ y) ⋆ ((x ⋆ 1) * z))"
using while_left_unfold by auto
also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (y * ((x ⋆ y) ⋆ ((x ⋆ 1) * z))))"
by (meson sup_mono while_one_mult_below while_sub_associative)
also have "... = (x ⋆ z) ⊔ (x ⋆ (y * (((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z))))"
by (metis mult_left_one while_denest_2)
also have "... = x ⋆ ((y * (x ⋆ 1)) ⋆ z)"
by (metis while_left_dist_sup while_productstar)
finally show ?thesis
.
qed

text ‹Theorem 10.10›

lemma while_sumstar_1:
"(x ⊔ y) ⋆ z = (x ⋆ y) ⋆ ((x ⋆ 1) * z)"
by (smt order.eq_iff order_trans while_sup_1_below while_sumstar while_sumstar_3_below while_sumstar_4_below)

text ‹Theorem 10.8›

lemma while_sumstar_2:
"(x ⊔ y) ⋆ z = x ⋆ ((y * (x ⋆ 1)) ⋆ z)"
using order.antisym while_sup_1_below while_sumstar_1 while_sumstar_4_below by auto

text ‹Theorem 10.9›

lemma while_sumstar_3:
"(x ⊔ y) ⋆ z = ((x ⋆ 1) * y) ⋆ (x ⋆ z)"
using order.antisym while_sumstar while_sumstar_1_below while_sumstar_2_below while_sumstar_2 by force

text ‹Theorem 10.6›

lemma while_decompose_6:
"x ⋆ ((y * (x ⋆ 1)) ⋆ z) = y ⋆ ((x * (y ⋆ 1)) ⋆ z)"
by (metis sup_commute while_sumstar_2)

text ‹Theorem 10.4›

lemma while_denest_4:
"(x ⋆ w) ⋆ (x ⋆ (y * z)) = (x ⋆ w) ⋆ ((x ⋆ y) * z)"
proof -
have "(x ⋆ w) ⋆ (x ⋆ (y * z)) = x ⋆ ((w * (x ⋆ 1)) ⋆ (y * z))"
using while_sumstar while_sumstar_2 by force
also have "... ≤ (x ⋆ w) ⋆ ((x ⋆ y) * z)"
by (metis while_01 while_right_isotone while_02)
finally show ?thesis
using order.antisym while_right_isotone while_sub_associative by auto
qed

text ‹Theorem 10.13›

lemma while_denest_5:
"w * ((x ⋆ (y * w)) ⋆ (x ⋆ (y * z))) = w * (((x ⋆ y) * w) ⋆ ((x ⋆ y) * z))"

text ‹Theorem 10.5›

lemma while_denest_6:
"(w * (x ⋆ y)) ⋆ z = z ⊔ w * ((x ⊔ y * w) ⋆ (y * z))"
by (metis while_denest_5 while_productstar while_sumstar)

text ‹Theorem 10.1›

lemma while_sum_below_one:
"y * ((x ⊔ y) ⋆ z) ≤ (y * (x ⋆ 1)) ⋆ z"

text ‹Theorem 10.14›

lemma while_separate_unfold:
"(y * (x ⋆ 1)) ⋆ z = (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z))))"
proof -
have "y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z))) ≤ y ⋆ (y * ((x ⊔ y) ⋆ z))"
using mult_right_isotone while_left_plus_below while_right_isotone mult_assoc while_sumstar_2 by auto
also have "... ≤ (y * (x ⋆ 1)) ⋆ z"
by (metis sup_commute sup_ge1 while_absorb_1 while_mult_star_exchange while_sum_below_one)
finally have "(y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z)))) ≤ (y * (x ⋆ 1)) ⋆ z"
using sup.bounded_iff while_back_loop_prefixpoint while_left_isotone by auto
thus ?thesis
qed

text ‹Theorem 10.7›

lemma while_finite_associative:
"x ⋆ bot = bot ⟹ (x ⋆ y) * z = x ⋆ (y * z)"
by (metis while_denest_4 while_zero)

text ‹Theorem 12›

lemma atomicity_refinement:
assumes "s = s * q"
and "x = q * x"
and "q * b = bot"
and "r * b ≤ b * r"
and "r * l ≤ l * r"
and "x * l ≤ l * x"
and "b * l ≤ l * b"
and "q * l ≤ l * q"
and "r ⋆ q ≤ q * (r ⋆ 1) ∧ q ≤ 1"
shows "s * ((x ⊔ b ⊔ r ⊔ l) ⋆ (q * z)) ≤ s * ((x * (b ⋆ q) ⊔ r ⊔ l) ⋆ z)"
proof -
have 1: "(x ⊔ b ⊔ r) * l ≤ l * (x ⊔ b ⊔ r)"
by (smt assms(5-7) mult_left_dist_sup semiring.add_mono semiring.distrib_right)
have "q * ((x * (b ⋆ r ⋆ 1) * q) ⋆ z) ≤ (x * (b ⋆ r ⋆ 1) * q) ⋆ z"
using assms(9) order_lesseq_imp while_increasing while_mult_upper_bound by blast
also have "... ≤ (x * (b ⋆ ((r ⋆ 1) * q))) ⋆ z"
by (simp add: mult_right_isotone while_left_isotone while_sub_associative mult_assoc)
also have "... ≤ (x * (b ⋆ r ⋆ q)) ⋆ z"
by (simp add: mult_right_isotone while_left_isotone while_one_mult_below while_right_isotone)
also have "... ≤ (x * (b ⋆ (q * (r ⋆ 1)))) ⋆ z"
by (simp add: assms(9) mult_right_isotone while_left_isotone while_right_isotone)
finally have 2: "q * ((x * (b ⋆ r ⋆ 1) * q) ⋆ z) ≤ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z"
using while_associative_while_1 mult_assoc by auto
have "s * ((x ⊔ b ⊔ r ⊔ l) ⋆ (q * z)) = s * (l ⋆ (x ⊔ b ⊔ r) ⋆ (q * z))"
using 1 sup_commute while_separate_1 by fastforce
also have "... = s * q * (l ⋆ b ⋆ r ⋆ (q * x * (b ⋆ r ⋆ 1)) ⋆ (q * z))"
by (smt assms(1,2,4) sup_assoc sup_commute while_sumstar_2 while_separate_1)
also have "... = s * q * (l ⋆ b ⋆ r ⋆ (q * ((x * (b ⋆ r ⋆ 1) * q) ⋆ z)))"
also have "... ≤ s * q * (l ⋆ b ⋆ r ⋆ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z)"
using 2 by (meson mult_right_isotone while_right_isotone)
also have "... ≤ s * (l ⋆ q * (b ⋆ r ⋆ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z))"
by (simp add: assms(8) mult_right_isotone while_simulate mult_assoc)
also have "... = s * (l ⋆ q * (r ⋆ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z))"
using assms(3) while_elimination by auto
also have "... ≤ s * (l ⋆ r ⋆ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z)"
by (meson assms(9) order.trans mult_right_isotone order.refl while_increasing while_mult_upper_bound while_right_isotone)
also have "... = s * (l ⋆ (r ⊔ x * (b ⋆ q)) ⋆ z)"