Theory N_Algebras

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

section ‹N-Algebras›

theory N_Algebras

imports Stone_Kleene_Relation_Algebras.Iterings Base Lattice_Ordered_Semirings

begin

class C_left_n_algebra = bounded_idempotent_left_semiring + bounded_distrib_lattice + n + L
begin

abbreviation C :: "'a ⇒ 'a" where "C x ≡ n(L) * top ⊓ x"

text ‹AACP Theorem 3.38›

lemma C_isotone:
  "x ≤ y ⟶ C x ≤ C y"
  using inf.sup_right_isotone by auto

text ‹AACP Theorem 3.40›

lemma C_decreasing:
  "C x ≤ x"
  by simp

end

class left_n_algebra = C_left_n_algebra +
  assumes n_dist_n_add            : "n(x) ⊔ n(y) = n(n(x) * top ⊔ y)"
  assumes n_export                : "n(x) * n(y) = n(n(x) * y)"
  assumes n_left_upper_bound      : "n(x) ≤ n(x ⊔ y)"
  assumes n_nL_meet_L_nL0         : "n(L) * x = (x ⊓ L) ⊔ n(L * bot) * x"
  assumes n_n_L_split_n_n_L_L     : "x * n(y) * L = x * bot ⊔ n(x * n(y) * L) * L"
  assumes n_sub_nL                : "n(x) ≤ n(L)"
  assumes n_L_decreasing          : "n(x) * L ≤ x"
  assumes n_L_T_meet_mult_combined: "C (x * y) * z ≤ C x * y * C z"
  assumes n_n_top_split_n_top     : "x * n(y) * top ≤ x * bot ⊔ n(x * y) * top"
  assumes n_top_meet_L_below_L    : "x * top * y ⊓ L ≤ x * L * y"
begin

subclass lattice_ordered_pre_left_semiring ..

lemma n_L_T_meet_mult_below:
  "C (x * y) ≤ C x * y"
proof -
  have "C (x * y) ≤ C x * y * C 1"
    by (meson order.trans mult_sub_right_one n_L_T_meet_mult_combined)
  also have "... ≤ C x * y"
    by (metis mult_1_right mult_left_sub_dist_inf_right)
  finally show ?thesis
    .
qed

text ‹AACP Theorem 3.41›

lemma n_L_T_meet_mult_propagate:
  "C x * y ≤ x * C y"
proof -
  have "C x * y ≤ C x * 1 * C y"
    by (metis mult_1_right mult_assoc n_L_T_meet_mult_combined mult_1_right)
  also have "... ≤ x * C y"
    by (simp add: mult_right_sub_dist_inf_right)
  finally show ?thesis
    .
qed

text ‹AACP Theorem 3.43›

lemma C_n_mult_closed:
  "C (n(x) * y) = n(x) * y"
  by (simp add: inf.absorb2 mult_isotone n_sub_nL)

text ‹AACP Theorem 3.40›

lemma meet_L_below_C:
  "x ⊓ L ≤ C x"
  by (simp add: le_supI1 n_nL_meet_L_nL0)

text ‹AACP Theorem 3.42›

lemma n_L_T_meet_mult:
  "C (x * y) = C x * y"
  apply (rule order.antisym)
  apply (rule n_L_T_meet_mult_below)
  by (smt (z3) C_n_mult_closed inf.boundedE inf.sup_monoid.add_assoc inf.sup_monoid.add_commute mult_right_sub_dist_inf mult_assoc)

text ‹AACP Theorem 3.42›

lemma C_mult_propagate:
  "C x * y = C x * C y"
  by (smt (z3) C_n_mult_closed order.eq_iff inf.left_commute inf.sup_monoid.add_commute mult_left_sub_dist_inf_right n_L_T_meet_mult_propagate)

text ‹AACP Theorem 3.32›

lemma meet_L_below_n_L:
  "x ⊓ L ≤ n(L) * x"
  by (simp add: n_nL_meet_L_nL0)

