Theory Binary_Iterings_Nonstrict

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

section ‹Nonstrict Binary Iterings›

theory Binary_Iterings_Nonstrict

imports Omega_Algebras Binary_Iterings

begin

class nonstrict_itering = bounded_left_zero_omega_algebra + while +
  assumes while_def: "x  y = xω  x * y"
begin

text ‹Theorem 8.2›

subclass bounded_binary_itering
proof (unfold_locales)
  fix x y z
  show "(x * y)  z = z  x * ((y * x)  (y * z))"
    by (metis sup_commute mult_assoc mult_left_dist_sup omega_loop_fixpoint omega_slide star.circ_slide while_def)
next
  fix x y z
  show "(x  y)  z = (x  y)  (x  z)"
  proof -
    have 1: "(x  y)  z = (x * y)ω  (x * y) * (xω  x * z)"
      using mult_left_dist_sup omega_decompose star.circ_sup_9 sup_assoc while_def mult_assoc by auto
    hence 2: "(x  y)  z  (x  y)  (x  z)"
      by (smt sup_mono sup_ge2 le_iff_sup mult_left_isotone omega_sub_dist star.circ_sub_dist while_def)
    let ?rhs = "x * y * ((xω  x * y)ω  (xω  x * y) * (xω  x * z))  (xω  x * z)"
    have "xω * (xω  x * y)ω  xω"
      by (simp add: omega_sub_vector)
    hence "xω * (xω  x * y)ω  x * y * (xω  x * y)ω  ?rhs"
      by (smt sup_commute sup_mono sup_ge1 mult_left_dist_sup order_trans)
    hence 3: "(xω  x * y)ω  ?rhs"
      by (metis mult_right_dist_sup omega_unfold)
    have "xω * (xω  x * y) * (xω  x * z)  xω"
      by (simp add: omega_mult_star_2 omega_sub_vector)
    hence "xω * (xω  x * y) * (xω  x * z)  x * y * (xω  x * y) * (xω  x * z)  ?rhs"
      by (smt sup_commute sup_mono sup_ge2 mult_assoc mult_left_dist_sup order_trans)
    hence "(xω  x * y) * (xω  x * z)  ?rhs"
      by (smt sup_assoc sup_ge2 le_iff_sup mult_assoc mult_right_dist_sup star.circ_loop_fixpoint)
    hence "(xω  x * y)ω  (xω  x * y) * (xω  x * z)  ?rhs"
      using 3 by simp
    hence "(xω  x * y)ω  (xω  x * y) * (xω  x * z)  (x * y)ω  (x * y) * (xω  x * z)"
      by (metis sup_commute omega_induct)
    thus ?thesis
      using 1 2 order.antisym while_def by force
  qed
next
  fix x y z
  show "x  (y  z) = (x  y)  (x  z)"
    using mult_left_dist_sup sup_assoc sup_commute while_def by auto
