[STATEMENT]
lemma  path_split_general:
assumes all:"\<forall>zs. xs \<noteq> ys@zs"
obtains j zs where "xs = (take j ys)@zs" and "j < length ys"
  and "\<forall>k > j. \<forall>zs'. xs \<noteq> (take k ys)@zs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j zs. \<lbrakk>xs = take j ys @ zs; j < length ys; \<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs')
[PROOF STEP]
from \<open>\<forall>zs. xs \<noteq> ys@zs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>zs. xs \<noteq> ys @ zs
[PROOF STEP]
show "\<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and>
               (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs')"
[PROOF STATE]
proof (prove)
using this:
\<forall>zs. xs \<noteq> ys @ zs

goal (1 subgoal):
 1. \<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs')
[PROOF STEP]
proof(induct ys arbitrary:xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. \<forall>zs. xs \<noteq> [] @ zs \<Longrightarrow> \<exists>j zs. xs = take j [] @ zs \<and> j < length [] \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k [] @ zs')
 2. \<And>a ys xs. \<lbrakk>\<And>xs. \<forall>zs. xs \<noteq> ys @ zs \<Longrightarrow> \<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs'); \<forall>zs. xs \<noteq> (a # ys) @ zs\<rbrakk> \<Longrightarrow> \<exists>j zs. xs = take j (a # ys) @ zs \<and> j < length (a # ys) \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (a # ys) @ zs')
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>zs. xs \<noteq> [] @ zs

goal (2 subgoals):
 1. \<And>xs. \<forall>zs. xs \<noteq> [] @ zs \<Longrightarrow> \<exists>j zs. xs = take j [] @ zs \<and> j < length [] \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k [] @ zs')
 2. \<And>a ys xs. \<lbrakk>\<And>xs. \<forall>zs. xs \<noteq> ys @ zs \<Longrightarrow> \<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs'); \<forall>zs. xs \<noteq> (a # ys) @ zs\<rbrakk> \<Longrightarrow> \<exists>j zs. xs = take j (a # ys) @ zs \<and> j < length (a # ys) \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (a # ys) @ zs')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>zs. xs \<noteq> [] @ zs

goal (1 subgoal):
 1. \<exists>j zs. xs = take j [] @ zs \<and> j < length [] \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k [] @ zs')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j zs. xs = take j [] @ zs \<and> j < length [] \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k [] @ zs')

goal (1 subgoal):
 1. \<And>a ys xs. \<lbrakk>\<And>xs. \<forall>zs. xs \<noteq> ys @ zs \<Longrightarrow> \<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs'); \<forall>zs. xs \<noteq> (a # ys) @ zs\<rbrakk> \<Longrightarrow> \<exists>j zs. xs = take j (a # ys) @ zs \<and> j < length (a # ys) \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (a # ys) @ zs')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ys xs. \<lbrakk>\<And>xs. \<forall>zs. xs \<noteq> ys @ zs \<Longrightarrow> \<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs'); \<forall>zs. xs \<noteq> (a # ys) @ zs\<rbrakk> \<Longrightarrow> \<exists>j zs. xs = take j (a # ys) @ zs \<and> j < length (a # ys) \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (a # ys) @ zs')
[PROOF STEP]
case (Cons y' ys')
[PROOF STATE]
proof (state)
this:
\<forall>zs. ?xs \<noteq> ys' @ zs \<Longrightarrow> \<exists>j zs. ?xs = take j ys' @ zs \<and> j < length ys' \<and> (\<forall>k>j. \<forall>zs'. ?xs \<noteq> take k ys' @ zs')
\<forall>zs. xs \<noteq> (y' # ys') @ zs

goal (1 subgoal):
 1. \<And>a ys xs. \<lbrakk>\<And>xs. \<forall>zs. xs \<noteq> ys @ zs \<Longrightarrow> \<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs'); \<forall>zs. xs \<noteq> (a # ys) @ zs\<rbrakk> \<Longrightarrow> \<exists>j zs. xs = take j (a # ys) @ zs \<and> j < length (a # ys) \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (a # ys) @ zs')
[PROOF STEP]
note IH = \<open>\<And>xs. \<forall>zs. xs \<noteq> ys' @ zs \<Longrightarrow>
      \<exists>j zs. xs = take j ys' @ zs \<and> j < length ys' \<and>
      (\<forall>k. j < k \<longrightarrow> (\<forall>zs'. xs \<noteq> take k ys' @ zs'))\<close>
[PROOF STATE]
proof (state)
this:
\<forall>zs. ?xs \<noteq> ys' @ zs \<Longrightarrow> \<exists>j zs. ?xs = take j ys' @ zs \<and> j < length ys' \<and> (\<forall>k>j. \<forall>zs'. ?xs \<noteq> take k ys' @ zs')

goal (1 subgoal):
 1. \<And>a ys xs. \<lbrakk>\<And>xs. \<forall>zs. xs \<noteq> ys @ zs \<Longrightarrow> \<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs'); \<forall>zs. xs \<noteq> (a # ys) @ zs\<rbrakk> \<Longrightarrow> \<exists>j zs. xs = take j (a # ys) @ zs \<and> j < length (a # ys) \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (a # ys) @ zs')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