text ‹AACP Theorem 3.27›

lemma n_vector_meet_L:
  "x * top ⊓ L ≤ x * L"
  by (metis mult_1_right n_top_meet_L_below_L)

lemma n_right_upper_bound:
  "n(x) ≤ n(y ⊔ x)"
  by (simp add: n_left_upper_bound sup_commute)

text ‹AACP Theorem 3.1›

lemma n_isotone:
  "x ≤ y ⟹ n(x) ≤ n(y)"
  by (metis le_iff_sup n_left_upper_bound)

lemma n_add_left_zero:
  "n(bot) ⊔ n(x) = n(x)"
  using le_iff_sup sup_bot_right sup_right_divisibility n_isotone by auto

text ‹AACP Theorem 3.13›

lemma n_mult_right_zero_L:
  "n(x) * bot ≤ L"
  by (meson bot_least mult_isotone n_L_decreasing n_sub_nL order_trans)

lemma n_add_left_top:
  "n(top) ⊔ n(x) = n(top)"
  by (simp add: sup_absorb1 n_isotone)

text ‹AACP Theorem 3.18›

lemma n_n_L:
  "n(n(x) * L) = n(x)"
  by (metis order.antisym n_dist_n_add n_export n_sub_nL sup_bot_right sup_commute sup_top_left n_add_left_zero n_right_upper_bound)

lemma n_mult_transitive:
  "n(x) * n(x) ≤ n(x)"
  by (metis mult_right_isotone n_export n_sub_nL n_n_L)

lemma n_mult_left_absorb_add_sub:
  "n(x) * (n(x) ⊔ n(y)) ≤ n(x)"
  by (metis mult_right_isotone n_dist_n_add n_export n_sub_nL n_n_L)

text ‹AACP Theorem 3.21›

lemma n_mult_left_lower_bound:
  "n(x) * n(y) ≤ n(x)"
  by (metis mult_right_isotone n_export n_sub_nL n_n_L)

text ‹AACP Theorem 3.20›

lemma n_mult_left_zero:
  "n(bot) * n(x) = n(bot)"
  by (metis n_export sup_absorb1 n_add_left_zero n_mult_left_lower_bound)

lemma n_mult_right_one:
  "n(x) * n(top) = n(x)"
  using n_dist_n_add n_export sup_commute n_add_left_zero by fastforce

lemma n_L_increasing:
  "n(x) ≤ n(n(x) * L)"
  by (simp add: n_n_L)

text ‹AACP Theorem 3.2›

lemma n_galois:
  "n(x) ≤ n(y) ⟷ n(x) * L ≤ y"
  by (metis mult_left_isotone n_L_decreasing n_L_increasing n_isotone order_trans)

lemma n_add_n_top:
  "n(x ⊔ n(x) * top) = n(x)"
  by (metis n_dist_n_add sup.idem sup_commute)

text ‹AACP Theorem 3.6›

lemma n_L_below_nL_top:
  "L ≤ n(L) * top"
  by (metis inf_top.left_neutral meet_L_below_n_L)

text ‹AACP Theorem 3.4›

lemma n_less_eq_char_n:
  "x ≤ y ⟷ x ≤ y ⊔ L ∧ C x ≤ y ⊔ n(y) * top"
proof
  assume "x ≤ y"
  thus "x ≤ y ⊔ L ∧ C x ≤ y ⊔ n(y) * top"
    by (simp add: inf.coboundedI2 le_supI1)
next
  assume 1: "x ≤ y ⊔ L ∧ C x ≤ y ⊔ n(y) * top"
  hence "x ≤ y ⊔ (x ⊓ L)"
    using sup_commute sup_inf_distrib2 by force
  also have "... ≤ y ⊔ C x"
    using sup_right_isotone meet_L_below_C by blast
  also have "... ≤ y ⊔ n(y) * top"
    using 1 by simp
  finally have "x ≤ y ⊔ (L ⊓ n(y) * top)"
    using 1 by (simp add: sup_inf_distrib1)
  thus "x ≤ y"
    by (metis inf_commute n_L_decreasing order_trans sup_absorb1 n_vector_meet_L)
