[STATEMENT]
lemma diamond_L_isotone:
  "w \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> \<parallel>w\<guillemotright>x \<le> \<parallel>y\<guillemotright>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> \<parallel> w \<guillemotright> x \<le> \<parallel> y \<guillemotright> z
[PROOF STEP]
using diamond_L_ni mult_isotone ni_isotone
[PROOF STATE]
proof (prove)
using this:
\<parallel> ?x \<guillemotright> ?y = ni (?x * ?y)
\<lbrakk>?w \<le> ?y; ?x \<le> ?z\<rbrakk> \<Longrightarrow> ?w * ?x \<le> ?y * ?z
?x \<le> ?y \<Longrightarrow> ni ?x \<le> ni ?y

goal (1 subgoal):
 1. \<lbrakk>w \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> \<parallel> w \<guillemotright> x \<le> \<parallel> y \<guillemotright> z
[PROOF STEP]
by force


[STATEMENT]
lemma box_diamond:
  "|x]y = an( |x>an(y * L) * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] y = an (| x > an (y * L) * L)
[PROOF STEP]
by (simp add: an_n_L nbox_def ndiamond_def)


[STATEMENT]
lemma diamond_box:
  "|x>y = an( |x]an(y * L) * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > y = an (| x ] an (y * L) * L)
[PROOF STEP]
using n_an_def n_mult nbox_def ndiamond_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
n ?x = an (an ?x * L)
n (?x * n ?y * L) = n (?x * ?y)
| ?x ] ?y = an (?x * an (?y * L) * L)
| ?x > ?y = n (?x * ?y * L)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | x > y = an (| x ] an (y * L) * L)
[PROOF STEP]
by force


[STATEMENT]
lemma box_x_bot:
  "|x]bot = an(x * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] bot = an (x * L)
[PROOF STEP]
by (simp add: an_bot nbox_def)


[STATEMENT]
lemma box_x_1:
  "|x]1 = an(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (1::'a) = an x
[PROOF STEP]
using an_L an_mult_an nbox_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
an L = bot
an (?x * an ?y) = an ?x
| ?x ] ?y = an (?x * an (?y * L) * L)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | x ] (1::'a) = an x
[PROOF STEP]
by auto


[STATEMENT]
lemma box_x_L:
  "|x]L = an(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] L = an x
[PROOF STEP]
using box_x_1 L_left_zero nbox_def
[PROOF STATE]
proof (prove)
using this:
| ?x ] (1::'a) = an ?x
L * ?x = L
| ?x ] ?y = an (?x * an (?y * L) * L)

goal (1 subgoal):
 1. | x ] L = an x
[PROOF STEP]
by auto


[STATEMENT]
lemma box_x_top:
  "|x]top = an(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] top = an x
[PROOF STEP]
by (metis box_diamond box_x_1 box_x_bot diamond_top_y)


[STATEMENT]
lemma box_x_n:
  "|x]n(y) = an(x * an(y) * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] n y = an (x * an y * L)
[PROOF STEP]
by (simp add: an_n_L nbox_def)


[STATEMENT]
lemma box_x_an:
  "|x]an(y) = an(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] an y = an (x * y)
[PROOF STEP]
using an_mult n_an_def nbox_def
[PROOF STATE]
proof (prove)
using this:
an (?x * n ?y * L) = an (?x * ?y)
n ?x = an (an ?x * L)
| ?x ] ?y = an (?x * an (?y * L) * L)

goal (1 subgoal):
 1. | x ] an y = an (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_bot_y:
  "|bot]y = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | bot ] y = (1::'a)
[PROOF STEP]
by (simp add: an_bot nbox_def)


[STATEMENT]
lemma box_1_y:
  "|1]y = n(y * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) ] y = n (y * L)
[PROOF STEP]
by (simp add: n_an_def nbox_def)


[STATEMENT]
lemma box_1_n:
  "|1]n(y) = n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) ] n y = n y
[PROOF STEP]
using box_1_y diamond_1_n diamond_1_y
[PROOF STATE]
proof (prove)
using this:
| (1::'a) ] ?y = n (?y * L)
| (1::'a) > n ?y = n ?y
| (1::'a) > ?y = n (?y * L)

goal (1 subgoal):
 1. | (1::'a) ] n y = n y
[PROOF STEP]
by auto


[STATEMENT]
lemma box_1_an:
  "|1]an(y) = an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) ] an y = an y
[PROOF STEP]
by (simp add: box_x_an)


[STATEMENT]
lemma box_L_y:
  "|L]y = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | L ] y = bot
[PROOF STEP]
by (simp add: L_left_zero an_L nbox_def)


[STATEMENT]
lemma box_top_y:
  "|top]y = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | top ] y = bot
[PROOF STEP]
by (simp add: box_diamond an_L diamond_top_y)


[STATEMENT]
lemma box_n_y:
  "|n(x)]y = an(x) \<squnion> n(y * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x ] y = an x \<squnion> n (y * L)
[PROOF STEP]
using an_export_n n_an_def nbox_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
an (n ?x * ?y) = an ?x \<squnion> an ?y
n ?x = an (an ?x * L)
| ?x ] ?y = an (?x * an (?y * L) * L)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | n x ] y = an x \<squnion> n (y * L)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_an_y:
  "|an(x)]y = n(x) \<squnion> n(y * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x ] y = n x \<squnion> n (y * L)
[PROOF STEP]
by (metis an_n_def box_n_y n_an_def)


[STATEMENT]
lemma box_n_bot:
  "|n(x)]bot = an(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x ] bot = an x
[PROOF STEP]
by (simp add: box_x_bot an_n_L)


[STATEMENT]
lemma box_an_bot:
  "|an(x)]bot = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x ] bot = n x
[PROOF STEP]
by (simp add: box_x_bot n_an_def)


[STATEMENT]
lemma box_n_1:
  "|n(x)]1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x ] (1::'a) = (1::'a)
[PROOF STEP]
using box_x_1 ani_an_L ani_n
[PROOF STATE]
proof (prove)
using this:
| ?x ] (1::'a) = an ?x
(ani ?x = L) = (an ?x = (1::'a))
ani (n ?x) = L

goal (1 subgoal):
 1. | n x ] (1::'a) = (1::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_an_1:
  "|an(x)]1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x ] (1::'a) = (1::'a)
[PROOF STEP]
using box_x_1 ani_an ani_an_L
[PROOF STATE]
proof (prove)
using this:
| ?x ] (1::'a) = an ?x
ani (an ?x) = L
(ani ?x = L) = (an ?x = (1::'a))

goal (1 subgoal):
 1. | an x ] (1::'a) = (1::'a)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma box_n_n:
  "|n(x)]n(y) = an(x) \<squnion> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x ] n y = an x \<squnion> n y
[PROOF STEP]
using box_1_n box_1_y box_n_y
[PROOF STATE]
proof (prove)
using this:
| (1::'a) ] n ?y = n ?y
| (1::'a) ] ?y = n (?y * L)
| n ?x ] ?y = an ?x \<squnion> n (?y * L)

goal (1 subgoal):
 1. | n x ] n y = an x \<squnion> n y
[PROOF STEP]
by auto


[STATEMENT]
lemma box_an_n:
  "|an(x)]n(y) = n(x) \<squnion> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x ] n y = n x \<squnion> n y
[PROOF STEP]
using box_x_n an_dist_sup n_an_def n_dist_sup
[PROOF STATE]
proof (prove)
using this:
| ?x ] n ?y = an (?x * an ?y * L)
an (?x \<squnion> ?y) = an ?x * an ?y
n ?x = an (an ?x * L)
n (?x \<squnion> ?y) = n ?x \<squnion> n ?y

goal (1 subgoal):
 1. | an x ] n y = n x \<squnion> n y
[PROOF STEP]
by auto


[STATEMENT]
lemma box_n_an:
  "|n(x)]an(y) = an(x) \<squnion> an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x ] an y = an x \<squnion> an y
[PROOF STEP]
by (simp add: box_x_an an_export_n)


[STATEMENT]
lemma box_an_an:
  "|an(x)]an(y) = n(x) \<squnion> an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x ] an y = n x \<squnion> an y
[PROOF STEP]
by (simp add: box_x_an an_export)


[STATEMENT]
lemma box_n_n_same:
  "|n(x)]n(x) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x ] n x = (1::'a)
[PROOF STEP]
by (simp add: box_n_n an_complement)


[STATEMENT]
lemma box_an_an_same:
  "|an(x)]an(x) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x ] an x = (1::'a)
[PROOF STEP]
using box_an_bot an_bot an_complement_bot nbox_def
[PROOF STATE]
proof (prove)
using this:
| an ?x ] bot = n ?x
an bot = (1::'a)
an ?x * n ?x = bot
| ?x ] ?y = an (?x * an (?y * L) * L)

goal (1 subgoal):
 1. | an x ] an x = (1::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_left_dist_sup:
  "|x \<squnion> y]z = |x]z * |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x \<squnion> y ] z = | x ] z * | y ] z
[PROOF STEP]
using an_dist_sup nbox_def semiring.distrib_right
[PROOF STATE]
proof (prove)
using this:
an (?x \<squnion> ?y) = an ?x * an ?y
| ?x ] ?y = an (?x * an (?y * L) * L)
(?a \<squnion> ?b) * ?c = ?a * ?c \<squnion> ?b * ?c

goal (1 subgoal):
 1. | x \<squnion> y ] z = | x ] z * | y ] z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_right_dist_sup:
  "|x](y \<squnion> z) = an(x * an(y * L) * an(z * L) * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (y \<squnion> z) = an (x * an (y * L) * an (z * L) * L)
[PROOF STEP]
by (simp add: an_dist_sup mult_right_dist_sup nbox_def mult_assoc)


[STATEMENT]
lemma box_associative:
  "|x * y]z = an(x * y * an(z * L) * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * y ] z = an (x * y * an (z * L) * L)
[PROOF STEP]
by (simp add: nbox_def)


[STATEMENT]
lemma box_left_mult:
  "|x * y]z = |x]|y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * y ] z = | x ] | y ] z
[PROOF STEP]
using box_x_an nbox_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
| ?x ] an ?y = an (?x * ?y)
| ?x ] ?y = an (?x * an (?y * L) * L)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | x * y ] z = | x ] | y ] z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_right_mult:
  "|x](y * z) = an(x * an(y * z * L) * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (y * z) = an (x * an (y * z * L) * L)
[PROOF STEP]
by (simp add: nbox_def)


[STATEMENT]
lemma box_right_mult_n_n:
  "|x](n(y) * n(z)) = |x]n(y) * |x]n(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (n y * n z) = | x ] n y * | x ] n z
[PROOF STEP]
by (smt an_dist_sup an_export_n an_n_L mult_assoc mult_left_dist_sup mult_right_dist_sup nbox_def)


[STATEMENT]
lemma box_right_mult_an_n:
  "|x](an(y) * n(z)) = |x]an(y) * |x]n(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (an y * n z) = | x ] an y * | x ] n z
[PROOF STEP]
by (metis an_n_def box_right_mult_n_n)


