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)
  by (simp add: while_one_while while_sumstar_2)

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"
    by (simp add: n_n_top_split_n_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"
    by (simp add: while_n_while_top_split)
  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"
    by (simp add: n_mult_omega_L_star_zero)
  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"
  by (simp add: while_def)

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"
    by (simp add: omega_slide sup_monoid.add_commute while_def)
  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)"
    by (simp add: while_def)
  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)"
      by (simp add: star_circ_simulate_right_plus)
    also have "... = y * z  y * y * n(yω) * L  y * w * x"
      by (simp add: L_mult_star semiring.distrib_left semiring.distrib_right sup_left_commute sup_monoid.add_commute mult_assoc)
    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))"
      by (simp add: while_def)
    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"
    by (simp add: mult_L_omega)
  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ω"
    by (simp add: omega_induct sup_monoid.add_commute)
  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"
  by (simp add: while_mult_L)

lemma tarski_top_omega_2:
  "x * L = (x * L)  bot"
  by (simp add: while_mult_L)

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