qed

text ‹AACP Theorem 3.31›

lemma n_L_decreasing_meet_L:
  "n(x) * L ≤ x ⊓ L"
  using n_sub_nL n_galois by auto

text ‹AACP Theorem 3.5›

lemma n_zero_L_zero:
  "n(bot) * L = bot"
  by (simp add: le_bot n_L_decreasing)

lemma n_L_top_below_L:
  "L * top ≤ L"
proof -
  have "n(L * bot) * L * top ≤ L * bot"
    by (metis dense_top_closed mult_isotone n_L_decreasing zero_vector mult_assoc)
  hence "n(L * bot) * L * top ≤ L"
    using order_lesseq_imp zero_right_mult_decreasing by blast
  hence "n(L) * L * top ≤ L"
    by (metis inf.absorb2 n_nL_meet_L_nL0 order.refl sup.absorb_iff1 top_right_mult_increasing mult_assoc)
  thus "L * top ≤ L"
    by (metis inf.absorb2 inf.sup_monoid.add_commute n_L_decreasing n_L_below_nL_top n_vector_meet_L)
qed

text ‹AACP Theorem 3.9›

lemma n_L_top_L:
  "L * top = L"
  by (simp add: order.antisym top_right_mult_increasing n_L_top_below_L)

text ‹AACP Theorem 3.10›

lemma n_L_below_L:
  "L * x ≤ L"
  by (metis mult_right_isotone top.extremum n_L_top_L)

text ‹AACP Theorem 3.7›

lemma n_nL_nT:
  "n(L) = n(top)"
  using order.eq_iff n_sub_nL n_add_left_top by auto

text ‹AACP Theorem 3.8›

lemma n_L_L:
  "n(L) * L = L"
  using order.antisym meet_L_below_n_L n_L_decreasing_meet_L by fastforce

lemma n_top_L:
  "n(top) * L = L"
  using n_L_L n_nL_nT by auto

text ‹AACP Theorem 3.23›

lemma n_n_L_split_n_L:
  "x * n(y) * L ≤ x * bot ⊔ n(x * y) * L"
  by (metis n_n_L_split_n_n_L_L n_L_decreasing mult_assoc mult_left_isotone mult_right_isotone n_isotone sup_right_isotone)

text ‹AACP Theorem 3.12›

lemma n_L_split_n_L_L:
  "x * L = x * bot ⊔ n(x * L) * L"
  apply (rule order.antisym)
  apply (metis mult_assoc n_n_L_split_n_L n_L_L)
  by (simp add: mult_right_isotone n_L_decreasing)

text ‹AACP Theorem 3.11›

lemma n_L_split_L:
  "x * L ≤ x * bot ⊔ L"
  by (metis n_n_L_split_n_n_L_L n_sub_nL sup_right_isotone mult_assoc n_L_L n_galois)

text ‹AACP Theorem 3.24›

lemma n_split_top:
  "x * n(y) * top ≤ x * y ⊔ n(x * y) * top"
proof -
  have "x * bot ⊔ n(x * y) * top ≤ x * y ⊔ n(x * y) * top"
    by (meson bot_least mult_isotone order.refl sup_left_isotone)
  thus ?thesis
    using order.trans n_n_top_split_n_top by blast
qed

text ‹AACP Theorem 3.9›

lemma n_L_L_L:
  "L * L = L"
  by (metis inf.sup_monoid.add_commute inf_absorb1 n_L_below_L n_L_top_L n_vector_meet_L)

text ‹AACP Theorem 3.9›

lemma n_L_top_L_L:
  "L * top * L = L"
  by (simp add: n_L_L_L n_L_top_L)

