Theory Binary_Square_Interpretation

(*  Title:      Binary Square Interpretation
    File:       Binary_Code_Imprimitive.Binary_Square_Interpretation
    Author:     Štěpán Holub, Charles University
    Author:     Martin Raška, Charles University

Part of Combinatorics on Words Formalized. See https://gitlab.com/formalcow/combinatorics-on-words-formalized/
*)

theory Binary_Square_Interpretation

imports
  Combinatorics_Words.Submonoids
  Combinatorics_Words.Equations_Basic
begin

section ‹Lemmas for covered x square›

text ‹This section explores various variants of the situation when @{term "x  x"} is covered with
 @{term "xy@ku  vy@lx"}, with @{term "y = uv"}, and the displayed dots being synchronized.
›

subsection ‹Two particular cases›

― ‹Very short and very large overlap›

lemma  pref_suf_pers_short: assumes "x ≤p v  x" and "|v  u| < |x|" and "x ≤s r  u  v  u" and "r  {u,v}"
  ― ‹@{term "x  x"} is covered by @{term "(puvu)  (vx)"}, the displayed dots being synchronized›
  ― ‹That is, the condition on the first @{term x} in @{term "xy@ku  vy@lx"} is relaxed›
  shows "uv = vu"
proof (rule nemp_comm)
  have "v  u <s x"
    using suf_prod_long_less[OF _  |v  u| < |x|, of "r  u", unfolded rassoc, OF x ≤s r  u  v  u].
  assume "u  ε" and "v  ε"
  obtain q where "x = q  v  u" and "q  ε"
    using v  u <s x  by (auto simp add: suffix_def)
  hence "q ≤s r  u"
    using x ≤s r  u  v  u by (auto simp add: suffix_def)
  from suf_trans[OF primroot_suf this]
  have "ρ q ≤s r  u".
  have "q  v = v  q"
    using pref_marker[OF x ≤p vx, of q ] x = q  v  u by simp
  from suf_marker_per_root[OF x ≤p v  x, of q u, unfolded rassoc x = q  v  u]
  have "u <p v  u"
    using v  ε by blast
  from per_root_primroot[OF this]
    comm_primroots'[OF q  ε v  ε  q  v = v  q]
  have "u ≤p ρ q  u"
    by force

  from  gen_prim[OF r  {u, v}, unfolded ]
  have "r  {u, ρ q}"
    unfolding ρ q = ρ v.
  from two_elem_root_suf_comm[OF u ≤p ρ q  u ρ q ≤s r  u this]
  show "u  v = v  u"
    using comm_primroot_conv[of _ v, folded ρ q = ρ v] by blast
qed

lemma pref_suf_pers_large_overlap:
  assumes
    "p ≤p x" and "s ≤s x" and "p ≤p r  p" and "s ≤s s  r" and "|x| + |r|  |p| + |s|"
  shows "x  r = r  x"
  using assms
proof (cases "r = ε")
  assume "r  ε" hence "r  ε" by blast
  have "|s|  |x|"
    using s ≤s x unfolding suffix_def by force
  have "|p|  |x|"
    using p ≤p x by (force simp add: prefix_def)
  have "|r|  |p|"
    using |x| + |r|  |p| + |s| |s|  |x| unfolding lenmorph by linarith
  have "|r|  |s|"
    using |x| + |r|  |p| + |s| |p|  |x| unfolding lenmorph by linarith
  obtain p1 ov s1 where "p1  ov  s1 = x"  and "p1  ov = p" and "ov  s1 = s"
    using pref_suf_overlapE[OF p ≤p x s ≤s x] using |x| + |r|  |p| + |s| by auto
  have "|r|  |ov|"
    using |x| + |r|  |p| + |s|[folded p1  ov  s1 = x p1  ov = p ov  s1 = s]
    unfolding lenmorph by force
  have "r ≤p p"
    using |r|  |p|[unfolded swap_len] pref_prod_long[OF p ≤p r  p] by blast
  hence "r ≤p x"
    using p ≤p x by auto
  have "r ≤s s"
    using |r|  |s|[unfolded swap_len] pref_prod_long[reversed, OF s ≤s s  r] by blast
  hence "r ≤s x"
    using s ≤s x by auto
  obtain k where "p ≤p r@k" "0 < k"
    using per_root_powE[OF per_rootI[OF p ≤p r  p r  ε]] sprefD1 by metis
  hence "p1  ov ≤f r@k"
    unfolding p1  ov = p by blast
  obtain l where "s ≤s r@ l" 0 < l
    using per_root_powE[reversed, OF per_rootI[reversed, OF s ≤s s  r r  ε]] ssufD1 by metis
  hence "ov  s1 ≤f r@ l"
    unfolding ov  s1 = s by blast
  from per_glue_facs[OF p1  ov ≤f r@ k ov  s1 ≤f r@ l |r|  |ov|, unfolded p1  ov  s1 = x]
  obtain m where "x ≤f r @ m".
  show "x  r = r  x"
    using root_suf_comm[OF
        pref_prod_root[OF marker_fac_pref[OF x ≤f r @ m r ≤p x]]
        suffix_appendI[OF r ≤s x]]..
qed simp

subsection ‹Main cases›

locale pref_suf_pers =
  fixes x u v k m
  assumes
    x_pref:  "x ≤p (v  (u  v)@k)  x" ― ‹@{term "x ≤p p  x"} and @{term "p ≤p q  p"} where @{term "q = v  u"}
    and
    x_suf:  "x ≤s x  (u  v)@m  u" ― ‹@{term "x ≤s s  x"} and @{term "s ≤s q'  s"} where @{term "q' = u  v"}
    and k_pos: "0 < k" and m_pos: "0 < m"
begin

lemma pref_suf_commute_all_commutes:
  assumes  "|u  v|  |x|" and "u  v = v  u"
  shows "commutes {u,v,x}"
  using assms