[STATEMENT]
lemma box_right_mult_n_an:
  "|x](n(y) * an(z)) = |x]n(y) * |x]an(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (n y * an z) = | x ] n y * | x ] an z
[PROOF STEP]
by (simp add: box_right_mult_an_n box_x_an box_x_n an_mult_commutative n_an_mult_commutative)


[STATEMENT]
lemma box_right_mult_an_an:
  "|x](an(y) * an(z)) = |x]an(y) * |x]an(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (an y * an z) = | x ] an y * | x ] an z
[PROOF STEP]
by (metis an_dist_sup box_x_an mult_left_dist_sup)


[STATEMENT]
lemma box_n_export:
  "|n(x) * y]z = an(x) \<squnion> |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x * y ] z = an x \<squnion> | y ] z
[PROOF STEP]
using box_left_mult box_n_an nbox_def
[PROOF STATE]
proof (prove)
using this:
| ?x * ?y ] ?z = | ?x ] | ?y ] ?z
| n ?x ] an ?y = an ?x \<squnion> an ?y
| ?x ] ?y = an (?x * an (?y * L) * L)

goal (1 subgoal):
 1. | n x * y ] z = an x \<squnion> | y ] z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_an_export:
  "|an(x) * y]z = n(x) \<squnion> |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x * y ] z = n x \<squnion> | y ] z
[PROOF STEP]
using box_an_an box_left_mult nbox_def
[PROOF STATE]
proof (prove)
using this:
| an ?x ] an ?y = n ?x \<squnion> an ?y
| ?x * ?y ] ?z = | ?x ] | ?y ] ?z
| ?x ] ?y = an (?x * an (?y * L) * L)

goal (1 subgoal):
 1. | an x * y ] z = n x \<squnion> | y ] z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_left_antitone:
  "y \<le> x \<Longrightarrow> |x]z \<le> |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> x \<Longrightarrow> | x ] z \<le> | y ] z
[PROOF STEP]
by (smt an_mult_commutative an_order box_diamond box_left_dist_sup le_iff_sup)


[STATEMENT]
lemma box_right_isotone:
  "y \<le> z \<Longrightarrow> |x]y \<le> |x]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> z \<Longrightarrow> | x ] y \<le> | x ] z
[PROOF STEP]
by (metis an_antitone mult_left_isotone mult_right_isotone nbox_def)


[STATEMENT]
lemma box_antitone_isotone:
  "y \<le> w \<Longrightarrow> x \<le> z \<Longrightarrow> |w]x \<le> |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<le> w; x \<le> z\<rbrakk> \<Longrightarrow> | w ] x \<le> | y ] z
[PROOF STEP]
by (meson box_left_antitone box_right_isotone order.trans)


[STATEMENT]
lemma nbox_to_L:
  "\<parallel>x\<rbrakk>y = |x]n(y) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x \<rbrakk> y = | x ] n y * L
[PROOF STEP]
by (simp add: box_x_n nbox_L_def)


[STATEMENT]
lemma nbox_from_L:
  "|x]y = n(\<parallel>x\<rbrakk>(y * L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] y = n (\<parallel> x \<rbrakk> (y * L))
[PROOF STEP]
using an_n_def nbox_def nbox_L_def
[PROOF STATE]
proof (prove)
using this:
an ?x = n (an ?x * L)
| ?x ] ?y = an (?x * an (?y * L) * L)
\<parallel> ?x \<rbrakk> ?y \<equiv> an (?x * an ?y * L) * L

goal (1 subgoal):
 1. | x ] y = n (\<parallel> x \<rbrakk> (y * L))
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_x_an:
  "|x>an(y) = n(x * an(y) * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > an y = n (x * an y * L)
[PROOF STEP]
by (simp add: ndiamond_def)


[STATEMENT]
lemma diamond_1_an:
  "|1>an(y) = an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) > an y = an y
[PROOF STEP]
using box_1_an box_1_y diamond_1_y
[PROOF STATE]
proof (prove)
using this:
| (1::'a) ] an ?y = an ?y
| (1::'a) ] ?y = n (?y * L)
| (1::'a) > ?y = n (?y * L)

goal (1 subgoal):
 1. | (1::'a) > an y = an y
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_an_y:
  "|an(x)>y = an(x) * n(y * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x > y = an x * n (y * L)
[PROOF STEP]
by (simp add: n_export_an ndiamond_def mult_assoc)


[STATEMENT]
lemma diamond_an_bot:
  "|an(x)>bot = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x > bot = bot
[PROOF STEP]
by (simp add: an_mult_right_zero n_bot ndiamond_def)


[STATEMENT]
lemma diamond_an_1:
  "|an(x)>1 = an(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x > (1::'a) = an x
[PROOF STEP]
using an_n_def diamond_x_1
[PROOF STATE]
proof (prove)
using this:
an ?x = n (an ?x * L)
| ?x > (1::'a) = n (?x * L)

goal (1 subgoal):
 1. | an x > (1::'a) = an x
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_an_n:
  "|an(x)>n(y) = an(x) * n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x > n y = an x * n y
[PROOF STEP]
by (simp add: diamond_x_n n_export_an)


[STATEMENT]
lemma diamond_n_an:
  "|n(x)>an(y) = n(x) * an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x > an y = n x * an y
[PROOF STEP]
using an_n_def diamond_n_y
[PROOF STATE]
proof (prove)
using this:
an ?x = n (an ?x * L)
| n ?x > ?y = n ?x * n (?y * L)

goal (1 subgoal):
 1. | n x > an y = n x * an y
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_an_an:
  "|an(x)>an(y) = an(x) * an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x > an y = an x * an y
[PROOF STEP]
using diamond_an_y an_n_def
[PROOF STATE]
proof (prove)
using this:
| an ?x > ?y = an ?x * n (?y * L)
an ?x = n (an ?x * L)

goal (1 subgoal):
 1. | an x > an y = an x * an y
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_an_an_same:
  "|an(x)>an(x) = an(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x > an x = an x
[PROOF STEP]
by (simp add: diamond_an_an an_mult_idempotent)


[STATEMENT]
lemma diamond_an_export:
  "|an(x) * y>z = an(x) * |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | an x * y > z = an x * | y > z
[PROOF STEP]
using diamond_an_an diamond_box diamond_left_mult
[PROOF STATE]
proof (prove)
using this:
| an ?x > an ?y = an ?x * an ?y
| ?x > ?y = an (| ?x ] an (?y * L) * L)
| ?x * ?y > ?z = | ?x > | ?y > ?z

goal (1 subgoal):
 1. | an x * y > z = an x * | y > z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_ani:
  "|x]y = an(x * ani(y * L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] y = an (x * ani (y * L))
[PROOF STEP]
by (simp add: ani_def nbox_def mult_assoc)


[STATEMENT]
lemma box_x_n_ani:
  "|x]n(y) = an(x * ani(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] n y = an (x * ani y)
[PROOF STEP]
by (simp add: box_x_n ani_def mult_assoc)


[STATEMENT]
lemma box_L_ani:
  "\<parallel>x\<rbrakk>y = ani(x * ani(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x \<rbrakk> y = ani (x * ani y)
[PROOF STEP]
using box_x_n_ani ani_def nbox_to_L
[PROOF STATE]
proof (prove)
using this:
| ?x ] n ?y = an (?x * ani ?y)
ani ?x \<equiv> an ?x * L
\<parallel> ?x \<rbrakk> ?y = | ?x ] n ?y * L

goal (1 subgoal):
 1. \<parallel> x \<rbrakk> y = ani (x * ani y)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_L_left_mult:
  "\<parallel>x * y\<rbrakk>z = \<parallel>x\<rbrakk>\<parallel>y\<rbrakk>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x * y \<rbrakk> z = \<parallel> x \<rbrakk> \<parallel> y \<rbrakk> z
[PROOF STEP]
using an_mult n_an_def mult_assoc nbox_L_def
[PROOF STATE]
proof (prove)
using this:
an (?x * n ?y * L) = an (?x * ?y)
n ?x = an (an ?x * L)
?a * ?b * ?c = ?a * (?b * ?c)
\<parallel> ?x \<rbrakk> ?y \<equiv> an (?x * an ?y * L) * L

goal (1 subgoal):
 1. \<parallel> x * y \<rbrakk> z = \<parallel> x \<rbrakk> \<parallel> y \<rbrakk> z
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_x_an_ani:
  "|x>an(y) = n(x * ani(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > an y = n (x * ani y)
[PROOF STEP]
by (simp add: ani_def ndiamond_def mult_assoc)


[STATEMENT]
lemma box_L_left_antitone:
  "y \<le> x \<Longrightarrow> \<parallel>x\<rbrakk>z \<le> \<parallel>y\<rbrakk>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> x \<Longrightarrow> \<parallel> x \<rbrakk> z \<le> \<parallel> y \<rbrakk> z
[PROOF STEP]
by (simp add: box_L_ani ani_antitone mult_left_isotone)


[STATEMENT]
lemma box_L_right_isotone:
  "y \<le> z \<Longrightarrow> \<parallel>x\<rbrakk>y \<le> \<parallel>x\<rbrakk>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> z \<Longrightarrow> \<parallel> x \<rbrakk> y \<le> \<parallel> x \<rbrakk> z
[PROOF STEP]
using ani_antitone ani_def mult_right_isotone mult_assoc nbox_L_def
[PROOF STATE]
proof (prove)
using this:
?y \<le> ?x \<Longrightarrow> ani ?x \<le> ani ?y
ani ?x \<equiv> an ?x * L
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
?a * ?b * ?c = ?a * (?b * ?c)
\<parallel> ?x \<rbrakk> ?y \<equiv> an (?x * an ?y * L) * L

goal (1 subgoal):
 1. y \<le> z \<Longrightarrow> \<parallel> x \<rbrakk> y \<le> \<parallel> x \<rbrakk> z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_L_antitone_isotone:
  "y \<le> w \<Longrightarrow> x \<le> z \<Longrightarrow> \<parallel>w\<rbrakk>x \<le> \<parallel>y\<rbrakk>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<le> w; x \<le> z\<rbrakk> \<Longrightarrow> \<parallel> w \<rbrakk> x \<le> \<parallel> y \<rbrakk> z
[PROOF STEP]
using ani_antitone ani_def mult_isotone mult_assoc nbox_L_def
[PROOF STATE]
proof (prove)
using this:
?y \<le> ?x \<Longrightarrow> ani ?x \<le> ani ?y
ani ?x \<equiv> an ?x * L
\<lbrakk>?w \<le> ?y; ?x \<le> ?z\<rbrakk> \<Longrightarrow> ?w * ?x \<le> ?y * ?z
?a * ?b * ?c = ?a * (?b * ?c)
\<parallel> ?x \<rbrakk> ?y \<equiv> an (?x * an ?y * L) * L

goal (1 subgoal):
 1. \<lbrakk>y \<le> w; x \<le> z\<rbrakk> \<Longrightarrow> \<parallel> w \<rbrakk> x \<le> \<parallel> y \<rbrakk> z
[PROOF STEP]
by force


[STATEMENT]
lemma diamond_omega:
  "|x\<^sup>\<omega>>y = |x\<^sup>\<omega>>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> > y = | x\<^sup>\<omega> > z
[PROOF STEP]
by (simp add: n_omega_mult ndiamond_def mult_assoc)


[STATEMENT]
lemma box_omega:
  "|x\<^sup>\<omega>]y = |x\<^sup>\<omega>]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> ] y = | x\<^sup>\<omega> ] z
[PROOF STEP]
by (metis box_diamond diamond_omega)


[STATEMENT]
lemma an_box_omega_induct:
  "|x]an(y) * n(z * L) \<le> an(y) \<Longrightarrow> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]z \<le> an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] an y * n (z * L) \<le> an y \<Longrightarrow> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] z \<le> an y
[PROOF STEP]
by (smt an_dist_sup an_omega_induct an_omega_mult box_left_dist_sup box_x_an mult_assoc n_an_def nbox_def)


[STATEMENT]
lemma n_box_omega_induct:
  "|x]n(y) * n(z * L) \<le> n(y) \<Longrightarrow> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]z \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] n y * n (z * L) \<le> n y \<Longrightarrow> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] z \<le> n y
[PROOF STEP]
by (simp add: an_box_omega_induct n_an_def)


[STATEMENT]
lemma an_box_omega_induct_an:
  "|x]an(y) * an(z) \<le> an(y) \<Longrightarrow> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(z) \<le> an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] an y * an z \<le> an y \<Longrightarrow> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an z \<le> an y
[PROOF STEP]
using an_box_omega_induct an_n_def
[PROOF STATE]
proof (prove)
using this:
| ?x ] an ?y * n (?z * L) \<le> an ?y \<Longrightarrow> | ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> ] ?z \<le> an ?y
an ?x = n (an ?x * L)

goal (1 subgoal):
 1. | x ] an y * an z \<le> an y \<Longrightarrow> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an z \<le> an y