proof(cases xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. \<And>a list. xs = a # list \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. \<And>a list. xs = a # list \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
case (Cons x' xs')
[PROOF STATE]
proof (state)
this:
xs = x' # xs'

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
with \<open>\<forall>zs. xs \<noteq> (y' # ys') @ zs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>zs. xs \<noteq> (y' # ys') @ zs
xs = x' # xs'
[PROOF STEP]
have "x' \<noteq> y' \<or> (\<forall>zs. xs' \<noteq> ys' @ zs)"
[PROOF STATE]
proof (prove)
using this:
\<forall>zs. xs \<noteq> (y' # ys') @ zs
xs = x' # xs'

goal (1 subgoal):
 1. x' \<noteq> y' \<or> (\<forall>zs. xs' \<noteq> ys' @ zs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x' \<noteq> y' \<or> (\<forall>zs. xs' \<noteq> ys' @ zs)

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
proof(cases "x' = y'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x' = y'

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
with \<open>x' \<noteq> y' \<or> (\<forall>zs. xs' \<noteq> ys' @ zs)\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<noteq> y' \<or> (\<forall>zs. xs' \<noteq> ys' @ zs)
x' = y'
[PROOF STEP]
have "\<forall>zs. xs' \<noteq> ys' @ zs"
[PROOF STATE]
proof (prove)
using this:
x' \<noteq> y' \<or> (\<forall>zs. xs' \<noteq> ys' @ zs)
x' = y'

goal (1 subgoal):
 1. \<forall>zs. xs' \<noteq> ys' @ zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>zs. xs' \<noteq> ys' @ zs

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j zs. xs' = take j ys' @ zs \<and> j < length ys' \<and> (\<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs')
[PROOF STEP]
have "\<exists>j zs. xs' = take j ys' @ zs \<and> j < length ys' \<and>
          (\<forall>k. j < k \<longrightarrow> (\<forall>zs'. xs' \<noteq> take k ys' @ zs'))"
[PROOF STATE]
proof (prove)
using this:
\<exists>j zs. xs' = take j ys' @ zs \<and> j < length ys' \<and> (\<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs')

goal (1 subgoal):
 1. \<exists>j zs. xs' = take j ys' @ zs \<and> j < length ys' \<and> (\<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>j zs. xs' = take j ys' @ zs \<and> j < length ys' \<and> (\<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs')

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j zs. xs' = take j ys' @ zs \<and> j < length ys' \<and> (\<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs')
[PROOF STEP]
obtain j zs where "xs' = take j ys' @ zs"
          and "j < length ys'"
          and all_sub:"\<forall>k. j < k \<longrightarrow> (\<forall>zs'. xs' \<noteq> take k ys' @ zs')"
[PROOF STATE]
proof (prove)
using this:
\<exists>j zs. xs' = take j ys' @ zs \<and> j < length ys' \<and> (\<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs')