next
  fix x y z
  show "(x  y) * z  x  (y * z)"
    using mult_semi_associative omega_sub_vector semiring.add_mono semiring.distrib_right while_def by fastforce
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 "x * z  z * (y  1)  w"
    hence 1: "x * z  z * yω  z * y  w"
      by (metis mult_left_dist_sup mult_1_right while_def)
    let ?rhs = "z * (yω  y * v)  xω  x * w * (yω  y * v)"
    have 2: "z * v  ?rhs"
      by (metis le_supI1 mult_left_sub_dist_sup_right omega_loop_fixpoint)
    have "x * z * (yω  y * v)  ?rhs"
    proof -
      have "x * z * (yω  y * v)  (z * yω  z * y  w) * (yω  y * v)"
        using 1 mult_left_isotone by auto
      also have "... = z * (yω * (yω  y * v)  y * (yω  y * v))  w * (yω  y * v)"
        by (smt mult_assoc mult_left_dist_sup mult_right_dist_sup)
      also have "... = z * (yω * (yω  y * v)  yω  y * v)  w * (yω  y * v)"
        by (smt sup_assoc mult_assoc mult_left_dist_sup star.circ_transitive_equal star_mult_omega)
      also have "...  z * (yω  y * v)  x * w * (yω  y * v)"
        by (smt sup_commute sup_mono sup_left_top mult_left_dist_sup mult_left_one mult_right_dist_sup mult_right_sub_dist_sup_left omega_vector order_refl star.circ_plus_one)
      finally show ?thesis
        by (smt sup_assoc sup_commute le_iff_sup)
    qed
    hence "x * ?rhs  ?rhs"
      by (smt sup_assoc sup_commute sup_ge1 le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup omega_unfold star.circ_increasing star.circ_transitive_equal)
    hence "z * v  x * ?rhs  ?rhs"
      using 2 le_supI by blast
    hence "x * z * v  ?rhs"
      by (simp add: star_left_induct mult_assoc)
    hence "xω  x * z * v  ?rhs"
      by (meson order_trans sup_ge1 sup_ge2 sup_least)
    thus "x  (z * v)  z * (y  v)  (x  (w * (y  v)))"
      by (simp add: sup_assoc while_def mult_assoc)
  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 "z * x  y * (yω  y * z)  w"
      by (simp add: while_def)
    hence 1: "z * x  yω  y * y * z  w"
      using mult_left_dist_sup omega_unfold mult_assoc by auto
    let ?rhs = "yω  y * z * v  y * w * (xω  x * v)"
    have 2: "z * xω  ?rhs"
    proof -
      have "z * xω  y * y * z * xω  yω * xω  w * xω"
        using 1 by (smt sup_commute le_iff_sup mult_assoc mult_right_dist_sup omega_unfold)
      also have "...  y * y * z * xω  yω  w * xω"
        using omega_sub_vector semiring.add_mono by blast
      also have "... = y * y * (z * xω)  (yω  w * xω)"
        by (simp add: sup_assoc mult_assoc)
      finally have "z * xω  (y * y)ω  (y * y) * (yω  w * xω)"
        by (simp add: omega_induct sup_commute)
      also have "... = yω  y * w * xω"
        by (simp add: left_plus_omega semiring.distrib_left star.left_plus_circ star_mult_omega mult_assoc)
      also have "...  ?rhs"
        using mult_left_sub_dist_sup_left sup.mono sup_ge1 by blast
      finally show ?thesis
        .
    qed
    let ?rhs2 = "yω  y * z  y * w * (xω  x)"
    have "?rhs2 * x  ?rhs2"
    proof -
      have 3: "yω * x  ?rhs2"
        by (simp add: le_supI1 omega_sub_vector)
      have "y * z * x  y * (yω  y * y * z  w)"
        using 1 mult_right_isotone mult_assoc by auto
      also have "... = yω  y * y * y * z  y * w"
        by (simp add: semiring.distrib_left star_mult_omega mult_assoc)
      also have "... = yω  y * y * z  y * w"
        by (simp add: star.circ_plus_same star.circ_transitive_equal mult_assoc)
      also have "...  yω  y * z  y * w"
        by (metis sup_left_isotone sup_right_isotone mult_left_isotone star.left_plus_below_circ)
      also have "...  yω  y * z  y * w * x"
        using semiring.add_left_mono star.circ_back_loop_prefixpoint by auto
      finally have 4: "y * z * x  ?rhs2"
        using mult_left_sub_dist_sup_right order_lesseq_imp semiring.add_left_mono by blast
      have "(xω  x) * x  xω  x"
        using omega_sub_vector semiring.distrib_right star.left_plus_below_circ star_plus sup_mono by fastforce
      hence "y * w * (xω  x) * x  ?rhs2"
        by (simp add: le_supI2 mult_right_isotone mult_assoc)
      thus ?thesis
        using 3 4 mult_right_dist_sup by force
    qed
    hence "z  ?rhs2 * x  ?rhs2"
      by (metis omega_loop_fixpoint sup.boundedE sup_ge1 sup_least)
    hence 5: "z * x  ?rhs2"
      using star_right_induct by blast
    have "z * x * v  ?rhs"
    proof -
      have "z * x * v  ?rhs2 * v"
        using 5 mult_left_isotone by auto
      also have "... = yω * v  y * z * v  y * w * (xω * v  x * v)"
        using mult_right_dist_sup mult_assoc by auto
      also have "...  yω  y * z * v  y * w * (xω * v  x * v)"
        using omega_sub_vector semiring.add_right_mono by blast
      also have "...  ?rhs"
        using mult_right_isotone omega_sub_vector semiring.add_left_mono semiring.add_right_mono by auto
      finally show ?thesis
        .
    qed
    hence "z * (xω  x * v)  ?rhs"
      using 2 semiring.distrib_left mult_assoc by force
    thus "z * (x  v)  y  (z * v  w * (x  v))"
      by (simp add: semiring.distrib_left sup_assoc while_def mult_assoc)
  qed