text ‹AACP Theorem 3.19›

lemma n_n_nL:
  "n(x) = n(x) * n(L)"
  by (simp add: n_export n_n_L)

lemma n_L_mult_idempotent:
  "n(L) * n(L) = n(L)"
  using n_n_nL by auto

text ‹AACP Theorem 3.22›

lemma n_n_L_n:
  "n(x * n(y) * L) ≤ n(x * y)"
  by (simp add: mult_right_isotone n_L_decreasing mult_assoc n_isotone)

text ‹AACP Theorem 3.3›

lemma n_less_eq_char:
  "x ≤ y ⟷ x ≤ y ⊔ L ∧ x ≤ y ⊔ n(y) * top"
  by (meson inf.coboundedI2 le_supI1 n_less_eq_char_n)

text ‹AACP Theorem 3.28›

lemma n_top_meet_L_split_L:
  "x * top * y ⊓ L ≤ x * bot ⊔ L * y"
proof -
  have "x * top * y ⊓ L ≤ x * bot ⊔ n(x * L) * L * y"
    by (smt n_top_meet_L_below_L mult_assoc n_L_L_L n_L_split_n_L_L mult_right_dist_sup mult_left_zero)
  also have "... ≤ x * bot ⊔ x * L * y"
    using mult_left_isotone n_L_decreasing sup_right_isotone by force
  also have "... ≤ x * bot ⊔ (x * bot ⊔ L) * y"
    using mult_left_isotone sup_right_isotone n_L_split_L by blast
  also have "... = x * bot ⊔ x * bot * y ⊔ L * y"
    by (simp add: mult_right_dist_sup sup_assoc)
  also have "... = x * bot ⊔ L * y"
    by (simp add: mult_assoc)
  finally show ?thesis
    .
qed

text ‹AACP Theorem 3.29›

lemma n_top_meet_L_L_meet_L:
  "x * top * y ⊓ L = x * L * y ⊓ L"
  apply (rule order.antisym)
  apply (simp add: n_top_meet_L_below_L)
  by (metis inf.sup_monoid.add_commute inf.sup_right_isotone mult_isotone order.refl top.extremum)

lemma n_n_top_below_n_L:
  "n(x * top) ≤ n(x * L)"
  by (meson order.trans n_L_decreasing_meet_L n_galois n_vector_meet_L)

text ‹AACP Theorem 3.14›

lemma n_n_top_n_L:
  "n(x * top) = n(x * L)"
  by (metis order.antisym mult_right_isotone n_isotone n_n_top_below_n_L top_greatest)

text ‹AACP Theorem 3.30›

lemma n_meet_L_0_below_0_meet_L:
  "(x ⊓ L) * bot ≤ x * bot ⊓ L"
  by (meson inf.boundedE inf.boundedI mult_right_sub_dist_inf_left zero_right_mult_decreasing)

text ‹AACP Theorem 3.15›

lemma n_n_L_below_L:
  "n(x) * L ≤ x * L"
  by (metis mult_assoc mult_left_isotone n_L_L_L n_L_decreasing)

lemma n_n_L_below_n_L_L:
  "n(x) * L ≤ n(x * L) * L"
  by (simp add: mult_left_isotone n_galois n_n_L_below_L)

text ‹AACP Theorem 3.16›

lemma n_below_n_L:
  "n(x) ≤ n(x * L)"
  by (simp add: n_galois n_n_L_below_L)

text ‹AACP Theorem 3.17›

lemma n_below_n_L_mult:
  "n(x) ≤ n(L) * n(x)"
  by (metis n_export order_trans meet_L_below_n_L n_L_decreasing_meet_L n_isotone n_n_L)

text ‹AACP Theorem 3.33›

lemma n_meet_L_below:
  "n(x) ⊓ L ≤ x"
  by (meson inf.coboundedI1 inf.coboundedI2 le_supI2 sup.cobounded1 top_right_mult_increasing n_less_eq_char)

