[STATEMENT]
lemma apx_meet_L:
  assumes "y \<sqsubseteq> x"
    shows "x \<sqinter> L \<le> y \<sqinter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
have "x \<sqinter> L = C x \<sqinter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> L = C x \<sqinter> L
[PROOF STEP]
by (simp add: inf.left_commute inf.sup_monoid.add_assoc n_L_top_meet_L)
[PROOF STATE]
proof (state)
this:
x \<sqinter> L = C x \<sqinter> L

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> L = C x \<sqinter> L

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
have "... \<le> (y \<squnion> n(y) * top) \<sqinter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C x \<sqinter> L \<le> (y \<squnion> n y * top) \<sqinter> L
[PROOF STEP]
using assms apx_def inf.sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
y \<sqsubseteq> x
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)
?y \<le> ?x \<Longrightarrow> ?y \<sqinter> ?z \<le> ?x \<sqinter> ?z

goal (1 subgoal):
 1. C x \<sqinter> L \<le> (y \<squnion> n y * top) \<sqinter> L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C x \<sqinter> L \<le> (y \<squnion> n y * top) \<sqinter> L

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C x \<sqinter> L \<le> (y \<squnion> n y * top) \<sqinter> L

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
have "... = (y \<sqinter> L) \<squnion> (n(y) * top \<sqinter> L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<squnion> n y * top) \<sqinter> L = y \<sqinter> L \<squnion> n y * top \<sqinter> L
[PROOF STEP]
by (simp add: inf_sup_distrib2)
[PROOF STATE]
proof (state)
this:
(y \<squnion> n y * top) \<sqinter> L = y \<sqinter> L \<squnion> n y * top \<sqinter> L

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y \<squnion> n y * top) \<sqinter> L = y \<sqinter> L \<squnion> n y * top \<sqinter> L

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
have "... \<le> (y \<sqinter> L) \<squnion> n(y \<sqinter> L) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sqinter> L \<squnion> n y * top \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top
[PROOF STEP]
using n_n_meet_L sup_right_isotone
[PROOF STATE]
proof (prove)
using this:
n ?x = n (?x \<sqinter> L)
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y

goal (1 subgoal):
 1. y \<sqinter> L \<squnion> n y * top \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y \<sqinter> L \<squnion> n y * top \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
by (metis le_iff_sup inf_le2 n_less_eq_char)
[PROOF STATE]
proof (state)
this:
x \<sqinter> L \<le> y \<sqinter> L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sup_apx_left_isotone_2:
  assumes "x \<sqsubseteq> y"
    shows "x \<squnion> z \<sqsubseteq> y \<squnion> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
have 1: "x \<squnion> z \<le> y \<squnion> z \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> z \<le> y \<squnion> z \<squnion> L
[PROOF STEP]
by (smt assms sup_assoc sup_commute sup_left_isotone apx_def)
[PROOF STATE]
proof (state)
this:
x \<squnion> z \<le> y \<squnion> z \<squnion> L

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
have "C (y \<squnion> z) \<le> x \<squnion> n(x) * top \<squnion> C z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (y \<squnion> z) \<le> x \<squnion> n x * top \<squnion> C z
[PROOF STEP]
using assms apx_def inf_sup_distrib1 sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
x \<sqsubseteq> y
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)
?x \<sqinter> (?y \<squnion> ?z) = ?x \<sqinter> ?y \<squnion> ?x \<sqinter> ?z
?x \<le> ?y \<Longrightarrow> ?x \<squnion> ?z \<le> ?y \<squnion> ?z

goal (1 subgoal):
 1. C (y \<squnion> z) \<le> x \<squnion> n x * top \<squnion> C z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C (y \<squnion> z) \<le> x \<squnion> n x * top \<squnion> C z

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (y \<squnion> z) \<le> x \<squnion> n x * top \<squnion> C z

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
have "... \<le> x \<squnion> z \<squnion> n(x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> n x * top \<squnion> C z \<le> x \<squnion> z \<squnion> n x * top
[PROOF STEP]
using inf.coboundedI1 inf.sup_monoid.add_commute sup.cobounded1 sup.cobounded2 sup_assoc sup_least sup_right_isotone
[PROOF STATE]
proof (prove)
using this:
?a \<le> ?c \<Longrightarrow> ?a \<sqinter> ?b \<le> ?c
?a \<sqinter> ?b = ?b \<sqinter> ?a
?a \<le> ?a \<squnion> ?b
?b \<le> ?a \<squnion> ?b
?x \<squnion> ?y \<squnion> ?z = ?x \<squnion> (?y \<squnion> ?z)
\<lbrakk>?y \<le> ?x; ?z \<le> ?x\<rbrakk> \<Longrightarrow> ?y \<squnion> ?z \<le> ?x
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y

goal (1 subgoal):
 1. x \<squnion> n x * top \<squnion> C z \<le> x \<squnion> z \<squnion> n x * top
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<squnion> n x * top \<squnion> C z \<le> x \<squnion> z \<squnion> n x * top

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<squnion> n x * top \<squnion> C z \<le> x \<squnion> z \<squnion> n x * top

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
have "... \<le> x \<squnion> z \<squnion> n(x \<squnion> z) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> z \<squnion> n x * top \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top
[PROOF STEP]
using mult_isotone n_left_upper_bound semiring.add_left_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?w \<le> ?y; ?x \<le> ?z\<rbrakk> \<Longrightarrow> ?w * ?x \<le> ?y * ?z
n ?x \<le> n (?x \<squnion> ?y)
?a \<le> ?b \<Longrightarrow> ?c \<squnion> ?a \<le> ?c \<squnion> ?b

goal (1 subgoal):
 1. x \<squnion> z \<squnion> n x * top \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x \<squnion> z \<squnion> n x * top \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
C (y \<squnion> z) \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C (y \<squnion> z) \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
using 1 apx_def
[PROOF STATE]
proof (prove)
using this:
C (y \<squnion> z) \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top
x \<squnion> z \<le> y \<squnion> z \<squnion> L
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<squnion> z \<sqsubseteq> y \<squnion> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_apx_left_isotone_2:
  assumes "x \<sqsubseteq> y"
    shows "x * z \<sqsubseteq> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
have "x * z \<le> y * z \<squnion> L * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<le> y * z \<squnion> L * z
[PROOF STEP]
by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
[PROOF STATE]
proof (state)
this:
x * z \<le> y * z \<squnion> L * z

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
hence 1: "x * z \<le> y * z \<squnion> L"
[PROOF STATE]
proof (prove)
using this:
x * z \<le> y * z \<squnion> L * z

goal (1 subgoal):
 1. x * z \<le> y * z \<squnion> L
[PROOF STEP]
using n_L_below_L order_lesseq_imp semiring.add_left_mono
[PROOF STATE]
proof (prove)
using this:
x * z \<le> y * z \<squnion> L * z
L * ?x \<le> L
(\<forall>z\<ge>?x. ?y \<le> z) = (?y \<le> ?x)
?a \<le> ?b \<Longrightarrow> ?c \<squnion> ?a \<le> ?c \<squnion> ?b

goal (1 subgoal):
 1. x * z \<le> y * z \<squnion> L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x * z \<le> y * z \<squnion> L

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
have "C (y * z) = C y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (y * z) = C y * z
[PROOF STEP]
by (simp add: n_L_T_meet_mult)
[PROOF STATE]
proof (state)
this:
C (y * z) = C y * z

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (y * z) = C y * z

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
have "... \<le> x * z \<squnion> n(x) * top * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C y * z \<le> x * z \<squnion> n x * top * z
[PROOF STEP]
by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
[PROOF STATE]
proof (state)
this:
C y * z \<le> x * z \<squnion> n x * top * z

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C y * z \<le> x * z \<squnion> n x * top * z

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
have "... \<le> x * z \<squnion> n(x * z) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<squnion> n x * top * z \<le> x * z \<squnion> n (x * z) * top
[PROOF STEP]
by (simp add: n_top_split)
[PROOF STATE]
proof (state)
this:
x * z \<squnion> n x * top * z \<le> x * z \<squnion> n (x * z) * top

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
C (y * z) \<le> x * z \<squnion> n (x * z) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C (y * z) \<le> x * z \<squnion> n (x * z) * top

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
C (y * z) \<le> x * z \<squnion> n (x * z) * top
x * z \<le> y * z \<squnion> L

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
by (simp add: apx_def)
[PROOF STATE]
proof (state)
this:
x * z \<sqsubseteq> y * z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_apx_right_isotone_2:
  assumes "x \<sqsubseteq> y"
    shows "z * x \<sqsubseteq> z * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "z * x \<le> z * y \<squnion> z * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * x \<le> z * y \<squnion> z * L