[PROOF STEP]
by auto


[STATEMENT]
lemma n_box_omega_induct_n:
  "|x]n(y) * n(z) \<le> n(y) \<Longrightarrow> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]n(z) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] n y * n z \<le> n y \<Longrightarrow> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n z \<le> n y
[PROOF STEP]
using an_box_omega_induct_an n_an_def
[PROOF STATE]
proof (prove)
using this:
| ?x ] an ?y * an ?z \<le> an ?y \<Longrightarrow> | ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> ] an ?z \<le> an ?y
n ?x = an (an ?x * L)

goal (1 subgoal):
 1. | x ] n y * n z \<le> n y \<Longrightarrow> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n z \<le> n y
[PROOF STEP]
by force


[STATEMENT]
lemma n_diamond_omega_induct:
  "n(y) \<le> |x>n(y) \<squnion> n(z * L) \<Longrightarrow> n(y) \<le> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y \<le> | x > n y \<squnion> n (z * L) \<Longrightarrow> n y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > z
[PROOF STEP]
using diamond_x_n mult_right_dist_sup n_dist_sup n_omega_induct n_omega_mult ndiamond_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
| ?x > n ?y = n (?x * ?y)
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z
n (?x \<squnion> ?y) = n ?x \<squnion> n ?y
n ?y \<le> n (?x * ?y \<squnion> ?z) \<Longrightarrow> n ?y \<le> n (?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> * ?z)
n (?x\<^sup>\<omega> * ?y) = n (?x\<^sup>\<omega>)
| ?x > ?y = n (?x * ?y * L)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. n y \<le> | x > n y \<squnion> n (z * L) \<Longrightarrow> n y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > z
[PROOF STEP]
by force


[STATEMENT]
lemma an_diamond_omega_induct:
  "an(y) \<le> |x>an(y) \<squnion> n(z * L) \<Longrightarrow> an(y) \<le> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an y \<le> | x > an y \<squnion> n (z * L) \<Longrightarrow> an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > z
[PROOF STEP]
by (metis n_diamond_omega_induct an_n_def)


[STATEMENT]
lemma n_diamond_omega_induct_n:
  "n(y) \<le> |x>n(y) \<squnion> n(z) \<Longrightarrow> n(y) \<le> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>n(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y \<le> | x > n y \<squnion> n z \<Longrightarrow> n y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > n z
[PROOF STEP]
using box_1_n box_1_y n_diamond_omega_induct
[PROOF STATE]
proof (prove)
using this:
| (1::'a) ] n ?y = n ?y
| (1::'a) ] ?y = n (?y * L)
n ?y \<le> | ?x > n ?y \<squnion> n (?z * L) \<Longrightarrow> n ?y \<le> | ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> > ?z

goal (1 subgoal):
 1. n y \<le> | x > n y \<squnion> n z \<Longrightarrow> n y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > n z
[PROOF STEP]
by auto


[STATEMENT]
lemma an_diamond_omega_induct_an:
  "an(y) \<le> |x>an(y) \<squnion> an(z) \<Longrightarrow> an(y) \<le> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>an(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an y \<le> | x > an y \<squnion> an z \<Longrightarrow> an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > an z
[PROOF STEP]
using an_diamond_omega_induct an_n_def
[PROOF STATE]
proof (prove)
using this:
an ?y \<le> | ?x > an ?y \<squnion> n (?z * L) \<Longrightarrow> an ?y \<le> | ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> > ?z
an ?x = n (an ?x * L)

goal (1 subgoal):
 1. an y \<le> | x > an y \<squnion> an z \<Longrightarrow> an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > an z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_segerberg_an:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y) = an(y) * |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>](n(y) \<squnion> |x]an(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y = an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
 2. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
have "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y) \<le> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]|x]an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] | x ] an y
[PROOF STEP]
by (smt box_left_dist_sup box_left_mult box_omega sup_right_isotone box_left_antitone mult_right_dist_sup star.right_plus_below_circ)
[PROOF STATE]
proof (state)
this:
| x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] | x ] an y

goal (2 subgoals):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
 2. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
hence "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y) \<le> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>](n(y) \<squnion> |x]an(y))"
[PROOF STATE]
proof (prove)
using this:
| x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] | x ] an y

goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
[PROOF STEP]
using box_right_isotone order_lesseq_imp sup.cobounded2
[PROOF STATE]
proof (prove)
using this:
| x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] | x ] an y
?y \<le> ?z \<Longrightarrow> | ?x ] ?y \<le> | ?x ] ?z
(\<forall>z\<ge>?x. ?y \<le> z) = (?y \<le> ?x)
?b \<le> ?a \<squnion> ?b

goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
| x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)

goal (2 subgoals):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
 2. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
thus"|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y) \<le> an(y) * |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>](n(y) \<squnion> |x]an(y))"
[PROOF STATE]
proof (prove)
using this:
| x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)

goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
[PROOF STEP]
by (metis le_sup_iff box_1_an box_left_antitone order_refl star_left_unfold_equal an_mult_least_upper_bound nbox_def)
[PROOF STATE]
proof (state)
this:
| x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y)

goal (1 subgoal):
 1. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
have "an(y) * |x](n(y) \<squnion> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y)) * (n(y) \<squnion> |x]an(y)) = |x]( |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y) * an(y)) * an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) = | x ] (| x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y * an y) * an y
[PROOF STEP]
by (smt sup_bot_left an_export an_mult_commutative box_right_mult_an_an mult_assoc mult_right_dist_sup n_complement_bot nbox_def)
[PROOF STATE]
proof (state)
this:
an y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) = | x ] (| x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y * an y) * an y

goal (1 subgoal):
 1. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
hence 1: "an(y) * |x](n(y) \<squnion> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y)) * (n(y) \<squnion> |x]an(y)) \<le> n(y) \<squnion> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
using this:
an y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) = | x ] (| x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y * an y) * an y

goal (1 subgoal):
 1. an y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) \<le> n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
by (smt sup_assoc sup_commute sup_ge2 box_1_an box_left_dist_sup box_left_mult mult_left_dist_sup omega_unfold star_left_unfold_equal star.circ_plus_one)
[PROOF STATE]
proof (state)
this:
an y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) \<le> n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y

goal (1 subgoal):
 1. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
have "n(y) * |x](n(y) \<squnion> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y)) * (n(y) \<squnion> |x]an(y)) \<le> n(y) \<squnion> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) \<le> n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
by (smt sup_ge1 an_n_def mult_left_isotone n_an_mult_left_lower_bound n_mult_left_absorb_sup nbox_def order_trans)
[PROOF STATE]
proof (state)
this:
n y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) \<le> n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y

goal (1 subgoal):
 1. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
thus "an(y) * |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>](n(y) \<squnion> |x]an(y)) \<le> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
using this:
n y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) \<le> n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y

goal (1 subgoal):
 1. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
n y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) \<le> n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
an y * | x ] (n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y) * (n y \<squnion> | x ] an y) \<le> n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y

goal (1 subgoal):
 1. an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
by (smt an_case_split_left an_shunting_an mult_assoc n_box_omega_induct_n n_dist_sup nbox_def nbox_from_L)
[PROOF STATE]
proof (state)
this:
an y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma box_segerberg_n:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]n(y) = n(y) * |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>](an(y) \<squnion> |x]n(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n y = n y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (an y \<squnion> | x ] n y)
[PROOF STEP]
using box_segerberg_an an_n_def n_an_def
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> ] an ?y = an ?y * | ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> ] (n ?y \<squnion> | ?x ] an ?y)
an ?x = n (an ?x * L)
n ?x = an (an ?x * L)

goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n y = n y * | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] (an y \<squnion> | x ] n y)
[PROOF STEP]
by force