qed

text ‹Theorem 13.8›

lemma while_top:
  "top  x = top"
  by (metis sup_left_top star.circ_top star_omega_top while_def)

text ‹Theorem 13.7›

lemma while_one_top:
  "1  x = top"
  by (simp add: omega_one while_def)

lemma while_finite_associative:
  "xω = bot  (x  y) * z = x  (y * z)"
  by (simp add: while_def mult_assoc)

lemma star_below_while:
  "x * y  x  y"
  by (simp add: while_def)

text ‹Theorem 13.9›

lemma while_sub_mult_one:
  "x * (1  y)  1  x"
  by (simp add: omega_one while_def)

lemma while_while_one:
  "y  (x  1) = yω  y * xω  y * x"
  using mult_left_dist_sup sup_assoc while_def by auto

lemma while_simulate_4_plus:
  assumes "y * x  x * (x  (1  y))"
    shows "y * x * x  x * (x  (1  y))"
proof -
  have 1: "x * (x  (1  y)) = xω  x * x  x * x * y"
    using mult_left_dist_sup omega_unfold sup_assoc while_def mult_assoc by force
  hence "y * x * x  (xω  x * x  x * x * y) * x"
    using assms mult_left_isotone by auto
  also have "... = xω * x  x * x * x  x * x * y * x"
    using mult_right_dist_sup by force
  also have "... = x * x * (y * x * x)  xω  x * x  x * x * y"
    by (smt sup_assoc sup_commute mult_assoc omega_mult_star_2 star.circ_back_loop_fixpoint star.circ_plus_same star.circ_transitive_equal)
  finally have "y * x * x  x * x * (y * x * x)  (xω  x * x  x * x * y)"
    using sup_assoc by force
  hence "y * x * x  (x * x)ω  (x * x) * (xω  x * x  x * x * y)"
    by (simp add: omega_induct sup_monoid.add_commute)
  also have "... = xω  x * (xω  x * x  x * x * y)"
    by (simp add: left_plus_omega star.left_plus_circ)
  finally show ?thesis
    using 1 by (metis while_def while_mult_star_exchange while_transitive)
qed

lemma while_simulate_4_omega:
  assumes "y * x  x * (x  (1  y))"
    shows "y * xω  xω"
proof -
  have "x * (x  (1  y)) = xω  x * x  x * x * y"
    using mult_1_right mult_left_dist_sup omega_unfold sup_assoc while_def mult_assoc by auto
  hence "y * 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ω  x * x * xω  x * x * y * xω"
    using semiring.distrib_right by auto
  also have "... = x * x * (y * xω)  xω"
    by (metis sup_commute le_iff_sup mult_assoc omega_sub_vector omega_unfold star_mult_omega)
  finally have "y * xω  x * x * (y * xω)  xω"
    .
  hence "y * xω  (x * x)ω  (x * x) * xω"
    by (simp add: omega_induct sup_commute)
  thus ?thesis
    by (metis sup_idem left_plus_omega star_mult_omega)
qed

text ‹Theorem 13.11›

lemma while_unfold_below:
  "x = z  y * x  x  y  z"
  by (simp add: omega_induct while_def)

text ‹Theorem 13.12›

lemma while_unfold_below_sub:
  "x  z  y * x  x  y  z"
  by (simp add: omega_induct while_def)

text ‹Theorem 13.10›