[PROOF STEP]
by (metis assms apx_def mult_left_dist_sup mult_right_isotone)
[PROOF STATE]
proof (state)
this:
z * x \<le> z * y \<squnion> z * L

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z * x \<le> z * y \<squnion> z * L

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "... \<le> z * y \<squnion> z * bot \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * y \<squnion> z * L \<le> z * y \<squnion> z * bot \<squnion> L
[PROOF STEP]
using n_L_split_L semiring.add_left_mono sup_assoc
[PROOF STATE]
proof (prove)
using this:
?x * L \<le> ?x * bot \<squnion> L
?a \<le> ?b \<Longrightarrow> ?c \<squnion> ?a \<le> ?c \<squnion> ?b
?x \<squnion> ?y \<squnion> ?z = ?x \<squnion> (?y \<squnion> ?z)

goal (1 subgoal):
 1. z * y \<squnion> z * L \<le> z * y \<squnion> z * bot \<squnion> L
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
z * y \<squnion> z * L \<le> z * y \<squnion> z * bot \<squnion> L

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
z * x \<le> z * y \<squnion> z * bot \<squnion> L
[PROOF STEP]
have 1: "z * x \<le> z * y \<squnion> L"
[PROOF STATE]
proof (prove)
using this:
z * x \<le> z * y \<squnion> z * bot \<squnion> L

goal (1 subgoal):
 1. z * x \<le> z * y \<squnion> L
[PROOF STEP]
using mult_right_isotone sup.absorb_iff1
[PROOF STATE]
proof (prove)
using this:
z * x \<le> z * y \<squnion> z * bot \<squnion> L
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
(?b \<le> ?a) = (?a \<squnion> ?b = ?a)

goal (1 subgoal):
 1. z * x \<le> z * y \<squnion> L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z * x \<le> z * y \<squnion> L

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "C (z * y) \<le> z * C y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (z * y) \<le> z * C y
[PROOF STEP]
by (simp add: n_L_T_meet_mult n_L_T_meet_mult_propagate)
[PROOF STATE]
proof (state)
this:
C (z * y) \<le> z * C y

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (z * y) \<le> z * C y

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "... \<le> z * (x \<squnion> n(x) * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * C y \<le> z * (x \<squnion> n x * top)
[PROOF STEP]
using assms apx_def mult_right_isotone
[PROOF STATE]
proof (prove)
using this:
x \<sqsubseteq> y
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y

goal (1 subgoal):
 1. z * C y \<le> z * (x \<squnion> n x * top)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z * C y \<le> z * (x \<squnion> n x * top)

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z * C y \<le> z * (x \<squnion> n x * top)

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "... = z * x \<squnion> z * n(x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * (x \<squnion> n x * top) = z * x \<squnion> z * n x * top
[PROOF STEP]
by (simp add: mult_left_dist_sup mult_assoc)
[PROOF STATE]
proof (state)
this:
z * (x \<squnion> n x * top) = z * x \<squnion> z * n x * top

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z * (x \<squnion> n x * top) = z * x \<squnion> z * n x * top

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "... \<le> z * x \<squnion> n(z * x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * x \<squnion> z * n x * top \<le> z * x \<squnion> n (z * x) * top
[PROOF STEP]
by (simp add: n_split_top)
[PROOF STATE]
proof (state)
this:
z * x \<squnion> z * n x * top \<le> z * x \<squnion> n (z * x) * top

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
C (z * y) \<le> z * x \<squnion> n (z * x) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C (z * y) \<le> z * x \<squnion> n (z * x) * top

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
using 1 apx_def
[PROOF STATE]
proof (prove)
using this:
C (z * y) \<le> z * x \<squnion> n (z * x) * top
z * x \<le> z * y \<squnion> L
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z * x \<sqsubseteq> z * y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma meet_L_apx_isotone:
  "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> L \<sqsubseteq> y \<sqinter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> L \<sqsubseteq> y \<sqinter> L
[PROOF STEP]
by (smt (verit) apx_meet_L apx_def inf.cobounded2 inf.left_commute n_L_top_meet_L n_less_eq_char sup.absorb2)


[STATEMENT]
lemma n_L_apx_isotone:
  assumes "x \<sqsubseteq> y"
    shows "n(x) * L \<sqsubseteq> n(y) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x * L \<sqsubseteq> n y * L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n x * L \<sqsubseteq> n y * L
[PROOF STEP]
have "C (n(y) * L) \<le> n(C y) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (n y * L) \<le> n (C y) * L
[PROOF STEP]
by (simp add: n_C)
[PROOF STATE]
proof (state)
this:
C (n y * L) \<le> n (C y) * L

goal (1 subgoal):
 1. n x * L \<sqsubseteq> n y * L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (n y * L) \<le> n (C y) * L

goal (1 subgoal):
 1. n x * L \<sqsubseteq> n y * L
[PROOF STEP]
have "... \<le> n(x) * L \<squnion> n(n(x) * L) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (C y) * L \<le> n x * L \<squnion> n (n x * L) * top
[PROOF STEP]
by (metis assms apx_def n_add_n_top n_galois n_isotone n_n_L)
[PROOF STATE]
proof (state)
this:
n (C y) * L \<le> n x * L \<squnion> n (n x * L) * top

goal (1 subgoal):
 1. n x * L \<sqsubseteq> n y * L
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
C (n y * L) \<le> n x * L \<squnion> n (n x * L) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C (n y * L) \<le> n x * L \<squnion> n (n x * L) * top

goal (1 subgoal):
 1. n x * L \<sqsubseteq> n y * L
[PROOF STEP]
using apx_def le_inf_iff n_L_decreasing_meet_L sup.absorb2
[PROOF STATE]
proof (prove)
using this:
C (n y * L) \<le> n x * L \<squnion> n (n x * L) * top
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)
(?x \<le> ?y \<sqinter> ?z) = (?x \<le> ?y \<and> ?x \<le> ?z)
n ?x * L \<le> ?x \<sqinter> L
?a \<le> ?b \<Longrightarrow> ?a \<squnion> ?b = ?b

goal (1 subgoal):
 1. n x * L \<sqsubseteq> n y * L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n x * L \<sqsubseteq> n y * L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mu_below_l:
  "\<mu> f \<le> \<mu> f \<squnion> (\<nu> f \<sqinter> L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
by simp


[STATEMENT]
lemma l_below_nu:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> \<mu> f \<squnion> (\<nu> f \<sqinter> L) \<le> \<nu> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f\<rbrakk> \<Longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<nu> f
[PROOF STEP]
by (simp add: mu_below_nu)


