diff --git a/thys/Binary_Code_Imprimitive/Binary_Code_Imprimitive.thy b/thys/Binary_Code_Imprimitive/Binary_Code_Imprimitive.thy
new file mode 100644
--- /dev/null
+++ b/thys/Binary_Code_Imprimitive/Binary_Code_Imprimitive.thy
@@ -0,0 +1,1168 @@
+(*  Title:      Binary Code Imprimitive
+    File:       Combinatorics_Words_Interpretations.Binary_Code_Imprimitive
+    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/
+*)
+
+chapter "Binary codes that do not preserve primitivity"
+
+theory Binary_Code_Imprimitive
+  imports 
+    Combinatorics_Words_Graph_Lemma.Glued_Codes 
+    Binary_Square_Interpretation
+begin
+
+text \<open>This theory focuses on the characterization of imprimitive words which are concatenations
+of copies of  two words (forming a binary code). 
+We follow the article @{cite lerest} (mainly Th\'eor\`eme 2.1 and Lemme 3.1),
+while substantially optimizing the proof. See also @{cite spehner} for an earlier result on this question,
+and @{cite Manuch} for another proof.\<close>
+
+section \<open>General primitivity not preserving codes\<close>
+
+context code
+
+begin
+
+text \<open>
+Two nontrivially conjugate elements generated by a code induce a disjoint interpretation.\<close>
+
+lemma shift_disjoint:
+  assumes  "ws \<in> lists \<C>" and "ws' \<in> lists \<C>" and  "z \<notin> \<langle>\<C>\<rangle>" and "z \<cdot> concat ws = concat ws' \<cdot> z" 
+    "us \<le>p ws\<^sup>@n" and "vs \<le>p ws'\<^sup>@n" 
+  shows "z \<cdot> concat us \<noteq> concat vs"
+  using \<open>z \<notin> \<langle>\<C>\<rangle>\<close>
+proof (elim contrapos_nn)
+  assume "z \<cdot> concat us = concat vs" 
+  have "z \<noteq> \<epsilon>"
+    using \<open>z \<notin> \<langle>\<C>\<rangle>\<close> by blast 
+  obtain us' where "ws\<^sup>@n = us \<cdot> us'"
+    using  prefixE[OF \<open>us \<le>p ws\<^sup>@n\<close>].    
+  obtain vs' where "ws'\<^sup>@n = vs \<cdot> vs'"
+    using  prefixE[OF \<open>vs \<le>p ws'\<^sup>@n\<close>].  
+  from conjug_pow[OF \<open>z \<cdot> concat ws = concat ws' \<cdot> z\<close>[symmetric], symmetric]
+  have "z \<cdot> concat (ws\<^sup>@n)  = concat (ws'\<^sup>@n) \<cdot> z"
+    unfolding concat_pow.
+  from this[ unfolded \<open>ws\<^sup>@n = us \<cdot> us'\<close> \<open>ws'\<^sup>@n = vs \<cdot> vs'\<close> concat_morph rassoc
+      \<open>z \<cdot> concat us = concat vs\<close>[symmetric] cancel]
+  have "concat vs' \<cdot> z = concat us'"..
+  show "z \<in> \<langle>\<C>\<rangle>"
+  proof (rule stability)
+    have "us \<in> lists \<C>" and "us' \<in> lists \<C>" and "vs \<in> lists \<C>" and "vs' \<in> lists \<C>"
+      using \<open>ws \<in> lists \<C>\<close> \<open>ws' \<in> lists \<C>\<close>  \<open>ws'\<^sup>@n = vs \<cdot> vs'\<close> \<open>ws\<^sup>@n = us \<cdot> us'\<close>
+      by inlists
+    thus "z \<cdot> concat us \<in> \<langle>\<C>\<rangle>" and "concat vs' \<in> \<langle>\<C>\<rangle>" and "concat us \<in> \<langle>\<C>\<rangle>" and "concat vs' \<cdot> z \<in> \<langle>\<C>\<rangle>"
+      unfolding \<open>concat vs' \<cdot> z = concat us'\<close> \<open>z \<cdot> concat us = concat vs\<close>
+      by (simp_all add: concat_in_hull') 
+  qed
+qed
+
+text\<open>This in particular yields a disjoint extendable interpretation of any prefix\<close>
+
+lemma  shift_interpret:
+  assumes  "ws \<in> lists \<C>" and "ws' \<in> lists \<C>"  and "z \<notin> \<langle>\<C>\<rangle>" and
+    conjug: "z \<cdot> concat ws = concat ws' \<cdot> z" and "\<^bold>|z\<^bold>| < \<^bold>|concat ws'\<^bold>|"
+    and "us \<le>p ws" and "us \<noteq> \<epsilon>"
+  obtains p s vs ps ss where  "p (concat us) s \<sim>\<^sub>\<I> vs" and "ps \<cdot> vs \<le>p ws' \<cdot> ws'" 
+    and "us \<cdot> ss = ws \<cdot> ws" and
+    "concat ps \<cdot> p = z" and "s \<le>p concat ss" and "p \<le>s concat ws" and "vs \<in> lists \<C>"
+    "\<And> us' vs'. us' \<le>p us \<Longrightarrow> vs' \<le>p vs \<Longrightarrow> p \<cdot> concat us' \<noteq> concat vs'" and "p \<noteq> \<epsilon>" and "s \<noteq> \<epsilon>"
+proof-
+  have "ws' \<cdot> ws' \<in> lists \<C>"
+    using \<open>ws' \<in> lists \<C>\<close> by inlists
+  have "concat us \<noteq> \<epsilon>"
+    using \<open>us \<noteq> \<epsilon>\<close> unfolding code_concat_eq_emp_iff[OF pref_in_lists[OF \<open>us \<le>p ws\<close> \<open>ws \<in> lists \<C>\<close>]].
+  have "\<^bold>|concat ws'\<^bold>| = \<^bold>|concat ws\<^bold>|"
+    using lenarg[OF conjug, unfolded lenmorph] by linarith
+  have "z \<cdot> concat(ws \<cdot> ws) = concat (ws' \<cdot> ws') \<cdot> z"
+    unfolding rassoc concat_morph conjug[symmetric] unfolding lassoc cancel_right 
+    using conjug.
+  hence "concat (ws' \<cdot> ws') \<le>p z \<cdot> concat (ws \<cdot> ws)" 
+    by blast
+  have "z \<cdot> concat ws \<le>p concat (ws' \<cdot> ws')"
+    unfolding concat_morph conjug pref_cancel_conv using eq_le_pref[OF conjug less_imp_le[OF \<open>\<^bold>|z\<^bold>| < \<^bold>|concat ws'\<^bold>|\<close>]].
+  from prefixE[OF pref_shorten[OF pref_concat_pref[OF \<open>us \<le>p ws\<close>] this], unfolded rassoc]
+  obtain su where fac_u[symmetric]: "concat (ws' \<cdot> ws') = z \<cdot> concat us \<cdot> su".  
+
+  from obtain_fac_interpret[OF fac_u \<open>concat us \<noteq> \<epsilon>\<close>]
+  obtain ps ss' p s vs where "p (concat us) s \<sim>\<^sub>\<I> vs" and
+    "ps \<cdot> vs \<cdot> ss' = ws' \<cdot> ws'" and "concat ps \<cdot> p = z" and "s \<cdot> concat ss' = su".
+  note fac_interpretE[OF \<open>p (concat us) s \<sim>\<^sub>\<I> vs\<close>]
+
+  from prefixE[OF pref_ext[OF \<open>us \<le>p ws\<close>]]
+  obtain ss where [symmetric]:"ws \<cdot> ws = us \<cdot> ss".
+
+  have "ps \<cdot> vs \<le>p ws' \<cdot> ws'"
+    unfolding \<open>ps \<cdot> vs \<cdot> ss' = ws' \<cdot> ws'\<close>[symmetric] lassoc using triv_pref.
+
+  hence "vs \<in> lists \<C>"
+    using \<open>ws'\<in> lists \<C>\<close>
+    by inlists
+
+  from \<open>concat (ws' \<cdot> ws') \<le>p z \<cdot> concat (ws \<cdot> ws)\<close>[folded arg_cong[OF \<open>ps \<cdot> vs \<cdot> ss' = ws' \<cdot> ws'\<close>, of concat] \<open>us \<cdot> ss = ws \<cdot> ws\<close>,
+      unfolded concat_morph, folded \<open>p \<cdot> concat us \<cdot> s = concat vs\<close> \<open>concat ps \<cdot> p = z\<close>,
+      unfolded rassoc pref_cancel_conv]
+  have "s \<le>p concat ss"
+    using append_prefixD by blast
+
+  have "\<^bold>|p\<^bold>| \<le> \<^bold>|concat ws\<^bold>|"
+    using  \<open>\<^bold>|z\<^bold>| < \<^bold>|concat ws'\<^bold>|\<close>[folded lenarg[OF \<open>concat ps \<cdot> p = z\<close>], unfolded \<open>\<^bold>|concat ws'\<^bold>| = \<^bold>|concat ws\<^bold>|\<close>]
+    by simp
+
+  with eqd[reversed, OF conjug[folded \<open>concat ps \<cdot> p = z\<close>, unfolded lassoc, symmetric] this]
+  have "p \<le>s concat ws"
+    by blast
+
+  have disjoint: "p \<cdot> concat us' \<noteq> concat vs'" if "us' \<le>p us" "vs' \<le>p vs" for us' vs'
+  proof
+    have "us' \<le>p ws \<cdot> ws"
+      using \<open>us \<le>p ws\<close> \<open>us' \<le>p us\<close> by auto
+    have "ps \<cdot> vs' \<le>p ws' \<cdot> ws'" 
+      using \<open>vs' \<le>p vs\<close> \<open>ps \<cdot> vs \<le>p ws' \<cdot> ws'\<close> pref_trans same_prefix_prefix by metis 
+    assume "p \<cdot> concat us' = concat vs'"
+    hence "z \<cdot> concat us' = concat (ps \<cdot> vs')"
+      unfolding concat_morph \<open>concat ps \<cdot> p = z\<close>[symmetric] rassoc cancel.
+    thus False
+      using shift_disjoint[OF \<open>ws \<in> lists \<C>\<close> \<open>ws' \<in> lists \<C>\<close> \<open>z \<notin> \<langle>\<C>\<rangle>\<close>
+          \<open>z \<cdot> concat ws = concat ws' \<cdot> z\<close> \<open>us' \<le>p ws \<cdot> ws\<close>[folded pow_two] \<open>ps \<cdot> vs' \<le>p ws' \<cdot> ws'\<close>[folded pow_two]] by fast
+  qed
+  from disjoint[of \<epsilon> \<epsilon>] 
+  have "p \<noteq> \<epsilon>" by blast
+  have "s \<noteq> \<epsilon>"
+    using \<open>p \<cdot> concat us \<cdot> s = concat vs\<close> disjoint by auto
+  
+  from that[OF \<open>p (concat us) s \<sim>\<^sub>\<I> vs\<close> \<open>ps \<cdot> vs \<le>p ws' \<cdot> ws'\<close> \<open>us \<cdot> ss = ws \<cdot> ws\<close> \<open>concat ps \<cdot> p = z\<close> \<open>s \<le>p concat ss\<close> \<open>p \<le>s concat ws\<close> \<open>vs \<in> lists \<C>\<close>
+      disjoint \<open>p \<noteq> \<epsilon>\<close> \<open> s \<noteq> \<epsilon>\<close>]
+  show thesis.
+qed
+
+text\<open>The conditions are in particular met by imprimitivity witnesses\<close>
+
+lemma imprim_witness_shift:
+  assumes "ws \<in> lists \<C>" and "primitive ws" and "\<not> primitive (concat ws)"
+  obtains z n  where "concat ws = z\<^sup>@Suc(Suc n)" "z \<notin> \<langle>\<C>\<rangle>" and "z \<cdot> concat ws = concat ws \<cdot> z" and "\<^bold>|z\<^bold>| < \<^bold>|concat ws\<^bold>|"
+proof-
+  have "concat ws \<noteq> \<epsilon>" 
+    using \<open>primitive ws\<close>  emp_concat_emp'[OF \<open>ws \<in> lists \<C>\<close>] emp_not_prim by blast 
+  obtain z n where [symmetric]: "z\<^sup>@Suc(Suc n) = concat ws"
+    using not_prim_primroot_expE[OF \<open>\<not> primitive (concat ws)\<close> \<open>concat ws \<noteq> \<epsilon>\<close>, of thesis] by force
+
+  hence "z \<noteq> \<epsilon>" 
+    using \<open>concat ws \<noteq> \<epsilon>\<close>  by force  
+
+  have "z \<notin> \<langle>\<C>\<rangle>" 
+  proof
+    assume "z \<in> \<langle>\<C>\<rangle>" 
+    then obtain zs where "zs \<in> lists \<C>" and "concat zs = z"
+      using hull_concat_lists0 by blast 
+    from is_code[OF \<open>ws \<in> lists \<C>\<close> pow_in_lists[OF \<open>zs \<in> lists \<C>\<close>],
+        unfolded concat_pow \<open>concat ws = z\<^sup>@Suc(Suc n)\<close> \<open>concat zs = z\<close>]
+    show False
+      using \<open>primitive ws\<close> pow_not_prim by blast 
+  qed   
+
+  have "\<^bold>|z\<^bold>| < \<^bold>|concat ws\<^bold>|"
+    unfolding lenarg[OF \<open>concat ws = z\<^sup>@Suc(Suc n)\<close>, unfolded lenmorph pow_len]
+    using nemp_len[OF \<open>z \<noteq> \<epsilon>\<close>] by simp
+
+  from that[OF \<open>concat ws = z\<^sup>@Suc(Suc n)\<close> \<open>z \<notin> \<langle>\<C>\<rangle>\<close> _  this]
+  show thesis
+    unfolding \<open>concat ws = z\<^sup>@Suc(Suc n)\<close>  pow_comm by blast
+
+qed
+
+end
+
+section \<open>Covered uniform square\<close>
+
+\<comment> \<open>Showing that two noncommuting words of the same length do not admit a non-trivial interpretation\<close>
+
+lemma cover_xy_xxx: assumes "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and "p \<cdot> x \<cdot> y \<cdot> s = x \<cdot> x \<cdot> x"
+  shows "x = y"
+  using append_assoc assms(1) assms(2) eq_le_pref le_refl long_pref lq_triv prefI pref_comm_eq' by metis 
+
+lemma cover_xy_yyy: assumes "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and eq: "p \<cdot> x \<cdot> y \<cdot> s = y \<cdot> y \<cdot> y"
+  shows "x = y"
+  using cover_xy_xxx[reversed, unfolded rassoc, OF \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close>[symmetric] eq, symmetric]. 
+
+lemma cover_xy_xxy: assumes "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and "s \<noteq> \<epsilon>" and eq: "p \<cdot> x \<cdot> y \<cdot> s = x \<cdot> x \<cdot> y"
+  shows "x = y"
+proof-
+  have "\<^bold>|p\<^bold>| < \<^bold>|x\<^bold>|"
+    using lenarg[OF eq] nemp_pos_len[OF \<open>s \<noteq> \<epsilon>\<close>] unfolding lenmorph by linarith
+  then obtain t where x: "x = p \<cdot> t" and "t \<noteq> \<epsilon>"
+    using eqd[OF eq] by force   
+  from eq[unfolded this rassoc cancel]
+  have "p \<cdot> t = t \<cdot> p" 
+    by mismatch
+  hence "x \<le>p t \<cdot> x"
+    unfolding x by auto 
+  from eq[unfolded x] 
+  have "y \<le>p t \<cdot> y" 
+    using \<open>p \<cdot> t = t \<cdot> p\<close> \<open>p \<cdot> t \<cdot> y \<cdot> s = t \<cdot> p \<cdot> t \<cdot> y\<close> pref_cancel' suf_marker_per_root triv_pref by metis   
+  show "x = y"
+    using same_len_nemp_root_eq[OF \<open>x \<le>p t \<cdot> x\<close> \<open>y \<le>p t \<cdot> y\<close> \<open>t \<noteq> \<epsilon>\<close> \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close>].
+qed
+
+lemma cover_xy_xyy: assumes "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and "p \<noteq> \<epsilon>" and eq: "p \<cdot> x \<cdot> y \<cdot> s = x \<cdot> y \<cdot> y"
+  shows "x = y"
+  using cover_xy_xxy[reversed, unfolded rassoc, OF assms(1)[symmetric] assms(2) eq]..
+
+lemma cover_xy_yyx: assumes "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and eq: "p \<cdot> x \<cdot> y \<cdot> s = y \<cdot> y \<cdot> x"
+  shows "x = y"
+proof-
+  have "\<^bold>|p\<^bold>| \<le> \<^bold>|y\<^bold>|"
+    using lenarg[OF eq]  unfolding lenmorph by linarith
+  then obtain t where y: "y = p \<cdot> t"
+    using eqd[OF eq] by force   
+  from eqd_eq[OF _  \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close>[unfolded y swap_len[of p]], unfolded rassoc,
+      OF eq[unfolded this rassoc cancel]] 
+  have x: "x = t \<cdot> p" by blast
+  from eq[unfolded x y rassoc cancel]
+  have "p \<cdot> t = t \<cdot> p"
+    by mismatch
+  thus "x = y"
+    unfolding x y.. 
+qed
+
+lemma cover_xy_yxx: assumes "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and eq: "p \<cdot> x \<cdot> y \<cdot> s = y \<cdot> x \<cdot> x"
+  shows "x = y"
+  using cover_xy_yyx[reversed, unfolded rassoc, OF assms(1)[symmetric] eq]..
+
+lemma cover_xy_xyx: assumes "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and "p \<noteq> \<epsilon>" and "s \<noteq> \<epsilon>" and eq: "p \<cdot> x \<cdot> y \<cdot> s = x \<cdot> y \<cdot> x"
+  shows "\<not> primitive (x \<cdot> y)"
+proof 
+  assume "primitive (x \<cdot> y)"
+  have "p \<cdot> (x \<cdot> y) \<cdot> (s \<cdot> y) = (x \<cdot> y) \<cdot> (x \<cdot> y)"
+    unfolding lassoc eq[unfolded lassoc].. 
+  from prim_overlap_sqE[OF \<open>primitive (x \<cdot> y)\<close> this]
+  show False
+    using \<open>p \<noteq> \<epsilon>\<close> \<open>s \<noteq> \<epsilon>\<close> by blast
+qed 
+
+lemma cover_xy_yxy: assumes "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and "p \<noteq> \<epsilon>" and \<open>s \<noteq> \<epsilon>\<close> and eq: "p \<cdot> x \<cdot> y \<cdot> s = y \<cdot> x \<cdot> y"
+  shows "\<not> primitive (x \<cdot> y)"
+  using cover_xy_xyx[reversed, unfolded rassoc, OF assms(1)[symmetric] assms(3) assms(2) eq]. 
+
+lemma eq_append_not_prim: "x = y \<Longrightarrow> \<not> primitive (x \<cdot> y)"
+  by (metis append_Nil2 comm_not_prim prim_nemp)
+
+theorem uniform_square_interp: assumes "x\<cdot>y \<noteq> y\<cdot>x" and  "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and "vs \<in> lists {x,y}"
+  and "p  (x \<cdot> y)  s \<sim>\<^sub>\<I> vs" and "p \<noteq> \<epsilon>"
+shows "\<not> primitive (x\<cdot>y)" and  "vs = [x,y,x] \<or> vs = [y,x,y]"
+proof-
+  note fac_interpretE[OF \<open>p  (x \<cdot> y)  s \<sim>\<^sub>\<I> vs\<close>]
+
+  have "vs \<noteq> \<epsilon>"
+    using \<open>p \<cdot> (x \<cdot> y) \<cdot> s = concat vs\<close> assms(5) by force
+  have "\<^bold>|p\<^bold>| < \<^bold>|x\<^bold>|"
+    using prefix_length_less[OF \<open>p <p hd vs\<close>] lists_hd_in_set[OF \<open>vs \<noteq> \<epsilon>\<close> \<open>vs \<in> lists {x,y}\<close>] 
+     \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close>
+    by fastforce  
+  have "\<^bold>|s\<^bold>| < \<^bold>|x\<^bold>|"
+    using suffix_length_less[OF \<open>s <s last vs\<close>] \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> lists_hd_in_set[reversed, OF \<open>vs \<noteq> \<epsilon>\<close> \<open>vs \<in> lists {x,y}\<close>]
+    by fastforce
+  have "\<^bold>|concat vs\<^bold>| = \<^bold>|x\<^bold>| * \<^bold>|vs\<^bold>|"
+    using assms(2-3)
+  proof (induction vs, force)
+    case (Cons a vs)
+    have "\<^bold>|a\<^bold>| = \<^bold>|x\<^bold>|" and "\<^bold>|a # vs\<^bold>| = Suc \<^bold>|vs\<^bold>|" and
+      "\<^bold>|concat (a # vs)\<^bold>| = \<^bold>|a\<^bold>| + \<^bold>|concat vs\<^bold>|" and "\<^bold>|concat vs\<^bold>| = \<^bold>|x\<^bold>| * \<^bold>|vs\<^bold>|"
+      using \<open>a#vs \<in> lists {x,y}\<close> \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> Cons.IH Cons.prems by auto  
+    then show ?case by force
+  qed
+  note leneq = lenarg[OF \<open>p \<cdot> (x \<cdot> y) \<cdot> s = concat vs\<close>, unfolded this lenmorph \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close>[symmetric]]
+  hence "\<^bold>|x\<^bold>| * \<^bold>|vs\<^bold>| < \<^bold>|x\<^bold>| * 4" and  "2 * \<^bold>|x\<^bold>| < \<^bold>|x\<^bold>| * \<^bold>|vs\<^bold>| " 
+    using \<open>\<^bold>|p\<^bold>| < \<^bold>|x\<^bold>|\<close> \<open>\<^bold>|s\<^bold>| < \<^bold>|x\<^bold>|\<close> nemp_pos_len[OF \<open>p \<noteq> \<epsilon>\<close>] by linarith+
+  hence "\<^bold>|vs\<^bold>| = 3"
+    by force
+  hence "s \<noteq> \<epsilon>" 
+    using leneq \<open>\<^bold>|p\<^bold>| < \<^bold>|x\<^bold>|\<close> by force
+  
+  have "x \<noteq> y"
+    using assms(1) by blast
+  with \<open>\<^bold>|vs\<^bold>| = 3\<close> \<open>vs \<in> lists {x,y}\<close> \<open>p \<cdot> (x \<cdot> y) \<cdot> s = concat vs\<close>
+  have "(\<not> primitive (x\<cdot>y)) \<and> (vs = [x,y,x] \<or> vs = [y,x,y])"
+  proof(list_inspection, simp_all)
+    assume "p \<cdot> x \<cdot> y \<cdot> s = x \<cdot> x \<cdot> x" 
+    from cover_xy_xxx[OF \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> this]
+    show False
+      using \<open>x \<noteq> y\<close> by blast
+  next
+    assume "p \<cdot> x \<cdot> y \<cdot> s = x \<cdot> x \<cdot> y" 
+    from cover_xy_xxy[OF \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> \<open>s \<noteq> \<epsilon>\<close> this]
+    show False
+      using \<open>x \<noteq> y\<close> by blast
+  next
+    assume "p \<cdot> x \<cdot> y \<cdot> s = x \<cdot> y \<cdot> x" 
+    from cover_xy_xyx[OF \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> \<open>p \<noteq> \<epsilon>\<close> \<open>s \<noteq> \<epsilon>\<close> this]
+    show "\<not> primitive (x \<cdot> y)"
+      by blast  
+  next
+    assume "p \<cdot> x \<cdot> y \<cdot> s = x \<cdot> y \<cdot> y" 
+    from cover_xy_xyy[OF \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> \<open>p \<noteq> \<epsilon>\<close> this]
+    show False
+      using \<open>x \<noteq> y\<close> by blast  
+  next
+    assume "p \<cdot> x \<cdot> y \<cdot> s = y \<cdot> x \<cdot> x" 
+    from cover_xy_yxx[OF \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> this]
+    show False
+      using \<open>x \<noteq> y\<close> by blast  
+  next
+    assume "p \<cdot> x \<cdot> y \<cdot> s = y \<cdot> x \<cdot> y" 
+    from cover_xy_yxy[OF \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> \<open>p \<noteq> \<epsilon>\<close> \<open>s \<noteq> \<epsilon>\<close> this]
+    show "\<not> primitive (x \<cdot> y)"
+      by blast  
+  next
+    assume "p \<cdot> x \<cdot> y \<cdot> s = y \<cdot> y \<cdot> x" 
+    from cover_xy_yyx[OF \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> this]
+    show False
+      using \<open>x \<noteq> y\<close> by blast  
+  next
+    assume "p \<cdot> x \<cdot> y \<cdot> s = y \<cdot> y \<cdot> y" 
+    from cover_xy_yyy[OF \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> this]
+    show False
+      using \<open>x \<noteq> y\<close> by blast  
+  qed
+  thus "\<not> primitive (x\<cdot>y)" "vs = [x,y,x] \<or> vs = [y,x,y]"
+    by blast+
+qed
+
+subsection \<open>Primitivity (non)preserving uniform binary codes\<close>
+
+\<comment> \<open>This in particular implies the following characterization of uniform binary primitive codes. Cf. V. Mitrana, Primitive morphisms, Information Processing Letters 64 (1997), 277--281\<close>
+
+theorem bin_uniform_prim_morph:
+  assumes "x \<cdot> y \<noteq> y \<cdot> x" and "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and "primitive (x \<cdot> y)"
+         and "ws \<in> lists {x,y}" and "2 \<le> \<^bold>|ws\<^bold>|"
+         shows "primitive ws \<longleftrightarrow>  primitive (concat ws)"
+proof (standard, rule ccontr)
+  assume \<open>primitive ws\<close> and \<open>\<not> primitive (concat ws)\<close>
+  from bin_prim_long_pref[OF \<open>ws \<in> lists {x,y}\<close> \<open>primitive ws\<close> \<open>2 \<le> \<^bold>|ws\<^bold>|\<close>]
+  obtain ws' where "ws \<sim> ws'" "[x, y] \<le>p ws'".
+  have "ws' \<in> lists {x,y}"
+    using conjug_in_lists'[OF \<open>ws \<sim> ws'\<close> \<open>ws \<in> lists {x,y}\<close>].
+  have "primitive ws'"
+    using prim_conjug[OF \<open>primitive ws\<close> \<open>ws \<sim> ws'\<close>].   
+  have "\<not> primitive (concat ws')"
+    using conjug_concat_prim_iff \<open>\<not> primitive (concat ws)\<close> \<open>ws \<sim> ws'\<close> by auto  
+  interpret code "{x,y}"
+    using bin_code_code[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close>].
+  
+  have "[x,y] \<noteq> \<epsilon>" by blast
+  from imprim_witness_shift[OF \<open>ws' \<in> lists {x,y}\<close> \<open>primitive ws'\<close> \<open>\<not> primitive (concat ws')\<close>]
+  obtain z n where "concat ws' = z \<^sup>@ Suc (Suc n)" "z \<notin> \<langle>{x, y}\<rangle>" "z \<cdot> concat ws' = concat ws' \<cdot> z" "\<^bold>|z\<^bold>| < \<^bold>|concat ws'\<^bold>|".
+  from shift_interpret[OF \<open>ws' \<in> lists {x,y}\<close> \<open>ws' \<in> lists {x,y}\<close> this(2-4) \<open>[x,y] \<le>p ws'\<close> \<open>[x,y] \<noteq> \<epsilon>\<close>]
+  obtain vs p s where "vs \<in> lists {x,y}"  "p (concat [x, y]) s \<sim>\<^sub>\<I> vs" "p \<noteq> \<epsilon>" by metis   
+  from uniform_square_interp(1)[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> \<open>\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|\<close> \<open>vs \<in> lists {x,y}\<close> _ \<open>p \<noteq> \<epsilon>\<close>]
+       \<open>primitive (x \<cdot> y)\<close> \<open>p (concat [x, y]) s \<sim>\<^sub>\<I> vs\<close>
+  show False by force
+qed (simp add: prim_concat_prim)
+
+\<comment> \<open>A stronger version is implied by the following lemma.\<close>
+
+lemma bin_uniform_imprim: assumes "x \<cdot> y \<noteq> y \<cdot> x" and "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and "\<not> primitive x"
+  shows "primitive (x \<cdot> y)"
+proof (rule ccontr)
+  obtain s n where "s\<^sup>@n = x" and "2 \<le> n"
+    using not_prim_pow[OF \<open>\<not> primitive x\<close>].
+  assume "\<not> primitive (x \<cdot> y)"
+  have "x \<cdot> y \<noteq> \<epsilon>"
+    using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> by blast
+  from not_prim_expE[OF \<open>\<not> primitive (x \<cdot> y)\<close> this]
+  obtain z k where "primitive z" and  "2 \<le> k" and "z\<^sup>@k = x \<cdot> y".
+  from split_pow[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> \<open>z\<^sup>@k = x \<cdot> y\<close>[symmetric]]
+  obtain l m u v where "z \<^sup>@ l \<cdot> u = x" "v \<cdot> z \<^sup>@ m = y" "u \<cdot> v = z" "u \<cdot> v \<noteq> v \<cdot> u" "k = Suc (l + m)".
+  have "u \<noteq> \<epsilon>" and "v \<noteq> \<epsilon>"
+    using \<open>u \<cdot> v \<noteq> v \<cdot> u\<close> by blast+
+  have "m = l" and "\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|" 
+    using almost_equal_equal[OF nemp_len[OF \<open>u \<noteq> \<epsilon>\<close>] nemp_len[OF \<open>v \<noteq> \<epsilon>\<close>], of l m] lenarg[OF \<open>z\<^sup>@l \<cdot> u = x\<close>[symmetric], unfolded \<open>\<^bold>|x\<^bold>| =\<^bold>|y\<^bold>|\<close>, folded lenarg[OF \<open>v \<cdot> z\<^sup>@m = y\<close>]] unfolding lenmorph pow_len
+           lenarg[OF \<open>u \<cdot> v = z\<close>, symmetric] by presburger+ 
+  have "x \<le>p z \<cdot> x"
+    using pref_prod_root[OF pref_ext[of x, OF self_pref, of y, folded \<open>z\<^sup>@k = x \<cdot> y\<close>]]. 
+  have "x \<le>p s \<cdot> x"
+    unfolding \<open>s\<^sup>@n = x\<close>[symmetric] using pref_prod_root by blast 
+  have "z \<cdot> s \<noteq> s \<cdot> z"
+    using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> comm_add_exps[of s z n k, unfolded \<open>s \<^sup>@ n = x\<close> \<open>z \<^sup>@ k = x \<cdot> y\<close> rassoc cancel]
+    by force
+  with two_pers[OF \<open>x \<le>p z \<cdot> x\<close> \<open>x \<le>p s \<cdot> x\<close>] 
+  have "\<^bold>|x\<^bold>| < \<^bold>|z\<^bold>| + \<^bold>|s\<^bold>|"  by linarith
+  have "l = 1"
+  proof (rule ccontr)
+    assume "l \<noteq> 1" hence "2 \<le> l"
+      using \<open>k = Suc (l + m)\<close> \<open>2 \<le> k\<close> unfolding \<open>m = l\<close> by force
+    from  trans_le_add1[OF mult_le_mono1[OF this]]
+    have "2*\<^bold>|z\<^bold>| \<le> \<^bold>|x\<^bold>|"
+      unfolding lenarg[OF \<open>z\<^sup>@l \<cdot> u = x\<close>, unfolded pow_len lenmorph, symmetric].
+    from  mult_le_mono1[OF \<open>2 \<le> n\<close>]
+    have "2*\<^bold>|s\<^bold>| \<le> \<^bold>|x\<^bold>|"
+      unfolding lenarg[OF \<open>s\<^sup>@n = x\<close>, unfolded pow_len lenmorph, symmetric].
+    hence "2*\<^bold>|z\<^bold>| + 2*\<^bold>|s\<^bold>| \<le> 2*\<^bold>|x\<^bold>|"
+      using \<open>2*\<^bold>|z\<^bold>| \<le> \<^bold>|x\<^bold>|\<close> by force
+    thus False
+      using mult_less_mono1[OF \<open>\<^bold>|x\<^bold>| < \<^bold>|z\<^bold>| + \<^bold>|s\<^bold>|\<close>, of 2] by force
+  qed
+  hence "x = u \<cdot> v \<cdot> u"
+    using \<open>u \<cdot> v = z\<close> \<open>z \<^sup>@ l \<cdot> u = x\<close> by fastforce
+  have "u \<noteq> v"
+     using \<open>u \<cdot> v \<noteq> v \<cdot> u\<close> by blast
+  hence "primitive [u,v,u]"
+    by primitivity_inspection
+  hence "primitive [u,v,u] \<noteq> primitive (concat [u, v, u])"
+    using \<open>x = u \<cdot> v \<cdot> u\<close> \<open>\<not> primitive x\<close> by auto 
+  with bin_uniform_prim_morph[OF \<open>u \<cdot> v \<noteq> v \<cdot> u\<close> \<open>\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|\<close> \<open>primitive z\<close>[folded \<open>u \<cdot> v = z\<close>], of "[u,v,u]"]
+  show False by simp
+qed
+
+theorem bin_uniform_prim_morph':
+  assumes "x \<cdot> y \<noteq> y \<cdot> x" and "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" and "primitive (x \<cdot> y) \<or> \<not> primitive x"
+         and "ws \<in> lists {x,y}" and "2 \<le> \<^bold>|ws\<^bold>|"
+       shows "primitive ws \<longleftrightarrow>  primitive (concat ws)"
+  using bin_uniform_prim_morph[OF assms(1-2) _ assms(4-5)] bin_uniform_imprim[OF assms(1-2)] assms(3) by fast
+
+section \<open>The main theorem\<close>
+
+subsection \<open>Imprimitive words with single y\<close>
+
+text \<open>If the shorter word occurs only once, the result is straightforward from the parametric solution of the Lyndon-Schutzenberger
+  equation.\<close>
+
+lemma bin_imprim_single_y: 
+  assumes  non_comm: "x \<cdot> y \<noteq> y \<cdot> x" and
+    "ws \<in> lists {x,y}" and
+    "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|" and
+    "2 \<le> count_list ws x" and
+    "count_list ws y < 2" and
+    "primitive ws" and 
+    "\<not> primitive (concat ws)"
+  shows "ws \<sim> [x,x,y]" and "primitive x" and "primitive y"
+proof-
+  have "x \<noteq> y" 
+    using non_comm by blast
+  have "count_list ws y \<noteq> 0"
+  proof
+    assume "count_list ws y = 0"
+    from bin_lists_count_zero'[OF \<open>ws \<in> lists {x,y}\<close> this]
+    have "ws \<in> lists {x}".
+    from  prim_exp_one[OF \<open>primitive ws\<close> sing_lists_exp_count[OF this]]
+    show False
+      using \<open>2 \<le> count_list ws x\<close> by simp
+  qed
+  hence "count_list ws y = 1"
+    using \<open>count_list ws y < 2\<close> by linarith
+
+  from this bin_count_one_conjug[OF \<open>ws \<in> lists {x,y}\<close> _ this]
+  have "ws \<sim> [x]\<^sup>@count_list ws x \<cdot> [y]"
+    using  non_comm (1) by metis  
+  from conjug_concat_prim_iff[OF this]
+  have "\<not> primitive (x\<^sup>@(count_list ws x) \<cdot> y)"
+    using \<open>\<not> primitive (concat ws)\<close> by (auto simp add: concat_pow)
+
+  from not_prim_pow[OF this]
+  obtain z l where [symmetric]: "z\<^sup>@l = x\<^sup>@(count_list ws x) \<cdot> y\<^sup>@1" and "2 \<le> l"
+    unfolding pow_one'. 
+
+  interpret LS_len_le x y "count_list ws x" 1 l z
+    apply (unfold_locales; fact?) 
+    using \<open>2 \<le> count_list ws x\<close> by auto
+
+  from case_j2k1[OF \<open>2 \<le> count_list ws x\<close> refl]
+  have "primitive x" and "primitive y" and "count_list ws x = 2" by blast+
+
+  with \<open>ws \<sim> [x]\<^sup>@count_list ws x \<cdot> [y]\<close>[unfolded this(3) pow_two append_Cons append_Nil]
+  show  "primitive x" and "primitive y" and "ws \<sim> [x,x,y]"
+    by simp_all   
+ 
+qed
+
+subsection \<open>Conjugate words\<close>
+
+
+lemma bin_imprim_not_conjug: 
+  assumes "ws \<in> lists {x,y}" and
+    "x \<cdot> y \<noteq> y \<cdot> x" and
+    "2 \<le> \<^bold>|ws\<^bold>|" and
+    "primitive ws" and 
+    "\<not> primitive (concat ws)"
+  shows "\<not> x \<sim> y"
+proof
+  assume "x \<sim> y"
+  hence "\<^bold>|x\<^bold>| = \<^bold>|y\<^bold>|" by force
+  from bin_uniform_prim_morph[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> this _ \<open>ws \<in> lists {x,y}\<close> \<open>2 \<le> \<^bold>|ws\<^bold>|\<close>] 
+  have "\<not> primitive (x\<cdot>y)"
+    using \<open>primitive ws\<close> \<open>\<not> primitive (concat ws)\<close> by blast
+
+  (* have "[x,y] \<noteq> \<epsilon>" and "\<^bold>|[x,y]\<^bold>| \<le> \<^bold>|ws\<^bold>|" and "concat[x,y] = x \<cdot> y" *)
+    (* using \<open>2 \<le> \<^bold>|ws\<^bold>|\<close> by auto *)
+
+  (* interpret binary_code x y *)
+    (* using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> by unfold_locales *)
+  (* from switch_fac[OF bin_code_neq bin_prim_long_set[OF \<open>ws \<in> lists {x,y}\<close> \<open>primitive ws\<close> \<open>2 \<le> \<^bold>|ws\<^bold>|\<close>]] *)
+  (* have "[x,y] \<le>f ws \<cdot> ws". *)
+  (* from rotate_into_pref_sq[OF this] *)
+  (* obtain ws' where "ws \<sim> ws'" and "[x,y] \<le>p ws'" *) 
+    (* using \<open>2 \<le> \<^bold>|ws\<^bold>|\<close> by auto *)  
+
+  (* have "ws' \<in> lists {x,y}" and "primitive ws'" and "\<not> primitive (concat ws')" *)
+    (* using \<open>ws \<in> lists {x,y}\<close>[unfolded conjug_in_lists_iff [OF \<open>ws \<sim> ws'\<close>]] *) 
+      (* prim_conjug[OF \<open>primitive ws\<close> \<open>ws \<sim> ws'\<close>] *) 
+      (* \<open>\<not> primitive (concat ws)\<close>[unfolded conjug_concat_prim_iff[OF \<open>ws \<sim> ws'\<close>]]. *) 
+
+  (* from imprim_witness_shift[OF \<open>ws' \<in> lists {x,y}\<close> \<open>primitive ws'\<close> \<open>\<not> primitive (concat ws')\<close>] *)
+  (* obtain z where "z \<notin> \<langle>{x, y}\<rangle>" and "z \<cdot> concat ws' = concat ws' \<cdot> z" and "\<^bold>|z\<^bold>| < \<^bold>|concat ws'\<^bold>|". *)
+
+  (* from shift_interpret[OF \<open>ws' \<in> lists {x,y}\<close> \<open>ws' \<in> lists {x,y}\<close> this \<open>[x,y] \<le>p ws'\<close> \<open>[x,y] \<noteq> \<epsilon>\<close>] *)
+  (* obtain p s vs where "p (x \<cdot> y) s \<sim>\<^sub>\<I> vs" and \<open>vs \<in> lists {x, y}\<close> and *)
+    (* disjoint: "(\<And>us' vs'. us' \<le>p [x, y] \<Longrightarrow> vs' \<le>p vs \<Longrightarrow> p \<cdot> concat us' \<noteq> concat vs')" *)
+    (* unfolding \<open>concat [x,y] = x \<cdot> y\<close> by metis *) 
+  (* from disjoint[of \<epsilon> \<epsilon>] have "p \<noteq> \<epsilon>" by simp *)
+
+  (* from uniform_square_interp(1)[OF \<open>x\<cdot>y \<noteq> y\<cdot>x\<close> conjug_len[OF \<open>x \<sim> y\<close>] \<open>vs \<in> lists {x, y}\<close> *)
+      (* \<open>p (x \<cdot> y) s \<sim>\<^sub>\<I> vs\<close> \<open>p \<noteq> \<epsilon>\<close>] *)
+  (* have "\<not> primitive (x \<cdot> y)". *)
+
+  from Lyndon_Schutzenberger_conjug[OF \<open>x \<sim> y\<close> this]  
+  show False 
+    using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> by blast
+qed
+
+subsection \<open>Square prefix of the longer word and both words primitive (was all\_assms\<close>
+
+text\<open>The main idea of the proof is as follows: Imprimitivity of the concatenation yields
+(at least) two overlapping factorizations into @{term "{x,y}"}. 
+Due to the presence of the square @{term "x \<cdot> x"}, these two can be synchronized, which yields that the 
+situation coincides with the canonical form.
+\<close>
+
+lemma bin_imprim_primitive:
+  assumes "x \<cdot> y \<noteq> y \<cdot> x"
+    and  "primitive x" and "primitive y"
+    and "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    and "ws \<in> lists {x, y}"
+    and "primitive ws" and "\<not> primitive (concat ws)"
+    and "[x, x] \<le>f ws \<cdot> ws"
+  shows "ws \<sim> [x, x, y]"
+proof-
+  have "x \<noteq> y"
+    using assms(1) by blast
+  hence "2 \<le> \<^bold>|ws\<^bold>|"
+    by (metis Cons_in_lists_iff Suc_1 Suc_leI assms(2) assms(3) assms(5) assms(6) assms(7) nemp_le_len order_le_less prim_nemp sing_word_concat two_elem_cases)
+  have "\<^bold>|[x, x]\<^bold>| \<le> \<^bold>|ws\<^bold>|"
+    using \<open>2 \<le> \<^bold>|ws\<^bold>|\<close> by force
+  obtain ws' where "ws \<sim> ws'" "[x,x] \<le>p ws'"
+    using rotate_into_pos_sq[of \<epsilon> "[x,x]", unfolded clean_emp, OF \<open>[x, x] \<le>f ws \<cdot> ws\<close>
+        _ \<open>\<^bold>|[x, x]\<^bold>| \<le> \<^bold>|ws\<^bold>|\<close>]
+    by auto
+
+  have "ws' \<in> lists {x,y}"
+    by (meson \<open>ws \<sim> ws'\<close> assms(5) conjug_in_lists')
+  have "primitive ws'"
+    by (meson \<open>ws \<sim> ws'\<close> assms(6) prim_conjug)
+  have "\<not> primitive (concat ws')"
+    using \<open>ws \<sim> ws'\<close> assms(7) conjug_concat_prim_iff by blast
+
+  have "ws' = [x,x,y]"
+  proof(rule ccontr)
+    assume "ws' \<noteq> [x,x,y]"
+
+    have "2 \<le> \<^bold>|ws'\<^bold>|" and "[x,x] \<noteq> \<epsilon>"
+      using \<open>[x,x] \<le>p ws'\<close> unfolding prefix_def by auto
+    have "x \<noteq> y" 
+      using  prim_exp_eq[OF \<open>primitive ws'\<close> sing_lists_exp_len] \<open>ws' \<in> lists {x,y}\<close> \<open>[x,x] \<le>p ws'\<close> by force    
+    hence "x \<cdot> y \<noteq> y \<cdot> x"
+      using comm_prim[OF \<open>primitive x\<close> \<open>primitive y\<close>] by blast 
+    from bin_imprim_not_conjug[OF \<open>ws' \<in> lists {x,y}\<close> this \<open>2 \<le> \<^bold>|ws'\<^bold>|\<close> \<open>primitive ws'\<close> \<open>\<not> primitive (concat ws')\<close>]
+    have "\<not> x \<sim> y". 
+    have "[x,x] \<le>np ws'"
+      using npI[OF _ \<open>[x,x] \<le>p ws'\<close>] by blast
+    have "concat ws' \<noteq> \<epsilon>"
+      using \<open>primitive x\<close> \<open>[x,x] \<le>p ws'\<close> by (fastforce simp add: prefix_def)
+    have "ws' \<noteq> \<epsilon>"
+      using \<open>concat ws' \<noteq> \<epsilon>\<close> by auto
+    have "ws' \<cdot> ws' \<cdot> ws' \<in> lists {x, y}" and "ws' \<cdot> ws' \<in> lists {x, y}" 
+      using \<open>ws' \<in> lists {x,y}\<close> by inlists
+    have "concat [x,x] = x \<cdot> x" by simp
+
+    have "primitive [x,x,y]" 
+      using \<open>x \<noteq> y\<close> by primitivity_inspection
+
+    interpret xy: binary_code x y
+      using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> by (unfold_locales)
+
+    from xy.imprim_witness_shift[OF \<open>ws' \<in> lists {x,y}\<close> \<open>primitive ws'\<close> \<open>\<not> primitive (concat ws')\<close>]
+    obtain z n where con_ws: "concat ws' = z \<^sup>@ Suc (Suc n)" and "z \<notin> \<langle>{x, y}\<rangle>" and "z \<cdot> concat ws' = concat ws' \<cdot> z" and "\<^bold>|z\<^bold>| < \<^bold>|concat ws'\<^bold>|".
+
+    obtain vs p s ps ss where "p (x \<cdot> x) s \<sim>\<^sub>\<I> vs" and "ps \<cdot> vs \<le>p ws' \<cdot> ws'" and 
+      "[x, x] \<cdot> ss = ws' \<cdot> ws'" and \<open>concat ps \<cdot> p = z\<close> and "s \<le>p concat ss" and "p \<le>s concat ws'" and \<open>vs \<in> lists {x, y}\<close> and
+      disjoint: "(\<And>us' vs'. us' \<le>p [x, x] \<Longrightarrow> vs' \<le>p vs \<Longrightarrow> p \<cdot> concat us' \<noteq> concat vs')" and "p \<noteq> \<epsilon>" and "s \<noteq> \<epsilon>"   
+      using xy.shift_interpret[OF \<open>ws' \<in> lists {x,y}\<close> \<open>ws' \<in> lists {x,y}\<close> \<open>z \<notin> \<langle>{x, y}\<rangle>\<close> \<open>z \<cdot> concat ws' = concat ws' \<cdot> z\<close>
+             \<open>\<^bold>|z\<^bold>| < \<^bold>|concat ws'\<^bold>|\<close> \<open>[x,x] \<le>p ws'\<close> \<open>[x,x] \<noteq> \<epsilon>\<close>, of thesis]
+      unfolding \<open>concat [x,x] = x \<cdot> x\<close> by fast  
+    from disjoint[of \<epsilon> \<epsilon>] have "p \<noteq> \<epsilon>" by simp
+
+    have triv: "2 \<le> Suc(Suc n)" "Suc 0 < Suc (Suc n)" by simp_all
+
+    have "ps \<in> lists {x,y}"
+      using \<open>ps \<cdot> vs \<le>p ws' \<cdot> ws'\<close> \<open>ws' \<in> lists {x,y}\<close> \<open>ws' \<cdot> ws' \<in> lists {x, y}\<close> append_prefixD pref_in_lists by metis 
+    have "vs \<in> lists {x,y}" 
+      using \<open>ws' \<in> lists {x,y}\<close> pref_in_lists[OF \<open>ps \<cdot> vs \<le>p ws' \<cdot> ws'\<close>] by inlists
+    have "ss \<in> lists {x,y}"
+      using \<open>ws' \<in> lists {x,y}\<close> \<open>[x,x] \<cdot> ss = ws' \<cdot> ws'\<close> append_in_lists_conv by metis 
+
+    interpret square_interp_ext x y p s vs
+      by (rule square_interp_ext.intro[OF square_interp.intro, unfolded square_interp_ext_axioms_def,
+            OF \<open>primitive x\<close> \<open>primitive y\<close> \<open>\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|\<close> \<open>vs \<in> lists {x,y}\<close> \<open>\<not> x \<sim> y\<close> disjoint], simp_all only: \<open>p x \<cdot> x s \<sim>\<^sub>\<I> vs\<close>)  
+        (meson \<open>p \<le>s concat ws'\<close> \<open>s \<le>p concat ss\<close> \<open>ss \<in> lists {x, y}\<close> \<open>ws' \<in> lists {x, y}\<close> concat_in_hull')
+
+\<comment> \<open>Establishing the connection between ws' = [x,x,y] and z = xp.\<close>
+
+    define xp where "xp = x \<cdot> p"
+
+    have "concat [x,x,y] = xp \<cdot> xp"
+      by (simp add: xxy_root xp_def) 
+
+    hence "ws' \<cdot> [x,x,y] \<noteq> [x,x,y] \<cdot> ws'"
+      using  comm_prim[OF \<open>primitive ws'\<close> \<open>primitive [x,x,y]\<close>] \<open>ws' \<noteq> [x,x,y] \<close>by force
+
+    have "z \<cdot> xp \<noteq> xp \<cdot> z"
+    proof
+      assume "z \<cdot> xp = xp \<cdot> z"
+      from power_commuting_commutes[symmetric, OF this[symmetric], of 2,
+          THEN power_commuting_commutes, of "Suc (Suc n)", unfolded pow_two]
+      have "z\<^sup>@Suc(Suc n) \<cdot> xp \<cdot> xp = xp \<cdot> xp \<cdot> z\<^sup>@Suc(Suc n)"
+        unfolding  rassoc.
+      hence "concat ws' \<cdot> concat [x,x,y] = concat [x,x,y] \<cdot> concat ws'"
+        unfolding con_ws \<open>concat [x,x,y] = xp \<cdot> xp\<close> rassoc  by simp
+      from  xy.is_code[OF _ _ this[folded concat_morph]]
+      have "ws' \<cdot> [x, x, y] = [x,x,y] \<cdot> ws'"
+        using append_in_lists \<open>ws' \<in> lists {x,y}\<close> by simp
+      thus False
+        using \<open>ws' \<cdot> [x, x, y] \<noteq> [x,x,y] \<cdot> ws'\<close> by fastforce
+    qed        
+
+    then interpret binary_code z xp 
+      by (unfold_locales)
+
+    have "\<not> concat (ws' \<cdot> [x, x, y]) \<bowtie> concat ([x, x, y] \<cdot> ws')"
+    proof (rule notI)
+      assume "concat (ws' \<cdot> [x, x, y]) \<bowtie> concat ([x, x, y] \<cdot> ws')"
+      from comm_comp_eq[OF this[unfolded concat_morph], unfolded \<open>concat [x,x,y] = xp \<cdot> xp\<close> con_ws]
+      have "z \<^sup>@ Suc (Suc n) \<cdot> xp\<^sup>@Suc(Suc 0) = xp\<^sup>@Suc(Suc 0) \<cdot> z \<^sup>@ Suc (Suc n)"
+        unfolding pow_Suc pow_zero clean_emp rassoc.
+      from comm_drop_exps[OF this] 
+      show False
+        using \<open>z \<cdot> xp \<noteq> xp \<cdot> z\<close> by blast 
+    qed
+
+\<comment> \<open>How the xp/z mismatch is reflected by mismatch in lists {x,y}?\<close>
+\<comment> \<open>Looking at the first occurrence of z:\<close>
+
+    define lcp_ws where "lcp_ws = ws' \<cdot> [x,x,y] \<and>\<^sub>p [x,x,y] \<cdot> ws'"
+
+    have "lcp_ws \<in> lists {x,y}"
+      unfolding lcp_ws_def by inlists
+
+    have lcp_xp_z: "concat (ws' \<cdot> [x,x,y]) \<and>\<^sub>p concat ([x,x,y] \<cdot> ws') = bin_lcp z (x \<cdot> p)"
+      unfolding concat_morph con_ws \<open>concat [x,x,y] = xp \<cdot> xp\<close> add_exps[symmetric] 
+      using bin_lcp_pows[of  "Suc n" "(x\<cdot>p)\<^sup>@Suc 0" "Suc 0" "z\<^sup>@(Suc n)"]  
+      unfolding xp_def pow_Suc pow_zero clean_emp rassoc.
+
+    have "(concat lcp_ws) \<cdot> bin_lcp x y = bin_lcp z (x \<cdot> p)"
+    proof (rule xy.bin_code_lcp_concat'[OF _ _  \<open>\<not> concat (ws' \<cdot> [x, x, y]) \<bowtie> concat ([x, x, y] \<cdot> ws')\<close>, folded lcp_ws_def, unfolded lcp_xp_z, symmetric])
+      show "ws' \<cdot> [x, x, y] \<in> lists {x, y}" and  "[x, x, y] \<cdot> ws' \<in> lists {x, y}"
+        by inlists
+    qed
+
+\<comment> \<open>Looking at the second occurrence of z:\<close>
+
+    define ws'' where "ws'' = ps \<cdot> [x,y]"
+    define lcp_ws' where "lcp_ws' = ws' \<cdot> ws'' \<and>\<^sub>p ws'' \<cdot> ws'"
+
+    have "lcp_ws' \<in> lists {x,y}"
+      unfolding lcp_ws'_def
+      using \<open>ps \<in> lists {x, y}\<close> \<open>ws' \<in> lists {x, y}\<close> ws''_def by inlists
+
+    have "concat ws'' = z \<cdot> xp"
+      unfolding ws''_def xp_def using \<open>concat ps \<cdot> p = z\<close> xxy_root by fastforce 
+
+    have "ws' \<cdot> ws'' \<noteq> ws'' \<cdot> ws'"
+    proof 
+      assume "ws' \<cdot> ws'' = ws'' \<cdot> ws'"
+      from arg_cong[OF this, of concat, unfolded concat_morph con_ws
+          \<open>concat ws'' = z \<cdot> xp\<close>,
+          unfolded lassoc pow_comm, unfolded rassoc cancel]
+      show False 
+        using \<open>z \<cdot> xp \<noteq> xp \<cdot> z\<close> comm_drop_exp' by blast
+    qed
+
+    have 
+      lcp_xp_z': "concat (ws' \<cdot> ws'') \<and>\<^sub>p concat (ws'' \<cdot> ws') = z \<cdot> bin_lcp z (x \<cdot> p)"  
+      unfolding concat_morph con_ws \<open>concat ws'' = z \<cdot> xp\<close> pow_Suc 
+      unfolding lassoc cancel 
+      unfolding rassoc lcp_ext_left cancel  
+      using bin_lcp_pows[of "(Suc n)" \<epsilon> 0 "z \<cdot> z\<^sup>@n", unfolded pow_one rassoc clean_emp]
+      unfolding lassoc pow_Suc[symmetric] pow_Suc2[symmetric]
+      using xp_def by auto
+
+    have "z \<cdot> bin_lcp z (x \<cdot> p) = concat (lcp_ws') \<cdot> bin_lcp x y" 
+      unfolding lcp_xp_z'[symmetric] lcp_ws'_def
+    proof (rule xy.bin_code_lcp_concat')
+      show "ws' \<cdot> ws'' \<in> lists {x, y}"
+        unfolding ws''_def using \<open>ws' \<cdot> ws' \<cdot> ws' \<in> lists {x, y}\<close> \<open>ps \<in> lists {x,y}\<close> by inlists
+      thus "ws'' \<cdot> ws' \<in> lists {x, y}"
+        by inlists
+      show "\<not> concat (ws' \<cdot> ws'') \<bowtie> concat (ws'' \<cdot> ws')"
+        unfolding concat_morph con_ws \<open>concat ws'' = z \<cdot> xp\<close> pow_Suc rassoc comp_cancel 
+        unfolding lassoc pow_Suc[symmetric] pow_Suc2[symmetric] comm_comp_eq_conv
+          comm_drop_exps_conv[of _ _ _ 0, unfolded pow_one]
+        using non_comm. 
+    qed
+
+    have "concat lcp_ws' = z \<cdot> concat lcp_ws"
+      unfolding cancel_right[of "concat lcp_ws'" "bin_lcp x y" "z \<cdot> concat lcp_ws", symmetric]
+      unfolding rassoc[of z] \<open>concat (lcp_ws) \<cdot> bin_lcp x y = bin_lcp z (x \<cdot> p)\<close> \<open>z \<cdot> bin_lcp z (x \<cdot> p) = concat (lcp_ws') \<cdot> bin_lcp x y\<close>..
+
+    have "lcp_ws \<le>p ws' \<cdot> [x,x,y]"
+      unfolding lcp_ws_def using  longest_common_prefix_prefix1.
+    have "lcp_ws \<noteq> ws' \<cdot> [x,x,y]"
+      unfolding lcp_ws_def lcp_pref_conv
+      using  \<open>ws' \<cdot> [x, x, y] \<noteq> [x, x, y] \<cdot> ws'\<close> pref_comm_eq by blast 
+    have "lcp_ws \<le>p ws' \<cdot> [x,x]"
+      using spref_butlast_pref[OF  \<open>lcp_ws \<le>p ws' \<cdot> [x,x,y]\<close> \<open>lcp_ws \<noteq> ws' \<cdot> [x,x,y]\<close>] 
+      unfolding butlast_append by simp 
+    from  prefixE[OF pref_prolong[OF this \<open>[x,x] \<le>p ws'\<close>]]
+    obtain ws''\<^sub>1 where "ws' \<cdot> ws' \<cdot> ws' = lcp_ws \<cdot> ws''\<^sub>1" using rassoc by metis 
+
+    have "ws' \<cdot> ps \<cdot> [x,y] \<le>p ws' \<cdot> ps \<cdot> [x,y,x]"
+      by simp
+    from pref_trans[OF pref_trans[OF longest_common_prefix_prefix1 this]]  
+    have "lcp_ws' \<le>p ws' \<cdot> ws' \<cdot> ws'"
+      unfolding lcp_ws'_def ws''_def using \<open>ps \<cdot> vs \<le>p ws' \<cdot> ws'\<close>[unfolded cover_xyx, unfolded pref_cancel_conv]
+      unfolding pref_cancel_conv[symmetric, of "ps \<cdot> [x,y,x]" "ws' \<cdot> ws'" ws'] by blast  
+    from prefixE[OF this]
+    obtain ws''\<^sub>2 where "ws' \<cdot> ws' \<cdot> ws' = lcp_ws' \<cdot> ws''\<^sub>2".  
+
+    have "concat lcp_ws'\<cdot> concat ws''\<^sub>1 = z \<cdot> concat(lcp_ws) \<cdot> concat ws''\<^sub>1"
+      unfolding lassoc \<open>concat lcp_ws' = z \<cdot> concat lcp_ws\<close>..
+    also have "... = z \<cdot> concat (ws' \<cdot> ws' \<cdot> ws')"
+      unfolding rassoc \<open>ws' \<cdot> ws' \<cdot> ws' = lcp_ws \<cdot> ws''\<^sub>1\<close> concat_morph..
+    also have "... = concat (ws' \<cdot> ws' \<cdot> ws') \<cdot> z"
+      unfolding concat_morph con_ws add_exps[symmetric]
+        pow_Suc[symmetric] pow_Suc2[symmetric]..
+    also have "... = concat lcp_ws'\<cdot> concat ws''\<^sub>2 \<cdot> z"
+      unfolding \<open>ws' \<cdot> ws' \<cdot> ws' = lcp_ws' \<cdot> ws''\<^sub>2\<close> concat_morph rassoc..
+    finally have "concat ws''\<^sub>1 = concat ws''\<^sub>2 \<cdot> z"
+      unfolding cancel.  
+
+    from xy.stability[of "concat ws''\<^sub>2"  "concat lcp_ws" z,
+        folded \<open>concat ws''\<^sub>1 = concat ws''\<^sub>2 \<cdot> z\<close> \<open>concat lcp_ws' = z \<cdot> concat lcp_ws\<close>]
+    have "z \<in> \<langle>{x, y}\<rangle>" 
+      using \<open>ws' \<cdot> ws' \<cdot> ws' = lcp_ws \<cdot> ws''\<^sub>1\<close> \<open>ws' \<cdot> ws' \<cdot> ws' = lcp_ws' \<cdot> ws''\<^sub>2\<close> \<open>ws' \<cdot> ws' \<cdot> ws' \<in> lists {x, y}\<close>
+        append_in_lists_dest append_in_lists_dest' concat_in_hull' by metis
+    thus False
+      using  \<open>z \<notin> \<langle>{x,y}\<rangle>\<close> by blast
+  qed
+  thus ?thesis
+    using \<open>ws \<sim> ws'\<close> by blast
+qed
+
+subsection \<open>Obtaining primitivity with two squares (refining)\<close>
+
+lemma bin_imprim_both_squares_prim:
+  assumes "x \<cdot> y \<noteq> y \<cdot> x"
+    and "ws \<in> lists {x, y}"
+    and "primitive ws" and "\<not> primitive (concat ws)"
+    and "[x, x] \<le>f ws \<cdot> ws"
+    and "[y, y] \<le>f ws \<cdot> ws"
+    and  "primitive x" and "primitive y"
+  shows False
+proof-
+  have "x \<noteq> y" using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close>
+    by blast
+  from bin_imprim_primitive[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> \<open>primitive x\<close> \<open>primitive y\<close>
+      _ \<open>ws \<in> lists {x,y}\<close> \<open>primitive ws\<close> \<open>\<not> primitive (concat ws)\<close> \<open>[x, x] \<le>f ws \<cdot> ws\<close>]
+    bin_imprim_primitive[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close>[symmetric] \<open>primitive y\<close> \<open>primitive x\<close>
+      _ \<open>ws \<in> lists {x,y}\<close>[unfolded insert_commute[of x]] \<open>primitive ws\<close> \<open>\<not> primitive (concat ws)\<close>
+      \<open>[y, y] \<le>f ws \<cdot> ws\<close>]
+  have "ws \<sim> [x, x, y] \<or> ws \<sim> [y, y, x]"
+    using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close>
+    by force
+  hence "\<^bold>|ws\<^bold>| = 3" 
+    using conjug_len by force
+  note[simp] = sublist_code(3)
+  from \<open>\<^bold>|ws\<^bold>| = 3\<close> \<open>ws \<in> lists {x,y}\<close> \<open>x \<noteq> y\<close>
+       \<open>[x, x] \<le>f ws \<cdot> ws\<close> \<open>[y, y] \<le>f ws \<cdot> ws\<close>
+  show False
+   by list_inspection simp_all
+qed
+
+lemma bin_imprim_both_squares:
+  assumes "x \<cdot> y \<noteq> y \<cdot> x"
+    and "ws \<in> lists {x, y}"
+    and "primitive ws" and "\<not> primitive (concat ws)"
+    and "[x, x] \<le>f ws \<cdot> ws"
+    and "[y, y] \<le>f ws \<cdot> ws"
+  shows False
+proof (rule bin_imprim_both_squares_prim) 
+  have "x \<noteq> \<epsilon>" and "y \<noteq> \<epsilon>" and "x \<noteq> y"
+    using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> by blast+
+  let ?R = "\<lambda> x. [\<rho> x]\<^sup>@(e\<^sub>\<rho> x)"
+  define ws' where "ws' = concat (map ?R ws)"
+  show "\<rho> x \<cdot> \<rho> y \<noteq> \<rho> y \<cdot> \<rho> x"
+    using  \<open>x \<cdot> y \<noteq> y \<cdot> x\<close>[unfolded comp_primroot_conv'[OF \<open>x \<noteq> \<epsilon>\<close> \<open>y \<noteq> \<epsilon>\<close>]]. 
+  have [simp]: "a = x \<or> a = y \<Longrightarrow> [\<rho> a] \<^sup>@ e\<^sub>\<rho> a \<in> lists {\<rho> x, \<rho> y}" for a
+    using insert_iff sing_pow_lists[of _ "{\<rho> x, \<rho> y}"] by metis 
+  show "ws' \<in> lists {\<rho> x, \<rho> y}"
+    unfolding ws'_def using \<open>ws \<in> lists {x,y}\<close> 
+    by (induction ws, simp_all)
+
+\<comment> \<open>The primitivity of ws' is obtained from the fact that the decompositions into
+    roots is a primitive morphism\<close>
+  interpret binary_code x y  
+    using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> by unfold_locales
+  note[simp] = sublist_code(3)
+  have "\<^bold>|ws\<^bold>| \<le> 3 \<Longrightarrow> ws \<in> lists {x,y} \<Longrightarrow> x \<noteq> y \<Longrightarrow> [x, x] \<le>f ws \<cdot> ws \<Longrightarrow> [y, y] \<le>f ws \<cdot> ws \<Longrightarrow> False"
+    by list_inspection simp_all
+  from this[OF _ \<open> ws \<in> lists {x,y}\<close> \<open>x \<noteq> y\<close> \<open>[x, x] \<le>f ws \<cdot> ws\<close> \<open>[y, y] \<le>f ws \<cdot> ws\<close>]
+      roots_prim_morph[OF \<open>ws \<in> lists {x,y}\<close> _ \<open>primitive ws\<close>]
+  show "primitive ws'"
+    unfolding ws'_def  by fastforce
+    
+  show "\<not> primitive (concat ws')"
+    unfolding ws'_def concat_root_dec_eq_concat[OF \<open>ws \<in> lists{x,y}\<close>] by fact
+
+  have "concat(map ?R [x,x]) \<le>f ws' \<cdot> ws'" and "concat(map ?R [y,y]) \<le>f ws' \<cdot> ws'"   
+    unfolding ws'_def
+    using concat_mono_fac[OF map_mono_sublist[OF \<open>[x,x] \<le>f ws \<cdot> ws\<close>]]
+          concat_mono_fac[OF map_mono_sublist[OF \<open>[y,y] \<le>f ws \<cdot> ws\<close>]]
+    unfolding concat_morph  map_append.    
+
+  have "Suc (Suc (e\<^sub>\<rho> x + e\<^sub>\<rho> x - 2)) = e\<^sub>\<rho> x + e\<^sub>\<rho> x"
+    using Suc_minus2 primroot_exp_nemp[OF \<open>x \<noteq> \<epsilon>\<close>] by simp
+  have "concat (map ?R [x,x]) = [\<rho> x] \<^sup>@ (Suc (e\<^sub>\<rho> x -1) + Suc (e\<^sub>\<rho> x - 1))"
+    unfolding  Suc_minus[OF primroot_exp_nemp[OF \<open>x \<noteq> \<epsilon>\<close>]] by (simp add: add_exps)
+  hence "[\<rho> x, \<rho> x] \<le>f concat (map ?R [x,x])"
+    by auto 
+  thus "[\<rho> x, \<rho> x] \<le>f ws' \<cdot> ws'" 
+    using fac_trans[OF _ \<open>concat(map ?R [x,x]) \<le>f ws' \<cdot> ws'\<close>] by blast 
+
+  have "Suc (Suc (e\<^sub>\<rho> y + e\<^sub>\<rho> y - 2)) = e\<^sub>\<rho> y + e\<^sub>\<rho> y"
+    using Suc_minus2 primroot_exp_nemp[OF \<open>y \<noteq> \<epsilon>\<close>] by simp
+  have "concat (map ?R [y,y]) = [\<rho> y] \<^sup>@ (Suc (e\<^sub>\<rho> y -1) + Suc (e\<^sub>\<rho> y - 1))"
+    unfolding  Suc_minus[OF primroot_exp_nemp[OF \<open>y \<noteq> \<epsilon>\<close>]] by (simp add: add_exps)
+  hence "[\<rho> y, \<rho> y] \<le>f concat (map ?R [y,y])"
+    by auto 
+  thus "[\<rho> y, \<rho> y] \<le>f ws' \<cdot> ws'" 
+    using fac_trans[OF _ \<open>concat(map ?R [y,y]) \<le>f ws' \<cdot> ws'\<close>] by blast 
+
+  show "primitive (\<rho> x)" and "primitive (\<rho> y)"
+    using  primroot_prim \<open>x \<noteq> \<epsilon>\<close> \<open>y \<noteq> \<epsilon>\<close> by blast+
+qed
+
+subsection \<open>Obtaining the square of the longer word (gluing)\<close>
+
+lemma bin_imprim_longer_twice:
+  \<comment> \<open>
+1. If there are both squares, then contradiction;
+2. If a square is missing:
+   a) if y appears once: the positive conclusion
+   b) if y appears twice, then gluing preserves presence of the longer word at least twice (because both appear twice)
+      and induction yields [x',x',y'] where y' is a suffix of x',
+      a contradiction with primitivity of words of the form xyxyy;
+\<close>
+  assumes "x \<cdot> y \<noteq> y \<cdot> x"
+    and "ws \<in> lists {x, y}"
+    and "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    and "count_list ws x \<ge> 2"
+    and "primitive ws" and "\<not> primitive (concat ws)"
+  shows "ws \<sim> [x,x,y] \<and> primitive x \<and> primitive y"
+  using assms proof (induction "\<^bold>|ws\<^bold>|" arbitrary: x y ws rule: less_induct)
+  case less
+  then show ?case
+  proof (cases)
+    assume "[x, x] \<le>f ws \<cdot> ws \<and> [y, y] \<le>f ws \<cdot> ws"
+    with bin_imprim_both_squares[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> \<open>ws \<in> lists {x,y}\<close> \<open>primitive ws\<close> \<open> \<not> primitive (concat ws)\<close>]  
+    have False by blast
+    thus ?case by blast 
+  next
+    assume missing_sq: "\<not> ([x, x] \<le>f ws \<cdot> ws \<and> [y, y] \<le>f ws \<cdot> ws)"
+    then show ?case
+    proof (cases)
+      assume "count_list ws y < 2"
+      with bin_imprim_single_y[OF less.prems(1-4) this less.prems(5-6)]      
+      show "ws \<sim> [x,x,y] \<and> primitive x \<and> primitive y"
+        by blast
+    next
+      assume "\<not> count_list ws y < 2" hence "2 \<le> count_list ws y" by simp 
+
+\<comment> \<open>Missing square and two y's allow gluing\<close>
+      define x' where "x' = (if \<not> [x, x] \<le>f ws \<cdot> ws then x else y)"
+      define y' where "y' = (if \<not> [x, x] \<le>f ws \<cdot> ws then y else x)"
+
+      have "{x', y'} = {x, y}"
+        by (simp add: doubleton_eq_iff x'_def y'_def) 
+      note cases = disjE[OF this[unfolded doubleton_eq_iff]]
+      have "\<not> [x', x'] \<le>f ws \<cdot> ws"
+        using missing_sq x'_def by presburger
+      have "count_list ws x' \<ge> 2" and "count_list ws y' \<ge> 2" 
+        unfolding x'_def y'_def using \<open>2 \<le> count_list ws x\<close> \<open>2 \<le> count_list ws y\<close> by presburger+ 
+      have "x' \<cdot>  y' \<noteq> y' \<cdot> x'"
+        by (rule cases, simp_all add: \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> \<open>x \<cdot> y \<noteq> y \<cdot> x\<close>[symmetric])   
+      have "x' \<noteq> \<epsilon>" and "x' \<noteq> y'" and "x' \<cdot> y' \<noteq> y'"
+        using \<open>x' \<cdot> y' \<noteq> y' \<cdot> x'\<close> by auto 
+
+\<comment> \<open>rotating last if necessary for successful gluing\<close>
+      note prim_nemp[OF \<open>primitive ws\<close>]
+      hence rot: "last ws = x' \<Longrightarrow> hd ws = x' \<Longrightarrow> butlast ws \<cdot> [x',x'] \<cdot> tl ws = ws \<cdot> ws"
+        using append_butlast_last_id hd_tl hd_word mult_assoc by metis 
+      from this[THEN facI']
+      have "last ws = x' \<Longrightarrow> hd ws \<noteq> x'"
+        using \<open>\<not> [x', x'] \<le>f ws \<cdot> ws\<close>  by blast 
+      define ws' where "ws' = (if last ws \<noteq> x' then ws else tl ws \<cdot> [hd ws])" 
+      have cond: "ws' = \<epsilon> \<or> last ws' \<noteq> x'" \<comment> \<open>gluing condition\<close>
+        unfolding ws'_def using \<open>last ws = x' \<Longrightarrow> hd ws \<noteq> x'\<close> by simp 
+      have "ws' \<sim> ws" 
+        unfolding ws'_def using \<open>ws \<noteq> \<epsilon>\<close> by fastforce 
+      hence counts': "count_list ws' x' \<ge> 2" "count_list ws' y' \<ge> 2" 
+        by (simp_all add: \<open>2 \<le> count_list ws x'\<close> \<open>2 \<le> count_list ws y'\<close> count_list_conjug)
+
+\<comment> \<open>verify induction assumptions of the glued word\<close>
+      let ?ws = "glue x' ws'"
+      have c1: "\<^bold>|?ws\<^bold>| < \<^bold>|ws\<^bold>|"
+        using len_glue[OF cond] conjug_len[OF \<open>ws' \<sim> ws\<close>] \<open>count_list ws' x' \<ge> 2\<close> by linarith  
+      hence c2: "(x' \<cdot> y') \<cdot> y' \<noteq> y' \<cdot> x' \<cdot> y'"
+        using \<open>x' \<cdot> y' \<noteq> y' \<cdot> x'\<close> by force
+
+      have "ws' \<le>f ws \<cdot> ws"
+        using conjugE[OF \<open>ws' \<sim> ws\<close>] rassoc sublist_appendI by metis  
+      hence "\<not> [x', x'] \<le>f ws'" 
+        using \<open>\<not> [x',x'] \<le>f ws \<cdot> ws\<close> by blast
+      have "ws' \<in> lists {x',y'}"  
+        using conjug_in_lists[OF \<open>ws' \<sim> ws\<close> \<open>ws \<in> lists {x,y}\<close>[folded \<open>{x',y'} = {x,y}\<close>]].
+      have  c3: "?ws \<in> lists {x' \<cdot> y', y'}" 
+        using single_bin_glue_in_lists[OF cond \<open>\<not> [x', x'] \<le>f ws'\<close> \<open>ws' \<in> lists {x',y'}\<close>].
+
+      have c4: "2 \<le> count_list (glue x' ws') (x' \<cdot> y')"
+        using \<open>2 \<le> count_list ws' x'\<close> 
+        unfolding count_list_single_bin_glue(1)[OF \<open>x' \<noteq> \<epsilon>\<close> \<open>x' \<noteq> y'\<close> cond \<open>ws' \<in> lists {x',y'}\<close> \<open>\<not> [x',x'] \<le>f ws'\<close>].
+
+      from \<open>primitive ws\<close>[folded conjug_prim_iff[OF \<open>ws' \<sim> ws\<close>]]
+      have c5: "primitive (glue x' ws')"
+        using prim_bin_glue [OF \<open>ws' \<in> lists {x',y'}\<close> \<open>x' \<noteq> \<epsilon>\<close> cond] by blast  
+
+      have "count_list ws' x' \<ge> 2" 
+        using \<open>count_list ws x \<ge> 2\<close> \<open>count_list ws y \<ge> 2\<close> \<open>{x', y'} = {x, y}\<close>
+          count_list_conjug[OF \<open>ws' \<sim> ws\<close>] x'_def by metis 
+
+      have "concat (glue x' ws') = concat ws'"
+        by (simp add: cond) 
+      have c6: "\<not> primitive (concat (glue x' ws'))"
+        unfolding \<open>concat (glue x' ws') = concat ws'\<close> using \<open>\<not> primitive (concat ws)\<close> \<open>ws' \<sim> ws\<close>
+          conjug_concat_conjug prim_conjug by metis
+          \<comment> \<open>The claim holds by induction\<close>
+      from less.hyps[OF c1 c2 c3 _ c4 c5 c6] 
+      have "glue x' ws' \<sim> [x' \<cdot> y', x' \<cdot> y', y']" by simp
+          \<comment> \<open>Which is impossible after gluing\<close>
+      from prim_xyxyy[OF \<open>x' \<cdot> y' \<noteq> y' \<cdot> x'\<close>] conjug_prim_iff[OF conjug_concat_conjug[OF this]]
+      have False
+        using \<open>\<not> primitive (concat (glue x' ws'))\<close> by simp
+      thus ?case by blast
+    qed
+  qed
+qed
+
+lemma bin_imprim_both_twice:
+  assumes "x \<cdot> y \<noteq> y \<cdot> x"
+    and "ws \<in> lists {x, y}"
+    and "count_list ws x \<ge> 2"
+    and "count_list ws y \<ge> 2"
+    and "primitive ws" and "\<not> primitive (concat ws)"
+  shows False
+proof-
+  have "x \<noteq> y"
+    using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> by blast
+  from bin_imprim_longer_twice[OF assms(1-2) _ assms(3) assms(5-6)]
+    bin_imprim_longer_twice[OF assms(1)[symmetric] assms(2)[unfolded insert_commute[of x]] _ assms(4) assms(5-6)]
+  have or: "ws \<sim> [x, x, y] \<or> ws \<sim> [y, y, x]" by linarith 
+  thus False
+  proof (rule disjE)
+    assume "ws \<sim> [x, x, y]"
+    from \<open>count_list ws y \<ge> 2\<close>[unfolded count_list_conjug[OF this]]
+    show False 
+      using \<open>x \<noteq> y\<close> by force  
+  next
+    assume "ws \<sim> [y, y, x]"
+    from \<open>count_list ws x \<ge> 2\<close>[unfolded count_list_conjug[OF this]]
+    show False 
+      using \<open>x \<noteq> y\<close> by force  
+  qed
+qed
+
+section \<open>Examples\<close>
+
+lemma "x \<noteq> \<epsilon> \<Longrightarrow>  \<epsilon> (x\<cdot>x) \<epsilon> \<sim>\<^sub>\<I> [x,x]"
+  unfolding factor_interpretation_def
+  by simp
+
+lemma assumes "x = [(0::nat),1,0,1,0]" and "y = [1,0,0,1]" 
+  shows "[0,1] (x\<cdot>x) [1,0] \<sim>\<^sub>\<I> [x,y,x]"
+  unfolding factor_interpretation_def assms by (simp add: suf_def)
+
+section "Primitivity non-preserving binary code"
+
+text\<open>In this section, we give the final form of imprimitive words over a given
+binary code @{term "{x,y}"}.
+We start with a lemma, then we show that the only possibility is that such
+word is conjugate with @{term "x\<^sup>@j \<cdot> y\<^sup>@k"}.\<close>
+
+lemma bin_imprim_expsE_y: assumes "x \<cdot> y \<noteq> y \<cdot> x" and
+  "ws \<in> lists {x,y}" and 
+  "2 \<le> \<^bold>|ws\<^bold>|" and
+  "primitive ws" and
+  "\<not> primitive (concat ws)" and
+  "count_list ws y = 1"
+obtains j k where "1 \<le> j" "1 \<le> k" "j = 1 \<or> k = 1"
+  "ws \<sim> [x]\<^sup>@j \<cdot> [y]\<^sup>@k"
+proof-
+  have "x \<noteq> y" using \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> by blast
+  obtain j1 j2 where "[x]\<^sup>@j1\<cdot>[y]\<cdot>[x]\<^sup>@j2 = ws"
+    using bin_count_one_decompose[OF \<open>ws \<in> lists {x,y}\<close> \<open>x \<noteq> y\<close> \<open>count_list ws y = 1\<close>].
+  have "1 \<le> j2 + j1"
+    using \<open>[x] \<^sup>@ j1 \<cdot> [y] \<cdot> [x] \<^sup>@ j2 = ws\<close> \<open>2 \<le> \<^bold>|ws\<^bold>|\<close> not_less_eq_eq  by fastforce
+  have "ws \<sim> [x]\<^sup>@(j2+j1)\<cdot>[y]\<^sup>@1"
+    using conjugI'[of "[x] \<^sup>@ j1 \<cdot> [y]" "[x] \<^sup>@ j2"]
+    unfolding \<open>[x] \<^sup>@ j1 \<cdot> [y] \<cdot> [x] \<^sup>@ j2 = ws\<close>[symmetric] power_add rassoc pow_one'.
+  from that[OF \<open>1 \<le> j2 + j1\<close> _ _ this]
+  show ?thesis 
+    by blast
+qed
+
+lemma bin_imprim_expsE: assumes "x \<cdot> y \<noteq> y \<cdot> x" and
+  "ws \<in> lists {x,y}" and 
+  "2 \<le> \<^bold>|ws\<^bold>|" and
+  "primitive ws" and
+  "\<not> primitive (concat ws)"
+obtains j k where "1 \<le> j" "1 \<le> k" "j = 1 \<or> k = 1"
+  "ws \<sim> [x]\<^sup>@j \<cdot> [y]\<^sup>@k"
+proof-
+  note \<open>ws \<in> lists {x,y}\<close>[unfolded insert_commute[of x]]
+
+  from bin_lists_count_zero[OF \<open>ws \<in> lists {x,y}\<close>]
+    sing_lists_exp_len[of ws y]
+    prim_exp_one[OF \<open>primitive ws\<close>, of "[y]" "\<^bold>|ws\<^bold>|"]
+  have "count_list ws x \<noteq> 0"
+    using \<open>2 \<le> \<^bold>|ws\<^bold>|\<close> by fastforce
+
+  from bin_lists_count_zero[OF \<open>ws \<in> lists {y,x}\<close>]
+    sing_lists_exp_len[of ws x]
+    prim_exp_one[OF \<open>primitive ws\<close>, of "[x]" "\<^bold>|ws\<^bold>|"]
+  have "count_list ws y \<noteq> 0"
+    using \<open>2 \<le> \<^bold>|ws\<^bold>|\<close> by fastforce
+
+  consider "count_list ws x = 1" | "count_list ws y = 1" 
+    using bin_imprim_both_twice[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> \<open>ws \<in> lists {x,y}\<close> _ _
+        \<open>primitive ws\<close> \<open>\<not> primitive (concat ws)\<close>]
+      \<open>count_list ws x \<noteq> 0\<close> \<open>count_list ws y \<noteq> 0\<close>
+    unfolding One_less_Two_le_iff[symmetric] less_one[symmetric] by fastforce
+  thus thesis
+  proof(cases)
+    assume \<open>count_list ws x = 1\<close>
+    from bin_imprim_expsE_y[reversed, OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> \<open>ws \<in> lists {y, x}\<close> \<open>2 \<le> \<^bold>|ws\<^bold>|\<close>
+        \<open>primitive ws\<close> \<open>\<not> primitive (concat ws)\<close> \<open>count_list ws x = 1\<close>]
+    show thesis 
+      using that by metis
+  next
+    assume \<open>count_list ws y = 1\<close>
+    from bin_imprim_expsE_y[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> \<open>ws \<in> lists {x, y}\<close> \<open>2 \<le> \<^bold>|ws\<^bold>|\<close>
+        \<open>primitive ws\<close> \<open>\<not> primitive (concat ws)\<close> \<open>count_list ws y = 1\<close>]
+    show ?thesis
+      using that.
+  qed
+qed
+
+subsection \<open>The target theorem\<close>
+
+text\<open>Given a binary code @{term "{x,y}"} such that there is a primitive factorisation
+@{term ws} over it whose concatenation is imprimitive, we finally show that there are
+integers @{term j} and @{term k} (depending only on @{term "{x,y}"}) such that
+any other such factorisation @{term ws'} is conjugate to @{term "[x]\<^sup>@j \<cdot> [y]\<^sup>@k"}.\<close>
+
+theorem bin_imprim_code: assumes "x \<cdot> y \<noteq> y \<cdot> x"  and "ws \<in> lists {x,y}" and 
+  "2 \<le> \<^bold>|ws\<^bold>|" and "primitive ws" and  "\<not> primitive (concat ws)"
+obtains j k where "1 \<le> j" and "1 \<le> k" and "j = 1 \<or> k = 1"
+  "\<And>ws. ws \<in> lists {x,y} \<Longrightarrow>  2 \<le> \<^bold>|ws\<^bold>| \<Longrightarrow> 
+       (primitive ws \<and> \<not> primitive (concat ws) \<longleftrightarrow> ws \<sim> [x]\<^sup>@j \<cdot> [y]\<^sup>@k)" and
+  "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>| \<Longrightarrow> 2 \<le> j \<Longrightarrow> j = 2 \<and> primitive x \<and> primitive y" and
+  "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>| \<Longrightarrow> 2 \<le> k \<Longrightarrow> j = 1 \<and> primitive x"
+proof-
+  obtain j k where "1 \<le> j" "1 \<le> k" "j = 1 \<or> k = 1"
+    "ws \<sim> [x]\<^sup>@j \<cdot> [y]\<^sup>@k"
+    using bin_imprim_expsE[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close>]
+    using assms by metis
+
+  have "\<not> primitive (x\<^sup>@j \<cdot> y\<^sup>@k)"
+    using \<open>\<not> primitive (concat ws)\<close> 
+    unfolding concat_morph  concat_sing_pow
+      conjug_prim_iff[OF conjug_concat_conjug[OF \<open>ws \<sim> [x] \<^sup>@ j \<cdot> [y] \<^sup>@ k\<close>]].
+
+  from not_prim_pow[OF this] 
+  obtain z l where [symmetric]: "z\<^sup>@l = x\<^sup>@j \<cdot> y\<^sup>@k" and "2 \<le> l". 
+
+  show thesis
+  proof (rule that[of j k ])
+    show "1 \<le> j" "1 \<le> k" "j = 1 \<or> k = 1" by fact+
+    
+    fix ws'
+    assume hyps: "ws' \<in> lists {x,y}" "2 \<le> \<^bold>|ws'\<^bold>|"
+    show  "primitive ws' \<and> \<not> primitive (concat ws') \<longleftrightarrow> ws' \<sim> [x]\<^sup>@j \<cdot> [y]\<^sup>@k"
+    proof
+      assume " primitive ws' \<and> \<not> primitive (concat ws')"
+      hence prems: "primitive ws'" "\<not> primitive (concat ws')" by blast+ 
+      obtain j' k' where "1 \<le> j'" "1 \<le> k'" "j' = 1 \<or> k' = 1"
+        "ws' \<sim> [x]\<^sup>@j' \<cdot> [y]\<^sup>@k'"
+        using bin_imprim_expsE[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> hyps prems].  
+
+      have "\<not> primitive (x \<^sup>@ j'\<cdot> y \<^sup>@ k')"
+        using  \<open>\<not> primitive (concat ws')\<close>
+        unfolding concat_morph  concat_sing_pow
+          conjug_prim_iff[OF conjug_concat_conjug[OF \<open>ws' \<sim> [x] \<^sup>@ j' \<cdot> [y] \<^sup>@ k'\<close>]].
+
+      have "j = j'" "k = k'"
+        using LS_unique[OF \<open>x \<cdot> y \<noteq> y \<cdot> x\<close> 
+            \<open>1 \<le> j\<close> \<open>1 \<le> k\<close>  \<open>\<not> primitive (x \<^sup>@ j \<cdot> y \<^sup>@ k)\<close>
+            \<open>1 \<le> j'\<close> \<open>1 \<le> k'\<close> \<open>\<not> primitive (x \<^sup>@ j'\<cdot> y \<^sup>@ k')\<close>].
+
+      show "ws' \<sim> [x] \<^sup>@ j \<cdot> [y] \<^sup>@ k"
+        unfolding \<open>j = j'\<close> \<open>k = k'\<close> by fact
+    next
+      assume  "ws' \<sim> [x]\<^sup>@j \<cdot> [y]\<^sup>@k"
+      note conjug_trans[OF \<open>ws \<sim> [x]\<^sup>@j \<cdot> [y]\<^sup>@k\<close> conjug_sym[OF this]]
+      from prim_conjug[OF \<open>primitive ws\<close> this] 
+           \<open>\<not> primitive (concat ws)\<close>[unfolded conjug_concat_prim_iff[OF \<open>ws \<sim> ws'\<close>]]
+      show "primitive ws' \<and> \<not> primitive (concat ws')" by blast
+    qed
+  next  
+    assume "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    interpret LS_len_le x y j k l z
+    by unfold_locales fact+
+
+    assume "2 \<le> j"
+    with jk_small 
+    have "k = 1" by fastforce
+    from case_j2k1[OF \<open>2 \<le> j\<close> this] 
+    show "j = 2 \<and> primitive x \<and> primitive y"
+      by blast
+  next
+    assume "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    interpret LS_len_le x y j k l z
+      by unfold_locales fact+
+
+    assume "2 \<le> k"
+    show "j = 1 \<and> primitive x"
+      using \<open>2 \<le> k\<close> \<open>j = 1 \<or> k = 1\<close>   case_j1k2_primitive by auto 
+  qed
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Binary_Code_Imprimitive/Binary_Square_Interpretation.thy b/thys/Binary_Code_Imprimitive/Binary_Square_Interpretation.thy
new file mode 100644
--- /dev/null
+++ b/thys/Binary_Code_Imprimitive/Binary_Square_Interpretation.thy
@@ -0,0 +1,1063 @@
+(*  Title:      Binary Square Interpretation
+    File:       Combinatorics_Words_Interpretations.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.Equations_Basic 
+begin
+
+section \<open>Lemmas for covered x square\<close>
+
+text \<open>This section explores various variants of the situation when @{term "x \<cdot> x"} is covered with
+ @{term "x\<cdot>y\<^sup>@k\<cdot>u \<cdot> v\<cdot>y\<^sup>@l\<cdot>x"}, with @{term "y = u\<cdot>v"}, and the displayed dots being synchronized. 
+\<close>
+
+subsection \<open>Two particular cases\<close>
+
+\<comment> \<open>Very short and very large overlap\<close>
+
+lemma pref_suf_pers_short: assumes "x \<le>p v \<cdot> x" and "\<^bold>|v \<cdot> u\<^bold>| < \<^bold>|x\<^bold>|" and "x \<le>s p \<cdot> u \<cdot> v \<cdot> u" and "p \<in> \<langle>{u,v}\<rangle>"   
+  \<comment> \<open>@{term "x \<cdot> x"} is covered by @{term "(p\<cdot>u\<cdot>v\<cdot>u) \<cdot> (v\<cdot>x)"}, the displayed dots being synchronized\<close>
+  \<comment> \<open>That is, the condition on the first @{term x} in @{term "x\<cdot>y\<^sup>@k\<cdot>u \<cdot> v\<cdot>y\<^sup>@l\<cdot>x"} is relaxed\<close>
+  shows "u\<cdot>v = v\<cdot>u"
+proof (rule nemp_comm)
+  have "v \<cdot> u <s x" 
+    using suf_prod_long_less[OF _  \<open>\<^bold>|v \<cdot> u\<^bold>| < \<^bold>|x\<^bold>|\<close>, of "p \<cdot> u", unfolded rassoc, OF \<open>x \<le>s p \<cdot> u \<cdot> v \<cdot> u\<close>].
+  assume "u \<noteq> \<epsilon>" and "v \<noteq> \<epsilon>"
+  obtain q where "x = q \<cdot> v \<cdot> u" and "q \<noteq> \<epsilon>"
+    using \<open>v \<cdot> u <s x\<close>  by (auto simp add: suf_def)
+  hence "q \<le>s p \<cdot> u"
+    using \<open>x \<le>s p \<cdot> u \<cdot> v \<cdot> u\<close> by (auto simp add: suf_def)
+  have "q \<cdot> v = v \<cdot> q"
+    using pref_marker[OF \<open>x \<le>p v\<cdot>x\<close>, of q ] \<open>x = q \<cdot> v \<cdot> u\<close> by simp
+  from suf_marker_per_root[OF \<open>x \<le>p v \<cdot> x\<close>, of q u, unfolded rassoc \<open>x = q \<cdot> v \<cdot> u\<close>]
+  have "u \<le>p v \<cdot> u" 
+    by blast
+  from root_comm_root[OF this \<open>q\<cdot>v = v\<cdot>q\<close> \<open>v \<noteq> \<epsilon>\<close>]
+  have  "u \<le>p q \<cdot> u" by simp 
+
+  consider  "u \<le>s q" | "q \<le>s u"
+    using \<open>q \<le>s p \<cdot> u\<close> suffix_same_cases by blast 
+  thus "u\<cdot>v = v\<cdot>u"
+  proof (cases)
+    assume "u \<le>s q"
+    from two_elem_root_suf_comm'[OF \<open>u \<le>p v \<cdot> u\<close> _ _ \<open>p \<in> \<langle>{u,v}\<rangle>\<close>, of "q\<^sup><\<inverse>u", unfolded rq_suf[OF this] lassoc, OF _ \<open>q \<cdot> v = v \<cdot> q\<close>] 
+    show ?thesis
+      using \<open>q \<le>s p \<cdot> u\<close>  rq_suf[OF \<open>u \<le>s q\<close>] same_suffix_suffix by metis
+  next
+    assume "q \<le>s u"
+    from root_suf_comm[OF \<open>u \<le>p q \<cdot> u\<close> suffix_appendI[OF this]]
+    have "q\<cdot>u = u\<cdot>q". 
+    from comm_trans[OF \<open>q \<cdot> u = u \<cdot> q\<close>[symmetric] \<open>q \<cdot> v = v \<cdot> q\<close>[symmetric] \<open>q \<noteq> \<epsilon>\<close>]
+    show "u\<cdot>v = v\<cdot>u".
+  qed
+qed 
+
+lemma pref_suf_pers_large_overlap: 
+  assumes
+    "p \<le>p x" and "s \<le>s x" and "p \<le>p r \<cdot> p" and "s \<le>s s \<cdot> r" and "\<^bold>|x\<^bold>| + \<^bold>|r\<^bold>| \<le> \<^bold>|p\<^bold>| + \<^bold>|s\<^bold>|"
+  shows "x \<cdot> r = r \<cdot> x"      
+  using assms
+proof (cases "r = \<epsilon>", force)
+  assume "r \<noteq> \<epsilon>" hence "r \<noteq> \<epsilon>" by blast
+  have "\<^bold>|s\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    using \<open>s \<le>s x\<close> unfolding suf_def by force
+  have "\<^bold>|p\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    using \<open>p \<le>p x\<close> by (force simp add: prefix_def)
+  have "\<^bold>|r\<^bold>| \<le> \<^bold>|p\<^bold>|"
+    using \<open>\<^bold>|x\<^bold>| + \<^bold>|r\<^bold>| \<le> \<^bold>|p\<^bold>| + \<^bold>|s\<^bold>|\<close> \<open>\<^bold>|s\<^bold>| \<le> \<^bold>|x\<^bold>|\<close> unfolding lenmorph by linarith 
+  have "\<^bold>|r\<^bold>| \<le> \<^bold>|s\<^bold>|"
+    using \<open>\<^bold>|x\<^bold>| + \<^bold>|r\<^bold>| \<le> \<^bold>|p\<^bold>| + \<^bold>|s\<^bold>|\<close> \<open>\<^bold>|p\<^bold>| \<le> \<^bold>|x\<^bold>|\<close> unfolding lenmorph by linarith 
+  obtain p1 ov s1 where "p1 \<cdot> ov \<cdot> s1 = x"  and "p1 \<cdot> ov = p" and "ov \<cdot> s1 = s"  
+    using pref_suf_overlapE[OF \<open>p \<le>p x\<close> \<open>s \<le>s x\<close>] using \<open>\<^bold>|x\<^bold>| + \<^bold>|r\<^bold>| \<le> \<^bold>|p\<^bold>| + \<^bold>|s\<^bold>|\<close> by auto
+  have "\<^bold>|r\<^bold>| \<le> \<^bold>|ov\<^bold>|" 
+    using \<open>\<^bold>|x\<^bold>| + \<^bold>|r\<^bold>| \<le> \<^bold>|p\<^bold>| + \<^bold>|s\<^bold>|\<close>[folded \<open>p1 \<cdot> ov \<cdot> s1 = x\<close> \<open>p1 \<cdot> ov = p\<close> \<open>ov \<cdot> s1 = s\<close>]
+    unfolding lenmorph by force
+  have "r \<le>p p"
+    using \<open>\<^bold>|r\<^bold>| \<le> \<^bold>|p\<^bold>|\<close>[unfolded swap_len] pref_prod_long[OF \<open>p \<le>p r \<cdot> p\<close>] by blast 
+  hence "r \<le>p x"
+    using \<open>p \<le>p x\<close> by auto
+  have "r \<le>s s"
+    using \<open>\<^bold>|r\<^bold>| \<le> \<^bold>|s\<^bold>|\<close>[unfolded swap_len] pref_prod_long[reversed, OF \<open>s \<le>s s \<cdot> r\<close>] by blast 
+  hence "r \<le>s x"
+    using \<open>s \<le>s x\<close> by auto
+  obtain k where "p \<le>p r\<^sup>@k"
+    using per_prefE[OF \<open>p \<le>p r \<cdot> p\<close> \<open>r \<noteq> \<epsilon>\<close>]. 
+  hence "p1 \<cdot> ov \<le>f r\<^sup>@k"
+    unfolding \<open>p1 \<cdot> ov = p\<close> by blast
+  obtain l where "s \<le>s r\<^sup>@l"
+    using per_prefE[reversed, OF \<open>s \<le>s s \<cdot> r\<close> \<open>r \<noteq> \<epsilon>\<close>].
+  hence "ov \<cdot> s1 \<le>f r\<^sup>@l"
+    unfolding \<open>ov \<cdot> s1 = s\<close> by blast
+  from per_glue_facs[OF \<open>p1 \<cdot> ov \<le>f r\<^sup>@k\<close> \<open>ov \<cdot> s1 \<le>f r\<^sup>@l\<close> \<open>\<^bold>|r\<^bold>| \<le> \<^bold>|ov\<^bold>|\<close>, unfolded \<open>p1 \<cdot> ov \<cdot> s1 = x\<close>]
+  obtain m where "x \<le>f r \<^sup>@ m".
+  show "x \<cdot> r = r \<cdot> x" 
+    using root_suf_comm[OF
+        pref_prod_root[OF marker_fac_pref[OF \<open>x \<le>f r \<^sup>@ m\<close> \<open>r \<le>p x\<close>]]
+        suffix_appendI[OF \<open>r \<le>s x\<close>]]..  
+qed
+
+subsection \<open>Main cases\<close>
+
+locale pref_suf_pers = 
+  fixes x u v k m
+  assumes 
+    x_pref:  "x \<le>p (v \<cdot> (u \<cdot> v)\<^sup>@(Suc k)) \<cdot> x" \<comment> \<open>@{term "x \<le>p p \<cdot> x"} and @{term "p \<le>p q \<cdot> p"} where @{term "q \<le>p v \<cdot> u"}\<close> 
+ and
+    x_suf:  "x \<le>s x \<cdot> (u \<cdot> v)\<^sup>@(Suc m) \<cdot> u" \<comment> \<open>@{term "x \<le>s s \<cdot> x"} and @{term "s \<le>s q' \<cdot> s"} where @{term "q' \<le>p u \<cdot> v"}\<close>
+begin
+
+lemma pref_suf_commute_all_commutes:
+  assumes  "\<^bold>|u \<cdot> v\<^bold>| \<le> \<^bold>|x\<^bold>|" and "u \<cdot> v = v \<cdot> u"
+  shows "commutes {u,v,x}"
+  using assms
+proof (cases "u \<cdot> v = \<epsilon>", force)
+  let ?p = "(v \<cdot> (u \<cdot> v)\<^sup>@(Suc k))"
+  let ?s = "(u \<cdot> v)\<^sup>@(Suc m) \<cdot> u"
+  note x_pref x_suf
+
+  assume "u \<cdot> v \<noteq> \<epsilon>"
+  have "?p \<noteq> \<epsilon>" and "?s \<noteq> \<epsilon>" and "v \<cdot> u \<noteq> \<epsilon>"
+    using \<open>u \<cdot> v \<noteq> \<epsilon>\<close> by force+
+  obtain r where "u \<in> r*" and "v \<in> r*" and "primitive r"
+    using \<open>u \<cdot> v = v \<cdot> u\<close> comm_primrootE by metis
+  hence "r \<noteq> \<epsilon>"
+    by force
+
+  have "?p \<in> r*" and "?s \<in> r*" and "v \<cdot> u \<in> r*" and "u \<cdot> v \<in> r*" 
+    using \<open>u \<in> r*\<close> \<open>v \<in> r*\<close> by fast+
+
+  have "x \<le>p r \<cdot> x"
+    using  \<open>?p \<in> r*\<close> \<open>x \<le>p ?p \<cdot> x\<close> \<open>?p \<noteq> \<epsilon>\<close> by blast 
+  have "v \<cdot> u \<le>s x"
+    using ruler_le[reversed, OF _ _ \<open>\<^bold>|u \<cdot> v\<^bold>| \<le> \<^bold>|x\<^bold>|\<close>[unfolded swap_len[of u]], 
+        of  "(x \<cdot> (u \<cdot> v) \<^sup>@ m \<cdot> u) \<cdot> v \<cdot> u", OF triv_suf, unfolded rassoc, OF \<open>x \<le>s x \<cdot> ?s\<close>[unfolded pow_Suc2 rassoc]]. 
+  have "r \<le>s  v \<cdot> u" 
+    using  \<open>v \<cdot> u \<noteq> \<epsilon>\<close> \<open>v \<cdot> u \<in> r*\<close> by blast
+  have "r \<le>s r \<cdot> x"
+    using suf_trans[OF \<open>r \<le>s  v \<cdot> u\<close> \<open>v \<cdot> u \<le>s x\<close>, THEN suffix_appendI] by blast 
+  have "x \<cdot> r  = r \<cdot> x"
+    using  root_suf_comm[OF \<open>x \<le>p r \<cdot> x\<close> \<open>r \<le>s r \<cdot> x\<close>, symmetric].
+  hence "x \<in> r*"
+    by (simp add: \<open>primitive r\<close> prim_comm_root) 
+  thus "commutes {u,v,x}" 
+    using \<open>u \<in> r*\<close> \<open>v \<in> r*\<close> commutesI_root[of "{u,v,x}"] by blast
+qed
+
+lemma no_overlap:
+  assumes
+    len: "\<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@(Suc k)\<^bold>| + \<^bold>|(u \<cdot> v)\<^sup>@(Suc m) \<cdot> u\<^bold>| \<le> \<^bold>|x\<^bold>|" (is "\<^bold>|?p\<^bold>| + \<^bold>|?s\<^bold>| \<le> \<^bold>|x\<^bold>|")
+  shows "commutes {u,v,x}"
+  using assms
+proof (cases "u \<cdot> v = \<epsilon>", force)
+  note x_pref x_suf
+  assume "u \<cdot> v \<noteq> \<epsilon>"
+  have "?p \<noteq> \<epsilon>" and "?s \<noteq> \<epsilon>"
+    using \<open>u \<cdot> v \<noteq> \<epsilon>\<close> by force+
+  from \<open>\<^bold>|?p\<^bold>| + \<^bold>|?s\<^bold>| \<le> \<^bold>|x\<^bold>|\<close>  
+  have "\<^bold>|?p\<^bold>| + \<^bold>|?s\<^bold>| - (gcd \<^bold>|?p\<^bold>| \<^bold>|?s\<^bold>|) \<le> \<^bold>|x\<^bold>|"
+    by linarith
+  from per_lemma_pref_suf[OF \<open>x \<le>p ?p \<cdot> x\<close> \<open>x \<le>s x \<cdot> ?s\<close> \<open>?p \<noteq> \<epsilon>\<close> \<open>?s \<noteq> \<epsilon>\<close> this]
+  obtain r s kp ks mw where "?p = (r \<cdot> s)\<^sup>@kp" and "?s = (s \<cdot> r)\<^sup>@ks" and "x = (r \<cdot> s)\<^sup>@mw \<cdot> r" and "primitive (r \<cdot> s)".
+  hence "\<rho> ?p = r \<cdot> s"
+    using \<open>v \<cdot> (u \<cdot> v) \<^sup>@ Suc k \<noteq> \<epsilon>\<close> comm_primroots nemp_pow_nemp pow_comm prim_self_root by metis
+  moreover have "\<rho> ?s = s \<cdot> r" 
+    using   pow_prim_primroot[OF \<open>?s \<noteq> \<epsilon>\<close> _ \<open>?s = (s \<cdot> r)\<^sup>@ks\<close>] prim_conjug[OF \<open>primitive (r \<cdot> s)\<close>] by blast
+  ultimately have "\<rho> ?p \<sim> \<rho> ?s" 
+    by force
+  from conj_pers_conj_comm[OF this]
+  have "u \<cdot> v = v \<cdot> u".
+
+  from pref_suf_commute_all_commutes[OF _ this]
+  show "commutes {u,v,x}" 
+    using len by auto
+qed
+
+lemma no_overlap':
+  assumes
+    len: "\<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@(Suc k)\<^bold>| + \<^bold>|(u \<cdot> v)\<^sup>@(Suc m) \<cdot> u\<^bold>| \<le> \<^bold>|x\<^bold>|" (is "\<^bold>|?p\<^bold>| + \<^bold>|?s\<^bold>| \<le> \<^bold>|x\<^bold>|")
+  shows "u \<cdot> v = v \<cdot> u"
+  by (rule commutesE[of "{u,v,x}"], simp_all add: no_overlap[OF len]) 
+
+lemma short_overlap: 
+  assumes
+    len1: "\<^bold>|x\<^bold>| < \<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@(Suc k)\<^bold>| + \<^bold>|(u \<cdot> v)\<^sup>@(Suc m) \<cdot> u\<^bold>|" (is "\<^bold>|x\<^bold>| < \<^bold>|?p\<^bold>| + \<^bold>|?s\<^bold>|") and
+    len2: "\<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@(Suc k)\<^bold>| + \<^bold>|(u \<cdot> v)\<^sup>@(Suc m) \<cdot> u\<^bold>| \<le> \<^bold>|x\<^bold>| + \<^bold>|u\<^bold>|" (is "\<^bold>|?p\<^bold>| + \<^bold>|?s\<^bold>| \<le> \<^bold>|x\<^bold>| + \<^bold>|u\<^bold>|")
+  shows "commutes {u,v,x}"
+proof (rule pref_suf_commute_all_commutes)
+  show "\<^bold>|u \<cdot> v\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    using len2  by force
+next
+  note x_pref x_suf
+    \<comment> \<open>obtain the overlap\<close>
+
+  have "\<^bold>|?p\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    using  len2 unfolding lenmorph by linarith
+  hence "?p \<le>p x"
+    using \<open>x \<le>p ?p \<cdot> x\<close> pref_prod_long by blast 
+
+  have "\<^bold>|?s\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    using  len2 unfolding pow_len lenmorph by auto
+  hence "?s \<le>s x"
+    using suf_prod_long[OF \<open>x \<le>s x \<cdot> ?s\<close>] by blast 
+
+  from  pref_suf_overlapE[OF \<open>?p \<le>p x\<close> \<open>?s \<le>s x\<close> less_imp_le[OF len1]]
+  obtain p1 ov s1 where "p1 \<cdot> ov \<cdot> s1 = x" and "p1 \<cdot> ov = ?p" and "ov \<cdot> s1 = ?s".
+
+  from len1[folded this]
+  have "ov \<noteq> \<epsilon>"
+    by fastforce 
+
+  have "\<^bold>|ov\<^bold>| \<le> \<^bold>|u\<^bold>|"
+    using len2[folded \<open>p1 \<cdot> ov \<cdot> s1 = x\<close> \<open>p1 \<cdot> ov = ?p\<close> \<open>ov \<cdot> s1 = ?s\<close>] unfolding lenmorph by auto
+
+  then obtain s' where "ov \<cdot> s' = u" and "s' \<cdot> v \<cdot> (u \<cdot> v) \<^sup>@ m \<cdot> u = s1"
+    using eqdE[OF \<open>ov \<cdot> s1 = ?s\<close>[unfolded pow_Suc rassoc]] by auto
+
+\<comment> \<open>obtain the left complement\<close>
+
+  from   eqdE[reversed, of p1 ov "v \<cdot> (u \<cdot> v)\<^sup>@k" "u \<cdot> v", unfolded rassoc, 
+      OF \<open>p1 \<cdot> ov = ?p\<close>[unfolded pow_Suc2]]  \<open>\<^bold>|ov\<^bold>| \<le> \<^bold>|u\<^bold>|\<close>
+  have "v \<cdot> (u \<cdot> v) \<^sup>@ k  \<le>p p1" by (auto simp add: prefix_def)
+
+  then obtain q where "v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> q = p1" 
+    by (force simp add: prefix_def)
+
+\<comment> \<open>main proof using the lemma @{thm uvu_suf_uvvu}\<close>
+
+  show "u \<cdot> v = v \<cdot> u"
+  proof (rule sym, rule uvu_suf_uvvu)
+    show "s' <s u" 
+      using \<open>ov \<cdot> s' = u\<close> \<open>ov \<noteq> \<epsilon>\<close> by blast
+    show "u \<cdot> v \<cdot> v \<cdot> u \<cdot> s' = q \<cdot> u \<cdot> v \<cdot> u" \<comment> \<open>the main fact: the overlap situation\<close>
+    proof-
+      have "u \<cdot> v \<cdot> u \<le>p ?s"
+        unfolding pow_Suc rassoc pref_cancel_conv shift_pow by blast
+      hence "p1 \<cdot> u \<cdot> v \<cdot> u \<le>p x"
+        unfolding \<open>p1 \<cdot> ov \<cdot> s1 = x\<close>[symmetric] \<open>ov \<cdot> s1 = ?s\<close> pref_cancel_conv.
+      hence "v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> q \<cdot> u \<cdot> v \<cdot> ov \<le>p x"
+        using \<open>v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> q = p1\<close> \<open>ov \<cdot> s' = u\<close> by (force simp add: prefix_def)
+
+      have "v \<cdot> u \<le>p x"
+        using \<open>?p \<le>p x\<close>[unfolded pow_Suc] by (auto simp add: prefix_def)
+      have "\<^bold>|?p \<cdot> v \<cdot> u\<^bold>| \<le> \<^bold>|x\<^bold>|"
+        using len2 unfolding lenmorph by force  
+      hence "?p \<cdot> v \<cdot> u \<le>p x"
+        using \<open>x \<le>p ?p \<cdot> x\<close> \<open>v \<cdot> u \<le>p x\<close> pref_prod_longer by blast
+      hence "v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> u \<cdot> v \<cdot> v \<cdot> u \<le>p x"
+        unfolding pow_Suc2 rassoc.
+
+      have "\<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> u \<cdot> v \<cdot> v \<cdot> u\<^bold>| = \<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> q \<cdot> u \<cdot> v \<cdot> ov\<^bold>|"
+        using lenarg[OF \<open>p1 \<cdot> ov = ?p\<close>[folded \<open>v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> q = p1\<close>, unfolded pow_Suc2 rassoc cancel]]
+        by force
+
+      from ruler_eq_len[OF  \<open>v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> u \<cdot> v \<cdot> v \<cdot> u \<le>p x\<close> \<open>v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> q \<cdot> u \<cdot> v \<cdot> ov \<le>p x\<close> this, unfolded cancel]
+      have "u \<cdot> v \<cdot> v \<cdot> u = q \<cdot> u \<cdot> v \<cdot> ov".
+
+      thus  "u \<cdot> v \<cdot> v \<cdot> u \<cdot> s' = q \<cdot> u \<cdot> v \<cdot> u"
+        using \<open>ov \<cdot> s' = u\<close> by auto
+    qed
+    show "q \<le>s v \<cdot> u"
+    proof (rule ruler_le[reversed])
+      show "q \<le>s x"
+      proof (rule suf_trans)
+        show "p1 \<le>s x"
+          using \<open>p1 \<cdot> ov \<cdot> s1 = x\<close>[unfolded \<open>ov \<cdot> s1 = ?s\<close>] \<open>x \<le>s x \<cdot> ?s\<close>  same_suffix_suffix by blast
+        show "q \<le>s p1"
+          using \<open>v \<cdot> (u \<cdot> v) \<^sup>@ k \<cdot> q = p1\<close> by auto 
+      qed                                                  
+      show "v \<cdot> u \<le>s x"
+        using \<open>?s \<le>s x\<close>[unfolded pow_Suc2 rassoc] suffix_appendD by metis  
+      show "\<^bold>|q\<^bold>| \<le> \<^bold>|v \<cdot> u\<^bold>|" 
+        using lenarg[OF \<open>u \<cdot> v \<cdot> v \<cdot> u \<cdot> s' = q \<cdot> u \<cdot> v \<cdot> u\<close>] lenarg[OF \<open>ov \<cdot> s' = u\<close>] by force
+    qed
+  qed auto
+qed
+
+lemma medium_overlap:
+  assumes 
+    len1: "\<^bold>|x\<^bold>| + \<^bold>|u\<^bold>| < \<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@(Suc k)\<^bold>| + \<^bold>|(u \<cdot> v)\<^sup>@(Suc m) \<cdot> u\<^bold>|" (is "\<^bold>|x\<^bold>| + \<^bold>|u\<^bold>| < \<^bold>|?p\<^bold>| + \<^bold>|?s\<^bold>|") and
+    len2: "\<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@(Suc k)\<^bold>| + \<^bold>|(u \<cdot> v)\<^sup>@(Suc m) \<cdot> u\<^bold>| < \<^bold>|x\<^bold>| + \<^bold>|u \<cdot> v\<^bold>|" (is "\<^bold>|?p\<^bold>| + \<^bold>|?s\<^bold>| < \<^bold>|x\<^bold>| + \<^bold>|u \<cdot> v\<^bold>|")
+  shows "commutes {u,v,x}"
+proof (rule pref_suf_commute_all_commutes)
+  show "\<^bold>|u \<cdot> v\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    using len2  by force
+next
+  note x_pref x_suf
+  have "\<^bold>|?p\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    using  len2 by auto 
+  hence "?p \<le>p x"
+    using \<open>x \<le>p ?p \<cdot> x\<close> pref_prod_long by blast 
+  hence  "v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> u \<cdot> v \<cdot> v \<le>p ?p \<cdot> x"
+    using \<open>x \<le>p ?p \<cdot> x\<close>  unfolding pow_Suc2 rassoc  by (auto simp add: prefix_def)
+
+  have "\<^bold>|?s\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    using  len2 unfolding pow_len lenmorph by auto
+  hence "?s \<le>s x"
+    using suf_prod_long[OF \<open>x \<le>s x \<cdot> ?s\<close>] by blast
+  then obtain p' where "p' \<cdot> u \<cdot> v \<le>p x" and "p' \<cdot> ?s = x"
+    by (auto simp add: suf_def)
+
+  have "\<^bold>|p' \<cdot> u \<cdot> v\<^bold>| \<le> \<^bold>|?p \<cdot> v\<^bold>|"
+    using len1[folded \<open>p' \<cdot> ?s = x\<close>] by force
+
+  have "\<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@k\<^bold>|  < \<^bold>|p'\<^bold>|"
+    using len2[folded \<open>p' \<cdot> ?s = x\<close>] by force
+
+  from less_imp_le[OF this]
+  obtain p where "v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> p = p'"
+    using ruler_le[OF \<open>?p \<le>p x\<close> \<open>p' \<cdot> u \<cdot> v \<le>p x\<close>, unfolded pow_Suc2 lassoc, THEN pref_cancel_right, THEN pref_cancel_right]  
+    by (auto simp add: prefix_def)
+
+  have "\<^bold>|p\<^bold>| \<le> \<^bold>|v\<^bold>|"
+    using \<open>v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> p = p'\<close> \<open>\<^bold>|p' \<cdot> u \<cdot> v\<^bold>| \<le> \<^bold>|?p \<cdot> v\<^bold>|\<close> by force
+
+  show "u \<cdot> v = v \<cdot> u"
+  proof (rule uv_fac_uvv)
+    show "p \<cdot> u \<cdot> v \<le>p u \<cdot> v \<cdot> v"
+    proof (rule pref_cancel[of "v \<cdot> (u \<cdot> v)\<^sup>@k"], rule ruler_le)
+      show "(v \<cdot> (u \<cdot> v) \<^sup>@ k) \<cdot> p \<cdot> u \<cdot> v \<le>p ?p \<cdot> x"
+        unfolding lassoc \<open>v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> p = p'\<close>[unfolded lassoc]
+        using \<open>p' \<cdot> u \<cdot> v \<le>p x\<close> \<open>x \<le>p ?p \<cdot> x\<close> by force 
+      show "(v \<cdot> (u \<cdot> v) \<^sup>@ k) \<cdot> u \<cdot> v \<cdot> v \<le>p (v \<cdot> (u \<cdot> v) \<^sup>@ Suc k) \<cdot> x"
+        unfolding pow_Suc2 rassoc
+        using \<open>v \<cdot> (u \<cdot> v) \<^sup>@ Suc k \<le>p x\<close> by (auto simp add: prefix_def)    
+      show "\<^bold>|(v \<cdot> (u \<cdot> v) \<^sup>@ k) \<cdot> p \<cdot> u \<cdot> v\<^bold>| \<le> \<^bold>|(v \<cdot> (u \<cdot> v) \<^sup>@ k) \<cdot> u \<cdot> v \<cdot> v\<^bold>|" 
+        using \<open>v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> p = p'\<close> \<open>\<^bold>|p' \<cdot> u \<cdot> v\<^bold>| \<le> \<^bold>|?p \<cdot> v\<^bold>|\<close> by force
+    qed
+
+    have "p \<le>s x" 
+      using  \<open>p' \<cdot> ?s = x\<close>[folded \<open>v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> p = p'\<close>] \<open>x \<le>s x \<cdot> ?s\<close> suf_cancel suffix_appendD by metis 
+
+    from ruler_le[reversed, OF this \<open>?s \<le>s x\<close>, unfolded pow_Suc2 rassoc]
+    show "p \<le>s (u \<cdot> v) \<^sup>@ m \<cdot> u \<cdot> v \<cdot> u"
+      using  \<open>\<^bold>|p\<^bold>| \<le> \<^bold>|v\<^bold>|\<close> unfolding lenmorph by auto
+
+    show "(u \<cdot> v) \<^sup>@ m \<cdot> u \<cdot> v \<cdot> u \<in> \<langle>{u, v}\<rangle>"
+      by (simp add: gen_in hull_closed power_in)
+
+    show "p \<noteq> \<epsilon>" 
+      using \<open>\<^bold>|v \<cdot> (u \<cdot> v)\<^sup>@k\<^bold>|  < \<^bold>|p'\<^bold>|\<close> \<open>v \<cdot> (u \<cdot> v)\<^sup>@k \<cdot> p = p'\<close> 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 \<open>Square interpretation\<close>
+
+text \<open>In this section fundamental description is given of (the only) 
+possible @{term "{x,y}"}-interpretation of the square @{term "x\<cdot>x"}, where @{term "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|"}. 
+The proof is divided into several locales.
+\<close>
+
+\<comment> \<open>An example motivating disjointness: an interpretation which is not disjoint.\<close>
+lemma cover_not_disjoint:
+  shows "primitive [0::nat,1,0,1,0,1,0]" (is "primitive ?x") and
+    "primitive[0::nat, 1]" (is "primitive ?y") and
+    "[0::nat,1,0,1,0,1,0] \<cdot> [0,1] \<noteq> [0,1] \<cdot> [0,1,0,1,0,1,0]" 
+    (is "?x \<cdot> ?y \<noteq> ?y \<cdot> ?x") and 
+    "\<epsilon> [0::nat,1,0,1,0,1,0] \<cdot> [0,1,0,1,0,1,0] [1,0,1,0] \<sim>\<^sub>\<I> [[0,1,0,1,0,1,0],[0,1],[0,1],[0,1,0,1,0,1,0]]"
+    (is "\<epsilon> ?x \<cdot> ?x ?s \<sim>\<^sub>\<I> [?x,?y,?y,?x]") 
+  unfolding factor_interpretation_def  
+  by (primitivity_inspection+) force
+
+subsection \<open>Locale: interpretation\<close>
+
+locale square_interp =
+  \<comment> \<open>The basic set of assumptions\<close>
+  \<comment> \<open>The goal is to arrive at @{term "ws = [x] \<cdot> [y]\<^sup>@k \<cdot> [x]"} including the description 
+   of the interpretation in terms of the first and the second occurrence of x in the interpreted square.\<close>
+  fixes x y p s ws  
+  assumes
+    prim_x: "primitive x" and prim_y: "primitive y" and
+    y_le_x: "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|" and
+    ws_lists: "ws \<in> lists {x,y}" and
+    nconjug: "\<not> x \<sim> y" and
+    disjoint:   "\<And> p1 p2. p1 \<le>p [x,x] \<Longrightarrow> p2 \<le>p ws \<Longrightarrow> p \<cdot> concat p1 \<noteq> concat p2" and
+    interp: "p (x\<cdot>x) s \<sim>\<^sub>\<I> ws"
+
+begin
+
+interpretation binary_code x y
+  using binary_code_def comm_prim nconjug nconjug_neq prim_x prim_y by metis
+
+lemmas interpret_concat = fac_interpretE(3)[OF interp]
+
+lemma p_nemp:  "p \<noteq> \<epsilon>"
+  using disjoint[of \<epsilon> \<epsilon>] by auto
+
+lemma s_nemp: "s \<noteq> \<epsilon>"
+  using disjoint[of "[x,x]" ws] interpret_concat by force
+
+lemma x_root: "\<rho> x = x"
+  using prim_x by blast
+
+lemma y_root: "\<rho> y = y"
+  using prim_y by blast
+
+lemma ws_nemp: "ws \<noteq> \<epsilon>"
+  using bin_fst_nemp fac_interpret_nemp interp by blast
+
+lemma hd_ws_lists: "hd ws \<in> {x, y}"
+  using lists_hd_in_set ws_lists ws_nemp by auto
+
+lemma last_ws_lists: "last ws \<in> {x, y}"
+  using lists_hd_in_set[reversed, OF ws_nemp ws_lists].
+
+lemma kE: obtains k where "[hd ws] \<cdot> [y]\<^sup>@k \<cdot> [last ws] = ws"
+proof-
+  from  list.collapse[OF ws_nemp] hd_word
+  obtain ws' where "ws = [hd ws] \<cdot> ws'"
+    by metis
+  hence "\<^bold>|hd ws\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    using  two_elem_cases[OF lists_hd_in_set[OF ws_nemp ws_lists]] y_le_x by blast
+  hence "\<^bold>|x\<^bold>| \<le> \<^bold>|concat ws'\<^bold>|"
+    using lenarg[OF interpret_concat, unfolded lenmorph]
+    unfolding concat.simps clean_emp  arg_cong[OF \<open>ws = [hd ws] \<cdot> ws'\<close>, of "\<lambda> x. \<^bold>|concat x\<^bold>|", unfolded concat_morph lenmorph] 
+    by linarith  
+  hence "ws' \<noteq> \<epsilon>"
+    using nemp_len[OF bin_fst_nemp] by fastforce
+  then obtain mid_ws where "ws' = mid_ws \<cdot> [last ws]"
+    using \<open>ws = [hd ws] \<cdot> ws'\<close> append_butlast_last_id last_appendR by metis
+  note \<open>ws = [hd ws] \<cdot> ws'\<close>[unfolded this]
+       fac_interpretE[OF interp]
+  obtain p' where [symmetric]:"p \<cdot> p' = hd ws" and "p' \<noteq> \<epsilon>" 
+    using sprefE[OF \<open>p <p hd ws\<close>].
+  obtain s' where  [symmetric]: "s'\<cdot> s  = last ws" and "s' \<noteq> \<epsilon>" 
+    using sprefE[reversed, OF \<open>s <s last ws\<close>].
+  have "p' \<cdot> concat mid_ws \<cdot> s' = x \<cdot> x"  
+    using \<open>ws = [hd ws] \<cdot> mid_ws \<cdot> [last ws]\<close>[unfolded \<open>hd ws = p \<cdot> p'\<close> \<open>last ws  = s'\<cdot> s\<close>] 
+           \<open>p \<cdot> (x \<cdot> x) \<cdot> s = concat ws\<close> by simp
+  note over = prim_overlap_sqE[OF prim_x, folded this]
+  have "mid_ws \<in> lists {x,y}"
+    using \<open>ws = [hd ws] \<cdot> ws'\<close> \<open>ws' = mid_ws \<cdot> [last ws]\<close> append_in_lists_conv ws_lists by metis 
+  have "x \<notin> set mid_ws" 
+  proof
+    assume "x \<in> set mid_ws"
+    then obtain r q where "concat mid_ws = r \<cdot> x \<cdot> q"
+      using concat.simps(2) concat_morph in_set_conv_decomp_first by metis
+    have "(p' \<cdot> r)  \<cdot> x \<cdot> (q \<cdot> s') = x \<cdot> x" 
+      using \<open>p' \<cdot> concat mid_ws \<cdot> s' = x \<cdot> x\<close>[unfolded \<open>concat mid_ws = r \<cdot> x \<cdot> q\<close>]
+      unfolding rassoc.
+    from prim_overlap_sqE[OF prim_x this]
+    show False
+      using \<open>p' \<noteq> \<epsilon>\<close> \<open>s' \<noteq> \<epsilon>\<close> by blast
+  qed
+  hence "mid_ws \<in> lists {y}"
+    using \<open>mid_ws \<in> lists {x,y}\<close> by force
+  from that sing_lists_exp[OF this]
+  show thesis 
+    using \<open>ws = [hd ws] \<cdot> mid_ws \<cdot> [last ws]\<close> by metis
+qed
+
+lemma l_mE: obtains m u v l where "(hd ws)\<cdot>y\<^sup>@m\<cdot>u = p\<cdot>x" and "v \<cdot> y\<^sup>@l \<cdot> (last ws) = x \<cdot> s" and
+  "u\<cdot>v = y"  and "u \<cdot> v \<noteq> v \<cdot> u"
+proof-
+  note fac_interpretE[OF interp]
+  obtain k where "[hd ws] \<cdot> [y]\<^sup>@k \<cdot> [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 \<cdot> y\<^sup>@k \<cdot> last ws = p \<cdot> x \<cdot> x \<cdot> s". 
+  have "\<^bold>|hd ws\<^bold>| \<le> \<^bold>|p \<cdot> x\<^bold>|"
+   unfolding lenmorph using y_le_x two_elem_cases[OF hd_ws_lists] using dual_order.trans by fastforce
+  from eqd[OF _ this]
+  obtain ya where "hd ws \<cdot> ya = p \<cdot> x"
+    using \<open>hd ws \<cdot> y\<^sup>@k \<cdot> last ws = p \<cdot> x \<cdot> x \<cdot> s\<close>  by auto 
+  have "\<^bold>|last ws\<^bold>| \<le> \<^bold>|x\<^bold>|"
+    unfolding lenmorph using dual_order.trans last_ws_lists y_le_x by auto 
+  hence "\<^bold>|last ws\<^bold>| < \<^bold>|x \<cdot> s\<^bold>|"
+    unfolding lenmorph using nemp_len[OF s_nemp] by linarith  
+  from eqd[reversed, OF _ less_imp_le[OF this]]                                            
+  obtain yb where "yb \<cdot> (last ws) = x \<cdot> s"
+    using \<open>(hd ws) \<cdot> y\<^sup>@k \<cdot> (last ws) = p \<cdot> x \<cdot> x \<cdot> s\<close> rassoc by metis 
+  hence "yb \<noteq> \<epsilon>"  
+    using s_nemp \<open>\<^bold>|last ws\<^bold>| < \<^bold>|x \<cdot> s\<^bold>|\<close> by force 
+  have "ya \<cdot> yb = y\<^sup>@k"
+    using \<open>(hd ws) \<cdot> y\<^sup>@k \<cdot> (last ws) = p \<cdot> x \<cdot> x \<cdot> s\<close>[folded \<open>yb \<cdot> (last ws) = x \<cdot> s\<close>, unfolded lassoc cancel_right, folded \<open>(hd ws) \<cdot> ya = p \<cdot> x\<close>, unfolded rassoc cancel, symmetric].  
+  then obtain m u where "m < k" and "u <p y" and "y\<^sup>@m \<cdot> u = ya" 
+    using pref_mod_power[of ya y k] \<open>yb \<noteq> \<epsilon>\<close>  by blast
+  have "y\<^sup>@m \<cdot> u \<cdot> (u\<inverse>\<^sup>>y) \<cdot> y\<^sup>@(k - m - 1) = y\<^sup>@m \<cdot> y \<cdot> y\<^sup>@(k - m - 1)"
+    using \<open>u <p y\<close>  by (auto simp add: prefix_def) 
+  also have "... = y\<^sup>@(m + 1 + (k-m-1))"
+    using mult_assoc add_exps pow_one' by metis
+  also have "... = y\<^sup>@k"
+    using \<open>m < k\<close>  by auto
+  then obtain l v where "u\<cdot>v = y" and "y\<^sup>@m \<cdot> u \<cdot> v \<cdot> y\<^sup>@l = y\<^sup>@k"
+    using \<open>y \<^sup>@ m \<cdot> u \<cdot> u\<inverse>\<^sup>>y \<cdot> y \<^sup>@ (k - m - 1) = y \<^sup>@ m \<cdot> y \<cdot> y \<^sup>@ (k - m - 1)\<close> calculation by auto
+  have "concat ([hd ws]\<cdot>[y] \<^sup>@ m) = hd ws \<cdot> y \<^sup>@ m"
+    by simp
+
+  have "v \<noteq> \<epsilon>"
+    using \<open>u <p y\<close> \<open>u\<cdot>v = y\<close> by fast
+
+  have "[hd ws] \<cdot> [y] \<^sup>@ m \<le>p ws"
+    using \<open>[hd ws] \<cdot> [y]\<^sup>@k \<cdot> [last ws] = ws\<close>[folded pop_pow[OF less_imp_le[OF \<open>m < k\<close>]]] by fastforce 
+  from disjoint[OF _ this, of "[x]", unfolded \<open>concat ([hd ws] \<cdot> [y] \<^sup>@ m) = hd ws \<cdot> y \<^sup>@ m\<close>]
+  have "u \<noteq> \<epsilon>"
+    using \<open>(hd ws) \<cdot> ya = p \<cdot> x\<close>[folded \<open>y\<^sup>@m \<cdot> u = ya\<close>] s_nemp by force
+  have "u\<cdot>v \<noteq> v\<cdot>u"
+    using comm_not_prim[OF \<open>u \<noteq> \<epsilon>\<close> \<open>v \<noteq> \<epsilon>\<close>]  prim_y \<open>u\<cdot>v = y\<close> by blast
+
+  from that[of m u "u\<inverse>\<^sup>>y" l, OF \<open>hd ws \<cdot> ya = p \<cdot> x\<close>[folded \<open>y \<^sup>@ m \<cdot> u = ya\<close>], folded \<open>yb \<cdot> last ws = x \<cdot> s\<close> \<open>u \<cdot> v = y\<close>,
+      unfolded lq_triv lassoc cancel_right, OF _ _ this] 
+  show thesis
+    using \<open>y \<^sup>@ m \<cdot> u \<cdot> v \<cdot> y \<^sup>@ l = y \<^sup>@ k\<close>[folded \<open>ya \<cdot> yb = y \<^sup>@ k\<close> \<open>y \<^sup>@ m \<cdot> u =  ya\<close>, unfolded rassoc cancel, folded \<open>u \<cdot> v = y\<close>] by blast
+qed
+
+lemma last_ws: "last ws = x"
+proof(rule ccontr)
+  assume "last ws \<noteq> x"
+  hence "last ws = y"
+    using last_ws_lists by blast 
+  obtain l m u v where "(hd ws)\<cdot>y\<^sup>@m\<cdot>u = p\<cdot>x" and "v \<cdot> y\<^sup>@l \<cdot> (last ws) = x \<cdot> s" and
+    "u\<cdot>v = y" and "u \<cdot> v \<noteq> v \<cdot> u"
+    using l_mE by metis
+  note y_le_x[folded \<open>u \<cdot> v = y\<close>,unfolded swap_len[of u]]
+
+  from \<open>v \<cdot> y\<^sup>@l \<cdot> (last ws) = x \<cdot> s\<close>[unfolded \<open>last ws = y\<close>, folded \<open>u \<cdot> v = y\<close>]
+  have "x \<le>p (v \<cdot> u)\<^sup>@Suc l \<cdot> v"
+    unfolding pow_Suc2 rassoc using append_eq_appendI prefix_def shift_pow by metis 
+  moreover have "(v \<cdot> u) \<^sup>@ Suc l \<cdot> v \<le>p (v \<cdot> u) \<cdot> (v \<cdot> u) \<^sup>@ Suc l \<cdot> v"
+    unfolding lassoc pow_comm[symmetric] using rassoc by blast
+  ultimately have "x \<le>p (v \<cdot> u) \<cdot> x"
+    using pref_keeps_root by blast
+
+  thus False
+  proof (cases "m = 0")
+    assume "m \<noteq> 0"
+    then obtain m' where "m = Suc m'"
+      using not0_implies_Suc by blast
+    have "v \<cdot> u \<le>s x"
+      using \<open>(hd ws)\<cdot>y\<^sup>@m\<cdot>u = p\<cdot>x\<close>[folded \<open>u \<cdot> v = y\<close>, unfolded \<open>m = Suc m'\<close> pow_Suc2 rassoc] 
+        suffix_appendD[THEN suf_prod_long[OF _ \<open>\<^bold>|v \<cdot> u\<^bold>| \<le> \<^bold>|x\<^bold>|\<close>], of p "hd ws \<cdot> (u \<cdot> v) \<^sup>@ m' \<cdot> u", unfolded rassoc] by simp   
+    have "(v \<cdot> u) \<cdot> x = x \<cdot> (v \<cdot> u)"
+      using root_suf_comm'[OF  \<open>x \<le>p (v \<cdot> u) \<cdot> x\<close> \<open>(v \<cdot> u) \<le>s x\<close>].
+    thus False
+      using \<open>u \<cdot> v = y\<close> comm_prim conjugI nconjug prim_conjug prim_x prim_y by metis 
+  next
+    assume "m = 0"  
+    thus False
+    proof (cases "hd ws = y")
+      assume "hd ws = y"
+      have "p \<cdot> (x \<cdot> x) \<cdot> s = y\<^sup>@Suc (Suc (Suc (m+l)))"
+        unfolding rassoc \<open>v \<cdot> y\<^sup>@l \<cdot> (last ws) = x \<cdot> s\<close>[unfolded \<open>last ws = y\<close>, symmetric] power_Suc2
+        unfolding lassoc \<open>(hd ws)\<cdot>y\<^sup>@m\<cdot>u = p\<cdot>x\<close>[unfolded \<open>hd ws = y\<close>, symmetric]
+           \<open>u \<cdot> v = y\<close>[symmetric]
+        by comparison
+      have "\<rho> x \<sim> \<rho> y"
+      proof (rule fac_two_conjug_primroot)
+        show "x \<noteq> \<epsilon>" and "y \<noteq> \<epsilon>" using bin_fst_nemp bin_snd_nemp.
+        show "x \<cdot> x \<le>f  y\<^sup>@Suc (Suc (Suc (m+l)))"
+          using facI[of "x\<cdot>x" p s,unfolded \<open>p \<cdot> (x \<cdot> x) \<cdot> s = y\<^sup>@Suc (Suc (Suc (m+l)))\<close>].
+        show "x \<cdot> x \<le>f x\<^sup>@2" 
+          unfolding pow_two by blast
+        show "\<^bold>|x\<^bold>| + \<^bold>|y\<^bold>| - (gcd \<^bold>|x\<^bold>| \<^bold>|y\<^bold>|) \<le> \<^bold>|x \<cdot> x\<^bold>|"
+          using y_le_x unfolding lenmorph by auto
+      qed
+      thus False
+        unfolding x_root y_root using nconjug by blast
+    next
+      assume "hd ws \<noteq> y"
+      hence "hd ws = x"
+        using hd_ws_lists by auto
+
+      have "u \<cdot> v = v \<cdot> u"
+      proof (rule pref_suf_pers_short[reversed])
+        show "x \<le>s x \<cdot> u"
+          using  \<open>(hd ws)\<cdot>y\<^sup>@m\<cdot>u = p\<cdot>x\<close>[unfolded \<open>m = 0\<close> \<open>hd ws = x\<close> pow_zero clean_emp]
+          by (simp add: suf_def)
+        have "v \<cdot> u \<le>p x"
+          using \<open>x \<le>p (v \<cdot> u) \<cdot> x\<close> y_le_x[folded \<open>u \<cdot> v = y\<close>,unfolded swap_len[of u]]
+            pref_prod_long by blast
+        thus "\<^bold>|v \<cdot> u\<^bold>| < \<^bold>|x\<^bold>|"
+          using  nconjug conjugI[OF _ \<open>u \<cdot> v = y\<close>, of x] \<open>\<^bold>|v \<cdot> u\<^bold>| \<le> \<^bold>|x\<^bold>|\<close>
+                 le_neq_implies_less pref_same_len by blast 
+        from \<open>x \<le>p (v \<cdot> u)\<^sup>@Suc l \<cdot> v\<close>  
+        show "x \<le>p ((v \<cdot> u) \<cdot> v) \<cdot> (u \<cdot> v)\<^sup>@l"
+          by comparison
+        show "(u \<cdot> v) \<^sup>@ l \<in> \<langle>{v, u}\<rangle>" 
+          by blast
+      qed
+      thus False 
+        using prim_y \<open>u \<cdot> v \<noteq> v \<cdot> u\<close> by simp
+    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) \<in> lists {rev x, rev y}"
+    using ws_lists  by force
+  show "(rev s) (rev x \<cdot> rev x) (rev p) \<sim>\<^sub>\<I> rev (map rev ws)"
+    using interp rev_fac_interp by fastforce 
+  show "\<^bold>|rev y\<^bold>| \<le> \<^bold>|rev x\<^bold>|"
+    using y_le_x by simp
+  show "\<not> (rev x) \<sim> (rev y)"
+    by (simp add: conjug_rev_conv nconjug) 
+  show "primitive (rev x)" and "primitive (rev y)"
+    using prim_x prim_y by (simp_all add: prim_rev_iff) 
+  show "\<And>p1 p2. p1 \<le>p [rev x, rev x] \<Longrightarrow> p2 \<le>p rev (map rev ws) \<Longrightarrow> rev s \<cdot> concat p1 \<noteq> concat p2"
+  proof
+    fix p1' p2' assume "p1' \<le>p [rev x, rev x]" and "p2' \<le>p rev (map rev ws)" and "rev s \<cdot> concat p1' = concat p2'"
+    obtain p1 p2 where "p1' \<cdot> p1 = [rev x, rev x]" and "p2'\<cdot>p2 = rev (map rev ws)"
+      using \<open>p1' \<le>p [rev x, rev x]\<close> \<open>p2' \<le>p rev (map rev ws)\<close> by (auto simp add: prefix_def)
+    hence "rev s \<cdot> (concat p1' \<cdot> concat p1) \<cdot> rev p = concat p2' \<cdot> concat p2"
+      unfolding concat_morph[symmetric] using \<open>(rev s) (rev x \<cdot> rev x) (rev p) \<sim>\<^sub>\<I> rev (map rev ws)\<close> fac_interpretE(3) by force
+    from this[unfolded lassoc, folded \<open>rev s \<cdot> concat p1' = concat p2'\<close>, unfolded rassoc cancel]
+    have "concat p1 \<cdot> rev p = concat p2".
+    hence "p \<cdot> (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) \<le>p [x,x]" 
+      using arg_cong[OF \<open>p1' \<cdot> p1 = [rev x, rev x]\<close>, of "\<lambda> x. rev (map rev x)", unfolded map_append rev_append]
+      by fastforce
+    have "rev  (map rev p2) \<le>p ws"
+      using arg_cong[OF \<open>p2'\<cdot>p2 = rev (map rev ws)\<close>, of "\<lambda> 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 \<open>rev  (map rev p1) \<le>p [x,x]\<close> \<open>rev  (map rev p2) \<le>p ws\<close>]
+    show False
+      using \<open>p \<cdot> (concat (rev  (map rev p1))) = concat (rev (map rev p2))\<close> by blast
+  qed
+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_interpretE(1) hd_ws interp by auto
+
+lemma s_suf: "s <s x"
+  using fac_interpretE(2) last_ws interp by auto
+
+end
+
+subsection \<open>Locale with additional parameters\<close>
+  \<comment> \<open>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" 
+\<close>
+
+locale square_interp_plus = square_interp +
+  fixes l m u v 
+  assumes fst_x: "x \<cdot> y\<^sup>@m \<cdot> u = p \<cdot> x" and
+    snd_x: "v \<cdot> y\<^sup>@l \<cdot> x = x \<cdot> s" and 
+    uv_y:  "u \<cdot> v = y" and
+    uv_code: "u \<cdot> v \<noteq> v \<cdot> u"
+begin
+
+interpretation  binary_code x y
+  using binary_code.intro comm_prim nconjug nconjug_neq prim_x prim_y by metis
+
+interpretation uv: binary_code u v
+  using uv_code by (simp add: binary_code.intro) 
+
+lemma rev_square_interpret_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_interpretE[OF interp, unfolded hd_ws last_ws]
+  note \<open>s <s x\<close>[unfolded strict_suffix_to_prefix]
+  note \<open>p <p x\<close>[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
+    apply standard
+       apply (simp_all del: rev_append add: rev_pow[symmetric] rev_append[symmetric])
+    by (simp_all only: uv_code, simp_all add: fst_x snd_x uv_y)
+qed
+
+subsubsection \<open>Exactly one of the exponents is zero: impossible.\<close>
+
+text \<open>Uses lemma @{thm pref_suf_pers_short} and exploits the symmetric interpretation.\<close>
+
+lemma fst_exp_zero: assumes "m = 0" and "l \<noteq> 0" shows "False"
+proof (rule notE[OF uv_code])
+  note y_le_x[folded uv_y, unfolded swap_len[of u]]
+  have "x \<le>p (v \<cdot> (u \<cdot> v) \<^sup>@ l) \<cdot> x"
+    unfolding rassoc using snd_x[folded uv_y] by fast 
+  moreover have "v \<cdot> (u \<cdot> v) \<^sup>@ l \<noteq> \<epsilon>"
+    using uv_code by force
+  ultimately obtain exp where "x \<le>p (v \<cdot> (u \<cdot> v) \<^sup>@ l)\<^sup>@exp"
+    using per_prefE by blast
+  hence "exp \<noteq> 0"
+    using pow_zero bin_fst_nemp[folded prefix_Nil] by metis
+
+  show "u \<cdot> v = v \<cdot> u"
+  proof (rule pref_suf_pers_short[reversed])
+    show "x \<le>s x \<cdot> u"
+      using fst_x[unfolded \<open>m = 0\<close>  pow_zero clean_emp] by (simp add: suf_def)
+    have "((v \<cdot> u) \<cdot> v) \<cdot> ((u \<cdot> v)\<^sup>@(l-1)) \<cdot> (v \<cdot> (u \<cdot> v) \<^sup>@ l)\<^sup>@(exp -1) = (v \<cdot> (u \<cdot> v) \<^sup>@ l)\<^sup>@exp"
+      (is "((v \<cdot> u) \<cdot> v) \<cdot> ?suf = (v \<cdot> (u \<cdot> v) \<^sup>@ l)\<^sup>@exp")
+      by (simp add: \<open>exp \<noteq> 0\<close> \<open>l \<noteq> 0\<close> pop_pow_one)
+    show "((u \<cdot> v)\<^sup>@(l-1)) \<cdot> (v \<cdot> (u \<cdot> v) \<^sup>@ l)\<^sup>@(exp -1) \<in> \<langle>{v,u}\<rangle>"
+      by (simp add: gen_in hull_closed power_in)
+    have "v \<cdot> u \<le>p x"
+      using pref_prod_longer[OF \<open>x \<le>p (v \<cdot> (u \<cdot> v) \<^sup>@ l) \<cdot> x\<close>[unfolded rassoc] _ \<open>\<^bold>|v \<cdot> u\<^bold>| \<le> \<^bold>|x\<^bold>|\<close>]
+      unfolding pop_pow_one[OF \<open>l \<noteq> 0\<close>] rassoc by blast
+    thus "\<^bold>|v \<cdot> u\<^bold>| < \<^bold>|x\<^bold>|"
+      using  nconjug conjugI[OF _ uv_y, of x] \<open>\<^bold>|v \<cdot> u\<^bold>| \<le> \<^bold>|x\<^bold>|\<close>
+             le_neq_implies_less pref_same_len by blast 
+    show "x \<le>p ((v \<cdot> u) \<cdot> v) \<cdot> ?suf" 
+      unfolding \<open>((v \<cdot> u) \<cdot> v) \<cdot> ?suf = (v \<cdot> (u \<cdot> v) \<^sup>@ l)\<^sup>@exp\<close> by fact
+  qed
+qed
+
+lemma snd_exp_zero: assumes "m \<noteq> 0" and "l = 0" shows "False"
+using square_interp_plus.fst_exp_zero[OF rev_square_interpret_plus, reversed,
+  rotated, OF assms]. 
+
+subsubsection \<open>Both exponents positive: impossible\<close>
+
+lemma both_exps_pos: assumes "m \<noteq> 0" and "l \<noteq> 0" shows "False"
+proof-
+  note fac_interpretE[OF interp, unfolded hd_ws last_ws]
+  have "\<^bold>|p\<^bold>| \<le> \<^bold>|x\<^bold>|" and "\<^bold>|s\<^bold>| \<le> \<^bold>|x\<^bold>|" 
+    using pref_len[OF sprefD1[OF \<open>p <p x\<close>]] suf_len[OF ssufD1[OF \<open>s <s x\<close>]].
+
+  obtain m' l' where "Suc m' = m" and "Suc l' = l"
+    using assms predE by metis
+  have "x \<le>p (v \<cdot> (u \<cdot> v)\<^sup>@Suc l') \<cdot> x" 
+    (is "x \<le>p ?pref \<cdot> x")
+    using snd_x[folded uv_y \<open>Suc l' = l\<close>] by force
+  moreover have "x \<le>s x \<cdot> ((u \<cdot> v)\<^sup>@Suc m' \<cdot> u)"
+    (is "x \<le>s x \<cdot> ?suf") 
+    using fst_x[folded uv_y \<open>Suc m' = m\<close>] by force 
+
+  ultimately interpret pref_suf_pers x u v l' m'
+    by (unfold_locales)
+
+  have "?pref \<le>p x"
+    using snd_x[folded uv_y \<open>Suc l' = l\<close> rassoc, symmetric]  eqd[reversed,  OF _ \<open>\<^bold>|s\<^bold>| \<le> \<^bold>|x\<^bold>|\<close>]  by blast
+  have "?suf \<le>s x"  
+    using fst_x[folded uv_y \<open>Suc m' = m\<close>, symmetric]  eqd[OF _ \<open>\<^bold>|p\<^bold>| \<le> \<^bold>|x\<^bold>|\<close>]  by blast
+
+  have in_particular: "commutes {u,v,x} \<Longrightarrow> u \<cdot> v = v \<cdot> u"
+    using commutes_def insertCI by metis
+  have in_particular': "x \<cdot> v \<cdot> u = (v \<cdot> u) \<cdot> x \<Longrightarrow> x \<sim> y"
+    using comm_prim conjugI' prim_conjug prim_x prim_y uv_y by metis
+
+\<comment>  \<open>Case analysis based on (slightly modified) lemmas for covered x square.\<close>
+
+  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 \<open>?pref \<le>p x\<close> \<open>?suf \<le>s x\<close>,THEN in_particular']
+
+  consider
+    (no_overlap)     "\<^bold>|?pref\<^bold>| + \<^bold>|?suf\<^bold>| \<le> \<^bold>|x\<^bold>|" |
+    (short_overlap)  "\<^bold>|x\<^bold>| <  \<^bold>|?pref\<^bold>| + \<^bold>|?suf\<^bold>| \<and>  \<^bold>|?pref\<^bold>| + \<^bold>|?suf\<^bold>| \<le> \<^bold>|x\<^bold>| + \<^bold>|u\<^bold>|" |
+    (medium_overlap) "\<^bold>|x\<^bold>| + \<^bold>|u\<^bold>| < \<^bold>|?pref\<^bold>| + \<^bold>|?suf\<^bold>| \<and>  \<^bold>|?pref\<^bold>| + \<^bold>|?suf\<^bold>| < \<^bold>|x\<^bold>| + \<^bold>|u \<cdot> v\<^bold>|" | 
+    (large_overlap)  "\<^bold>|x\<^bold>| + \<^bold>|v \<cdot> u\<^bold>| \<le>  \<^bold>|?pref\<^bold>| + \<^bold>|?suf\<^bold>|"
+    unfolding swap_len[of v] by linarith
+  thus False 
+  proof (cases)
+    case no_overlap
+    then show False         
+      using no_overlap_comm uv_code by blast
+  next
+    case short_overlap
+    then show False         
+      using short_overlap_comm uv_code by blast
+  next
+    case medium_overlap
+    then show False         
+      using medium_overlap_comm uv_code by blast
+  next
+    case large_overlap
+    show False
+      thm large_overlap_conjug nconjug 
+    proof (rule notE[OF nconjug], rule large_overlap_conjug[OF _ _ large_overlap])
+      have "(u \<cdot> v) \<^sup>@ l' \<le>p (u \<cdot> v) \<^sup>@ Suc l'"
+        using pref_pow_ext by blast  
+      thus "v \<cdot> (u \<cdot> v) \<^sup>@ Suc l' \<le>p (v \<cdot> u) \<cdot> v \<cdot> (u \<cdot> v) \<^sup>@ Suc l'"
+        unfolding pow_Suc rassoc pref_cancel_conv.
+      show "(u \<cdot> v) \<^sup>@ Suc m' \<cdot> u \<le>s ((u \<cdot> v) \<^sup>@ Suc m' \<cdot> u) \<cdot> v \<cdot> u"
+        by comparison 
+    qed
+  qed
+qed  
+
+thm suf_cancel_conv
+
+end 
+
+subsection \<open>Back to the main locale\<close>
+
+context square_interp
+
+begin
+
+definition u where "u = x\<inverse>\<^sup>>(p \<cdot> x)"
+definition v where "v = (x \<cdot> s)\<^sup><\<inverse>x"
+
+lemma cover_xyx: "ws = [x,y,x]" and uv_code: "u \<cdot> v \<noteq> v \<cdot> u" and uv_y: "u \<cdot> v = y" and
+  px_xu:  "p \<cdot> x = x \<cdot> u" and  vx_xs:  "v \<cdot> x = x \<cdot> s"
+proof-
+  note prim_nemp[OF prim_y] 
+  obtain k where ws: "[x] \<cdot> [y]\<^sup>@k \<cdot> [x] = ws"
+    using kE[unfolded hd_ws last_ws].
+  obtain m u' v' l where  "x \<cdot> y \<^sup>@ m \<cdot> u' = p \<cdot> x" and "v' \<cdot> y \<^sup>@ l \<cdot> x = x \<cdot> s" and "u' \<cdot> v' = y" and "u' \<cdot> v' \<noteq> v' \<cdot> u'"
+    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"
+    using both_exps_pos snd_exp_zero fst_exp_zero by blast+
+  have "u' = u"
+    unfolding u_def
+    using conjug_lq[OF fst_x[unfolded \<open>m = 0\<close> pow_zero clean_emp, symmetric]].
+  have "v' = v"
+    unfolding v_def
+    using conjug_lq[reversed, OF snd_x[unfolded \<open>l = 0\<close> pow_zero clean_emp, symmetric]].
+  have "x \<cdot> y \<^sup>@ m \<cdot> (u' \<cdot> v') \<cdot> y\<^sup>@l \<cdot> x = concat ws"
+    unfolding interpret_concat[symmetric] using fst_x snd_x by force
+  from this[folded ws, unfolded \<open>u' \<cdot> v' = y\<close> \<open>m = 0\<close> \<open>l = 0\<close> pow_zero clean_emp]
+  have "k = 1"
+    unfolding eq_pow_exp[OF \<open>y \<noteq> \<epsilon>\<close>, of k 1, symmetric] pow_one' concat_morph concat_pow 
+    by simp
+  from ws[unfolded this pow_one']
+  show "ws = [x,y,x]" by simp
+  show "u \<cdot> v  = y" and "u \<cdot> v \<noteq> v \<cdot> u"
+    unfolding \<open>u' = u\<close>[symmetric] \<open>v' = v\<close>[symmetric] by fact+
+  show  "p \<cdot> x = x \<cdot> u"
+    using \<open>x \<cdot> y \<^sup>@ m \<cdot> u' = p \<cdot> x\<close>[unfolded \<open>m = 0\<close> \<open>u' = u\<close> pow_zero clean_emp, symmetric].
+  show  " v \<cdot> x = x \<cdot> s"
+    using \<open>v' \<cdot> y \<^sup>@ l \<cdot> x = x \<cdot> s\<close>[unfolded \<open>l = 0\<close> \<open>v' = v\<close> pow_zero clean_emp].
+qed
+
+lemma u_nemp: "u \<noteq> \<epsilon>" and v_nemp: "v \<noteq> \<epsilon>"
+  using uv_code by force+
+
+lemma cover: "x \<cdot> y \<cdot> x = p \<cdot> x \<cdot> x \<cdot> s"
+  using interpret_concat cover_xyx by auto 
+
+lemma conjug_facs: "\<rho> u \<sim> \<rho> v"
+proof-
+  note sufI[OF px_xu]
+  have "u \<noteq> \<epsilon>"
+    using p_nemp px_xu by force 
+  obtain expu where "x \<le>f u\<^sup>@expu"
+    using per_prefE[reversed, OF \<open> x \<le>s x \<cdot> u\<close> \<open>u \<noteq> \<epsilon>\<close> pref_fac[reversed,elim_format]].
+
+  note prefI[OF vx_xs[symmetric]]
+  have "v \<noteq> \<epsilon>"
+    using s_nemp vx_xs by force
+  obtain expv where "x \<le>f v\<^sup>@expv"
+    using per_prefE[OF \<open>x \<le>p v \<cdot> x\<close> \<open>v \<noteq> \<epsilon>\<close> pref_fac[elim_format]].
+
+  show "\<rho> u \<sim> \<rho> v"
+  proof(rule fac_two_conjug_primroot[OF \<open>x \<le>f u\<^sup>@expu\<close> \<open>x \<le>f v\<^sup>@expv\<close> \<open>u \<noteq> \<epsilon>\<close> \<open>v \<noteq> \<epsilon>\<close>])
+    show "\<^bold>|u\<^bold>| + \<^bold>|v\<^bold>| - (gcd \<^bold>|u\<^bold>| \<^bold>|v\<^bold>|) \<le> \<^bold>|x\<^bold>|"
+      using y_le_x[folded uv_y, unfolded lenmorph] by fastforce
+  qed 
+qed
+
+term square_interp.v
+
+\<comment> \<open>We have a detailed information about all words\<close>
+lemma bin_sq_interpE: obtains r t m k l
+  where "(t \<cdot> r)\<^sup>@Suc k = u" and  "(r \<cdot> t)\<^sup>@Suc l = v" and
+    "(r \<cdot> t)\<^sup>@Suc m \<cdot> r = x" and "(t \<cdot> r)\<^sup>@Suc k \<cdot> (r \<cdot> t)\<^sup>@Suc l = y"
+    and "(r \<cdot> t)\<^sup>@Suc k = p" and  "(t \<cdot> r)\<^sup>@Suc l = s"  and "r \<cdot> t \<noteq> t \<cdot> r"
+proof-
+
+  obtain r t k m where "(r \<cdot> t)\<^sup>@Suc k = p" and "(t \<cdot> r)\<^sup>@Suc k = u" and "(r \<cdot> t)\<^sup>@m \<cdot> r = x" and
+    "t \<noteq> \<epsilon>" and "primitive (r \<cdot> t)" 
+    using conjug_eq_primrootE[OF px_xu p_nemp]. 
+  have "t \<cdot> r = \<rho> u"
+    using  prim_conjug[OF \<open>primitive (r \<cdot> t)\<close>, THEN pow_prim_primroot[OF u_nemp], OF conjugI' \<open>(t \<cdot> r)\<^sup>@Suc k = u\<close>[symmetric]]..
+
+  have "m \<noteq> 0"
+  proof
+    assume "m = 0"
+    hence "x = r" using \<open>(r \<cdot> t)\<^sup>@m \<cdot> r = x\<close> by simp
+    from y_le_x[folded uv_y, folded \<open>(t \<cdot> r)\<^sup>@Suc k = u\<close>, unfolded lenmorph pow_len this]
+    show False
+      using nemp_len[OF \<open>t \<noteq> \<epsilon>\<close>] by force
+  qed
+
+  then obtain pred_m where "m = Suc pred_m"
+    using not0_implies_Suc by auto
+
+  from \<open>(r \<cdot> t)\<^sup>@m \<cdot> r = x\<close>[unfolded this]
+  have "r \<cdot> t \<le>p x"
+    by auto
+
+  have "r \<cdot> t = \<rho> v"
+  proof (rule ruler_eq_len[of "\<rho> v" "x" "r \<cdot> t", symmetric])
+    have "\<^bold>|\<rho> v\<^bold>| \<le> \<^bold>|x\<^bold>|"
+      unfolding conjug_len[OF conjug_facs, symmetric] \<open>t \<cdot> r = \<rho> u\<close>[symmetric]
+      unfolding \<open>(r \<cdot> t)\<^sup>@m \<cdot> r = x\<close>[symmetric]
+        lenmorph pow_len
+      using \<open>m = Suc pred_m\<close> by auto         
+    from ruler_le[OF _ _ this, of "v \<cdot> x"]
+    show "\<rho> v \<le>p x"
+      using vx_xs prefI prefix_prefix primroot_pref v_nemp by metis 
+    show "r \<cdot> t \<le>p x" by fact
+    show "\<^bold>|\<rho> v\<^bold>| = \<^bold>|r \<cdot> t\<^bold>|"
+      unfolding conjug_len[OF conjug_facs, symmetric, folded \<open>t \<cdot> r = \<rho> u\<close>] lenmorph by simp
+  qed
+
+  then obtain l where "(r \<cdot> t)\<^sup>@Suc l = v"
+    using primroot_expE v_nemp by metis
+
+  have "(t \<cdot> r)\<^sup>@Suc l = s" 
+    using vx_xs[folded \<open>(r \<cdot> t)\<^sup>@m \<cdot> r = x\<close> \<open>(r \<cdot> t)\<^sup>@Suc l = v\<close>, unfolded lassoc pows_comm[of _ _ m],
+        unfolded rassoc cancel, unfolded shift_pow cancel]. 
+
+  have "r \<cdot> t \<noteq> t \<cdot> r"
+    using \<open>(t \<cdot> r) \<^sup>@ Suc k = u\<close> \<open>(r \<cdot> t) \<^sup>@ Suc l = v\<close> pows_comm[of "t \<cdot> r" "Suc k" "Suc l"] uv_code by force
+
+  show thesis
+    using that[OF \<open>(t \<cdot>r)\<^sup>@Suc k = u\<close> \<open>(r \<cdot> t) \<^sup>@ Suc l = v\<close> \<open>(r \<cdot> t)\<^sup>@m \<cdot> r = x\<close>[unfolded \<open>m = Suc pred_m\<close>]
+        uv_y[folded \<open>(t \<cdot>r)\<^sup>@Suc k = u\<close> \<open>(r \<cdot> t) \<^sup>@ Suc l = v\<close>] \<open>(r \<cdot> t) \<^sup>@ Suc k = p\<close> \<open>(t \<cdot> r) \<^sup>@ Suc l = s\<close>  \<open>r \<cdot> t \<noteq> t \<cdot> r\<close>].
+qed
+
+end
+
+subsection \<open>Locale: Extendable interpretation\<close>
+text \<open>Further specification follows from the assumption that the interpretation is extendable,
+ that is, the covered @{term "x\<cdot>x"} is a factor of a word composed of @{term "{x,y}"}. Namely, @{term u} and @{term v} are then conjugate by @{term x}.\<close>
+
+locale square_interp_ext = square_interp +
+  assumes p_extend: "\<exists> pe. pe \<in> \<langle>{x,y}\<rangle> \<and> p \<le>s pe" and
+    s_extend: "\<exists> se. se \<in> \<langle>{x,y}\<rangle> \<and> s \<le>p se"
+
+begin
+
+lemma s_pref_y: "s \<le>p y"
+proof-
+  obtain sy ry eu ev ex
+    where "(ry \<cdot> sy)\<^sup>@Suc eu = u" and  "(sy \<cdot> ry)\<^sup>@Suc ev = v" and
+      "(sy \<cdot> ry)\<^sup>@Suc eu = p" and  "(ry \<cdot> sy)\<^sup>@Suc ev = s" and
+      "(sy \<cdot> ry)\<^sup>@Suc ex \<cdot> sy = x" and "sy \<cdot> ry \<noteq> ry \<cdot> sy"
+    using bin_sq_interpE.
+
+  obtain se where "se \<in> \<langle>{x,y}\<rangle>" and  "s \<le>p se"
+    using s_extend by blast
+  hence "se \<noteq> \<epsilon>" using s_nemp by force
+
+  from \<open>(sy \<cdot> ry)\<^sup>@Suc ex \<cdot> sy = x\<close>
+  have "sy \<cdot> ry \<le>p x"
+    unfolding pow_Suc rassoc by force
+
+  have "x \<le>p se \<or> y \<le>p se"
+    using  \<open>se \<noteq> \<epsilon>\<close> hull.cases[OF \<open>se \<in> \<langle>{x,y}\<rangle>\<close>, of "x \<le>p se \<or> y \<le>p se"]
+      prefix_append triv_pref two_elem_cases by blast 
+  moreover have "\<not> x \<le>p se"
+  proof
+    assume "x \<le>p se"
+    from ruler_eq_len[of "sy \<cdot> ry" se "ry \<cdot> sy", OF pref_trans[OF \<open>sy \<cdot> ry \<le>p x\<close> this]]
+    show False  
+      using \<open>s \<le>p se\<close>[folded \<open>(ry \<cdot> sy)\<^sup>@Suc ev = s\<close>[unfolded pow_Suc]] \<open>sy \<cdot> ry \<noteq> ry \<cdot> sy\<close> by (force simp add: prefix_def)
+  qed
+  ultimately have y_pref_se: "y \<le>p se" by blast
+
+  from ruler_le[OF \<open>s \<le>p se\<close> this] 
+  show "s \<le>p y"
+    using lenarg[OF vx_xs] unfolding uv_y[symmetric] lenmorph by linarith
+qed
+
+lemma rev_square_interpret_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 "\<exists>pe. pe \<in> \<langle>{rev x, rev y}\<rangle> \<and> rev s \<le>s pe"
+      using pref_rev_suf_iff s_pref_y by blast
+    obtain pe where "pe \<in> \<langle>{x, y}\<rangle>" and  "p \<le>s pe"
+      using p_extend by blast
+    hence "rev pe \<in> \<langle>{rev x, rev y}\<rangle>"
+      by (simp add: rev_hull rev_in_conv) 
+    thus "\<exists>se. se \<in> \<langle>{rev x, rev y}\<rangle> \<and> rev p \<le>p se"
+      using \<open>p \<le>s pe\<close>[unfolded suf_rev_pref_iff prefix_def] rev_rev_ident by blast
+  qed
+qed
+
+lemma p_suf_y: "p \<le>s y"
+proof-
+  interpret i: square_interp_ext "(rev x)" "(rev y)" "(rev s)" "(rev p)" "(rev (map rev ws))"
+    using rev_square_interpret_ext.
+
+  from i.s_pref_y[reversed]
+  show "p \<le>s y".
+qed   
+
+theorem bin_sq_interpret_extE: obtains r t k m where  "(r \<cdot> t)\<^sup>@Suc m \<cdot> r = x" and  "(t \<cdot> r)\<^sup>@Suc k \<cdot> (r \<cdot> t)\<^sup>@ Suc k = y"
+  "(r \<cdot> t)\<^sup>@Suc k = p" and "(t \<cdot> r)\<^sup>@ Suc k = s" and "r \<cdot> t \<noteq> t \<cdot> r" and "u = s" and "v = p" and "\<^bold>|p\<^bold>| = \<^bold>|s\<^bold>|"
+proof-  
+  obtain r t k k' m
+    where u: "(t \<cdot> r)\<^sup>@Suc k = u" and v:  "(r \<cdot> t)\<^sup>@Suc k' = v" and
+      p: "(r \<cdot> t)\<^sup>@Suc k = p" and s: "(t \<cdot> r)\<^sup>@Suc k' = s" and
+      x: "(r \<cdot> t)\<^sup>@Suc m \<cdot> r = x" and code: "r \<cdot> t \<noteq> t \<cdot> r"
+    using bin_sq_interpE. 
+  have "\<^bold>|u \<cdot> v\<^bold>| = \<^bold>|s \<cdot> p\<^bold>|"
+    using lenarg[OF px_xu, unfolded lenmorph] lenarg[OF vx_xs, unfolded lenmorph] by simp
+  hence "u \<cdot> v = s \<cdot> p"
+    unfolding uv_y using s_pref_y p_suf_y by (auto simp add: prefix_def suf_def)
+  note eq = \<open>u \<cdot> v = s \<cdot> p\<close>[unfolded  \<open>(t \<cdot> r)\<^sup>@Suc k = u\<close>[symmetric] \<open>(r \<cdot> t)\<^sup>@Suc k' = v\<close>[symmetric],
+      unfolded \<open>(t \<cdot> r)\<^sup>@Suc k' = s\<close>[symmetric] \<open>(r \<cdot> t)\<^sup>@Suc k = p\<close>[symmetric]]
+  from pows_eq_comm[OF this, THEN comm_add_exps, of "Suc k" "Suc k'"]
+  have "k = k'"
+    unfolding \<open>(t \<cdot> r) \<^sup>@ Suc k = u\<close> \<open>(r \<cdot> t) \<^sup>@ Suc k' = v\<close> using uv_code by blast  
+  have "\<^bold>|p\<^bold>| = \<^bold>|s\<^bold>|"
+    using lenarg[OF p] lenarg[OF s] unfolding \<open>k = k'\<close> pow_len lenmorph add.commute[of "\<^bold>|r\<^bold>|"] by fastforce
+  thus thesis
+    using that[OF x uv_y[folded u v \<open>k = k'\<close>] p s[folded \<open>k = k'\<close>] code] u v p s unfolding \<open>k = k'\<close> by argo   
+qed
+
+lemma ps_len: "\<^bold>|p\<^bold>| = \<^bold>|s\<^bold>|" and p_eq_v: "p = v" and s_eq_u: "s = u"
+  using bin_sq_interpret_extE by blast+
+
+lemma v_x_x_u: "v \<cdot> x = x \<cdot> u"
+  using vx_xs unfolding s_eq_u.
+
+lemma sp_y: "s \<cdot> p = y"
+  using p_eq_v s_eq_u uv_y by auto 
+
+lemma p_x_x_s: "p \<cdot> x = x \<cdot> s"
+  by (simp add: px_xu s_eq_u)
+
+lemma xxy_root: "x \<cdot> x \<cdot> y = (x \<cdot> p) \<cdot> (x \<cdot> p)"
+  using p_x_x_s sp_y by force
+
+theorem sq_ext_interp: "ws = [x, y, x]" "s \<cdot> p = y" "p \<cdot> x = x \<cdot> s"
+  using cover_xyx sp_y p_x_x_s.
+
+end
+
+theorem bin_sq_interpE:  
+  assumes "primitive x" and "primitive y" and "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|" and "ws \<in> lists {x, y}" and "\<not> x \<sim> y" and 
+    "\<And> p1 p2. p1 \<le>p [x, x] \<Longrightarrow> p2 \<le>p ws \<Longrightarrow> p \<cdot> concat p1 \<noteq> concat p2" and "p x \<cdot> x s \<sim>\<^sub>\<I> ws"
+  obtains r t m k l where "(r \<cdot> t)\<^sup>@Suc m \<cdot> r = x" and "(t \<cdot> r)\<^sup>@Suc k \<cdot> (r \<cdot> t)\<^sup>@ Suc l = y"
+    "(r \<cdot> t)\<^sup>@Suc k = p" and "(t \<cdot> r)\<^sup>@ Suc l = s" and "r \<cdot> t \<noteq> t \<cdot> r"
+  using  square_interp.bin_sq_interpE[OF square_interp.intro, OF assms, of thesis].
+
+theorem bin_sq_interpret_extE:  
+  assumes "primitive x" and "primitive y" and "\<^bold>|y\<^bold>| \<le> \<^bold>|x\<^bold>|" and "ws \<in> lists {x, y}"  and "\<not> x \<sim> y" and
+    "\<And> p1 p2. p1 \<le>p [x, x] \<Longrightarrow> p2 \<le>p ws \<Longrightarrow> p \<cdot> concat p1 \<noteq> concat p2"  and "p x \<cdot> x s \<sim>\<^sub>\<I> ws" and
+    p_extend: "\<exists> pe. pe \<in> \<langle>{x,y}\<rangle> \<and> p \<le>s pe" and
+    s_extend: "\<exists> se. se \<in> \<langle>{x,y}\<rangle> \<and> s \<le>p se"
+  obtains r t m k where "(r \<cdot> t)\<^sup>@Suc m \<cdot> r = x" and "(t \<cdot> r)\<^sup>@Suc k \<cdot> (r \<cdot> t)\<^sup>@ Suc k = y"
+    "(r \<cdot> t)\<^sup>@Suc k = p" and "(t \<cdot> r)\<^sup>@ Suc k = s" and "r \<cdot> t \<noteq> t \<cdot> r"
+  using  square_interp_ext.bin_sq_interpret_extE[OF square_interp_ext.intro, OF square_interp.intro square_interp_ext_axioms.intro, OF assms, of thesis].
+
+end
\ No newline at end of file
diff --git a/thys/Binary_Code_Imprimitive/ROOT b/thys/Binary_Code_Imprimitive/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Binary_Code_Imprimitive/ROOT
@@ -0,0 +1,12 @@
+chapter AFP
+
+session Binary_Code_Imprimitive (AFP) = Combinatorics_Words +
+  options [timeout = 600]
+  sessions
+    Combinatorics_Words_Graph_Lemma
+  theories
+    Binary_Square_Interpretation
+    Binary_Code_Imprimitive
+  document_files
+    root.tex
+    root.bib
diff --git a/thys/Binary_Code_Imprimitive/document/root.bib b/thys/Binary_Code_Imprimitive/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Binary_Code_Imprimitive/document/root.bib
@@ -0,0 +1,37 @@
+@PhdThesis{spehner,
+	title = "{Quelques probl\`{e}mes d'extension, de conjugaison et de présentation des sous-mono\"{i}des d'un mono\"{i}de libre.}",
+	author = "Spehner, J.-C.",
+	school = "Universit\'{e} Paris VII, Paris",
+	year = "1976",
+}
+
+@Article{lerest,
+  author    = {Barbin-Le Rest, Evelyne and Le Rest, Michel},
+  title     = {Sur la Combinatoire des Codes \`{a} Deux Mots.},
+  journal   = {Theor. Comput. Sci.},
+  year      = {1985},
+  volume    = {41},
+  pages     = {61--80},
+  added-at  = {2011-09-07T00:00:00.000+0200},
+  biburl    = {http://www.bibsonomy.org/bibtex/253c7e2761f4ea85902779bcf0c728123/dblp},
+  ee        = {http://dx.doi.org/10.1016/0304-3975(85)90060-X},
+  interhash = {f84dac1c875cca36656e0d06f0f35127},
+  intrahash = {53c7e2761f4ea85902779bcf0c728123},
+  keywords  = {dblp},
+  timestamp = {2011-09-07T00:00:00.000+0200},
+}
+
+@article{Manuch,
+	author    = {J{\'{a}}n Ma{\v n}uch},
+	title     = {Defect Effect of Bi-infinite Words in the Two-element Case},
+	journal   = {Discret. Math. Theor. Comput. Sci.},
+	volume    = {4},
+	number    = {2},
+	pages     = {273--290},
+	year      = {2001},
+	url       = {http://dmtcs.episciences.org/279},
+	timestamp = {Fri, 13 Mar 2020 14:37:54 +0100},
+	biburl    = {https://dblp.org/rec/journals/dmtcs/Manuch01.bib},
+	bibsource = {dblp computer science bibliography, https://dblp.org},
+	doi = {10.46298/dmtcs.279}
+}
\ No newline at end of file
diff --git a/thys/Binary_Code_Imprimitive/document/root.tex b/thys/Binary_Code_Imprimitive/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Binary_Code_Imprimitive/document/root.tex
@@ -0,0 +1,76 @@
+\documentclass[11pt,a4paper]{report}
+\usepackage[utf8]{inputenc}
+\usepackage{isabelle,isabellesym}
+\usepackage{fontspec}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap]{stmaryrd}
+  %for \<Sqinter>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+
+\begin{document}
+
+\title{Combinatorics on Words formalized \\ Binary codes that do not preserve primitivity}
+\author{Štěpán Holub \\ Martin Raška }
+  
+
+ \date{ \today
+ \vfill
+  Funded by the Czech Science Foundation grant GA\v CR 20-20621S.}
+  
+\maketitle
+
+%\begin{abstract}
+%Lecture notes
+%\end{abstract}
+
+\tableofcontents
+\vspace{\baselineskip}
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\cleardoublepage
+\phantomsection
+\addcontentsline{toc}{chapter}{References}
+\renewcommand{\bibname}{References}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,734 +1,735 @@
 ABY3_Protocols
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AOT
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Ackermanns_not_PR
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Balog_Szemeredi_Gowers
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
+Binary_Code_Imprimitive
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Birkhoff_Finite_Distributive_Lattices
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Boolos_Curious_Inference
 Boolos_Curious_Inference_Automated
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CHERI-C_Memory_Model
 CISC-Kernel
 CRDT
 CRYSTALS-Kyber
 CSP_RefTK
 CVP_Hardness
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 Clique_and_Monotone_Circuits
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinable_Wands
 Combinatorial_Enumeration_Algorithms
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Commuting_Hermitian
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 Cook_Levin
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Cubic_Quartic_Equations
 DFS_Framework
 DOM_Components
 DPRM_Theorem
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Digit_Expansions
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Edwards_Elliptic_Curves_Group
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Eval_FO
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 FOL_Seq_Calc3
 FO_Theory_Rewriting
 FSM_Tests
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finite_Fields
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Fishers_Inequality
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 Frequency_Moments
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 Given_Clause_Loops
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Hales_Jewett
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 HoareForDivergence
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 Hyperdual
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IMP_Compiler_Reuse
 IP_Addresses
 Imperative_Insertion_Sort
 Implicational_Logic
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Involutions2Squares
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 IsaNet
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Khovanskii_Theorem
 Kleene_Algebra
 Kneser_Cauchy_Davenport
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LP_Duality
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Maximum_Segment_Sum
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Multiset_Ordering_NPC
 Multitape_To_Singletape_TM
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nano_JSON
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Number_Theoretic_Transform
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PAL
 PAPP_Impossibility
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Package_logic
 Padic_Field
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Pluennecke_Ruzsa_Inequality
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Prefix_Free_Code_Combinators
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Probability_Inequality_Completeness
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Logic_Class
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quantifier_Elimination_Hybrid
 Quasi_Borel_Spaces
 Quaternions
 Query_Optimization
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Real_Time_Deque
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rensets
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewrite_Properties_Reduction
 Rewriting_Z
 Ribbon_Proofs
 Risk_Free_Lending
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SCC_Bloemen_Sequential
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Safe_Range_RC
 Saturation_Framework
 Saturation_Framework_Extensions
 Sauer_Shelah_Lemma
 Schutz_Spacetime
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 Separation_Logic_Unbounded
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Solidity
 Sophomores_Dream
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Stalnaker_Logic
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 StrictOmegaCategories
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Suppes_Theorem
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Synthetic_Completeness
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Turans_Graph_Theorem
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Undirected_Graph_Theory
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 VYDRA_MDL
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Arithmetic_Geometric_Mean
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL