[STATEMENT]
lemma length_lang_pow_lb:
  assumes "\<forall>x\<in>X. |x| \<ge> k" "x \<in> X^n"
  shows "|x| \<ge> k*n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<cdot> n \<le> |x|
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. k \<le> |x|
x \<in> X\<^bsup>n\<^esup>

goal (1 subgoal):
 1. k \<cdot> n \<le> |x|
[PROOF STEP]
proof (induct n arbitrary: x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>0\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> 0 \<le> |x|
 2. \<And>n x. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. k \<le> |x|
x \<in> X\<^bsup>0\<^esup>

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>0\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> 0 \<le> |x|
 2. \<And>n x. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. k \<le> |x|
x \<in> X\<^bsup>0\<^esup>

goal (1 subgoal):
 1. k \<cdot> 0 \<le> |x|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<cdot> 0 \<le> |x|

goal (1 subgoal):
 1. \<And>n x. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>X. k \<le> |x|; ?x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |?x|
\<forall>x\<in>X. k \<le> |x|
x \<in> X\<^bsup>Suc n\<^esup>

goal (1 subgoal):
 1. \<And>n x. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
note hyp = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>X. k \<le> |x|; ?x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |?x|
\<forall>x\<in>X. k \<le> |x|
x \<in> X\<^bsup>Suc n\<^esup>

goal (1 subgoal):
 1. \<And>n x. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>x\<in>X. k \<le> |x|; ?x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |?x|
\<forall>x\<in>X. k \<le> |x|
x \<in> X\<^bsup>Suc n\<^esup>

goal (1 subgoal):
 1. k \<cdot> Suc n \<le> |x|
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
have "x \<in> X\<^bsup>Suc n\<^esup> \<longleftrightarrow> (\<exists> y z. x = y@z \<and> y \<in> X \<and> z \<in> X\<^bsup>n\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> X\<^bsup>Suc n\<^esup>) = (\<exists>y z. x = y @ z \<and> y \<in> X \<and> z \<in> X\<^bsup>n\<^esup>)
[PROOF STEP]
by (simp add:c_prod_def times_list_def)
[PROOF STATE]
proof (state)
this:
(x \<in> X\<^bsup>Suc n\<^esup>) = (\<exists>y z. x = y @ z \<and> y \<in> X \<and> z \<in> X\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<in> X\<^bsup>Suc n\<^esup>) = (\<exists>y z. x = y @ z \<and> y \<in> X \<and> z \<in> X\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
from hyp
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<forall>x\<in>X. k \<le> |x|; ?x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |?x|
\<forall>x\<in>X. k \<le> |x|
x \<in> X\<^bsup>Suc n\<^esup>
[PROOF STEP]
have "... \<longrightarrow> (\<exists> y z. x = y@z \<and> |y| \<ge> k \<and> |z| \<ge> k*n)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>x\<in>X. k \<le> |x|; ?x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |?x|
\<forall>x\<in>X. k \<le> |x|
x \<in> X\<^bsup>Suc n\<^esup>

goal (1 subgoal):
 1. (\<exists>y z. x = y @ z \<and> y \<in> X \<and> z \<in> X\<^bsup>n\<^esup>) \<longrightarrow> (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z|)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>y z. x = y @ z \<and> y \<in> X \<and> z \<in> X\<^bsup>n\<^esup>) \<longrightarrow> (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z|)

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>y z. x = y @ z \<and> y \<in> X \<and> z \<in> X\<^bsup>n\<^esup>) \<longrightarrow> (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z|)

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
have "... \<longleftrightarrow> (\<exists> y z. x = y@z \<and> |y| \<ge> k \<and> |z| \<ge> k*n \<and> ( |x| = |y| + |z| ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z|) = (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z| \<and> |x| = |y| + |z|)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z|) = (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z| \<and> |x| = |y| + |z|)

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z|) = (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z| \<and> |x| = |y| + |z|)

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
have "... \<longleftrightarrow> (\<exists> y z. x = y@z \<and> |y| \<ge> k \<and> |z| \<ge> k*n \<and> ( |x| \<ge> (n + 1) * k ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z| \<and> |x| = |y| + |z|) = (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z| \<and> (n + 1) \<cdot> k \<le> |x|)
[PROOF STEP]
by (auto, metis add_mono mult.commute, force)
[PROOF STATE]
proof (state)
this:
(\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z| \<and> |x| = |y| + |z|) = (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z| \<and> (n + 1) \<cdot> k \<le> |x|)

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>\<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> n \<le> |x|; \<forall>x\<in>X. k \<le> |x|; x \<in> X\<^bsup>Suc n\<^esup>\<rbrakk> \<Longrightarrow> k \<cdot> Suc n \<le> |x|
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> X\<^bsup>Suc n\<^esup> \<longrightarrow> (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z| \<and> (n + 1) \<cdot> k \<le> |x|)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> X\<^bsup>Suc n\<^esup> \<longrightarrow> (\<exists>y z. x = y @ z \<and> k \<le> |y| \<and> k \<cdot> n \<le> |z| \<and> (n + 1) \<cdot> k \<le> |x|)

goal (1 subgoal):
 1. k \<cdot> Suc n \<le> |x|
[PROOF STEP]
by (metis Suc_eq_plus1 hyp(3) mult.commute)
[PROOF STATE]
proof (state)
this:
k \<cdot> Suc n \<le> |x|

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<cdot> Suc n \<le> |x|

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma l_prod_elim: "w\<in>X \<cdot> Y \<longleftrightarrow> (\<exists>u v. w = u@v \<and> u\<in>X \<and> v\<in>Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<in> X \<cdot> Y) = (\<exists>u v. w = u @ v \<and> u \<in> X \<and> v \<in> Y)
[PROOF STEP]
by (simp add: c_prod_def times_list_def)


[STATEMENT]
lemma power_minor_var:
  assumes "\<forall>w\<in>X. k\<le>|w|"
  shows "\<forall>w\<in>X\<^bsup>Suc n\<^esup>. n*k\<le>|w|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>X\<^bsup>Suc n\<^esup>. n \<cdot> k \<le> |w|
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>X. k \<le> |w|

goal (1 subgoal):
 1. \<forall>w\<in>X\<^bsup>Suc n\<^esup>. n \<cdot> k \<le> |w|
[PROOF STEP]
apply (auto simp add: l_prod_elim)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u v. \<lbrakk>\<forall>w\<in>X. k \<le> |w|; u \<in> X; v \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> n \<cdot> k \<le> |u| + |v|
[PROOF STEP]
using length_lang_pow_lb trans_le_add2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>x\<in>?X. ?k \<le> |x|; ?x \<in> ?X\<^bsup>?n\<^esup>\<rbrakk> \<Longrightarrow> ?k \<cdot> ?n \<le> |?x|
?i \<le> ?j \<Longrightarrow> ?i \<le> ?m + ?j

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>\<forall>w\<in>X. k \<le> |w|; u \<in> X; v \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> n \<cdot> k \<le> |u| + |v|
[PROOF STEP]
by (simp add: length_lang_pow_lb trans_le_add2 mult.commute)


[STATEMENT]
lemma power_lb: "(\<forall>w\<in>X. k\<le>|w| ) \<longrightarrow> (\<forall>w. w\<in>X\<^bsup>Suc n\<^esup> \<longrightarrow> n*k\<le>|w| )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w\<in>X. k \<le> |w|) \<longrightarrow> (\<forall>w. w \<in> X\<^bsup>Suc n\<^esup> \<longrightarrow> n \<cdot> k \<le> |w|)
[PROOF STEP]
by (metis power_minor_var)


[STATEMENT]
lemma prod_lb:
  "\<lbrakk> (\<forall>w\<in>X. m \<le> length w); (\<forall>w\<in>Y. n \<le> length w) \<rbrakk> \<Longrightarrow> (\<forall>w\<in>(X\<cdot>Y). (m+n) \<le> length w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>w\<in>X. m \<le> |w|; \<forall>w\<in>Y. n \<le> |w|\<rbrakk> \<Longrightarrow> \<forall>w\<in>X \<cdot> Y. m + n \<le> |w|
[PROOF STEP]
by (metis l_prod_elim add_le_mono length_append)


[STATEMENT]
lemma suicide_aux_l:
  "\<lbrakk> (\<forall>w\<in>Y. 0\<le>length w); (\<forall>w\<in>X\<^bsup>Suc n\<^esup>. n \<le> length w) \<rbrakk> \<Longrightarrow> (\<forall>w\<in>X\<^bsup>Suc n \<^esup>\<cdot> Y. n \<le> length w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>w\<in>Y. 0 \<le> |w|; \<forall>w\<in>X\<^bsup>Suc n\<^esup>. n \<le> |w|\<rbrakk> \<Longrightarrow> \<forall>w\<in>X\<^bsup>Suc n\<^esup> \<cdot> Y. n \<le> |w|
[PROOF STEP]
apply (auto simp: l_prod_elim)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v ua va. \<lbrakk>\<forall>w\<in>X \<cdot> X\<^bsup>n\<^esup>. n \<le> |w|; v \<in> Y; ua \<in> X; va \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> n \<le> |ua| + (|va| + |v|)
[PROOF STEP]
apply (drule_tac x="ua @ va" in bspec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v ua va. \<lbrakk>v \<in> Y; ua \<in> X; va \<in> X\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> ua @ va \<in> X \<cdot> X\<^bsup>n\<^esup>
 2. \<And>v ua va. \<lbrakk>v \<in> Y; ua \<in> X; va \<in> X\<^bsup>n\<^esup>; n \<le> |ua @ va|\<rbrakk> \<Longrightarrow> n \<le> |ua| + (|va| + |v|)
[PROOF STEP]
apply (auto simp add: l_prod_elim)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma suicide_aux_r:
  "\<lbrakk> (\<forall>w\<in>Y. 0\<le>length w); (\<forall>w\<in>X\<^bsup>Suc n\<^esup>. n \<le> length w) \<rbrakk> \<Longrightarrow> (\<forall>w\<in>Y \<cdot> X\<^bsup>Suc n\<^esup>. n \<le> length w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>w\<in>Y. 0 \<le> |w|; \<forall>w\<in>X\<^bsup>Suc n\<^esup>. n \<le> |w|\<rbrakk> \<Longrightarrow> \<forall>w\<in>Y \<cdot> X\<^bsup>Suc n\<^esup>. n \<le> |w|
[PROOF STEP]
by (auto, metis (full_types) le0 plus_nat.add_0 prod_lb)


[STATEMENT]
lemma word_suicide_l:
  assumes "\<not> l_ewp X" "Y \<noteq> {}"
  shows "(\<forall>w\<in>Y. \<exists>n. w\<notin>X\<^bsup>Suc n \<^esup>\<cdot> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y
[PROOF STEP]
have  "\<forall>v\<in>Y. 0\<le>length v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>Y. 0 \<le> |v|
[PROOF STEP]
by (metis le0)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>Y. 0 \<le> |v|

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> l_ewp X
Y \<noteq> {}
[PROOF STEP]
have "\<forall>v\<in>X. 1\<le>length v"
[PROOF STATE]
proof (prove)
using this:
\<not> l_ewp X
Y \<noteq> {}

goal (1 subgoal):
 1. \<forall>v\<in>X. 1 \<le> |v|
[PROOF STEP]
by (simp add: l_ewp_def, metis le_0_eq length_0_conv not_less_eq_eq)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>X. 1 \<le> |v|

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y
[PROOF STEP]
hence "\<forall>w\<in>Y. \<exists>n. w\<notin>X\<^bsup>Suc n \<^esup>\<cdot> Y"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>X. 1 \<le> |v|

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y
[PROOF STEP]
by (metis nat_mult_1_right power_lb suicide_aux_l le0 Suc_n_not_le_n)
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>Y. \<exists>n. w \<notin> X\<^bsup>Suc n\<^esup> \<cdot> Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma word_suicide_r:
  assumes "\<not> l_ewp X" "Y \<noteq> {}"
  shows "(\<forall>w\<in>Y. \<exists>n. w\<notin>Y \<cdot> X\<^bsup>Suc n\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>
[PROOF STEP]
have  "\<forall>v\<in>Y. 0\<le>length v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>Y. 0 \<le> |v|
[PROOF STEP]
by (metis le0)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>Y. 0 \<le> |v|

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> l_ewp X
Y \<noteq> {}
[PROOF STEP]
have "\<forall>v\<in>X. 1\<le>length v"
[PROOF STATE]
proof (prove)
using this:
\<not> l_ewp X
Y \<noteq> {}

goal (1 subgoal):
 1. \<forall>v\<in>X. 1 \<le> |v|
[PROOF STEP]
by (simp add: l_ewp_def, metis le_0_eq length_0_conv not_less_eq_eq)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>X. 1 \<le> |v|

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>
[PROOF STEP]
hence "\<forall>w\<in>Y. \<exists>n. w\<notin>Y \<cdot> X\<^bsup>Suc n \<^esup>"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>X. 1 \<le> |v|

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>
[PROOF STEP]
by (metis nat_mult_1_right power_lb suicide_aux_r le0 Suc_n_not_le_n)
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>

goal (1 subgoal):
 1. \<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>Y. \<exists>n. w \<notin> Y \<cdot> X\<^bsup>Suc n\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma word_suicide_lang_l: "\<lbrakk> \<not> l_ewp X; Y \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists> n. \<not> (Y \<le> X\<^bsup>Suc n \<^esup>\<cdot> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> l_ewp X; Y \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>n. \<not> Y \<subseteq> X\<^bsup>Suc n\<^esup> \<cdot> Y
[PROOF STEP]
by (metis Set.set_eqI empty_iff in_mono word_suicide_l)


[STATEMENT]
lemma word_suicide_lang_r: "\<lbrakk> \<not> l_ewp X; Y \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists> n. \<not> (Y \<le> Y \<cdot> X\<^bsup>Suc n\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> l_ewp X; Y \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>n. \<not> Y \<subseteq> Y \<cdot> X\<^bsup>Suc n\<^esup>
[PROOF STEP]
by (metis Set.set_eqI empty_iff in_mono word_suicide_r)


[STATEMENT]
lemma power_dual_transfer [simp]:
  "power.power (1::'a) (\<odot>) x n = x\<^bsup>n\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. power.power (1::'a) (\<odot>) x n = x\<^bsup>n\<^esup>
[PROOF STEP]
by (induct n, simp_all, metis opp_mult_def power_commutes)


[STATEMENT]
lemma aarden_aux_l:
  "y \<le> x \<cdot> y + z \<Longrightarrow> y \<le>  x\<^bsup>Suc n\<^esup> \<cdot> y + x\<^sup>\<star> \<cdot> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> x \<cdot> y + z \<Longrightarrow> y \<le> x\<^bsup>Suc n\<^esup> \<cdot> y + x\<^sup>\<star> \<cdot> z
[PROOF STEP]
using dual.aarden_aux[of "y" "x" "z" "n"]
[PROOF STATE]
proof (prove)
using this:
y \<le> y \<odot> x + z \<Longrightarrow> y \<le> y \<odot> power.power (1::'a) (\<odot>) x (Suc n) + z \<odot> x\<^sup>\<star>

goal (1 subgoal):
 1. y \<le> x \<cdot> y + z \<Longrightarrow> y \<le> x\<^bsup>Suc n\<^esup> \<cdot> y + x\<^sup>\<star> \<cdot> z
[PROOF STEP]
by (auto simp add:opp_mult_def)


[STATEMENT]
lemma arden_l:
  assumes "\<not> l_ewp y" "x = y\<cdot>x + z"
  shows "x = y\<^sup>\<star> \<cdot> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y\<^sup>\<star> \<cdot> z
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<subseteq> y\<^sup>\<star> \<cdot> z
 2. y\<^sup>\<star> \<cdot> z \<subseteq> x
[PROOF STEP]
show one: "y\<^sup>\<star> \<cdot> z \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y\<^sup>\<star> \<cdot> z \<subseteq> x
[PROOF STEP]
by (metis assms(2) join_semilattice_class.add_comm left_near_kleene_algebra_class.star_inductl_eq)
[PROOF STATE]
proof (state)
this:
y\<^sup>\<star> \<cdot> z \<subseteq> x

goal (1 subgoal):
 1. x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
show "x \<le> y\<^sup>\<star> \<cdot> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<subseteq> y\<^sup>\<star> \<cdot> z
 2. x \<noteq> 0 \<Longrightarrow> x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
show "x = 0 \<Longrightarrow> x \<le> y\<^sup>\<star>\<cdot>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = 0 \<Longrightarrow> x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = 0 \<Longrightarrow> x \<subseteq> y\<^sup>\<star> \<cdot> z

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
assume assms': "x \<noteq> 0"
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
have "\<And> n. x \<le> y\<^bsup>Suc n \<^esup>\<cdot> x + y\<^sup>\<star> \<cdot> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. x \<subseteq> y\<^bsup>Suc n\<^esup> \<cdot> x + y\<^sup>\<star> \<cdot> z
[PROOF STEP]
by (metis assms(2) kleene_algebra_class.aarden_aux_l subsetI)
[PROOF STATE]
proof (state)
this:
x \<subseteq> y\<^bsup>Suc ?n\<^esup> \<cdot> x + y\<^sup>\<star> \<cdot> z

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<subseteq> y\<^bsup>Suc ?n\<^esup> \<cdot> x + y\<^sup>\<star> \<cdot> z

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<subseteq> y\<^bsup>Suc ?n\<^esup> \<cdot> x + y\<^sup>\<star> \<cdot> z
[PROOF STEP]
have "\<And> w n. w \<in> x \<Longrightarrow> w \<in> y\<^bsup>Suc n \<^esup>\<cdot> x \<or> w \<in> y\<^sup>\<star> \<cdot> z"
[PROOF STATE]
proof (prove)
using this:
x \<subseteq> y\<^bsup>Suc ?n\<^esup> \<cdot> x + y\<^sup>\<star> \<cdot> z

goal (1 subgoal):
 1. \<And>w n. w \<in> x \<Longrightarrow> w \<in> y\<^bsup>Suc n\<^esup> \<cdot> x \<or> w \<in> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
by (force simp: plus_set_def)
[PROOF STATE]
proof (state)
this:
?w \<in> x \<Longrightarrow> ?w \<in> y\<^bsup>Suc ?n\<^esup> \<cdot> x \<or> ?w \<in> y\<^sup>\<star> \<cdot> z

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<subseteq> y\<^bsup>Suc ?n\<^esup> \<cdot> x + y\<^sup>\<star> \<cdot> z
?w \<in> x \<Longrightarrow> ?w \<in> y\<^bsup>Suc ?n\<^esup> \<cdot> x \<or> ?w \<in> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
show "x \<le> y\<^sup>\<star> \<cdot> z"
[PROOF STATE]
proof (prove)
using this:
x \<subseteq> y\<^bsup>Suc ?n\<^esup> \<cdot> x + y\<^sup>\<star> \<cdot> z
?w \<in> x \<Longrightarrow> ?w \<in> y\<^bsup>Suc ?n\<^esup> \<cdot> x \<or> ?w \<in> y\<^sup>\<star> \<cdot> z

goal (1 subgoal):
 1. x \<subseteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
by (metis (full_types) all_not_in_conv assms(1) subsetI word_suicide_l)
[PROOF STATE]
proof (state)
this:
x \<subseteq> y\<^sup>\<star> \<cdot> z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<subseteq> y\<^sup>\<star> \<cdot> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arden_r:
  assumes "\<not> l_ewp y" "x = x \<cdot> y + z"
  shows "x = z \<cdot> y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = z \<cdot> y\<^sup>\<star>
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<subseteq> z \<cdot> y\<^sup>\<star>
 2. z \<cdot> y\<^sup>\<star> \<subseteq> x
[PROOF STEP]
show one: "z \<cdot> y\<^sup>\<star> \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<cdot> y\<^sup>\<star> \<subseteq> x
[PROOF STEP]
by (metis assms(2) join.sup_commute kleene_algebra_class.star_inductr_var order_refl)
[PROOF STATE]
proof (state)
this:
z \<cdot> y\<^sup>\<star> \<subseteq> x

goal (1 subgoal):
 1. x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
show "x \<le> z \<cdot> y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<subseteq> z \<cdot> y\<^sup>\<star>
 2. x \<noteq> 0 \<Longrightarrow> x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
show "x = 0 \<Longrightarrow> x \<le> z \<cdot> y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = 0 \<Longrightarrow> x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = 0 \<Longrightarrow> x \<subseteq> z \<cdot> y\<^sup>\<star>

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
assume assms': "x \<noteq> 0"
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
have "\<And> n. x \<le> x \<cdot> y\<^bsup>Suc n\<^esup> + z \<cdot> y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. x \<subseteq> x \<cdot> y\<^bsup>Suc n\<^esup> + z \<cdot> y\<^sup>\<star>
[PROOF STEP]
by (metis assms(2) kleene_algebra_class.aarden_aux subsetI)
[PROOF STATE]
proof (state)
this:
x \<subseteq> x \<cdot> y\<^bsup>Suc ?n\<^esup> + z \<cdot> y\<^sup>\<star>

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<subseteq> x \<cdot> y\<^bsup>Suc ?n\<^esup> + z \<cdot> y\<^sup>\<star>

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<subseteq> x \<cdot> y\<^bsup>Suc ?n\<^esup> + z \<cdot> y\<^sup>\<star>
[PROOF STEP]
have "\<And> w n. w \<in> x \<Longrightarrow> w \<in> x \<cdot> y\<^bsup>Suc n\<^esup> \<or> w \<in> z \<cdot> y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
x \<subseteq> x \<cdot> y\<^bsup>Suc ?n\<^esup> + z \<cdot> y\<^sup>\<star>

goal (1 subgoal):
 1. \<And>w n. w \<in> x \<Longrightarrow> w \<in> x \<cdot> y\<^bsup>Suc n\<^esup> \<or> w \<in> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
by (force simp: plus_set_def)
[PROOF STATE]
proof (state)
this:
?w \<in> x \<Longrightarrow> ?w \<in> x \<cdot> y\<^bsup>Suc ?n\<^esup> \<or> ?w \<in> z \<cdot> y\<^sup>\<star>

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<subseteq> x \<cdot> y\<^bsup>Suc ?n\<^esup> + z \<cdot> y\<^sup>\<star>
?w \<in> x \<Longrightarrow> ?w \<in> x \<cdot> y\<^bsup>Suc ?n\<^esup> \<or> ?w \<in> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
show "x \<le> z \<cdot> y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
x \<subseteq> x \<cdot> y\<^bsup>Suc ?n\<^esup> + z \<cdot> y\<^sup>\<star>
?w \<in> x \<Longrightarrow> ?w \<in> x \<cdot> y\<^bsup>Suc ?n\<^esup> \<or> ?w \<in> z \<cdot> y\<^sup>\<star>

goal (1 subgoal):
 1. x \<subseteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
by (metis (full_types) all_not_in_conv assms(1) subsetI word_suicide_r)
[PROOF STATE]
proof (state)
this:
x \<subseteq> z \<cdot> y\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<subseteq> z \<cdot> y\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arden_l_counter: "\<exists> (x::'a lan) (y::'a lan) (z::'a lan). x = y \<cdot> x + z \<and> x \<noteq> y\<^sup>\<star> \<cdot> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. x = y \<cdot> x + z \<and> x \<noteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x y z. x = y \<cdot> x + z \<and> x \<noteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
have one: "(0::'a lan) + 1 \<cdot> 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + 1 \<cdot> 1 = 1
[PROOF STEP]
by (metis ab_near_semiring_one_class.mult_onel kleene_algebra_class.dual.add_zerol)
[PROOF STATE]
proof (state)
this:
0 + 1 \<cdot> 1 = 1

goal (1 subgoal):
 1. \<exists>x y z. x = y \<cdot> x + z \<and> x \<noteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
have two: "(1::'a lan) \<noteq> 1\<^sup>\<star> \<cdot> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<noteq> 1\<^sup>\<star> \<cdot> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<noteq> 1\<^sup>\<star> \<cdot> 0
[PROOF STEP]
have "\<exists>x\<^sub>1. (0::'a list set) \<noteq> x\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<^sub>1. 0 \<noteq> x\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<^sub>1. 0 \<noteq> x\<^sub>1

goal (1 subgoal):
 1. 1 \<noteq> 1\<^sup>\<star> \<cdot> 0
[PROOF STEP]
hence "(1::'a list set) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<^sub>1. 0 \<noteq> x\<^sub>1

goal (1 subgoal):
 1. 1 \<noteq> 0
[PROOF STEP]
by (metis kleene_algebra_class.dual.annir kleene_algebra_class.dual.mult.right_neutral)
[PROOF STATE]
proof (state)
this:
1 \<noteq> 0

goal (1 subgoal):
 1. 1 \<noteq> 1\<^sup>\<star> \<cdot> 0
[PROOF STEP]
thus "(1::'a list set) \<noteq> 1\<^sup>\<star> \<cdot> 0"
[PROOF STATE]
proof (prove)
using this:
1 \<noteq> 0

goal (1 subgoal):
 1. 1 \<noteq> 1\<^sup>\<star> \<cdot> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<noteq> 1\<^sup>\<star> \<cdot> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 \<noteq> 1\<^sup>\<star> \<cdot> 0

goal (1 subgoal):
 1. \<exists>x y z. x = y \<cdot> x + z \<and> x \<noteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. x = y \<cdot> x + z \<and> x \<noteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
using one and two
[PROOF STATE]
proof (prove)
using this:
0 + 1 \<cdot> 1 = 1
1 \<noteq> 1\<^sup>\<star> \<cdot> 0

goal (1 subgoal):
 1. \<exists>x y z. x = y \<cdot> x + z \<and> x \<noteq> y\<^sup>\<star> \<cdot> z
[PROOF STEP]
by (metis kleene_algebra_class.dual.add_zerol kleene_algebra_class.dual.add_zeror)
[PROOF STATE]
proof (state)
this:
\<exists>x y z. x = y \<cdot> x + z \<and> x \<noteq> y\<^sup>\<star> \<cdot> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arden_r_counter: "\<exists> (x::'a lan) (y::'a lan) (z::'a lan). x = x \<cdot> y + z \<and> x \<noteq> z \<cdot> y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. x = x \<cdot> y + z \<and> x \<noteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x y z. x = x \<cdot> y + z \<and> x \<noteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
have one: "(0::'a lan) + 1 \<cdot> 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + 1 \<cdot> 1 = 1
[PROOF STEP]
by (metis ab_near_semiring_one_class.mult_onel kleene_algebra_class.dual.add_zerol)
[PROOF STATE]
proof (state)
this:
0 + 1 \<cdot> 1 = 1

goal (1 subgoal):
 1. \<exists>x y z. x = x \<cdot> y + z \<and> x \<noteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
have two: "(1::'a lan) \<noteq> 0 \<cdot> 1\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<noteq> 0 \<cdot> 1\<^sup>\<star>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<noteq> 0 \<cdot> 1\<^sup>\<star>
[PROOF STEP]
have "\<exists>x\<^sub>1. (0::'a list set) \<noteq> x\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<^sub>1. 0 \<noteq> x\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<^sub>1. 0 \<noteq> x\<^sub>1

goal (1 subgoal):
 1. 1 \<noteq> 0 \<cdot> 1\<^sup>\<star>
[PROOF STEP]
hence "(1::'a list set) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<^sub>1. 0 \<noteq> x\<^sub>1

goal (1 subgoal):
 1. 1 \<noteq> 0
[PROOF STEP]
by (metis kleene_algebra_class.dual.annir kleene_algebra_class.dual.mult.right_neutral)
[PROOF STATE]
proof (state)
this:
1 \<noteq> 0

goal (1 subgoal):
 1. 1 \<noteq> 0 \<cdot> 1\<^sup>\<star>
[PROOF STEP]
thus "(1::'a list set) \<noteq> 0 \<cdot> 1\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
1 \<noteq> 0

goal (1 subgoal):
 1. 1 \<noteq> 0 \<cdot> 1\<^sup>\<star>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<noteq> 0 \<cdot> 1\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 \<noteq> 0 \<cdot> 1\<^sup>\<star>

goal (1 subgoal):
 1. \<exists>x y z. x = x \<cdot> y + z \<and> x \<noteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. x = x \<cdot> y + z \<and> x \<noteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
using one and two
[PROOF STATE]
proof (prove)
using this:
0 + 1 \<cdot> 1 = 1
1 \<noteq> 0 \<cdot> 1\<^sup>\<star>

goal (1 subgoal):
 1. \<exists>x y z. x = x \<cdot> y + z \<and> x \<noteq> z \<cdot> y\<^sup>\<star>
[PROOF STEP]
by (metis kleene_algebra_class.dual.add_zerol kleene_algebra_class.dual.add_zeror)
[PROOF STATE]
proof (state)
this:
\<exists>x y z. x = x \<cdot> y + z \<and> x \<noteq> z \<cdot> y\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rexp_ewp_l_ewp: "l_ewp (lang x) = rexp_ewp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_ewp (lang x) = rexp_ewp x
[PROOF STEP]
proof (induct x)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. l_ewp (lang 0\<^sub>r) = rexp_ewp 0\<^sub>r
 2. l_ewp (lang 1\<^sub>r) = rexp_ewp 1\<^sub>r
 3. \<And>x. l_ewp (lang \<langle>x\<rangle>) = rexp_ewp \<langle>x\<rangle>
 4. \<And>x1 x2. \<lbrakk>l_ewp (lang x1) = rexp_ewp x1; l_ewp (lang x2) = rexp_ewp x2\<rbrakk> \<Longrightarrow> l_ewp (lang (x1 +\<^sub>r x2)) = rexp_ewp (x1 +\<^sub>r x2)
 5. \<And>x1 x2. \<lbrakk>l_ewp (lang x1) = rexp_ewp x1; l_ewp (lang x2) = rexp_ewp x2\<rbrakk> \<Longrightarrow> l_ewp (lang (x1 \<cdot>\<^sub>r x2)) = rexp_ewp (x1 \<cdot>\<^sub>r x2)
 6. \<And>x. l_ewp (lang x) = rexp_ewp x \<Longrightarrow> l_ewp (lang (x\<^sup>\<star>\<^sub>r)) = rexp_ewp (x\<^sup>\<star>\<^sub>r)
[PROOF STEP]
case (Star x)
[PROOF STATE]
proof (state)
this:
l_ewp (lang x) = rexp_ewp x

goal (6 subgoals):
 1. l_ewp (lang 0\<^sub>r) = rexp_ewp 0\<^sub>r
 2. l_ewp (lang 1\<^sub>r) = rexp_ewp 1\<^sub>r
 3. \<And>x. l_ewp (lang \<langle>x\<rangle>) = rexp_ewp \<langle>x\<rangle>
 4. \<And>x1 x2. \<lbrakk>l_ewp (lang x1) = rexp_ewp x1; l_ewp (lang x2) = rexp_ewp x2\<rbrakk> \<Longrightarrow> l_ewp (lang (x1 +\<^sub>r x2)) = rexp_ewp (x1 +\<^sub>r x2)
 5. \<And>x1 x2. \<lbrakk>l_ewp (lang x1) = rexp_ewp x1; l_ewp (lang x2) = rexp_ewp x2\<rbrakk> \<Longrightarrow> l_ewp (lang (x1 \<cdot>\<^sub>r x2)) = rexp_ewp (x1 \<cdot>\<^sub>r x2)
 6. \<And>x. l_ewp (lang x) = rexp_ewp x \<Longrightarrow> l_ewp (lang (x\<^sup>\<star>\<^sub>r)) = rexp_ewp (x\<^sup>\<star>\<^sub>r)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l_ewp (lang x) = rexp_ewp x

goal (1 subgoal):
 1. l_ewp (lang (x\<^sup>\<star>\<^sub>r)) = rexp_ewp (x\<^sup>\<star>\<^sub>r)
[PROOF STEP]
by (simp, metis lan_salomaa_l.EWP left_near_kleene_algebra_class.star_plus_one)
[PROOF STATE]
proof (state)
this:
l_ewp (lang (x\<^sup>\<star>\<^sub>r)) = rexp_ewp (x\<^sup>\<star>\<^sub>r)

goal (5 subgoals):
 1. l_ewp (lang 0\<^sub>r) = rexp_ewp 0\<^sub>r
 2. l_ewp (lang 1\<^sub>r) = rexp_ewp 1\<^sub>r
 3. \<And>x. l_ewp (lang \<langle>x\<rangle>) = rexp_ewp \<langle>x\<rangle>
 4. \<And>x1 x2. \<lbrakk>l_ewp (lang x1) = rexp_ewp x1; l_ewp (lang x2) = rexp_ewp x2\<rbrakk> \<Longrightarrow> l_ewp (lang (x1 +\<^sub>r x2)) = rexp_ewp (x1 +\<^sub>r x2)
 5. \<And>x1 x2. \<lbrakk>l_ewp (lang x1) = rexp_ewp x1; l_ewp (lang x2) = rexp_ewp x2\<rbrakk> \<Longrightarrow> l_ewp (lang (x1 \<cdot>\<^sub>r x2)) = rexp_ewp (x1 \<cdot>\<^sub>r x2)
[PROOF STEP]
qed (simp_all add:l_ewp_def zero_set_def one_set_def one_list_def plus_set_def c_prod_def times_list_def)


[STATEMENT]
theorem regexp_ewp:
  defines P_def: "P(t) \<equiv> \<exists> t'. t \<sim> ro(t) +\<^sub>r t' \<and> ro(t') = 0\<^sub>r"
  shows "P t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. P 0\<^sub>r
 2. P 1\<^sub>r
 3. \<And>x. P \<langle>x\<rangle>
 4. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 5. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 6. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
show "P(0\<^sub>r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0\<^sub>r
[PROOF STEP]
by (simp add:P_def r_lang_def, rule_tac x="0\<^sub>r" in exI, simp)
[PROOF STATE]
proof (state)
this:
P 0\<^sub>r

goal (5 subgoals):
 1. P 1\<^sub>r
 2. \<And>x. P \<langle>x\<rangle>
 3. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 4. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 5. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. P 1\<^sub>r
 2. \<And>x. P \<langle>x\<rangle>
 3. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 4. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 5. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. P 1\<^sub>r
 2. \<And>x. P \<langle>x\<rangle>
 3. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 4. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 5. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
show "P(\<langle>a\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<langle>a\<rangle>
[PROOF STEP]
by (simp add:P_def r_lang_def, rule_tac x="\<langle>a\<rangle>" in exI, simp)
[PROOF STATE]
proof (state)
this:
P \<langle>a\<rangle>

goal (4 subgoals):
 1. P 1\<^sub>r
 2. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 3. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 4. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. P 1\<^sub>r
 2. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 3. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 4. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
show "P(1\<^sub>r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 1\<^sub>r
[PROOF STEP]
by (simp add:P_def r_lang_def, rule_tac x="0\<^sub>r" in exI, simp)
[PROOF STATE]
proof (state)
this:
P 1\<^sub>r

goal (3 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 2. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 3. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 2. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 3. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
fix t1 t2
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 2. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 3. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
assume "P(t1)" "P(t2)"
[PROOF STATE]
proof (state)
this:
P t1
P t2

goal (3 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 2. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 3. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P t1
P t2
[PROOF STEP]
obtain t1' t2'
    where "t1 \<sim> ro(t1) +\<^sub>r t1'" "ro(t1') = 0\<^sub>r"
          "t2 \<sim> ro(t2) +\<^sub>r t2'" "ro(t2') = 0\<^sub>r"
[PROOF STATE]
proof (prove)
using this:
P t1
P t2

goal (1 subgoal):
 1. (\<And>t1' t2'. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms rexp.distinct(1))
[PROOF STATE]
proof (state)
this:
t1 \<sim> ro t1 +\<^sub>r t1'
ro t1' = 0\<^sub>r
t2 \<sim> ro t2 +\<^sub>r t2'
ro t2' = 0\<^sub>r

goal (3 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 +\<^sub>r t2)
 2. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 3. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
thus "P(t1 +\<^sub>r t2)"
[PROOF STATE]
proof (prove)
using this:
t1 \<sim> ro t1 +\<^sub>r t1'
ro t1' = 0\<^sub>r
t2 \<sim> ro t2 +\<^sub>r t2'
ro t2' = 0\<^sub>r

goal (1 subgoal):
 1. P (t1 +\<^sub>r t2)
[PROOF STEP]
apply (subst P_def, transfer)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 t1' t2 t2'. \<lbrakk>lang t1 = lang (ro t1 +\<^sub>r t1'); ro t1' = 0\<^sub>r; lang t2 = lang (ro t2 +\<^sub>r t2'); ro t2' = 0\<^sub>r; lang t1 = lang (ro t1 +\<^sub>r t1'); ro t1' = 0\<^sub>r; lang t2 = lang (ro t2 +\<^sub>r t2'); ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> \<exists>t'. lang (t1 +\<^sub>r t2) = lang (ro (t1 +\<^sub>r t2) +\<^sub>r t') \<and> ro t' = 0\<^sub>r
[PROOF STEP]
apply (rule_tac x="t1' +\<^sub>r t2'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 t1' t2 t2'. \<lbrakk>lang t1 = lang (ro t1 +\<^sub>r t1'); ro t1' = 0\<^sub>r; lang t2 = lang (ro t2 +\<^sub>r t2'); ro t2' = 0\<^sub>r; lang t1 = lang (ro t1 +\<^sub>r t1'); ro t1' = 0\<^sub>r; lang t2 = lang (ro t2 +\<^sub>r t2'); ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> lang (t1 +\<^sub>r t2) = lang (ro (t1 +\<^sub>r t2) +\<^sub>r (t1' +\<^sub>r t2')) \<and> ro (t1' +\<^sub>r t2') = 0\<^sub>r
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 t1' t2 t2'. \<lbrakk>lang t1 = lang (ro t1) + lang t1'; ro t1' = 0\<^sub>r; lang t2 = lang (ro t2) + lang t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> (rexp_ewp t1 \<longrightarrow> (rexp_ewp t2 \<longrightarrow> \<not> rexp_ewp t1' \<and> \<not> rexp_ewp t2' \<and> (\<not> rexp_ewp t1' \<and> \<not> rexp_ewp t2' \<longrightarrow> 1 + lang t1' + (1 + lang t2') = 1 + (lang t1' + lang t2'))) \<and> (\<not> rexp_ewp t2 \<longrightarrow> \<not> rexp_ewp t1' \<and> \<not> rexp_ewp t2' \<and> (\<not> rexp_ewp t1' \<and> \<not> rexp_ewp t2' \<longrightarrow> 1 + lang t1' + lang t2' = 1 + (lang t1' + lang t2')))) \<and> (\<not> rexp_ewp t1 \<longrightarrow> (rexp_ewp t2 \<longrightarrow> \<not> rexp_ewp t1' \<and> \<not> rexp_ewp t2' \<and> (\<not> rexp_ewp t1' \<and> \<not> rexp_ewp t2' \<longrightarrow> lang t1' + (1 + lang t2') = 1 + (lang t1' + lang t2'))) \<and> (\<not> rexp_ewp t2 \<longrightarrow> \<not> rexp_ewp t1' \<and> \<not> rexp_ewp t2'))
[PROOF STEP]
by (metis (no_types, lifting) add.left_commute join.sup_assoc join.sup_left_idem rexp.distinct(2))
[PROOF STATE]
proof (state)
this:
P (t1 +\<^sub>r t2)

goal (2 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 2. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 2. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
fix t1 t2
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 2. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
assume "P(t1)" "P(t2)"
[PROOF STATE]
proof (state)
this:
P t1
P t2

goal (2 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 2. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P t1
P t2
[PROOF STEP]
obtain t1' t2'
    where t1: "t1 \<sim> ro(t1) +\<^sub>r t1'" "ro(t1') = 0\<^sub>r" and
          t2: "t2 \<sim> ro(t2) +\<^sub>r t2'" "ro(t2') = 0\<^sub>r"
[PROOF STATE]
proof (prove)
using this:
P t1
P t2

goal (1 subgoal):
 1. (\<And>t1' t2'. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms rexp.distinct(1))
[PROOF STATE]
proof (state)
this:
t1 \<sim> ro t1 +\<^sub>r t1'
ro t1' = 0\<^sub>r
t2 \<sim> ro t2 +\<^sub>r t2'
ro t2' = 0\<^sub>r

goal (2 subgoals):
 1. \<And>t1 t2. \<lbrakk>P t1; P t2\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
 2. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
thus "P(t1 \<cdot>\<^sub>r t2)"
[PROOF STATE]
proof (prove)
using this:
t1 \<sim> ro t1 +\<^sub>r t1'
ro t1' = 0\<^sub>r
t2 \<sim> ro t2 +\<^sub>r t2'
ro t2' = 0\<^sub>r

goal (1 subgoal):
 1. P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
let ?t' = "ro(t1) \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro(t2) +\<^sub>r t1' \<cdot>\<^sub>r t2'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
from t1 t2
[PROOF STATE]
proof (chain)
picking this:
t1 \<sim> ro t1 +\<^sub>r t1'
ro t1' = 0\<^sub>r
t2 \<sim> ro t2 +\<^sub>r t2'
ro t2' = 0\<^sub>r
[PROOF STEP]
have r1: "ro(?t') = 0\<^sub>r"
[PROOF STATE]
proof (prove)
using this:
t1 \<sim> ro t1 +\<^sub>r t1'
ro t1' = 0\<^sub>r
t2 \<sim> ro t2 +\<^sub>r t2'
ro t2' = 0\<^sub>r

goal (1 subgoal):
 1. ro (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2') = 0\<^sub>r
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
ro (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2') = 0\<^sub>r

goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
from t1 t2
[PROOF STATE]
proof (chain)
picking this:
t1 \<sim> ro t1 +\<^sub>r t1'
ro t1' = 0\<^sub>r
t2 \<sim> ro t2 +\<^sub>r t2'
ro t2' = 0\<^sub>r
[PROOF STEP]
have "t1 \<cdot>\<^sub>r t2 \<sim> (ro(t1) +\<^sub>r t1') \<cdot>\<^sub>r (ro(t2) +\<^sub>r t2')" (is "?l \<sim> ?r")
[PROOF STATE]
proof (prove)
using this:
t1 \<sim> ro t1 +\<^sub>r t1'
ro t1' = 0\<^sub>r
t2 \<sim> ro t2 +\<^sub>r t2'
ro t2' = 0\<^sub>r

goal (1 subgoal):
 1. t1 \<cdot>\<^sub>r t2 \<sim> (ro t1 +\<^sub>r t1') \<cdot>\<^sub>r (ro t2 +\<^sub>r t2')
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
t1 \<cdot>\<^sub>r t2 \<sim> (ro t1 +\<^sub>r t1') \<cdot>\<^sub>r (ro t2 +\<^sub>r t2')

goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t1 \<cdot>\<^sub>r t2 \<sim> (ro t1 +\<^sub>r t1') \<cdot>\<^sub>r (ro t2 +\<^sub>r t2')

goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
have "?r \<sim> ro(t1) \<cdot>\<^sub>r ro(t2) +\<^sub>r ro(t1) \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro(t2) +\<^sub>r t1' \<cdot>\<^sub>r t2'" (is "?l \<sim> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ro t1 +\<^sub>r t1') \<cdot>\<^sub>r (ro t2 +\<^sub>r t2') \<sim> ro t1 \<cdot>\<^sub>r ro t2 +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2'
[PROOF STEP]
apply (transfer, unfold lang.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 t1' t2 t2'. (lang (ro t1) + lang t1') \<cdot> (lang (ro t2) + lang t2') = lang (ro t1) \<cdot> lang (ro t2) + lang (ro t1) \<cdot> lang t2' + lang t1' \<cdot> lang (ro t2) + lang t1' \<cdot> lang t2'
[PROOF STEP]
apply (simp only: distrib_right' semiring_class.distrib_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 t1' t2 t2'. (lang (ro t1) + lang t1') \<cdot> lang (ro t2) + (lang (ro t1) + lang t1') \<cdot> lang t2' = lang (ro t1) \<cdot> lang (ro t2) + lang (ro t1) \<cdot> lang t2' + lang t1' \<cdot> lang (ro t2) + lang t1' \<cdot> lang t2'
[PROOF STEP]
apply (metis (opaque_lifting, no_types) join_semilattice_class.add_comm semiring_class.combine_common_factor)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(ro t1 +\<^sub>r t1') \<cdot>\<^sub>r (ro t2 +\<^sub>r t2') \<sim> ro t1 \<cdot>\<^sub>r ro t2 +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2'

goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(ro t1 +\<^sub>r t1') \<cdot>\<^sub>r (ro t2 +\<^sub>r t2') \<sim> ro t1 \<cdot>\<^sub>r ro t2 +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2'

goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
have "?r \<sim> ro(t1 \<cdot>\<^sub>r t2) +\<^sub>r ro(t1) \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro(t2) +\<^sub>r t1' \<cdot>\<^sub>r t2'" (is "?l \<sim> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ro t1 \<cdot>\<^sub>r ro t2 +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2' \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2'
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
ro t1 \<cdot>\<^sub>r ro t2 +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2' \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2'

goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ro t1 \<cdot>\<^sub>r ro t2 +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2' \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2'

goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
have "?r \<sim> ro(t1 \<cdot>\<^sub>r t2) +\<^sub>r ?t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2' \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2')
[PROOF STEP]
apply (transfer, unfold lang.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 t2 t2' t1'. lang (ro (t1 \<cdot>\<^sub>r t2)) + lang (ro t1) \<cdot> lang t2' + lang t1' \<cdot> lang (ro t2) + lang t1' \<cdot> lang t2' = lang (ro (t1 \<cdot>\<^sub>r t2)) + (lang (ro t1) \<cdot> lang t2' + lang t1' \<cdot> lang (ro t2) + lang t1' \<cdot> lang t2')
[PROOF STEP]
apply (metis (mono_tags) join_semilattice_class.add_assoc')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2' \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2')

goal (1 subgoal):
 1. \<lbrakk>t1 \<sim> ro t1 +\<^sub>r t1'; ro t1' = 0\<^sub>r; t2 \<sim> ro t2 +\<^sub>r t2'; ro t2' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
t1 \<cdot>\<^sub>r t2 \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t1 \<cdot>\<^sub>r t2 \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2')

goal (1 subgoal):
 1. P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
using r1
[PROOF STATE]
proof (prove)
using this:
t1 \<cdot>\<^sub>r t2 \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2')
ro (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2') = 0\<^sub>r

goal (1 subgoal):
 1. P (t1 \<cdot>\<^sub>r t2)
[PROOF STEP]
apply (unfold P_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<cdot>\<^sub>r t2 \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2'); ro (ro t1 \<cdot>\<^sub>r t2' +\<^sub>r t1' \<cdot>\<^sub>r ro t2 +\<^sub>r t1' \<cdot>\<^sub>r t2') = 0\<^sub>r\<rbrakk> \<Longrightarrow> \<exists>t'. t1 \<cdot>\<^sub>r t2 \<sim> ro (t1 \<cdot>\<^sub>r t2) +\<^sub>r t' \<and> ro t' = 0\<^sub>r
[PROOF STEP]
apply (rule_tac x="?t'" in exI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
P (t1 \<cdot>\<^sub>r t2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (t1 \<cdot>\<^sub>r t2)

goal (1 subgoal):
 1. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
assume assm:"P s"
[PROOF STATE]
proof (state)
this:
P s

goal (1 subgoal):
 1. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P s
[PROOF STEP]
obtain s' where r1: "s \<sim> ro(s) +\<^sub>r s'" "ro(s') = 0\<^sub>r"
[PROOF STATE]
proof (prove)
using this:
P s

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>s \<sim> ro s +\<^sub>r s'; ro s' = 0\<^sub>r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms rexp.distinct(1))
[PROOF STATE]
proof (state)
this:
s \<sim> ro s +\<^sub>r s'
ro s' = 0\<^sub>r

goal (1 subgoal):
 1. \<And>t. P t \<Longrightarrow> P (t\<^sup>\<star>\<^sub>r)
[PROOF STEP]
thus "P (s\<^sup>\<star>\<^sub>r)"
[PROOF STATE]
proof (prove)
using this:
s \<sim> ro s +\<^sub>r s'
ro s' = 0\<^sub>r

goal (1 subgoal):
 1. P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>s \<sim> ro s +\<^sub>r s'; ro s' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
let ?t' = "s' \<cdot>\<^sub>r (s')\<^sup>\<star>\<^sub>r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>s \<sim> ro s +\<^sub>r s'; ro s' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
have r2: "ro(?t') = 0\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ro (s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r) = 0\<^sub>r
[PROOF STEP]
by (metis r1(2) rexp.distinct(1) rexp_ewp.simps(5))
[PROOF STATE]
proof (state)
this:
ro (s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r) = 0\<^sub>r

goal (1 subgoal):
 1. \<lbrakk>s \<sim> ro s +\<^sub>r s'; ro s' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
from assm r1
[PROOF STATE]
proof (chain)
picking this:
P s
s \<sim> ro s +\<^sub>r s'
ro s' = 0\<^sub>r
[PROOF STEP]
have "(ro(s) +\<^sub>r s')\<^sup>\<star>\<^sub>r \<sim> (s')\<^sup>\<star>\<^sub>r" (is "?l \<sim> ?r")
[PROOF STATE]
proof (prove)
using this:
P s
s \<sim> ro s +\<^sub>r s'
ro s' = 0\<^sub>r

goal (1 subgoal):
 1. (ro s +\<^sub>r s')\<^sup>\<star>\<^sub>r \<sim> s'\<^sup>\<star>\<^sub>r
[PROOF STEP]
by (transfer, auto)
[PROOF STATE]
proof (state)
this:
(ro s +\<^sub>r s')\<^sup>\<star>\<^sub>r \<sim> s'\<^sup>\<star>\<^sub>r

goal (1 subgoal):
 1. \<lbrakk>s \<sim> ro s +\<^sub>r s'; ro s' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(ro s +\<^sub>r s')\<^sup>\<star>\<^sub>r \<sim> s'\<^sup>\<star>\<^sub>r

goal (1 subgoal):
 1. \<lbrakk>s \<sim> ro s +\<^sub>r s'; ro s' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
have "?r \<sim> 1\<^sub>r +\<^sub>r s' \<cdot>\<^sub>r (s')\<^sup>\<star>\<^sub>r" (is "?l \<sim> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s'\<^sup>\<star>\<^sub>r \<sim> 1\<^sub>r +\<^sub>r s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r
[PROOF STEP]
by (transfer, auto)
[PROOF STATE]
proof (state)
this:
s'\<^sup>\<star>\<^sub>r \<sim> 1\<^sub>r +\<^sub>r s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r

goal (1 subgoal):
 1. \<lbrakk>s \<sim> ro s +\<^sub>r s'; ro s' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
s'\<^sup>\<star>\<^sub>r \<sim> 1\<^sub>r +\<^sub>r s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r

goal (1 subgoal):
 1. \<lbrakk>s \<sim> ro s +\<^sub>r s'; ro s' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
have "?r \<sim> ro(s\<^sup>\<star>\<^sub>r) +\<^sub>r ?t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r +\<^sub>r s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r \<sim> ro (s\<^sup>\<star>\<^sub>r) +\<^sub>r s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r
[PROOF STEP]
by (metis (full_types) rexp_ewp.simps(6))
[PROOF STATE]
proof (state)
this:
1\<^sub>r +\<^sub>r s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r \<sim> ro (s\<^sup>\<star>\<^sub>r) +\<^sub>r s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r

goal (1 subgoal):
 1. \<lbrakk>s \<sim> ro s +\<^sub>r s'; ro s' = 0\<^sub>r\<rbrakk> \<Longrightarrow> P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(ro s +\<^sub>r s')\<^sup>\<star>\<^sub>r \<sim> ro (s\<^sup>\<star>\<^sub>r) +\<^sub>r s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(ro s +\<^sub>r s')\<^sup>\<star>\<^sub>r \<sim> ro (s\<^sup>\<star>\<^sub>r) +\<^sub>r s' \<cdot>\<^sub>r s'\<^sup>\<star>\<^sub>r

goal (1 subgoal):
 1. P (s\<^sup>\<star>\<^sub>r)
[PROOF STEP]
by (metis assms lang.simps(6) r1(1) r2 r_lang.abs_eq r_lang.rep_eq)
[PROOF STATE]
proof (state)
this:
P (s\<^sup>\<star>\<^sub>r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (s\<^sup>\<star>\<^sub>r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem arden_regexp_l:
  assumes "ro(y) = 0\<^sub>r" "x \<sim> y \<cdot>\<^sub>r x +\<^sub>r z"
  shows "x \<sim> y\<^sup>\<star>\<^sub>r \<cdot>\<^sub>r z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sim> y\<^sup>\<star>\<^sub>r \<cdot>\<^sub>r z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ro y = 0\<^sub>r
x \<sim> y \<cdot>\<^sub>r x +\<^sub>r z

goal (1 subgoal):
 1. x \<sim> y\<^sup>\<star>\<^sub>r \<cdot>\<^sub>r z
[PROOF STEP]
by (transfer, metis arden_l lang.simps(4) lang.simps(5) lang.simps(6) rexp.distinct(1) rexp_ewp_l_ewp)


[STATEMENT]
theorem arden_regexp_r:
  assumes "ro(y) = 0\<^sub>r" "x \<sim> x \<cdot>\<^sub>r y +\<^sub>r z"
  shows "x \<sim> z \<cdot>\<^sub>r y\<^sup>\<star>\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sim> z \<cdot>\<^sub>r y\<^sup>\<star>\<^sub>r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ro y = 0\<^sub>r
x \<sim> x \<cdot>\<^sub>r y +\<^sub>r z

goal (1 subgoal):
 1. x \<sim> z \<cdot>\<^sub>r y\<^sup>\<star>\<^sub>r
[PROOF STEP]
by transfer (metis lan_salomaa_r.Ar lang.simps(4) lang.simps(5) lang.simps(6) rexp.distinct(1) rexp_ewp_l_ewp)


[STATEMENT]
lemma PdXXX_linear:
  shows "Linear_order (Pd' d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (Pd' d)
[PROOF STEP]
using Pd_linear Pd'_d'_linear Pd'
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Linear_order (Pd d)
Linear_order (Pd' d')
\<forall>d. d \<noteq> d' \<longrightarrow> Pd' d = Pd d

goal (1 subgoal):
 1. Linear_order (Pd' d)
[PROOF STEP]
by (cases "d = d'") simp_all


[STATEMENT]
lemma PdXXX_range:
  shows "Field (Pd' d) \<subseteq> {x. Xd x = d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (Pd' d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
using Pd_range Pd'_d'_range Pd'
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
Field (Pd' d') \<subseteq> {y. Xd y = d'}
\<forall>d. d \<noteq> d' \<longrightarrow> Pd' d = Pd d

goal (1 subgoal):
 1. Field (Pd' d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
by (cases "d = d'") simp_all


[STATEMENT]
theorem Pd_above_irrelevant:
  assumes d'_Field: "dX X d' \<subseteq> Field (Pd' d')"
  assumes d'_Above: "Above (Pd' d') (dX X d') \<subseteq> Above (Pd d') (dX X d')"
  assumes "x \<in> X"
  assumes "stable_on ds X"
  shows "\<exists>y \<in> PdXXX.cop ds. (x, y) \<in> Pd' (Xd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>PdXXX.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
proof(rule PdXXX.Theorem_5[OF ccontr \<open>x \<in> X\<close>])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> PdXXX.stable_on ds X \<Longrightarrow> False
[PROOF STEP]
assume "\<not>PdXXX.stable_on ds X"
[PROOF STATE]
proof (state)
this:
\<not> PdXXX.stable_on ds X

goal (1 subgoal):
 1. \<not> PdXXX.stable_on ds X \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> PdXXX.stable_on ds X
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> PdXXX.stable_on ds X

goal (1 subgoal):
 1. False
[PROOF STEP]
proof(cases rule: PdXXX.not_stable_on_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> PdXXX.individually_rational_on ds X \<Longrightarrow> False
 2. \<not> PdXXX.stable_no_blocking_on ds X \<Longrightarrow> False
[PROOF STEP]
case not_individually_rational
[PROOF STATE]
proof (state)
this:
\<not> PdXXX.individually_rational_on ds X

goal (2 subgoals):
 1. \<not> PdXXX.individually_rational_on ds X \<Longrightarrow> False
 2. \<not> PdXXX.stable_no_blocking_on ds X \<Longrightarrow> False
[PROOF STEP]
from Pd' \<open>stable_on ds X\<close> d'_Field
[PROOF STATE]
proof (chain)
picking this:
\<forall>d. d \<noteq> d' \<longrightarrow> Pd' d = Pd d
stable_on ds X
PdXXX.dX X d' \<subseteq> Field (Pd' d')
[PROOF STEP]
have "x \<in> PdXXX.Cd (Xd x) X" if "x \<in> X" for x
[PROOF STATE]
proof (prove)
using this:
\<forall>d. d \<noteq> d' \<longrightarrow> Pd' d = Pd d
stable_on ds X
PdXXX.dX X d' \<subseteq> Field (Pd' d')

goal (1 subgoal):
 1. x \<in> PdXXX.Cd (Xd x) X
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>d. d \<noteq> d' \<longrightarrow> Pd' d = Pd d
stable_on ds X
PdXXX.dX X d' \<subseteq> Field (Pd' d')
x \<in> X

goal (1 subgoal):
 1. x \<in> PdXXX.Cd (Xd x) X
[PROOF STEP]
unfolding dX_def
[PROOF STATE]
proof (prove)
using this:
\<forall>d. d \<noteq> d' \<longrightarrow> Pd' d = Pd d
stable_on ds X
{x \<in> X. Xd x = d'} \<subseteq> Field (Pd' d')
x \<in> X

goal (1 subgoal):
 1. x \<in> PdXXX.Cd (Xd x) X
[PROOF STEP]
by (force simp: stable_on_range' stable_on_allocation PdXXX.Cd_single)
[PROOF STATE]
proof (state)
this:
?x \<in> X \<Longrightarrow> ?x \<in> PdXXX.Cd (Xd ?x) X

goal (2 subgoals):
 1. \<not> PdXXX.individually_rational_on ds X \<Longrightarrow> False
 2. \<not> PdXXX.stable_no_blocking_on ds X \<Longrightarrow> False
[PROOF STEP]
with \<open>stable_on ds X\<close> not_individually_rational
[PROOF STATE]
proof (chain)
picking this:
stable_on ds X
\<not> PdXXX.individually_rational_on ds X
?x \<in> X \<Longrightarrow> ?x \<in> PdXXX.Cd (Xd ?x) X
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
\<not> PdXXX.individually_rational_on ds X
?x \<in> X \<Longrightarrow> ?x \<in> PdXXX.Cd (Xd ?x) X

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding PdXXX.individually_rational_on_def
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
\<not> (PdXXX.CD_on ds X = X \<and> PdXXX.CH X = X)
?x \<in> X \<Longrightarrow> ?x \<in> PdXXX.Cd (Xd ?x) X

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: PdXXX.mem_CD_on_Cd stable_on_Xd dest: stable_on_CH PdXXX.CD_on_range')
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> PdXXX.stable_no_blocking_on ds X \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> PdXXX.stable_no_blocking_on ds X \<Longrightarrow> False
[PROOF STEP]
case not_no_blocking
[PROOF STATE]
proof (state)
this:
\<not> PdXXX.stable_no_blocking_on ds X

goal (1 subgoal):
 1. \<not> PdXXX.stable_no_blocking_on ds X \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> PdXXX.stable_no_blocking_on ds X
[PROOF STEP]
obtain h X'' where "PdXXX.blocking_on ds X h X''"
[PROOF STATE]
proof (prove)
using this:
\<not> PdXXX.stable_no_blocking_on ds X

goal (1 subgoal):
 1. (\<And>h X''. PdXXX.blocking_on ds X h X'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding PdXXX.stable_no_blocking_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>h X'. \<not> PdXXX.blocking_on ds X h X')

goal (1 subgoal):
 1. (\<And>h X''. PdXXX.blocking_on ds X h X'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
PdXXX.blocking_on ds X h X''

goal (1 subgoal):
 1. \<not> PdXXX.stable_no_blocking_on ds X \<Longrightarrow> False
[PROOF STEP]
have "blocking_on ds X h X''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blocking_on ds X h X''
[PROOF STEP]
proof(rule blocking_onI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. X'' \<noteq> Ch h X
 2. X'' = Ch h (X \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. X'' \<noteq> Ch h X
 2. X'' = Ch h (X \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
assume "x \<in> X''"
[PROOF STATE]
proof (state)
this:
x \<in> X''

goal (3 subgoals):
 1. X'' \<noteq> Ch h X
 2. X'' = Ch h (X \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
note Pbos = PdXXX.blocking_on_Field[OF \<open>PdXXX.blocking_on ds X h X''\<close>]
                  PdXXX.blocking_on_allocation[OF \<open>PdXXX.blocking_on ds X h X''\<close>]
                  PdXXX.blocking_on_CD_on'[OF \<open>PdXXX.blocking_on ds X h X''\<close> \<open>x \<in> X''\<close>]
[PROOF STATE]
proof (state)
this:
PdXXX.dX X'' ?d \<subseteq> Field (Pd' ?d)
inj_on Xd X''
x \<in> PdXXX.CD_on ds (X \<union> X'')

goal (3 subgoals):
 1. X'' \<noteq> Ch h X
 2. X'' = Ch h (X \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
show "x \<in> CD_on ds (X \<union> X'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
proof(cases "Xd x = d'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Xd x = d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
 2. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Xd x = d'

goal (2 subgoals):
 1. Xd x = d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
 2. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
from Pd_linear' d'_Field d'_Above \<open>x \<in> X''\<close> \<open>Xd x = d'\<close> Pbos
[PROOF STATE]
proof (chain)
picking this:
Linear_order (Pd ?d)
PdXXX.dX X d' \<subseteq> Field (Pd' d')
Above (Pd' d') (PdXXX.dX X d') \<subseteq> Above (Pd d') (PdXXX.dX X d')
x \<in> X''
Xd x = d'
PdXXX.dX X'' ?d \<subseteq> Field (Pd' ?d)
inj_on Xd X''
x \<in> PdXXX.CD_on ds (X \<union> X'')
[PROOF STEP]
have "dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))"
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd ?d)
PdXXX.dX X d' \<subseteq> Field (Pd' d')
Above (Pd' d') (PdXXX.dX X d') \<subseteq> Above (Pd d') (PdXXX.dX X d')
x \<in> X''
Xd x = d'
PdXXX.dX X'' ?d \<subseteq> Field (Pd' ?d)
inj_on Xd X''
x \<in> PdXXX.CD_on ds (X \<union> X'')

goal (1 subgoal):
 1. PdXXX.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))
[PROOF STEP]
by (force simp: PdXXX.mem_CD_on_Cd PdXXX.Cd_Above PdXXX.dX_Int_Field_Pd Above_union
                          Int_Un_distrib2 dX_singular intro: Above_Field)
[PROOF STATE]
proof (state)
this:
PdXXX.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
 2. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
PdXXX.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
 2. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
from \<open>stable_on ds X\<close>
[PROOF STATE]
proof (chain)
picking this:
stable_on ds X
[PROOF STEP]
have "dX X (Xd x) \<subseteq> Field (Pd (Xd x))"
[PROOF STATE]
proof (prove)
using this:
stable_on ds X

goal (1 subgoal):
 1. PdXXX.dX X (Xd x) \<subseteq> Field (Pd (Xd x))
[PROOF STEP]
by (force dest: dX_range' stable_on_range')
[PROOF STATE]
proof (state)
this:
PdXXX.dX X (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
 2. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
PdXXX.dX X (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
 2. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
note Pd_linear' Pd_range PdXXX_range d'_Field d'_Above \<open>x \<in> X''\<close> \<open>Xd x = d'\<close> Pbos
[PROOF STATE]
proof (state)
this:
Linear_order (Pd ?d)
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
Field (Pd' ?d) \<subseteq> {x. Xd x = ?d}
PdXXX.dX X d' \<subseteq> Field (Pd' d')
Above (Pd' d') (PdXXX.dX X d') \<subseteq> Above (Pd d') (PdXXX.dX X d')
x \<in> X''
Xd x = d'
PdXXX.dX X'' ?d \<subseteq> Field (Pd' ?d)
inj_on Xd X''
x \<in> PdXXX.CD_on ds (X \<union> X'')

goal (2 subgoals):
 1. Xd x = d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
 2. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
PdXXX.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))
PdXXX.dX X (Xd x) \<subseteq> Field (Pd (Xd x))
Linear_order (Pd ?d)
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
Field (Pd' ?d) \<subseteq> {x. Xd x = ?d}
PdXXX.dX X d' \<subseteq> Field (Pd' d')
Above (Pd' d') (PdXXX.dX X d') \<subseteq> Above (Pd d') (PdXXX.dX X d')
x \<in> X''
Xd x = d'
PdXXX.dX X'' ?d \<subseteq> Field (Pd' ?d)
inj_on Xd X''
x \<in> PdXXX.CD_on ds (X \<union> X'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
PdXXX.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))
PdXXX.dX X (Xd x) \<subseteq> Field (Pd (Xd x))
Linear_order (Pd ?d)
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
Field (Pd' ?d) \<subseteq> {x. Xd x = ?d}
PdXXX.dX X d' \<subseteq> Field (Pd' d')
Above (Pd' d') (PdXXX.dX X d') \<subseteq> Above (Pd d') (PdXXX.dX X d')
x \<in> X''
Xd x = d'
PdXXX.dX X'' ?d \<subseteq> Field (Pd' ?d)
inj_on Xd X''
x \<in> PdXXX.CD_on ds (X \<union> X'')

goal (1 subgoal):
 1. x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
by (clarsimp simp: PdXXX.mem_CD_on_Cd PdXXX.Cd_Above_dX mem_CD_on_Cd Cd_Above_dX
                             Above_union dX_union Int_Un_distrib2)
             (fastforce simp: dX_singular intro: Above_Linear_singleton)
[PROOF STATE]
proof (state)
this:
x \<in> CD_on ds (X \<union> X'')

goal (1 subgoal):
 1. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Xd x \<noteq> d'

goal (1 subgoal):
 1. Xd x \<noteq> d' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
with \<open>x \<in> PdXXX.CD_on ds (X \<union> X'')\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> PdXXX.CD_on ds (X \<union> X'')
Xd x \<noteq> d'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> PdXXX.CD_on ds (X \<union> X'')
Xd x \<noteq> d'

goal (1 subgoal):
 1. x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
by (clarsimp simp: Pd' PdXXX.mem_CD_on_Cd mem_CD_on_Cd PdXXX.Cd_greatest Cd_greatest)
[PROOF STATE]
proof (state)
this:
x \<in> CD_on ds (X \<union> X'')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> CD_on ds (X \<union> X'')

goal (2 subgoals):
 1. X'' \<noteq> Ch h X
 2. X'' = Ch h (X \<union> X'')
[PROOF STEP]
qed (use \<open>PdXXX.blocking_on ds X h X''\<close> in \<open>simp_all add: PdXXX.blocking_on_def\<close>)
[PROOF STATE]
proof (state)
this:
blocking_on ds X h X''

goal (1 subgoal):
 1. \<not> PdXXX.stable_no_blocking_on ds X \<Longrightarrow> False
[PROOF STEP]
with \<open>stable_on ds X\<close>
[PROOF STATE]
proof (chain)
picking this:
stable_on ds X
blocking_on ds X h X''
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
blocking_on ds X h X''

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: blocking_on_imp_not_stable)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Pd_singletons_for_ds_range:
  shows "Field (Pd_singletons_for_ds X ds d) \<subseteq> {x. Xd x = d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (Pd_singletons_for_ds X ds d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
using Pd_range dX_range
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
\<forall>d. dX ?X d \<subseteq> {x. Xd x = d}

goal (1 subgoal):
 1. Field (Pd_singletons_for_ds X ds d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
unfolding Pd_singletons_for_ds_def
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
\<forall>d. dX ?X d \<subseteq> {x. Xd x = d}

goal (1 subgoal):
 1. Field (override_on Pd (\<lambda>d. dX X d \<times> dX X d) ds d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
by (clarsimp simp: Field_def override_on_def) blast


[STATEMENT]
lemma Pd_singletons_for_ds_linear:
  assumes "allocation X"
  shows "Linear_order (Pd_singletons_for_ds X ds d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (Pd_singletons_for_ds X ds d)
[PROOF STEP]
unfolding Pd_singletons_for_ds_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (override_on Pd (\<lambda>d. dX X d \<times> dX X d) ds d)
[PROOF STEP]
using Pd_linear dX_linear[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Linear_order (Pd d)
Linear_order (dX X ?d \<times> dX X ?d)

goal (1 subgoal):
 1. Linear_order (override_on Pd (\<lambda>d. dX X d \<times> dX X d) ds d)
[PROOF STEP]
by (simp add: override_on_def)


[STATEMENT]
lemma Pd_singletons_for_ds_simps:
  shows "d \<in> ds \<Longrightarrow> Pd_singletons_for_ds X ds d = dX X d \<times> dX X d"
    and "d \<notin> ds \<Longrightarrow> Pd_singletons_for_ds X ds d = Pd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d \<in> ds \<Longrightarrow> Pd_singletons_for_ds X ds d = dX X d \<times> dX X d) &&& (d \<notin> ds \<Longrightarrow> Pd_singletons_for_ds X ds d = Pd d)
[PROOF STEP]
unfolding Pd_singletons_for_ds_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d \<in> ds \<Longrightarrow> override_on Pd (\<lambda>d. dX X d \<times> dX X d) ds d = dX X d \<times> dX X d) &&& (d \<notin> ds \<Longrightarrow> override_on Pd (\<lambda>d. dX X d \<times> dX X d) ds d = Pd d)
[PROOF STEP]
by simp_all


[STATEMENT]
theorem Theorem_10_fp_cop_F:
  assumes "x \<in> X"
  shows "\<exists>y \<in> Singleton_for_d.cop d ds. (x, y) \<in> Pd_singletons_for_ds X {d} (Xd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>Singleton_for_d.cop d ds. (x, y) \<in> Pd_singletons_for_ds X {d} (Xd x)
[PROOF STEP]
proof(rule Pd_above_irrelevant[where ds=ds and d'=d and X=X])
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. Linear_order (Pd_singletons_for_ds X {d} d)
 2. Field (Pd_singletons_for_ds X {d} d) \<subseteq> {y. Xd y = d}
 3. \<forall>da. da \<noteq> d \<longrightarrow> Pd_singletons_for_ds X {d} da = Pd da
 4. Singleton_for_d.dX X d \<subseteq> Field (Pd_singletons_for_ds X {d} d)
 5. Above (Pd_singletons_for_ds X {d} d) (Singleton_for_d.dX X d) \<subseteq> Above (Pd d) (Singleton_for_d.dX X d)
 6. x \<in> X
 7. stable_on ds X
[PROOF STEP]
from stable_on_allocation \<open>stable_on ds X\<close>
[PROOF STATE]
proof (chain)
picking this:
stable_on ?ds ?X \<Longrightarrow> inj_on Xd ?X
stable_on ds X
[PROOF STEP]
show "Above (Pd_singletons_for_ds X {d} d) (Singleton_for_d.dX X d) \<subseteq> Above (Pd d) (Singleton_for_d.dX X d)"
[PROOF STATE]
proof (prove)
using this:
stable_on ?ds ?X \<Longrightarrow> inj_on Xd ?X
stable_on ds X

goal (1 subgoal):
 1. Above (Pd_singletons_for_ds X {d} d) (Singleton_for_d.dX X d) \<subseteq> Above (Pd d) (Singleton_for_d.dX X d)
[PROOF STEP]
by (clarsimp simp: Above_def Pd_singletons_for_ds_simps dX_def) (metis inj_on_eq_iff stable_on_range' Pd_refl)
[PROOF STATE]
proof (state)
this:
Above (Pd_singletons_for_ds X {d} d) (Singleton_for_d.dX X d) \<subseteq> Above (Pd d) (Singleton_for_d.dX X d)

goal (6 subgoals):
 1. Linear_order (Pd_singletons_for_ds X {d} d)
 2. Field (Pd_singletons_for_ds X {d} d) \<subseteq> {y. Xd y = d}
 3. \<forall>da. da \<noteq> d \<longrightarrow> Pd_singletons_for_ds X {d} da = Pd da
 4. Singleton_for_d.dX X d \<subseteq> Field (Pd_singletons_for_ds X {d} d)
 5. x \<in> X
 6. stable_on ds X
[PROOF STEP]
qed (use stable_on_allocation \<open>stable_on ds X\<close> Pd_singletons_for_ds_linear Pd_singletons_for_ds_range assms
     in \<open>simp_all, simp_all add: Pd_singletons_for_ds_simps dX_def\<close>)


[STATEMENT]
theorem Theorem_10:
  assumes "x \<in> match (gfp_F ds)"
  shows "\<exists>y \<in> match (Singleton_for_d.gfp_F ds d ds). (x, y) \<in> Pd_singletons_for_ds (match (gfp_F ds)) {d} (Xd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>Singleton_for_d.match (Singleton_for_d.gfp_F ds d ds). (x, y) \<in> Pd_singletons_for_ds (Singleton_for_d.match (gfp_F ds)) {d} (Xd x)
[PROOF STEP]
using Theorem_10_fp_cop_F Singleton_for_d.Theorem_15_match Theorem_15_match gfp_F_stable_on assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stable_on ?ds ?X; ?x \<in> ?X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Singleton_for_d.CH (Contracts.fp_cop_F (Pd_singletons_for_ds ?X {?d}) Ch ?ds). (?x, y) \<in> Pd_singletons_for_ds ?X {?d} (Xd ?x)
Singleton_for_d.match (Singleton_for_d.gfp_F ?dsa ?d ?ds) = Singleton_for_d.cop ?dsa ?d ?ds
Singleton_for_d.match (gfp_F ?ds) = cop ?ds
stable_on ?ds (Singleton_for_d.match (gfp_F ?ds))
x \<in> Singleton_for_d.match (gfp_F ds)

goal (1 subgoal):
 1. \<exists>y\<in>Singleton_for_d.match (Singleton_for_d.gfp_F ds d ds). (x, y) \<in> Pd_singletons_for_ds (Singleton_for_d.match (gfp_F ds)) {d} (Xd x)
[PROOF STEP]
by simp


[STATEMENT]
lemma Pd'_linear:
  shows "Linear_order (Pd' d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (Pd' d)
[PROOF STEP]
using Pd_linear Pd'_d'_linear Pd'
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Linear_order (Pd d)
Linear_order (Pd' (Xd x))
\<forall>d. d \<noteq> Xd x \<longrightarrow> Pd' d = Pd d

goal (1 subgoal):
 1. Linear_order (Pd' d)
[PROOF STEP]
by (cases "d = Xd x") simp_all


[STATEMENT]
lemma Pd'_range:
  shows "Field (Pd' d) \<subseteq> {x. Xd x = d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (Pd' d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
using Pd_range Pd'_d'_range Pd'
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
Field (Pd' (Xd x)) \<subseteq> {y. Xd y = Xd x}
\<forall>d. d \<noteq> Xd x \<longrightarrow> Pd' d = Pd d

goal (1 subgoal):
 1. Field (Pd' d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
by (cases "d = Xd x") simp_all


[STATEMENT]
lemma Pd'_tax_linear:
  shows "Linear_order (Pd'_tax d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (Pd'_tax d)
[PROOF STEP]
using Pd'_linear Pd'_d'_linear Linear_order_Restr
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd' ?d)
Linear_order (Pd' (Xd x))
Linear_order ?r \<Longrightarrow> Linear_order (Restr ?r ?A)

goal (1 subgoal):
 1. Linear_order (Pd'_tax d)
[PROOF STEP]
unfolding Pd'_tax_def
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd' ?d)
Linear_order (Pd' (Xd x))
Linear_order ?r \<Longrightarrow> Linear_order (Restr ?r ?A)

goal (1 subgoal):
 1. Linear_order ((Pd'(Xd x := Restr (Pd' (Xd x)) (above (Pd' (Xd x)) x))) d)
[PROOF STEP]
by auto


[STATEMENT]
lemma Pd'_tax_Pd':
  shows "Pd'_tax d \<subseteq> Pd' d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pd'_tax d \<subseteq> Pd' d
[PROOF STEP]
unfolding Pd'_tax_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Pd'(Xd x := Restr (Pd' (Xd x)) (above (Pd' (Xd x)) x))) d \<subseteq> Pd' d
[PROOF STEP]
by simp


[STATEMENT]
lemma Pd'_tax_range:
  shows "Field (Pd'_tax d) \<subseteq> {x. Xd x = d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (Pd'_tax d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
using Pd'_range Pd'_tax_Pd'
[PROOF STATE]
proof (prove)
using this:
Field (Pd' ?d) \<subseteq> {x. Xd x = ?d}
Pd'_tax ?d \<subseteq> Pd' ?d

goal (1 subgoal):
 1. Field (Pd'_tax d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
by (meson mono_Field subset_trans)


[STATEMENT]
lemma Pd'_tax_x:
  shows "x \<in> Field (Pd'_tax (Xd x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Field (Pd'_tax (Xd x))
[PROOF STEP]
using Pd'_d'_x Pd'_d'_linear
[PROOF STATE]
proof (prove)
using this:
x \<in> Field (Pd' (Xd x))
Linear_order (Pd' (Xd x))

goal (1 subgoal):
 1. x \<in> Field (Pd'_tax (Xd x))
[PROOF STEP]
unfolding Pd'_tax_def above_def order_on_defs
[PROOF STATE]
proof (prove)
using this:
x \<in> Field (Pd' (Xd x))
((Refl (Pd' (Xd x)) \<and> trans (Pd' (Xd x))) \<and> antisym (Pd' (Xd x))) \<and> Total (Pd' (Xd x))

goal (1 subgoal):
 1. x \<in> Field ((Pd'(Xd x := Restr (Pd' (Xd x)) {b. (x, b) \<in> Pd' (Xd x)})) (Xd x))
[PROOF STEP]
by (fastforce intro: FieldI2 dest: refl_onD)


[STATEMENT]
lemma Pd'_Above:
  assumes "Y \<subseteq> above (Pd' (Xd x)) x"
  assumes "Y \<noteq> {}"
  shows "Above (Pd' d) Y \<subseteq> Above (Pd'_tax d) Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Above (Pd' d) Y \<subseteq> Above (Pd'_tax d) Y
[PROOF STEP]
using Pd'_d'_linear assms
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd' (Xd x))
Y \<subseteq> above (Pd' (Xd x)) x
Y \<noteq> {}

goal (1 subgoal):
 1. Above (Pd' d) Y \<subseteq> Above (Pd'_tax d) Y
[PROOF STEP]
unfolding Above_def Pd'_tax_def above_def order_on_defs
[PROOF STATE]
proof (prove)
using this:
((Refl (Pd' (Xd x)) \<and> trans (Pd' (Xd x))) \<and> antisym (Pd' (Xd x))) \<and> Total (Pd' (Xd x))
Y \<subseteq> {b. (x, b) \<in> Pd' (Xd x)}
Y \<noteq> {}

goal (1 subgoal):
 1. {b \<in> Field (Pd' d). \<forall>a\<in>Y. (a, b) \<in> Pd' d} \<subseteq> {b \<in> Field ((Pd'(Xd x := Restr (Pd' (Xd x)) {b. (x, b) \<in> Pd' (Xd x)})) d). \<forall>a\<in>Y. (a, b) \<in> (Pd'(Xd x := Restr (Pd' (Xd x)) {b. (x, b) \<in> Pd' (Xd x)})) d}
[PROOF STEP]
by (auto simp: Refl_Field_Restr subset_eq elim: transE)


[STATEMENT]
lemma Xd_x_ds:
  shows "Xd x \<in> ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xd x \<in> ds
[PROOF STEP]
using %invisible X stable_on_Xd x
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
\<lbrakk>stable_on ?ds ?X; ?x \<in> ?X\<rbrakk> \<Longrightarrow> Xd ?x \<in> ?ds
x \<in> X

goal (1 subgoal):
 1. Xd x \<in> ds
[PROOF STEP]
by blast


[STATEMENT]
lemma TruePref_tax_Cd_not_x:
  assumes "d \<noteq> Xd x"
  shows "TruePref_tax.Cd d = Singleton_for_d.Cd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TruePref_tax.Cd d = Singleton_for_d.Cd d
[PROOF STEP]
using assms spec[OF Pd', of d] stable_on_allocation[OF X]
[PROOF STATE]
proof (prove)
using this:
d \<noteq> Xd x
d \<noteq> Xd x \<longrightarrow> Pd' d = Pd d
inj_on Xd X

goal (1 subgoal):
 1. TruePref_tax.Cd d = Singleton_for_d.Cd d
[PROOF STEP]
unfolding TruePref_tax.Cd_def Singleton_for_d.Cd_def
[PROOF STATE]
proof (prove)
using this:
d \<noteq> Xd x
d \<noteq> Xd x \<longrightarrow> Pd' d = Pd d
inj_on Xd X

goal (1 subgoal):
 1. set_option \<circ> MaxR.MaxR_opt (Pd'_tax d) = set_option \<circ> MaxR.MaxR_opt (Pd_singletons_for_ds X {Xd x} d)
[PROOF STEP]
by (simp add: Pd'_tax_def Pd_singletons_for_ds_simps)