[STATEMENT]
lemma n_l_nu:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> (\<mu> f \<squnion> (\<nu> f \<sqinter> L)) \<sqinter> L = \<nu> f \<sqinter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f\<rbrakk> \<Longrightarrow> (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqinter> L = \<nu> f \<sqinter> L
[PROOF STEP]
by (meson l_below_nu inf.cobounded1 inf.sup_same_context order_trans sup_ge2)


[STATEMENT]
lemma l_apx_mu:
  "\<mu> f \<squnion> (\<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f
[PROOF STEP]
have 1: "\<mu> f \<squnion> (\<nu> f \<sqinter> L) \<le> \<mu> f \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> L
[PROOF STEP]
using sup_right_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> L

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f
[PROOF STEP]
have "C (\<mu> f) \<le> \<mu> f \<squnion> (\<nu> f \<sqinter> L) \<squnion> n(\<mu> f \<squnion> (\<nu> f \<sqinter> L)) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (\<mu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
by (simp add: le_supI1)
[PROOF STATE]
proof (state)
this:
C (\<mu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
C (\<mu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f
[PROOF STEP]
using 1 apx_def
[PROOF STATE]
proof (prove)
using this:
C (\<mu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> L
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nu_below_mu_nu_nu_below_mu_nu_2:
  assumes "nu_below_mu_nu f"
    shows "nu_below_mu_nu_2 f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
have "C (\<nu> f) = C (C (\<nu> f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (\<nu> f) = C (C (\<nu> f))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C (\<nu> f) = C (C (\<nu> f))

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (\<nu> f) = C (C (\<nu> f))

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
have "... \<le> C (\<mu> f \<squnion> (\<nu> f \<sqinter> L) \<squnion> n(\<nu> f) * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (C (\<nu> f)) \<le> C (\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top)
[PROOF STEP]
using assms nu_below_mu_nu_def
[PROOF STATE]
proof (prove)
using this:
nu_below_mu_nu f
nu_below_mu_nu ?f \<equiv> C (\<nu> ?f) \<le> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<squnion> n (\<nu> ?f) * top

goal (1 subgoal):
 1. C (C (\<nu> f)) \<le> C (\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C (C (\<nu> f)) \<le> C (\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top)

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (C (\<nu> f)) \<le> C (\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top)

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
have "... = C (\<mu> f \<squnion> (\<nu> f \<sqinter> L)) \<squnion> C (n(\<nu> f) * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top) = C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> C (n (\<nu> f) * top)
[PROOF STEP]
using inf_sup_distrib1
[PROOF STATE]
proof (prove)
using this:
?x \<sqinter> (?y \<squnion> ?z) = ?x \<sqinter> ?y \<squnion> ?x \<sqinter> ?z

goal (1 subgoal):
 1. C (\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top) = C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> C (n (\<nu> f) * top)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C (\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top) = C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> C (n (\<nu> f) * top)

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top) = C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> C (n (\<nu> f) * top)

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
have "... = C (\<mu> f \<squnion> (\<nu> f \<sqinter> L)) \<squnion> n(\<nu> f) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> C (n (\<nu> f) * top) = C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> n (\<nu> f) * top
[PROOF STEP]
by (simp add: C_n_mult_closed)
[PROOF STATE]
proof (state)
this:
C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> C (n (\<nu> f) * top) = C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> n (\<nu> f) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> C (n (\<nu> f) * top) = C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> n (\<nu> f) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
have "... \<le> \<mu> f \<squnion> (\<nu> f \<sqinter> L) \<squnion> n(\<nu> f) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> n (\<nu> f) * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top
[PROOF STEP]
using inf_le2 sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<sqinter> ?y \<le> ?y
?x \<le> ?y \<Longrightarrow> ?x \<squnion> ?z \<le> ?y \<squnion> ?z

goal (1 subgoal):
 1. C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> n (\<nu> f) * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> n (\<nu> f) * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> n (\<nu> f) * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
have "... = \<mu> f \<squnion> (\<nu> f \<sqinter> L) \<squnion> n(\<nu> f \<sqinter> L) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top = \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f \<sqinter> L) * top
[PROOF STEP]
using n_n_meet_L
[PROOF STATE]
proof (prove)
using this:
n ?x = n (?x \<sqinter> L)

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top = \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f \<sqinter> L) * top
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top = \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top = \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
have "... \<le> \<mu> f \<squnion> (\<nu> f \<sqinter> L) \<squnion> n(\<mu> f \<squnion> (\<nu> f \<sqinter> L)) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f \<sqinter> L) * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
using mult_isotone n_right_upper_bound semiring.add_left_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?w \<le> ?y; ?x \<le> ?z\<rbrakk> \<Longrightarrow> ?w * ?x \<le> ?y * ?z
n ?x \<le> n (?y \<squnion> ?x)
?a \<le> ?b \<Longrightarrow> ?c \<squnion> ?a \<le> ?c \<squnion> ?b

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f \<sqinter> L) * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f \<sqinter> L) * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
by (simp add: nu_below_mu_nu_2_def)
[PROOF STATE]
proof (state)
this:
nu_below_mu_nu_2 f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nu_below_mu_nu_2_nu_below_mu_nu:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "nu_below_mu_nu_2 f"
    shows "nu_below_mu_nu f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nu_below_mu_nu f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nu_below_mu_nu f
[PROOF STEP]
have "C (\<nu> f) \<le> \<mu> f \<squnion> (\<nu> f \<sqinter> L) \<squnion> n(\<mu> f \<squnion> (\<nu> f \<sqinter> L)) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
using assms(3) nu_below_mu_nu_2_def
[PROOF STATE]
proof (prove)
using this:
nu_below_mu_nu_2 f
nu_below_mu_nu_2 ?f \<equiv> C (\<nu> ?f) \<le> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<squnion> n (\<mu> ?f \<squnion> \<nu> ?f \<sqinter> L) * top

goal (1 subgoal):
 1. C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu f
[PROOF STEP]
have "... \<le> \<mu> f \<squnion> (\<nu> f \<sqinter> L) \<squnion> n(\<nu> f) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top
[PROOF STEP]
by (metis assms(1,2) order.eq_iff n_n_meet_L n_l_nu)
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top

goal (1 subgoal):
 1. nu_below_mu_nu f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top

goal (1 subgoal):
 1. nu_below_mu_nu f
[PROOF STEP]
using nu_below_mu_nu_def
[PROOF STATE]
proof (prove)
using this:
C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<nu> f) * top
nu_below_mu_nu ?f \<equiv> C (\<nu> ?f) \<le> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<squnion> n (\<nu> ?f) * top

goal (1 subgoal):
 1. nu_below_mu_nu f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
nu_below_mu_nu f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nu_below_mu_nu_equivalent:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> (nu_below_mu_nu f \<longleftrightarrow> nu_below_mu_nu_2 f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f\<rbrakk> \<Longrightarrow> nu_below_mu_nu f = nu_below_mu_nu_2 f
[PROOF STEP]
using nu_below_mu_nu_2_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f; nu_below_mu_nu_2 ?f\<rbrakk> \<Longrightarrow> nu_below_mu_nu ?f
nu_below_mu_nu ?f \<Longrightarrow> nu_below_mu_nu_2 ?f

goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f\<rbrakk> \<Longrightarrow> nu_below_mu_nu f = nu_below_mu_nu_2 f
[PROOF STEP]
by blast


[STATEMENT]
lemma nu_below_mu_nu_2_mu_nu_apx_nu:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "nu_below_mu_nu_2 f"
    shows "mu_nu_apx_nu f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mu_nu_apx_nu f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mu_nu_apx_nu f
[PROOF STEP]
have "\<mu> f \<squnion> (\<nu> f \<sqinter> L) \<le> \<nu> f \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<nu> f \<squnion> L
[PROOF STEP]
using assms(1,2) l_below_nu le_supI1
[PROOF STATE]
proof (prove)
using this:
has_least_fixpoint f
has_greatest_fixpoint f
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f\<rbrakk> \<Longrightarrow> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<le> \<nu> ?f
?x \<le> ?a \<Longrightarrow> ?x \<le> ?a \<squnion> ?b

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<nu> f \<squnion> L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<nu> f \<squnion> L

goal (1 subgoal):
 1. mu_nu_apx_nu f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<nu> f \<squnion> L

goal (1 subgoal):
 1. mu_nu_apx_nu f
[PROOF STEP]
using assms(3) apx_def mu_nu_apx_nu_def nu_below_mu_nu_2_def
[PROOF STATE]
proof (prove)
using this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<nu> f \<squnion> L
nu_below_mu_nu_2 f
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)
mu_nu_apx_nu ?f \<equiv> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<sqsubseteq> \<nu> ?f
nu_below_mu_nu_2 ?f \<equiv> C (\<nu> ?f) \<le> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<squnion> n (\<mu> ?f \<squnion> \<nu> ?f \<sqinter> L) * top

goal (1 subgoal):
 1. mu_nu_apx_nu f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mu_nu_apx_nu f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mu_nu_apx_nu_mu_nu_apx_meet:
  assumes "mu_nu_apx_nu f"
    shows "mu_nu_apx_meet f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mu_nu_apx_meet f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mu_nu_apx_meet f
[PROOF STEP]
let ?l = "\<mu> f \<squnion> (\<nu> f \<sqinter> L)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mu_nu_apx_meet f
[PROOF STEP]
have "is_apx_meet (\<mu> f) (\<nu> f) ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_apx_meet (\<mu> f) (\<nu> f) (\<mu> f \<squnion> \<nu> f \<sqinter> L)
[PROOF STEP]
proof (unfold is_apx_meet_def, intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f
 2. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<nu> f
 3. \<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
show "?l \<sqsubseteq> \<mu> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f
[PROOF STEP]
by (simp add: l_apx_mu)
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f

goal (2 subgoals):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<nu> f
 2. \<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
show "?l \<sqsubseteq> \<nu> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<nu> f
[PROOF STEP]
using assms mu_nu_apx_nu_def
[PROOF STATE]
proof (prove)
using this:
mu_nu_apx_nu f
mu_nu_apx_nu ?f \<equiv> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<sqsubseteq> \<nu> ?f

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<nu> f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<nu> f

goal (1 subgoal):
 1. \<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
show "\<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
by (metis apx_meet_L le_inf_iff sup.absorb1 sup_apx_left_isotone)
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_apx_meet (\<mu> f) (\<nu> f) (\<mu> f \<squnion> \<nu> f \<sqinter> L)

goal (1 subgoal):
 1. mu_nu_apx_meet f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_apx_meet (\<mu> f) (\<nu> f) (\<mu> f \<squnion> \<nu> f \<sqinter> L)

goal (1 subgoal):
 1. mu_nu_apx_meet f
[PROOF STEP]
by (simp add: apx_meet_char mu_nu_apx_meet_def)
[PROOF STATE]
proof (state)
this:
mu_nu_apx_meet f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mu_nu_apx_meet_apx_meet_below_nu:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> mu_nu_apx_meet f \<Longrightarrow> apx_meet_below_nu f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; mu_nu_apx_meet f\<rbrakk> \<Longrightarrow> apx_meet_below_nu f
[PROOF STEP]
using apx_meet_below_nu_def l_below_nu mu_nu_apx_meet_def
[PROOF STATE]
proof (prove)
using this:
apx_meet_below_nu ?f \<equiv> has_apx_meet (\<mu> ?f) (\<nu> ?f) \<and> \<mu> ?f \<triangle> \<nu> ?f \<le> \<nu> ?f
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f\<rbrakk> \<Longrightarrow> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<le> \<nu> ?f
mu_nu_apx_meet ?f \<equiv> has_apx_meet (\<mu> ?f) (\<nu> ?f) \<and> \<mu> ?f \<triangle> \<nu> ?f = \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L

goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; mu_nu_apx_meet f\<rbrakk> \<Longrightarrow> apx_meet_below_nu f
[PROOF STEP]
by auto


[STATEMENT]
lemma apx_meet_below_nu_nu_below_mu_nu_2:
  assumes "apx_meet_below_nu f"
    shows "nu_below_mu_nu_2 f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
let ?l = "\<mu> f \<squnion> (\<nu> f \<sqinter> L)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
have "\<forall>m . m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<longrightarrow> C (\<nu> f) \<le> ?l \<squnion> n(?l) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
show "m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<longrightarrow> C (\<nu> f) \<le> ?l \<squnion> n(?l) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<Longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
assume 1: "m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f"
[PROOF STATE]
proof (state)
this:
m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f

goal (1 subgoal):
 1. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<Longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
hence "m \<le> ?l"
[PROOF STATE]
proof (prove)
using this:
m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f

goal (1 subgoal):
 1. m \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
by (smt (z3) apx_def sup.left_commute sup_inf_distrib1 sup_left_divisibility)
[PROOF STATE]
proof (state)
this:
m \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L

goal (1 subgoal):
 1. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<Longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
hence "m \<squnion> n(m) * top \<le> ?l \<squnion> n(?l) * top"
[PROOF STATE]
proof (prove)
using this:
m \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L

goal (1 subgoal):
 1. m \<squnion> n m * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
by (metis sup_mono mult_left_isotone n_isotone)
[PROOF STATE]
proof (state)
this:
m \<squnion> n m * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<Longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
thus "C (\<nu> f) \<le> ?l \<squnion> n(?l) * top"
[PROOF STATE]
proof (prove)
using this:
m \<squnion> n m * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
using 1 apx_def order.trans
[PROOF STATE]
proof (prove)
using this:
m \<squnion> n m * top \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

goal (1 subgoal):
 1. C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>m. m \<sqsubseteq> \<mu> f \<and> m \<sqsubseteq> \<nu> f \<and> m \<le> \<nu> f \<longrightarrow> C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_2 f
[PROOF STEP]
by (smt (verit, ccfv_threshold) assms apx_meet_below_nu_def apx_meet_same apx_meet_unique is_apx_meet_def nu_below_mu_nu_2_def)
[PROOF STATE]
proof (state)
this:
nu_below_mu_nu_2 f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_apx_least_fixpoint_kappa_apx_meet:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "apx.has_least_fixpoint f"
    shows "kappa_apx_meet f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kappa_apx_meet f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. kappa_apx_meet f
[PROOF STEP]
have 1: "\<forall>w . w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> C (\<kappa> f) \<le> w \<squnion> n(w) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> C (\<kappa> f) \<le> w \<squnion> n w * top
[PROOF STEP]
by (metis assms(2,3) apx_def inf.sup_right_isotone order_trans kappa_below_nu)
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> C (\<kappa> f) \<le> w \<squnion> n w * top

goal (1 subgoal):
 1. kappa_apx_meet f
[PROOF STEP]
have "\<forall>w . w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<le> \<kappa> f \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<le> \<kappa> f \<squnion> L
[PROOF STEP]
by (metis assms(1,3) sup_left_isotone apx_def mu_below_kappa order_trans)
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<le> \<kappa> f \<squnion> L

goal (1 subgoal):
 1. kappa_apx_meet f
[PROOF STEP]
hence "\<forall>w . w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<kappa> f"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<le> \<kappa> f \<squnion> L

goal (1 subgoal):
 1. \<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<kappa> f
[PROOF STEP]
using 1 apx_def
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<le> \<kappa> f \<squnion> L
\<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> C (\<kappa> f) \<le> w \<squnion> n w * top
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)

goal (1 subgoal):
 1. \<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<kappa> f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<kappa> f

goal (1 subgoal):
 1. kappa_apx_meet f
[PROOF STEP]
hence "is_apx_meet (\<mu> f) (\<nu> f) (\<kappa> f)"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<sqsubseteq> \<mu> f \<and> w \<sqsubseteq> \<nu> f \<longrightarrow> w \<sqsubseteq> \<kappa> f

goal (1 subgoal):
 1. is_apx_meet (\<mu> f) (\<nu> f) (\<kappa> f)
[PROOF STEP]
by (simp add: assms is_apx_meet_def kappa_apx_below_mu kappa_apx_below_nu)
[PROOF STATE]
proof (state)
this:
is_apx_meet (\<mu> f) (\<nu> f) (\<kappa> f)

goal (1 subgoal):
 1. kappa_apx_meet f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_apx_meet (\<mu> f) (\<nu> f) (\<kappa> f)

goal (1 subgoal):
 1. kappa_apx_meet f
[PROOF STEP]
by (simp add: assms(3) kappa_apx_meet_def apx_meet_char)
[PROOF STATE]
proof (state)
this:
kappa_apx_meet f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kappa_apx_meet_apx_meet_below_nu:
  "has_greatest_fixpoint f \<Longrightarrow> kappa_apx_meet f \<Longrightarrow> apx_meet_below_nu f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_greatest_fixpoint f; kappa_apx_meet f\<rbrakk> \<Longrightarrow> apx_meet_below_nu f
[PROOF STEP]
using apx_meet_below_nu_def kappa_apx_meet_def kappa_below_nu
[PROOF STATE]
proof (prove)
using this:
apx_meet_below_nu ?f \<equiv> has_apx_meet (\<mu> ?f) (\<nu> ?f) \<and> \<mu> ?f \<triangle> \<nu> ?f \<le> \<nu> ?f
kappa_apx_meet ?f \<equiv> order.has_least_fixpoint (\<sqsubseteq>) ?f \<and> has_apx_meet (\<mu> ?f) (\<nu> ?f) \<and> \<kappa> ?f = \<mu> ?f \<triangle> \<nu> ?f
\<lbrakk>has_greatest_fixpoint ?f; order.has_least_fixpoint (\<sqsubseteq>) ?f\<rbrakk> \<Longrightarrow> \<kappa> ?f \<le> \<nu> ?f

goal (1 subgoal):
 1. \<lbrakk>has_greatest_fixpoint f; kappa_apx_meet f\<rbrakk> \<Longrightarrow> apx_meet_below_nu f
[PROOF STEP]
by force


[STATEMENT]
lemma apx_meet_below_nu_kappa_mu_nu:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "isotone f"
      and "apx.isotone f"
      and "apx_meet_below_nu f"
    shows "kappa_mu_nu f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
let ?l = "\<mu> f \<squnion> (\<nu> f \<sqinter> L)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
let ?m = "\<mu> f \<triangle> \<nu> f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
have 1: "?m = ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<triangle> \<nu> f = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
by (metis assms(1,2,5) apx_meet_below_nu_nu_below_mu_nu_2 mu_nu_apx_meet_def mu_nu_apx_nu_mu_nu_apx_meet nu_below_mu_nu_2_mu_nu_apx_nu)
[PROOF STATE]
proof (state)
this:
\<mu> f \<triangle> \<nu> f = \<mu> f \<squnion> \<nu> f \<sqinter> L

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
have 2: "?l \<le> f(?l) \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
have "?l \<le> \<mu> f \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> L
[PROOF STEP]
using sup_right_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> L

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> L

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
have "... = f(\<mu> f) \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> L = f (\<mu> f) \<squnion> L
[PROOF STEP]
by (simp add: assms(1) mu_unfold)
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> L = f (\<mu> f) \<squnion> L

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> L = f (\<mu> f) \<squnion> L

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
have "... \<le> f(?l) \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<mu> f) \<squnion> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
using assms(3) isotone_def sup_ge1 sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
isotone f
isotone ?f \<equiv> \<forall>x y. x \<le> y \<longrightarrow> ?f x \<le> ?f y
?x \<le> ?x \<squnion> ?y
?x \<le> ?y \<Longrightarrow> ?x \<squnion> ?z \<le> ?y \<squnion> ?z

goal (1 subgoal):
 1. f (\<mu> f) \<squnion> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f (\<mu> f) \<squnion> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
show "?l \<le> f(?l) \<squnion> L"
[PROOF STATE]
proof (prove)
using this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
have "C (f(?l)) \<le> ?l \<squnion> n(?l) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
have "C (f(?l)) \<le> C (f(\<nu> f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> C (f (\<nu> f))
[PROOF STEP]
using assms(1-3) l_below_nu inf.sup_right_isotone isotone_def
[PROOF STATE]
proof (prove)
using this:
has_least_fixpoint f
has_greatest_fixpoint f
isotone f
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f\<rbrakk> \<Longrightarrow> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<le> \<nu> ?f
?y \<le> ?x \<Longrightarrow> ?z \<sqinter> ?y \<le> ?z \<sqinter> ?x
isotone ?f \<equiv> \<forall>x y. x \<le> y \<longrightarrow> ?f x \<le> ?f y

goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> C (f (\<nu> f))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> C (f (\<nu> f))

goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> C (f (\<nu> f))

goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
have "... = C (\<nu> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (f (\<nu> f)) = C (\<nu> f)
[PROOF STEP]
by (metis assms(2) nu_unfold)
[PROOF STATE]
proof (state)
this:
C (f (\<nu> f)) = C (\<nu> f)

goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (f (\<nu> f)) = C (\<nu> f)

goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
have "... \<le> ?l \<squnion> n(?l) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
by (metis assms(5) apx_meet_below_nu_nu_below_mu_nu_2 nu_below_mu_nu_2_def)
[PROOF STATE]
proof (state)
this:
C (\<nu> f) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
show "C (f(?l)) \<le> ?l \<squnion> n(?l) * top"
[PROOF STATE]
proof (prove)
using this:
C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
hence 3: "?l \<sqsubseteq> f(?l)"
[PROOF STATE]
proof (prove)
using this:
C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> f (\<mu> f \<squnion> \<nu> f \<sqinter> L)
[PROOF STEP]
using 2 apx_def
[PROOF STATE]
proof (prove)
using this:
C (f (\<mu> f \<squnion> \<nu> f \<sqinter> L)) \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<squnion> L
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> f (\<mu> f \<squnion> \<nu> f \<sqinter> L)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> f (\<mu> f \<squnion> \<nu> f \<sqinter> L)

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
have 4: "f(?l) \<sqsubseteq> \<mu> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f
[PROOF STEP]
have "?l \<sqsubseteq> \<mu> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f
[PROOF STEP]
by (simp add: l_apx_mu)
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f

goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f
[PROOF STEP]
thus "f(?l) \<sqsubseteq> \<mu> f"
[PROOF STATE]
proof (prove)
using this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<mu> f

goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f
[PROOF STEP]
by (metis assms(1,4) mu_unfold ord.isotone_def)
[PROOF STATE]
proof (state)
this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
have "f(?l) \<sqsubseteq> \<nu> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<nu> f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<nu> f
[PROOF STEP]
have "?l \<sqsubseteq> \<nu> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<nu> f
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<mu> f \<triangle> \<nu> f = \<mu> f \<squnion> \<nu> f \<sqinter> L

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<nu> f
[PROOF STEP]
by (metis apx_meet_below_nu_def assms(5) apx_meet is_apx_meet_def)
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<nu> f

goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<nu> f
[PROOF STEP]
thus "f(?l) \<sqsubseteq> \<nu> f"
[PROOF STATE]
proof (prove)
using this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> \<nu> f

goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<nu> f
[PROOF STEP]
by (metis assms(2,4) nu_unfold ord.isotone_def)
[PROOF STATE]
proof (state)
this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<nu> f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<nu> f

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
hence "f(?l) \<sqsubseteq> ?l"
[PROOF STATE]
proof (prove)
using this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<nu> f

goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
using 1 4 apx_meet_below_nu_def assms(5) apx_meet is_apx_meet_def
[PROOF STATE]
proof (prove)
using this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<nu> f
\<mu> f \<triangle> \<nu> f = \<mu> f \<squnion> \<nu> f \<sqinter> L
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f
apx_meet_below_nu ?f \<equiv> has_apx_meet (\<mu> ?f) (\<nu> ?f) \<and> \<mu> ?f \<triangle> \<nu> ?f \<le> \<nu> ?f
apx_meet_below_nu f
has_apx_meet ?x ?y \<Longrightarrow> is_apx_meet ?x ?y (?x \<triangle> ?y)
is_apx_meet ?x ?y ?z \<equiv> ?z \<sqsubseteq> ?x \<and> ?z \<sqsubseteq> ?y \<and> (\<forall>w. w \<sqsubseteq> ?x \<and> w \<sqsubseteq> ?y \<longrightarrow> w \<sqsubseteq> ?z)

goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
hence 5: "f(?l) = ?l"
[PROOF STATE]
proof (prove)
using this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L

goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
using 3 apx.order.antisym
[PROOF STATE]
proof (prove)
using this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) \<sqsubseteq> \<mu> f \<squnion> \<nu> f \<sqinter> L
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> f (\<mu> f \<squnion> \<nu> f \<sqinter> L)
\<lbrakk>?a \<sqsubseteq> ?b; ?b \<sqsubseteq> ?a\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. f (\<mu> f \<squnion> \<nu> f \<sqinter> L) = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) = \<mu> f \<squnion> \<nu> f \<sqinter> L

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
have "\<forall>y . f(y) = y \<longrightarrow> ?l \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. f y = y \<longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. f y = y \<longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. f y = y \<longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
show "f(y) = y \<longrightarrow> ?l \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f y = y \<longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f y = y \<Longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
assume 6: "f(y) = y"
[PROOF STATE]
proof (state)
this:
f y = y

goal (1 subgoal):
 1. f y = y \<Longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
hence 7: "?l \<le> y \<squnion> L"
[PROOF STATE]
proof (prove)
using this:
f y = y

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> y \<squnion> L
[PROOF STEP]
using assms(1) inf.cobounded2 is_least_fixpoint_def least_fixpoint semiring.add_mono
[PROOF STATE]
proof (prove)
using this:
f y = y
has_least_fixpoint f
?a \<sqinter> ?b \<le> ?b
is_least_fixpoint ?f ?x \<equiv> ?f ?x = ?x \<and> (\<forall>y. ?f y = y \<longrightarrow> ?x \<le> y)
has_least_fixpoint ?f \<Longrightarrow> is_least_fixpoint ?f (\<mu> ?f)
\<lbrakk>?a \<le> ?b; ?c \<le> ?d\<rbrakk> \<Longrightarrow> ?a \<squnion> ?c \<le> ?b \<squnion> ?d

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> y \<squnion> L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> y \<squnion> L

goal (1 subgoal):
 1. f y = y \<Longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
have "y \<le> \<nu> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> \<nu> f
[PROOF STEP]
using 6 assms(2) greatest_fixpoint is_greatest_fixpoint_def
[PROOF STATE]
proof (prove)
using this:
f y = y
has_greatest_fixpoint f
has_greatest_fixpoint ?f \<Longrightarrow> is_greatest_fixpoint ?f (\<nu> ?f)
is_greatest_fixpoint ?f ?x \<equiv> ?f ?x = ?x \<and> (\<forall>y. ?f y = y \<longrightarrow> y \<le> ?x)

goal (1 subgoal):
 1. y \<le> \<nu> f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<le> \<nu> f

goal (1 subgoal):
 1. f y = y \<Longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
hence "C y \<le> ?l \<squnion> n(?l) * top"
[PROOF STATE]
proof (prove)
using this:
y \<le> \<nu> f

goal (1 subgoal):
 1. C y \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
using assms(5) apx_meet_below_nu_nu_below_mu_nu_2 inf.sup_right_isotone nu_below_mu_nu_2_def order_trans
[PROOF STATE]
proof (prove)
using this:
y \<le> \<nu> f
apx_meet_below_nu f
apx_meet_below_nu ?f \<Longrightarrow> nu_below_mu_nu_2 ?f
?y \<le> ?x \<Longrightarrow> ?z \<sqinter> ?y \<le> ?z \<sqinter> ?x
nu_below_mu_nu_2 ?f \<equiv> C (\<nu> ?f) \<le> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<squnion> n (\<mu> ?f \<squnion> \<nu> ?f \<sqinter> L) * top
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z

goal (1 subgoal):
 1. C y \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C y \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. f y = y \<Longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
thus "?l \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
using this:
C y \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
using 7 apx_def
[PROOF STATE]
proof (prove)
using this:
C y \<le> \<mu> f \<squnion> \<nu> f \<sqinter> L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> y \<squnion> L
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f y = y \<longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>y. f y = y \<longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y. f y = y \<longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
using 5 apx.least_fixpoint_same apx.has_least_fixpoint_def apx.is_least_fixpoint_def kappa_mu_nu_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y. f y = y \<longrightarrow> \<mu> f \<squnion> \<nu> f \<sqinter> L \<sqsubseteq> y
f (\<mu> f \<squnion> \<nu> f \<sqinter> L) = \<mu> f \<squnion> \<nu> f \<sqinter> L
order.is_least_fixpoint (\<sqsubseteq>) ?f ?x \<Longrightarrow> ?x = \<kappa> ?f
order.has_least_fixpoint (\<sqsubseteq>) ?f \<equiv> \<exists>x. order.is_least_fixpoint (\<sqsubseteq>) ?f x
order.is_least_fixpoint (\<sqsubseteq>) ?f ?x \<equiv> ?f ?x = ?x \<and> (\<forall>y. ?f y = y \<longrightarrow> ?x \<sqsubseteq> y)
kappa_mu_nu ?f \<equiv> order.has_least_fixpoint (\<sqsubseteq>) ?f \<and> \<kappa> ?f = \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L

goal (1 subgoal):
 1. kappa_mu_nu f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
kappa_mu_nu f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kappa_mu_nu_has_apx_least_fixpoint:
  "kappa_mu_nu f \<Longrightarrow> apx.has_least_fixpoint f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kappa_mu_nu f \<Longrightarrow> order.has_least_fixpoint (\<sqsubseteq>) f
[PROOF STEP]
by (simp add: kappa_mu_nu_def)


[STATEMENT]
lemma nu_below_mu_nu_kappa_mu_nu:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> isotone f \<Longrightarrow> apx.isotone f \<Longrightarrow> nu_below_mu_nu f \<Longrightarrow> kappa_mu_nu f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; isotone f; ord.isotone (\<sqsubseteq>) f; nu_below_mu_nu f\<rbrakk> \<Longrightarrow> kappa_mu_nu f
[PROOF STEP]
using apx_meet_below_nu_kappa_mu_nu mu_nu_apx_meet_apx_meet_below_nu mu_nu_apx_nu_mu_nu_apx_meet nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_nu_below_mu_nu_2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f; isotone ?f; ord.isotone (\<sqsubseteq>) ?f; apx_meet_below_nu ?f\<rbrakk> \<Longrightarrow> kappa_mu_nu ?f
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f; mu_nu_apx_meet ?f\<rbrakk> \<Longrightarrow> apx_meet_below_nu ?f
mu_nu_apx_nu ?f \<Longrightarrow> mu_nu_apx_meet ?f
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f; nu_below_mu_nu_2 ?f\<rbrakk> \<Longrightarrow> mu_nu_apx_nu ?f
nu_below_mu_nu ?f \<Longrightarrow> nu_below_mu_nu_2 ?f

goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; isotone f; ord.isotone (\<sqsubseteq>) f; nu_below_mu_nu f\<rbrakk> \<Longrightarrow> kappa_mu_nu f
[PROOF STEP]
by blast


[STATEMENT]
lemma kappa_mu_nu_nu_below_mu_nu:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> kappa_mu_nu f \<Longrightarrow> nu_below_mu_nu f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; kappa_mu_nu f\<rbrakk> \<Longrightarrow> nu_below_mu_nu f
[PROOF STEP]
by (simp add: apx_meet_below_nu_nu_below_mu_nu_2 has_apx_least_fixpoint_kappa_apx_meet kappa_apx_meet_apx_meet_below_nu kappa_mu_nu_has_apx_least_fixpoint nu_below_mu_nu_2_nu_below_mu_nu)


[STATEMENT]
lemma n_below_l:
  "x \<squnion> n(y) * L \<le> x \<squnion> (y \<sqinter> L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> n y * L \<le> x \<squnion> y \<sqinter> L
[PROOF STEP]
using n_L_decreasing_meet_L semiring.add_left_mono
[PROOF STATE]
proof (prove)
using this:
n ?x * L \<le> ?x \<sqinter> L
?a \<le> ?b \<Longrightarrow> ?c \<squnion> ?a \<le> ?c \<squnion> ?b

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


[STATEMENT]
lemma n_equal_l:
  assumes "nu_below_mu_nu_L f"
    shows "\<mu> f \<squnion> n(\<nu> f) * L = \<mu> f \<squnion> (\<nu> f \<sqinter> L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
have "\<nu> f \<sqinter> L \<le> (\<mu> f \<squnion> n(\<nu> f) * top) \<sqinter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> f \<sqinter> L \<le> (\<mu> f \<squnion> n (\<nu> f) * top) \<sqinter> L
[PROOF STEP]
by (meson assms order.trans inf.boundedI inf.cobounded2 meet_L_below_C nu_below_mu_nu_L_def)
[PROOF STATE]
proof (state)
this:
\<nu> f \<sqinter> L \<le> (\<mu> f \<squnion> n (\<nu> f) * top) \<sqinter> L

goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<nu> f \<sqinter> L \<le> (\<mu> f \<squnion> n (\<nu> f) * top) \<sqinter> L

goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
have "... \<le> \<mu> f \<squnion> (n(\<nu> f) * top \<sqinter> L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> f \<squnion> n (\<nu> f) * top) \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * top \<sqinter> L
[PROOF STEP]
by (simp add: inf.coboundedI2 inf.sup_monoid.add_commute inf_sup_distrib1)
[PROOF STATE]
proof (state)
this:
(\<mu> f \<squnion> n (\<nu> f) * top) \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * top \<sqinter> L

goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<mu> f \<squnion> n (\<nu> f) * top) \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * top \<sqinter> L

goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
have "... \<le> \<mu> f \<squnion> n(\<nu> f) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * top \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * L
[PROOF STEP]
by (simp add: n_T_meet_L)
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> n (\<nu> f) * top \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * L

goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<nu> f \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * L
[PROOF STEP]
have "\<mu> f \<squnion> (\<nu> f \<sqinter> L) \<le> \<mu> f \<squnion> n(\<nu> f) * L"
[PROOF STATE]
proof (prove)
using this:
\<nu> f \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * L

goal (1 subgoal):
 1. \<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * L

goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
thus "\<mu> f \<squnion> n(\<nu> f) * L = \<mu> f \<squnion> (\<nu> f \<sqinter> L)"
[PROOF STATE]
proof (prove)
using this:
\<mu> f \<squnion> \<nu> f \<sqinter> L \<le> \<mu> f \<squnion> n (\<nu> f) * L

goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L
[PROOF STEP]
by (meson order.antisym n_below_l)
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> n (\<nu> f) * L = \<mu> f \<squnion> \<nu> f \<sqinter> L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nu_below_mu_nu_L_nu_below_mu_nu:
  "nu_below_mu_nu_L f \<Longrightarrow> nu_below_mu_nu f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nu_below_mu_nu_L f \<Longrightarrow> nu_below_mu_nu f
[PROOF STEP]
by (metis sup_assoc sup_right_top mult_left_dist_sup n_equal_l nu_below_mu_nu_L_def nu_below_mu_nu_def)


[STATEMENT]
lemma nu_below_mu_nu_L_kappa_mu_nu_L:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> isotone f \<Longrightarrow> apx.isotone f \<Longrightarrow> nu_below_mu_nu_L f \<Longrightarrow> kappa_mu_nu_L f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; isotone f; ord.isotone (\<sqsubseteq>) f; nu_below_mu_nu_L f\<rbrakk> \<Longrightarrow> kappa_mu_nu_L f
[PROOF STEP]
using kappa_mu_nu_L_def kappa_mu_nu_def n_equal_l nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_kappa_mu_nu
[PROOF STATE]
proof (prove)
using this:
kappa_mu_nu_L ?f \<equiv> order.has_least_fixpoint (\<sqsubseteq>) ?f \<and> \<kappa> ?f = \<mu> ?f \<squnion> n (\<nu> ?f) * L
kappa_mu_nu ?f \<equiv> order.has_least_fixpoint (\<sqsubseteq>) ?f \<and> \<kappa> ?f = \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L
nu_below_mu_nu_L ?f \<Longrightarrow> \<mu> ?f \<squnion> n (\<nu> ?f) * L = \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L
nu_below_mu_nu_L ?f \<Longrightarrow> nu_below_mu_nu ?f
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f; isotone ?f; ord.isotone (\<sqsubseteq>) ?f; nu_below_mu_nu ?f\<rbrakk> \<Longrightarrow> kappa_mu_nu ?f

goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; isotone f; ord.isotone (\<sqsubseteq>) f; nu_below_mu_nu_L f\<rbrakk> \<Longrightarrow> kappa_mu_nu_L f
[PROOF STEP]
by force


[STATEMENT]
lemma nu_below_mu_nu_L_mu_nu_apx_nu_L:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> nu_below_mu_nu_L f \<Longrightarrow> mu_nu_apx_nu_L f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; nu_below_mu_nu_L f\<rbrakk> \<Longrightarrow> mu_nu_apx_nu_L f
[PROOF STEP]
using mu_nu_apx_nu_L_def mu_nu_apx_nu_def n_equal_l nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2
[PROOF STATE]
proof (prove)
using this:
mu_nu_apx_nu_L ?f \<equiv> \<mu> ?f \<squnion> n (\<nu> ?f) * L \<sqsubseteq> \<nu> ?f
mu_nu_apx_nu ?f \<equiv> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<sqsubseteq> \<nu> ?f
nu_below_mu_nu_L ?f \<Longrightarrow> \<mu> ?f \<squnion> n (\<nu> ?f) * L = \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f; nu_below_mu_nu_2 ?f\<rbrakk> \<Longrightarrow> mu_nu_apx_nu ?f
nu_below_mu_nu_L ?f \<Longrightarrow> nu_below_mu_nu ?f
nu_below_mu_nu ?f \<Longrightarrow> nu_below_mu_nu_2 ?f

goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; nu_below_mu_nu_L f\<rbrakk> \<Longrightarrow> mu_nu_apx_nu_L f
[PROOF STEP]
by auto


[STATEMENT]
lemma nu_below_mu_nu_L_mu_nu_apx_meet_L:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> nu_below_mu_nu_L f \<Longrightarrow> mu_nu_apx_meet_L f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; nu_below_mu_nu_L f\<rbrakk> \<Longrightarrow> mu_nu_apx_meet_L f
[PROOF STEP]
using mu_nu_apx_meet_L_def mu_nu_apx_meet_def mu_nu_apx_nu_mu_nu_apx_meet n_equal_l nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2
[PROOF STATE]
proof (prove)
using this:
mu_nu_apx_meet_L ?f \<equiv> has_apx_meet (\<mu> ?f) (\<nu> ?f) \<and> \<mu> ?f \<triangle> \<nu> ?f = \<mu> ?f \<squnion> n (\<nu> ?f) * L
mu_nu_apx_meet ?f \<equiv> has_apx_meet (\<mu> ?f) (\<nu> ?f) \<and> \<mu> ?f \<triangle> \<nu> ?f = \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L
mu_nu_apx_nu ?f \<Longrightarrow> mu_nu_apx_meet ?f
nu_below_mu_nu_L ?f \<Longrightarrow> \<mu> ?f \<squnion> n (\<nu> ?f) * L = \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f; nu_below_mu_nu_2 ?f\<rbrakk> \<Longrightarrow> mu_nu_apx_nu ?f
nu_below_mu_nu_L ?f \<Longrightarrow> nu_below_mu_nu ?f
nu_below_mu_nu ?f \<Longrightarrow> nu_below_mu_nu_2 ?f

goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; nu_below_mu_nu_L f\<rbrakk> \<Longrightarrow> mu_nu_apx_meet_L f
[PROOF STEP]
by auto


[STATEMENT]
lemma mu_nu_apx_nu_L_nu_below_mu_nu_L:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "mu_nu_apx_nu_L f"
    shows "nu_below_mu_nu_L f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
let ?n = "\<mu> f \<squnion> n(\<nu> f) * L"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
let ?l = "\<mu> f \<squnion> (\<nu> f \<sqinter> L)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
have "C (\<nu> f) \<le> ?n \<squnion> n(?n) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (\<nu> f) \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> n (\<nu> f) * L) * top
[PROOF STEP]
using assms(3) apx_def mu_nu_apx_nu_L_def
[PROOF STATE]
proof (prove)
using this:
mu_nu_apx_nu_L f
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)
mu_nu_apx_nu_L ?f \<equiv> \<mu> ?f \<squnion> n (\<nu> ?f) * L \<sqsubseteq> \<nu> ?f

goal (1 subgoal):
 1. C (\<nu> f) \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> n (\<nu> f) * L) * top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C (\<nu> f) \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> n (\<nu> f) * L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (\<nu> f) \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> n (\<nu> f) * L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
have "... \<le> ?n \<squnion> n(?l) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> n (\<nu> f) * L) * top \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
using mult_left_isotone n_L_decreasing_meet_L n_isotone semiring.add_left_mono
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
n ?x * L \<le> ?x \<sqinter> L
?x \<le> ?y \<Longrightarrow> n ?x \<le> n ?y
?a \<le> ?b \<Longrightarrow> ?c \<squnion> ?a \<le> ?c \<squnion> ?b

goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> n (\<nu> f) * L) * top \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> n (\<nu> f) * L) * top \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> n (\<nu> f) * L) * top \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top

goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
have "... \<le> ?n \<squnion> n(\<nu> f) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<nu> f) * top
[PROOF STEP]
using assms(1,2) l_below_nu mult_left_isotone n_isotone sup_right_isotone
[PROOF STATE]
proof (prove)
using this:
has_least_fixpoint f
has_greatest_fixpoint f
\<lbrakk>has_least_fixpoint ?f; has_greatest_fixpoint ?f\<rbrakk> \<Longrightarrow> \<mu> ?f \<squnion> \<nu> ?f \<sqinter> L \<le> \<nu> ?f
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
?x \<le> ?y \<Longrightarrow> n ?x \<le> n ?y
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y

goal (1 subgoal):
 1. \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<nu> f) * top
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<mu> f \<squnion> \<nu> f \<sqinter> L) * top \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<nu> f) * top

goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
C (\<nu> f) \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<nu> f) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C (\<nu> f) \<le> \<mu> f \<squnion> n (\<nu> f) * L \<squnion> n (\<nu> f) * top

goal (1 subgoal):
 1. nu_below_mu_nu_L f
[PROOF STEP]
by (metis sup_assoc sup_right_top mult_left_dist_sup nu_below_mu_nu_L_def)
[PROOF STATE]
proof (state)
this:
nu_below_mu_nu_L f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kappa_mu_nu_L_mu_nu_apx_nu_L:
  "has_greatest_fixpoint f \<Longrightarrow> kappa_mu_nu_L f \<Longrightarrow> mu_nu_apx_nu_L f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_greatest_fixpoint f; kappa_mu_nu_L f\<rbrakk> \<Longrightarrow> mu_nu_apx_nu_L f
[PROOF STEP]
using kappa_mu_nu_L_def kappa_apx_below_nu mu_nu_apx_nu_L_def
[PROOF STATE]
proof (prove)
using this:
kappa_mu_nu_L ?f \<equiv> order.has_least_fixpoint (\<sqsubseteq>) ?f \<and> \<kappa> ?f = \<mu> ?f \<squnion> n (\<nu> ?f) * L
\<lbrakk>has_greatest_fixpoint ?f; order.has_least_fixpoint (\<sqsubseteq>) ?f\<rbrakk> \<Longrightarrow> \<kappa> ?f \<sqsubseteq> \<nu> ?f
mu_nu_apx_nu_L ?f \<equiv> \<mu> ?f \<squnion> n (\<nu> ?f) * L \<sqsubseteq> \<nu> ?f

goal (1 subgoal):
 1. \<lbrakk>has_greatest_fixpoint f; kappa_mu_nu_L f\<rbrakk> \<Longrightarrow> mu_nu_apx_nu_L f
[PROOF STEP]
by fastforce


[STATEMENT]
lemma mu_nu_apx_meet_L_mu_nu_apx_nu_L:
  "mu_nu_apx_meet_L f \<Longrightarrow> mu_nu_apx_nu_L f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mu_nu_apx_meet_L f \<Longrightarrow> mu_nu_apx_nu_L f
[PROOF STEP]
using apx_meet_char is_apx_meet_def mu_nu_apx_meet_L_def mu_nu_apx_nu_L_def
[PROOF STATE]
proof (prove)
using this:
is_apx_meet ?x ?y ?z = (has_apx_meet ?x ?y \<and> ?z = ?x \<triangle> ?y)
is_apx_meet ?x ?y ?z \<equiv> ?z \<sqsubseteq> ?x \<and> ?z \<sqsubseteq> ?y \<and> (\<forall>w. w \<sqsubseteq> ?x \<and> w \<sqsubseteq> ?y \<longrightarrow> w \<sqsubseteq> ?z)
mu_nu_apx_meet_L ?f \<equiv> has_apx_meet (\<mu> ?f) (\<nu> ?f) \<and> \<mu> ?f \<triangle> \<nu> ?f = \<mu> ?f \<squnion> n (\<nu> ?f) * L
mu_nu_apx_nu_L ?f \<equiv> \<mu> ?f \<squnion> n (\<nu> ?f) * L \<sqsubseteq> \<nu> ?f

