[STATEMENT]
lemma n_Omega_circ_simulate_right_sup:
  assumes "z * x \<le> y * y\<^sup>\<Omega> * z \<squnion> w"
    shows "z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
have "z * x \<le> y * y\<^sup>\<Omega> * z \<squnion> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * x \<le> y * y\<^sup>\<Omega> * z \<squnion> w
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
z * x \<le> y * y\<^sup>\<Omega> * z \<squnion> w

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

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
have "... = y * n(y\<^sup>\<omega>) * L \<squnion> y * y\<^sup>\<star> * z \<squnion> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * y\<^sup>\<Omega> * z \<squnion> w = y * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w
[PROOF STEP]
using L_left_zero Omega_def mult_right_dist_sup semiring.distrib_left mult_assoc
[PROOF STATE]
proof (prove)
using this:
L * ?x = L
?x\<^sup>\<Omega> = n (?x\<^sup>\<omega>) * L \<squnion> ?x\<^sup>\<star>
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z
?a * (?b \<squnion> ?c) = ?a * ?b \<squnion> ?a * ?c
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. y * y\<^sup>\<Omega> * z \<squnion> w = y * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y * y\<^sup>\<Omega> * z \<squnion> w = y * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
z * x \<le> y * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w
[PROOF STEP]
have 1: "z * x \<le> n(y\<^sup>\<omega>) * L \<squnion> y * y\<^sup>\<star> * z \<squnion> w"
[PROOF STATE]
proof (prove)
using this:
z * x \<le> y * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w

goal (1 subgoal):
 1. z * x \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w
[PROOF STEP]
by (metis sup_assoc sup_commute sup_bot_left mult_assoc mult_left_dist_sup n_L_split omega_unfold)
[PROOF STATE]
proof (state)
this:
z * x \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
hence "(n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>) * x \<le> n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * (n(y\<^sup>\<omega>) * L \<squnion> y * y\<^sup>\<star> * z \<squnion> w) \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
z * x \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w

goal (1 subgoal):
 1. (n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>) * x \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * (n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w) \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>
[PROOF STEP]
by (smt L_left_zero sup_assoc sup_ge1 sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup star.circ_back_loop_fixpoint)
[PROOF STATE]
proof (state)
this:
(n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>) * x \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * (n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w) \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>) * x \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * (n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w) \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
have "... = n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * (n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w) \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>
[PROOF STEP]
using semiring.distrib_left sup_assoc mult_assoc
[PROOF STATE]
proof (prove)
using this:
?a * (?b \<squnion> ?c) = ?a * ?b \<squnion> ?a * ?c
?x \<squnion> ?y \<squnion> ?z = ?x \<squnion> (?y \<squnion> ?z)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * (n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w) \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * (n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w) \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * (n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w) \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
have "... = n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>
[PROOF STEP]
by (smt (verit, ccfv_SIG) le_supI1 order.refl semiring.add_mono star.circ_back_loop_prefixpoint sup.bounded_iff sup.coboundedI1 sup.mono sup_left_divisibility sup_right_divisibility sup_same_context)
[PROOF STATE]
proof (state)
this:
n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
have "... = n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>
[PROOF STEP]
by (smt sup_assoc sup_commute sup_idem mult_assoc mult_left_dist_sup n_L_split star_mult_omega)
[PROOF STATE]
proof (state)
this:
n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
have "... \<le> n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>
[PROOF STEP]
by (meson mult_left_isotone order_refl semiring.add_left_mono star.circ_mult_upper_bound star.right_plus_below_circ sup_left_isotone)
[PROOF STATE]
proof (state)
this:
n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * y * y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star> \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>) * x \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>
[PROOF STEP]
have 2: "z * x\<^sup>\<star> \<le> n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
(n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>) * x \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<star> \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>
[PROOF STEP]
by (smt le_supI1 le_sup_iff sup_ge1 star.circ_loop_fixpoint star_right_induct)
[PROOF STATE]
proof (state)
this:
z * x\<^sup>\<star> \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
have "z * x * x\<^sup>\<omega> \<le> n(y\<^sup>\<omega>) * L \<squnion> y * y\<^sup>\<star> * z * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * x * x\<^sup>\<omega> \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<omega>
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
z * x \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z \<squnion> w

goal (1 subgoal):
 1. z * x * x\<^sup>\<omega> \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<omega>
[PROOF STEP]
by (smt (verit, del_insts) L_left_zero mult_assoc mult_left_isotone mult_right_dist_sup)
[PROOF STATE]
proof (state)
this:
z * x * x\<^sup>\<omega> \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<omega>

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
hence "n(z * x * x\<^sup>\<omega>) \<le> n(y * y\<^sup>\<star> * z * x\<^sup>\<omega> \<squnion> n(y\<^sup>\<omega>) * L \<squnion> w * x\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
using this:
z * x * x\<^sup>\<omega> \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>+ * z * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<omega>

goal (1 subgoal):
 1. n (z * x * x\<^sup>\<omega>) \<le> n (y\<^sup>+ * z * x\<^sup>\<omega> \<squnion> n (y\<^sup>\<omega>) * L \<squnion> w * x\<^sup>\<omega>)
[PROOF STEP]
by (simp add: n_isotone sup_commute)
[PROOF STATE]
proof (state)
this:
n (z * x * x\<^sup>\<omega>) \<le> n (y\<^sup>+ * z * x\<^sup>\<omega> \<squnion> n (y\<^sup>\<omega>) * L \<squnion> w * x\<^sup>\<omega>)

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
hence "n(z * x\<^sup>\<omega>) \<le> n(y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
using this:
n (z * x * x\<^sup>\<omega>) \<le> n (y\<^sup>+ * z * x\<^sup>\<omega> \<squnion> n (y\<^sup>\<omega>) * L \<squnion> w * x\<^sup>\<omega>)

goal (1 subgoal):
 1. n (z * x\<^sup>\<omega>) \<le> n (y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega>)