lemma while_unfold_below_1:
  "x = y * x  x  y  1"
  by (simp add: while_unfold_below_sub)

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 (simp add: while_unfold_below_sub)

lemma while_loop_is_greatest_postfixpoint:
  "is_greatest_postfixpoint (λx . y * x  z) (y  z)"
proof -
  have "(y  z)  (λx . y * x  z) (y  z)"
    using sup_commute while_left_unfold by force
  thus ?thesis
    by (simp add: is_greatest_postfixpoint_def sup_commute while_unfold_below_sub)
qed

lemma while_loop_is_greatest_fixpoint:
  "is_greatest_fixpoint (λx . y * x  z) (y  z)"
  by (simp add: omega_loop_is_greatest_fixpoint while_def)

proposition while_sumstar_4_below: "(x  y)  ((x  1) * z)  x  ((y * (x  1))  z)" nitpick [expect=genuine,card=6] oops
proposition while_sumstar_2: "(x  y)  z = x  ((y * (x  1))  z)" nitpick [expect=genuine,card=6] 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)" nitpick [expect=genuine,card=6] 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 "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

proposition while_mult_sub_while_while: "x  (y * z)  (x  y)  z" oops
proposition while_zero_zero: "(x  bot)  bot = x  bot" oops
proposition while_denest_3: "(x  w)  (x  bot) = (x  w)  bot" oops
proposition while_02: "x  ((x  w)  ((x  y) * z)) = (x  w)  ((x  y) * z)" oops
proposition while_sumstar_3_below: "(x  y)  (x  z)  (x  y)  ((x  1) * z)" oops
proposition while_sumstar_1: "(x  y)  z = (x  y)  ((x  1) * z)" oops
proposition while_denest_4: "(x  w)  (x  (y * z)) = (x  w)  ((x  y) * z)" oops

end

class nonstrict_itering_zero = nonstrict_itering +
  assumes mult_right_zero: "x * bot = bot"
begin

lemma while_finite_associative_2:
  "x  bot = bot  (x  y) * z = x  (y * z)"
  by (metis sup_bot_left sup_bot_right mult_assoc mult_right_zero while_def)

text ‹Theorem 13 counterexamples›

proposition while_mult_top: "(x * top)  z = z  x * top" nitpick [expect=genuine,card=3] oops
proposition tarski_mult_top_idempotent: "x * top = x * top * x * top" nitpick [expect=genuine,card=3] oops

proposition while_denest_0: "w * (x  (y * z))  (w * (x  y))  (w * (x  y) * z)" nitpick [expect=genuine,card=3] oops
proposition while_denest_1: "w * (x  (y * z))  (w * (x  y))  z" nitpick [expect=genuine,card=3] oops
proposition while_mult_zero_zero: "(x * (y  bot))  bot = x * (y  bot)" nitpick [expect=genuine,card=3] oops
proposition while_denest_2: "w * ((x  (y * w))  z) = w * (((x  y) * w)  z)" nitpick [expect=genuine,card=3] oops
proposition while_denest_5: "w * ((x  (y * w))  (x  (y * z))) = w * (((x  y) * w)  ((x  y) * z))" nitpick [expect=genuine,card=3] oops
proposition while_denest_6: "(w * (x  y))  z = z  w * ((x  y * w)  (y * z))" nitpick [expect=genuine,card=3] oops
proposition while_sum_below_one: "y * ((x  y)  z)  (y * (x  1))  z" nitpick [expect=genuine,card=3] oops
proposition while_separate_unfold: "(y * (x  1))  z = (y  z)  (y  (y * x * (x  ((y * (x  1))  z))))" nitpick [expect=genuine,card=3] oops