goal (1 subgoal):
 1. mu_nu_apx_meet_L f \<Longrightarrow> mu_nu_apx_nu_L f
[PROOF STEP]
by fastforce


[STATEMENT]
lemma kappa_mu_nu_L_nu_below_mu_nu_L:
  "has_least_fixpoint f \<Longrightarrow> has_greatest_fixpoint f \<Longrightarrow> kappa_mu_nu_L f \<Longrightarrow> nu_below_mu_nu_L f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_least_fixpoint f; has_greatest_fixpoint f; kappa_mu_nu_L f\<rbrakk> \<Longrightarrow> nu_below_mu_nu_L f
[PROOF STEP]
by (simp add: kappa_mu_nu_L_mu_nu_apx_nu_L mu_nu_apx_nu_L_nu_below_mu_nu_L)


[STATEMENT]
lemma unfold_fold_2:
  assumes "isotone f"
      and "apx.isotone f"
      and "has_least_prefixpoint f"
      and "has_greatest_fixpoint f"
      and "apx.has_least_fixpoint f"
      and "f(x) \<le> x"
      and "\<kappa> f \<sqinter> L \<le> x \<sqinter> L"
    shows "\<kappa> f \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> f \<le> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<kappa> f \<le> x
[PROOF STEP]
have "\<kappa> f \<sqinter> L = \<nu> f \<sqinter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> f \<sqinter> L = \<nu> f \<sqinter> L
[PROOF STEP]
by (smt (z3) apx_meet_L assms(4,5) order.eq_iff inf.cobounded1 kappa_apx_below_nu kappa_below_nu le_inf_iff)
[PROOF STATE]
proof (state)
this:
\<kappa> f \<sqinter> L = \<nu> f \<sqinter> L

goal (1 subgoal):
 1. \<kappa> f \<le> x
[PROOF STEP]
hence "\<kappa> f = (\<kappa> f \<sqinter> L) \<squnion> \<mu> f"
[PROOF STATE]
proof (prove)
using this:
\<kappa> f \<sqinter> L = \<nu> f \<sqinter> L

goal (1 subgoal):
 1. \<kappa> f = \<kappa> f \<sqinter> L \<squnion> \<mu> f
[PROOF STEP]
by (metis assms(1-5) apx_meet_below_nu_kappa_mu_nu has_apx_least_fixpoint_kappa_apx_meet sup_commute least_fixpoint_char least_prefixpoint_fixpoint kappa_apx_meet_apx_meet_below_nu kappa_mu_nu_def)
[PROOF STATE]
proof (state)
this:
\<kappa> f = \<kappa> f \<sqinter> L \<squnion> \<mu> f

goal (1 subgoal):
 1. \<kappa> f \<le> x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<kappa> f = \<kappa> f \<sqinter> L \<squnion> \<mu> f

goal (1 subgoal):
 1. \<kappa> f \<le> x
[PROOF STEP]
by (metis assms(1,3,6,7) sup_least is_least_prefixpoint_def least_prefixpoint le_inf_iff pmu_mu)
[PROOF STATE]
proof (state)
this:
\<kappa> f \<le> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apx_transitive_2:
  assumes "x \<sqsubseteq> y"
      and "y \<sqsubseteq> z"
    shows "x \<sqsubseteq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
have "z \<le> y \<squnion> n(y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<le> y \<squnion> n y * top
[PROOF STEP]
using assms(2) apx_def
[PROOF STATE]
proof (prove)
using this:
y \<sqsubseteq> z
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> ?y \<le> ?x \<squnion> n ?x * top)

goal (1 subgoal):
 1. z \<le> y \<squnion> n y * top
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<le> y \<squnion> n y * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z \<le> y \<squnion> n y * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
have "... \<le> x \<squnion> n(x) * top \<squnion> n(y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<squnion> n y * top \<le> x \<squnion> n x * top \<squnion> n y * top
[PROOF STEP]
using assms(1) apx_def sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
x \<sqsubseteq> y
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> ?y \<le> ?x \<squnion> n ?x * top)
?x \<le> ?y \<Longrightarrow> ?x \<squnion> ?z \<le> ?y \<squnion> ?z

goal (1 subgoal):
 1. y \<squnion> n y * top \<le> x \<squnion> n x * top \<squnion> n y * top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<squnion> n y * top \<le> x \<squnion> n x * top \<squnion> n y * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y \<squnion> n y * top \<le> x \<squnion> n x * top \<squnion> n y * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
have "... \<le> x \<squnion> n(x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> n x * top \<squnion> n y * top \<le> x \<squnion> n x * top
[PROOF STEP]
by (metis assms(1) sup_assoc sup_idem sup_right_isotone apx_def mult_left_isotone n_add_n_top n_isotone)
[PROOF STATE]
proof (state)
this:
x \<squnion> n x * top \<squnion> n y * top \<le> x \<squnion> n x * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
z \<le> x \<squnion> n x * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<le> x \<squnion> n x * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
by (smt assms sup_assoc sup_commute apx_def le_iff_sup)
[PROOF STATE]
proof (state)
this:
x \<sqsubseteq> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apx_meet_L:
  assumes "y \<sqsubseteq> x"
    shows "x \<sqinter> L \<le> y \<sqinter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
have "x \<sqinter> L \<le> (y \<sqinter> L) \<squnion> (n(y) * top \<sqinter> L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L \<squnion> n y * top \<sqinter> L
[PROOF STEP]
by (metis assms apx_def inf.sup_left_isotone inf_sup_distrib2)
[PROOF STATE]
proof (state)
this:
x \<sqinter> L \<le> y \<sqinter> L \<squnion> n y * top \<sqinter> L

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> L \<le> y \<sqinter> L \<squnion> n y * top \<sqinter> L

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
have "... \<le> (y \<sqinter> L) \<squnion> n(y \<sqinter> L) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sqinter> L \<squnion> n y * top \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top
[PROOF STEP]
using n_n_meet_L sup_right_isotone
[PROOF STATE]
proof (prove)
using this:
n ?x = n (?x \<sqinter> L)
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y

goal (1 subgoal):
 1. y \<sqinter> L \<squnion> n y * top \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y \<sqinter> L \<squnion> n y * top \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<sqinter> L \<le> y \<sqinter> L \<squnion> n (y \<sqinter> L) * top

goal (1 subgoal):
 1. x \<sqinter> L \<le> y \<sqinter> L
[PROOF STEP]
by (metis le_iff_sup inf_le2 n_less_eq_char)
[PROOF STATE]
proof (state)
this:
x \<sqinter> L \<le> y \<sqinter> L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sup_apx_left_isotone_2:
  assumes "x \<sqsubseteq> y"
    shows "x \<squnion> z \<sqsubseteq> y \<squnion> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
have 1: "x \<squnion> z \<le> y \<squnion> z \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> z \<le> y \<squnion> z \<squnion> L
[PROOF STEP]
by (smt assms sup_assoc sup_commute sup_left_isotone apx_def)
[PROOF STATE]
proof (state)
this:
x \<squnion> z \<le> y \<squnion> z \<squnion> L

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
have "y \<squnion> z \<le> x \<squnion> n(x) * top \<squnion> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<squnion> z \<le> x \<squnion> n x * top \<squnion> z
[PROOF STEP]
using assms apx_def sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
x \<sqsubseteq> y
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> ?y \<le> ?x \<squnion> n ?x * top)
?x \<le> ?y \<Longrightarrow> ?x \<squnion> ?z \<le> ?y \<squnion> ?z

goal (1 subgoal):
 1. y \<squnion> z \<le> x \<squnion> n x * top \<squnion> z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<squnion> z \<le> x \<squnion> n x * top \<squnion> z

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y \<squnion> z \<le> x \<squnion> n x * top \<squnion> z

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
have "... \<le> x \<squnion> z \<squnion> n(x \<squnion> z) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> n x * top \<squnion> z \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top
[PROOF STEP]
by (metis sup_assoc sup_commute sup_right_isotone mult_left_isotone n_right_upper_bound)
[PROOF STATE]
proof (state)
this:
x \<squnion> n x * top \<squnion> z \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y \<squnion> z \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<squnion> z \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
using 1 apx_def
[PROOF STATE]
proof (prove)
using this:
y \<squnion> z \<le> x \<squnion> z \<squnion> n (x \<squnion> z) * top
x \<squnion> z \<le> y \<squnion> z \<squnion> L
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> ?y \<le> ?x \<squnion> n ?x * top)

goal (1 subgoal):
 1. x \<squnion> z \<sqsubseteq> y \<squnion> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<squnion> z \<sqsubseteq> y \<squnion> z

goal:
No subgoals!
[PROOF STEP]
qed