text ‹AACP Theorem 3.35›

lemma n_meet_L_top_below_n_L:
  "(n(x) ⊓ L) * top ≤ n(x) * L"
proof -
  have "(n(x) ⊓ L) * top ≤ n(x) * top ⊓ L * top"
    by (meson mult_right_sub_dist_inf)
  thus ?thesis
    by (metis n_L_top_L n_vector_meet_L order_trans)
qed

text ‹AACP Theorem 3.34›

lemma n_meet_L_top_below:
  "(n(x) ⊓ L) * top ≤ x"
  using order.trans n_L_decreasing n_meet_L_top_below_n_L by blast

text ‹AACP Theorem 3.36›

lemma n_n_meet_L:
  "n(x) = n(x ⊓ L)"
  by (meson order.antisym inf.cobounded1 n_L_decreasing_meet_L n_galois n_isotone)

lemma n_T_below_n_meet:
  "n(x) * top = n(C x) * top"
  by (metis inf.absorb2 inf.sup_monoid.add_assoc meet_L_below_C n_n_meet_L)

text ‹AACP Theorem 3.44›

lemma n_C:
  "n(C x) = n(x)"
  by (metis n_T_below_n_meet n_export n_mult_right_one)

text ‹AACP Theorem 3.37›

lemma n_T_meet_L:
  "n(x) * top ⊓ L = n(x) * L"
  by (metis antisym_conv n_L_decreasing_meet_L n_n_L n_n_top_n_L n_vector_meet_L)

text ‹AACP Theorem 3.39›

lemma n_L_top_meet_L:
  "C L = L"
  by (simp add: n_L_L n_T_meet_L)

end

class n_algebra = left_n_algebra + idempotent_left_zero_semiring
begin

(* independence of axioms, checked in n_algebra without the respective axiom: *)
proposition n_dist_n_add            : "n(x) ⊔ n(y) = n(n(x) * top ⊔ y)" (* nitpick [expect=genuine,card=5] *) oops
proposition n_export                : "n(x) * n(y) = n(n(x) * y)" (* nitpick [expect=genuine,card=4] *) oops
proposition n_left_upper_bound      : "n(x) ≤ n(x ⊔ y)" (* nitpick [expect=genuine,card=5] *) oops
proposition n_nL_meet_L_nL0         : "n(L) * x = (x ⊓ L) ⊔ n(L * bot) * x" (* nitpick [expect=genuine,card=2] *) oops
proposition n_n_L_split_n_n_L_L     : "x * n(y) * L = x * bot ⊔ n(x * n(y) * L) * L" (* nitpick [expect=genuine,card=6] *) oops
proposition n_sub_nL                : "n(x) ≤ n(L)" (* nitpick [expect=genuine,card=2] *) oops
proposition n_L_decreasing          : "n(x) * L ≤ x" (* nitpick [expect=genuine,card=3] *) oops
proposition n_L_T_meet_mult_combined: "C (x * y) * z ≤ C x * y * C z" (* nitpick [expect=genuine,card=4] *) oops
proposition n_n_top_split_n_top     : "x * n(y) * top ≤ x * bot ⊔ n(x * y) * top" (* nitpick [expect=genuine,card=4] *) oops
proposition n_top_meet_L_below_L    : "x * top * y ⊓ L ≤ x * L * y" (* nitpick [expect=genuine,card=5] *) oops

text ‹AACP Theorem 3.25›

lemma n_top_split_0:
  "n(x) * top * y ≤ x * y ⊔ n(x * bot) * top"