proof (cases "u  v = ε")
  let ?p = "(v  (u  v)@k)"
  let ?s = "(u  v)@m  u"
  note x_pref x_suf

  assume "u  v  ε"
  have "?p  ε" and "?s  ε" and "v  u  ε"
    using u  v  ε m_pos k_pos by auto
  obtain r where "u  r*" and "v  r*" and "primitive r"
    using u  v = v  u comm_primrootE by metis
  hence "r  ε"
    by force

  have "?p  r*" and "?s  r*" and "v  u  r*" and "u  v  r*"
    using u  r* v  r*
    by (simp_all add: add_roots root_pow_root)

  have "x ≤p r  x"
    using  ?p  r* x ≤p ?p  x ?p  ε by blast
  have "v  u ≤s x"
    using ruler_le[reversed, OF _ _ |u  v|  |x|[unfolded swap_len[of u]],
        of  "(x  (u  v) @ (m-1)  u)  v  u", OF triv_suf, unfolded rassoc, OF x ≤s x  ?s[unfolded pow_pos'[OF m_pos] rassoc]].
  have "r ≤s  v  u"
    using  v  u  ε v  u  r* per_root_suf by blast
  have "r ≤s r  x"
    using suf_trans[OF r ≤s  v  u v  u ≤s x, THEN suffix_appendI] by blast
  have "x  r  = r  x"
    using  root_suf_comm[OF x ≤p r  x r ≤s r  x, symmetric].
  hence "x  r*"
    by (simp add: primitive r prim_comm_root)
  thus "commutes {u,v,x}"
    using u  r* v  r* commutesI_root[of "{u,v,x}"] by blast
qed simp

lemma no_overlap:
  assumes
    len: "|v  (u  v)@k| + |(u  v)@m  u|  |x|" (is "|?p| + |?s|  |x|") and
    "0 < k" "0 < m"
  shows "commutes {u,v,x}"
  using assms
proof (cases "u  v = ε")
  note x_pref x_suf
  assume "u  v  ε"
  have "?p  ε" and "?s  ε"
    using u  v  ε m_pos k_pos by force+
  from per_lemma_pref_suf[OF per_rootI[OF x ≤p ?p  x ?p  ε] per_rootI[reversed, OF x ≤s x  ?s  ?s  ε] |?p| + |?s|  |x|]
  obtain r s kp ks mw where "?p = (r  s)@kp" and "?s = (s  r)@ks" and "x = (r  s)@mw  r" and "primitive (r  s)".
  hence "ρ ?p = r  s"
    using v  (u  v) @k  ε comm_primroots nemp_pow_nemp pow_comm prim_self_root by metis
  moreover have "ρ ?s = s  r"
    using   primroot_unique[OF ?s  ε _ ?s = (s  r)@ks] prim_conjug[OF primitive (r  s)] by blast
  ultimately have "ρ ?p  ρ ?s"
    by force
  from conj_pers_conj_comm[OF this k_pos m_pos]
  have "u  v = v  u".

  from pref_suf_commute_all_commutes[OF _ this]
  show "commutes {u,v,x}"
    using len by auto
qed simp

lemma no_overlap':
  assumes
    len: "|v  (u  v)@k| + |(u  v)@m  u|  |x|" (is "|?p| + |?s|  |x|")
    and "0 < k" "0 < m"
  shows "u  v = v  u"
  by (rule commutesE[of "{u,v,x}"], simp_all add: no_overlap[OF assms])

lemma short_overlap:
  assumes
    len1: "|x| < |v  (u  v)@k| + |(u  v)@m  u|" (is "|x| < |?p| + |?s|") and
    len2: "|v  (u  v)@k| + |(u  v)@m  u|  |x| + |u|" (is "|?p| + |?s|  |x| + |u|")
  shows "commutes {u,v,x}"
proof (rule pref_suf_commute_all_commutes)
  show "|u  v|  |x|"
    using len2 unfolding pow_pos[OF k_pos] lenmorph by simp
next
  note x_pref x_suf
    ― ‹obtain the overlap›

  have "|?p|  |x|"
    using  len2 unfolding lenmorph by linarith
  hence "?p ≤p x"
    using x ≤p ?p  x pref_prod_long by blast

  have "|?s|  |x|"
    using  len2 unfolding pow_pos[OF k_pos] pow_len lenmorph by auto
  hence "?s ≤s x"
    using suf_prod_long[OF x ≤s x  ?s] by blast

  from  pref_suf_overlapE[OF ?p ≤p x ?s ≤s x less_imp_le[OF len1]]
  obtain p1 ov s1 where "p1  ov  s1 = x" and "p1  ov = ?p" and "ov  s1 = ?s".

  from len1[folded this]
  have "ov  ε"
    by fastforce

  have "|ov|  |u|"
    using len2[folded p1  ov  s1 = x p1  ov = ?p ov  s1 = ?s] unfolding lenmorph by auto

  then obtain s' where "ov  s' = u" and "s'  v  (u  v) @ (m -1)  u = s1"
    using eqdE[OF ov  s1 = ?s[unfolded pow_pos[OF m_pos] rassoc]] by auto

― ‹obtain the left complement›

  from   eqdE[reversed, of p1 ov "v  (u  v)@(k-1)" "u  v", unfolded rassoc,
      OF p1  ov = ?p[unfolded pow_pos'[OF k_pos]] ] |ov|  |u|
  have "v  (u  v) @ (k -1)  ≤p p1"
     unfolding lenmorph by (auto simp add: prefix_def)

  then obtain q where "v  (u  v)@(k-1)  q = p1"
    by (force simp add: prefix_def)

― ‹main proof using the lemma @{thm uvu_suf_uvvu}

  show "u  v = v  u"
  proof (rule sym, rule uvu_suf_uvvu)
    show "s' ≤s u"
      using ov  s' = u ov  ε by blast
    show "u  v  v  u  s' = q  u  v  u" ― ‹the main fact: the overlap situation›
    proof-
      have "u  v  u ≤p ?s"
        unfolding pow_pos[OF m_pos] rassoc pref_cancel_conv shift_pow by blast
      hence "p1  u  v  u ≤p x"
        unfolding p1  ov  s1 = x[symmetric] ov  s1 = ?s pref_cancel_conv.
      hence "v  (u  v)@(k-1)  q  u  v  ov ≤p x"
        using v  (u  v)@(k-1)  q = p1 ov  s' = u by (force simp add: prefix_def)

      have "v  u ≤p x"
        using ?p ≤p x[unfolded pow_pos[OF k_pos]] by (auto simp add: prefix_def)
      have "|?p  v  u|  |x|"
        using len2 unfolding pow_pos[OF m_pos] lenmorph by force
      hence "?p  v  u ≤p x"
        using x ≤p ?p  x v  u ≤p x pref_prod_longer by blast
      hence "v  (u  v)@(k-1)  u  v  v  u ≤p x"
        unfolding pow_pos'[OF k_pos] rassoc.

      have "|v  (u  v)@(k-1)  u  v  v  u| = |v  (u  v)@(k-1)  q  u  v  ov|"
        using lenarg[OF p1  ov = ?p[folded v  (u  v)@(k-1)  q = p1, unfolded pow_pos[OF k_pos] rassoc cancel]]
        by force

      from ruler_eq_len[OF  v  (u  v)@(k-1)  u  v  v  u ≤p x v  (u  v)@(k-1)  q  u  v  ov ≤p x this, unfolded cancel]
      have "u  v  v  u = q  u  v  ov".

      thus  "u  v  v  u  s' = q  u  v  u"
        using ov  s' = u by auto
    qed
    show "q ≤s v  u"
    proof (rule ruler_le[reversed])
      show "q ≤s x"
      proof (rule suf_trans)
        show "p1 ≤s x"
          using p1  ov  s1 = x[unfolded ov  s1 = ?s] x ≤s x  ?s  same_suffix_suffix by blast
        show "q ≤s p1"
          using v  (u  v) @ (k-1)  q = p1 by auto
      qed
      show "v  u ≤s x"
        using ?s ≤s x[unfolded pow_pos'[OF m_pos] rassoc] suf_extD by metis
      show "|q|  |v  u|"
        using lenarg[OF u  v  v  u  s' = q  u  v  u] lenarg[OF ov  s' = u] by force
    qed
  qed auto
qed

lemma medium_overlap:
  assumes
    len1: "|x| + |u| < |v  (u  v)@k| + |(u  v)@m  u|" (is "|x| + |u| < |?p| + |?s|") and
    len2: "|v  (u  v)@k| + |(u  v)@m  u| < |x| + |u  v|" (is "|?p| + |?s| < |x| + |u  v|")
  shows "commutes {u,v,x}"
proof (rule pref_suf_commute_all_commutes)
  show "|u  v|  |x|"
    using len2 unfolding pow_pos[OF k_pos] by force
next
  note x_pref x_suf
  have "|?p|  |x|"
    using  len2 unfolding pow_pos[OF m_pos] by auto
  hence "?p ≤p x"
    using x ≤p ?p  x pref_prod_long by blast
  hence  "v  (u  v)@(k-1)  u  v  v ≤p ?p  x"
    using x ≤p ?p  x  unfolding pow_pos'[OF k_pos] rassoc  by (auto simp add: prefix_def)

  have "|?s|  |x|"
    using  len2 unfolding pow_pos[OF k_pos] pow_len lenmorph by auto
  hence "?s ≤s x"
    using suf_prod_long[OF x ≤s x  ?s] by blast
  then obtain p' where "p'  u  v ≤p x" and "p'  ?s = x"
    unfolding pow_pos[OF m_pos] by (auto simp add: suffix_def)

  have "|p'  u  v|  |?p  v|"
    using len1[folded p'  ?s = x] by force

  have "|v  (u  v)@(k-1)|  < |p'|"
    using len2[folded p'  ?s = x] unfolding pow_pos'[OF k_pos] by force

  from less_imp_le[OF this]
  obtain p where "v  (u  v)@(k-1)  p = p'"
    using ruler_le[OF ?p ≤p x p'  u  v ≤p x,
        unfolded pow_pos'[OF k_pos] lassoc, THEN pref_cancel_right, THEN pref_cancel_right]
    unfolding lenmorph  by (auto simp add: prefix_def)

  have "|p|  |v|"
    using v  (u  v)@(k-1)  p = p' |p'  u  v|  |?p  v| unfolding pow_pos'[OF k_pos] by force

  show "u  v = v  u"
  proof (rule uv_fac_uvv)
    show "p  u  v ≤p u  v  v"
    proof (rule pref_cancel[of "v  (u  v)@(k-1)"], rule ruler_le)
      show "(v  (u  v) @ (k-1))  p  u  v ≤p ?p  x"
        unfolding lassoc v  (u  v)@(k-1)  p = p'[unfolded lassoc]
        using p'  u  v ≤p x x ≤p ?p  x unfolding pow_pos'[OF k_pos] by force
      show "(v  (u  v) @ (k-1))  u  v  v ≤p (v  (u  v) @ k)  x"
        unfolding pow_pos'[OF k_pos] rassoc
        using v  (u  v) @ k ≤p x by (auto simp add: prefix_def)
      show "|(v  (u  v) @ (k-1))  p  u  v|  |(v  (u  v) @ (k-1))  u  v  v|"
        using v  (u  v)@(k-1)  p = p' |p'  u  v|  |?p  v| unfolding pow_pos'[OF k_pos] by force
    qed

    have "p ≤s x"
      using  p'  ?s = x[folded v  (u  v)@(k-1)  p = p'] x ≤s x  ?s suf_cancel suf_extD by metis

    from ruler_le[reversed, OF this ?s ≤s x, unfolded pow_pos'[OF m_pos] rassoc]
    show "p ≤s (u  v) @ (m-1)  u  v  u"
      using  |p|  |v| unfolding  lenmorph by auto

    show "(u  v) @ (m-1)  u  v  u  {u, v}"
      by (simp add: gen_in hull_closed power_in)

    show "p  ε"
      using |v  (u  v)@(k-1)|  < |p'| v  (u  v)@(k-1)  p = p' by force
  qed
qed

thm
  no_overlap
  short_overlap
  medium_overlap

end

thm
  pref_suf_pers.no_overlap
  pref_suf_pers.short_overlap
  pref_suf_pers.medium_overlap
  pref_suf_pers_large_overlap

section ‹Square interpretation›

text ‹In this section fundamental description is given of (the only)
possible @{term "{x,y}"}-interpretation of the square @{term "xx"}, where @{term "|y|  |x|"}.
The proof is divided into several locales.
›

― ‹An example motivating disjointness: an interpretation which is not disjoint.›
lemma cover_not_disjoint:
  shows "primitive (𝔞𝔟𝔞𝔟𝔞𝔟𝔞)" (is "primitive ?x") and
        "primitive (𝔞𝔟)" (is "primitive ?y") and
    "(𝔞𝔟𝔞𝔟𝔞𝔟𝔞)  (𝔞𝔟)  (𝔞𝔟)  (𝔞𝔟𝔞𝔟𝔞𝔟𝔞)"
    (is "?x  ?y  ?y  ?x") and
    "ε (𝔞𝔟𝔞𝔟𝔞𝔟𝔞)  (𝔞𝔟𝔞𝔟𝔞𝔟𝔞) (𝔟𝔞𝔟𝔞)  [(𝔞𝔟𝔞𝔟𝔞𝔟𝔞),(𝔞𝔟),(𝔞𝔟),(𝔞𝔟𝔞𝔟𝔞𝔟𝔞)]"
    (is "ε ?x  ?x ?s  [?x,?y,?y,?x]")
  unfolding factor_interpretation_def
  by primitivity_inspection+ force

subsection ‹Locale: interpretation›

locale square_interp =
  ― ‹The basic set of assumptions›
  ― ‹The goal is to arrive at @{term "ws = [x]  [y]@k  [x]"} including the description
   of the interpretation in terms of the first and the second occurrence of x in the interpreted square.›
  fixes x y p s ws
  assumes
    non_comm: "x  y  y  x" and
    prim_x: "primitive x" and
        y_le_x: "|y|  |x|" and
    ws_lists: "ws  lists {x,y}" and
    nconjug: "¬ x  y" and
    disj_interp: "p [x,x] s 𝒟 ws"

begin

lemma interp: "p (xx) s  ws"
  using disj_interpD[OF disj_interp] by force

lemma disjoint:  "p1 ≤p [x,x]  p2 ≤p ws  p  concat p1  concat p2"
  using disj_interpD1[OF disj_interp].

interpretation binary_code x y
  using non_comm by unfold_locales

lemmas interpret_concat = fac_interpD(3)[OF interp]

lemma p_nemp:  "p  ε"
  using disjoint[of ε ε] by auto

lemma s_nemp: "s  ε"
  using disjoint[of "[x,x]" ws] interpret_concat by force

lemma x_root: "ρ x = x"
  using prim_x by blast


lemma ws_nemp: "ws  ε"
  using bin_fst_nemp fac_interp_nemp interp by blast

lemma hd_ws_lists: "hd ws  {x, y}"
  using lists_hd_in_set ws_lists ws_nemp by auto

lemma last_ws_lists: "last ws  {x, y}"
  using lists_hd_in_set[reversed, OF ws_nemp ws_lists].

lemma kE: obtains k where "[hd ws]  [y]@k  [last ws] = ws"
proof-
  from  list.collapse[OF ws_nemp] hd_word
  obtain ws' where "ws = [hd ws]  ws'"
    by metis
  hence "|hd ws|  |x|"
    using  two_elem_cases[OF lists_hd_in_set[OF ws_nemp ws_lists]] y_le_x by blast
  hence "|x|  |concat ws'|"
    using lenarg[OF interpret_concat, unfolded lenmorph]
    unfolding concat.simps emp_simps  arg_cong[OF ws = [hd ws]  ws', of "λ x. |concat x|", unfolded concat_morph lenmorph]
    by linarith
  hence "ws'  ε"
    using nemp_len[OF bin_fst_nemp] by fastforce
  then obtain mid_ws where "ws' = mid_ws  [last ws]"
    using ws = [hd ws]  ws' append_butlast_last_id last_appendR by metis
  note ws = [hd ws]  ws'[unfolded this]
    fac_interpD[OF interp]
  obtain p' where [symmetric]:"p  p' = hd ws" and "p'  ε"
    using spref_exE[OF p <p hd ws].
  obtain s' where  [symmetric]: "s' s  = last ws" and "s'  ε"
    using spref_exE[reversed, OF s <s last ws].
  have "p'  concat mid_ws  s' = x  x"
    using ws = [hd ws]  mid_ws  [last ws][unfolded hd ws = p  p' last ws  = s' s]
      p  (x  x)  s = concat ws by simp
  note over = prim_overlap_sqE[OF prim_x, folded this]
  have "mid_ws  lists {x,y}"
    using ws = [hd ws]  ws' ws' = mid_ws  [last ws] append_in_lists_conv ws_lists by metis
  have "x  set mid_ws"
  proof
    assume "x  set mid_ws"
    then obtain r q where "concat mid_ws = r  x  q"
      using concat.simps(2) concat_morph in_set_conv_decomp_first by metis
    have "(p'  r)   x  (q  s') = x  x"
      using p'  concat mid_ws  s' = x  x[unfolded concat mid_ws = r  x  q]
      unfolding rassoc.
    from prim_overlap_sqE[OF prim_x this]
    show False
      using p'  ε s'  ε by blast
  qed
  hence "mid_ws  lists {y}"
    using mid_ws  lists {x,y} by force
  from that sing_lists_exp[OF this]
  show thesis
    using ws = [hd ws]  mid_ws  [last ws] by metis
qed

lemma l_mE: obtains m u v l where "(hd ws)y@mu = px" and "v  y@l  (last ws) = x  s" and
  "uv = y" "u  ε" "v  ε" and "x  (v  u)  (v  u)  x"
 proof-
  note fac_interpD[OF interp]
  obtain k where "[hd ws]  [y]@k  [last ws] = ws"
    using kE.
  from arg_cong[OF this, of concat, folded interpret_concat, unfolded concat_morph rassoc concat_sing' concat_sing_pow]
  have "hd ws  y@k  last ws = p  x  x  s".
  have "|hd ws|  |p  x|"
    unfolding lenmorph by (rule two_elem_cases[OF hd_ws_lists])
    (use dual_order.trans[OF le_add2 y_le_x] le_add2[of "|x|"] in fast)+
  from eqd[OF _ this]
  obtain ya where "hd ws  ya = p  x"
    using hd ws  y@k  last ws = p  x  x  s  by auto
  have "|last ws|  |x|"
    unfolding lenmorph using dual_order.trans last_ws_lists y_le_x by auto
  hence "|last ws| < |x  s|"
    unfolding lenmorph using nemp_len[OF s_nemp] by linarith
  from eqd[reversed, OF _ less_imp_le[OF this]]
  obtain yb where "yb  (last ws) = x  s"
    using (hd ws)  y@k  (last ws) = p  x  x  s rassoc by metis
  hence "yb  ε"
    using s_nemp |last ws| < |x  s| by force
  have "ya  yb = y@k"
    using (hd ws)  y@k  (last ws) = p  x  x  s[folded yb  (last ws) = x  s, unfolded lassoc cancel_right, folded (hd ws)  ya = p  x, unfolded rassoc cancel, symmetric].
  from pref_mod_pow'[OF sprefI[OF prefI[OF this]], folded this]
  obtain m u where "m < k" and "u <p y" and "y@m  u = ya"
    using yb  ε by blast
  have "y@m  u  (u¯>y)  y@(k - m - 1) = y@m  y  y@(k - m - 1)"
    using u <p y  by (auto simp add: prefix_def)
  also have "... = y@(m + 1 + (k-m-1))"
    using rassoc add_exps pow_1 by metis
  also have "... = y@k"
    using m < k  by auto
  finally obtain l v where "uv = y" and "y@m  u  v  y@l = y@k"
    using u <p y lq_pref by blast
  have "concat ([hd ws][y] @ m) = hd ws  y @ m"
    by simp
  have "v  ε"
    using u <p y uv = y  by force
  have "[hd ws]  [y] @ m ≤p ws"
    using [hd ws]  [y]@k  [last ws] = ws[folded pop_pow[OF less_imp_le[OF m < k]]] by fastforce
  from disjoint[OF _ this, of "[x]", unfolded concat ([hd ws]  [y] @ m) = hd ws  y @ m]
  have "u  ε"
    using (hd ws)  ya = p  x[folded y@m  u = ya] s_nemp by force
         have "x  (v  u)  (v  u)  x"
  proof
    assume "x  v  u = (v  u)  x"
    from comm_primroots'[OF  bin_fst_nemp suf_nemp[OF u  ε] this, unfolded x_root]
    have "x = ρ (v  u)".
    thus False
      using u  v = y  nconjug y_le_x
      using conjugI' nle_le pref_same_len primroot_emp primroot_len_le primroot_pref swap_len by metis
  qed
  with that[of m u "u¯>y" l, OF hd ws  ya = p  x[folded y @ m  u = ya], folded yb  last ws = x  s u  v = y,
      unfolded lq_triv lassoc cancel_right, OF _ _ u  ε v  ε this[unfolded lassoc]]
  show thesis
    using y @ m  u  v  y @ l = y @ k[folded ya  yb = y @ k y @ m  u =  ya, unfolded rassoc cancel, folded u  v = y] by blast
qed

lemma last_ws: "last ws = x"
proof(rule ccontr)
  assume "last ws  x"
  hence "last ws = y"
    using last_ws_lists by blast
  obtain l m u v where "(hd ws)y@mu = px" and "v  y@l  (last ws) = x  s" and
    "uv = y" and "u  ε" and "v  ε" and "x  v  u  (v  u)  x"
    using l_mE by metis
  note y_le_x[folded u  v = y,unfolded swap_len[of u]]

  from v  y@l  (last ws) = x  s[unfolded last ws = y, folded u  v = y]
  have "x ≤p (v  u)@Suc l  v"
    unfolding pow_Suc' rassoc using append_eq_appendI prefix_def shift_pow by metis
  moreover have "(v  u) @ Suc l  v ≤p (v  u)  (v  u) @ Suc l  v"
    unfolding lassoc pow_comm[symmetric] using rassoc by blast
  ultimately have "x ≤p (v  u)  x"
    using pref_keeps_per_root by blast

  thus False
  proof (cases "m = 0")
    assume "m  0"
    have "v  u ≤s x"
      using (hd ws)y@mu = px[folded u  v = y, unfolded pow_pos'[OF m  0[unfolded neq0_conv]] rassoc]
        suf_extD[THEN suf_prod_long[OF _ |v  u|  |x|], of p "hd ws  (u  v) @ (m-1)  u", unfolded rassoc] by simp
    have [symmetric]: "(v  u)  x = x  (v  u)"
      using root_suf_comm'[OF  x ≤p (v  u)  x (v  u) ≤s x].
    thus False
      using x  v  u  (v  u)  x by blast
  next
    assume "m = 0"
    thus False
    proof (cases "hd ws = y")
      assume "hd ws = y"
      have "p  (x  x)  s = y@Suc (Suc (Suc (m+l)))"
        unfolding rassoc v  y@l  (last ws) = x  s[unfolded last ws = y, symmetric] power_Suc2
        unfolding lassoc (hd ws)y@mu = px[unfolded hd ws = y, symmetric]
          u  v = y[symmetric]
        by comparison
      have "ρ x  ρ y"
      proof (rule fac_two_conjug_primroot')
        show "x  ε" and "y  ε" using bin_fst_nemp bin_snd_nemp.
        show "x  x ≤f  y@Suc (Suc (Suc (m+l)))"
          using facI[of "xx" p s,unfolded p  (x  x)  s = y@Suc (Suc (Suc (m+l)))].
        show "x  x ≤f x@2"
          unfolding pow_two by blast
        show "|x| + |y|  |x  x|"
          using y_le_x unfolding lenmorph by auto
      qed
      thus False
        unfolding x_root  using nconjug y_le_x
        by (metis conjug_len long_pref primroot_pref)
    next
      assume "hd ws  y"
      hence "hd ws = x"
        using hd_ws_lists by auto

      have "x ≤s x  u"
        using  (hd ws)y@mu = px[unfolded m = 0 hd ws = x pow_zero emp_simps]
        by (simp add: suffix_def)
      have "v  u ≤p x"
        using x ≤p (v  u)  x y_le_x[folded u  v = y,unfolded swap_len[of u]]
          pref_prod_long by blast
      hence "|v  u| < |x|"
        using  nconjug conjugI[OF _ u  v = y, of x] |v  u|  |x|
          le_neq_implies_less pref_same_len by blast
      have "u  v = v  u"
      proof (rule pref_suf_pers_short[reversed])
        from x ≤p (v  u)@Suc l  v
        show "x ≤p ((v  u)  v)  (u  v)@l"
          by comparison
        show "(u  v) @ l  {v, u}"
          by blast
      qed fact+
      from pref_extD[OF v  u ≤p x[folded u  v = v  u]]
      have "x  u = u  x"
        using x ≤s x  u suf_root_pref_comm by blast
      with comm_trans[OF this u  v = v  u[symmetric] u  ε]
      have "x  (v  u) = (v  u)  x"
        using comm_prod by blast
      thus False
        using x  v  u  (v  u)  x by blast
    qed
  qed
qed

lemma rev_square_interp:
  "square_interp (rev x) (rev y) (rev s) (rev p) (rev (map rev ws))"
proof (unfold_locales)
  show "rev (map rev ws)  lists {rev x, rev y}"
    using ws_lists  by force
  show "|rev y|  |rev x|"
    using y_le_x by simp
  show "¬ (rev x)  (rev y)"
    by (simp add: conjug_rev_conv nconjug)
  show "primitive (rev x)"
    using prim_x
    by (simp_all add: prim_rev_iff)
  show "(rev s) [rev x, rev x] (rev p) 𝒟 (rev (map rev ws))"
  proof
    show "(rev s) (concat [rev x, rev x]) (rev p)  rev (map rev ws)"
      using interp rev_fac_interp by fastforce
    show "p1 p2. p1 ≤p [rev x, rev x]  p2 ≤p rev (map rev ws)  rev s  concat p1  concat p2"
    proof
      fix p1' p2' assume "p1' ≤p [rev x, rev x]" and "p2' ≤p rev (map rev ws)" and "rev s  concat p1' = concat p2'"
      obtain p1 p2 where "p1'  p1 = [rev x, rev x]" and "p2'p2 = rev (map rev ws)"
        using p1' ≤p [rev x, rev x] p2' ≤p rev (map rev ws) by (auto simp add: prefix_def)
      hence "rev s  (concat p1'  concat p1)  rev p = concat p2'  concat p2"
        unfolding concat_morph[symmetric] using (rev s) (concat[rev x,rev x]) (rev p)  rev (map rev ws)
          fac_interpD(3) by force
      from this[unfolded lassoc, folded rev s  concat p1' = concat p2', unfolded rassoc cancel]
      have "concat p1  rev p = concat p2".
      hence "p  (concat (rev  (map rev p1))) = concat (rev (map rev p2))"
        using rev_append rev_concat rev_map rev_rev_ident by metis
      have "rev  (map rev p1) ≤p [x,x]"
        using arg_cong[OF p1'  p1 = [rev x, rev x], of "λ x. rev (map rev x)", unfolded map_append rev_append]
        by fastforce
      have "rev  (map rev p2) ≤p ws"
        using arg_cong[OF p2'p2 = rev (map rev ws), of "λ x. rev (map rev x)", unfolded map_append rev_append rev_map
            rev_rev_ident map_rev_involution, folded rev_map] by blast
      from disjoint[OF rev  (map rev p1) ≤p [x,x] rev  (map rev p2) ≤p ws]
      show False
        using p  (concat (rev  (map rev p1))) = concat (rev (map rev p2)) by blast
    qed
  qed
  show "rev x  rev y  rev y  rev x"
    using  non_comm unfolding comm_rev_iff.
qed

lemma hd_ws: "hd ws = x"
  using square_interp.last_ws[reversed, OF rev_square_interp]
  unfolding hd_map[OF ws_nemp]
  by simp

lemma p_pref: "p <p x"
  using fac_interpD(1) hd_ws interp by auto

lemma s_suf: "s <s x"
  using fac_interpD(2) last_ws interp by auto

end

subsection ‹Locale with additional parameters›
  ― ‹Obtained parameters added into the context, we show that there is just one @{term y} in @{term ws},
      that is, that @{term "m = 0"} and @{term "l = 0"}.
      The proof harvests results obtained in the section "Lemmas for covered x square"
›

locale square_interp_plus = square_interp +
  fixes l m u v
  assumes fst_x: "x  y@m  u = p  x" and
    snd_x: "v  y@l  x = x  s" and
    uv_y:  "u  v = y" and
    u_nemp: "u  ε" and v_nemp: "v  ε" and
    vu_x_non_comm: "x  (v  u)  (v  u)  x"
begin

interpretation  binary_code x y
  using non_comm by unfold_locales


lemma rev_square_interp_plus:  "square_interp_plus (rev x) (rev y) (rev s) (rev p) (rev (map rev ws)) m l (rev v) (rev u)"
proof-
  note fac_interpD[OF interp, unfolded hd_ws last_ws]
  note s <s x[unfolded strict_suffix_to_prefix]
  note p <p x[unfolded spref_rev_suf_iff]

  interpret i: square_interp "(rev x)" "(rev y)" "(rev s)" "(rev p)" "(rev (map rev ws))"
    using rev_square_interp.
  show ?thesis
    by standard
       (simp_all del: rev_append add: rev_pow[symmetric] rev_append[symmetric],
        simp_all add: fst_x snd_x uv_y v_nemp u_nemp vu_x_non_comm[symmetric, unfolded rassoc])
qed

subsubsection ‹Exactly one of the exponents is zero: impossible.›

text ‹Uses lemma @{thm pref_suf_pers_short} and exploits the symmetric interpretation.›

lemma fst_exp_zero: assumes "m = 0" and "0 < l" shows "False"
proof (rule notE[OF vu_x_non_comm])
  note y_le_x[folded uv_y, unfolded swap_len[of u]]
  have "x ≤p (v  (u  v) @ l)  x"
    unfolding rassoc using snd_x[folded uv_y] by blast
  have "v  (u  v) @ l  ε"
    using v_nemp by force
  obtain exp where "x ≤p (v  (u  v) @ l)@exp" "0 < exp"
    using per_root_powE[OF per_rootI[OF x ≤p (v  (u  v) @ l)  x v  (u  v) @ l  ε], of thesis] by blast

  have "x ≤s x  u"
      using fst_x[unfolded m = 0  pow_zero emp_simps] by (simp add: suffix_def)
    have "((v  u)  v)  ((u  v)@(l-1))  (v  (u  v) @ l)@(exp-1) = (v  (u  v) @ l)@exp"
      (is "((v  u)  v)  ?suf = (v  (u  v) @ l)@exp")
      using 0 < l 0 < exp by comparison
    have "v  u ≤p x"
      using pref_prod_longer[OF x ≤p (v  (u  v) @ l)  x[unfolded rassoc] _ |v  u|  |x|]
      unfolding pow_pos[OF 0 < l] rassoc by blast
    hence "|v  u| < |x|"
      using  nconjug conjugI[OF _ uv_y, of x] |v  u|  |x|
        le_neq_implies_less pref_same_len by blast
    have "u  v = v  u"
  proof (rule pref_suf_pers_short[reversed])
    show "x ≤p ((v  u)  v)  ?suf"
      unfolding ((v  u)  v)  ?suf = (v  (u  v) @ l)@exp by fact
    show "((u  v)@(l-1))  (v  (u  v) @ l)@(exp-1)  {v,u}"
      by (simp add: gen_in hull_closed power_in)
  qed fact+
  show "x  v  u = (v  u)  x"
    using root_suf_comm[OF _ x ≤s x  u] pref_keeps_per_root comm_trans[OF u  v = v  u[symmetric] _ u_nemp, symmetric] v  u ≤p x  comm_prod  prefI
    by metis
qed

lemma snd_exp_zero: assumes "0 < m" and "l = 0" shows "False"
  using square_interp_plus.fst_exp_zero[OF rev_square_interp_plus, reversed,
      rotated, OF assms].

subsubsection ‹Both exponents positive: impossible›

lemma both_exps_pos: assumes "0 < m" and "0 < l" shows "False"
proof-
  note fac_interpD[OF interp, unfolded hd_ws last_ws]
  have "|p|  |x|" and "|s|  |x|"
    using pref_len[OF sprefD1[OF p <p x]] suf_len[OF ssufD1[OF s <s x]].

  have "x ≤p (v  (u  v)@l)  x"
    (is "x ≤p ?pref  x")
    using snd_x[folded uv_y] by force
  moreover have "x ≤s x  ((u  v)@m  u)"
    (is "x ≤s x  ?suf")
    using fst_x[folded uv_y] by force

  ultimately interpret pref_suf_pers x u v l m
    using 0 < l 0 < m by unfold_locales

  have "?pref ≤p x"
    using snd_x[folded uv_y  rassoc, symmetric]  eqd[reversed,  OF _ |s|  |x|]  by blast
  have "?suf ≤s x"
    using fst_x[folded uv_y, symmetric]  eqd[OF _ |p|  |x|]  by blast

  have in_particular: "commutes {u,v,x}  x  (vu) = (vu)  x"
    unfolding commutes_def by (rule comm_prod) blast+

―  ‹Case analysis based on (slightly modified) lemmas for covered x square.›

  note  no_overlap_comm = no_overlap[THEN in_particular] and
    short_overlap_comm = short_overlap[THEN in_particular] and
    medium_overlap_comm = medium_overlap[THEN in_particular] and
    large_overlap_conjug = pref_suf_pers_large_overlap[OF ?pref ≤p x ?suf ≤s x, of "vu"]

  consider
    (no_overlap)     "|?pref| + |?suf|  |x|" |
    (short_overlap)  "|x| <  |?pref| + |?suf|   |?pref| + |?suf|  |x| + |u|" |
    (medium_overlap) "|x| + |u| < |?pref| + |?suf|   |?pref| + |?suf| < |x| + |u  v|" |
    (large_overlap)  "|x| + |v  u|   |?pref| + |?suf|"
    unfolding swap_len[of v] by linarith
  thus False
  proof (cases)
    case no_overlap
    then show False
      using no_overlap_comm vu_x_non_comm 0 < l 0 < m by blast
  next
    case short_overlap
    then show False
      using short_overlap_comm vu_x_non_comm by blast
  next
    case medium_overlap
    then show False
      using medium_overlap_comm vu_x_non_comm by blast
  next
    case large_overlap
    show False
      thm large_overlap_conjug nconjug
    proof (rule notE[OF vu_x_non_comm], rule large_overlap_conjug[OF _ _ large_overlap])
      have "(u  v) @ (l-1) ≤p (u  v) @ Suc (l-1)"
        using pref_pow_ext by blast
      thus "v  (u  v) @ l ≤p (v  u)  v  (u  v) @ l"
        unfolding pow_pos[OF 0 < l] pow_Suc rassoc pref_cancel_conv.
      show "(u  v) @ m  u ≤s ((u  v) @ m  u)  v  u"
        by comparison
    qed
  qed
qed

thm suf_cancel_conv

end

subsection ‹Back to the main locale›

context square_interp

begin

definition u where "u = x¯>(p  x)"
definition v where "v = (x  s)<¯x"

lemma cover_xyx: "ws = [x,y,x]" and vu_x_non_comm: "x  (v  u)  (v  u)  x" and uv_y: "u  v = y" and
  px_xu:  "p  x = x  u" and  vx_xs:  "v  x = x  s" and u_nemp: "u  ε" and v_nemp: "v  ε"
proof-
     obtain k where ws: "[x]  [y]@k  [x] = ws"
    using kE[unfolded hd_ws last_ws].
  obtain m u' v' l where  "x  y @ m  u' = p  x" and "v'  y @ l  x = x  s" and "u'  v' = y"
  and "u'  ε" and "v'  ε" and "x  v'  u'  (v'  u')  x"
    using l_mE[unfolded hd_ws last_ws].
  then interpret square_interp_plus x y p s ws l m u' v'
    by (unfold_locales)
  have "m = 0" and "l = 0" and "y  ε"
    using both_exps_pos snd_exp_zero fst_exp_zero u'  v' = y u'  ε by blast+
  have "u' = u"
    unfolding u_def
    using conjug_lq[OF fst_x[unfolded m = 0 pow_zero emp_simps, symmetric]].
  have "v' = v"
    unfolding v_def
    using conjug_lq[reversed, OF snd_x[unfolded l = 0 pow_zero emp_simps, symmetric]].
  have "x  y @ m  (u'  v')  y@l  x = concat ws"
    unfolding interpret_concat[symmetric] using fst_x snd_x by force
  from this[folded ws, unfolded u'  v' = y m = 0 l = 0 pow_zero emp_simps]
  have "k = 1"
    unfolding eq_pow_exp[OF y  ε, of k 1, symmetric] pow_1 concat_morph concat_pow
    by simp
  from ws[unfolded this pow_1]
    show "ws = [x,y,x]" by simp
  show "u  v  = y"
    unfolding u' = u[symmetric] v' = v[symmetric] by fact+
  show  "p  x = x  u"
    using x  y @ m  u' = p  x[unfolded m = 0 u' = u pow_zero emp_simps, symmetric].
  show  " v  x = x  s"
    using v'  y @ l  x = x  s[unfolded l = 0 v' = v pow_zero emp_simps].
  show "x  (v  u)  (v  u)  x"
    using x  v'  u'  (v'  u')  x[unfolded u' = u v' = v].
  show "u  ε" and "v  ε"
    using u'  ε v'  ε unfolding u' = u v' = v.
qed

lemma cover: "x  y  x = p  x  x  s"
  using interpret_concat cover_xyx by auto

lemma conjug_facs: "ρ u  ρ v"
proof-
  note sufI[OF px_xu]
  have "u  ε"
    using p_nemp px_xu by force
  obtain expu where "x <s u@ expu" "0 < expu"
    using per_root_powE[reversed, OF per_rootI[reversed, OF x ≤s x  u u  ε]].
  hence "x ≤f u@ expu"
    using ssufD1 by blast

  note prefI[OF vx_xs[symmetric]]
  have "v  ε"
    using s_nemp vx_xs by force
  obtain expv where "x <p v@expv" "0 < expv"
    using per_root_powE[OF per_rootI[OF x ≤p v  x v  ε]].
  hence "x ≤f v@expv"  by blast

  show "ρ u  ρ v"
  proof(rule fac_two_conjug_primroot'[OF x ≤f u@expu x ≤f v@expv u  ε v  ε])
    show "|u| + |v|  |x|"
      using y_le_x[folded uv_y, unfolded lenmorph] by fastforce
  qed
qed

term square_interp.v

― ‹We have a detailed information about all words›
lemma bin_sq_interpE: obtains r t m k l
  where "(t  r)@k = u" and  "(r  t)@l = v" and
    "(r  t)@m  r = x" and "(t  r)@k  (r  t)@ l = y"
    and "(r  t)@k = p" and  "(t  r)@ l = s"  and "r  t  t  r" and
    "0 < k" and "0 < m" and "0 < l"
proof-

  obtain r t k m where "(r  t)@ k = p" and "(t  r)@ k = u" and "(r  t)@m  r = x" and
    "t  ε" and "0 < k"  and "primitive (r  t)"
    using conjug_eq_primrootE[OF px_xu p_nemp].
  have "t  r = ρ u"
    using  prim_conjug[OF primitive (r  t), THEN primroot_unique[OF u_nemp], OF conjugI' (t  r)@k = u[symmetric]]..

  have "0 < m"
  proof (rule ccontr)
    assume "¬ 0 < m"
    hence "x = r" using (r  t)@m  r = x by simp
    show False
      using 0 < k (r  t) @ k = p x = r comp_pows_pref_zero p_pref by blast
  qed


  from (r  t)@m  r = x[unfolded pow_pos[OF 0 < m]]
  have "r  t ≤p x"
    by auto

  have "r  t = ρ v"
  proof (rule ruler_eq_len[of "ρ v" "x" "r  t", symmetric])
    have "|ρ v|  |x|"
      unfolding conjug_len[OF conjug_facs, symmetric] t  r = ρ u[symmetric]
      unfolding (r  t)@m  r = x[symmetric] pow_pos[OF 0 < m]
        lenmorph pow_len  by auto
    from ruler_le[OF _ _ this, of "v  x"]
    show "ρ v ≤p x"
      using vx_xs prefI prefix_prefix primroot_pref v_nemp by metis
    show "r  t ≤p x" by fact
    show "|ρ v| = |r  t|"
      unfolding conjug_len[OF conjug_facs, symmetric, folded t  r = ρ u] lenmorph by simp
  qed

  then obtain l where "(r  t)@ l = v" and "0 < l"
    using primroot_expE v_nemp by metis

  have "(t  r)@ l = s"
    using vx_xs[folded (r  t)@m  r = x (r  t)@ l = v, unfolded lassoc pows_comm[of _ _ m],
        unfolded rassoc cancel, unfolded shift_pow cancel].

  have "r  t  t  r"
  proof
    assume "r  t = t  r"
    hence aux: "r  (t  r) @ e = (t  r) @ e  r" for e
      by comparison
    have "x  (v  u) = (v  u)  x"
      unfolding (t  r) @  k = u[symmetric] (r  t) @ l = v[symmetric]
      unfolding  (r  t)@m  r = x[symmetric]  add_exps[symmetric] r  t = t  r aux rassoc
      unfolding lassoc cancel_right add_exps[symmetric]
      by (simp add: add.commute)
    thus False
      using vu_x_non_comm by blast
  qed

  show thesis
    using that[OF (t r)@ k = u (r  t) @ l = v (r  t)@m  r = x
        uv_y[folded (t r)@ k = u (r  t) @ l = v] (r  t) @ k = p (t  r) @ l = s  r  t  t  r
        0 < k 0 < m 0 < l].
qed

end

subsection ‹Locale: Extendable interpretation›
text ‹Further specification follows from the assumption that the interpretation is extendable,
 that is, the covered @{term "xx"} is a factor of a word composed of @{term "{x,y}"}. Namely, @{term u} and @{term v} are then conjugate by @{term x}.›

locale square_interp_ext = square_interp +
  assumes p_extend: " pe. pe  {x,y}  p ≤s pe" and
    s_extend: " se. se  {x,y}  s ≤p se"

begin

lemma s_pref_y: "s ≤p y"
proof-
  obtain sy ry eu ev ex
    where "(ry  sy)@eu = u" and  "(sy  ry)@ ev = v" and
      "(sy  ry)@ eu = p" and  "(ry  sy)@ ev = s" and
      "(sy  ry)@ ex  sy = x" and "sy  ry  ry  sy" and
      "0 < eu" and "0 < ev" and "0 < ex"
    using bin_sq_interpE.

  obtain se where "se  {x,y}" and  "s ≤p se"
    using s_extend by blast
  hence "se  ε" using s_nemp by force

  from (sy  ry)@ ex  sy = x
  have "sy  ry ≤p x"
    unfolding pow_pos[OF 0 < ex] rassoc by force

  have "x ≤p se  y ≤p se"
    using  se  ε hull.cases[OF se  {x,y}, of "x ≤p se  y ≤p se"]
      prefix_append triv_pref two_elem_cases by blast
  moreover have "¬ x ≤p se"
  proof
    assume "x ≤p se"
    from ruler_eq_len[of "sy  ry" se "ry  sy", OF pref_trans[OF sy  ry ≤p x this]]
    show False
      using s ≤p se[folded (ry  sy)@ ev = s[unfolded pow_pos[OF 0 < ev]]] sy  ry  ry  sy by (force simp add: prefix_def)
  qed
  ultimately have y_pref_se: "y ≤p se" by blast

  from ruler_le[OF s ≤p se this]
  show "s ≤p y"
    using lenarg[OF vx_xs] unfolding uv_y[symmetric] lenmorph by linarith
qed

lemma rev_square_interp_ext: "square_interp_ext (rev x) (rev y) (rev s) (rev p) (rev (map rev ws))"
proof-
  interpret i: square_interp "(rev x)" "(rev y)" "(rev s)" "(rev p)" "(rev (map rev ws))"
    using rev_square_interp.
  show ?thesis
  proof
    show "pe. pe  {rev x, rev y}  rev s ≤s pe"
      using  s_pref_y unfolding pref_rev_suf_iff by blast
    obtain pe where "pe  {x, y}" and  "p ≤s pe"
      using p_extend by blast
    hence "rev pe  {rev x, rev y}"
      by (simp add: rev_hull rev_in_conv)
    thus "se. se  {rev x, rev y}  rev p ≤p se"
      using p ≤s pe[unfolded suf_rev_pref_iff prefix_def] rev_rev_ident by blast
  qed
qed

lemma p_suf_y: "p ≤s y"
proof-
  interpret i: square_interp_ext "(rev x)" "(rev y)" "(rev s)" "(rev p)" "(rev (map rev ws))"
    using rev_square_interp_ext.

  from i.s_pref_y[reversed]
  show "p ≤s y".
qed

theorem bin_sq_interp_extE: obtains r t k m where  "(r  t)@m  r = x" and  "(t  r)@k  (r  t)@ k = y"
  "(r  t)@ k = p" and "(t  r)@  k = s" and "r  t  t  r" and "u = s" and "v = p" and "|p| = |s|" and
  "0 < k" and "0 < m"
proof-
  obtain r t k k' m
    where u: "(t  r)@ k = u" and v:  "(r  t)@ k' = v" and
      p: "(r  t)@ k = p" and s: "(t  r)@ k' = s" and
      x: "(r  t)@ m  r = x" and code: "r  t  t  r" and
      "0 < k'" "0 < m" "0 < k"
    using bin_sq_interpE.
  have "|u  v| = |s  p|"
    using lenarg[OF px_xu, unfolded lenmorph] lenarg[OF vx_xs, unfolded lenmorph] by simp
  hence "u  v = s  p"
    unfolding uv_y using s_pref_y p_suf_y by (auto simp add: prefix_def suffix_def)
  note eq = u  v = s  p[unfolded  (t  r)@ k = u[symmetric] (r  t)@ k' = v[symmetric],
      unfolded (t  r)@ k' = s[symmetric] (r  t)@ k = p[symmetric]]
  from pows_comm_comm[OF this]
  have "k = k'"
    using r  t  t  r eqd_eq(1)[OF _ swap_len, of t r] by fastforce
  have "|