[PROOF STEP]
by (smt (verit, del_insts) sup_assoc sup_commute left_plus_omega le_iff_sup mult_assoc mult_left_dist_sup n_L_decreasing n_omega_induct omega_unfold star.left_plus_circ star_mult_omega)
[PROOF STATE]
proof (state)
this:
n (z * x\<^sup>\<omega>) \<le> n (y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * w * x\<^sup>\<omega>)

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

goal (1 subgoal):
 1. n (z * x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L
[PROOF STEP]
by (metis n_dist_sup n_galois n_mult n_n_L)
[PROOF STATE]
proof (state)
this:
n (z * x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
hence "z * n(x\<^sup>\<omega>) * L \<le> z * bot \<squnion> n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L"
[PROOF STATE]
proof (prove)
using this:
n (z * x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L

goal (1 subgoal):
 1. z * n (x\<^sup>\<omega>) * L \<le> z * bot \<squnion> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L
[PROOF STEP]
using n_L_split semiring.add_left_mono sup_assoc
[PROOF STATE]
proof (prove)
using this:
n (z * x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L
?x * n ?y * L = ?x * bot \<squnion> n (?x * ?y) * 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 * n (x\<^sup>\<omega>) * L \<le> z * bot \<squnion> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z * n (x\<^sup>\<omega>) * L \<le> z * bot \<squnion> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z * n (x\<^sup>\<omega>) * L \<le> z * bot \<squnion> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
have "... \<le> n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * bot \<squnion> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L
[PROOF STEP]
by (smt (z3) order.trans mult_1_left mult_right_sub_dist_sup_left semiring.add_right_mono star_left_unfold_equal sup_commute zero_right_mult_decreasing)
[PROOF STATE]
proof (state)
this:
z * bot \<squnion> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
z * n (x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L
[PROOF STEP]
have "z * n(x\<^sup>\<omega>) * L \<le> n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n(x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
z * n (x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L

goal (1 subgoal):
 1. z * n (x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * w * x\<^sup>\<star>
[PROOF STEP]
using le_supI1
[PROOF STATE]
proof (prove)
using this:
z * n (x\<^sup>\<omega>) * L \<le> n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> * z \<squnion> y\<^sup>\<star> * w * n (x\<^sup>\<omega>) * L
?x \<le> ?a \<Longrightarrow> ?x \<le> ?a \<squnion> ?b

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

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

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

goal (1 subgoal):
 1. z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)
[PROOF STEP]
by (smt L_left_zero Omega_def sup_assoc le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup)
[PROOF STATE]
proof (state)
this:
z * x\<^sup>\<Omega> \<le> y\<^sup>\<Omega> * (z \<squnion> w * x\<^sup>\<Omega>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma n_Omega_circ_simulate_left_sup:
  assumes "x * z \<le> z * y\<^sup>\<Omega> \<squnion> w"
    shows "x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
have "x * (z * n(y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n(x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n(y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) = x * z * n(y\<^sup>\<omega>) * L \<squnion> x * z * y\<^sup>\<star> \<squnion> n(x\<^sup>\<omega>) * L \<squnion> x * x\<^sup>\<star> * w * n(y\<^sup>\<omega>) * L \<squnion> x * x\<^sup>\<star> * w * y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) = x * z * n (y\<^sup>\<omega>) * L \<squnion> x * z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * y\<^sup>\<star>
[PROOF STEP]
by (smt sup_assoc sup_commute mult_assoc mult_left_dist_sup n_L_split omega_unfold)
[PROOF STATE]
proof (state)
this:
x * (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) = x * z * n (y\<^sup>\<omega>) * L \<squnion> x * z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) = x * z * n (y\<^sup>\<omega>) * L \<squnion> x * z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
have "... \<le> (z * n(y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * n(y\<^sup>\<omega>) * L \<squnion> (z * n(y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<star> \<squnion> n(x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n(y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z * n (y\<^sup>\<omega>) * L \<squnion> x * z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * y\<^sup>\<star> \<le> (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * n (y\<^sup>\<omega>) * L \<squnion> (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>
[PROOF STEP]
by (smt assms Omega_def sup_assoc sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup star.circ_loop_fixpoint)
[PROOF STATE]
proof (state)
this:
x * z * n (y\<^sup>\<omega>) * L \<squnion> x * z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * y\<^sup>\<star> \<le> (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * n (y\<^sup>\<omega>) * L \<squnion> (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * z * n (y\<^sup>\<omega>) * L \<squnion> x * z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>+ * w * y\<^sup>\<star> \<le> (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * n (y\<^sup>\<omega>) * L \<squnion> (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
have "... = z * n(y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> * n(y\<^sup>\<omega>) * L \<squnion> w * n(y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n(x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n(y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * n (y\<^sup>\<omega>) * L \<squnion> (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star> = z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> w * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>
[PROOF STEP]
by (smt L_left_zero sup_assoc sup_commute sup_idem mult_assoc mult_right_dist_sup star.circ_transitive_equal)
[PROOF STATE]
proof (state)
this:
(z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * n (y\<^sup>\<omega>) * L \<squnion> (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star> = z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> w * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * n (y\<^sup>\<omega>) * L \<squnion> (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star> = z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> w * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
have "... = z * n(y\<^sup>\<omega>) * L \<squnion> w * n(y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n(x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n(y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> w * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star> = z * n (y\<^sup>\<omega>) * L \<squnion> w * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>
[PROOF STEP]
by (smt sup_assoc sup_commute sup_idem le_iff_sup mult_assoc n_L_split star_mult_omega zero_right_mult_decreasing)
[PROOF STATE]
proof (state)
this:
z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> * n (y\<^sup>\<omega>) * L \<squnion> w * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star> = z * n (y\<^sup>\<omega>) * L \<squnion> w * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>

goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) \<le> z * n (y\<^sup>\<omega>) * L \<squnion> w * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>
[PROOF STEP]
have "x * (z * n(y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n(x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n(y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) \<le> z * n(y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n(x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n(y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
x * (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) \<le> z * n (y\<^sup>\<omega>) * L \<squnion> w * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>

goal (1 subgoal):
 1. x * (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) \<le> z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>
[PROOF STEP]
by (smt sup_assoc sup_commute sup_idem mult_assoc star.circ_loop_fixpoint)
[PROOF STATE]
proof (state)
this:
x * (z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>) \<le> z * n (y\<^sup>\<omega>) * L \<squnion> z * y\<^sup>\<star> \<squnion> n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * n (y\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>

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

goal (1 subgoal):
 1. x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>
[PROOF STEP]
by (smt (verit, del_insts) L_left_zero Omega_def sup_assoc le_supI1 le_sup_iff sup_ge1 mult_assoc mult_left_dist_sup mult_right_dist_sup star.circ_back_loop_fixpoint star_left_induct)
[PROOF STATE]
proof (state)
this:
x\<^sup>\<Omega> * z \<le> (z \<squnion> x\<^sup>\<Omega> * w) * y\<^sup>\<Omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma circ_sup_8:
  "n((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<le> (x\<^sup>\<star> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<le> (x\<^sup>\<star> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
by (metis sup_ge1 nL_omega.circ_sup_4 Omega_def mult_left_isotone n_isotone omega_sum_unfold_3 order_trans)


[STATEMENT]
lemma n_split_omega_omega:
  "x\<^sup>\<omega> \<le> x\<^sup>\<omega> * bot \<squnion> n(x\<^sup>\<omega>) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<omega> \<le> x\<^sup>\<omega> * bot \<squnion> n (x\<^sup>\<omega>) * top
[PROOF STEP]
by (metis n_split n_top_L omega_vector)


[STATEMENT]
lemma n_below_n_star:
  "n(x) \<le> n(x\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x \<le> n (x\<^sup>\<star>)
[PROOF STEP]
by (simp add: n_isotone star.circ_increasing)


[STATEMENT]
lemma n_star_below_n_omega:
  "n(x\<^sup>\<star>) \<le> n(x\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x\<^sup>\<star>) \<le> n (x\<^sup>\<omega>)
[PROOF STEP]
by (metis n_mult_left_upper_bound star_mult_omega)


[STATEMENT]
lemma n_below_n_omega:
  "n(x) \<le> n(x\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x \<le> n (x\<^sup>\<omega>)
[PROOF STEP]
using order.trans n_below_n_star n_star_below_n_omega
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c
n ?x \<le> n (?x\<^sup>\<star>)
n (?x\<^sup>\<star>) \<le> n (?x\<^sup>\<omega>)

goal (1 subgoal):
 1. n x \<le> n (x\<^sup>\<omega>)
[PROOF STEP]
by blast


[STATEMENT]
lemma star_n_L:
  "x\<^sup>\<star> * n(x) * L = x\<^sup>\<star> * bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> * n x * L = x\<^sup>\<star> * bot
[PROOF STEP]
by (metis sup_bot_left mult_left_zero n_L_split n_dist_sup n_mult_bot n_one ni_def ni_split star_left_unfold_equal star_plus)


[STATEMENT]
lemma star_L_split:
  assumes "y \<le> z"
      and "x * z * L \<le> x * bot \<squnion> z * L"
    shows "x\<^sup>\<star> * y * L \<le> x\<^sup>\<star> * bot \<squnion> z * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> * y * L \<le> x\<^sup>\<star> * bot \<squnion> z * L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sup>\<star> * y * L \<le> x\<^sup>\<star> * bot \<squnion> z * L
[PROOF STEP]
have "x * (x\<^sup>\<star> * bot \<squnion> z * L) \<le> x\<^sup>\<star> * bot \<squnion> x * z * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (x\<^sup>\<star> * bot \<squnion> z * L) \<le> x\<^sup>\<star> * bot \<squnion> x * z * L
[PROOF STEP]
by (metis sup_bot_right order.eq_iff mult_assoc mult_left_dist_sup star.circ_loop_fixpoint)
[PROOF STATE]
proof (state)
this:
x * (x\<^sup>\<star> * bot \<squnion> z * L) \<le> x\<^sup>\<star> * bot \<squnion> x * z * L

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

goal (1 subgoal):
 1. x\<^sup>\<star> * y * L \<le> x\<^sup>\<star> * bot \<squnion> z * L
[PROOF STEP]
have "... \<le> x\<^sup>\<star> * bot \<squnion> x * bot \<squnion> z * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> * bot \<squnion> x * z * L \<le> x\<^sup>\<star> * bot \<squnion> x * bot \<squnion> z * L
[PROOF STEP]
using assms(2) semiring.add_left_mono sup_assoc
[PROOF STATE]
proof (prove)
using this:
x * z * L \<le> x * bot \<squnion> z * 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. x\<^sup>\<star> * bot \<squnion> x * z * L \<le> x\<^sup>\<star> * bot \<squnion> x * bot \<squnion> z * L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x\<^sup>\<star> * bot \<squnion> x * z * L \<le> x\<^sup>\<star> * bot \<squnion> x * bot \<squnion> z * L

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

goal (1 subgoal):
 1. x\<^sup>\<star> * y * L \<le> x\<^sup>\<star> * bot \<squnion> z * L
[PROOF STEP]
have "... = x\<^sup>\<star> * bot \<squnion> z * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> * bot \<squnion> x * bot \<squnion> z * L = x\<^sup>\<star> * bot \<squnion> z * L
[PROOF STEP]
using mult_left_isotone star.circ_increasing sup.absorb_iff2 sup_commute
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
?x \<le> ?x\<^sup>\<star>
(?a \<le> ?b) = (?a \<squnion> ?b = ?b)
?x \<squnion> ?y = ?y \<squnion> ?x

goal (1 subgoal):
 1. x\<^sup>\<star> * bot \<squnion> x * bot \<squnion> z * L = x\<^sup>\<star> * bot \<squnion> z * L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x\<^sup>\<star> * bot \<squnion> x * bot \<squnion> z * L = x\<^sup>\<star> * bot \<squnion> z * L

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

goal (1 subgoal):
 1. y * L \<squnion> x * (x\<^sup>\<star> * bot \<squnion> z * L) \<le> x\<^sup>\<star> * bot \<squnion> z * L
[PROOF STEP]
by (metis assms(1) le_sup_iff sup_ge2 mult_left_isotone order_trans)
[PROOF STATE]
proof (state)
this:
y * L \<squnion> x * (x\<^sup>\<star> * bot \<squnion> z * L) \<le> x\<^sup>\<star> * bot \<squnion> z * L

goal (1 subgoal):
 1. x\<^sup>\<star> * y * L \<le> x\<^sup>\<star> * bot \<squnion> z * L
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y * L \<squnion> x * (x\<^sup>\<star> * bot \<squnion> z * L) \<le> x\<^sup>\<star> * bot \<squnion> z * L

goal (1 subgoal):
 1. x\<^sup>\<star> * y * L \<le> x\<^sup>\<star> * bot \<squnion> z * L
[PROOF STEP]
by (simp add: star_left_induct mult_assoc)
[PROOF STATE]
proof (state)
this:
x\<^sup>\<star> * y * L \<le> x\<^sup>\<star> * bot \<squnion> z * L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma star_L_split_same:
  "x * y * L \<le> x * bot \<squnion> y * L \<Longrightarrow> x\<^sup>\<star> * y * L = x\<^sup>\<star> * bot \<squnion> y * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y * L \<le> x * bot \<squnion> y * L \<Longrightarrow> x\<^sup>\<star> * y * L = x\<^sup>\<star> * bot \<squnion> y * L
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x * y * L \<le> x * bot \<squnion> y * L \<Longrightarrow> x\<^sup>\<star> * y * L \<le> x\<^sup>\<star> * bot \<squnion> y * L
 2. x * y * L \<le> x * bot \<squnion> y * L \<Longrightarrow> x\<^sup>\<star> * bot \<squnion> y * L \<le> x\<^sup>\<star> * y * L
[PROOF STEP]
apply (simp add: star_L_split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y * L \<le> x * bot \<squnion> y * L \<Longrightarrow> x\<^sup>\<star> * bot \<squnion> y * L \<le> x\<^sup>\<star> * y * L
[PROOF STEP]
by (metis bot_least le_supI mult_isotone nL_star.star_below_circ star.circ_loop_fixpoint sup.cobounded2 mult_assoc)


[STATEMENT]
lemma star_n_L_split_equal:
  "n(x * y) \<le> n(y) \<Longrightarrow> x\<^sup>\<star> * n(y) * L = x\<^sup>\<star> * bot \<squnion> n(y) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x * y) \<le> n y \<Longrightarrow> x\<^sup>\<star> * n y * L = x\<^sup>\<star> * bot \<squnion> n y * L
[PROOF STEP]
by (simp add: n_mult_right_upper_bound star_L_split_same)


[STATEMENT]
lemma n_star_mult:
  "n(x * y) \<le> n(y) \<Longrightarrow> n(x\<^sup>\<star> * y) = n(x\<^sup>\<star>) \<squnion> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x * y) \<le> n y \<Longrightarrow> n (x\<^sup>\<star> * y) = n (x\<^sup>\<star>) \<squnion> n y
[PROOF STEP]
by (metis n_dist_sup n_mult n_mult_bot n_n_L star_n_L_split_equal)


[STATEMENT]
lemma n_omega_mult:
  "n(x\<^sup>\<omega> * y) = n(x\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x\<^sup>\<omega> * y) = n (x\<^sup>\<omega>)
[PROOF STEP]
by (simp add: n_isotone n_mult_left_upper_bound omega_sub_vector order.eq_iff)


[STATEMENT]
lemma n_star_left_unfold:
  "n(x\<^sup>\<star>) = n(x * x\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x\<^sup>\<star>) = n (x\<^sup>+)
[PROOF STEP]
by (metis n_mult n_mult_bot star.circ_plus_same star_n_L)


[STATEMENT]
lemma ni_star_below_ni_omega:
  "ni(x\<^sup>\<star>) \<le> ni(x\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x\<^sup>\<star>) \<le> ni (x\<^sup>\<omega>)
[PROOF STEP]
by (simp add: ni_n_order n_star_below_n_omega)


[STATEMENT]
lemma ni_below_ni_omega:
  "ni(x) \<le> ni(x\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni x \<le> ni (x\<^sup>\<omega>)
[PROOF STEP]
by (simp add: ni_n_order n_below_n_omega)


[STATEMENT]
lemma ni_star:
  "ni(x)\<^sup>\<star> = 1 \<squnion> ni(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni x\<^sup>\<star> = (1::'a) \<squnion> ni x
[PROOF STEP]
by (simp add: mult_L_star ni_def)


[STATEMENT]
lemma ni_omega:
  "ni(x)\<^sup>\<omega> = ni(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni x\<^sup>\<omega> = ni x
[PROOF STEP]
using mult_L_omega ni_def
[PROOF STATE]
proof (prove)
using this:
(?x * L)\<^sup>\<omega> = ?x * L
ni ?x = n ?x * L

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


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

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


[STATEMENT]
lemma star_ni:
  "x\<^sup>\<star> * ni(x) = x\<^sup>\<star> * bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> * ni x = x\<^sup>\<star> * bot
[PROOF STEP]
using ni_def mult_assoc star_n_L
[PROOF STATE]
proof (prove)
using this:
ni ?x = n ?x * L
?a * ?b * ?c = ?a * (?b * ?c)
?x\<^sup>\<star> * n ?x * L = ?x\<^sup>\<star> * bot

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


[STATEMENT]
lemma star_ni_split_equal:
  "ni(x * y) \<le> ni(y) \<Longrightarrow> x\<^sup>\<star> * ni(y) = x\<^sup>\<star> * bot \<squnion> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x * y) \<le> ni y \<Longrightarrow> x\<^sup>\<star> * ni y = x\<^sup>\<star> * bot \<squnion> ni y
[PROOF STEP]
using ni_def ni_mult_right_upper_bound mult_assoc star_L_split_same
[PROOF STATE]
proof (prove)
using this:
ni ?x = n ?x * L
(ni (?x * ?y) \<le> ni ?z) = (ni ?x \<le> ni ?z \<and> ?x * ni ?y \<le> ?x * bot \<squnion> ni ?z)
?a * ?b * ?c = ?a * (?b * ?c)
?x * ?y * L \<le> ?x * bot \<squnion> ?y * L \<Longrightarrow> ?x\<^sup>\<star> * ?y * L = ?x\<^sup>\<star> * bot \<squnion> ?y * L

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


[STATEMENT]
lemma ni_star_mult:
  "ni(x * y) \<le> ni(y) \<Longrightarrow> ni(x\<^sup>\<star> * y) = ni(x\<^sup>\<star>) \<squnion> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x * y) \<le> ni y \<Longrightarrow> ni (x\<^sup>\<star> * y) = ni (x\<^sup>\<star>) \<squnion> ni y
[PROOF STEP]
using mult_right_dist_sup ni_def ni_n_order n_star_mult
[PROOF STATE]
proof (prove)
using this:
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z
ni ?x = n ?x * L
(ni ?x \<le> ni ?y) = (n ?x \<le> n ?y)
n (?x * ?y) \<le> n ?y \<Longrightarrow> n (?x\<^sup>\<star> * ?y) = n (?x\<^sup>\<star>) \<squnion> n ?y

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


[STATEMENT]
lemma ni_omega_mult:
  "ni(x\<^sup>\<omega> * y) = ni(x\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x\<^sup>\<omega> * y) = ni (x\<^sup>\<omega>)
[PROOF STEP]
by (simp add: ni_def n_omega_mult)


[STATEMENT]
lemma ni_star_left_unfold:
  "ni(x\<^sup>\<star>) = ni(x * x\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x\<^sup>\<star>) = ni (x\<^sup>+)
[PROOF STEP]
by (simp add: ni_def n_star_left_unfold)


[STATEMENT]
lemma n_star_import:
  assumes "n(y) * x \<le> x * n(y)"
    shows "n(y) * x\<^sup>\<star> = n(y) * (n(y) * x)\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y * x\<^sup>\<star> = n y * (n y * x)\<^sup>\<star>
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n y * x\<^sup>\<star> \<le> n y * (n y * x)\<^sup>\<star>
 2. n y * (n y * x)\<^sup>\<star> \<le> n y * x\<^sup>\<star>
[PROOF STEP]
have "n(y) * (n(y) * x)\<^sup>\<star> * x \<le> n(y) * (n(y) * x)\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y * (n y * x)\<^sup>\<star> * x \<le> n y * (n y * x)\<^sup>\<star>
[PROOF STEP]
by (smt assms mult_assoc mult_right_dist_sup mult_right_sub_dist_sup_left n_mult_idempotent n_preserves_equation star.circ_back_loop_fixpoint)
[PROOF STATE]
proof (state)
this:
n y * (n y * x)\<^sup>\<star> * x \<le> n y * (n y * x)\<^sup>\<star>

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

goal (1 subgoal):
 1. n y * x\<^sup>\<star> \<le> n y * (n y * x)\<^sup>\<star>
[PROOF STEP]
using assms eq_refl n_mult_idempotent n_sub_one star.circ_import
[PROOF STATE]
proof (prove)
using this:
n y * (n y * x)\<^sup>\<star> * x \<le> n y * (n y * x)\<^sup>\<star>
n y * x \<le> x * n y
?x = ?y \<Longrightarrow> ?x \<le> ?y
idempotent (n ?x)
coreflexive (n ?x)
\<lbrakk>dense_rel ?p; coreflexive ?p; ?p * ?x \<le> ?x * ?p\<rbrakk> \<Longrightarrow> ?p * ?x\<^sup>\<star> = ?p * (?p * ?x)\<^sup>\<star>

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

goal (1 subgoal):
 1. n y * (n y * x)\<^sup>\<star> \<le> n y * x\<^sup>\<star>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n y * (n y * x)\<^sup>\<star> \<le> n y * x\<^sup>\<star>
[PROOF STEP]
show "n(y) * (n(y) * x)\<^sup>\<star> \<le> n(y) * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y * (n y * x)\<^sup>\<star> \<le> n y * x\<^sup>\<star>
[PROOF STEP]
by (simp add: assms n_mult_idempotent n_sub_one star.circ_import)
[PROOF STATE]
proof (state)
this:
n y * (n y * x)\<^sup>\<star> \<le> n y * x\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma n_omega_export:
  "n(y) * x \<le> x * n(y) \<Longrightarrow> n(y) * x\<^sup>\<omega> = (n(y) * x)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y * x \<le> x * n y \<Longrightarrow> n y * x\<^sup>\<omega> = (n y * x)\<^sup>\<omega>
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n y * x \<le> x * n y \<Longrightarrow> n y * x\<^sup>\<omega> \<le> (n y * x)\<^sup>\<omega>
 2. n y * x \<le> x * n y \<Longrightarrow> (n y * x)\<^sup>\<omega> \<le> n y * x\<^sup>\<omega>
[PROOF STEP]
apply (simp add: n_preserves_equation omega_simulation)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y * x \<le> x * n y \<Longrightarrow> (n y * x)\<^sup>\<omega> \<le> n y * x\<^sup>\<omega>
[PROOF STEP]
by (metis mult_right_isotone mult_1_right n_sub_one omega_isotone omega_slide)


[STATEMENT]
lemma n_omega_import:
  "n(y) * x \<le> x * n(y) \<Longrightarrow> n(y) * x\<^sup>\<omega> = n(y) * (n(y) * x)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y * x \<le> x * n y \<Longrightarrow> n y * x\<^sup>\<omega> = n y * (n y * x)\<^sup>\<omega>
[PROOF STEP]
by (simp add: n_mult_idempotent omega_import)


[STATEMENT]
lemma star_n_omega_top:
  "x\<^sup>\<star> * n(x\<^sup>\<omega>) * top = x\<^sup>\<star> * bot \<squnion> n(x\<^sup>\<omega>) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> * n (x\<^sup>\<omega>) * top = x\<^sup>\<star> * bot \<squnion> n (x\<^sup>\<omega>) * top
[PROOF STEP]
by (smt (verit, del_insts) le_supI le_sup_iff sup_right_divisibility order.antisym mult_assoc nL_star.circ_mult_omega nL_star.star_zero_below_circ_mult n_top_split star.circ_loop_fixpoint)


[STATEMENT]
lemma find_first_distinct_ofsm_table_gt_code[code] :
  "find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
proof (cases "q1 \<in> states M \<and> q2 \<in> states M \<and> ((ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
 2. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2) \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2)

goal (2 subgoals):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
 2. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2) \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
have "find_first_distinct_ofsm_table_gt M q1 q2 k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 k = 0
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2)

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 k = 0
[PROOF STEP]
by (metis find_first_distinct_ofsm_table_gt.simps)
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt M q1 q2 k = 0

goal (2 subgoals):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
 2. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2) \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt M q1 q2 k = 0

goal (2 subgoals):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
 2. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2) \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
have "find_first_distinct_ofsm_table_gt' M q1 q2 k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
proof (cases "q1 \<in> states M \<and> q2 \<in> states M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
 2. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M) \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M

goal (2 subgoals):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
 2. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M) \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M
[PROOF STEP]
have "q1 \<in> FSM.states M" and "q2 \<in> FSM.states M"
          and "ofsm_table_fix M (\<lambda>q . states M) 0 q1 = ofsm_table_fix M (\<lambda>q . states M) 0 q2"
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M

goal (1 subgoal):
 1. q1 \<in> FSM.states M &&& q2 \<in> FSM.states M &&& ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 = ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M
\<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2)

goal (1 subgoal):
 1. q1 \<in> FSM.states M &&& q2 \<in> FSM.states M &&& ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 = ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 = ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (2 subgoals):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
 2. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M) \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 = ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
have "q2 \<in> ofsm_table_fix M (\<lambda>q . states M) 0 q1"
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 = ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. q2 \<in> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1
[PROOF STEP]
using ofsm_table_fix_eq_if_elem[of q1 M q2]
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 = ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
\<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; equivalence_relation_on_states M ?f\<rbrakk> \<Longrightarrow> (ofsm_table_fix M ?f 0 q1 = ofsm_table_fix M ?f 0 q2) = (q2 \<in> ofsm_table_fix M ?f 0 q1)

goal (1 subgoal):
 1. q2 \<in> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1
[PROOF STEP]
using minimise_initial_partition
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 = ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
\<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; equivalence_relation_on_states M ?f\<rbrakk> \<Longrightarrow> (ofsm_table_fix M ?f 0 q1 = ofsm_table_fix M ?f 0 q2) = (q2 \<in> ofsm_table_fix M ?f 0 q1)
equivalence_relation_on_states ?M (\<lambda>q. FSM.states ?M)

goal (1 subgoal):
 1. q2 \<in> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q2 \<in> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1

goal (2 subgoals):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
 2. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M) \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q2 \<in> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q2 \<in> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
by (metis find_first_distinct_ofsm_table_gt'.simps)
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt' M q1 q2 k = 0

goal (1 subgoal):
 1. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M) \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M) \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M)

goal (1 subgoal):
 1. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M) \<Longrightarrow> find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M)

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
by (meson find_first_distinct_ofsm_table_gt'.simps)
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt' M q1 q2 k = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt' M q1 q2 k = 0

goal (2 subgoals):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
 2. \<not> (q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2) \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
find_first_distinct_ofsm_table_gt M q1 q2 k = 0
find_first_distinct_ofsm_table_gt' M q1 q2 k = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
find_first_distinct_ofsm_table_gt M q1 q2 k = 0
find_first_distinct_ofsm_table_gt' M q1 q2 k = 0

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k

goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
have "q1 \<in> FSM.states M" and "q2 \<in> FSM.states M"
        and "ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2"
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. q1 \<in> FSM.states M &&& q2 \<in> FSM.states M &&& ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
have "q2 \<notin> ofsm_table_fix M (\<lambda>q . states M) 0 q1"
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. q2 \<notin> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1
[PROOF STEP]
using ofsm_table_fix_eq_if_elem[of q1 M q2]
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
\<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; equivalence_relation_on_states M ?f\<rbrakk> \<Longrightarrow> (ofsm_table_fix M ?f 0 q1 = ofsm_table_fix M ?f 0 q2) = (q2 \<in> ofsm_table_fix M ?f 0 q1)

goal (1 subgoal):
 1. q2 \<notin> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1
[PROOF STEP]
using minimise_initial_partition
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
\<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; equivalence_relation_on_states M ?f\<rbrakk> \<Longrightarrow> (ofsm_table_fix M ?f 0 q1 = ofsm_table_fix M ?f 0 q2) = (q2 \<in> ofsm_table_fix M ?f 0 q1)
equivalence_relation_on_states ?M (\<lambda>q. FSM.states ?M)

goal (1 subgoal):
 1. q2 \<notin> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q2 \<notin> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1

goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
obtain k' where "\<And> q . q \<in> states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q . states M) 0 q = ofsm_table M (\<lambda>q . states M) k' q" and "\<And> q k'' . q \<in> states M \<Longrightarrow> k'' \<ge> k' \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k'' q = ofsm_table M (\<lambda>q . states M) k' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) k' q; \<And>q k''. \<lbrakk>q \<in> FSM.states M; k' \<le> k''\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k'' q = ofsm_table M (\<lambda>q. FSM.states M) k' q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ofsm_table_fix_length[of M "(\<lambda>q . states M) "]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> FSM.states M \<subseteq> FSM.states M; \<And>k. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) k q; \<And>q k'. \<lbrakk>q \<in> FSM.states M; k \<le> k'\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q = ofsm_table M (\<lambda>q. FSM.states M) k q\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) k' q; \<And>q k''. \<lbrakk>q \<in> FSM.states M; k' \<le> k''\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k'' q = ofsm_table M (\<lambda>q. FSM.states M) k' q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?q \<in> FSM.states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q = ofsm_table M (\<lambda>q. FSM.states M) k' ?q
\<lbrakk>?q \<in> FSM.states M; k' \<le> ?k''\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) ?k'' ?q = ofsm_table M (\<lambda>q. FSM.states M) k' ?q

goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
have f1: "find_first_distinct_ofsm_table_gt M q1 q2 =
              (\<lambda>x. if ofsm_table M (\<lambda>q . states M) x q1 \<noteq> ofsm_table M (\<lambda>q . states M) x q2
                then x
                else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))
[PROOF STEP]
using find_first_distinct_ofsm_table_gt.simps[of M q1 q2]
[PROOF STATE]
proof (prove)
using this:
find_first_distinct_ofsm_table_gt M q1 q2 ?k = (if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 then if ofsm_table M (\<lambda>q. FSM.states M) ?k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) ?k q2 then ?k else find_first_distinct_ofsm_table_gt M q1 q2 (Suc ?k) else 0)

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
find_first_distinct_ofsm_table_gt M q1 q2 ?k = (if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 then if ofsm_table M (\<lambda>q. FSM.states M) ?k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) ?k q2 then ?k else find_first_distinct_ofsm_table_gt M q1 q2 (Suc ?k) else 0)
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))

goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
have f2: "find_first_distinct_ofsm_table_no_check M q1 q2 =
              (\<lambda>x. if ofsm_table M (\<lambda>q . states M) x q1 \<noteq> ofsm_table M (\<lambda>q . states M) x q2
                then x
                else find_first_distinct_ofsm_table_no_check M q1 q2 (Suc x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first_distinct_ofsm_table_no_check M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_no_check M q1 q2 (Suc x))
[PROOF STEP]
using True find_first_distinct_ofsm_table_no_check.simps[of M q1 q2]
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
find_first_distinct_ofsm_table_no_check M q1 q2 ?k = (if ofsm_table M (\<lambda>q. FSM.states M) ?k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) ?k q2 then ?k else find_first_distinct_ofsm_table_no_check M q1 q2 (Suc ?k))

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_no_check M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_no_check M q1 q2 (Suc x))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_no_check M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_no_check M q1 q2 (Suc x))

goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
have "(\<And>x. k' \<le> x \<Longrightarrow> ofsm_table M (\<lambda>q . states M) x q1 \<noteq> ofsm_table M (\<lambda>q . states M) x q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. k' \<le> x \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2
[PROOF STEP]
using \<open>\<And> q k'' . q \<in> states M \<Longrightarrow> k'' \<ge> k' \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k'' q = ofsm_table M (\<lambda>q . states M) k' q\<close> \<open>q1 \<in> FSM.states M\<close> \<open>q2 \<in> FSM.states M\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> FSM.states M; k' \<le> ?k''\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) ?k'' ?q = ofsm_table M (\<lambda>q. FSM.states M) k' ?q
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. \<And>x. k' \<le> x \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2
[PROOF STEP]
by (metis True \<open>\<And> q . q \<in> states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q . states M) 0 q = ofsm_table M (\<lambda>q . states M) k' q\<close>)
[PROOF STATE]
proof (state)
this:
k' \<le> ?x \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) ?x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) ?x q2

goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
have "find_first_distinct_ofsm_table_gt' M q1 q2 k = find_first_distinct_ofsm_table_no_check M q1 q2 k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt' M q1 q2 k = find_first_distinct_ofsm_table_no_check M q1 q2 k
[PROOF STEP]
using True \<open>q2 \<notin> ofsm_table_fix M (\<lambda>q . states M) 0 q1\<close> find_first_distinct_ofsm_table_gt'.simps[of M]
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
q2 \<notin> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1
find_first_distinct_ofsm_table_gt' M ?q1.0 ?q2.0 ?k = (if ?q1.0 \<in> FSM.states M \<and> ?q2.0 \<in> FSM.states M \<and> ?q2.0 \<notin> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q1.0 then find_first_distinct_ofsm_table_no_check M ?q1.0 ?q2.0 ?k else 0)

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt' M q1 q2 k = find_first_distinct_ofsm_table_no_check M q1 q2 k
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt' M q1 q2 k = find_first_distinct_ofsm_table_no_check M q1 q2 k

goal (1 subgoal):
 1. q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
find_first_distinct_ofsm_table_gt' M q1 q2 k = find_first_distinct_ofsm_table_no_check M q1 q2 k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
find_first_distinct_ofsm_table_gt' M q1 q2 k = find_first_distinct_ofsm_table_no_check M q1 q2 k

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
using recursion_renaming_helper[OF f1 f2 \<open>(\<And>x. k' \<le> x \<Longrightarrow> ofsm_table M (\<lambda>q . states M) x q1 \<noteq> ofsm_table M (\<lambda>q . states M) x q2)\<close>, of k']
[PROOF STATE]
proof (prove)
using this:
find_first_distinct_ofsm_table_gt' M q1 q2 k = find_first_distinct_ofsm_table_no_check M q1 q2 k
(\<And>x. k' \<le> x \<Longrightarrow> k' \<le> x) \<Longrightarrow> find_first_distinct_ofsm_table_gt M q1 q2 = find_first_distinct_ofsm_table_no_check M q1 q2

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt M q1 q2 k = find_first_distinct_ofsm_table_gt' M q1 q2 k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_first_distinct_ofsm_table_gt_is_first_gt :
  assumes "q1 \<in> FSM.states M"
      and "q2 \<in> FSM.states M"
      and "ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2"
shows "ofsm_table M (\<lambda>q . states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q . states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2"
  and "k \<le> k' \<Longrightarrow> k' < (find_first_distinct_ofsm_table_gt M q1 q2 k) \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k' q1 = ofsm_table M (\<lambda>q . states M) k' q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2 &&& (\<lbrakk>k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2
 2. \<lbrakk>k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2
[PROOF STEP]
have f: "find_first_distinct_ofsm_table_gt M q1 q2 =
              (\<lambda>x. if ofsm_table M (\<lambda>q . states M) x q1 \<noteq> ofsm_table M (\<lambda>q . states M) x q2
                then x
                else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))