[STATEMENT]
lemma diamond_segerberg_an:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>an(y) = an(y) \<squnion> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>(n(y) * |x>an(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > an y = an y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > (n y * | x > an y)
[PROOF STEP]
by (smt an_export an_n_L box_diamond box_segerberg_an diamond_box mult_assoc n_an_def)


[STATEMENT]
lemma diamond_segerberg_n:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>n(y) = n(y) \<squnion> |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>(an(y) * |x>n(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > n y = n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > (an y * | x > n y)
[PROOF STEP]
using diamond_segerberg_an an_n_L n_an_def
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> > an ?y = an ?y \<squnion> | ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> > (n ?y * | ?x > an ?y)
an (n ?x * L) = an ?x
n ?x = an (an ?x * L)

goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > n y = n y \<squnion> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > (an y * | x > n y)
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_star_unfold_n:
  "|x\<^sup>\<star>>n(y) = n(y) \<squnion> |an(y) * x>|x\<^sup>\<star>>n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> > n y = n y \<squnion> | an y * x > | x\<^sup>\<star> > n y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. | x\<^sup>\<star> > n y = n y \<squnion> | an y * x > | x\<^sup>\<star> > n y
[PROOF STEP]
have "|x\<^sup>\<star>>n(y) = n(y) \<squnion> n(y) * |x * x\<^sup>\<star>>n(y) \<squnion> |an(y) * x * x\<^sup>\<star>>n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> > n y = n y \<squnion> n y * | x\<^sup>+ > n y \<squnion> | an y * x * x\<^sup>\<star> > n y
[PROOF STEP]
by (smt sup_assoc sup_commute sup_bot_right an_complement an_complement_bot diamond_an_n diamond_left_dist_sup diamond_n_export diamond_n_n_same mult_assoc mult_left_one mult_right_dist_sup star_left_unfold_equal)
[PROOF STATE]
proof (state)
this:
| x\<^sup>\<star> > n y = n y \<squnion> n y * | x\<^sup>+ > n y \<squnion> | an y * x * x\<^sup>\<star> > n y

goal (1 subgoal):
 1. | x\<^sup>\<star> > n y = n y \<squnion> | an y * x > | x\<^sup>\<star> > n y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
| x\<^sup>\<star> > n y = n y \<squnion> n y * | x\<^sup>+ > n y \<squnion> | an y * x * x\<^sup>\<star> > n y

goal (1 subgoal):
 1. | x\<^sup>\<star> > n y = n y \<squnion> | an y * x > | x\<^sup>\<star> > n y
[PROOF STEP]
by (metis diamond_left_mult diamond_x_n n_sup_left_absorb_mult)
[PROOF STATE]
proof (state)
this:
| x\<^sup>\<star> > n y = n y \<squnion> | an y * x > | x\<^sup>\<star> > n y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diamond_star_unfold_an:
  "|x\<^sup>\<star>>an(y) = an(y) \<squnion> |n(y) * x>|x\<^sup>\<star>>an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> > an y = an y \<squnion> | n y * x > | x\<^sup>\<star> > an y
[PROOF STEP]
by (metis an_n_def diamond_star_unfold_n n_an_def)


[STATEMENT]
lemma box_star_unfold_n:
  "|x\<^sup>\<star>]n(y) = n(y) * |n(y) * x]|x\<^sup>\<star>]n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> ] n y = n y * | n y * x ] | x\<^sup>\<star> ] n y
[PROOF STEP]
by (smt an_export an_n_L box_diamond diamond_box diamond_star_unfold_an n_an_def n_export)


[STATEMENT]
lemma box_star_unfold_an:
  "|x\<^sup>\<star>]an(y) = an(y) * |an(y) * x]|x\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> ] an y = an y * | an y * x ] | x\<^sup>\<star> ] an y
[PROOF STEP]
by (metis an_n_def box_star_unfold_n)


[STATEMENT]
lemma diamond_omega_unfold_n:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>n(y) = n(y) \<squnion> |an(y) * x>|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > n y = n y \<squnion> | an y * x > | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > n y
[PROOF STEP]
by (smt sup_assoc sup_commute diamond_an_export diamond_left_dist_sup diamond_right_dist_sup diamond_star_unfold_n diamond_x_n n_omega_mult n_plus_complement_intro_n omega_unfold)


[STATEMENT]
lemma diamond_omega_unfold_an:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>an(y) = an(y) \<squnion> |n(y) * x>|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > an y = an y \<squnion> | n y * x > | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > an y
[PROOF STEP]
by (metis an_n_def diamond_omega_unfold_n n_an_def)


[STATEMENT]
lemma box_omega_unfold_an:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y) = an(y) * |an(y) * x]|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y = an y * | an y * x ] | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
by (metis an_n_def box_omega_unfold_n)


[STATEMENT]
lemma box_cut_iteration_an:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]an(y) = |(an(y) * x)\<^sup>\<omega> \<squnion> (an(y) * x)\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y = | (an y * x)\<^sup>\<omega> \<squnion> (an y * x)\<^sup>\<star> ] an y
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y \<le> | (an y * x)\<^sup>\<omega> \<squnion> (an y * x)\<^sup>\<star> ] an y
 2. | (an y * x)\<^sup>\<omega> \<squnion> (an y * x)\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
apply (meson semiring.add_mono an_case_split_left box_left_antitone omega_isotone order_refl star.circ_isotone)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (an y * x)\<^sup>\<omega> \<squnion> (an y * x)\<^sup>\<star> ] an y \<le> | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] an y
[PROOF STEP]
by (smt (z3) an_box_omega_induct_an an_mult_commutative box_omega_unfold_an nbox_def order_refl)


[STATEMENT]
lemma box_cut_iteration_n:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]n(y) = |(n(y) * x)\<^sup>\<omega> \<squnion> (n(y) * x)\<^sup>\<star>]n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n y = | (n y * x)\<^sup>\<omega> \<squnion> (n y * x)\<^sup>\<star> ] n y
[PROOF STEP]
using box_cut_iteration_an n_an_def
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> ] an ?y = | (an ?y * ?x)\<^sup>\<omega> \<squnion> (an ?y * ?x)\<^sup>\<star> ] an ?y
n ?x = an (an ?x * L)

goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n y = | (n y * x)\<^sup>\<omega> \<squnion> (n y * x)\<^sup>\<star> ] n y
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_cut_iteration_an:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>an(y) = |(n(y) * x)\<^sup>\<omega> \<squnion> (n(y) * x)\<^sup>\<star>>an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > an y = | (n y * x)\<^sup>\<omega> \<squnion> (n y * x)\<^sup>\<star> > an y
[PROOF STEP]
using box_cut_iteration_n diamond_box n_an_def
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> ] n ?y = | (n ?y * ?x)\<^sup>\<omega> \<squnion> (n ?y * ?x)\<^sup>\<star> ] n ?y
| ?x > ?y = an (| ?x ] an (?y * L) * L)
n ?x = an (an ?x * L)

goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > an y = | (n y * x)\<^sup>\<omega> \<squnion> (n y * x)\<^sup>\<star> > an y
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_cut_iteration_n:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>n(y) = |(an(y) * x)\<^sup>\<omega> \<squnion> (an(y) * x)\<^sup>\<star>>n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > n y = | (an y * x)\<^sup>\<omega> \<squnion> (an y * x)\<^sup>\<star> > n y
[PROOF STEP]
using box_cut_iteration_an an_n_L diamond_box
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> ] an ?y = | (an ?y * ?x)\<^sup>\<omega> \<squnion> (an ?y * ?x)\<^sup>\<star> ] an ?y
an (n ?x * L) = an ?x
| ?x > ?y = an (| ?x ] an (?y * L) * L)

goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > n y = | (an y * x)\<^sup>\<omega> \<squnion> (an y * x)\<^sup>\<star> > n y
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_diamond_omega_induct:
  "ni(y) \<le> \<parallel>x\<guillemotright>ni(y) \<squnion> ni(z) \<Longrightarrow> ni(y) \<le> \<parallel>x\<^sup>\<omega> \<squnion> x\<^sup>\<star>\<guillemotright>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni y \<le> \<parallel> x \<guillemotright> ni y \<squnion> ni z \<Longrightarrow> ni y \<le> \<parallel> x\<^sup>\<omega> \<squnion> x\<^sup>\<star> \<guillemotright> z
[PROOF STEP]
by (metis diamond_L_left_dist_sup diamond_L_x_ni diamond_L_ni ni_dist_sup ni_omega_induct ni_omega_mult)


[STATEMENT]
lemma ani_diamond_omega_induct:
  "ani(y) \<le> \<parallel>x\<guillemotright>ani(y) \<squnion> ni(z) \<Longrightarrow> ani(y) \<le> \<parallel>x\<^sup>\<omega> \<squnion> x\<^sup>\<star>\<guillemotright>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani y \<le> \<parallel> x \<guillemotright> ani y \<squnion> ni z \<Longrightarrow> ani y \<le> \<parallel> x\<^sup>\<omega> \<squnion> x\<^sup>\<star> \<guillemotright> z
[PROOF STEP]
by (metis ni_ani ni_diamond_omega_induct)


[STATEMENT]
lemma n_diamond_omega_L:
  "|n(x\<^sup>\<omega>) * L>y = |x\<^sup>\<omega>>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n (x\<^sup>\<omega>) * L > y = | x\<^sup>\<omega> > y
[PROOF STEP]
using L_left_zero mult_1_right n_L n_export n_omega_mult ndiamond_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
L * ?x = L
?a * (1::'a) = ?a
n L = (1::'a)
n (n ?x * ?y) = n ?x * n ?y
n (?x\<^sup>\<omega> * ?y) = n (?x\<^sup>\<omega>)
| ?x > ?y = n (?x * ?y * L)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | n (x\<^sup>\<omega>) * L > y = | x\<^sup>\<omega> > y
[PROOF STEP]
by auto


[STATEMENT]
lemma n_diamond_loop:
  "|x\<^sup>\<Omega>>y = |x\<^sup>\<omega> \<squnion> x\<^sup>\<star>>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<Omega> > y = | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> > y
[PROOF STEP]
by (metis Omega_def diamond_left_dist_sup n_diamond_omega_L)


[STATEMENT]
lemma cut_iteration_loop:
  "|x\<^sup>\<Omega>>n(y) = |(an(y) * x)\<^sup>\<Omega>>n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<Omega> > n y = | (an y * x)\<^sup>\<Omega> > n y
[PROOF STEP]
using diamond_cut_iteration_n n_diamond_loop
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> > n ?y = | (an ?y * ?x)\<^sup>\<omega> \<squnion> (an ?y * ?x)\<^sup>\<star> > n ?y
| ?x\<^sup>\<Omega> > ?y = | ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> > ?y

goal (1 subgoal):
 1. | x\<^sup>\<Omega> > n y = | (an y * x)\<^sup>\<Omega> > n y
[PROOF STEP]
by auto


[STATEMENT]
lemma cut_iteration_while_loop:
  "|x\<^sup>\<Omega>>n(y) = |(an(y) * x)\<^sup>\<Omega> * n(y)>n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<Omega> > n y = | (an y * x)\<^sup>\<Omega> * n y > n y
[PROOF STEP]
using cut_iteration_loop diamond_left_mult diamond_n_n_same
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<Omega> > n ?y = | (an ?y * ?x)\<^sup>\<Omega> > n ?y
| ?x * ?y > ?z = | ?x > | ?y > ?z
| n ?x > n ?x = n ?x

goal (1 subgoal):
 1. | x\<^sup>\<Omega> > n y = | (an y * x)\<^sup>\<Omega> * n y > n y
[PROOF STEP]
by auto


[STATEMENT]
lemma cut_iteration_while_loop_2:
  "|x\<^sup>\<Omega>>n(y) = |an(y) \<star> x>n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<Omega> > n y = | an y \<star> x > n y
[PROOF STEP]
by (metis cut_iteration_while_loop an_uminus n_an_def while_Omega_def)


[STATEMENT]
lemma modal_while:
  assumes "-q * -p * L \<le> x * -p * L \<and> -p \<le> -q \<squnion> -r"
    shows "-p \<le> |n((-q * x)\<^sup>\<omega>) * L \<squnion> (-q * x)\<^sup>\<star> * --q>(-r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
have 1: "--q * -p \<le> |-q * x>(-p) \<squnion> --q * -r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - q * - p \<le> | - q * x > (- p) \<squnion> - - q * - r
[PROOF STEP]
using assms mult_right_isotone sup.coboundedI2 tests_dual.sup_complement_intro
[PROOF STATE]
proof (prove)
using this:
- q * - p * L \<le> x * - p * L \<and> - p \<le> - q \<squnion> - r
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
?c \<le> ?b \<Longrightarrow> ?c \<le> ?a \<squnion> ?b
- ?x * - ?y = - ?x * (- - ?x \<squnion> - ?y)

goal (1 subgoal):
 1. - - q * - p \<le> | - q * x > (- p) \<squnion> - - q * - r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- - q * - p \<le> | - q * x > (- p) \<squnion> - - q * - r

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
have "-q * -p = n(-q * -q * -p * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - q * - p = n (- q * - q * - p * L)
[PROOF STEP]
using an_uminus n_export_an mult_assoc mult_1_right n_L tests_dual.sup_idempotent
[PROOF STATE]
proof (prove)
using this:
- ?x = an (?x * L)
n (an ?x * ?y) = an ?x * n ?y
?a * ?b * ?c = ?a * (?b * ?c)
?a * (1::'a) = ?a
n L = (1::'a)
idempotent (- ?x)

goal (1 subgoal):
 1. - q * - p = n (- q * - q * - p * L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- q * - p = n (- q * - q * - p * L)

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- q * - p = n (- q * - q * - p * L)

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
have "... \<le> n(-q * x * -p * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (- q * - q * - p * L) \<le> n (- q * x * - p * L)
[PROOF STEP]
by (metis assms n_isotone mult_right_isotone mult_assoc)
[PROOF STATE]
proof (state)
this:
n (- q * - q * - p * L) \<le> n (- q * x * - p * L)

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n (- q * - q * - p * L) \<le> n (- q * x * - p * L)

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
have "... \<le> |-q * x>(-p) \<squnion> --q * -r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (- q * x * - p * L) \<le> | - q * x > (- p) \<squnion> - - q * - r
[PROOF STEP]
by (simp add: ndiamond_def)
[PROOF STATE]
proof (state)
this:
n (- q * x * - p * L) \<le> | - q * x > (- p) \<squnion> - - q * - r

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- q * - p \<le> | - q * x > (- p) \<squnion> - - q * - r
[PROOF STEP]
have "-p \<le> |-q * x>(-p) \<squnion> --q * -r"
[PROOF STATE]
proof (prove)
using this:
- q * - p \<le> | - q * x > (- p) \<squnion> - - q * - r

goal (1 subgoal):
 1. - p \<le> | - q * x > (- p) \<squnion> - - q * - r
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
- q * - p \<le> | - q * x > (- p) \<squnion> - - q * - r
- - q * - p \<le> | - q * x > (- p) \<squnion> - - q * - r

goal (1 subgoal):
 1. - p \<le> | - q * x > (- p) \<squnion> - - q * - r
[PROOF STEP]
by (smt sup_assoc le_iff_sup tests_dual.inf_cases sub_comm)
[PROOF STATE]
proof (state)
this:
- p \<le> | - q * x > (- p) \<squnion> - - q * - r

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
- p \<le> | - q * x > (- p) \<squnion> - - q * - r

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)
[PROOF STEP]
by (smt L_left_zero an_diamond_omega_induct_an an_uminus diamond_left_dist_sup mult_assoc n_n_L n_omega_mult ndiamond_def sub_mult_closed)
[PROOF STATE]
proof (state)
this:
- p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma modal_while_loop:
  "-q * -p * L \<le> x * -p * L \<and> -p \<le> -q \<squnion> -r \<Longrightarrow> -p \<le> |(-q * x)\<^sup>\<Omega> * --q>(-r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - q * - p * L \<le> x * - p * L \<and> - p \<le> - q \<squnion> - r \<Longrightarrow> - p \<le> | (- q * x)\<^sup>\<Omega> * - - q > (- r)
[PROOF STEP]
by (metis L_left_zero Omega_def modal_while mult_assoc mult_right_dist_sup)


[STATEMENT]
lemma modal_while_loop_2:
  "-q * -p * L \<le> x * -p * L \<and> -p \<le> -q \<squnion> -r \<Longrightarrow> -p \<le> |-q \<star> x>(-r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - q * - p * L \<le> x * - p * L \<and> - p \<le> - q \<squnion> - r \<Longrightarrow> - p \<le> | - q \<star> x > (- r)
[PROOF STEP]
by (simp add: while_Omega_def modal_while_loop)


[STATEMENT]
lemma modal_while_2:
  assumes "-p * L \<le> x * -p * L"
    shows "-p \<le> |n((-q * x)\<^sup>\<omega>) * L \<squnion> (-q * x)\<^sup>\<star> * --q>(--q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- - q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- - q)
[PROOF STEP]
have "-p \<le> |-q * x>(-p) \<squnion> --q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<le> | - q * x > (- p) \<squnion> - - q
[PROOF STEP]
by (smt (verit, del_insts) assms an_uminus tests_dual.double_negation n_an_def n_isotone ndiamond_def diamond_an_export sup_assoc sup_commute le_iff_sup tests_dual.inf_complement_intro)
[PROOF STATE]
proof (state)
this:
- p \<le> | - q * x > (- p) \<squnion> - - q

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- - q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
- p \<le> | - q * x > (- p) \<squnion> - - q

goal (1 subgoal):
 1. - p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- - q)
[PROOF STEP]
by (smt L_left_zero an_diamond_omega_induct_an an_uminus diamond_left_dist_sup mult_assoc tests_dual.sup_idempotent n_n_L n_omega_mult ndiamond_def)
[PROOF STATE]
proof (state)
this:
- p \<le> | n ((- q * x)\<^sup>\<omega>) * L \<squnion> (- q * x)\<^sup>\<star> * - - q > (- - q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma n_star_induct_sup:
  "n(z \<squnion> x * y) \<le> n(y) \<Longrightarrow> n(x\<^sup>\<star> * z) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (z \<squnion> x * y) \<le> n y \<Longrightarrow> n (x\<^sup>\<star> * z) \<le> n y
[PROOF STEP]
by (metis an_dist_sup an_mult_least_upper_bound an_n_order n_mult_right_upper_bound n_star_induct star_L_split)


[STATEMENT]
lemma n_star_induct_star:
  "n(x * y) \<le> n(y) \<Longrightarrow> n(x\<^sup>\<star>) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x * y) \<le> n y \<Longrightarrow> n (x\<^sup>\<star>) \<le> n y
[PROOF STEP]
using n_star_induct n_star_mult
[PROOF STATE]
proof (prove)
using this:
n (?x * ?y) \<le> n ?y \<longrightarrow> n (?x\<^sup>\<star> * ?y) \<le> n ?y
n (?x * ?y) \<le> n ?y \<Longrightarrow> n (?x\<^sup>\<star> * ?y) = n (?x\<^sup>\<star>) \<squnion> n ?y

goal (1 subgoal):
 1. n (x * y) \<le> n y \<Longrightarrow> n (x\<^sup>\<star>) \<le> n y
[PROOF STEP]
by auto


[STATEMENT]
lemma n_star_induct_iff:
  "n(x * y) \<le> n(y) \<longleftrightarrow> n(x\<^sup>\<star> * y) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n (x * y) \<le> n y) = (n (x\<^sup>\<star> * y) \<le> n y)
[PROOF STEP]
by (metis mult_left_isotone n_isotone n_star_induct order_trans star.circ_increasing)


[STATEMENT]
lemma n_star_bot:
  "n(x) = bot \<longleftrightarrow> n(x\<^sup>\<star>) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n x = bot) = (n (x\<^sup>\<star>) = bot)
[PROOF STEP]
by (metis sup_bot_right le_iff_sup mult_1_right n_one n_star_induct_iff)


[STATEMENT]
lemma n_diamond_star_induct:
  "|x>n(y) \<le> n(y) \<Longrightarrow> |x\<^sup>\<star>>n(y) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > n y \<le> n y \<Longrightarrow> | x\<^sup>\<star> > n y \<le> n y
[PROOF STEP]
by (simp add: diamond_x_n n_star_induct)


[STATEMENT]
lemma n_diamond_star_induct_sup:
  "|x>n(y) \<squnion> n(z) \<le> n(y) \<Longrightarrow> |x\<^sup>\<star>>n(z) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > n y \<squnion> n z \<le> n y \<Longrightarrow> | x\<^sup>\<star> > n z \<le> n y
[PROOF STEP]
by (simp add: diamond_x_n n_dist_sup n_star_induct_sup)


[STATEMENT]
lemma n_diamond_star_induct_iff:
  "|x>n(y) \<le> n(y) \<longleftrightarrow> |x\<^sup>\<star>>n(y) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (| x > n y \<le> n y) = (| x\<^sup>\<star> > n y \<le> n y)
[PROOF STEP]
using diamond_x_n n_star_induct_iff
[PROOF STATE]
proof (prove)
using this:
| ?x > n ?y = n (?x * ?y)
(n (?x * ?y) \<le> n ?y) = (n (?x\<^sup>\<star> * ?y) \<le> n ?y)

goal (1 subgoal):
 1. (| x > n y \<le> n y) = (| x\<^sup>\<star> > n y \<le> n y)
[PROOF STEP]
by auto


[STATEMENT]
lemma an_star_induct:
  "an(y) \<le> an(x * y) \<Longrightarrow> an(y) \<le> an(x\<^sup>\<star> * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an y \<le> an (x * y) \<Longrightarrow> an y \<le> an (x\<^sup>\<star> * y)
[PROOF STEP]
using an_n_order n_star_induct
[PROOF STATE]
proof (prove)
using this:
(an ?x \<le> an ?y) = (n ?y \<le> n ?x)
n (?x * ?y) \<le> n ?y \<longrightarrow> n (?x\<^sup>\<star> * ?y) \<le> n ?y

goal (1 subgoal):
 1. an y \<le> an (x * y) \<Longrightarrow> an y \<le> an (x\<^sup>\<star> * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma an_star_induct_sup:
  "an(y) \<le> an(z \<squnion> x * y) \<Longrightarrow> an(y) \<le> an(x\<^sup>\<star> * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an y \<le> an (z \<squnion> x * y) \<Longrightarrow> an y \<le> an (x\<^sup>\<star> * z)
[PROOF STEP]
using an_n_order n_star_induct_sup
[PROOF STATE]
proof (prove)
using this:
(an ?x \<le> an ?y) = (n ?y \<le> n ?x)
n (?z \<squnion> ?x * ?y) \<le> n ?y \<Longrightarrow> n (?x\<^sup>\<star> * ?z) \<le> n ?y

goal (1 subgoal):
 1. an y \<le> an (z \<squnion> x * y) \<Longrightarrow> an y \<le> an (x\<^sup>\<star> * z)
[PROOF STEP]
by auto


[STATEMENT]
lemma an_star_induct_star:
  "an(y) \<le> an(x * y) \<Longrightarrow> an(y) \<le> an(x\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an y \<le> an (x * y) \<Longrightarrow> an y \<le> an (x\<^sup>\<star>)
[PROOF STEP]
by (simp add: an_n_order n_star_induct_star)


[STATEMENT]
lemma an_star_induct_iff:
  "an(y) \<le> an(x * y) \<longleftrightarrow> an(y) \<le> an(x\<^sup>\<star> * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (an y \<le> an (x * y)) = (an y \<le> an (x\<^sup>\<star> * y))
[PROOF STEP]
using an_n_order n_star_induct_iff
[PROOF STATE]
proof (prove)
using this:
(an ?x \<le> an ?y) = (n ?y \<le> n ?x)
(n (?x * ?y) \<le> n ?y) = (n (?x\<^sup>\<star> * ?y) \<le> n ?y)

goal (1 subgoal):
 1. (an y \<le> an (x * y)) = (an y \<le> an (x\<^sup>\<star> * y))
[PROOF STEP]
by auto


[STATEMENT]
lemma an_star_one:
  "an(x) = 1 \<longleftrightarrow> an(x\<^sup>\<star>) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (an x = (1::'a)) = (an (x\<^sup>\<star>) = (1::'a))
[PROOF STEP]
by (metis an_n_equal an_bot n_star_bot n_bot)


[STATEMENT]
lemma an_box_star_induct:
  "an(y) \<le> |x]an(y) \<Longrightarrow> an(y) \<le> |x\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an y \<le> | x ] an y \<Longrightarrow> an y \<le> | x\<^sup>\<star> ] an y
[PROOF STEP]
by (simp add: an_star_induct box_x_an)


[STATEMENT]
lemma an_box_star_induct_sup:
  "an(y) \<le> |x]an(y) * an(z) \<Longrightarrow> an(y) \<le> |x\<^sup>\<star>]an(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an y \<le> | x ] an y * an z \<Longrightarrow> an y \<le> | x\<^sup>\<star> ] an z
[PROOF STEP]
by (simp add: an_star_induct_sup an_dist_sup an_mult_commutative box_x_an)


[STATEMENT]
lemma an_box_star_induct_iff:
  "an(y) \<le> |x]an(y) \<longleftrightarrow> an(y) \<le> |x\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (an y \<le> | x ] an y) = (an y \<le> | x\<^sup>\<star> ] an y)
[PROOF STEP]
using an_star_induct_iff box_x_an
[PROOF STATE]
proof (prove)
using this:
(an ?y \<le> an (?x * ?y)) = (an ?y \<le> an (?x\<^sup>\<star> * ?y))
| ?x ] an ?y = an (?x * ?y)

goal (1 subgoal):
 1. (an y \<le> | x ] an y) = (an y \<le> | x\<^sup>\<star> ] an y)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_star_segerberg_an:
  "|x\<^sup>\<star>]an(y) = an(y) * |x\<^sup>\<star>](n(y) \<squnion> |x]an(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> ] an y = an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. | x\<^sup>\<star> ] an y \<le> an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
 2. an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<star> ] an y
[PROOF STEP]
show "|x\<^sup>\<star>]an(y) \<le> an(y) * |x\<^sup>\<star>](n(y) \<squnion> |x]an(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> ] an y \<le> an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y)
[PROOF STEP]
by (smt (verit) sup_ge2 box_1_an box_left_dist_sup box_left_mult box_right_isotone mult_right_isotone star.circ_right_unfold)
[PROOF STATE]
proof (state)
this:
| x\<^sup>\<star> ] an y \<le> an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y)

goal (1 subgoal):
 1. an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<star> ] an y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<star> ] an y
[PROOF STEP]
have "an(y) * |x\<^sup>\<star>](n(y) \<squnion> |x]an(y)) \<le> an(y) * |x]an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> an y * | x ] an y
[PROOF STEP]
by (metis sup_bot_left an_complement_bot box_an_an box_left_antitone box_x_an mult_left_dist_sup mult_left_one mult_right_isotone star.circ_reflexive)
[PROOF STATE]
proof (state)
this:
an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> an y * | x ] an y

goal (1 subgoal):
 1. an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<star> ] an y
[PROOF STEP]
thus "an(y) * |x\<^sup>\<star>](n(y) \<squnion> |x]an(y)) \<le> |x\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
using this:
an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> an y * | x ] an y

goal (1 subgoal):
 1. an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<star> ] an y
[PROOF STEP]
by (smt an_box_star_induct_sup an_case_split_left an_dist_sup an_mult_least_upper_bound box_left_antitone box_left_mult box_right_mult_an_an star.left_plus_below_circ nbox_def)
[PROOF STATE]
proof (state)
this:
an y * | x\<^sup>\<star> ] (n y \<squnion> | x ] an y) \<le> | x\<^sup>\<star> ] an y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma box_star_segerberg_n:
  "|x\<^sup>\<star>]n(y) = n(y) * |x\<^sup>\<star>](an(y) \<squnion> |x]n(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> ] n y = n y * | x\<^sup>\<star> ] (an y \<squnion> | x ] n y)
[PROOF STEP]
using box_star_segerberg_an an_n_def n_an_def
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<star> ] an ?y = an ?y * | ?x\<^sup>\<star> ] (n ?y \<squnion> | ?x ] an ?y)
an ?x = n (an ?x * L)
n ?x = an (an ?x * L)

goal (1 subgoal):
 1. | x\<^sup>\<star> ] n y = n y * | x\<^sup>\<star> ] (an y \<squnion> | x ] n y)
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_segerberg_an:
  "|x\<^sup>\<star>>an(y) = an(y) \<squnion> |x\<^sup>\<star>>(n(y) * |x>an(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> > an y = an y \<squnion> | x\<^sup>\<star> > (n y * | x > an y)
[PROOF STEP]
by (smt an_export an_n_L box_diamond box_star_segerberg_an diamond_box mult_assoc n_an_def)


[STATEMENT]
lemma diamond_star_segerberg_n:
  "|x\<^sup>\<star>>n(y) = n(y) \<squnion> |x\<^sup>\<star>>(an(y) * |x>n(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> > n y = n y \<squnion> | x\<^sup>\<star> > (an y * | x > n y)
[PROOF STEP]
using an_n_def diamond_segerberg_an n_an_def
[PROOF STATE]
proof (prove)
using this:
an ?x = n (an ?x * L)
| ?x\<^sup>\<star> > an ?y = an ?y \<squnion> | ?x\<^sup>\<star> > (n ?y * | ?x > an ?y)
n ?x = an (an ?x * L)

goal (1 subgoal):
 1. | x\<^sup>\<star> > n y = n y \<squnion> | x\<^sup>\<star> > (an y * | x > n y)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_cut_star_iteration_an:
  "|x\<^sup>\<star>]an(y) = |(an(y) * x)\<^sup>\<star>]an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> ] an y = | (an y * x)\<^sup>\<star> ] an y
[PROOF STEP]
by (smt an_box_star_induct_sup an_mult_commutative an_mult_complement_intro_an order.antisym box_an_export box_star_unfold_an nbox_def order_refl)


[STATEMENT]
lemma box_cut_star_iteration_n:
  "|x\<^sup>\<star>]n(y) = |(n(y) * x)\<^sup>\<star>]n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> ] n y = | (n y * x)\<^sup>\<star> ] n y
[PROOF STEP]
using box_cut_star_iteration_an n_an_def
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<star> ] an ?y = | (an ?y * ?x)\<^sup>\<star> ] an ?y
n ?x = an (an ?x * L)

goal (1 subgoal):
 1. | x\<^sup>\<star> ] n y = | (n y * x)\<^sup>\<star> ] n y
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_cut_star_iteration_an:
  "|x\<^sup>\<star>>an(y) = |(n(y) * x)\<^sup>\<star>>an(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> > an y = | (n y * x)\<^sup>\<star> > an y
[PROOF STEP]
using box_cut_star_iteration_an diamond_box n_an_def
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<star> ] an ?y = | (an ?y * ?x)\<^sup>\<star> ] an ?y
| ?x > ?y = an (| ?x ] an (?y * L) * L)
n ?x = an (an ?x * L)

goal (1 subgoal):
 1. | x\<^sup>\<star> > an y = | (n y * x)\<^sup>\<star> > an y
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_cut_star_iteration_n:
  "|x\<^sup>\<star>>n(y) = |(an(y) * x)\<^sup>\<star>>n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<star> > n y = | (an y * x)\<^sup>\<star> > n y
[PROOF STEP]
using box_cut_star_iteration_an an_n_L diamond_box
[PROOF STATE]
proof (prove)
using this:
| ?x\<^sup>\<star> ] an ?y = | (an ?y * ?x)\<^sup>\<star> ] an ?y
an (n ?x * L) = an ?x
| ?x > ?y = an (| ?x ] an (?y * L) * L)

goal (1 subgoal):
 1. | x\<^sup>\<star> > n y = | (an y * x)\<^sup>\<star> > n y
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_star_induct:
  "ni(x * y) \<le> ni(y) \<Longrightarrow> ni(x\<^sup>\<star> * y) \<le> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x * y) \<le> ni y \<Longrightarrow> ni (x\<^sup>\<star> * y) \<le> ni y
[PROOF STEP]
using n_star_induct ni_n_order
[PROOF STATE]
proof (prove)
using this:
n (?x * ?y) \<le> n ?y \<longrightarrow> n (?x\<^sup>\<star> * ?y) \<le> n ?y
(ni ?x \<le> ni ?y) = (n ?x \<le> n ?y)

goal (1 subgoal):
 1. ni (x * y) \<le> ni y \<Longrightarrow> ni (x\<^sup>\<star> * y) \<le> ni y
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_star_induct_sup:
  "ni(z \<squnion> x * y) \<le> ni(y) \<Longrightarrow> ni(x\<^sup>\<star> * z) \<le> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (z \<squnion> x * y) \<le> ni y \<Longrightarrow> ni (x\<^sup>\<star> * z) \<le> ni y
[PROOF STEP]
by (simp add: ni_n_order n_star_induct_sup)


[STATEMENT]
lemma ni_star_induct_star:
  "ni(x * y) \<le> ni(y) \<Longrightarrow> ni(x\<^sup>\<star>) \<le> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x * y) \<le> ni y \<Longrightarrow> ni (x\<^sup>\<star>) \<le> ni y
[PROOF STEP]
using ni_n_order n_star_induct_star
[PROOF STATE]
proof (prove)
using this:
(ni ?x \<le> ni ?y) = (n ?x \<le> n ?y)
n (?x * ?y) \<le> n ?y \<Longrightarrow> n (?x\<^sup>\<star>) \<le> n ?y

goal (1 subgoal):
 1. ni (x * y) \<le> ni y \<Longrightarrow> ni (x\<^sup>\<star>) \<le> ni y
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_star_induct_iff:
  "ni(x * y) \<le> ni(y) \<longleftrightarrow> ni(x\<^sup>\<star> * y) \<le> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ni (x * y) \<le> ni y) = (ni (x\<^sup>\<star> * y) \<le> ni y)
