theory CoWLyndonSchutzenberger
  imports CoWBasic 
begin

chapter \<open>Lyndon-Sch\"utzenberger Equation\<close>

text\<open>We set up a locale representing the Lyndon-Sch\"utzenberger Equation.\<close>

locale LS =
  fixes x a y b z c
  assumes a:  "2 \<le> a" and b: "2 \<le> b" and c: "2 \<le> c"   and eq: "x\<^sup>@a \<cdot> y\<^sup>@b = z\<^sup>@c" 
begin

lemma per_lemma_case:
  assumes "\<^bold>|z\<^bold>| + \<^bold>|x\<^bold>| \<le> \<^bold>|x\<^sup>@a\<^bold>|" and "x \<noteq> \<epsilon>"   
  shows "x\<cdot>y=y\<cdot>x"
proof-
  { have "x\<^sup>@a \<le>p z\<^sup>@c" using eq
      by (metis prefI)
    hence "x\<cdot>z = z\<cdot>x"
      by (metis append_self_conv append_self_conv2 \<open>\<^bold>|z\<^bold>| + \<^bold>|x\<^bold>| \<le> \<^bold>|x\<^sup>@a\<^bold>|\<close> per_pref self_pref two_pers)
    hence "x\<^sup>@a\<cdot>z\<^sup>@c  = z\<^sup>@c\<cdot>x\<^sup>@a"
      by (metis comm_add_exp) 
    hence "x\<^sup>@a \<cdot> y\<^sup>@b = y\<^sup>@b \<cdot> x\<^sup>@a"
      by (metis \<open>x\<^sup>@a \<le>p z\<^sup>@c\<close> eq lqI lq_reassoc)
    hence ?thesis using a b
      by (metis add_leE comm_powers_roots le_numeral_extra(2) one_add_one) 
  }
  thus ?thesis
    by fastforce
qed

lemma core_case:
  assumes 
    "c = 3" and 
    "b*\<^bold>|y\<^bold>| \<le> a*\<^bold>|x\<^bold>|" and "x \<noteq> \<epsilon>" and "y \<noteq> \<epsilon>" and 
    lenx: "a*\<^bold>|x\<^bold>| < \<^bold>|z\<^bold>| + \<^bold>|x\<^bold>|" and
    leny: "b*\<^bold>|y\<^bold>| < \<^bold>|z\<^bold>| + \<^bold>|y\<^bold>|"
  shows "x\<cdot>y = y\<cdot>x" 