proof -
  have 1: "n(x) * top * y ⊓ L ≤ x * y"
    using inf.coboundedI1 mult_left_isotone n_L_decreasing_meet_L n_top_meet_L_L_meet_L by force
  have "n(x) * top * y = n(x) * n(L) * top * y"
    using n_n_nL by auto
  also have "... = n(x) * ((top * y ⊓ L) ⊔ n(L * bot) * top * y)"
    by (metis mult_assoc n_nL_meet_L_nL0)
  also have "... ≤ n(x) * (top * y ⊓ L) ⊔ n(x) * n(L * bot) * top"
    by (metis sup_right_isotone mult_assoc mult_left_dist_sup mult_right_isotone top_greatest)
  also have "... ≤ (n(x) * top * y ⊓ L) ⊔ n(n(x) * L * bot) * top"
    by (smt sup_left_isotone order.trans inf_greatest mult_assoc mult_left_sub_dist_inf_left mult_left_sub_dist_inf_right n_export n_galois n_sub_nL)
  also have "... ≤ x * y ⊔ n(n(x) * L * bot) * top"
    using 1 sup_left_isotone by blast
  also have "... ≤ x * y ⊔ n(x * bot) * top"
    using mult_left_isotone n_galois n_isotone order.refl sup_right_isotone by auto
  finally show ?thesis
    .
qed

text ‹AACP Theorem 3.26›

lemma n_top_split:
  "n(x) * top * y ≤ x * y ⊔ n(x * y) * top"
  by (metis order.trans sup_bot_right mult_assoc sup_right_isotone mult_left_isotone mult_left_sub_dist_sup_right n_isotone n_top_split_0)

proposition n_zero: "n(bot) = bot" nitpick [expect=genuine,card=2] oops
proposition n_one: "n(1) = bot" nitpick [expect=genuine,card=2] oops
proposition n_nL_one: "n(L) = 1" nitpick [expect=genuine,card=2] oops
proposition n_nT_one: "n(top) = 1" nitpick [expect=genuine,card=2] oops
proposition n_n_zero: "n(x) = n(x * bot)" nitpick [expect=genuine,card=2] oops
proposition n_dist_add: "n(x) ⊔ n(y) = n(x ⊔ y)" nitpick [expect=genuine,card=4] oops
proposition n_L_split: "x * n(y) * L = x * bot ⊔ n(x * y) * L" nitpick [expect=genuine,card=3] oops
proposition n_split: "x ≤ x * bot ⊔ n(x * L) * top" nitpick [expect=genuine,card=2] oops
proposition n_mult_top_1: "n(x * y) ≤ n(x * n(y) * top)" nitpick [expect=genuine,card=3] oops
proposition l91_1: "n(L) * x ≤ n(x * top) * top" nitpick [expect=genuine,card=3] oops
proposition meet_domain_top: "x ⊓ n(y) * top = n(y) * x" nitpick [expect=genuine,card=3] oops
proposition meet_domain_2: "x ⊓ n(y) * top ≤ n(L) * x" nitpick [expect=genuine,card=4] oops
proposition n_nL_top_n_top_meet_L_top_2: "n(L) * x * top ≤ n(x * top ⊓ L) * top" nitpick [expect=genuine,card=3] oops
proposition n_nL_top_n_top_meet_L_top_1: "n(x * top ⊓ L) * top ≤ n(L) * x * top" nitpick [expect=genuine,card=2] oops
proposition l9: "x * bot ⊓ L ≤ n(x * L) * L" nitpick [expect=genuine,card=4] oops
proposition l18_2: "n(x * L) * L ≤ n(x) * L" nitpick [expect=genuine,card=3] oops
proposition l51_1: "n(x) * L ≤ (x ⊓ L) * bot" nitpick [expect=genuine,card=2] oops
proposition l51_2: "(x ⊓ L) * bot ≤ n(x) * L" nitpick [expect=genuine,card=4] oops