[PROOF STEP]
using ni_n_order n_star_induct_iff
[PROOF STATE]
proof (prove)
using this:
(ni ?x \<le> ni ?y) = (n ?x \<le> n ?y)
(n (?x * ?y) \<le> n ?y) = (n (?x\<^sup>\<star> * ?y) \<le> n ?y)

goal (1 subgoal):
 1. (ni (x * y) \<le> ni y) = (ni (x\<^sup>\<star> * y) \<le> ni y)
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_star_bot:
  "ni(x) = bot \<longleftrightarrow> ni(x\<^sup>\<star>) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ni x = bot) = (ni (x\<^sup>\<star>) = bot)
[PROOF STEP]
using ni_n_bot n_star_bot
[PROOF STATE]
proof (prove)
using this:
(ni ?x = bot) = (n ?x = bot)
(n ?x = bot) = (n (?x\<^sup>\<star>) = bot)

goal (1 subgoal):
 1. (ni x = bot) = (ni (x\<^sup>\<star>) = bot)
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_diamond_star_induct:
  "\<parallel>x\<guillemotright>ni(y) \<le> ni(y) \<Longrightarrow> \<parallel>x\<^sup>\<star>\<guillemotright>ni(y) \<le> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x \<guillemotright> ni y \<le> ni y \<Longrightarrow> \<parallel> x\<^sup>\<star> \<guillemotright> ni y \<le> ni y
[PROOF STEP]
by (simp add: diamond_L_x_ni ni_star_induct)


[STATEMENT]
lemma ni_diamond_star_induct_sup:
  "\<parallel>x\<guillemotright>ni(y) \<squnion> ni(z) \<le> ni(y) \<Longrightarrow> \<parallel>x\<^sup>\<star>\<guillemotright>ni(z) \<le> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x \<guillemotright> ni y \<squnion> ni z \<le> ni y \<Longrightarrow> \<parallel> x\<^sup>\<star> \<guillemotright> ni z \<le> ni y
[PROOF STEP]
by (simp add: diamond_L_x_ni ni_dist_sup ni_star_induct_sup)


[STATEMENT]
lemma ni_diamond_star_induct_iff:
  "\<parallel>x\<guillemotright>ni(y) \<le> ni(y) \<longleftrightarrow> \<parallel>x\<^sup>\<star>\<guillemotright>ni(y) \<le> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<parallel> x \<guillemotright> ni y \<le> ni y) = (\<parallel> x\<^sup>\<star> \<guillemotright> ni y \<le> ni y)
[PROOF STEP]
using diamond_L_x_ni ni_star_induct_iff
[PROOF STATE]
proof (prove)
using this:
\<parallel> ?x \<guillemotright> ni ?y = ni (?x * ?y)
(ni (?x * ?y) \<le> ni ?y) = (ni (?x\<^sup>\<star> * ?y) \<le> ni ?y)

goal (1 subgoal):
 1. (\<parallel> x \<guillemotright> ni y \<le> ni y) = (\<parallel> x\<^sup>\<star> \<guillemotright> ni y \<le> ni y)
[PROOF STEP]
by auto


[STATEMENT]
lemma ani_star_induct:
  "ani(y) \<le> ani(x * y) \<Longrightarrow> ani(y) \<le> ani(x\<^sup>\<star> * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani y \<le> ani (x * y) \<Longrightarrow> ani y \<le> ani (x\<^sup>\<star> * y)
[PROOF STEP]
using an_star_induct ani_an_order
[PROOF STATE]
proof (prove)
using this:
an ?y \<le> an (?x * ?y) \<Longrightarrow> an ?y \<le> an (?x\<^sup>\<star> * ?y)
(ani ?x \<le> ani ?y) = (an ?x \<le> an ?y)

goal (1 subgoal):
 1. ani y \<le> ani (x * y) \<Longrightarrow> ani y \<le> ani (x\<^sup>\<star> * y)
[PROOF STEP]
by blast


[STATEMENT]
lemma ani_star_induct_sup:
  "ani(y) \<le> ani(z \<squnion> x * y) \<Longrightarrow> ani(y) \<le> ani(x\<^sup>\<star> * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani y \<le> ani (z \<squnion> x * y) \<Longrightarrow> ani y \<le> ani (x\<^sup>\<star> * z)
[PROOF STEP]
by (simp add: an_star_induct_sup ani_an_order)


[STATEMENT]
lemma ani_star_induct_star:
  "ani(y) \<le> ani(x * y) \<Longrightarrow> ani(y) \<le> ani(x\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani y \<le> ani (x * y) \<Longrightarrow> ani y \<le> ani (x\<^sup>\<star>)
[PROOF STEP]
using an_star_induct_star ani_an_order
[PROOF STATE]
proof (prove)
using this:
an ?y \<le> an (?x * ?y) \<Longrightarrow> an ?y \<le> an (?x\<^sup>\<star>)
(ani ?x \<le> ani ?y) = (an ?x \<le> an ?y)

goal (1 subgoal):
 1. ani y \<le> ani (x * y) \<Longrightarrow> ani y \<le> ani (x\<^sup>\<star>)
[PROOF STEP]
by auto


[STATEMENT]
lemma ani_star_induct_iff:
  "ani(y) \<le> ani(x * y) \<longleftrightarrow> ani(y) \<le> ani(x\<^sup>\<star> * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ani y \<le> ani (x * y)) = (ani y \<le> ani (x\<^sup>\<star> * y))
[PROOF STEP]
using an_star_induct_iff ani_an_order
[PROOF STATE]
proof (prove)
using this:
(an ?y \<le> an (?x * ?y)) = (an ?y \<le> an (?x\<^sup>\<star> * ?y))
(ani ?x \<le> ani ?y) = (an ?x \<le> an ?y)

goal (1 subgoal):
 1. (ani y \<le> ani (x * y)) = (ani y \<le> ani (x\<^sup>\<star> * y))
[PROOF STEP]
by auto


[STATEMENT]
lemma ani_star_L:
  "ani(x) = L \<longleftrightarrow> ani(x\<^sup>\<star>) = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ani x = L) = (ani (x\<^sup>\<star>) = L)