[PROOF STEP]
using assms find_first_distinct_ofsm_table_gt.simps[of M]
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
find_first_distinct_ofsm_table_gt M ?q1.0 ?q2.0 ?k = (if ?q1.0 \<in> FSM.states M \<and> ?q2.0 \<in> FSM.states M \<and> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q1.0 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q2.0 then if ofsm_table M (\<lambda>q. FSM.states M) ?k ?q1.0 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) ?k ?q2.0 then ?k else find_first_distinct_ofsm_table_gt M ?q1.0 ?q2.0 (Suc ?k) else 0)

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt M q1 q2 = (\<lambda>x. if ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2 then x else find_first_distinct_ofsm_table_gt M q1 q2 (Suc x))

goal (2 subgoals):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2
 2. \<lbrakk>k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2
[PROOF STEP]
obtain kx where "\<And> q . q \<in> states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q . states M) 0 q = ofsm_table M (\<lambda>q . states M) kx q" and "\<And> q k'' . q \<in> states M \<Longrightarrow> k'' \<ge> kx \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k'' q = ofsm_table M (\<lambda>q . states M) kx q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>kx. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) kx q; \<And>q k''. \<lbrakk>q \<in> FSM.states M; kx \<le> k''\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k'' q = ofsm_table M (\<lambda>q. FSM.states M) kx q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ofsm_table_fix_length[of M "(\<lambda>q . states M)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> FSM.states M \<subseteq> FSM.states M; \<And>k. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) k q; \<And>q k'. \<lbrakk>q \<in> FSM.states M; k \<le> k'\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q = ofsm_table M (\<lambda>q. FSM.states M) k q\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>kx. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) kx q; \<And>q k''. \<lbrakk>q \<in> FSM.states M; kx \<le> k''\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k'' q = ofsm_table M (\<lambda>q. FSM.states M) kx q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?q \<in> FSM.states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q = ofsm_table M (\<lambda>q. FSM.states M) kx ?q
\<lbrakk>?q \<in> FSM.states M; kx \<le> ?k''\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) ?k'' ?q = ofsm_table M (\<lambda>q. FSM.states M) kx ?q