goal (1 subgoal):
 1. (\<And>j zs. \<lbrakk>xs' = take j ys' @ zs; j < length ys'; \<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xs' = take j ys' @ zs
j < length ys'
\<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs'

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
from \<open>xs' = take j ys' @ zs\<close> True
[PROOF STATE]
proof (chain)
picking this:
xs' = take j ys' @ zs
x' = y'
[PROOF STEP]
have "(x'#xs') = take (Suc j) (y' # ys') @ zs"
[PROOF STATE]
proof (prove)
using this:
xs' = take j ys' @ zs
x' = y'

goal (1 subgoal):
 1. x' # xs' = take (Suc j) (y' # ys') @ zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x' # xs' = take (Suc j) (y' # ys') @ zs

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
from all_sub True
[PROOF STATE]
proof (chain)
picking this:
\<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs'
x' = y'
[PROOF STEP]
have all_imp:"\<forall>k. j < k \<longrightarrow>
          (\<forall>zs'. (x'#xs') \<noteq> take (Suc k) (y' # ys') @ zs')"
[PROOF STATE]
proof (prove)
using this:
\<forall>k>j. \<forall>zs'. xs' \<noteq> take k ys' @ zs'
x' = y'

goal (1 subgoal):
 1. \<forall>k>j. \<forall>zs'. x' # xs' \<noteq> take (Suc k) (y' # ys') @ zs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k>j. \<forall>zs'. x' # xs' \<noteq> take (Suc k) (y' # ys') @ zs'

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>k>j. \<forall>zs'. x' # xs' \<noteq> take (Suc k) (y' # ys') @ zs'

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
assume "(Suc j) < l"
[PROOF STATE]
proof (state)
this:
Suc j < l

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc j < l
[PROOF STEP]
obtain k where [simp]:"l = Suc k"
[PROOF STATE]
proof (prove)
using this:
Suc j < l

goal (1 subgoal):
 1. (\<And>k. l = Suc k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases l) auto
[PROOF STATE]
proof (state)
this:
l = Suc k

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
with \<open>(Suc j) < l\<close>
[PROOF STATE]
proof (chain)
picking this:
Suc j < l
l = Suc k
[PROOF STEP]
have "j < k"
[PROOF STATE]
proof (prove)
using this:
Suc j < l
l = Suc k

goal (1 subgoal):
 1. j < k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j < k

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
with all_imp
[PROOF STATE]
proof (chain)
picking this:
\<forall>k>j. \<forall>zs'. x' # xs' \<noteq> take (Suc k) (y' # ys') @ zs'
j < k
[PROOF STEP]
have "\<forall>zs'. (x'#xs') \<noteq> take (Suc k) (y' # ys') @ zs'"
[PROOF STATE]
proof (prove)
using this:
\<forall>k>j. \<forall>zs'. x' # xs' \<noteq> take (Suc k) (y' # ys') @ zs'
j < k

goal (1 subgoal):
 1. \<forall>zs'. x' # xs' \<noteq> take (Suc k) (y' # ys') @ zs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>zs'. x' # xs' \<noteq> take (Suc k) (y' # ys') @ zs'

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
hence "\<forall>zs'. (x'#xs') \<noteq> take l (y' # ys') @ zs'"
[PROOF STATE]
proof (prove)
using this:
\<forall>zs'. x' # xs' \<noteq> take (Suc k) (y' # ys') @ zs'

goal (1 subgoal):
 1. \<forall>zs'. x' # xs' \<noteq> take l (y' # ys') @ zs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>zs'. x' # xs' \<noteq> take l (y' # ys') @ zs'

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Suc j < ?l2 \<Longrightarrow> \<forall>zs'. x' # xs' \<noteq> take ?l2 (y' # ys') @ zs'

goal (2 subgoals):
 1. x' = y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
 2. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
with \<open>(x'#xs') = take (Suc j) (y' # ys') @ zs\<close> \<open>j < length ys'\<close> Cons
[PROOF STATE]
proof (chain)
picking this:
x' # xs' = take (Suc j) (y' # ys') @ zs
j < length ys'
xs = x' # xs'
Suc j < ?l2 \<Longrightarrow> \<forall>zs'. x' # xs' \<noteq> take ?l2 (y' # ys') @ zs'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x' # xs' = take (Suc j) (y' # ys') @ zs
j < length ys'
xs = x' # xs'
Suc j < ?l2 \<Longrightarrow> \<forall>zs'. x' # xs' \<noteq> take ?l2 (y' # ys') @ zs'

goal (1 subgoal):
 1. \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
by (metis Suc_length_conv less_Suc_eq_0_disj)
[PROOF STATE]
proof (state)
this:
\<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')

goal (1 subgoal):
 1. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x' \<noteq> y'

goal (1 subgoal):
 1. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
xs = x' # xs'
x' \<noteq> y'
[PROOF STEP]
have "\<forall>i zs'. i > 0 \<longrightarrow> xs \<noteq> take i (y' # ys') @ zs'"
[PROOF STATE]
proof (prove)
using this:
xs = x' # xs'
x' \<noteq> y'

goal (1 subgoal):
 1. \<forall>i zs'. 0 < i \<longrightarrow> xs \<noteq> take i (y' # ys') @ zs'
[PROOF STEP]
by auto(case_tac i,auto)
[PROOF STATE]
proof (state)
this:
\<forall>i zs'. 0 < i \<longrightarrow> xs \<noteq> take i (y' # ys') @ zs'

goal (1 subgoal):
 1. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i zs'. 0 < i \<longrightarrow> xs \<noteq> take i (y' # ys') @ zs'

goal (1 subgoal):
 1. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
have "\<exists>zs. xs = take 0 (y' # ys') @ zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>zs. xs = take 0 (y' # ys') @ zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>zs. xs = take 0 (y' # ys') @ zs

goal (1 subgoal):
 1. x' \<noteq> y' \<Longrightarrow> \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i zs'. 0 < i \<longrightarrow> xs \<noteq> take i (y' # ys') @ zs'
\<exists>zs. xs = take 0 (y' # ys') @ zs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i zs'. 0 < i \<longrightarrow> xs \<noteq> take i (y' # ys') @ zs'
\<exists>zs. xs = take 0 (y' # ys') @ zs

goal (1 subgoal):
 1. \<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')
[PROOF STEP]
by(rule_tac x="0" in exI,auto)
[PROOF STATE]
proof (state)
this:
\<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j zs. xs = take j (y' # ys') @ zs \<and> j < length (y' # ys') \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k (y' # ys') @ zs')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j zs. xs = take j ys @ zs \<and> j < length ys \<and> (\<forall>k>j. \<forall>zs'. xs \<noteq> take k ys @ zs')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma divmod_integer_code''[code]: "divmod_integer k l =
  (if k = 0 then (0, 0)
    else if l > 0 then
            (if k > 0 then divmod_abs' k l
             else case divmod_abs' (- k) l of (r, s) \<Rightarrow>
                  if s = 0 then (- r, 0) else (- r - 1, l - s))
    else if l = 0 then (0, k)
    else apsnd uminus
            (if k < 0 then divmod_abs' (-k) (-l)
             else case divmod_abs' k (-l) of (r, s) \<Rightarrow>
                  if s = 0 then (- r, 0) else (- r - 1, - l - s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divmod_integer k l = (if k = 0 then (0, 0) else if 0 < l then if 0 < k then divmod_abs' k l else case divmod_abs' (- k) l of (r, s) \<Rightarrow> if s = 0 then (- r, 0) else (- r - 1, l - s) else if l = 0 then (0, k) else apsnd uminus (if k < 0 then divmod_abs' (- k) (- l) else case divmod_abs' k (- l) of (r, s) \<Rightarrow> if s = 0 then (- r, 0) else (- r - 1, - l - s)))
[PROOF STEP]
unfolding divmod_integer_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if k = 0 then (0, 0) else if 0 < l then if 0 < k then Code_Numeral.divmod_abs k l else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow> if s = 0 then (- r, 0) else (- r - 1, l - s) else if l = 0 then (0, k) else apsnd uminus (if k < 0 then Code_Numeral.divmod_abs k l else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow> if s = 0 then (- r, 0) else (- r - 1, - l - s))) = (if k = 0 then (0, 0) else if 0 < l then if 0 < k then divmod_abs' k l else case divmod_abs' (- k) l of (r, s) \<Rightarrow> if s = 0 then (- r, 0) else (- r - 1, l - s) else if l = 0 then (0, k) else apsnd uminus (if k < 0 then divmod_abs' (- k) (- l) else case divmod_abs' k (- l) of (r, s) \<Rightarrow> if s = 0 then (- r, 0) else (- r - 1, - l - s)))
[PROOF STEP]
by (cases "l = 0"; cases "l < 0"; cases "l > 0"; auto split: prod.splits simp: divmod_abs'_def divmod_abs_def)


[STATEMENT]
lemma divmod_nat_code'[code]: "Euclidean_Division.divmod_nat m n = (
  let k = integer_of_nat m; l = integer_of_nat n
  in map_prod nat_of_integer nat_of_integer
  (if k = 0 then (0, 0)
    else if l = 0 then (0,k) else
            divmod_abs' k l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Euclidean_Division.divmod_nat m n = (let k = integer_of_nat m; l = integer_of_nat n in map_prod nat_of_integer nat_of_integer (if k = 0 then (0, 0) else if l = 0 then (0, k) else divmod_abs' k l))
[PROOF STEP]
using divmod_nat_code [of m n]
[PROOF STATE]
proof (prove)
using this:
Euclidean_Division.divmod_nat m n = (let k = integer_of_nat m; l = integer_of_nat n in map_prod nat_of_integer nat_of_integer (if k = 0 then (0, 0) else if l = 0 then (0, k) else Code_Numeral.divmod_abs k l))

goal (1 subgoal):
 1. Euclidean_Division.divmod_nat m n = (let k = integer_of_nat m; l = integer_of_nat n in map_prod nat_of_integer nat_of_integer (if k = 0 then (0, 0) else if l = 0 then (0, k) else divmod_abs' k l))
[PROOF STEP]
by (simp add: divmod_abs'_def integer_of_nat_eq_of_nat Let_def)


[STATEMENT]
lemma binomial_code[code]:
  "n choose k = (if k \<le> n then fact n div (fact k * fact (n - k)) else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n choose k = (if k \<le> n then fact n div (fact k * fact (n - k)) else 0)
[PROOF STEP]
using binomial_eq_0[of n k] binomial_altdef_nat[of k n]
[PROOF STATE]
proof (prove)
using this:
n < k \<Longrightarrow> n choose k = 0
k \<le> n \<Longrightarrow> n choose k = fact n div (fact k * fact (n - k))

goal (1 subgoal):
 1. n choose k = (if k \<le> n then fact n div (fact k * fact (n - k)) else 0)
[PROOF STEP]
by simp


[STATEMENT]
lemma while_top:
  "top \<star> x = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top \<star> x = top
[PROOF STEP]
by (metis sup_left_top star.circ_top star_omega_top while_def)


[STATEMENT]
lemma while_one_top:
  "1 \<star> x = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<star> x = top
[PROOF STEP]
by (simp add: omega_one while_def)


[STATEMENT]
lemma while_finite_associative:
  "x\<^sup>\<omega> = bot \<Longrightarrow> (x \<star> y) * z = x \<star> (y * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<omega> = bot \<Longrightarrow> (x \<star> y) * z = x \<star> y * z
[PROOF STEP]
by (simp add: while_def mult_assoc)


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


[STATEMENT]
lemma while_sub_mult_one:
  "x * (1 \<star> y) \<le> 1 \<star> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * ((1::'a) \<star> y) \<le> (1::'a) \<star> x
[PROOF STEP]
by (simp add: omega_one while_def)


[STATEMENT]
lemma while_while_one:
  "y \<star> (x \<star> 1) = y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * x\<^sup>\<omega> \<squnion> y\<^sup>\<star> * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<star> x \<star> (1::'a) = y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * x\<^sup>\<omega> \<squnion> y\<^sup>\<star> * x\<^sup>\<star>
[PROOF STEP]
using mult_left_dist_sup sup_assoc while_def
[PROOF STATE]
proof (prove)
using this:
?x * (?y \<squnion> ?z) = ?x * ?y \<squnion> ?x * ?z
?x \<squnion> ?y \<squnion> ?z = ?x \<squnion> (?y \<squnion> ?z)
?x \<star> ?y = ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> * ?y

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


[STATEMENT]
lemma while_simulate_4_plus:
  assumes "y * x \<le> x * (x \<star> (1 \<squnion> y))"
    shows "y * x * x\<^sup>\<star> \<le> x * (x \<star> (1 \<squnion> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> x * (x \<star> (1::'a) \<squnion> y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> x * (x \<star> (1::'a) \<squnion> y)
[PROOF STEP]
have 1: "x * (x \<star> (1 \<squnion> y)) = x\<^sup>\<omega> \<squnion> x * x\<^sup>\<star> \<squnion> x * x\<^sup>\<star> * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (x \<star> (1::'a) \<squnion> y) = x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y
[PROOF STEP]
using mult_left_dist_sup omega_unfold sup_assoc while_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
?x * (?y \<squnion> ?z) = ?x * ?y \<squnion> ?x * ?z
?y\<^sup>\<omega> = ?y * ?y\<^sup>\<omega>
?x \<squnion> ?y \<squnion> ?z = ?x \<squnion> (?y \<squnion> ?z)
?x \<star> ?y = ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> * ?y
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. x * (x \<star> (1::'a) \<squnion> y) = x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x * (x \<star> (1::'a) \<squnion> y) = x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y

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

goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y) * x\<^sup>\<star>
[PROOF STEP]
using assms mult_left_isotone
[PROOF STATE]
proof (prove)
using this:
x * (x \<star> (1::'a) \<squnion> y) = x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y
y * x \<le> x * (x \<star> (1::'a) \<squnion> y)
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z

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

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

goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> x * (x \<star> (1::'a) \<squnion> y)
[PROOF STEP]
have "... = x\<^sup>\<omega> * x\<^sup>\<star> \<squnion> x * x\<^sup>\<star> * x\<^sup>\<star> \<squnion> x * x\<^sup>\<star> * y * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y) * x\<^sup>\<star> = x\<^sup>\<omega> * x\<^sup>\<star> \<squnion> x\<^sup>+ * x\<^sup>\<star> \<squnion> x\<^sup>+ * y * x\<^sup>\<star>
[PROOF STEP]
using mult_right_dist_sup
[PROOF STATE]
proof (prove)
using this:
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z

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

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

goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> x * (x \<star> (1::'a) \<squnion> y)
[PROOF STEP]
have "... = x * x\<^sup>\<star> * (y * x * x\<^sup>\<star>) \<squnion> x\<^sup>\<omega> \<squnion> x * x\<^sup>\<star> \<squnion> x * x\<^sup>\<star> * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<omega> * x\<^sup>\<star> \<squnion> x\<^sup>+ * x\<^sup>\<star> \<squnion> x\<^sup>+ * y * x\<^sup>\<star> = x\<^sup>+ * (y * x * x\<^sup>\<star>) \<squnion> x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y
[PROOF STEP]
by (smt sup_assoc sup_commute mult_assoc omega_mult_star_2 star.circ_back_loop_fixpoint star.circ_plus_same star.circ_transitive_equal)
[PROOF STATE]
proof (state)
this:
x\<^sup>\<omega> * x\<^sup>\<star> \<squnion> x\<^sup>+ * x\<^sup>\<star> \<squnion> x\<^sup>+ * y * x\<^sup>\<star> = x\<^sup>+ * (y * x * x\<^sup>\<star>) \<squnion> x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y

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

goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> x\<^sup>+ * (y * x * x\<^sup>\<star>) \<squnion> (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y)
[PROOF STEP]
using sup_assoc
[PROOF STATE]
proof (prove)
using this:
y * x * x\<^sup>\<star> \<le> x\<^sup>+ * (y * x * x\<^sup>\<star>) \<squnion> x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y
?x \<squnion> ?y \<squnion> ?z = ?x \<squnion> (?y \<squnion> ?z)

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

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

goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> x\<^sup>+\<^sup>\<omega> \<squnion> x\<^sup>+\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y)
[PROOF STEP]
by (simp add: omega_induct sup_monoid.add_commute)
[PROOF STATE]
proof (state)
this:
y * x * x\<^sup>\<star> \<le> x\<^sup>+\<^sup>\<omega> \<squnion> x\<^sup>+\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y)

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

goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> x * (x \<star> (1::'a) \<squnion> y)
[PROOF STEP]
have "... = x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x * x\<^sup>\<star> \<squnion> x * x\<^sup>\<star> * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>+\<^sup>\<omega> \<squnion> x\<^sup>+\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y) = x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y)
[PROOF STEP]
by (simp add: left_plus_omega star.left_plus_circ)
[PROOF STATE]
proof (state)
this:
x\<^sup>+\<^sup>\<omega> \<squnion> x\<^sup>+\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y) = x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y)

goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> x * (x \<star> (1::'a) \<squnion> y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y * x * x\<^sup>\<star> \<le> x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y * x * x\<^sup>\<star> \<le> x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y)

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

goal (1 subgoal):
 1. y * x * x\<^sup>\<star> \<le> x * (x \<star> (1::'a) \<squnion> y)
[PROOF STEP]
by (metis while_def while_mult_star_exchange while_transitive)
[PROOF STATE]
proof (state)
this:
y * x * x\<^sup>\<star> \<le> x * (x \<star> (1::'a) \<squnion> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma while_simulate_4_omega:
  assumes "y * x \<le> x * (x \<star> (1 \<squnion> y))"
    shows "y * x\<^sup>\<omega> \<le> x\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * x\<^sup>\<omega> \<le> x\<^sup>\<omega>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y * x\<^sup>\<omega> \<le> x\<^sup>\<omega>
[PROOF STEP]
have "x * (x \<star> (1 \<squnion> y)) = x\<^sup>\<omega> \<squnion> x * x\<^sup>\<star> \<squnion> x * x\<^sup>\<star> * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (x \<star> (1::'a) \<squnion> y) = x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y
[PROOF STEP]
using mult_1_right mult_left_dist_sup omega_unfold sup_assoc while_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
?a * (1::'a) = ?a
?x * (?y \<squnion> ?z) = ?x * ?y \<squnion> ?x * ?z
?y\<^sup>\<omega> = ?y * ?y\<^sup>\<omega>
?x \<squnion> ?y \<squnion> ?z = ?x \<squnion> (?y \<squnion> ?z)
?x \<star> ?y = ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> * ?y
?a * ?b * ?c = ?a * (?b * ?c)

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

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

goal (1 subgoal):
 1. y * x\<^sup>\<omega> \<le> (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y) * x\<^sup>\<omega>
[PROOF STEP]
by (smt assms le_iff_sup mult_assoc mult_right_dist_sup omega_unfold)
[PROOF STATE]
proof (state)
this:
y * x\<^sup>\<omega> \<le> (x\<^sup>\<omega> \<squnion> x\<^sup>+ \<squnion> x\<^sup>+ * y) * x\<^sup>\<omega>

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

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

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

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

goal (1 subgoal):
 1. y * x\<^sup>\<omega> \<le> x\<^sup>\<omega>
[PROOF STEP]
have "... = x * x\<^sup>\<star> * (y * x\<^sup>\<omega>) \<squnion> x\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<omega> * x\<^sup>\<omega> \<squnion> x\<^sup>+ * x\<^sup>\<omega> \<squnion> x\<^sup>+ * y * x\<^sup>\<omega> = x\<^sup>+ * (y * x\<^sup>\<omega>) \<squnion> x\<^sup>\<omega>
[PROOF STEP]
by (metis sup_commute le_iff_sup mult_assoc omega_sub_vector omega_unfold star_mult_omega)
[PROOF STATE]
proof (state)
this:
x\<^sup>\<omega> * x\<^sup>\<omega> \<squnion> x\<^sup>+ * x\<^sup>\<omega> \<squnion> x\<^sup>+ * y * x\<^sup>\<omega> = x\<^sup>+ * (y * x\<^sup>\<omega>) \<squnion> x\<^sup>\<omega>

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

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

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

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

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

goal (1 subgoal):
 1. y * x\<^sup>\<omega> \<le> x\<^sup>\<omega>
[PROOF STEP]
by (metis sup_idem left_plus_omega star_mult_omega)
[PROOF STATE]
proof (state)
this:
y * x\<^sup>\<omega> \<le> x\<^sup>\<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma while_unfold_below:
  "x = z \<squnion> y * x \<Longrightarrow> x \<le> y \<star> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = z \<squnion> y * x \<Longrightarrow> x \<le> y \<star> z
[PROOF STEP]
by (simp add: omega_induct while_def)


[STATEMENT]
lemma while_unfold_below_sub:
  "x \<le> z \<squnion> y * x \<Longrightarrow> x \<le> y \<star> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> z \<squnion> y * x \<Longrightarrow> x \<le> y \<star> z
[PROOF STEP]
by (simp add: omega_induct while_def)


[STATEMENT]
lemma while_unfold_below_1:
  "x = y * x \<Longrightarrow> x \<le> y \<star> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y * x \<Longrightarrow> x \<le> y \<star> (1::'a)
[PROOF STEP]
by (simp add: while_unfold_below_sub)


[STATEMENT]
lemma while_square_1:
  "x \<star> 1 = (x * x) \<star> (x \<squnion> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<star> (1::'a) = x * x \<star> x \<squnion> (1::'a)
[PROOF STEP]
by (metis mult_1_right omega_square star_square_2 while_def)


[STATEMENT]
lemma while_absorb_below_one:
  "y * x \<le> x \<Longrightarrow> y \<star> x \<le> 1 \<star> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * x \<le> x \<Longrightarrow> y \<star> x \<le> (1::'a) \<star> x
[PROOF STEP]
by (simp add: while_unfold_below_sub)


[STATEMENT]
lemma while_loop_is_greatest_postfixpoint:
  "is_greatest_postfixpoint (\<lambda>x . y * x \<squnion> z) (y \<star> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_greatest_postfixpoint (\<lambda>x. y * x \<squnion> z) (y \<star> z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_greatest_postfixpoint (\<lambda>x. y * x \<squnion> z) (y \<star> z)
[PROOF STEP]
have "(y \<star> z) \<le> (\<lambda>x . y * x \<squnion> z) (y \<star> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<star> z \<le> y * (y \<star> z) \<squnion> z
[PROOF STEP]
using sup_commute while_left_unfold
[PROOF STATE]
proof (prove)
using this:
?x \<squnion> ?y = ?y \<squnion> ?x
?x \<star> ?y = ?y \<squnion> ?x * (?x \<star> ?y)

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

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

goal (1 subgoal):
 1. is_greatest_postfixpoint (\<lambda>x. y * x \<squnion> z) (y \<star> z)
[PROOF STEP]
by (simp add: is_greatest_postfixpoint_def sup_commute while_unfold_below_sub)
[PROOF STATE]
proof (state)
this:
is_greatest_postfixpoint (\<lambda>x. y * x \<squnion> z) (y \<star> z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma while_loop_is_greatest_fixpoint:
  "is_greatest_fixpoint (\<lambda>x . y * x \<squnion> z) (y \<star> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_greatest_fixpoint (\<lambda>x. y * x \<squnion> z) (y \<star> z)
[PROOF STEP]
by (simp add: omega_loop_is_greatest_fixpoint while_def)


[STATEMENT]
lemma while_finite_associative_2:
  "x \<star> bot = bot \<Longrightarrow> (x \<star> y) * z = x \<star> (y * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<star> bot = bot \<Longrightarrow> (x \<star> y) * z = x \<star> y * z
[PROOF STEP]
by (metis sup_bot_left sup_bot_right mult_assoc mult_right_zero while_def)


[STATEMENT]
lemma tarski_mult_top_idempotent:
  "x * top = x * top * x * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top = x * top * x * top
[PROOF STEP]
by (metis sup_commute le_iff_sup mult_assoc star.circ_back_loop_fixpoint star.circ_left_top tarski top_mult_top)


[STATEMENT]
lemma tarski_top_omega_below:
  "x * top \<le> (x * top)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top \<le> (x * top)\<^sup>\<omega>
[PROOF STEP]
using omega_induct_mult order.refl mult_assoc tarski_mult_top_idempotent
[PROOF STATE]
proof (prove)
using this:
?y \<le> ?x * ?y \<Longrightarrow> ?y \<le> ?x\<^sup>\<omega>
?a \<le> ?a
?a * ?b * ?c = ?a * (?b * ?c)
?x * top = ?x * top * ?x * top

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


[STATEMENT]
lemma tarski_top_omega:
  "x * top = (x * top)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top = (x * top)\<^sup>\<omega>
[PROOF STEP]
by (simp add: order.eq_iff mult_top_omega tarski_top_omega_below)


[STATEMENT]
lemma tarski_below_top_omega:
  "x \<le> (x * top)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> (x * top)\<^sup>\<omega>
[PROOF STEP]
using top_right_mult_increasing tarski_top_omega
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?x * top
?x * top = (?x * top)\<^sup>\<omega>

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


[STATEMENT]
lemma tarski_mult_omega_omega:
  "(x * y\<^sup>\<omega>)\<^sup>\<omega> = x * y\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y\<^sup>\<omega>)\<^sup>\<omega> = x * y\<^sup>\<omega>
[PROOF STEP]
by (metis mult_assoc omega_vector tarski_top_omega)


[STATEMENT]
lemma tarski_omega_idempotent:
  "x\<^sup>\<omega>\<^sup>\<omega> = x\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<omega>\<^sup>\<omega> = x\<^sup>\<omega>
[PROOF STEP]
by (metis omega_vector tarski_top_omega)


[STATEMENT]
lemma while_denest_2a:
  "w * ((x \<star> (y * w)) \<star> z) = w * (((x \<star> y) * w) \<star> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) = w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) = w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
have "(x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<omega> = (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> * (((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<omega> \<squnion> ((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<star> * (x\<^sup>\<star> * y * w)\<^sup>\<omega>) \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<omega> = (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> * (((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<omega> \<squnion> ((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<star> * (x\<^sup>\<star> * y * w)\<^sup>\<omega>) \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<omega>
[PROOF STEP]
by (metis sup_commute omega_decompose omega_loop_fixpoint)
[PROOF STATE]
proof (state)
this:
(x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<omega> = (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> * (((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<omega> \<squnion> ((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<star> * (x\<^sup>\<star> * y * w)\<^sup>\<omega>) \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<omega>

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

goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) = w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
have "... \<le> (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> * (((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<omega> \<squnion> ((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<star> * (x\<^sup>\<star> * y * w)\<^sup>\<omega>) \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<omega> \<le> (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<omega>
[PROOF STEP]
by (metis sup_left_isotone mult_assoc mult_right_isotone omega_sub_vector)
[PROOF STATE]
proof (state)
this:
(x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> * (((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<omega> \<squnion> ((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<star> * (x\<^sup>\<star> * y * w)\<^sup>\<omega>) \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<omega> \<le> (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<omega>

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

goal (1 subgoal):
 1. w * (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<omega> \<le> (w * x\<^sup>\<star> * y)\<^sup>\<star> * w * x\<^sup>\<omega> \<squnion> (w * x\<^sup>\<star> * y)\<^sup>\<omega>
[PROOF STEP]
by (smt sup_commute le_iff_sup mult_assoc mult_left_dist_sup while_def while_slide)
[PROOF STATE]
proof (state)
this:
w * (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<omega> \<le> (w * x\<^sup>\<star> * y)\<^sup>\<star> * w * x\<^sup>\<omega> \<squnion> (w * x\<^sup>\<star> * y)\<^sup>\<omega>

goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) = w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
have "(x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<star> * z = (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> * ((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>\<star> * (x\<^sup>\<star> * y * w)\<^sup>\<star> * z \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<star> * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<star> * z = ((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>+ * (x\<^sup>\<star> * y * w)\<^sup>\<star> * z \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<star> * z
[PROOF STEP]
by (smt sup_commute mult_assoc star.circ_sup star.circ_loop_fixpoint)
[PROOF STATE]
proof (state)
this:
(x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<star> * z = ((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>+ * (x\<^sup>\<star> * y * w)\<^sup>\<star> * z \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<star> * z

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

goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) = w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
have "... \<le> (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<star> * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>+ * (x\<^sup>\<star> * y * w)\<^sup>\<star> * z \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<star> * z \<le> (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<star> * z
[PROOF STEP]
by (smt sup_commute sup_right_isotone mult_assoc mult_right_isotone omega_sub_vector)
[PROOF STATE]
proof (state)
this:
((x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega>)\<^sup>+ * (x\<^sup>\<star> * y * w)\<^sup>\<star> * z \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<star> * z \<le> (x\<^sup>\<star> * y * w)\<^sup>\<star> * x\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y * w)\<^sup>\<star> * z

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

goal (1 subgoal):
 1. w * (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<star> * z \<le> (w * x\<^sup>\<star> * y)\<^sup>\<star> * w * x\<^sup>\<omega> \<squnion> (w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z
[PROOF STEP]
by (metis mult_assoc mult_left_dist_sup mult_right_isotone star.circ_slide)
[PROOF STATE]
proof (state)
this:
w * (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<star> * z \<le> (w * x\<^sup>\<star> * y)\<^sup>\<star> * w * x\<^sup>\<omega> \<squnion> (w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z

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

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

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

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

goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) = w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
have "... \<le> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w * x\<^sup>\<star> * y)\<^sup>\<star> * (w * x\<^sup>\<omega>)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z \<le> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z
[PROOF STEP]
by (metis sup_mono sup_ge1 sup_ge2 mult_isotone mult_left_isotone omega_isotone star.circ_isotone)
[PROOF STATE]
proof (state)
this:
(w * x\<^sup>\<star> * y)\<^sup>\<star> * (w * x\<^sup>\<omega>)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z \<le> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z

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

goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) = w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
have "... = (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z = (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z
[PROOF STEP]
by (simp add: star_mult_omega)
[PROOF STATE]
proof (state)
this:
(w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z = (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (w * x\<^sup>\<omega> \<squnion> w * x\<^sup>\<star> * y)\<^sup>\<star> * w * z

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

goal (1 subgoal):
 1. w * ((x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<omega> \<squnion> (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<star> * z) \<le> w * ((x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y) * w)\<^sup>\<omega> \<squnion> w * ((x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y) * w)\<^sup>\<star> * z
[PROOF STEP]
by (smt mult_assoc mult_left_dist_sup omega_slide star.circ_slide)
[PROOF STATE]
proof (state)
this:
w * ((x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<omega> \<squnion> (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y * w)\<^sup>\<star> * z) \<le> w * ((x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y) * w)\<^sup>\<omega> \<squnion> w * ((x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * y) * w)\<^sup>\<star> * z

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

goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) \<le> w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
by (simp add: mult_left_dist_sup while_def mult_assoc)
[PROOF STATE]
proof (state)
this:
w * ((x \<star> y * w) \<star> z) \<le> w * ((x \<star> y) * w \<star> z)

goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) = w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
have "w * (((x \<star> y) * w) \<star> z) \<le> w * ((x \<star> (y * w)) \<star> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w * ((x \<star> y) * w \<star> z) \<le> w * ((x \<star> y * w) \<star> z)
[PROOF STEP]
by (simp add: mult_right_isotone while_left_isotone while_sub_associative)
[PROOF STATE]
proof (state)
this:
w * ((x \<star> y) * w \<star> z) \<le> w * ((x \<star> y * w) \<star> z)

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

goal (1 subgoal):
 1. w * ((x \<star> y * w) \<star> z) = w * ((x \<star> y) * w \<star> z)
[PROOF STEP]
using 2 order.antisym
[PROOF STATE]
proof (prove)
using this:
w * ((x \<star> y) * w \<star> z) \<le> w * ((x \<star> y * w) \<star> z)
w * ((x \<star> y * w) \<star> z) \<le> w * ((x \<star> y) * w \<star> z)
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma while_denest_3:
  "(x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>
[PROOF STEP]
have 1: "(x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega> \<squnion> (x \<star> w)\<^sup>\<star> * x\<^sup>\<omega>\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega> \<squnion> (x \<star> w)\<^sup>\<star> * x\<^sup>\<omega>\<^sup>\<omega>
[PROOF STEP]
by (simp add: while_def tarski_omega_idempotent)
[PROOF STATE]
proof (state)
this:
(x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega> \<squnion> (x \<star> w)\<^sup>\<star> * x\<^sup>\<omega>\<^sup>\<omega>

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

goal (1 subgoal):
 1. (x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>
[PROOF STEP]
have "... \<le> (x \<star> w)\<^sup>\<omega> \<squnion> (x \<star> w)\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * w)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<star> w)\<^sup>\<omega> \<squnion> (x \<star> w)\<^sup>\<star> * x\<^sup>\<omega>\<^sup>\<omega> \<le> (x \<star> w)\<^sup>\<omega> \<squnion> (x \<star> w)\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * w)\<^sup>\<omega>
[PROOF STEP]
using mult_right_isotone omega_sub_dist semiring.add_left_mono
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
?x\<^sup>\<omega> \<le> (?x \<squnion> ?y)\<^sup>\<omega>
?a \<le> ?b \<Longrightarrow> ?c \<squnion> ?a \<le> ?c \<squnion> ?b

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

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

goal (1 subgoal):
 1. (x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>
[PROOF STEP]
have "... = (x \<star> w)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<star> w)\<^sup>\<omega> \<squnion> (x \<star> w)\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * w)\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>
[PROOF STEP]
by (simp add: star_mult_omega while_def)
[PROOF STATE]
proof (state)
this:
(x \<star> w)\<^sup>\<omega> \<squnion> (x \<star> w)\<^sup>\<star> * (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * w)\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>

goal (1 subgoal):
 1. (x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(x \<star> w) \<star> x\<^sup>\<omega> \<le> (x \<star> w)\<^sup>\<omega>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x \<star> w) \<star> x\<^sup>\<omega> \<le> (x \<star> w)\<^sup>\<omega>

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

goal (1 subgoal):
 1. (x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>
[PROOF STEP]
by (simp add: sup.order_iff)
[PROOF STATE]
proof (state)
this:
(x \<star> w) \<star> x\<^sup>\<omega> = (x \<star> w)\<^sup>\<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma while_denest_4a:
  "(x \<star> w) \<star> (x \<star> (y * z)) = (x \<star> w) \<star> ((x \<star> y) * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<star> w) \<star> x \<star> y * z = (x \<star> w) \<star> (x \<star> y) * z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x \<star> w) \<star> x \<star> y * z = (x \<star> w) \<star> (x \<star> y) * z
[PROOF STEP]
have "(x \<star> w) \<star> (x \<star> (y * z)) = (x \<star> w)\<^sup>\<omega> \<squnion> ((x \<star> w) \<star> (x\<^sup>\<star> * y * z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<star> w) \<star> x \<star> y * z = (x \<star> w)\<^sup>\<omega> \<squnion> ((x \<star> w) \<star> x\<^sup>\<star> * y * z)
[PROOF STEP]
using while_def while_denest_3 while_left_dist_sup mult_assoc
[PROOF STATE]
proof (prove)
using this:
?x \<star> ?y = ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> * ?y
(?x \<star> ?w) \<star> ?x\<^sup>\<omega> = (?x \<star> ?w)\<^sup>\<omega>
?x \<star> ?y \<squnion> ?z = (?x \<star> ?y) \<squnion> (?x \<star> ?z)
?a * ?b * ?c = ?a * (?b * ?c)

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

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

goal (1 subgoal):
 1. (x \<star> w) \<star> x \<star> y * z = (x \<star> w) \<star> (x \<star> y) * z
[PROOF STEP]
have "... \<le> (x \<star> w)\<^sup>\<omega> \<squnion> ((x \<star> w) \<star> ((x \<star> y) * z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<star> w)\<^sup>\<omega> \<squnion> ((x \<star> w) \<star> x\<^sup>\<star> * y * z) \<le> (x \<star> w)\<^sup>\<omega> \<squnion> ((x \<star> w) \<star> (x \<star> y) * z)
[PROOF STEP]
using mult_right_sub_dist_sup_right order.refl semiring.add_mono while_def while_right_isotone
[PROOF STATE]
proof (prove)
using this:
?y * ?z \<le> (?x \<squnion> ?y) * ?z
?a \<le> ?a
\<lbrakk>?a \<le> ?b; ?c \<le> ?d\<rbrakk> \<Longrightarrow> ?a \<squnion> ?c \<le> ?b \<squnion> ?d
?x \<star> ?y = ?x\<^sup>\<omega> \<squnion> ?x\<^sup>\<star> * ?y
?y \<le> ?z \<Longrightarrow> ?x \<star> ?y \<le> ?x \<star> ?z

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

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

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

goal (1 subgoal):
 1. (x \<star> w) \<star> x \<star> y * z = (x \<star> w) \<star> (x \<star> y) * z
[PROOF STEP]
have "(x \<star> w) \<star> ((x \<star> y) * z) \<le> (x \<star> w) \<star> (x \<star> (y * z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<star> w) \<star> (x \<star> y) * z \<le> (x \<star> w) \<star> x \<star> y * z
[PROOF STEP]
by (simp add: while_right_isotone while_sub_associative)
[PROOF STATE]
proof (state)
this:
(x \<star> w) \<star> (x \<star> y) * z \<le> (x \<star> w) \<star> x \<star> y * z

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

goal (1 subgoal):
 1. (x \<star> w) \<star> x \<star> y * z = (x \<star> w) \<star> (x \<star> y) * z
[PROOF STEP]
using 1 order.antisym
[PROOF STATE]
proof (prove)
using this:
(x \<star> w) \<star> (x \<star> y) * z \<le> (x \<star> w) \<star> x \<star> y * z
(x \<star> w) \<star> x \<star> y * z \<le> (x \<star> w) \<star> (x \<star> y) * z
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma while_mult_top:
  "(x * top) \<star> z = z \<squnion> x * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top \<star> z = z \<squnion> x * top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * top \<star> z = z \<squnion> x * top
[PROOF STEP]
have 1: "z \<squnion> x * top \<le> (x * top) \<star> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<squnion> x * top \<le> x * top \<star> z
[PROOF STEP]
by (metis le_supI sup_ge1 while_def while_increasing tarski_top_omega)
[PROOF STATE]
proof (state)
this:
z \<squnion> x * top \<le> x * top \<star> z

goal (1 subgoal):
 1. x * top \<star> z = z \<squnion> x * top
[PROOF STEP]
have "(x * top) \<star> z = z \<squnion> x * top * ((x * top) \<star> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top \<star> z = z \<squnion> x * top * (x * top \<star> z)
[PROOF STEP]
using while_left_unfold
[PROOF STATE]
proof (prove)
using this:
?x \<star> ?y = ?y \<squnion> ?x * (?x \<star> ?y)

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

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

goal (1 subgoal):
 1. x * top \<star> z = z \<squnion> x * top
[PROOF STEP]
have "... \<le> z \<squnion> x * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<squnion> x * top * (x * top \<star> z) \<le> z \<squnion> x * top
[PROOF STEP]
using mult_right_isotone sup_right_isotone top_greatest mult_assoc
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y
?x \<le> top
?a * ?b * ?c = ?a * (?b * ?c)

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

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

goal (1 subgoal):
 1. x * top \<star> z = z \<squnion> x * top
[PROOF STEP]
using 1 order.antisym
[PROOF STATE]
proof (prove)
using this:
x * top \<star> z \<le> z \<squnion> x * top
z \<squnion> x * top \<le> x * top \<star> z
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tarski_top_omega_below_2:
  "x * top \<le> (x * top) \<star> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top \<le> x * top \<star> bot
[PROOF STEP]
by (simp add: while_mult_top)


[STATEMENT]
lemma tarski_top_omega_2:
  "x * top = (x * top) \<star> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top = x * top \<star> bot
[PROOF STEP]
by (simp add: while_mult_top)


[STATEMENT]
lemma tarski_below_top_omega_2:
  "x \<le> (x * top) \<star> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> x * top \<star> bot
[PROOF STEP]
using top_right_mult_increasing tarski_top_omega_2
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?x * top
?x * top = ?x * top \<star> bot

goal (1 subgoal):
 1. x \<le> x * top \<star> bot
[PROOF STEP]
by auto


[STATEMENT]
lemma while_bot_1:
  "1 = (x * bot) \<star> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) = x * bot \<star> (1::'a)
[PROOF STEP]
by (simp add: mult_right_zero while_zero)


[STATEMENT]
lemma gcsort_count_input:
 "count_inv (count (mset xs)) (0, [length xs], xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_inv (count (mset xs)) (0, [length xs], xs)
[PROOF STEP]
by simp


[STATEMENT]
lemma gcsort_count_intro:
 "count_inv f t \<Longrightarrow> count (mset (gcsort_out t)) x = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_inv f t \<Longrightarrow> count (mset (gcsort_out t)) x = f x
[PROOF STEP]
by (cases t, simp add: gcsort_out_def)


[STATEMENT]
lemma offs_num_cons:
 "offs_num n (x # xs) index key mi ma i =
   (if index key x n mi ma = i then Suc else id) (offs_num n xs index key mi ma i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_num n (x # xs) index key mi ma i = (if index key x n mi ma = i then Suc else id) (offs_num n xs index key mi ma i)
[PROOF STEP]
by (simp add: offs_num_def)