[PROOF STEP]
using an_star_one ani_an_L
[PROOF STATE]
proof (prove)
using this:
(an ?x = (1::'a)) = (an (?x\<^sup>\<star>) = (1::'a))
(ani ?x = L) = (an ?x = (1::'a))

goal (1 subgoal):
 1. (ani x = L) = (ani (x\<^sup>\<star>) = L)
[PROOF STEP]
by auto


[STATEMENT]
lemma ani_box_star_induct:
  "ani(y) \<le> \<parallel>x\<rbrakk>ani(y) \<Longrightarrow> ani(y) \<le> \<parallel>x\<^sup>\<star>\<rbrakk>ani(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani y \<le> \<parallel> x \<rbrakk> ani y \<Longrightarrow> ani y \<le> \<parallel> x\<^sup>\<star> \<rbrakk> ani y
[PROOF STEP]
by (metis an_ani ani_def ani_star_induct_iff n_ani box_L_ani)


[STATEMENT]
lemma ani_box_star_induct_iff:
  "ani(y) \<le> \<parallel>x\<rbrakk>ani(y) \<longleftrightarrow> ani(y) \<le> \<parallel>x\<^sup>\<star>\<rbrakk>ani(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ani y \<le> \<parallel> x \<rbrakk> ani y) = (ani y \<le> \<parallel> x\<^sup>\<star> \<rbrakk> ani y)
[PROOF STEP]
using ani_box_star_induct box_L_left_antitone order_lesseq_imp star.circ_increasing
[PROOF STATE]
proof (prove)
using this:
ani ?y \<le> \<parallel> ?x \<rbrakk> ani ?y \<Longrightarrow> ani ?y \<le> \<parallel> ?x\<^sup>\<star> \<rbrakk> ani ?y
?y \<le> ?x \<Longrightarrow> \<parallel> ?x \<rbrakk> ?z \<le> \<parallel> ?y \<rbrakk> ?z
(\<forall>z\<ge>?x. ?y \<le> z) = (?y \<le> ?x)
?x \<le> ?x\<^sup>\<star>

goal (1 subgoal):
 1. (ani y \<le> \<parallel> x \<rbrakk> ani y) = (ani y \<le> \<parallel> x\<^sup>\<star> \<rbrakk> ani y)
[PROOF STEP]
by blast


[STATEMENT]
lemma ani_box_star_induct_sup:
  "ani(y) \<le> \<parallel>x\<rbrakk>ani(y) \<Longrightarrow> ani(y) \<le> ani(z) \<Longrightarrow> ani(y) \<le> \<parallel>x\<^sup>\<star>\<rbrakk>ani(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ani y \<le> \<parallel> x \<rbrakk> ani y; ani y \<le> ani z\<rbrakk> \<Longrightarrow> ani y \<le> \<parallel> x\<^sup>\<star> \<rbrakk> ani z
[PROOF STEP]
by (meson ani_box_star_induct_iff box_L_right_isotone order_trans)


[STATEMENT]
lemma worker_wrapper_fusion_new:
  fixes wrap :: "'b::pcpo \<rightarrow> 'a::pcpo"
  fixes unwrap :: "'a \<rightarrow> 'b"
  fixes body' :: "'b \<rightarrow> 'b"
  assumes wrap_unwrap: "wrap oo unwrap = (ID :: 'a \<rightarrow> 'a)"
  assumes unwrap_strict: "unwrap\<cdot>\<bottom> = \<bottom>"
  assumes body_body': "unwrap oo body oo wrap = body' oo (unwrap oo wrap)"
  shows "fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
from body_body'
[PROOF STATE]
proof (chain)
picking this:
unwrap oo body oo wrap = body' oo unwrap oo wrap
[PROOF STEP]
have "unwrap oo body oo (wrap oo unwrap) = (body' oo unwrap oo (wrap oo unwrap))"
[PROOF STATE]
proof (prove)
using this:
unwrap oo body oo wrap = body' oo unwrap oo wrap

goal (1 subgoal):
 1. unwrap oo body oo wrap oo unwrap = body' oo unwrap oo wrap oo unwrap
[PROOF STEP]
by (simp add: assoc_oo)
[PROOF STATE]
proof (state)
this:
unwrap oo body oo wrap oo unwrap = body' oo unwrap oo wrap oo unwrap

goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
with wrap_unwrap
[PROOF STATE]
proof (chain)
picking this:
wrap oo unwrap = ID
unwrap oo body oo wrap oo unwrap = body' oo unwrap oo wrap oo unwrap
[PROOF STEP]
have "unwrap oo body = body' oo unwrap"
[PROOF STATE]
proof (prove)
using this:
wrap oo unwrap = ID
unwrap oo body oo wrap oo unwrap = body' oo unwrap oo wrap oo unwrap

goal (1 subgoal):
 1. unwrap oo body = body' oo unwrap
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
unwrap oo body = body' oo unwrap

goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
with unwrap_strict
[PROOF STATE]
proof (chain)
picking this:
unwrap\<cdot>\<bottom> = \<bottom>
unwrap oo body = body' oo unwrap
[PROOF STEP]
have "unwrap\<cdot>(fix\<cdot>body) = fix\<cdot>body'"
[PROOF STATE]
proof (prove)
using this:
unwrap\<cdot>\<bottom> = \<bottom>
unwrap oo body = body' oo unwrap

goal (1 subgoal):
 1. unwrap\<cdot>(fix\<cdot>body) = fix\<cdot>body'
[PROOF STEP]
by (rule lfp_fusion)
[PROOF STATE]
proof (state)
this:
unwrap\<cdot>(fix\<cdot>body) = fix\<cdot>body'

goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
hence "(wrap oo unwrap)\<cdot>(fix\<cdot>body) = wrap\<cdot>(fix\<cdot>body')"
[PROOF STATE]
proof (prove)
using this:
unwrap\<cdot>(fix\<cdot>body) = fix\<cdot>body'

goal (1 subgoal):
 1. (wrap oo unwrap)\<cdot>(fix\<cdot>body) = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(wrap oo unwrap)\<cdot>(fix\<cdot>body) = wrap\<cdot>(fix\<cdot>body')

goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
with wrap_unwrap
[PROOF STATE]
proof (chain)
picking this:
wrap oo unwrap = ID
(wrap oo unwrap)\<cdot>(fix\<cdot>body) = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wrap oo unwrap = ID
(wrap oo unwrap)\<cdot>(fix\<cdot>body) = wrap\<cdot>(fix\<cdot>body')

goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma worker_wrapper_fusion_new_general:
  fixes wrap :: "'b::pcpo \<rightarrow> 'a::pcpo"
  fixes unwrap :: "'a \<rightarrow> 'b"
  assumes wrap_unwrap: "wrap oo unwrap = (ID :: 'a \<rightarrow> 'a)"
  assumes unwrap_strict: "unwrap\<cdot>\<bottom> = \<bottom>"
  assumes body_body': "\<And>r. (unwrap oo wrap)\<cdot>r = r
                        \<Longrightarrow> (unwrap oo body oo wrap)\<cdot>r = body'\<cdot>r"
  shows "fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
let ?P = "\<lambda>(x, y). x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
have "?P (fix\<cdot>(unwrap oo body oo wrap), (fix\<cdot>body'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (fix\<cdot>(unwrap oo body oo wrap), fix\<cdot>body') of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
proof(induct rule: parallel_fix_ind)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. adm (\<lambda>x. case (fst x, snd x) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x)
 2. case (\<bottom>, \<bottom>) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
 3. \<And>x y. case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x \<Longrightarrow> case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. adm (\<lambda>x. case (fst x, snd x) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x)
 2. case (\<bottom>, \<bottom>) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
 3. \<And>x y. case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x \<Longrightarrow> case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
with retraction_strict unwrap_strict wrap_unwrap
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. ?f\<cdot>(?g\<cdot>x) = x \<Longrightarrow> ?f\<cdot>\<bottom> = \<bottom>
unwrap\<cdot>\<bottom> = \<bottom>
wrap oo unwrap = ID
[PROOF STEP]
show "?P (\<bottom>, \<bottom>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ?f\<cdot>(?g\<cdot>x) = x \<Longrightarrow> ?f\<cdot>\<bottom> = \<bottom>
unwrap\<cdot>\<bottom> = \<bottom>
wrap oo unwrap = ID

goal (1 subgoal):
 1. case (\<bottom>, \<bottom>) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
by (bestsimp simp add: cfun_eq_iff)
[PROOF STATE]
proof (state)
this:
case (\<bottom>, \<bottom>) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x

goal (2 subgoals):
 1. adm (\<lambda>x. case (fst x, snd x) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x)
 2. \<And>x y. case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x \<Longrightarrow> case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
case (3 x y)
[PROOF STATE]
proof (state)
this:
case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x

goal (2 subgoals):
 1. adm (\<lambda>x. case (fst x, snd x) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x)
 2. \<And>x y. case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x \<Longrightarrow> case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
hence xy: "x = y" and unwrap_wrap: "unwrap\<cdot>(wrap\<cdot>x) = x"
[PROOF STATE]
proof (prove)
using this:
case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x

goal (1 subgoal):
 1. x = y &&& unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = y
unwrap\<cdot>(wrap\<cdot>x) = x

goal (2 subgoals):
 1. adm (\<lambda>x. case (fst x, snd x) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x)
 2. \<And>x y. case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x \<Longrightarrow> case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
from body_body' xy unwrap_wrap
[PROOF STATE]
proof (chain)
picking this:
(unwrap oo wrap)\<cdot>?r = ?r \<Longrightarrow> (unwrap oo body oo wrap)\<cdot>?r = body'\<cdot>?r
x = y
unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
have "(unwrap oo body oo wrap)\<cdot>x = body'\<cdot>y"
[PROOF STATE]
proof (prove)
using this:
(unwrap oo wrap)\<cdot>?r = ?r \<Longrightarrow> (unwrap oo body oo wrap)\<cdot>?r = body'\<cdot>?r
x = y
unwrap\<cdot>(wrap\<cdot>x) = x

goal (1 subgoal):
 1. (unwrap oo body oo wrap)\<cdot>x = body'\<cdot>y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(unwrap oo body oo wrap)\<cdot>x = body'\<cdot>y

goal (2 subgoals):
 1. adm (\<lambda>x. case (fst x, snd x) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x)
 2. \<And>x y. case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x \<Longrightarrow> case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(unwrap oo body oo wrap)\<cdot>x = body'\<cdot>y

goal (2 subgoals):
 1. adm (\<lambda>x. case (fst x, snd x) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x)
 2. \<And>x y. case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x \<Longrightarrow> case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
from wrap_unwrap
[PROOF STATE]
proof (chain)
picking this:
wrap oo unwrap = ID
[PROOF STEP]
have "unwrap\<cdot>(wrap\<cdot>((unwrap oo body oo wrap)\<cdot>x)) = (unwrap oo body oo wrap)\<cdot>x"
[PROOF STATE]
proof (prove)
using this:
wrap oo unwrap = ID

goal (1 subgoal):
 1. unwrap\<cdot>(wrap\<cdot>((unwrap oo body oo wrap)\<cdot>x)) = (unwrap oo body oo wrap)\<cdot>x
[PROOF STEP]
by (simp add: cfun_eq_iff)
[PROOF STATE]
proof (state)
this:
unwrap\<cdot>(wrap\<cdot>((unwrap oo body oo wrap)\<cdot>x)) = (unwrap oo body oo wrap)\<cdot>x

goal (2 subgoals):
 1. adm (\<lambda>x. case (fst x, snd x) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x)
 2. \<And>x y. case (x, y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x \<Longrightarrow> case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(unwrap oo body oo wrap)\<cdot>x = body'\<cdot>y
unwrap\<cdot>(wrap\<cdot>((unwrap oo body oo wrap)\<cdot>x)) = (unwrap oo body oo wrap)\<cdot>x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(unwrap oo body oo wrap)\<cdot>x = body'\<cdot>y
unwrap\<cdot>(wrap\<cdot>((unwrap oo body oo wrap)\<cdot>x)) = (unwrap oo body oo wrap)\<cdot>x

goal (1 subgoal):
 1. case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
case ((unwrap oo body oo wrap)\<cdot>x, body'\<cdot>y) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x

goal (1 subgoal):
 1. adm (\<lambda>x. case (fst x, snd x) of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
case (fix\<cdot>(unwrap oo body oo wrap), fix\<cdot>body') of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x

goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
case (fix\<cdot>(unwrap oo body oo wrap), fix\<cdot>body') of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x

goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
using worker_wrapper_id[OF wrap_unwrap refl]
[PROOF STATE]
proof (prove)
using this:
case (fix\<cdot>(unwrap oo body oo wrap), fix\<cdot>body') of (x, y) \<Rightarrow> x = y \<and> unwrap\<cdot>(wrap\<cdot>x) = x
fix\<cdot>?body = wrap\<cdot>(fix\<cdot>(unwrap oo ?body oo wrap))

goal (1 subgoal):
 1. fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fix\<cdot>body = wrap\<cdot>(fix\<cdot>body')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma from_cnf_less_\<omega>_exp:
  assumes "\<forall>k \<in> set ks. k < l"
  shows "from_cnf ks < \<omega> ** l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_cnf ks < \<omega> ** l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>set ks. k < l

goal (1 subgoal):
 1. from_cnf ks < \<omega> ** l
[PROOF STEP]
by (induct ks) (auto simp: additive_principal.sum_less additive_principal_omega_exp)


[STATEMENT]
lemma from_cnf_0_iff[simp]: "from_cnf ks = 0 \<longleftrightarrow> ks = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (from_cnf ks = 0) = (ks = [])
[PROOF STEP]
by (induct ks) (auto simp: ordinal_plus_not_0)


[STATEMENT]
lemma from_cnf_append[simp]: "from_cnf (ks @ ls) = from_cnf ks + from_cnf ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_cnf (ks @ ls) = from_cnf ks + from_cnf ls
[PROOF STEP]
by (induct ks) (auto simp: ordinal_plus_assoc)


[STATEMENT]
lemma subseq_from_cnf_less_eq: "Sublist.subseq ks ls \<Longrightarrow> from_cnf ks \<le> from_cnf ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq ks ls \<Longrightarrow> from_cnf ks \<le> from_cnf ls
[PROOF STEP]
by (induct rule: list_emb.induct) (auto intro: ordinal_le_plusL order_trans)


[STATEMENT]
lemma ordinal_of_hmset_0[simp]: "ordinal_of_hmset 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset 0 = 0
[PROOF STEP]
unfolding zero_hmultiset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset (HMSet {#}) = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma ordinal_of_hmset_suc[simp]: "ordinal_of_hmset (k + 1) = ordinal_of_hmset k + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset (k + 1) = ordinal_of_hmset k + 1
[PROOF STEP]
unfolding plus_hmultiset_def one_hmultiset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset (HMSet (hmsetmset k + hmsetmset (\<omega>\<^sub>h^ 0))) = ordinal_of_hmset k + 1
[PROOF STEP]
by (cases k) simp


[STATEMENT]
lemma ordinal_of_hmset_1[simp]: "ordinal_of_hmset 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset 1 = 1
[PROOF STEP]
using ordinal_of_hmset_suc[of 0]
[PROOF STATE]
proof (prove)
using this:
ordinal_of_hmset (0 + 1) = ordinal_of_hmset 0 + 1

goal (1 subgoal):
 1. ordinal_of_hmset 1 = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma ordinal_of_hmset_singleton[simp]: "ordinal_of_hmset (\<omega>^k) = \<omega> ** ordinal_of_hmset k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset (\<omega>\<^sub>h^ k) = \<omega> ** ordinal_of_hmset k
[PROOF STEP]
by simp


[STATEMENT]
lemma ordinal_of_hmset_iff[simp]: "ordinal_of_hmset k = 0 \<longleftrightarrow> k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ordinal_of_hmset k = 0) = (k = 0)
[PROOF STEP]
by (induct k) auto