goal (2 subgoals):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2
 2. \<lbrakk>k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2
[PROOF STEP]
have P: "(\<And>x. kx \<le> x \<Longrightarrow> ofsm_table M (\<lambda>q . states M) x q1 \<noteq> ofsm_table M (\<lambda>q . states M) x q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. kx \<le> x \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2
[PROOF STEP]
using \<open>\<And> q k'' . q \<in> states M \<Longrightarrow> k'' \<ge> kx \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k'' q = ofsm_table M (\<lambda>q . states M) kx q\<close> \<open>q1 \<in> FSM.states M\<close> \<open>q2 \<in> FSM.states M\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> FSM.states M; kx \<le> ?k''\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) ?k'' ?q = ofsm_table M (\<lambda>q. FSM.states M) kx ?q
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. \<And>x. kx \<le> x \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) x q2
[PROOF STEP]
by (metis assms \<open>\<And> q . q \<in> states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q . states M) 0 q = ofsm_table M (\<lambda>q . states M) kx q\<close>)
[PROOF STATE]
proof (state)
this:
kx \<le> ?x \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) ?x q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) ?x q2

goal (2 subgoals):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2
 2. \<lbrakk>k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2
[PROOF STEP]
show "ofsm_table M (\<lambda>q . states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q . states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2
[PROOF STEP]
using minimal_fixpoint_helper(1)[OF f P, of kx k]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. kx \<le> x \<Longrightarrow> kx \<le> x) \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2

goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 k) q2

goal (1 subgoal):
 1. \<lbrakk>k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2
[PROOF STEP]
show "k \<le> k' \<Longrightarrow> k' < (find_first_distinct_ofsm_table_gt M q1 q2 k) \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k' q1 = ofsm_table M (\<lambda>q . states M) k' q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2
[PROOF STEP]
using minimal_fixpoint_helper(2)[OF f P, of kx k k']
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. kx \<le> x \<Longrightarrow> kx \<le> x; k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> \<not> ofsm_table M (\<lambda>q. FSM.states M) k' q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k' q2

goal (1 subgoal):
 1. \<lbrakk>k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>k \<le> k'; k' < find_first_distinct_ofsm_table_gt M q1 q2 k\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_first_distinct_ofsm_table_is_first :
  assumes "q1 \<in> FSM.states M"
      and "q2 \<in> FSM.states M"
      and "ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2"
shows "ofsm_table M (\<lambda>q . states M) (find_first_distinct_ofsm_table M q1 q2) q1 \<noteq> ofsm_table M (\<lambda>q . states M) (find_first_distinct_ofsm_table M q1 q2) q2"
  and "k' < (find_first_distinct_ofsm_table M q1 q2) \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k' q1 = ofsm_table M (\<lambda>q . states M) k' q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q2 &&& (k' < find_first_distinct_ofsm_table_gt M q1 q2 0 \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2)
[PROOF STEP]
using find_first_distinct_ofsm_table_gt_is_first_gt[OF assms, of 0]
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q2
\<lbrakk>0 \<le> ?k'; ?k' < find_first_distinct_ofsm_table_gt M q1 q2 0\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) ?k' q1 = ofsm_table M (\<lambda>q. FSM.states M) ?k' q2

goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q2 &&& (k' < find_first_distinct_ofsm_table_gt M q1 q2 0 \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k' q1 = ofsm_table M (\<lambda>q. FSM.states M) k' q2)
[PROOF STEP]
by blast+