proposition while_sub_while_zero: "x  z  (x  y)  z" nitpick [expect=genuine,card=4] oops
proposition while_while_sub_associative: "x  (y  z)  (x  y)  z" nitpick [expect=genuine,card=4] oops
proposition tarski: "x  x * top * x * top" nitpick [expect=genuine,card=3] oops
proposition tarski_top_omega_below: "x * top  (x * top)ω" nitpick [expect=genuine,card=3] oops
proposition tarski_top_omega: "x * top = (x * top)ω" nitpick [expect=genuine,card=3] oops
proposition tarski_below_top_omega: "x  (x * top)ω" nitpick [expect=genuine,card=3] oops
proposition tarski_mult_omega_omega: "(x * yω)ω = x * yω" nitpick [expect=genuine,card=3] oops
proposition tarski_mult_omega_omega: "(z . zωω = zω)  (x * yω)ω = x * yω" nitpick [expect=genuine,card=3] oops
proposition tarski: "x = bot  top * x * top = top" nitpick [expect=genuine,card=3] oops

end

class nonstrict_itering_tarski = nonstrict_itering +
  assumes tarski: "x  x * top * x * top"
begin

text ‹Theorem 13.14›

lemma tarski_mult_top_idempotent:
  "x * top = x * top * x * top"
  by (metis sup_commute le_iff_sup mult_assoc star.circ_back_loop_fixpoint star.circ_left_top tarski top_mult_top)

lemma tarski_top_omega_below:
  "x * top  (x * top)ω"
  using omega_induct_mult order.refl mult_assoc tarski_mult_top_idempotent by auto

lemma tarski_top_omega:
  "x * top = (x * top)ω"
  by (simp add: order.eq_iff mult_top_omega tarski_top_omega_below)

lemma tarski_below_top_omega:
  "x  (x * top)ω"
  using top_right_mult_increasing tarski_top_omega by auto

lemma tarski_mult_omega_omega:
  "(x * yω)ω = x * yω"
  by (metis mult_assoc omega_vector tarski_top_omega)

lemma tarski_omega_idempotent:
  "xωω = xω"
  by (metis omega_vector tarski_top_omega)

lemma while_denest_2a:
  "w * ((x  (y * w))  z) = w * (((x  y) * w)  z)"
proof -
  have "(xω  x * y * w)ω = (x * y * w) * xω * (((x * y * w) * xω)ω  ((x * y * w) * xω) * (x * y * w)ω)  (x * y * w)ω"
    by (metis sup_commute omega_decompose omega_loop_fixpoint)
  also have "...  (x * y * w) * xω  (x * y * w)ω"
    by (metis sup_left_isotone mult_assoc mult_right_isotone omega_sub_vector)
  finally have 1: "w * (xω  x * y * w)ω  (w * x * y) * w * xω  (w * x * y)ω"
    by (smt sup_commute le_iff_sup mult_assoc mult_left_dist_sup while_def while_slide)
  have "(xω  x * y * w) * z = (x * y * w) * xω * ((x * y * w) * xω) * (x * y * w) * z  (x * y * w) * z"
    by (smt sup_commute mult_assoc star.circ_sup star.circ_loop_fixpoint)
  also have "...  (x * y * w) * xω  (x * y * w) * z"
    by (smt sup_commute sup_right_isotone mult_assoc mult_right_isotone omega_sub_vector)
  finally have "w * (xω  x * y * w) * z  (w * x * y) * w * xω  (w * x * y) * w * z"
    by (metis mult_assoc mult_left_dist_sup mult_right_isotone star.circ_slide)
  hence "w * (xω  x * y * w)ω  w * (xω  x * y * w) * z  (w * x * y) * (w * xω)ω  (w * x * y)ω  (w * x * y) * w * z"
    using 1 by (smt sup_assoc sup_commute le_iff_sup mult_assoc tarski_mult_omega_omega)
  also have "...  (w * xω  w * x * y) * (w * xω  w * x * y)ω  (w * xω  w * x * y)ω  (w * xω  w * x * y) * w * z"
    by (metis sup_mono sup_ge1 sup_ge2 mult_isotone mult_left_isotone omega_isotone star.circ_isotone)
  also have "... = (w * xω  w * x * y)ω  (w * xω  w * x * y) * w * z"
    by (simp add: star_mult_omega)
  finally have "w * ((xω  x * y * w)ω  (xω  x * y * w) * z)  w * ((xω  x * y) * w)ω  w * ((xω  x * y) * w) * z"
    by (smt mult_assoc mult_left_dist_sup omega_slide star.circ_slide)
  hence 2: "w * ((x  (y * w))  z)  w * (((x  y) * w)  z)"
    by (simp add: mult_left_dist_sup while_def mult_assoc)
  have "w * (((x  y) * w)  z)  w * ((x  (y * w))  z)"
    by (simp add: mult_right_isotone while_left_isotone while_sub_associative)
  thus ?thesis
    using 2 order.antisym by auto
