Theory Lyndon_Schutzenberger
theory Lyndon_Schutzenberger
imports Submonoids Periodicity_Lemma
begin
chapter ‹Lyndon-Schützenberger Equation›
section ‹The original result›
text‹The Lyndon-Schützenberger equation is the following equation:
\[
x^ay^b = z^c,
\]
in this formalization denoted as @{term "x⇧@a⋅y⇧@b = z⇧@c"}.
We formalize here a complete solution of this equation.
The main result, proved by Lyndon and Schützenberger is that the equation has periodic solutions only in free groups if $2 \leq a,b,c$
In this formalization we consider the equation in words only. Then the original result can be formulated as saying that all words
$x$, $y$ and $z$ satisfying the equality ith $2 \leq a,b,c$ pairwise commute.
The result in free groups was first proved in \cite{ LySch62}.
For words, there are several proofs to be found in the literature (for instance \cite{Lo83,Dmsi2006}).
The presented proof is the authors' proof.
In addition, we give a full parametric solution of the equation for any $a$, $b$ and $c$.
›
section "The original result"
text‹If $x^a$ or $y^b$ is sufficiently long, then the claim follows from the periodicity Lemma.›
lemma LS_per_lemma_case1:
assumes eq: "x⇧@a⋅y⇧@b = z⇧@c" and "0 < a" and "0 < b" and "❙|z❙| + ❙|x❙| - 1 ≤ ❙|x⇧@a❙|"
shows "x ⋅ y = y ⋅ x" and "x ⋅ z = z ⋅ x"
proof (rule nemp_comm)
have "x⇧@a ≤p (z⇧@c) ⋅ x⇧@a" "x ⇧@ a ≤p x ⋅ x ⇧@ a"
unfolding eq[symmetric] shifts_rev by blast+
hence "x⇧@a ≤p z ⋅ x⇧@a"
using eq pref_pow_root triv_pref by metis
from two_pers_1[OF this ‹x ⇧@ a ≤p x ⋅ x ⇧@ a› ‹❙|z❙| + ❙|x❙| - 1 ≤ ❙|x ⇧@ a❙|›, symmetric]
show "x ⋅ z = z ⋅ x".
hence "z⇧@c⋅x⇧@a = x⇧@a⋅z⇧@c"
by (simp add: comm_pows_comm)
from this[folded eq, unfolded rassoc cancel, symmetric]
have "x⇧@a ⋅ y⇧@b = y⇧@b ⋅ x⇧@a".
from this[unfolded comm_pow_roots[OF ‹0 < a› ‹0 < b›]]
show "x ⋅ y = y ⋅ x".
qed
text ‹A weaker version will be often more convenient›
lemma LS_per_lemma_case:
assumes eq: "x⇧@a⋅y⇧@b = z⇧@c" and "0 < a" and "0 < b" and "❙|z❙| + ❙|x❙| ≤ ❙|x⇧@a❙|"
shows "x ⋅ y = y ⋅ x" and "x ⋅ z = z ⋅ x"
using LS_per_lemma_case1[OF assms(1-3)] assms(4) by force+
text‹The most challenging case is when $c = 3$.›
lemma LS_core_case:
assumes
eq: "x⇧@a ⋅ y⇧@b = z⇧@c" and
"2 ≤ a" and "2 ≤ b" and "2 ≤ c" and
"c = 3" and
"b*❙|y❙| ≤ a*❙|x❙|" and "x ≠ ε" and "y ≠ ε" and
lenx: "a*❙|x❙| < ❙|z❙| + ❙|x❙|" and
leny: "b*❙|y❙| < ❙|z❙| + ❙|y❙|"
shows "x⋅y = y⋅x"
proof-
have "0 < a" and "0 < b"
using ‹2 ≤ a› ‹2 ≤ b› by auto
have "a*❙|x❙|+b*❙|y❙| = 3*❙|z❙|"
using ‹c = 3› eq lenmorph[of "x⇧@a" "y⇧@b"]
by (simp add: pow_len)
hence "3*❙|z❙| ≤ a*❙|x❙| + a*❙|x❙|"
using ‹b*❙|y❙| ≤ a*❙|x❙|› by simp
hence "3*❙|z❙| < 2*❙|z❙| + 2*❙|x❙|"
using lenx by linarith
hence "❙|z❙| + ❙|x❙| < 3 * ❙|x❙|" by simp
from less_trans[OF lenx this, unfolded mult_less_cancel2]
have "a = 2" using ‹2 ≤ a› by force
hence "❙|y❙| ≤ ❙|x❙|" using ‹b*❙|y❙| ≤ a*❙|x❙|› ‹2 ≤ b›
pow_len[of 2 x] pow_len[of b y]
mult_le_less_imp_less[of a b "❙|x❙|" "❙|y❙|"] not_le
by auto
have "x⋅x⋅y⇧@b = z⋅z⋅z" using ‹2 ≤ a› eq ‹c=3› ‹a=2›
by (simp add: numeral_2_eq_2 numeral_3_eq_3)
have "❙|z❙| < ❙|x⋅x❙|"
using ‹❙|z❙| + ❙|x❙| < 3 * ❙|x❙|› add.commute by auto
from ruler_le[THEN prefD, OF triv_pref[of z "z⋅z"] _ less_imp_le[OF this]]
obtain w where "z⋅w = x⋅x"
using prefI[of "x⋅x" "y⇧@b" "z⋅z⋅z", unfolded rassoc, OF ‹x⋅x⋅y⇧@b = z⋅z⋅z›] by fastforce
have "❙|x❙| < ❙|z❙|"
using ‹a = 2› lenx by auto
from ruler_le[THEN prefD, OF _ _ less_imp_le[OF this], of "x⋅x⋅y⇧@b", OF triv_pref, unfolded ‹x⋅x⋅y⇧@b = z⋅z⋅z›, OF triv_pref]
obtain u :: "'a list" where "x⋅u=z"
by blast
have "u ≠ ε"
using ‹❙|x❙| < ❙|z❙|› ‹x⋅u = z› by auto
have "x = u⋅w" using ‹z⋅w = x⋅x› ‹x⋅u = z› by auto
have "❙|x⋅x❙| < ❙|z⋅z❙|" by (simp add: ‹❙|x❙| < ❙|z❙|› add_less_mono)
from ruler_le[OF triv_pref[of "x⋅x" "y⇧@b", unfolded rassoc ‹x⋅x⋅y⇧@b = z⋅z⋅z›, unfolded lassoc] triv_pref, OF less_imp_le[OF this]]
have "z⋅w ≤p z⋅z"
unfolding ‹z⋅w = x⋅x›.
obtain v :: "'a list" where "w ⋅ v = x"
using lq_pref[of w x]
pref_prod_pref'[OF pref_cancel[OF ‹z⋅w ≤p z⋅z›, folded ‹x ⋅ u = z›, unfolded ‹x = u ⋅ w› rassoc], folded ‹x = u ⋅ w›] by blast
have "u⋅w⋅v ≠ ε"
by (simp add: ‹u ≠ ε›)
hence "z = w⋅v⋅u"
using ‹w ⋅ v = x› ‹x ⋅ u = z› by auto
from ‹x ⋅ x ⋅ y⇧@b = z ⋅ z ⋅ z›[unfolded this lassoc, folded ‹z ⋅ w = x ⋅ x›, unfolded this rassoc]
have "w⋅v ⋅ u⋅w ⋅ y⇧@b = w⋅v⋅u⋅w⋅v⋅u⋅w⋅v⋅u".
hence "y⇧@b = v⋅u⋅w⋅v⋅u"
using pref_cancel by auto
from period_fac_period[of v "u ⋅ w ⋅ v" u "❙|y❙|", unfolded rassoc, folded this]
have "period (u⋅w⋅v) ❙|y❙|"
using pow_per[of b y].
have "u⋅w⋅v = x ⋅v"
by (simp add: ‹x = u ⋅ w›)
have "u⋅w⋅v = u⋅ x"
by (simp add: ‹w ⋅ v = x›)
have "u⋅w⋅v <p u ⋅ (u⋅w⋅v)"
using ‹u ⋅ w ⋅ v = u ⋅ x›[unfolded ‹x = u ⋅ w›] ‹u ≠ ε› triv_pref[of "u ⋅ u ⋅ w" v]
by force
have "period (u⋅w⋅v) ❙|u❙|"
using ‹u⋅w⋅v <p u ⋅ (u⋅w⋅v)› by auto
obtain d::nat where "d=gcd ❙|y❙| ❙|u❙|"
by simp
have "❙|y❙| + ❙|u❙| ≤ ❙|u⋅w⋅v❙|" using ‹❙|y❙| ≤ ❙|x❙|› lenmorph ‹u⋅w⋅v = u⋅ x›
by simp
hence "period (u⋅w⋅v) d"
using ‹period (u ⋅ w ⋅ v) ❙|u❙|› ‹period (u ⋅ w ⋅ v) ❙|y❙|› ‹d = gcd ❙|y❙| ❙|u❙|› two_periods
by blast
have "v⋅u⋅z=y⇧@b"
by (simp add: ‹y⇧@b = v ⋅ u ⋅ w ⋅ v ⋅ u› ‹z = w ⋅ v ⋅ u›)
have "❙|u❙| = ❙|v❙|"
using ‹x = u ⋅ w› ‹w ⋅ v = x› lenmorph[of u w] lenmorph[of w v] add.commute[of "❙|u❙|" "❙|w❙|"] add_left_cancel
by simp
hence "d dvd ❙|v❙|" using gcd_nat.cobounded1[of "❙|v❙|" "❙|y❙|"] gcd.commute[of "❙|y❙|" "❙|u❙|"]
by (simp add: ‹d = gcd ❙|y❙| ❙|u❙|›)
have "d dvd ❙|u❙|"
by (simp add: ‹d = gcd ❙|y❙| ❙|u❙|›)
have "❙|z❙| + ❙|u❙| + ❙|v❙| = b*❙|y❙|"
using lenarg[OF ‹v⋅u⋅z=y⇧@b›, unfolded lenmorph pow_len] by auto
from dvd_add_left_iff[OF ‹d dvd ❙|v❙|›, of "❙|z❙|+❙|u❙|", unfolded this dvd_add_left_iff[OF ‹d dvd ❙|u❙|›, of "❙|z❙|"]]
have "d dvd ❙|z❙|"
using ‹d = gcd ❙|y❙| ❙|u❙|› dvd_mult by blast
from lenarg[OF ‹z = w ⋅ v ⋅ u›, unfolded lenmorph pow_len]
have "d dvd ❙|w❙|"
using ‹d dvd ❙|z❙|› ‹d dvd ❙|u❙|› ‹d dvd ❙|v❙|› by (simp add: dvd_add_left_iff)
hence "d dvd ❙|x❙|"
using ‹d dvd ❙|v❙|› ‹w ⋅ v = x› by force
have "x ≤p u⋅w⋅v"
by (simp add: ‹x = u ⋅ w›)
have "period x d"
using ‹period (u⋅w⋅v) d › ‹x ≤p u ⋅ w ⋅ v› period_pref_period by blast
hence "x ∈ ⟨{take d x}⟩"
using ‹d dvd ❙|x❙|› by (rule root_divisor)
hence "period u d " using ‹x = u ⋅ w› period_pref_period
using ‹period x d› ‹u ≠ ε› by blast
have " take d x = take d u" using ‹u≠ε› ‹x = u ⋅ w› pref_share_take
by (simp add: ‹d = gcd ❙|y❙| ❙|u❙|›)
from root_divisor[OF ‹period u d› ‹d dvd ❙|u❙|›, folded this]
have "u ∈ ⟨{take d x}⟩".
hence "z ∈ ⟨{take d x}⟩"
using ‹x⋅u=z› ‹x ∈ ⟨{take d x}⟩›
by blast
from comm_rootI[OF ‹u ∈ ⟨{take d x}⟩› ‹x ∈ ⟨{take d x}⟩› ]
have "y⇧@b ∈ ⟨{take d x}⟩"
using ‹u ⋅ w ⋅ v = u ⋅ x›[unfolded ‹u ⋅ x = x ⋅ u› ‹u ⋅ w ⋅ v = x ⋅ v› cancel]
‹u ∈ ⟨{take d x}⟩› ‹v ⋅ u ⋅ z = y ⇧@ b› ‹x ∈ ⟨{take d x}⟩› ‹z ∈ ⟨{take d x}⟩› hull_closed
by metis
from comm_rootI[OF ‹x ∈ ⟨{take d x}⟩› this]
show "x ⋅ y = y ⋅ x"
using comm_pow_roots[OF ‹0 < a› ‹0 < b›, of x y] comm_pow_comm by meson
qed
text‹The main proof is by induction on the length of $z$. It also uses the reverse symmetry of the equation which is
exploited by two interpretations of the locale @{term LS}. Note also that the case $|x^a| < |y^b|$ is solved by
using induction on $|z| + |y^b|$ instead of just on $|z|$.
›
lemma Lyndon_Schutzenberger':
"⟦ x⇧@a⋅y⇧@b = z⇧@c; 2 ≤ a; 2 ≤ b; 2 ≤ c ⟧
⟹ x⋅y = y⋅x"
proof (induction "❙|z❙| + b* ❙|y❙|" arbitrary: x y z a b c rule: less_induct)
case less
have "0 < a" and "0 < b"
using ‹2 ≤ a› ‹2 ≤ b› by auto
have LSrev_eq: "rev y ⇧@ b ⋅ rev x ⇧@ a = rev z ⇧@ c"
using ‹x⇧@a⋅y⇧@b = z⇧@c›
unfolding rev_append[symmetric] rev_pow[symmetric]
by blast
have leneq: "a * ❙|x❙| + b*❙|y❙| = c * ❙|z❙|"
using lenarg[OF ‹x⇧@a⋅y⇧@b = z⇧@c›] unfolding pow_len lenmorph.
show "x ⋅ y = y ⋅ x"
proof (rule nemp_comm)
assume "x ≠ ε" and "y ≠ ε" and "x ≠ y"
show "x ⋅ y = y ⋅ x"
proof (cases "❙|x ⇧@ a❙| < ❙|y ⇧@ b❙|")
assume "❙|x⇧@a❙| < ❙|y⇧@b❙|"
have "❙|rev z❙| + a* ❙|rev x❙| < ❙|z❙| + b* ❙|y❙|" using ‹❙|x⇧@a❙| < ❙|y⇧@b❙|›
by (simp add: pow_len)
from "less.hyps"[OF this LSrev_eq ‹2 ≤ b› ‹2 ≤ a› ‹2 ≤ c›, symmetric]
show "x ⋅ y = y ⋅ x"
unfolding rev_append[symmetric] rev_is_rev_conv by simp
next
assume " ¬ ❙|x⇧@a❙| < ❙|y⇧@b❙|" hence "❙|y⇧@b❙| ≤ ❙|x⇧@a❙|" by force
note minus = Suc_minus2[OF ‹2 ≤ a›] Suc_minus2[OF ‹2 ≤ b›]
consider (with_periodicity_lemma)
"❙|z❙| + ❙|x❙| ≤ ❙|x ⇧@ Suc(Suc (a-2))❙| ∨ ❙|z❙| + ❙|y❙| ≤ ❙|y ⇧@ Suc(Suc (b-2))❙|" |
(without_periodicity_lemma)
"❙|x⇧@Suc(Suc (a-2))❙| < ❙|z❙| + ❙|x❙|" and "❙|y⇧@Suc(Suc (b-2))❙| < ❙|z❙| + ❙|y❙|"
unfolding minus
using not_le_imp_less by blast
thus "x ⋅ y = y ⋅ x"
proof (cases)
case with_periodicity_lemma
have "x = ε ∨ rev y = ε ⟹ x ⋅ y = y ⋅ x"
by auto
thus "x ⋅ y = y ⋅ x"
using LS_per_lemma_case[OF ‹x⇧@a⋅y⇧@b = z⇧@c› ‹0 < a› ‹0 < b›]
LS_per_lemma_case[OF LSrev_eq ‹0 < b› ‹0 < a›] with_periodicity_lemma[unfolded minus]
unfolding length_rev rev_append[symmetric] rev_is_rev_conv rev_pow[symmetric]
by linarith
next
case without_periodicity_lemma
assume lenx: "❙|x⇧@Suc (Suc (a-2))❙| < ❙|z❙| + ❙|x❙|" and leny: "❙|y⇧@Suc (Suc (b-2))❙| < ❙|z❙| + ❙|y❙|"
have "Suc (Suc (a-2)) * ❙|x❙| + Suc (Suc (b-2))*❙|y❙| < 4 * ❙|z❙|"
using lenx leny unfolding pow_len by fastforce
hence "c < 4" using leneq unfolding minus by auto
consider (c_is_3) "c = 3" | (c_is_2) "c = 2"
using ‹c < 4› ‹2 ≤ c› by linarith
then show "x ⋅ y = y ⋅ x"
proof (cases)
case c_is_3
show "x ⋅ y = y ⋅ x"
using
LS_core_case[OF ‹x⇧@a⋅y⇧@b = z⇧@c› ‹2 ≤ a› ‹2 ≤ b› ‹2 ≤ c› ‹c = 3› ‹❙|y⇧@b❙| ≤ ❙|x⇧@a❙|›[unfolded pow_len]
_ _ lenx[unfolded pow_len minus] leny[unfolded pow_len minus]]
‹x ≠ ε› ‹y ≠ ε›
by blast
next
assume "c = 2"
hence eq2: "x⇧@a ⋅ y⇧@b = z ⋅ z"
by (simp add: ‹x⇧@a⋅y⇧@b = z⇧@c›)
from dual_order.trans le_cases[of "❙|x⇧@a❙|" "❙|z❙|" "❙|z❙| ≤ ❙|x⇧@a❙|", unfolded eq_len_iff[OF this]]
have "❙|z❙| ≤ ❙|x⇧@a❙|"
using ‹❙|y⇧@b❙| ≤ ❙|x⇧@a❙|› by blast
define a' where "a' ≡ a - 1"
have "Suc a' = a" and "1 ≤ a'"
using ‹2 ≤ a› unfolding a'_def by auto
from eq2[folded ‹Suc a' = a›, unfolded pow_Suc2 rassoc] pow_Suc2[of a' x, unfolded this, symmetric]
have eq3: "x ⇧@ a' ⋅ x ⋅ y ⇧@ b = z ⋅ z" and aa':"x ⇧@ a' ⋅ x = x ⇧@ a ".
have "❙|x⇧@a'❙| < ❙|z❙|"
using ‹Suc a' = a› lenx unfolding pow_len minus by fastforce
hence "❙|x❙| < ❙|z❙|"
using mult_le_mono[of 1 a' "❙|z❙|" "❙|x❙|", OF ‹1 ≤ a'›, THEN leD] unfolding pow_len
by linarith
obtain u w where "x⇧@a'⋅u = z" and "w ⋅ y⇧@b = z"
using eqdE[OF eq3[unfolded rassoc] less_imp_le[OF ‹❙|x⇧@a'❙| < ❙|z❙|›], of thesis]
eqdE[OF eq2[symmetric] ‹❙|z❙| ≤ ❙|x⇧@a❙|›, of thesis] by fast
have "x⇧@a'⋅x⋅y⇧@b = x⇧@a'⋅u⋅w⋅y⇧@b"
unfolding lassoc ‹x ⇧@ a' ⋅ u = z› ‹w ⋅ y⇧@b = z› aa' eq2 cancel..
hence "u⋅w=x"
by auto
hence "❙|w⋅u❙| = ❙|x❙|"
using swap_len by blast
have "w⇧@2⋅y⇧@b = (w⋅u)⇧@a"
unfolding pow_list_2 using ‹w ⋅ y ⇧@ b = z› ‹x ⇧@ a' ⋅ u = z› ‹u⋅w=x› pow_list_slide[of w a' u, unfolded ‹Suc a' = a›] by simp
from "less.hyps"[OF _ this _ ‹2 ≤ b› ‹2 ≤ a›, unfolded ‹❙|w⋅u❙| = ❙|x❙|›]
have "y⋅w = w⋅y"
using ‹❙|x❙| < ❙|z❙|› by force
have "y ⋅ z = z ⋅ y"
unfolding ‹w ⋅ y⇧@b = z›[symmetric] lassoc ‹y⋅w = w⋅y›
by (simp add: pow_comm)
hence "z⇧@c⋅y⇧@b = y⇧@b⋅z⇧@c"
by (simp add: comm_pows_comm)
from this[folded ‹x⇧@a⋅y⇧@b = z⇧@c›, unfolded lassoc]
have "x⇧@a⋅y⇧@b = y⇧@b⋅x⇧@a"
using cancel_right by blast
from this[unfolded comm_pow_roots[OF ‹0 < a› ‹0 < b›]]
show "x ⋅ y = y ⋅ x".
qed
qed
qed
qed
qed
theorem Lyndon_Schutzenberger:
assumes "x⇧@a⋅y⇧@b = z⇧@c" and "2 ≤ a" and "2 ≤ b" and "2 ≤ c"
shows "x⋅y = y⋅x" and "x⋅z = z⋅x" and "y⋅z = z⋅y"
proof-
show "x ⋅ y = y ⋅ x"
using Lyndon_Schutzenberger'[OF assms].
have "0 < c" and "0 < b"
using ‹2 ≤ c› ‹2 ≤ b› by auto
have "x ⋅ x⇧@a ⋅ y⇧@b = x⇧@a ⋅ y⇧@b ⋅ x" and "y ⋅ x⇧@a ⋅ y⇧@b = x⇧@a ⋅ y⇧@b ⋅ y"
unfolding comm_pow_comm[OF ‹x ⋅ y = y ⋅ x›[symmetric], of b]
unfolding lassoc pow_comm comm_pow_comm[OF ‹x ⋅ y = y ⋅ x›, symmetric, of a] by blast+
thus "x⋅z = z⋅x" and "y⋅z = z⋅y"
using comm_drop_exp[OF ‹0 < c›] unfolding lassoc ‹x⇧@a⋅y⇧@b = z⇧@c› by metis+
qed
hide_fact Lyndon_Schutzenberger' LS_core_case
subsection "Some alternative formulations."
lemma Lyndon_Schutzenberger_conjug: assumes "u ∼ v" and "¬ primitive (u ⋅ v)" shows "u ⋅ v = v ⋅ u"
proof-
obtain r s where "u = r ⋅ s" and "v = s ⋅ r"
using ‹u ∼ v› by blast
have "u ⋅ v ∼ r⇧@2 ⋅ s⇧@2"
using conjugI'[of "r ⋅ s ⋅ s" r] unfolding ‹u = r ⋅ s› ‹v = s ⋅ r› pow_list_2 rassoc.
hence "¬ primitive (r⇧@2 ⋅ s⇧@2)"
using ‹¬ primitive (u ⋅ v)› prim_conjug by auto
from not_prim_primroot_expE[OF this, of "r ⋅ s = s ⋅ r"]
have "r ⋅ s = s ⋅ r"
using Lyndon_Schutzenberger(1)[of 2 r 2 s, OF _ order.refl order.refl] by metis
thus "u ⋅ v = v ⋅ u"
using ‹u = r ⋅ s› ‹v = s ⋅ r› by presburger
qed
lemma Lyndon_Schutzenberger_prim: assumes "¬ primitive x" and "¬ primitive y" and "¬ primitive (x ⋅ y)"
shows "x ⋅ y = y ⋅ x"
proof (rule nemp_comm)
assume "x ≠ ε" and "y ≠ ε"
from not_prim_primroot_expE[OF ‹¬ primitive y›]
obtain m where "ρ y⇧@m = y" and "2 ≤ m".
from not_prim_primroot_expE[OF ‹¬ primitive x›]
obtain k where "ρ x⇧@k = x" and "2 ≤ k".
from not_prim_primroot_expE[OF ‹¬ primitive (x ⋅ y)›]
obtain l where "ρ(x ⋅ y)⇧@l = x ⋅ y" and "2 ≤ l".
from Lyndon_Schutzenberger(1)[of k "ρ x" m "ρ y" l "ρ (x ⋅ y)",
OF _ ‹2 ≤ k› ‹2 ≤ m› ‹2 ≤ l›]
show "x ⋅ y = y ⋅ x"
unfolding ‹ρ y⇧@m = y› ‹ρ x⇧@k = x› ‹ρ(x ⋅ y)⇧@l = x ⋅ y›
comm_primroot_conv'[of x y] by blast
qed
lemma Lyndon_Schutzenberger_rotate: assumes "x⇧@c = r ⇧@ k ⋅ u⇧@b ⋅ r ⇧@ k'"
and "2 ≤ b" and "2 ≤ c" and "0 < k" and "0 < k'"
shows "u ⋅ r = r ⋅ u"
proof(rule comm_drop_exps)
show "u⇧@b ⋅ r⇧@(k' + k) = r⇧@(k' + k) ⋅ u⇧@b"
proof(rule Lyndon_Schutzenberger_prim)
have "2 ≤ (k' + k)"
using ‹0 < k› ‹0 < k'› by simp
from pow_nemp_imprim[OF ‹2 ≤ b›] pow_nemp_imprim[OF this]
show "¬ primitive (u⇧@b)" and "¬ primitive (r ⇧@ (k' + k))"
unfolding Suc_minus2[OF ‹2 ≤ b›].
from pow_nemp_imprim[OF ‹2 ≤ c›]
have "¬ primitive (r ⇧@ k ⋅ u⇧@b ⋅ r ⇧@ k')"
unfolding assms(1)[symmetric].
from this[unfolded conjug_prim_iff[OF conjugI'[of "r ⇧@ k" "u ⇧@ b ⋅ r ⇧@ k'"]] rassoc]
show "¬ primitive (u ⇧@ b ⋅ r ⇧@ (k' + k))"
unfolding pow_add[symmetric] by force
qed
qed (use assms in force)+
section ‹Parametric solution of the equation @{term "x⇧@j⋅y⇧@k = z⇧@l"}›
subsection ‹Auxiliary lemmas›
lemma xjy_imprim_len: assumes "x ⋅ y ≠ y ⋅ x" and eq: "x⇧@j ⋅ y = z⇧@l" and "2 ≤ j" and "2 ≤ l"
shows "❙|x⇧@j❙| < ❙|y❙| + 2*❙|x❙|" and "❙|z❙| < ❙|x❙| + ❙|y❙|" and "❙|x❙| < ❙|z❙|" and "❙|x⇧@j❙| < ❙|z❙| + ❙|x❙|"
proof-
define j' where "j' ≡ j - 2"
have "0 < j" "j = Suc(Suc j')"
unfolding j'_def using ‹2 ≤ j› by force+
from LS_per_lemma_case[of _ _ 1, unfolded pow_list_1, OF eq ‹0 < j›]
show "❙|x⇧@j❙| < ❙|z❙| + ❙|x❙|"
using ‹x ⋅ y ≠ y ⋅ x› by linarith
from lenarg[OF eq, unfolded lenmorph, unfolded pow_len]
add_less_mono1[OF this, of "❙|y❙|", unfolded pow_len]
show "❙|z❙| < ❙|x❙| + ❙|y❙|"
using mult_le_mono1[OF ‹2 ≤ l›, unfolded mult_2, of "❙|z❙|"] by force
with ‹❙|x⇧@j❙| < ❙|z❙| + ❙|x❙|›
show "❙|x❙| < ❙|z❙|" and "❙|x⇧@j❙| < ❙|y❙| + 2*❙|x❙|"
unfolding ‹j = Suc (Suc j')› pow_Suc lenmorph mult_2 by linarith+
qed
lemma case_j1k1: assumes
eq: "x⋅y = z⇧@l" and
non_comm: "x ⋅ y ≠ y ⋅ x" and
l_min: "2 ≤ l"
obtains r q m n where
"x = (r⋅q)⇧@m⋅r" and
"y = q⋅ (r ⋅ q)⇧@n" and
"z = r⋅q" and
"l = m + n + 1" and "r⋅q ≠ q⋅r" and "❙|x❙| + ❙|y❙| ≥ 4"
proof-
have "0 < l" "y ≠ ε"
using l_min non_comm by force+
from split_pow[OF eq this]
obtain r q m n where
x: "x = (r ⋅ q) ⇧@ m ⋅ r" and
y: "y = (q ⋅ r)⇧@ n ⋅ q" and
z: "z = r ⋅ q" and
l: "l = m + n + 1".
from non_comm[unfolded x y]
have "r ⋅ q ≠ q ⋅ r"
unfolding shifts
unfolding lassoc pow_add[symmetric] pow_Suc[symmetric] add.commute[of m]
by force
hence "r ≠ ε" and "q ≠ ε"
by blast+
have "2 ≤ ❙|r ⋅ q❙|"
using nemp_len[OF ‹r ≠ ε›] nemp_len[OF ‹q ≠ ε›]
unfolding lenmorph by linarith
have "❙|x❙| + ❙|y❙| ≥ 4"
unfolding x y lenmorph[symmetric] shifts
unfolding pow_add[symmetric] lassoc lenmorph[of "r ⋅ q"]
mult_Suc[symmetric] pow_len Suc_eq_plus1 l[symmetric]
using mult_le_mono[OF ‹2 ≤ l› ‹2 ≤ ❙|r ⋅ q❙|›]
by presburger
from that[OF x y[unfolded shift_pow] z l ‹r ⋅ q ≠ q ⋅ r› this]
show thesis.
qed
subsection ‹@{term x} is longer›
text‹We set up a locale representing the Lyndon-Schützenberger Equation
with relaxed exponents and a length assumption breaking the symmetry.›
locale LS_len_le = binary_code x y for x y +
fixes j k l z
assumes
y_le_x: "❙|y❙| ≤ ❙|x❙|"
and eq: "x⇧@j ⋅ y⇧@k = z⇧@l"
and l_min: "2 ≤ l"
and j_min: "1 ≤ j"
and k_min: "1 ≤ k"
begin
lemma jk_small: obtains "j = 1" | "k = 1"
using Lyndon_Schutzenberger(1)[OF eq _ _ l_min]
le_neq_implies_less[OF j_min]
le_neq_implies_less[OF k_min]
non_comm
unfolding One_less_Two_le_iff
by blast
subsubsection ‹case @{term "2 ≤ j"}›
lemma case_j2k1: assumes "2 ≤ j" "k = 1"
obtains r q t where
"(r ⋅ q) ⇧@ t ⋅ r = x" and
"q ⋅ r ⋅ r ⋅ q = y" and
"(r ⋅ q) ⇧@ t ⋅ r ⋅ r ⋅ q = z" and "2 ≤ t"
"j = 2" and "l = 2" and "r⋅q ≠ q⋅r" and
"primitive x" and "primitive y"
proof-
note eq' = eq[unfolded ‹k = 1› pow_list_1]
note xjy_imprim_len[OF non_comm eq[unfolded ‹k = 1› pow_list_1] ‹2 ≤ j› l_min]
obtain j' where "j = Suc (Suc j')"
using ‹2 ≤ j› using at_least2_Suc by metis
hence "0 < j" by blast
from lenarg[OF eq', unfolded lenmorph, unfolded pow_len]
add_less_mono1[OF ‹❙|x⇧@j❙| < ❙|z❙| + ❙|x❙|›, of "❙|y❙|", unfolded pow_len]
have "l*❙|z❙| < 3*❙|z❙|"
using ‹❙|x❙| < ❙|z❙|› y_le_x by linarith
hence "l = 2"
using l_min by simp
from ‹❙|x ⇧@ j❙| < ❙|z❙| + ❙|x❙|› add_less_mono1[OF ‹❙|z❙| < ❙|x❙| + ❙|y❙|›, of "❙|x❙|"] y_le_x
have "j' * ❙|x❙| < ❙|x❙|"
unfolding ‹j = Suc (Suc j')› pow_Suc lenmorph pow_len by linarith
hence "j = 2"
using ‹j = Suc (Suc j')› by simp
note eq[ unfolded ‹k = 1› pow_list_1 ‹j = 2› ‹l = 2› pow_list_2 rassoc]
from eqd[OF this less_imp_le[OF ‹❙|x❙| < ❙|z❙|›]]
obtain p where "x ⋅ p = z" and "p ⋅ z = x ⋅ y"
by blast
from eqd[OF ‹p ⋅ z = x ⋅ y›[folded ‹x ⋅ p = z›, unfolded lassoc, symmetric]]
obtain s where "x ⋅ s = p ⋅ x" and "s ⋅ p = y"
by auto
have "p ≠ ε"
using ‹x ⋅ p = z› ‹❙|x❙| < ❙|z❙|› by fastforce
have "s ≠ ε"
using ‹p ≠ ε› ‹x ⋅ s = p ⋅ x› by force
from conjug_eqE[OF ‹x ⋅ s = p ⋅ x›[symmetric] ‹p ≠ ε›]
obtain r q t where "r ⋅ q = p" and "q ⋅ r = s" and "(r ⋅ q)⇧@t⋅r = x" and "q ≠ ε".
note ‹s ⋅ p = y›[folded ‹q ⋅ r = s› ‹r ⋅ q = p›, unfolded rassoc]
from y_le_x[folded this ‹(r ⋅ q)⇧@t⋅r = x›, unfolded lenmorph pow_len] nemp_len[OF ‹q ≠ ε›]
add_le_mono1[OF mult_le_mono1[of t 1 "❙|r❙| + ❙|q❙|", unfolded mult_1], of "❙|r❙|"]
have "2 ≤ t"
by linarith
from ‹p ⋅ z = x ⋅ y›[folded ‹q ⋅ r ⋅ r ⋅ q = y› ‹(r ⋅ q)⇧@t⋅r = x› ‹r ⋅ q = p›, symmetric]
have z: "(r ⋅ q) ⇧@ t ⋅ r ⋅ r ⋅ q = z"
by comparison
from comm_drop_exp[OF ‹0 < j›, of y x j, unfolded eq']
have "primitive y"
using Lyndon_Schutzenberger_prim[OF pow_nemp_imprim[OF ‹2 ≤j›], of y x, unfolded eq', OF _ pow_nemp_imprim[OF l_min]] non_comm by argo
hence "q ⋅ r ≠ r ⋅ q"
using ‹p ≠ ε› ‹q ⋅ r = s› ‹r ⋅ q = p› ‹s ⋅ p = y› comm_not_prim[OF ‹s ≠ ε› ‹p ≠ ε›] by argo
thm per_le_prim_iff[of x p]
have "x ≤p p ⋅ x"
unfolding ‹(r ⋅ q)⇧@t⋅r = x›[symmetric] ‹r ⋅ q = p›[symmetric]
by comparison
have "2*❙|p❙| ≤ ❙|x❙|"
unfolding ‹(r ⋅ q)⇧@t⋅r = x›[symmetric] ‹r ⋅ q = p›[symmetric] lenmorph pow_len
using mult_le_mono1[OF ‹2 ≤ t›, of "(❙|r❙| + ❙|q❙|)"] by linarith
have [symmetric]: "p ⋅ x ≠ x ⋅ p"
unfolding ‹(r ⋅ q)⇧@t⋅r = x›[symmetric] ‹r ⋅ q = p›[symmetric] lassoc pow_comm[symmetric]
unfolding rassoc cancel by fact
with per_le_prim_iff[OF ‹x ≤p p ⋅ x› ‹p ≠ ε› ‹ 2 * ❙|p❙| ≤ ❙|x❙|›]
have "primitive x"
by blast
from that[OF ‹(r ⋅ q)⇧@t⋅r = x› ‹q ⋅ r ⋅ r ⋅ q = y› z ‹2 ≤ t›
‹j = 2› ‹l = 2› ‹q⋅r ≠ r⋅q›[symmetric] ‹primitive x› ‹primitive y›]
show thesis.
qed
subsubsection ‹case @{term "j = 1"}›
lemma case_j1k2_primitive: assumes "j = 1" "2 ≤ k"
shows "primitive x"
using Lyndon_Schutzenberger_prim[OF _ pow_nemp_imprim
pow_nemp_imprim[OF l_min, of z, folded eq], OF _ ‹2 ≤ k›]
comm_pow_roots[of j k x y] k_min non_comm
unfolding ‹j = 1› pow_list_1
by linarith
lemma case_j1k2_a: assumes "j = 1" "2 ≤ k" "z ≤s y⇧@k"
obtains r q t where
"x = ((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)) ⇧@ (l - 2) ⋅
(((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 2)) ⋅ r) ⋅ q" and
"y = r ⋅ (q ⋅ r) ⇧@ t" and
"z = (q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)" and ‹0 < t› and "r⋅q ≠ q⋅r"
proof-
have "z ≠ ε"
using assms(1) bin_fst_nemp eq by force
have "0 < k" "0 < k -1"
using ‹2 ≤ k› by linarith+
have "0 < l" "0 < l - 1"
using l_min by linarith+
from LS_per_lemma_case[reversed, OF eq ‹0 < k›, unfolded ‹j = 1›]
have perlem: "❙|y⇧@k❙| < ❙|z❙| + ❙|y❙|"
using non_comm
by linarith
obtain v where "y⇧@k = v⋅z"
using ‹z ≤s y⇧@k› suffix_def by blast
have "❙|v❙| < ❙|y❙|"
using perlem[unfolded lenarg[OF ‹y⇧@k = v⋅z›] lenmorph]
by simp
have "v <p y"
using prefI[OF ‹y⇧@k = v⋅z›[symmetric]]
unfolding pow_pos[OF ‹0 < k›]
using ‹❙|v❙| < ❙|y❙|› less_or_eq_imp_le by blast
obtain u where "v⋅u = y" "u ≠ ε"
using ‹v <p y› spref_exE by blast
have "z = u⋅y⇧@(k-1)"
using ‹y⇧@k = v⋅z›[unfolded pow_pos[OF ‹0 < k›],
folded ‹v ⋅ u = y›, unfolded rassoc cancel,
unfolded ‹v ⋅ u = y›, symmetric].
note eq[unfolded pow_pos2[OF ‹0 < l›] ‹y⇧@k = v⋅z› lassoc cancel_right
‹j = 1› pow_list_1]
obtain u' where "u'⋅v = y"
proof-
have "v ≤s z⇧@(l-1)"
using ‹x ⋅ v = z ⇧@ (l - 1)› by blast
moreover have "y ≤s z⇧@(l-1)"
unfolding ‹z = u⋅y⇧@(k-1)› pow_pos2[OF ‹0 < k - 1›]
pow_pos2[OF ‹0 < l - 1›] lassoc
by blast
ultimately have "v ≤s y"
using order_less_imp_le[OF ‹❙|v❙| < ❙|y❙|›] suffix_length_suffix by blast
thus thesis
using sufD that by blast
qed
hence "u' ≠ ε"
using ‹v <p y› by force
from conjugation[OF ‹u'⋅v = y›[folded ‹v⋅u = y›] ‹u' ≠ ε›]
obtain r q t where "r ⋅ q = u'" "q ⋅ r = u" "(r ⋅ q) ⇧@ t ⋅ r = v"
by blast
have y: "y = r ⋅ (q ⋅ r) ⇧@ Suc t"
using ‹u' ⋅ v = y›[symmetric, folded ‹(r ⋅ q) ⇧@ t ⋅ r = v› ‹r ⋅ q = u'›]
unfolding rassoc pow_list_slide[symmetric].
have z: "z = (q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ Suc t) ⇧@ (k - 1)"
using ‹q ⋅ r = u› ‹z = u ⋅ y ⇧@ (k - 1)› y by blast
let ?x = "((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ Suc t) ⇧@ (k - 1)) ⇧@ (l - 2) ⋅
(((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ Suc t) ⇧@ (k - 2)) ⋅ r) ⋅ q"
have "?x ⋅ v = z ⇧@ (l - 1)"
unfolding z ‹(r ⋅ q) ⇧@ t ⋅ r = v›[symmetric] pow_pos2[OF ‹0 < k - 1›]
pow_pos2[OF ‹0 < l - 1›] diff_diff_left nat_1_add_1
by (simp only: shifts)
from ‹x ⋅ v = z ⇧@ (l - 1)›[folded this]
have x: "x = ?x"
by blast
have "z⋅y ≠ y⋅z"
using non_comm
using comm_pow_comm[of z y l, folded eq,
unfolded rassoc pow_comm, unfolded lassoc cancel_right
‹j = 1› pow_list_1]
by blast
hence "r⋅q ≠ q⋅r"
unfolding ‹q ⋅ r = u› ‹r ⋅ q = u'› ‹u'⋅ v = y›[symmetric]
‹z = u ⋅ y ⇧@ (k - 1)› pow_pos2[OF ‹0 < k›] rassoc
‹y ⇧@ k = v ⋅ z›[unfolded ‹u' ⋅ v = y›[symmetric]
‹z = u ⋅ y ⇧@ (k - 1)›, symmetric] cancel_right..
show thesis
using that[OF x y z _ ‹r⋅q ≠ q⋅r›] by blast
qed
lemma case_j1k2_b: assumes "j = 1" "2 ≤ k" "y⇧@k <s z"
obtains q where
"x = (q⋅y⇧@k)⇧@(l-1)⋅q" and
"z = q⋅y⇧@k" and
"q⋅y ≠ y⋅q"
proof-
obtain q where "z = q⋅y⇧@k" "q ≠ ε"
using ssufD[OF ‹y⇧@k <s z›]
unfolding suffix_def
by blast
have "0 < l" using l_min by linarith
have "x = (q⋅y⇧@k)⇧@(l-1)⋅q"
using eq[unfolded pow_pos2[OF ‹0 < l›] ‹j = 1› pow_list_1,
unfolded ‹z = q⋅y⇧@k› lassoc cancel_right].
have "q⋅y ≠ y⋅q"
using
comm_trans[OF _ _ ‹q ≠ ε›, of y x] conjug_pow[of y q y k, symmetric]
conjug_pow[of "q ⋅ y ⇧@ k" q "q ⋅ y ⇧@ k" "l-1"] non_comm
unfolding append_same_eq[symmetric, of ‹(q ⋅ y ⇧@ k) ⇧@ (l - 1) ⋅ q› ‹q ⋅ (q ⋅ y ⇧@ k) ⇧@ (l - 1)› q]
unfolding ‹x = (q ⋅ y ⇧@ k) ⇧@ (l - 1) ⋅ q› rassoc
by argo
show ?thesis
using ‹x = (q ⋅ y ⇧@ k) ⇧@ (l - 1) ⋅ q› ‹z = q ⋅ y ⇧@ k› ‹q⋅y ≠ y⋅q› that by blast
qed
subsection ‹Putting things together›
lemma solution_cases: obtains
"j = 2" "k = 1" |
"j = 1" "2 ≤ k" "z <s y⇧@k" |
"j = 1" "2 ≤ k" "y⇧@k <s z" |
"j = 1" "k = 1"
proof-
have "0 < l" "0 < l-1"
using l_min by linarith+
have "0 < k"
using k_min by linarith
have "0 < j"
using j_min by linarith
have "z ≠ ε"
using eq nemp_pow_nemp[of l z] bin_fst_nemp[folded pow_list_Nil_iff_Nil[OF ‹0 < j›, of x], THEN pref_nemp]
by force
have "z ≠ y⇧@k"
proof
assume "z = y⇧@k"
with eq[unfolded pow_pos2[OF ‹0 < l›], folded this, unfolded cancel_right]
have "x⇧@j ⋅ y⇧@k = y⇧@k ⋅ x⇧@j"
using pow_comm by auto
from comm_drop_exps[OF ‹0 < j› ‹0 < k› this]
show False
using non_comm by blast
qed
consider
"2 ≤ j" "k = 1" |
"j = 1" "2 ≤ k" |
"j = 1" "k = 1"
using jk_small j_min k_min le_neq_implies_less
unfolding One_less_Two_le_iff[symmetric]
by metis
moreover consider "z <s y⇧@k" | "y⇧@k <s z"
using suffix_order.less_le
triv_suf[of "y⇧@k" "x⇧@j", unfolded eq, THEN suf_prod_root,
THEN ruler_suf'] ‹z ≠ y⇧@k›
by blast
moreover consider "j = 1" | "j = 2"
using case_j2k1[of thesis] calculation(1) by blast
ultimately show ?thesis
using that
by metis
qed
theorem parametric_solutionE: obtains
r q m n where
"x = (r⋅q)⇧@m⋅r" and
"y = q⋅(r⋅q)⇧@n" and
"z = r⋅q" and
"l = m + n + 1" and "r⋅q ≠ q⋅r"
|
r q t where
"x = ((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)) ⇧@ (l - 2) ⋅
(((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 2)) ⋅ r) ⋅ q" and
"y = r ⋅ (q ⋅ r) ⇧@ t" and
"z = (q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)" and
"0 < t" and "r⋅q ≠ q⋅r"
|
q where
"x = (q⋅y⇧@k)⇧@(l-1)⋅q" and
"z = q⋅y⇧@k" and
"q⋅y ≠ y⋅q"
|
r q t where
"x = (r ⋅ q) ⇧@ t ⋅ r" and
"y = q ⋅ r ⋅ r ⋅ q" and
"z = (r ⋅ q) ⇧@ t ⋅ r ⋅ r ⋅ q" and
"j = 2" and "l = 2" and "2 ≤ t" and "r⋅q ≠ q⋅r" and
"primitive x" and "primitive y"
proof-
show ?thesis
using solution_cases
proof(cases)
case 1
from case_j2k1[OF _ ‹k = 1›, of thesis] ‹j = 2›
show ?thesis
using that(4) by blast
next
case 2
from case_j1k2_a[OF this(1-2) ssufD1[OF this(3)], of thesis]
show thesis
using that(2)
by blast
next
case 3
from case_j1k2_b[OF this, of thesis]
show ?thesis
using that(3) by blast
next
case 4
from case_j1k1[OF eq[unfolded ‹k = 1› ‹j = 1› pow_list_1] non_comm l_min, of thesis]
show thesis
using that(1).
qed
qed
end
text ‹Using the solution from locale @{term LS_len_le},
the following theorem gives the full characterization of the equation in question:
$$ x^iy^j = z^\ell $$
›
theorem LS_parametric_solution:
assumes y_le_x: "❙|y❙| ≤ ❙|x❙|"
and j_min: "1 ≤ j" and k_min: "1 ≤ k" and l_min: "2 ≤ l"
shows
"x⇧@j ⋅ y⇧@k = z⇧@l
⟷
(∃r m n t.
x = r⇧@m ∧ y = r⇧@n ∧ z = r⇧@t ∧ m*j+n*k=t*l)
∨ (j = 1 ∧ k = 1) ∧
(∃r q m n.
x = (r⋅q)⇧@m⋅r ∧ y = q⋅(r⋅q)⇧@n ∧ z = r⋅q ∧ m + n + 1 = l ∧ r⋅q ≠ q⋅r)
∨ (j = 1 ∧ 2 ≤ k) ∧
(∃r q.
x = (q⋅r⇧@k)⇧@(l-1)⋅q ∧ y = r ∧ z = q⋅r⇧@k ∧ r⋅q ≠ q⋅r)
∨ (j = 1 ∧ 2 ≤ k) ∧
(∃r q t. 0 < t ∧
x = ((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)) ⇧@ (l - 2)⋅(((q ⋅ r) ⋅
(r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 2)) ⋅ r) ⋅ q
∧ y = r ⋅ (q ⋅ r) ⇧@ t
∧ z = (q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)
∧ r⋅q ≠ q⋅r)
∨ (j = 2 ∧ k = 1 ∧ l = 2) ∧
(∃r q t. 2 ≤ t ∧
x = (r ⋅ q) ⇧@ t ⋅ r ∧ y = q ⋅ r ⋅ r ⋅ q
∧ z = (r ⋅ q) ⇧@ t ⋅ r ⋅ r ⋅ q ∧ r⋅q ≠ q⋅r )
"
(is "?eq =
(?sol_per ∨ (?cond_j1k1 ∧ ?sol_j1k1) ∨
(?cond_j1k2 ∧ ?sol_j1k2_b) ∨
(?cond_j1k2 ∧ ?sol_j1k2_a) ∨
(?cond_j2k1l2 ∧ ?sol_j2k1l2))")
proof(rule iffI)
assume eq: "x ⇧@ j ⋅ y ⇧@ k = z ⇧@ l"
show
"(?sol_per ∨ (?cond_j1k1 ∧ ?sol_j1k1) ∨
(?cond_j1k2 ∧ ?sol_j1k2_b) ∨
(?cond_j1k2 ∧ ?sol_j1k2_a) ∨
(?cond_j2k1l2 ∧ ?sol_j2k1l2))"
proof(cases)
assume "x⋅y = y⋅x"
from comm_primrootE'[OF this]
obtain r m n where "x = r ⇧@ m" "y = r ⇧@ n" "primitive r".
note eqs = eq[unfolded this, folded pow_mult, folded pow_add[of "m*j" "n*k" r ], symmetric]
obtain t where "z = r ⇧@ t"
using l_min pow_list_comm_comm[OF _ eqs,
THEN prim_comm_exp[OF ‹primitive r›]]
by auto
from eqs[unfolded this, folded pow_mult, symmetric]
have "m * j + n * k = t * l"
unfolding prim_nemp[OF ‹primitive r›, THEN eq_pow_exp].
hence ?sol_per
using ‹x = r ⇧@ m› ‹y = r ⇧@ n› ‹z = r ⇧@ t› by blast
thus ?thesis
by blast
next
assume "x⋅y ≠ y⋅x"
interpret LS_len_le x y j k l z
using ‹x ⇧@ j ⋅ y ⇧@ k = z ⇧@ l› ‹x⋅y ≠ y⋅x› j_min k_min l_min y_le_x
by(unfold_locales)
show ?thesis
using solution_cases
proof(cases)
case 1
from case_j2k1[OF less_or_eq_imp_le[of 2 j] ‹k = 1›, OF disjI2, OF ‹j = 2›[symmetric], of "?sol_j2k1l2 ∧ l = 2"]
have "?sol_j2k1l2" and "l = 2"
by auto
thus ?thesis
using ‹k = 1› ‹j = 2› by blast
next
case 2
have "?sol_j1k2_a"
using case_j1k2_a[OF ‹j = 1› ‹2 ≤ k› ssufD1[OF ‹z <s y ⇧@ k›], of ?sol_j1k2_a]
unfolding Suc_eq_plus1
by blast
thus ?thesis
using ‹j = 1› ‹2 ≤ k› by blast
next
case 3
with case_j1k2_b[OF this, of "?sol_j1k2_b"]
have "?sol_j1k2_b" by metis
thus ?thesis
using ‹j = 1› ‹2 ≤ k› by blast
next
case 4
with case_j1k1[OF eq[unfolded ‹k = 1› ‹j = 1› pow_list_1] non_comm l_min, of ?sol_j1k1]
have"?sol_j1k1"
unfolding Suc_eq_plus1 shift_pow
by blast
thus ?thesis
using ‹j = 1› ‹k = 1› by blast
qed
qed
next
have "l ≠ 0" "l - 1 ≠ 0"
using l_min by auto
have "k ≠ 0" using k_min by auto
have "j ≠ 0" using j_min by auto
assume "(?sol_per ∨ (?cond_j1k1 ∧ ?sol_j1k1) ∨
(?cond_j1k2 ∧ ?sol_j1k2_b) ∨
(?cond_j1k2 ∧ ?sol_j1k2_a) ∨
(?cond_j2k1l2 ∧ ?sol_j2k1l2))"
then show ?eq
proof(elim disjE conjE exE)
fix r m n t
assume sol: "x = r ⇧@ m" "y = r ⇧@ n" "z = r ⇧@ t"
and "m * j + n * k = t * l"
show ?thesis
unfolding sol
unfolding pow_mult[symmetric] pow_add[symmetric]
unfolding ‹m * j + n * k = t * l›..
next
fix r q m n
assume "j = 1" "k = 1" and sol: "x = (r⋅q)⇧@m⋅r"
"y = q⋅(r⋅q)⇧@n" "z = r⋅q"
and "m + n + 1 = l"
hence "Suc (m+n) = l"
by simp
show ?thesis
unfolding sol
unfolding ‹j = 1› ‹k = 1› ‹Suc (m + n) = l›[symmetric] pow_list_1
unfolding lassoc pow_Suc pow_add
unfolding pow_comm[of m, symmetric] lassoc..
next
fix r q
assume "j = 1" "2 ≤ k" and sol: "x = (q ⋅ r ⇧@ k) ⇧@ (l - 1) ⋅ q" "y = r" "z = q ⋅ r ⇧@ k"
have "0 < l"
using ‹2 ≤ l› by force
show ?thesis
unfolding sol ‹j = 1› pow_list_1
unfolding pow_pos2[OF ‹0 < l›] rassoc..
next
fix r q t
assume "j = 1" "2 ≤ k" and sol:
"x =
((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)) ⇧@ (l - 2) ⋅
(((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 2)) ⋅ r) ⋅ q"
"y = r ⋅ (q ⋅ r) ⇧@ t"
"z = (q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)"
"0 < t"
obtain k' where "Suc (Suc k') = k" using Suc_minus2[OF ‹2 ≤ k›] by blast
hence k1: "k - 1 = Suc k'" and k2: "k - 2 = k'" and k: "k = k'+ 2" by fastforce+
obtain l' where "Suc (Suc l') = l" using Suc_minus2[OF ‹2 ≤ l›] by blast
hence l2: "l - 2 = l'" and l: "l = l' + 2" by fastforce+
show "x ⇧@ j ⋅ y ⇧@ k = z ⇧@ l"
unfolding sol ‹j = 1› k1 k2 l2 unfolding k l by comparison
next
fix r q t
assume "j = 2" "k = 1" "l = 2" and sol:
"x = (r ⋅ q) ⇧@ t ⋅ r"
"y = q ⋅ r ⋅ r ⋅ q" "z = (r ⋅ q) ⇧@ t ⋅ r ⋅ r ⋅ q"
"2 ≤ t"
show "x ⇧@ j ⋅ y ⇧@ k = z ⇧@ l"
unfolding ‹j = 2› ‹k = 1› ‹l = 2› sol pow_list_1 pow_list_2
by comparison
qed
qed
subsection ‹Uniqueness of the imprimitivity witness›
text‹In this section, we show that given a binary code @{term "{x,y}"} and
two imprimitive words @{term "x⇧@j⋅y⇧@k"} and @{term "x⇧@j'⋅y⇧@k'"} is possible
only if the two words are equals, that is, if @{term "j=j'"} and @{term "k=k'"}.›
lemma LS_unique_same: assumes "x ⋅ y ≠ y ⋅ x"
and "0 < j" and "0 < k" and "¬ primitive(x⇧@j⋅y⇧@k)"
and "0 < k'" and "¬ primitive(x⇧@j⋅y⇧@k')"
shows "k = k'"
proof(rule ccontr)
assume "k ≠ k'"
define ka where "ka = (if k < k' then k else k')"
define ka' where "ka' = (if k < k' then k' else k)"
have "ka < ka'" and "ka ≠ ka'"
unfolding ka_def ka'_def using ‹k ≠ k'› by auto
then obtain dif where [symmetric]: "ka + dif = ka'" and "dif ≠ 0"
using less_imp_add_positive by blast
have "ka ≠ 0" and "ka' ≠ 0" and ‹j ≠ 0›
unfolding ka_def ka'_def using ‹0 < k› ‹0 < k'› ‹0 < j› by force+
have "¬ primitive(x⇧@j⋅y⇧@ka)" "¬ primitive(x⇧@j⋅y⇧@ka')"
unfolding ka_def ka'_def using assms(4) assms(6) by presburger+
have "x⇧@j⋅y⇧@ka' = x⇧@j⋅y⇧@ka⋅y⇧@dif"
unfolding pow_add[symmetric] ‹ka' = ka + dif›..
consider "dif = 1" | "2 ≤ dif"
using ‹ka < ka'› ‹ka' = ka + dif› by fastforce
hence "x ⋅ y = y ⋅ x"
proof(cases)
assume "dif = 1"
define u where "u = x⇧@j⋅y⇧@(ka - 1)"
have "¬ primitive (u ⋅ y)"
unfolding u_def rassoc pow_Suc2[symmetric] Suc_minus[OF ‹ka ≠ 0›] by fact
have "¬ primitive (u ⋅ y ⋅ y)"
unfolding u_def rassoc using ‹¬ primitive(x⇧@j⋅y⇧@ka')›[unfolded ‹x⇧@j⋅y⇧@ka' = x⇧@j⋅y⇧@ka⋅y⇧@dif› ‹dif = 1› pow_list_1]
unfolding pow_Suc2[of "ka - 1" y, unfolded Suc_minus[OF ‹ka ≠ 0›]] rassoc.
from imprim_ext_suf_comm[OF ‹¬ primitive (u ⋅ y)› ‹¬ primitive (u ⋅ y ⋅ y)›]
have "(x ⇧@ j ⋅ y ⇧@ (ka - 1)) ⋅ y = y ⋅ x ⇧@ j ⋅ y ⇧@ (ka - 1)"
unfolding u_def.
thus "x ⋅ y = y ⋅ x"
using ‹j ≠ 0› by mismatch
next
assume "2 ≤ dif"
hence "¬ primitive (y⇧@dif)"..
from Lyndon_Schutzenberger_prim[OF ‹¬ primitive (x ⇧@ j ⋅ y ⇧@ ka)› this ‹¬ primitive (x ⇧@ j ⋅ y ⇧@ ka')›[unfolded ‹x ⇧@ j ⋅ y ⇧@ ka' = x ⇧@ j ⋅ y ⇧@ ka⋅ y⇧@dif› lassoc]]
show "x ⋅ y = y ⋅ x"
using ‹dif ≠ 0› ‹j ≠ 0› by mismatch
qed
thus False
using ‹x ⋅ y ≠ y ⋅ x› by blast
qed
lemma LS_unique_distinct_le: assumes "x ⋅ y ≠ y ⋅ x"
and "2 ≤ j" and "¬ primitive(x⇧@j⋅y)"
and "2 ≤ k" and "¬ primitive(x⋅y⇧@k)"
and "❙|y❙| ≤ ❙|x❙|"
shows False
proof-
have "0 < k"
using ‹2 ≤ k› by linarith
obtain l z where [symmetric]:"z⇧@l = x⇧@j⋅y" and "2 ≤ l"
using not_prim_primroot_expE[OF ‹¬ primitive(x⇧@j⋅y)›].
have "x⇧@j⋅y⇧@1 = z⇧@l"
by (simp add: ‹x ⇧@ j ⋅ y = z ⇧@ l›)
interpret eq1: LS_len_le x y j 1 l z
using ‹x ⋅ y ≠ y ⋅ x› ‹❙|y❙| ≤ ❙|x❙|› ‹x⇧@j⋅y⇧@1 = z⇧@l› ‹2 ≤ l› ‹2 ≤ j›
by(unfold_locales) linarith+
from eq1.case_j2k1[OF ‹2 ≤ j› refl]
obtain r q t where
x[symmetric]: "(r ⋅ q) ⇧@ t ⋅ r = x" and
y[symmetric]: "q ⋅ r ⋅ r ⋅ q = y" and
z[symmetric]: "(r ⋅ q) ⇧@ t ⋅ r ⋅ r ⋅ q = z" and
"2 ≤ t" and "j = 2" and "l = 2" and "r⋅q ≠ q⋅r" and
"primitive x" and "primitive y".
have "q⋅r ≠ ε" "r⋅q ≠ ε"
using eq1.bin_snd_nemp y by fastforce+
obtain z' l' where "x⋅y⇧@k = z'⇧@l'" "2 ≤ l'"
using not_prim_primroot_expE[OF ‹¬ primitive (x ⋅ y ⇧@ k)›] by metis
from ‹x⋅y⇧@k = z'⇧@l'›[unfolded x y, unfolded rassoc, symmetric]
have z': "z' ⇧@ l' = (r ⋅ q) ⇧@ t ⋅ r ⋅ (q ⋅ r ⋅ r ⋅ q) ⇧@ k".
have "0 < l'" and "0 < l' - 1"
using ‹2 ≤ l'› by auto
have "r ⋅ q ⋅ r ⋅ q ≤p x"
using pref_extD[of "r⋅q⋅r⋅q" "(r ⋅ q) ⇧@ (t - 2) ⋅ r"]
unfolding x[folded pop_pow[OF ‹2 ≤ t›], unfolded pow_list_2] rassoc by blast
have per1: "x ⋅ q ⋅ r ≤p (r ⋅ q) ⋅ x ⋅ q ⋅ r"
unfolding x by comparison
have per2: "x ⋅ q ⋅ r ≤p z' ⋅ x ⋅ q ⋅ r"
by (rule pref_pow_root[of _ l'],
unfold ‹x⋅y⇧@k = z'⇧@l'›[unfolded y pow_pos[OF ‹0 < k›], symmetric])
comparison
have "(r ⋅ q) ⋅ z' ≠ z' ⋅ (r ⋅ q)"
proof
assume "(r ⋅ q) ⋅ z' = z' ⋅ (r ⋅ q)"
hence "(r ⋅ q) ⋅ z'⇧@l' = z'⇧@l' ⋅ r ⋅ q"
by (simp add: comm_pow_comm)
from this[unfolded z']
have "r ⋅ q = q ⋅ r"
using ‹0 < k› by mismatch
thus False
using ‹r ⋅ q ≠ q ⋅ r› by presburger
qed
with two_pers[OF per1 per2]
have "❙|x❙| ≤ ❙|z'❙|"
unfolding lenmorph by linarith
from eqdE[OF ‹x⋅y⇧@k = z'⇧@l'›[unfolded pow_pos[OF ‹0 < l'›]
pow_pos2[OF ‹0 < l'-1›]] ‹❙|x❙| ≤ ❙|z'❙|› ]
obtain w where "x ⋅ w = z'" "w ⋅ z' ⇧@ (l' - 1 - 1) ⋅ z' = y ⇧@ k".
from this(1) this(2)[unfolded lassoc]
have "x ≤f y⇧@k"
by blast
hence "r⋅q⋅r⋅q ≤f (q⋅r⋅r⋅q)⇧@k"
unfolding y
using pref_fac[OF ‹r ⋅ q ⋅ r ⋅ q ≤p x›] by blast
have "❙|r ⋅ q ⋅ r ⋅ q❙| = ❙|q ⋅ r ⋅ r ⋅ q❙|"
by simp
from xyxy_conj_yxxy[OF fac_pow_len_conjug[OF this ‹r⋅q⋅r⋅q ≤f (q⋅r⋅r⋅q)⇧@k›, symmetric]]
have "r ⋅ q = q ⋅ r".
thus False
using ‹r ⋅ q ≠ q ⋅ r› by blast
qed
lemma LS_unique_distinct: assumes "x ⋅ y ≠ y ⋅ x"
and "2 ≤ j" and "¬ primitive(x⇧@j⋅y)"
and "2 ≤ k" and "¬ primitive(x⋅y⇧@k)"
shows False
using LS_unique_distinct_le[OF assms] LS_unique_distinct_le[reversed, OF assms(1,4-5,2-3)] by fastforce
lemma LS_unique': assumes "x ⋅ y ≠ y ⋅ x"
and "0 < j" and "0 < k" and "¬ primitive(x⇧@j⋅y⇧@k)"
and "0 < j'" and "0 < k'" and "¬ primitive(x⇧@j'⋅y⇧@k')"
shows "k = k'"
proof-
have "j = 1 ∨ k = 1"
using Lyndon_Schutzenberger_prim[OF pow_non_prim pow_non_prim,
OF _ _ ‹¬ primitive (x ⇧@ j ⋅ y ⇧@ k)›]
comm_drop_exps[OF ‹0 < j› ‹0 < k›] ‹x ⋅ y ≠ y ⋅ x› by blast
have "j' = 1 ∨ k' = 1"
using Lyndon_Schutzenberger_prim[OF pow_non_prim pow_non_prim,
OF _ _ ‹¬ primitive (x ⇧@ j' ⋅ y ⇧@ k')›]
comm_drop_exps[OF ‹0 < j'› ‹0 < k'›] ‹x ⋅ y ≠ y ⋅ x› by blast
show "k = k'"
proof (cases "j = j'")
assume "j = j'"
from LS_unique_same[OF assms(1-4,6,7)[folded this]]
show "k = k'".
next
assume "j ≠ j'"
show "k = k'"
proof(rule ccontr, cases "j = 1")
assume "k ≠ k'" and "j = 1"
hence "2 ≤ j'" and "k' = 1" and "2 ≤ k"
using ‹j ≠ j'› ‹0 < j'› ‹k ≠ k'› ‹0 < k› ‹j' = 1 ∨ k' = 1› by auto
from LS_unique_distinct[OF ‹x ⋅ y ≠ y ⋅ x› ‹2 ≤ j'› _ ‹2 ≤ k›]
show False
using ‹¬ primitive(x⇧@j'⋅y⇧@k')›[unfolded ‹k'=1› pow_list_1] ‹¬ primitive(x⇧@j⋅y⇧@k)›[unfolded ‹j=1› pow_list_1]
by blast
next
assume "k ≠ k'" and "j ≠ 1"
hence "2 ≤ j" and "k = 1" and "2 ≤ k'" and "j' = 1"
using ‹0 < j› ‹j = 1 ∨ k = 1› ‹0 < k'› ‹j' = 1 ∨ k' = 1› by auto
from LS_unique_distinct[OF ‹x ⋅ y ≠ y ⋅ x› ‹2 ≤ j› _ ‹2 ≤ k'›]
show False
using ‹¬ primitive(x⇧@j'⋅y⇧@k')›[unfolded ‹j'=1› pow_list_1] ‹¬ primitive(x⇧@j⋅y⇧@k)›[unfolded ‹k=1› pow_list_1]
by blast
qed
qed
qed
lemma LS_unique: assumes "x ⋅ y ≠ y ⋅ x"
and "0 < j" and "0 < k" and "¬ primitive(x⇧@j⋅y⇧@k)"
and "0 < j'" and "0 < k'" and "¬ primitive(x⇧@j'⋅y⇧@k')"
shows "j = j'" and "k = k'"
using LS_unique'[OF ‹x ⋅ y ≠ y ⋅ x›
‹0 < j› ‹0 < k› ‹¬ primitive (x ⇧@ j ⋅ y ⇧@ k)›
‹0 < j'› ‹0 < k'› ‹¬ primitive (x ⇧@ j'⋅ y ⇧@ k')›]
LS_unique'[reversed, OF ‹x ⋅ y ≠ y ⋅ x›
‹0 < k› ‹0 < j› ‹¬ primitive (x ⇧@ j ⋅ y ⇧@ k)›
‹0 < k'› ‹0 < j'› ‹¬ primitive (x ⇧@ j'⋅ y ⇧@ k')›]
by blast+
section "The bound on the exponent in Lyndon-Schützenberger equation"
lemma (in LS_len_le) case_j1k2_exp_le:
assumes "j = 1" "2 ≤ k"
shows "k*❙|y❙|+ 4 ≤ ❙|x❙|+2*❙|y❙|"
proof-
have "x ⋅ y ⇧@ k = z ⇧@ l" and "❙|y❙| ≠ 0" and "0 < l"
using eq[unfolded ‹j = 1› cow_simps] nemp_len[OF bin_snd_nemp] l_min
by linarith+
consider "y ⇧@ k <s z" | "z ≤s y⇧@k"
using ruler_eq'[reversed,
OF ‹x ⋅ y⇧@k = z⇧@l›[symmetric, unfolded pow_pos2[OF ‹0 < l›]]] by blast
thus ?thesis
proof(cases)
assume "y⇧@k <s z"
from case_j1k2_b[OF assms this]
obtain q where
x: "x = (q ⋅ y ⇧@ k) ⇧@ (l - 1) ⋅ q" and
"z = q ⋅ y ⇧@ k" and
"q ⋅ y ≠ y ⋅ q".
have "1 ≤ ❙|q❙|"
using nemp_le_len[of q] ‹q ⋅ y ≠ y ⋅ q› by blast
have "❙|y❙| ≥ 1"
using bin_snd_nemp nemp_le_len by blast
have lle: "x ≤ (l-1)*x" for x
using l_min
by (simp add: quotient_smaller)
have "❙|x❙| ≥ k*❙|y❙| + 2"
unfolding x lenmorph pow_len
using le_trans[OF _ lle, of "k * ❙|y❙| + 1" "❙|q❙| + k * ❙|y❙|", THEN add_le_mono[OF ‹1 ≤ ❙|q❙|›]]
unfolding add.commute[of "❙|q❙|"]
using ‹1 ≤ ❙|q❙|› by auto
thus ?thesis
using ‹❙|y❙| ≥ 1› by linarith
next
assume "z ≤s y ⇧@ k "
from case_j1k2_a[OF assms this]
obtain q r t where
x: "x = ((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)) ⇧@ (l - 2) ⋅ (((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 2)) ⋅ r) ⋅ q" and
"y = r ⋅ (q ⋅ r) ⇧@ t" and
"z = (q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 1)" and
"0 < t" and "r ⋅ q ≠ q ⋅ r".
have "q ≠ ε" "r ≠ ε"
using ‹r ⋅ q ≠ q ⋅ r› by blast+
hence "❙|q❙| ≥ 1" "❙|r❙| ≥ 1"
using nemp_le_len by blast+
hence "❙|q⋅r❙| + ❙|r❙| + ❙|q❙| ≥ 4"
by simp
have "❙|x❙| ≥ ❙|(((q ⋅ r) ⋅ (r ⋅ (q ⋅ r) ⇧@ t) ⇧@ (k - 2)) ⋅ r) ⋅ q❙|"
using x suf_len' by blast
hence "❙|x❙| ≥ ❙|q⋅r❙| + (k-2)*❙|y❙| + ❙|r❙| + ❙|q❙|"
unfolding ‹y = r ⋅ (q ⋅ r) ⇧@ t›[symmetric]
by (simp add: pow_len)
hence "❙|x❙| ≥ (k-2)*❙|y❙| + 4"
using ‹4 ≤ ❙|q ⋅ r❙| + ❙|r❙| + ❙|q❙|› by linarith
thus ?thesis
unfolding add.commute[of "❙|x❙|"]
unfolding nat_le_add_iff1[OF ‹2 ≤ k›].
qed
qed
lemma (in LS_len_le) case_j2k1_exp_le:
assumes "2 ≤ j" "k = 1"
shows "j*❙|x❙| + 4 ≤ ❙|y❙| + 2*❙|x❙|"
proof-
from case_j2k1[OF assms]
obtain r q t where
"(r ⋅ q) ⇧@ t ⋅ r = x" and
"q ⋅ r ⋅ r ⋅ q = y" and
"(r ⋅ q) ⇧@ t ⋅ r ⋅ r ⋅ q = z" and
‹2 ≤ t› and "j = 2" and "l = 2" and
"r ⋅ q ≠ q ⋅ r" and
"primitive x" and
"primitive y".
have "❙|r❙| ≥ 1" "❙|q❙| ≥ 1"
using ‹r ⋅ q ≠ q ⋅ r› nemp_le_len by blast+
hence "❙|y❙| ≥ 4"
unfolding ‹q ⋅ r ⋅ r ⋅ q = y›[symmetric] lenmorph
by linarith
thus ?thesis
by (simp add: ‹j = 2›)
qed
theorem LS_exp_le_one:
assumes eq: "x ⋅ y ⇧@ k = z ⇧@ l"
and "2 ≤ l"
and "x ⋅ y ≠ y ⋅ x"
and "1 ≤ k"
shows "k*❙|y❙| + 4 ≤ ❙|x❙|+2*❙|y❙|"
proof-
have "x ≠ ε" "y ≠ ε" "x ≠ y" "❙|y❙| ≠ 0" "z ≠ ε"
using ‹x ⋅ y ≠ y ⋅ x› ‹x ⋅ y ⇧@ k = z ⇧@ l› by fastforce+
have "l ≠ 0" ‹1 ≤ l-1›
using ‹2 ≤ l› by force+
consider "k = 1" | "k ≥ 2"
using ‹1 ≤ k› by linarith
then show ?thesis
proof(cases)
assume "k=1"
have "4 ≤ ❙|x❙| + ❙|y❙|"
using case_j1k1[OF eq[unfolded ‹k = 1› pow_list_1] ‹x ⋅ y ≠ y ⋅ x› ‹2 ≤ l›]
by blast
thus ?thesis
unfolding ‹k = 1› by force
next
assume "k ≥ 2"
show ?thesis
proof(rule le_cases)
assume "❙|y❙| ≤ ❙|x❙|"
then interpret LS_len_le x y 1 k l z
using assms by unfold_locales (blast, blast, force, blast+)
from case_j1k2_exp_le[OF refl ‹k ≥ 2›]
show ?thesis.
next
assume "❙|x❙| ≤ ❙|y❙|"
have "y ⋅ x ≠ x ⋅ y"
using assms(3) by force
define z' where "z' = rotate ❙|x❙| z"
hence "y⇧@k ⋅ x = z' ⇧@ l"
using arg_cong[OF assms(1), of "λt. rotate ❙|x❙| t"]
unfolding rotate_append rotate_pow_list_swap
by blast
interpret LS_len_le y x k 1 l z'
using ‹❙|x❙| ≤ ❙|y❙|› ‹y ⋅ x ≠ x ⋅ y› ‹y⇧@k ⋅ x = z' ⇧@ l› ‹2 ≤ l› ‹1 ≤ k›
by (unfold_locales) (blast, blast, force, blast+)
from case_j2k1_exp_le[OF ‹2 ≤ k› refl]
show ?thesis.
qed
qed
qed
lemma LS_exp_le_conv_rat:
fixes x y k::"'a::linordered_field"
assumes "y > 0"
shows "k * y + 4 ≤ x + 2 * y ⟷ k ≤ (x - 4)/y+ 2"
unfolding le_diff_eq[symmetric]
unfolding diff_conv_add_uminus
unfolding add.assoc add.commute[of "2*y"]
unfolding add.assoc[symmetric]
unfolding diff_le_eq[of _ "2*y" "x + - 4",symmetric] left_diff_distrib'[symmetric]
unfolding pos_le_divide_eq[OF ‹y > 0›, symmetric]
unfolding diff_le_eq..
end