proposition n_split_equal: "x ⊔ n(x * L) * top = x * bot ⊔ n(x * L) * top" nitpick [expect=genuine,card=2] oops
proposition n_split_top: "x * top ≤ x * bot ⊔ n(x * L) * top" nitpick [expect=genuine,card=2] oops
proposition n_mult: "n(x * n(y) * L) = n(x * y)" nitpick [expect=genuine,card=3] oops
proposition n_mult_1: "n(x * y) ≤ n(x * n(y) * L)" nitpick [expect=genuine,card=3] oops
proposition n_mult_top: "n(x * n(y) * top) = n(x * y)" nitpick [expect=genuine,card=3] oops
proposition n_mult_right_upper_bound: "n(x * y) ≤ n(z) ⟷ n(x) ≤ n(z) ∧ x * n(y) * L ≤ x * bot ⊔ n(z) * L" nitpick [expect=genuine,card=2] oops
proposition meet_domain: "x ⊓ n(y) * z = n(y) * (x ⊓ z)" nitpick [expect=genuine,card=3] oops
proposition meet_domain_1: "x ⊓ n(y) * z ≤ n(y) * x" nitpick [expect=genuine,card=3] oops
proposition meet_domain_top_3: "x ⊓ n(y) * top ≤ n(y) * x" nitpick [expect=genuine,card=3] oops
proposition n_n_top_n_top_split_n_n_top_top: "n(x) * top ⊔ x * n(y) * top = x * bot ⊔ n(x * n(y) * top) * top" nitpick [expect=genuine,card=2] oops
proposition n_n_top_n_top_split_n_n_top_top_1: "x * bot ⊔ n(x * n(y) * top) * top ≤ n(x) * top ⊔ x * n(y) * top" nitpick [expect=genuine,card=5] oops
proposition n_n_top_n_top_split_n_n_top_top_2: "n(x) * top ⊔ x * n(y) * top ≤ x * bot ⊔ n(x * n(y) * top) * top" nitpick [expect=genuine,card=2] oops
proposition n_nL_top_n_top_meet_L_top: "n(L) * x * top = n(x * top ⊓ L) * top" nitpick [expect=genuine,card=2] oops
proposition l18: "n(x) * L = n(x * L) * L" nitpick [expect=genuine,card=3] oops
proposition l22: "x * bot ⊓ L = n(x) * L" nitpick [expect=genuine,card=2] oops
proposition l22_1: "x * bot ⊓ L = n(x * L) * L" nitpick [expect=genuine,card=2] oops
proposition l22_2: "x ⊓ L = n(x) * L" nitpick [expect=genuine,card=3] oops
proposition l22_3: "x ⊓ L = n(x * L) * L" nitpick [expect=genuine,card=3] oops
proposition l22_4: "x ⊓ L ≤ n(x) * L" nitpick [expect=genuine,card=3] oops
proposition l22_5: "x * bot ⊓ L ≤ n(x) * L" nitpick [expect=genuine,card=4] oops
proposition l23: "x * top ⊓ L = n(x) * L" nitpick [expect=genuine,card=3] oops
proposition l51: "n(x) * L = (x ⊓ L) * bot" nitpick [expect=genuine,card=2] oops
proposition l91: "x = x * top ⟶ n(L) * x ≤ n(x) * top" nitpick [expect=genuine,card=3] oops
proposition l92: "x = x * top ⟶ n(L) * x ≤ n(x ⊓ L) * top" nitpick [expect=genuine,card=3] oops
proposition "x ⊓ L ≤ n(x) * top" nitpick [expect=genuine,card=3] oops
proposition n_meet_comp: "n(x) ⊓ n(y) ≤ n(x) * n(y)" nitpick [expect=genuine,card=3] oops

proposition n_n_meet_L_n_zero: "n(x) = (n(x) ⊓ L) ⊔ n(x * bot)" oops
proposition n_below_n_zero: "n(x) ≤ x ⊔ n(x * bot)" oops
proposition n_n_top_split_n_L_n_zero_top: "n(x) * top = n(x) * L ⊔ n(x * bot) * top" oops
proposition n_meet_L_0_0_meet_L: "(x ⊓ L) * bot = x * bot ⊓ L" oops

end

end