proof- 
  \<comment>\<open>We first show that a = 2\<close>
  have "a*\<^bold>|x\<^bold>|+b*\<^bold>|y\<^bold>| = 3*\<^bold>|z\<^bold>|"
    using \<open>c = 3\<close> eq length_append[of "x\<^sup>@a" "y\<^sup>@b"]
    by (simp add: power_len)
  hence "3*\<^bold>|z\<^bold>| \<le> a*\<^bold>|x\<^bold>| + a*\<^bold>|x\<^bold>|"
    using \<open>b*\<^bold>|y\<^bold>| \<le> a*\<^bold>|x\<^bold>|\<close>  by simp
  hence "3*\<^bold>|z\<^bold>| < 2*\<^bold>|z\<^bold>| + 2*\<^bold>|x\<^bold>|"
    using lenx by linarith
  hence "\<^bold>|z\<^bold>| + \<^bold>|x\<^bold>| < 3 * \<^bold>|x\<^bold>|" by simp
  hence "a * \<^bold>|x\<^bold>| < 3 * \<^bold>|x\<^bold>|" using lenx by linarith
  hence "a = 2"  using a by simp

  hence "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|" using \<open>b*\<^bold>|y\<^bold>| \<le> a*\<^bold>|x\<^bold>|\<close> b 
      power_len[of x 2]  power_len[of y b] mult_le_less_imp_less[of a b "\<^bold>|x\<^bold>|" "\<^bold>|y\<^bold>|"] not_le
    by auto
  have "x\<cdot>x\<cdot>y\<^sup>@b = z\<cdot>z\<cdot>z" using a eq \<open>c=3\<close> \<open>a=2\<close>
    by (simp add: numeral_2_eq_2 numeral_3_eq_3) 

   \<comment> \<open>Find words u, v, w\<close>
  have "\<^bold>|z\<^bold>| < \<^bold>|x\<cdot>x\<^bold>|"
    using \<open>\<^bold>|z\<^bold>| + \<^bold>|x\<^bold>| < 3 * \<^bold>|x\<^bold>|\<close> add.commute by auto 
  then obtain w  where "x\<cdot>x = z\<cdot>w" using \<open>x\<cdot>x\<cdot>y\<^sup>@b = z\<cdot>z\<cdot>z\<close> ruler_le  nat_less_le append.assoc
    by (metis prefix_def)

  have "\<^bold>|x\<^bold>| < \<^bold>|z\<^bold>|"
    using \<open>a = 2\<close> lenx by auto
  then obtain u :: "'a list" where "z=x\<cdot>u" using \<open>x\<cdot>x\<cdot>y\<^sup>@b = z\<cdot>z\<cdot>z\<close> nat_less_le append.assoc ruler_le
    by (metis prefix_def)
  have "u \<noteq> \<epsilon>"
    using \<open>\<^bold>|x\<^bold>| < \<^bold>|z\<^bold>|\<close> \<open>z = x\<cdot>u\<close> by auto 
  have "x = u\<cdot>w" using  \<open>x\<cdot>x = z\<cdot>w\<close> \<open>z = x\<cdot>u\<close>   by auto

  have "\<^bold>|x\<cdot>x\<^bold>| < \<^bold>|z\<cdot>z\<^bold>|"  by (simp add: \<open>\<^bold>|x\<^bold>| < \<^bold>|z\<^bold>|\<close> add_less_mono)
  have "z\<cdot>w \<le>p z\<cdot>z"  using  \<open>x\<cdot>x = z\<cdot>w\<close>  \<open>x\<cdot>x\<cdot>y\<^sup>@b = z\<cdot>z\<cdot>z\<close>
    by (metis \<open>\<^bold>|x \<cdot> x\<^bold>| < \<^bold>|z \<cdot> z\<^bold>|\<close> less_imp_le_nat prefI ruler_le)
  then obtain v :: "'a list" where "x  = w \<cdot> v"
    by (metis \<open>x = u \<cdot> w\<close> \<open>z = x \<cdot> u\<close> lq_pref pref_cancel pref_prod_shorter1)
  have "u\<cdot>w\<cdot>v \<noteq> \<epsilon>"
    by (simp add: \<open>u \<noteq> \<epsilon>\<close>)

  \<comment> \<open>Express x, y and z in terms of  u, v and w\<close>
  hence "z = w\<cdot>v\<cdot>u" by (simp add: \<open>z = x\<cdot>u\<close> \<open>x  = w \<cdot> v\<close>)
  hence "w\<cdot>v \<cdot> u\<cdot>w \<cdot> y\<^sup>@b = w\<cdot>v\<cdot>u\<cdot>w\<cdot>v\<cdot>u\<cdot>w\<cdot>v\<cdot>u"
    using \<open>x \<cdot> x = z \<cdot> w\<close> \<open>x \<cdot> x \<cdot> y\<^sup>@b = z \<cdot> z \<cdot> z\<close> by auto
  hence "y\<^sup>@b = v\<cdot>u\<cdot>w\<cdot>v\<cdot>u"
    using \<open>x = u\<cdot>w\<close> \<open>x = w\<cdot>v\<close> \<open>x\<cdot>x\<cdot>y\<^sup>@b = z\<cdot>z\<cdot>z\<close> append.assoc by auto

  \<comment> \<open>Double period of uwv\<close>
  hence "periodN (u\<cdot>w\<cdot>v) \<^bold>|y\<^bold>|" using \<open>x \<noteq> \<epsilon>\<close> \<open>y \<noteq> \<epsilon>\<close> per_factor[of y "u\<cdot>w\<cdot>v" v u b, OF \<open>y \<noteq> \<epsilon>\<close> \<open>u\<cdot>w\<cdot>v\<noteq>\<epsilon>\<close>]
    by (metis  append_assoc)
  have "u\<cdot>w\<cdot>v = x \<cdot>v"
    by (simp add: \<open>x = u \<cdot> w\<close>) 
  have "u\<cdot>w\<cdot>v = u\<cdot> x"
    by (simp add: \<open>x = w \<cdot> v\<close>)
  have "u\<cdot>w\<cdot>v \<le>p u\<^sup>\<omega>"
    by (metis \<open>u \<cdot> w \<cdot> v = u \<cdot> x\<close> \<open>u \<noteq> \<epsilon>\<close> \<open>x = u \<cdot> w\<close> period_root_def pref_ext triv_pref)
  have "periodN (u\<cdot>w\<cdot>v) \<^bold>|u\<^bold>|"
    using \<open>u \<cdot> w \<cdot> v \<le>p u \<^sup>\<omega>\<close> by auto

  \<comment> \<open>Common period d\<close>
  obtain d::nat where "d=gcd \<^bold>|y\<^bold>| \<^bold>|u\<^bold>|"
    by simp
  have "\<^bold>|y\<^bold>| + \<^bold>|u\<^bold>| \<le> \<^bold>|u\<cdot>w\<cdot>v\<^bold>|" using \<open>\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|\<close> length_append \<open>u\<cdot>w\<cdot>v = u\<cdot> x\<close>
    by simp
  hence "periodN (u\<cdot>w\<cdot>v) d" 
    using \<open>periodN (u \<cdot> w \<cdot> v) \<^bold>|u\<^bold>|\<close> \<open>periodN (u \<cdot> w \<cdot> v) \<^bold>|y\<^bold>|\<close> \<open>d = gcd \<^bold>|y\<^bold>| \<^bold>|u\<^bold>|\<close> two_periodsN
    by blast

  \<comment> \<open>Divisibility\<close>
  have "v\<cdot>u\<cdot>z=y\<^sup>@b"
    by (simp add: \<open>y\<^sup>@b = v \<cdot> u \<cdot> w \<cdot> v \<cdot> u\<close> \<open>z = w \<cdot> v \<cdot> u\<close>)
  have "\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|"
    using \<open>x = u \<cdot> w\<close> \<open>x = w \<cdot> v\<close> length_append[of u w] length_append[of w v] add.commute[of "\<^bold>|u\<^bold>|" "\<^bold>|w\<^bold>|"] add_left_cancel
    by simp
  hence "d dvd \<^bold>|v\<^bold>|" using gcd_nat.cobounded1[of "\<^bold>|v\<^bold>|" "\<^bold>|y\<^bold>|"] gcd.commute[of "\<^bold>|y\<^bold>|" "\<^bold>|u\<^bold>|"]
    by (simp add: \<open>d = gcd \<^bold>|y\<^bold>| \<^bold>|u\<^bold>|\<close>)
  have "d dvd \<^bold>|u\<^bold>|"
    by (simp add: \<open>d = gcd  \<^bold>|y\<^bold>| \<^bold>|u\<^bold>|\<close>)
  have "\<^bold>|z\<^bold>| = b*\<^bold>|y\<^bold>| - \<^bold>|u\<^bold>| - \<^bold>|v\<^bold>|" using  \<open>v\<cdot>u\<cdot>z=y\<^sup>@b\<close>
    by (metis add.commute add_diff_cancel_left' diff_diff_add length_append power_len)
  hence "d dvd \<^bold>|z\<^bold>|" using \<open>v\<cdot>u\<cdot>z=y\<^sup>@b\<close> length_append power_len \<open>d dvd \<^bold>|u\<^bold>|\<close> \<open>d dvd \<^bold>|v\<^bold>|\<close> 
    using \<open>d = gcd  \<^bold>|y\<^bold>| \<^bold>|u\<^bold>|\<close> \<open>d dvd \<^bold>|v\<^bold>|\<close> by auto 
  hence "d dvd \<^bold>|w\<^bold>|" using  \<open>z = w \<cdot> v \<cdot> u\<close>  \<open>d dvd \<^bold>|u\<^bold>|\<close> \<open>d dvd \<^bold>|v\<^bold>|\<close>
    by (metis gcd_add1 gcd_nat.bounded_iff length_append)
  hence "d dvd \<^bold>|x\<^bold>|"
    by (simp add: \<open>d dvd \<^bold>|v\<^bold>|\<close> \<open>x = w \<cdot> v\<close>)

  \<comment> \<open>x and y commute\<close>
  have "x \<le>p u\<cdot>w\<cdot>v"
    by (simp add: \<open>x = u \<cdot> w\<close>)   
  have "periodN x d" using per_pref'[OF \<open>x\<noteq>\<epsilon>\<close>  \<open>periodN (u\<cdot>w\<cdot>v) d \<close> \<open>x \<le>p u \<cdot>w\<cdot>v\<close>].
  hence "x \<in> (take d x)*"
    using \<open>d dvd \<^bold>|x\<^bold>|\<close>
    using root_divisor by blast 

  hence "periodN u d " using \<open>x = u \<cdot> w\<close> per_pref'
    using \<open>periodN x d\<close> \<open>u \<noteq> \<epsilon>\<close> by blast
  have " take d x = take d u" using \<open>u\<noteq>\<epsilon>\<close>  \<open>x = u \<cdot> w\<close> pref_share_take
    by (simp add: \<open>d = gcd  \<^bold>|y\<^bold>| \<^bold>|u\<^bold>|\<close>)
  hence "u \<in> (take d x)*"
    by (metis \<open>periodN u d\<close>  \<open>d dvd \<^bold>|u\<^bold>|\<close> root_divisor)

  hence "z \<in> (take d x)*" using \<open>z=x\<cdot>u\<close> \<open>x \<in> (take d x)*\<close>
    using add_roots by blast
  hence "y\<^sup>@b \<in> (take d x)*" using eq  \<open>u \<cdot> w \<cdot> v = u \<cdot> x\<close> \<open>u \<cdot> w \<cdot> v = x \<cdot> v\<close> \<open>u \<in> take d x*\<close> \<open>v \<cdot> u \<cdot> z = y\<^sup>@b\<close> \<open>x \<in> take d x*\<close> \<open>z \<in> take d x*\<close> add_roots cancel comm_root1 by (metis) 
  thus ?thesis using  \<open>x \<in> (take d x)*\<close> comm_drop_exp
    by (metis \<open>u \<noteq> \<epsilon>\<close> \<open>y\<^sup>@b = v \<cdot> u \<cdot> w \<cdot> v \<cdot> u\<close> append_is_Nil_conv comm_root1 power_zero)
 qed

end \<comment> \<open>locale LS\<close>

theorem Lyndon_Schutzenberger:
  "\<lbrakk> x\<^sup>@a\<cdot>y\<^sup>@b = z\<^sup>@c;  2 \<le> a;  2 \<le> b; 2 \<le> c \<rbrakk>
  \<Longrightarrow> x\<cdot>y = y\<cdot>x"
proof (induction "\<^bold>|z\<^bold>| + b* \<^bold>|y\<^bold>|" arbitrary: x y z a b c  rule: nat_less_induct)
  case 1
  then show ?case
  proof-

    interpret LS x a y b z c using \<open> x\<^sup>@a\<cdot>y\<^sup>@b = z\<^sup>@c\<close> \<open> 2 \<le>a \<close> \<open> 2 \<le> b\<close> \<open> 2 \<le> c\<close>
      by (simp add: LS.intro)
    interpret LSrev: LS "rev y" b "rev x" a "rev z" c using   \<open>x\<^sup>@a \<cdot> y\<^sup>@b = z\<^sup>@c\<close>
      by (metis LS.intro a b c rev_append rev_power)

    \<comment> \<open>trivial case\<close>
    have triv: "x = \<epsilon> \<or>  y = \<epsilon> \<Longrightarrow> ?thesis"
      by auto

    \<comment> \<open>WLOG assumption\<close>
    { assume "\<^bold>|x\<^sup>@a\<^bold>| < \<^bold>|y\<^sup>@b\<^bold>|"
      have "\<^bold>|rev z\<^bold>| + a* \<^bold>|rev x\<^bold>| < \<^bold>|z\<^bold>| + b* \<^bold>|y\<^bold>|" using \<open>\<^bold>|x\<^sup>@a\<^bold>| < \<^bold>|y\<^sup>@b\<^bold>|\<close>
        by (simp add: power_len)
      hence "(rev y)\<cdot>(rev x) = (rev x)\<cdot>(rev y)"
        using "1.hyps" LSrev.eq a b c by blast 
      hence ?thesis  by (metis rev_append rev_rev_ident) 
    } note WLOG_assumption = this 
    {assume "\<^bold>|y\<^sup>@b\<^bold>| \<le> \<^bold>|x\<^sup>@a\<^bold>|"

     \<comment> \<open>case solved by the Periodicity lemma\<close>
      { assume short: "(\<^bold>|z\<^bold>| + \<^bold>|x\<^bold>| \<le> \<^bold>|x\<^sup>@a\<^bold>|) \<or> (\<^bold>|z\<^bold>| + \<^bold>|y\<^bold>| \<le> \<^bold>|y\<^sup>@b\<^bold>|)"         
        have triv': "x = \<epsilon> \<or>  rev y = \<epsilon> \<Longrightarrow> ?thesis"
          by auto
        hence ?thesis
          using per_lemma_case LSrev.per_lemma_case short
          by (metis length_rev rev_append rev_is_rev_conv rev_power)
      } note periodicity_lemma_case = this

     \<comment> \<open>the case without Periodicity lemma\<close>
      { assume lenx: "\<^bold>|x\<^sup>@a\<^bold>| < \<^bold>|z\<^bold>| + \<^bold>|x\<^bold>|" and leny: "\<^bold>|y\<^sup>@b\<^bold>| < \<^bold>|z\<^bold>| + \<^bold>|y\<^bold>|"
      \<comment> \<open>implies c < 4\<close>
        have ex: "\<exists> k. d = Suc (Suc k)" if "2 \<le> d" for d
          using nat_le_iff_add that by auto 
        have "\<^bold>|x\<^sup>@a\<^bold>| + \<^bold>|y\<^sup>@b\<^bold>| < 4 * \<^bold>|z\<^bold>|" 
          using ex[OF \<open>2 \<le> a\<close>] ex[OF \<open>2 \<le> b\<close>] lenx leny by auto
        hence "c < 4"
          using power_len eq length_append mult_less_cancel2[of c "\<^bold>|z\<^bold>|" 4] by metis

      \<comment> \<open>case c = 3\<close>
        {assume "c = 3" and "x \<noteq> \<epsilon>" and "y \<noteq> \<epsilon>"
          hence ?thesis 
            using \<open>\<^bold>|y\<^sup>@b\<^bold>| \<le> \<^bold>|x\<^sup>@a\<^bold>|\<close> core_case lenx leny
            by (simp add: power_len)
        } note c_equals_3 = this

       \<comment> \<open>the remaining case c = 2\<close>
        {assume "c = 2"  and "x \<noteq> \<epsilon>" and "y \<noteq> \<epsilon>"
          hence eq2: "x\<^sup>@a \<cdot> y\<^sup>@b = z \<cdot> z"
            by (simp add: \<open>x \<noteq> \<epsilon>\<close> eq power2_list)
          obtain a' where "a = Suc a'" using \<open>2 \<le> a\<close>
            using ex by auto
          hence "x\<^sup>@a'\<cdot>x\<cdot>y\<^sup>@b=z\<cdot>z" using \<open>c = 2\<close> \<open>x\<^sup>@a\<cdot>y\<^sup>@b = z\<^sup>@c\<close>
            by (metis add_one_exp eq2)
          have "(Suc d)*m < (n::nat)" if "(Suc (Suc d))*m < n + m" for d m n
            using that by auto 
          hence "\<^bold>|x\<^sup>@a'\<^bold>| < \<^bold>|z\<^bold>|" using \<open>a = Suc a'\<close>  lenx  power_len
            by auto
          hence "x\<^sup>@a' \<le>p z" using \<open>x\<^sup>@a'\<cdot>x\<cdot>y\<^sup>@b=z\<cdot>z\<close>
            by (metis append.assoc less_imp_le_nat prefI pref_comp_len ruler_comp)
          have "x\<^sup>@a' \<noteq> z"
            using \<open>\<^bold>|x\<^sup>@a'\<^bold>| < \<^bold>|z\<^bold>|\<close> by blast 

          then obtain u where "z=x\<^sup>@a'\<cdot>u" and "u \<noteq> \<epsilon>" 
            using \<open>x\<^sup>@a' \<le>p z\<close> prefE by blast
          have "\<^bold>|y\<^sup>@b\<^bold>| + \<^bold>|y\<^sup>@b\<^bold>| \<le> \<^bold>|z\<^bold>| + \<^bold>|z\<^bold>|"  using \<open>\<^bold>|y\<^sup>@b\<^bold>| \<le> \<^bold>|x\<^sup>@a\<^bold>|\<close> eq2 length_append[of "x\<^sup>@a" "y\<^sup>@b"] length_append[of z z]
            by simp
          hence "\<^bold>|y\<^sup>@b\<^bold>| \<le> \<^bold>|z\<^bold>|" by simp 
          have "y\<^sup>@b \<le>s z"  using \<open>x\<^sup>@a'\<cdot>x\<cdot>y\<^sup>@b=z\<cdot>z\<close>
            by (metis \<open>\<^bold>|y\<^sup>@b\<^bold>| \<le> \<^bold>|z\<^bold>|\<close> suf_prod_shorter4 suffix_def)
          then obtain w where "z=w\<cdot>y\<^sup>@b" using  \<open> x\<^sup>@a\<cdot>y\<^sup>@b = z\<^sup>@c\<close> \<open>c=2\<close>
            using suffix_def by blast

          hence "x\<^sup>@a'\<cdot>x\<cdot>y\<^sup>@b = x\<^sup>@a'\<cdot>u\<cdot>w\<cdot>y\<^sup>@b" 
            using \<open>x\<^sup>@a'\<cdot>x\<cdot>y\<^sup>@b=z\<cdot>z\<close> \<open>z=x\<^sup>@a'\<cdot>u\<close>  by simp
          hence "u\<cdot>w=x"
            by auto
          hence "w\<cdot>z = (w\<cdot>u)\<^sup>@a" using \<open>z=x\<^sup>@a'\<cdot>u\<close> power_slide[of w u a'] append_assoc
            by (simp add: \<open>a = Suc a'\<close>)

         \<comment> \<open>Induction step: new equation with shorter z\<close>
          hence "(w\<cdot>u)\<^sup>@a = w\<^sup>@2\<cdot>y\<^sup>@b"
            by (simp add: \<open>z = w \<cdot> y\<^sup>@b\<close> power2_list)
          have "\<^bold>|x\<^bold>| \<le> \<^bold>|x\<^sup>@(a-1)\<^bold>|"  using  a
            using le_diff_iff' nat_le_iff_add by auto
          hence  "\<^bold>|x\<^bold>| < \<^bold>|z\<^bold>|"
            using \<open>\<^bold>|x\<^sup>@a'\<^bold>| < \<^bold>|z\<^bold>|\<close> le_less_trans
            by (simp add: \<open>a = Suc a'\<close>)
          hence "\<^bold>|w\<cdot>u\<^bold>| + b* \<^bold>|y\<^bold>| < \<^bold>|z\<^bold>| + b*\<^bold>|y\<^bold>|" using  \<open>u\<cdot>w=x\<close>
            by auto 
          hence "w\<cdot>y = y\<cdot>w" using \<open>(w\<cdot>u)\<^sup>@a = w\<^sup>@2\<cdot>y\<^sup>@b\<close> \<open>a \<ge> 2\<close> \<open>b \<ge> 2\<close>  "1.hyps"
            by (metis \<open>c = 2\<close> c) 

          hence "(w\<cdot>u)\<^sup>@a \<cdot> w = w \<cdot> (w\<cdot>u)\<^sup>@a"
            by (metis \<open>w \<cdot> z = (w \<cdot> u)\<^sup>@a\<close> \<open>z = w \<cdot> y\<^sup>@b\<close> append_assoc comm_add_exp)
          hence "w \<cdot> u = u \<cdot> w"
            using comm_drop_exp[OF _ \<open>(w\<cdot>u)\<^sup>@a \<cdot> w = w \<cdot> (w\<cdot>u)\<^sup>@a\<close>] \<open>2 \<le> a\<close> by simp
          hence "x\<^sup>@a\<cdot>y=y\<cdot>x\<^sup>@a"
          proof-
            have "x\<^sup>@a \<cdot> y = w \<cdot> z \<cdot> y"
              by (simp add: \<open>u \<cdot> w = x\<close> \<open>w \<cdot> u = u \<cdot> w\<close> \<open>w \<cdot> z = (w \<cdot> u)\<^sup>@a\<close>)
            also have "... = w \<cdot> w \<cdot> y\<^sup>@b \<cdot> y"
              by (simp add: \<open>z = w \<cdot> y\<^sup>@b\<close>)
            also have "... = y \<cdot> w \<cdot> w \<cdot> y\<^sup>@b"
              by (simp add: \<open>w \<cdot> y = y \<cdot> w\<close> comm_add_exp)
            also have "... = y\<cdot>x\<^sup>@a"
              using \<open>u \<cdot> w = x\<close> \<open>w \<cdot> u = u \<cdot> w\<close> \<open>w \<cdot> z = (w \<cdot> u)\<^sup>@a\<close> \<open>z = w \<cdot> y\<^sup>@b\<close> by auto
            finally show ?thesis
              by simp
          qed  
          hence "x \<cdot> y = y \<cdot> x"
            using comm_drop_exp[OF _ \<open>x\<^sup>@a\<cdot>y=y\<cdot>x\<^sup>@a\<close>] \<open>2 \<le> a\<close> by simp
        }note c_equals_2 = this

        hence ?thesis  using  triv c_equals_3  \<open>c < 4\<close>  \<open>c \<ge> 2\<close>
          by (metis Suc_numeral leD less_antisym  semiring_norm(2) semiring_norm(5) semiring_norm(8)) 
      } note core_case = this

      hence ?thesis using periodicity_lemma_case
        using not_le_imp_less by blast
    } 

    thus ?thesis using WLOG_assumption leI by blast
  qed

qed

end