qed

lemma while_denest_3:
  "(x  w)  xω = (x  w)ω"
proof -
  have 1: "(x  w)  xω = (x  w)ω  (x  w) * xωω"
    by (simp add: while_def tarski_omega_idempotent)
  also have "...  (x  w)ω  (x  w) * (xω  x * w)ω"
    using mult_right_isotone omega_sub_dist semiring.add_left_mono by blast
  also have "... = (x  w)ω"
    by (simp add: star_mult_omega while_def)
  finally show ?thesis
    using 1 by (simp add: sup.order_iff)
qed

lemma while_denest_4a:
  "(x  w)  (x  (y * z)) = (x  w)  ((x  y) * z)"
proof -
  have "(x  w)  (x  (y * z)) = (x  w)ω  ((x  w)  (x * y * z))"
    using while_def while_denest_3 while_left_dist_sup mult_assoc by auto
  also have "...  (x  w)ω  ((x  w)  ((x  y) * z))"
    using mult_right_sub_dist_sup_right order.refl semiring.add_mono while_def while_right_isotone by auto
  finally have 1: "(x  w)  (x  (y * z))  (x  w)  ((x  y) * z)"
    by (simp add: while_def)
  have "(x  w)  ((x  y) * z)  (x  w)  (x  (y * z))"
    by (simp add: while_right_isotone while_sub_associative)
  thus ?thesis
    using 1 order.antisym by auto
qed

text ‹Theorem 8.3›

subclass bounded_extended_binary_itering
  apply unfold_locales
  by (smt mult_assoc while_denest_2a while_denest_4a while_increasing while_slide)

text ‹Theorem 13.13›

lemma while_mult_top:
  "(x * top)  z = z  x * top"
proof -
  have 1: "z  x * top  (x * top)  z"
    by (metis le_supI sup_ge1 while_def while_increasing tarski_top_omega)
  have "(x * top)  z = z  x * top * ((x * top)  z)"
    using while_left_unfold by auto
  also have "...  z  x * top"
    using mult_right_isotone sup_right_isotone top_greatest mult_assoc by auto
  finally show ?thesis
    using 1 order.antisym by auto
qed

lemma tarski_top_omega_below_2:
  "x * top  (x * top)  bot"
  by (simp add: while_mult_top)

lemma tarski_top_omega_2:
  "x * top = (x * top)  bot"
  by (simp add: while_mult_top)

lemma tarski_below_top_omega_2:
  "x  (x * top)  bot"
  using top_right_mult_increasing tarski_top_omega_2 by auto

proposition "1 = (x * bot)  1" nitpick [expect=genuine,card=3] oops

end

class nonstrict_itering_tarski_zero = nonstrict_itering_tarski + nonstrict_itering_zero
begin

lemma while_bot_1:
  "1 = (x * bot)  1"
  by (simp add: mult_right_zero while_zero)

text ‹Theorem 13 counterexamples›

proposition while_associative: "(x  y) * z = x  (y * z)" nitpick [expect=genuine,card=2] oops
proposition "(x  1) * y = x  y" nitpick [expect=genuine,card=2] oops
proposition while_one_mult: "(x  1) * x = x  x" nitpick [expect=genuine,card=4] oops
proposition "(x  y)  z = ((x  1) * y)  ((x  1) * 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_top_2: "top  z = top * z" nitpick [expect=genuine,card=2] oops

proposition tarski: "x = bot  top * x * top = top" nitpick [expect=genuine,card=3] 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 tarski: "x = bot  top * x * top = top" nitpick [expect=genuine,card=3] oops
proposition tarski_case: assumes t1: "x = bot  P x" and t2: "top * x * top = top  P x" shows "P x" nitpick [expect=genuine,card=3] oops

end

end