Theory Two_Generated_Word_Monoids_Intersection

(*  Title:      Two Generated Word Monoids_Intersection
    File:       Two_Generated_Word_Monoids_Intersection.Two_Generated_Word_Monoids_Intersection
    Author:     Štěpán Holub, Charles University
    Author:     Štěpán Starosta, CTU in Prague

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

theory Two_Generated_Word_Monoids_Intersection
  imports Combinatorics_Words.Equations_Basic Combinatorics_Words.Binary_Code_Morphisms Combinatorics_Words_Graph_Lemma.Glued_Codes
begin

text
  ‹The characterization of intersection of binary languages formalized here is due to @{cite Ka_intersections}.›

chapter "Binary Intersection Formalized"

locale  binary_codes_coincidence_two_generators = binary_codes_coincidence +
  assumes  two_coins: "∃ r s r' s'. g r =m h s ∧ g r' =m h s' ∧ (r,s) ≠ (r',s')"

begin

lemma  criticalE':
  obtains p q r1 s1 r2 s2 where
    "g p ⋅ αg = h q ⋅ αh" and
    "g (p ⋅ r1) = h (q ⋅ s1)" and
    "g (p ⋅ r2) = h (q ⋅ s2)" and
    "r1 ≠ ε" and "r2 ≠ ε" and
    "hd r1 ≠ hd r2"
proof-
  obtain r s r' s' where "g r =m h s" and  "g r' =m h s'" and "(r,s) ≠ (r',s')"
    using two_coins by blast
  note eqs =  min_coinD[OF ‹g r =m h s›] min_coinD[OF ‹g r' =m h s'›]
  have "s ⋅ s' ≠ s' ⋅ s"
  proof
    assume "s ⋅ s' = s' ⋅ s"
    from arg_cong[OF this, of h]
    have "g (r ⋅ r') = g (r' ⋅ r)"
      unfolding g.morph h.morph using ‹g r = h s› ‹g r' = h s'› by argo
    from g.code_morph_code[OF this]
    have "r ⋅ r' = r' ⋅ r".
    from ruler_eq[OF ‹r ⋅ r' = r' ⋅ r›] ruler_eq[OF ‹s ⋅ s' = s' ⋅ s›]
    have "s ≤p s' ⟹ r ≤p r'" and "s' ≤p s ⟹ r' ≤p r"
      using ‹g r = h s› ‹g r' = h s'› g.pref_morph_pref_eq h.pref_mono by metis+
    hence "(r, s) = (r', s')"
      using ‹s ≤p s' ∨ s' ≤p s› ‹g r =m h s› ‹g r' =m h s'› npI
      unfolding min_coin_def by metis
    thus False
      using ‹(r, s) ≠ (r', s')› by blast
  qed
  hence "h (s ⋅ s') ⋅ αh ≠ h (s' ⋅ s) ⋅ αh"
    unfolding cancel_right using h.code_morph_code by blast
  hence "¬ h (s ⋅ s') ⋅ αh ⨝ h (s' ⋅ s) ⋅ αh"
    unfolding h.morph using comm_comp_eq_conv comp_prefs_comp by metis
  hence hm: "h (s ⋅ s') ⋅ αh ⋅ α ∧p h(s' ⋅ s) ⋅ αh ⋅ α = h (s ⋅ s' ∧p s' ⋅ s) ⋅ αh"
    using lcp_ext_right_conv[of "h (s ⋅ s') ⋅ αh" "h (s' ⋅ s) ⋅ αh" "α" "α"]
      h.bin_code_lcp[symmetric] unfolding h.bin_code_lcp[symmetric] rassoc by blast

  let ?p = "r ⋅ r' ∧p r' ⋅ r"
  let ?q = "s ⋅ s' ∧p s' ⋅ s"
  let ?r1 = "?p¯>(r ⋅ r')"
  let ?r2 = "?p¯>(r' ⋅ r)"
  let ?s1 = "?q¯>(s ⋅ s')"
  let ?s2 = "?q¯>(s' ⋅ s)"

  from eqs
  have "g (r ⋅ r') ⋅ αg = h (s ⋅ s') ⋅ αh ⋅ α" and
    "g (r' ⋅ r) ⋅ αg = h (s' ⋅ s) ⋅ αh ⋅ α"
    unfolding g.morph h.morph  lcp_diff cancel_right by auto

  hence "g ?p ⋅ αg = h ?q ⋅ αh"
    unfolding g.bin_code_lcp[symmetric] hm[symmetric] by argo

  have "g (?p ⋅ ?r1) = h (?q ⋅ ?s1)"
    unfolding lq_pref[OF lcp_pref] g.morph h.morph ‹g r = h s› ‹g r' = h s'›..
  have "g (?p ⋅ ?r2) = h (?q ⋅ ?s2)"
    unfolding lq_pref[OF lcp_pref'] g.morph h.morph ‹g r = h s› ‹g r' = h s'›..

  have "r ⋅ r' ≠ r' ⋅ r"
  proof
    assume "r ⋅ r' = r' ⋅ r"
    from arg_cong[OF this, of g]
    have "h (s ⋅ s') = h (s' ⋅ s)"
      unfolding g.morph h.morph using ‹g r = h s› ‹g r' = h s'› by argo
    from h.code_morph_code[OF this] ‹s ⋅ s' ≠ s' ⋅ s›
    show False by blast
  qed
  from ‹r ⋅ r' ≠ r' ⋅ r›
  have "¬ r ⋅ r' ⨝ r' ⋅ r"
    using comm_comp_eq by blast

  from that[OF ‹g ?p ⋅ αg = h ?q ⋅ αh› ‹g (?p ⋅ ?r1) = h (?q ⋅ ?s1)›
      ‹g (?p ⋅ ?r2) = h (?q ⋅ ?s2)›] lcp_mismatch_lq[OF ‹¬ r ⋅ r' ⨝ r' ⋅ r›]
  show thesis
    by blast
qed

lemma alphas_suf: "αh ≤s αg"
proof-
  from criticalE'
  obtain p q where "g p ⋅ αg = h q ⋅ αh" by meson
  from eqd[reversed, OF this[symmetric] alphas_len]
  show "αh ≤s αg" by blast
qed

lemma c_def: "𝖼 ⋅ αh = αg"
  unfolding critical_overflow_def using rq_suf[OF alphas_suf].

lemma marked_version_solution_conv: "gm r = hm s ⟷ g r ⋅ 𝖼  = 𝖼 ⋅  h s"
  unfolding cancel_right[of "g r ⋅ 𝖼" αh  "𝖼 ⋅ h s", symmetric] c_def rassoc
    g.marked_version_conjugates[symmetric] h.marked_version_conjugates[symmetric]
  unfolding lassoc c_def cancel..

lemma  criticalE:
  obtains p q r1 s1 r2 s2 where
    "αg ⋅ gm p = αh ⋅ hm q" and
    "⋀ p' q'. αg ⋅ gm p' = αh ⋅ hm q' ⟹ p ≤p p' ∧ q ≤p q'" and
    "gm (r1 ⋅ p) = hm (s1 ⋅ q)" and
    "gm (r2 ⋅ p) = hm (s2 ⋅ q)" and
    "r1 ⋅ p ≠ ε" and "r2 ⋅ p ≠ ε" and
    "hd (r1 ⋅ p) ≠ hd (r2 ⋅ p)"
proof-
  from criticalE'
  obtain p' q' r1 s1 r2 s2 where
    "g p' ⋅ αg = h q' ⋅ αh" and
    "g (p' ⋅ r1) = h (q' ⋅ s1)" and
    "g (p' ⋅ r2) = h (q' ⋅ s2)" and
    "r1 ≠ ε" and "r2 ≠ ε" and
    "hd r1 ≠ hd r2".
  from this(1)[folded g.marked_version_conjugates h.marked_version_conjugates]
  have "αg ⋅ gm p' = αh ⋅ hm q'".
  from min_completionE[OF this]
  obtain p q where "αg ⋅ gm p = αh ⋅ hm q" and "⋀p' q'. αg ⋅ gm p' = αh ⋅ hm q' ⟹ p ≤p p' ∧ q ≤p q'"
    by blast
  show thesis
  proof(rule)
    show "αg ⋅ gm p = αh ⋅ hm q" by fact
    hence "g p ⋅ 𝖼 = h q"
      unfolding g.marked_version_conjugates h.marked_version_conjugates unfolding c_def[symmetric] lassoc cancel_right.
    from  ‹g (p' ⋅ r1) = h (q' ⋅ s1)›[unfolded g.morph h.morph]
    have "g r1 = 𝖼 ⋅ h s1"
      unfolding ‹g p' ⋅ αg = h q' ⋅ αh›[unfolded c_def[symmetric] lassoc cancel_right, symmetric] rassoc cancel.
    show "gm (r1 ⋅ p) = hm (s1 ⋅ q)"
      unfolding marked_version_solution_conv g.morph h.morph rassoc ‹g p ⋅ 𝖼 = h q› ‹g r1 = 𝖼 ⋅ h s1›..
    from  ‹g (p' ⋅ r2) = h (q' ⋅ s2)›[unfolded g.morph h.morph]
    have "g r2 = 𝖼 ⋅ h s2"
      unfolding ‹g p' ⋅ αg = h q' ⋅ αh›[unfolded c_def[symmetric] lassoc cancel_right, symmetric] rassoc cancel.
    show "gm (r2 ⋅ p) = hm (s2 ⋅ q)"
      unfolding marked_version_solution_conv g.morph h.morph rassoc ‹g p ⋅ 𝖼 = h q› ‹g r2 = 𝖼 ⋅ h s2›..
    show "r1 ⋅ p ≠ ε"
      using ‹r1 ≠ ε› by blast
    show "r2 ⋅ p ≠ ε"
      using ‹r2 ≠ ε› by blast
    show "hd (r1 ⋅ p) ≠ hd (r2 ⋅ p)"
      using ‹hd r1 ≠ hd r2› ‹r1 ≠ ε› ‹r2 ≠ ε› by simp
    show " ⋀p' q'. αg ⋅ gm p' = αh ⋅ hm q' ⟹ p ≤p p' ∧ q ≤p q'" by fact
  qed
qed

text ‹Defining the beginning block›

definition beginning_block :: "binA list * binA list"  where
  "beginning_block = (SOME pair. αg ⋅ gm (fst pair) = αh ⋅ hm (snd pair) ∧
   (∀ p' q'. αg ⋅ gm p' = αh ⋅ hm q' ⟶ (fst pair) ≤p p' ∧ (snd pair) ≤p q'))"

definition fst_beginning_block ("p") where
  "fst_beginning_block ≡ fst beginning_block"
definition snd_beginning_block ("q") where
  "snd_beginning_block ≡ snd beginning_block"

lemma begin_block: "α ⋅ gm p = hm q" and
  begin_block_min: "α ⋅ gm p' = hm q' ⟹ p ≤p p' ∧ q ≤p q'"
proof-
  from criticalE
  obtain pa qa r1 s1 r2 s2 where
   "αg ⋅ gm pa = αh ⋅ hm qa" and
  "(⋀p' q'. αg ⋅ gm p' = αh ⋅ hm q' ⟹ pa ≤p p' ∧ qa ≤p q')" and
   "gm (r1 ⋅ pa) = hm (s1 ⋅ qa)" and "gm (r2 ⋅ pa) = hm (s2 ⋅ qa)" and
   "r1 ⋅ pa ≠ ε" and "r2 ⋅ pa ≠ ε" and "hd (r1 ⋅ pa) ≠ hd (r2 ⋅ pa)" by blast
  hence *: "αg ⋅ gm (fst (pa, qa)) = αh ⋅ hm (snd (pa, qa)) ∧
    (∀p' q'. αg ⋅ gm p' = αh ⋅ hm q' ⟶ fst (pa, qa) ≤p p' ∧ snd (pa, qa) ≤p q')"
    unfolding fst_conv snd_conv by fast
  let ?P =  "λ pair. (αg ⋅ gm (fst pair) = αh ⋅ hm (snd pair) ∧
   (∀ p' q'. αg ⋅ gm p' = αh ⋅ hm q' ⟶ (fst pair) ≤p p' ∧ (snd pair) ≤p q'))"
  from someI[of ?P, OF *]
  have pq: "αg ⋅ gm p = αh ⋅ hm q" "αg ⋅ gm p' = αh ⋅ hm q' ⟹ p ≤p p' ∧ q ≤p q'"
    unfolding fst_beginning_block_def snd_beginning_block_def beginning_block_def
    by blast+
  show "α ⋅ gm p =  hm q" and "α ⋅ gm p' = hm q' ⟹ p ≤p p' ∧ q ≤p q'"
    using pq unfolding lcp_diff[symmetric] rassoc cancel.
qed

lemma begin_block_conjug_conv:
  assumes "r ⋅ p = p ⋅ r'" and "s ⋅ q = q ⋅ s'"
  shows "g r = h s ⟷ gm r' = hm s'"
  unfolding solution_marked_version_conv
proof-
  have "α ⋅ gm r = hm s ⋅ α ⟷ α ⋅ gm r ⋅ gm p = hm s ⋅ α ⋅ gm p"
    unfolding lassoc cancel_right..
  also have "... ⟷ α ⋅ gm p ⋅ gm r' = hm q ⋅ hm s'"
    unfolding begin_block gm.morph[symmetric] hm.morph[symmetric] assms..
  also have "... ⟷ gm r' = hm s'"
    unfolding lassoc begin_block cancel..
  finally show "(α ⋅ gm r = hm s ⋅ α) = (gm r' = hm s')".
qed

lemma solution_ext_conv: "g r = h s ⟷ α ⋅ gm (r ⋅ p) = hm (s ⋅ q)"
  unfolding gm.morph hm.morph lassoc begin_block[symmetric]  cancel_right solution_marked_version_conv..

text ‹Both block exist›

lemma both_blocks: "marked.blockP c"
proof-
  from criticalE
  obtain p' q' r1 s1 r2 s2
    where "αg ⋅ gm p' = αh ⋅ hm q'"
          "gm (r1 ⋅ p') = hm (s1 ⋅ q')" "gm (r2 ⋅ p') = hm (s2 ⋅ q')" "r1 ⋅ p' ≠ ε" "r2 ⋅ p' ≠ ε" "hd (r1 ⋅ p') ≠ hd (r2 ⋅ p')".
  let ?ua = "r1 ⋅ p'" let ?va = "s1 ⋅ q'" let ?ub = "r2 ⋅ p'" let ?vb = "s2 ⋅ q'"
  obtain ea fa where "gm (ea) =m hm (fa)" and "hd ea = hd ?ua"
    using marked.min_coin_prefE[OF ‹gm (?ua) = hm (?va)› ‹?ua ≠ ε›].
  obtain eb fb where "gm (eb) =m hm (fb)" and "hd eb = hd ?ub"
    using  marked.min_coin_prefE[OF ‹gm ?ub = hm ?vb› ‹?ub ≠ ε›].
  from bin_neq_induct[OF ‹hd ?ua ≠ hd ?ub›[folded ‹hd ea = hd ?ua› ‹hd eb = hd ?ub›] marked.block_ex[OF ‹gm ea =m hm fa›] marked.block_ex[OF ‹gm eb =m hm fb›]]
  show "marked.blockP c".
qed

notation marked.suc_fst ("𝔢") and
         marked.suc_snd ("𝔣")

lemma sucs_eq: "gm (𝔢 τ) = hm (𝔣 τ)"
  using marked.blocks_eq both_blocks by blast

sublocale marked: two_binary_marked_blocks gm hm
  by unfold_locales (use both_blocks in fast)


section ‹Blocks and intersection›

text‹Every solution has a block decomposition. However, not all block combinations yield a solution. This motivates the following definition.›

definition coin_block where "coin_block τ  ≡ p ≤s p ⋅ (𝔢 τ) ∧ q ≤s q ⋅ (𝔣 τ)"

theorem  char_coincidence:
  "g r = h s ⟷ (∃ τ. coin_block τ ∧ r = (p ⋅ 𝔢 τ)<¯p ∧ s = (q ⋅ 𝔣 τ)<¯q)" (is "g r = h s ⟷ ?Q")
proof
  assume "g r = h s"
  hence "p ≤p r ⋅ p" and "q ≤p s ⋅ q"
    unfolding solution_ext_conv using begin_block_min  by blast+
  from lq_pref[OF this(1), symmetric] lq_pref[OF this(2), symmetric]
  have "r ⋅ p = p ⋅ p¯>(r ⋅ p)" and "s ⋅ q = q ⋅ q¯>(s ⋅ q)".
  hence "gm (p¯>(r ⋅ p)) = hm (q¯>(s ⋅ q))"
    using ‹g r = h s› begin_block_conjug_conv[of r "p¯> (r ⋅ p)" s "q¯> (s ⋅ q)"]
     by fast
  from marked.block_decomposition[OF this]
  obtain τ where gsuc: "𝔢 τ = p¯>(r ⋅ p)" and hsuc: "𝔣 τ = q¯>(s ⋅ q)".
  note lq = lq_pref[OF ‹p ≤p r ⋅ p›] lq_pref[OF ‹q ≤p s ⋅ q›]
  have r: "r = (p ⋅ 𝔢 τ)<¯p" and s: "s = (q ⋅ 𝔣 τ)<¯q"
    unfolding ‹𝔢 τ = p¯>(r ⋅ p)› ‹𝔣 τ = q¯>(s ⋅ q)›lq rq_triv by simp_all
  have "coin_block τ"
    unfolding coin_block_def gsuc hsuc lq using triv_suf by blast+
  thus ?Q
    using s r by blast
next
  assume ?Q
  then obtain τ where "p ≤s p ⋅ (𝔢 τ)" and "q ≤s q ⋅ (𝔣 τ)"
    and r: "r = (p⋅ (𝔢 τ))<¯p" and s: "s = (q⋅(𝔣 τ))<¯q" unfolding coin_block_def by blast
  hence gp: "gm p ⋅ gm (𝔢 τ) = gm ((p⋅(𝔢 τ))<¯p) ⋅ gm p"
    unfolding gm.morph[symmetric] rq_suf[OF ‹p ≤s p ⋅ (𝔢 τ)›] by blast
  have hq: "hm q ⋅ hm (𝔣 τ) = hm ((q⋅(𝔣 τ))<¯q) ⋅ hm q"
    unfolding  hm.morph[symmetric] rq_suf[OF ‹q ≤s q ⋅ (𝔣 τ)›] by blast
  from this
  show "g r = h s"
    unfolding begin_block[symmetric] sucs_eq[symmetric] rassoc gp
    unfolding lassoc cancel_right
    unfolding solution_marked_version_conv
    unfolding r s.
qed

theorem  char_coincidence':
  "g r = h s ⟷ (gm (p¯>(r ⋅ p)) = hm (q¯>(s ⋅ q)) ∧ p ≤p r ⋅ p ∧ q ≤p s ⋅ q)" (is "g r = h s ⟷ ?Q")
proof
  assume "g r = h s"
  from this[unfolded char_coincidence coin_block_def]
  obtain e f where  "gm e = hm f" "p ≤s p ⋅ e" "q ≤s q ⋅ f" "r = (p ⋅ e)<¯p" "s = (q ⋅ f)<¯q"
    using sucs_eq by blast
  have "r ⋅ p = p ⋅ e" and "s ⋅ q = q ⋅ f"
    unfolding ‹r = (p ⋅ e)<¯p› rq_suf[OF ‹p ≤s p ⋅ e›] ‹s = (q ⋅ f)<¯q› rq_suf[OF ‹q ≤s q ⋅ f›] by blast+
  hence "e = p¯>(r ⋅ p)" and "f = q¯>(s ⋅ q)"
    using lq_triv by fastforce+
  from ‹gm e = hm f›[unfolded this]
  show ?Q
    using triv_pref ‹r ⋅ p = p ⋅ e› ‹s ⋅ q = q ⋅ f› by blast
next
  assume ?Q
  hence "gm (p¯>(r ⋅ p)) = hm (q¯>(s ⋅ q))" and "p ≤p r ⋅ p" and "q ≤p s ⋅ q"
    by blast+
  from this(1)
  show "g r = h s"
    unfolding begin_block_conjug_conv[of r "p¯>(r ⋅ p)" s "q¯>(s ⋅ q)", OF lq_pref[symmetric] lq_pref[symmetric], OF ‹p ≤p r ⋅ p› ‹q ≤p s ⋅ q›].
qed

theorem coincidence_eq_blocks: "ℭ g h = {((p ⋅ 𝔢 τ)<¯p,(q ⋅ 𝔣 τ)<¯q) | τ. coin_block τ}"
  unfolding coincidence_set_def
  using pairs_extensional'[OF char_coincidence].

lemma
  minblock0:  "gm (𝔢 𝔞) =m hm (𝔣 𝔞)" and
  minblock1:  "gm (𝔢 𝔟) =m hm (𝔣 𝔟)" and
  hdblock0:   "hd (𝔢 𝔞)  = bina" and
  hdblock1:   "hd (𝔢 𝔟) = binb"
  using marked.blockP_D both_blocks marked.blockP_D_hd  by blast+

definition 𝒯 where "𝒯 ≡ {τ . coin_block τ}"

lemma 𝒯_def': "τ ∈ 𝒯 ⟷ coin_block τ"
  unfolding 𝒯_def mem_Collect_eq..

text‹Properties of the set of coincidence blocks›

lemma 𝒯_closed: assumes "coin_block τ1" and "coin_block τ2"
  shows "coin_block (τ1⋅τ2)"
proof-
  from assms
  have "p ≤s p ⋅ 𝔢 τ2" and "p ≤s p ⋅ 𝔢 τ1" and
    "q ≤s q ⋅ 𝔣 τ2" and "q ≤s q ⋅ 𝔣 τ1"
    unfolding coin_block_def by blast+
  from suf_prolong[OF this(1-2), unfolded rassoc] suf_prolong[OF this(3-4), unfolded rassoc]
  show "coin_block (τ1⋅τ2)"
    unfolding coin_block_def marked.sucs.h.morph marked.sucs.g.morph by blast
qed

lemma emp_block: "coin_block ε"
  unfolding coin_block_def marked.sucs.g.emp_to_emp marked.sucs.h.emp_to_emp by force

lemma 𝒯_hull:  "⟨𝒯⟩ = 𝒯"
proof (intro hull_I)
  show "ε ∈ 𝒯"
    unfolding 𝒯_def' coin_block_def marked.sucs.g.emp_to_emp marked.sucs.h.emp_to_emp by force
  show "⋀x y. x ∈ 𝒯 ⟹ y ∈ 𝒯 ⟹ x ⋅ y ∈ 𝒯"
    unfolding 𝒯_def' using 𝒯_closed.
qed

lemma  𝒯_pref: "coin_block τ1 ⟹ coin_block (τ1 ⋅ τ2) ⟹ coin_block τ2"
  using suf_prod_suf[of p "p ⋅ 𝔢 τ1" "𝔢 τ2"]
    suf_prod_suf[of q "q ⋅ 𝔣 τ1" "𝔣 τ2"]
  unfolding coin_block_def marked.sucs.g.morph marked.sucs.h.morph rassoc
  by blast

text ‹Translation from blocks to the intersection›

lemma translate_coin_blocks_to_intersection:
  "(h ∘ (λ x. (q ⋅ x)<¯q) ∘ 𝔣) ` 𝒯 = range g ∩ range h"
  unfolding coin_set_inter_snd[of h g, unfolded coincidence_eq_blocks, symmetric] 𝒯_def
proof-
  have   "(h ∘ snd) ` {(F x, G x) | x. coin_block x} = {h (G x) | x. coin_block x}" for F G :: "binA list ⇒ binA list"
    by (standard, standard, auto, force)
  note rule1 = this[of "λτ. (p ⋅ 𝔢 τ)<¯p" "λτ. (q ⋅ 𝔣 τ)<¯q"]
  have "(h ∘ I ∘ 𝔣) ` {x . coin_block x} = {h (I (𝔣 x))| x. coin_block x}" for I
    by rule auto
  from this[of "(λx. (q ⋅ x)<¯q)", folded rule1]
  show "(h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) ` Collect coin_block =
    (h ∘ snd) ` {((p ⋅ 𝔢 τ)<¯p , (q ⋅ 𝔣 τ)<¯q ) |τ. coin_block τ}".
qed

lemma translation_blocks_inj:
  "inj_on (h ∘ (λ x. (q ⋅ x)<¯q) ∘ 𝔣) ⟨𝒯⟩"
proof
  fix x y assume "x ∈ ⟨𝒯⟩" and "y ∈ ⟨𝒯⟩"
  hence "q ≤s q ⋅ 𝔣 x" and "q ≤s q ⋅ 𝔣 y" unfolding 𝒯_def' 𝒯_hull coin_block_def by blast+
  assume "(h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) x = (h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) y"
  hence "h ((q ⋅ 𝔣 x)<¯q) = h ((q ⋅ 𝔣 y)<¯q)"
    by simp
  from h.code_morph_code[OF this] rq_suf[OF ‹q ≤s q ⋅ 𝔣 x›] rq_suf[OF ‹q ≤s q ⋅ 𝔣 y›]
  have "𝔣 x = 𝔣 y"
    unfolding cancel[of q "𝔣 x" "𝔣 y", symmetric] by argo
  thus "x = y"
    using marked.sucs.h.code_morph_code by blast
qed

lemma translation_blocks_morph_on:  "morphism_on (h ∘ (λ x. (q ⋅ x)<¯q) ∘ 𝔣) 𝒯"
proof
  fix x y assume "x ∈ ⟨𝒯⟩" and "y ∈ ⟨𝒯⟩"
  hence "q ≤s q ⋅ 𝔣 x" and "q ≤s q ⋅ 𝔣 y"
    unfolding 𝒯_hull 𝒯_def' coin_block_def by blast+
  show "(h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) (x ⋅ y) =
           (h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) x⋅ (h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) y"
    unfolding comp_apply h.morph[symmetric] rq_reassoc[OF ‹q ≤s q ⋅ 𝔣 y›] lassoc rq_suf[OF ‹q ≤s q ⋅ 𝔣 x›]
    unfolding rassoc marked.sucs.h.morph..
qed

interpretation  morphism_on "(h ∘ (λ x. (q ⋅ x)<¯q) ∘ 𝔣)" 𝒯
  using translation_blocks_morph_on.

theorem inter_basis: "𝔅 (range g ∩ range h) = (h ∘ (λ x. (q ⋅ x)<¯q) ∘ 𝔣) ` (𝔅 𝒯)"
  using inj_basis_to_basis[OF translation_blocks_inj, unfolded 𝒯_hull]
    translate_coin_blocks_to_intersection by presburger


section ‹Simple blocks›

text ‹If both letters are blocks, the situation is easy›

theorem simple_blocks:  assumes "⋀ a. coin_block [a]" shows
  "coin_block τ"
  by (induct "τ", simp add: emp_block)
    (use assms 𝒯_closed[OF assms] hd_word in force)

theorem simple_blocks_UNIV: "(⋀ a. coin_block [a]) ⟹ 𝒯 = UNIV"
  using simple_blocks 𝒯_def' by auto

theorem simple_blocks_basis: assumes "⋀a. coin_block [a]"
  shows "𝔅 𝒯 = {𝔞, 𝔟}"
  using  basis_of_hull[of "{𝔞,𝔟}"] code.code_is_basis[OF bin_basis_code]
  unfolding bin_basis_generates simple_blocks_UNIV[OF assms, symmetric]
  by argo

section ‹At least one block›

text ‹At least one letter -- the last one -- is a block›

lemma last_letter_fst_suf: assumes "coin_block (z ⋅ [c])"
  shows  "p <s 𝔢 [c]"
proof-
  from assms
  have "p ≤s p ⋅ 𝔢 (z ⋅ [c])" and "q ≤s q ⋅ 𝔣 (z ⋅ [c])"
    unfolding coin_block_def by blast+
  hence "p ⨝s 𝔢 [c]" and "q ⨝s 𝔣 [c]"
    unfolding marked.sucs.g.morph marked.sucs.h.morph lassoc using ruler_suf'' by blast+
  have "¬ 𝔢 [c] ≤s p"
  proof
    assume "𝔢 [c] ≤s p"
    hence "gm (𝔢 [c]) ≤s α ⋅ gm p"
      using gm.suf_mono suf_ext by blast
    hence "hm (𝔣 [c]) ≤s hm q"
      unfolding begin_block sucs_eq.
    hence "𝔣 [c] ≤s q"
      using hm.suf_mono
        ‹q ⨝s 𝔣 [c]›[unfolded suf_comp_or] hm.code_morph_code  suffix_order.antisym by metis
    have "α ⋅ gm (p<¯𝔢 [c] ⋅ 𝔢 [c]) = hm (q<¯𝔣[c] ⋅ 𝔣[c])"
      unfolding rq_suf[OF ‹𝔢 [c] ≤s p›] rq_suf[OF ‹𝔣 [c] ≤s q›] begin_block[symmetric]..
    hence "α ⋅ gm (p<¯𝔢 [c]) = hm (q<¯𝔣[c])"
      unfolding gm.morph hm.morph marked.block_eq[OF both_blocks] lassoc cancel_right.
    from conjunct1[OF begin_block_min[OF this]]
    have "𝔢 [c] = ε"
      using rq_suf[OF ‹𝔢 [c] ≤s p›] same_prefix_nil by metis
    thus False
      using marked.sucs.g.sing_to_nemp by blast
  qed
  thus "p <s 𝔢 [c]"
    unfolding strict_suffix_def using ‹p ⨝s 𝔢 [c]›[unfolded suf_comp_or]
    by metis
qed

lemma rich_block_suf_fst':
  assumes "coin_block (z ⋅ [1-c] ⋅ [c]@Suc i)"
  shows "gm.bin_code_lcs ⋅ gm p ≤s gm (𝔢 ([1-c]⋅[c]@Suc i))"
proof-
  from last_letter_fst_suf assms[unfolded pow_Suc' lassoc]
  have "p <s 𝔢 [c]"
    by blast
  hence "𝔢 [c] = [c] ⋅ tl (𝔢 [c])"
    using marked.blockP_D_hd[OF both_blocks[of c]] hd_tl[OF marked.sucs.g.sing_to_nemp] by metis
  then obtain p' where "𝔢 [c] = [c] ⋅ p' ⋅ p"
    using ssufE[OF ‹p <s 𝔢 [c]›] ssuf_tl_suf suffix_def by metis
  hence *: "𝔢([1-c] ⋅ [c]@Suc i) = 𝔢 ([1-c] ⋅ [c]@i) ⋅ [c] ⋅ p' ⋅ p"
    unfolding pow_Suc' marked.sucs.g.morph by force
  have f1: "[c] ≤f 𝔢 ([1 - c] ⋅ [c] @ i) ⋅ [c] ⋅ p'"
    by fast
  have "[1 - c] ≤f ([1 - c] ⋅ tl (𝔢 [1 - c])) ⋅ 𝔢 ([c] @ i) ⋅ [c] ⋅ p'"
    unfolding rassoc by blast
  from this[unfolded hd_tl[OF marked.sucs.g.sing_to_nemp, of "1-c", unfolded marked.blockP_D_hd[OF both_blocks[of "1-c"]]]]
  have f2: "[1-c] ≤f 𝔢 ([1 - c] ⋅ [c] @ i) ⋅ [c] ⋅ p'"
    unfolding marked.sucs.g.morph rassoc.
  from marked.revs.g.bin_lcp_pref''[reversed, OF f1 f2, unfolded g.marked_lcs] g.marked_lcs
  show "gm.bin_code_lcs ⋅ gm p ≤s gm (𝔢 ([1-c]⋅[c]@Suc i))"
    unfolding * gm.morph lassoc suf_cancel_conv lcp_diff[symmetric] by simp
qed

lemma rich_block_suf_fst:
  assumes "coin_block (z ⋅ [1-c] ⋅ [c]@Suc i)"
  shows "α ⋅ gm (p) ≤s gm (𝔢 ([1-c]⋅[c]@Suc i))"
  using rich_block_suf_fst'[OF assms]
  using g.marked_lcs lcp_diff[symmetric] rassoc
  using suf_extD by metis

lemma rich_block_suf_snd':
  assumes "coin_block (z ⋅ [1-c] ⋅ [c]@Suc i)"
  shows "αh ⋅ hm q ≤s hm (𝔣 ([1-c]⋅[c]@Suc i))"
  using rich_block_suf_fst'[OF assms, unfolded marked.suc_eq'[OF both_blocks] g.marked_lcs rassoc]
  unfolding lcp_diff[symmetric] rassoc begin_block
  using  suf_extD by blast

lemma rich_block_suf_snd:
  assumes "coin_block (z ⋅ [1-c] ⋅ [c]@Suc i)"
  shows "q ≤s 𝔣 ([1-c]⋅[c]@Suc i)"
proof(rule ccontr)
  assume notsuf: "¬ q ≤s 𝔣 ([1 - c] ⋅ [c] @ Suc i)"
  from conjunct2[OF assms[unfolded coin_block_def]]
  have "q ≤s (q ⋅ 𝔣 z) ⋅ 𝔣 ([1 - c] ⋅ [c] @ Suc i)"
    unfolding marked.sucs.h.morph rassoc.
  note ruler = suf_ruler[OF this triv_suf]
  from this
  have "𝔣 ([1 - c] ⋅ [c] @ Suc i) <s q"
    using notsuf suffix_order.less_le_not_le by blast
   from hm.ssuf_mono[OF this]  rich_block_suf_fst[OF assms, unfolded marked.suc_eq'[OF both_blocks] begin_block]
  show False by force
qed

lemma  last_letter_block: assumes "coin_block (z ⋅ [c])"
  shows "coin_block [c]"
proof (cases)
  assume "z ∈ [c]*"
  from sing_pow_exp[OF this]
  obtain i where "z = [c]@i"
    by blast
  have "z ⋅ [c] = [c]@Suc i"
    unfolding ‹z = [c]@i› pow_Suc'..
  have "𝔢 (z ⋅ [c]) = (𝔢 [c])@Suc i" and "𝔣 (z ⋅ [c]) = (𝔣 [c])@Suc i"
    unfolding ‹z ⋅ [c] = [c]@Suc i› marked.sucs.g.pow_morph marked.sucs.h.pow_morph by simp_all
  from ‹coin_block (z ⋅ [c])›[unfolded coin_block_def this]
  show "coin_block [c]"
    unfolding coin_block_def using per_drop_exp_rev[OF zero_less_Suc] by metis
next
  assume "z ∉ [c]*"
  from distinct_letter_in_suf[OF this]
  obtain t z' b where z: "z = z' ⋅ [b] ⋅ [c]@t" and "b ≠ c"
    unfolding suffix_def by metis
  have "p <s 𝔢 [c]"
    using last_letter_fst_suf[OF ‹coin_block (z ⋅ [c])›].
  from ssufD[OF this, unfolded suffix_def]
  obtain p' where "p'⋅ p = 𝔢[c]" and "p' ≠ ε" by force
  hence "hd p' = c"
    using marked.blockP_D_hd[OF both_blocks[of c]] hd_append2[OF ‹p' ≠ ε›, of p] by argo
  hence "𝔢[c] = [c] ⋅ tl p' ⋅ p"
    unfolding ‹p'⋅ p = 𝔢[c]›[symmetric] using hd_tl[OF ‹p' ≠ ε›] by simp
  show "coin_block [c]"
  proof(cases)
    assume "q ≤s q ⋅ 𝔣 [c]"
    thus "coin_block [c]"
      unfolding coin_block_def using ssufD1[OF ssuf_ext[OF ‹p <s 𝔢 [c]›]] by blast
  next ― ‹the other option leads to a contradiction›
    write
      marked.sucs.h.bin_morph_mismatch_suf ("𝔡") and
      marked.sucs.h.bin_code_lcs ("β𝔥") and
      hm.bin_code_lcs ("βH") and
      gm.bin_code_lcs ("βG") and
      g.bin_code_lcs ("βg")
    assume "¬ q ≤s q ⋅ 𝔣 [c]"
      ― ‹suffix of @{term q}›
    hence "¬ q ≤s q ⋅ 𝔣 ([c]@ Suc t)"
      unfolding marked.sucs.h.pow_morph using per_drop_exp'[reversed] by blast
    hence "¬ q ≤s β𝔥 ⋅ 𝔣 ([c]@Suc t)"
      using suf_prolong_per_root[OF _ marked.sucs.revs.h.bin_lcp_pref_all[reversed], of q "[c]@Suc t"] by blast

― ‹analysis of q›
    have "q ≤s q ⋅ 𝔣(z' ⋅ [b] ⋅ [c]@Suc t)"
      using ‹coin_block (z ⋅ [c])›
      unfolding z coin_block_def rassoc pow_Suc' by blast
    note per_exp_pref[reversed, OF this, of 2, unfolded pow_two]
    hence suf1:  "q ≤s q ⋅ 𝔣 (z' ⋅ [b]) ⋅ 𝔣 ([c] @ Suc t ⋅ z' ⋅ [b]) ⋅ 𝔣 ([c] @ Suc t)"
      unfolding marked.sucs.h.morph rassoc.
    have "[𝔡 b] ⋅ β𝔥 ≤s 𝔣 ([c]@Suc t ⋅ z') ⋅ 𝔣 [b]"
      by (rule marked.sucs.revs.h.bin_lcp_mismatch_pref_all_set[reversed])
        (unfold bin_neq_swap[OF ‹b ≠ c›], simp)
    from this[folded marked.sucs.h.morph lassoc, unfolded suffix_def]
    obtain zs where "𝔣 ([c] @ Suc t ⋅ z' ⋅ [b]) = zs ⋅ [𝔡 b] ⋅ β𝔥"
      by blast
    have suf2: "[𝔡 b] ⋅ β𝔥 ⋅ 𝔣 ([c]@Suc t) ≤s q ⋅ 𝔣 (z' ⋅ [b]) ⋅ 𝔣 ([c] @ Suc t ⋅ z' ⋅ [b]) ⋅ 𝔣 ([c] @ Suc t)"
      unfolding ‹𝔣 ([c] @ Suc t ⋅ z' ⋅ [b]) = zs ⋅ [𝔡 b] ⋅ β𝔥›
      using triv_suf[of "[𝔡 b] ⋅ β𝔥 ⋅ 𝔣 ([c] @ Suc t)" "q ⋅ 𝔣 (z' ⋅ [b]) ⋅ zs"] unfolding rassoc.
    have "q ⨝s [𝔡 b] ⋅ β𝔥 ⋅ 𝔣 ([c]@Suc t)"
      using ruler[reversed, OF suf1 suf2] unfolding suf_comp_or.
    with ‹¬ q ≤s β𝔥 ⋅ 𝔣 ([c]@Suc t)›
    have "[𝔡 b] ⋅ β𝔥 ⋅ 𝔣 ([c]@Suc t) ≤s q"
      unfolding suf_comp_or hd_word[symmetric] suffix_Cons using suffix_order.eq_refl[OF sym, of q] by blast
    from suffixE[OF this]
    obtain q' where q_factors: "q = q' ⋅ [𝔡 b] ⋅ β𝔥 ⋅ 𝔣 ([c] @ Suc t)".

― ‹length of @{term "βH ∧p α"}›
― ‹1. inequality›
    from marked.lcs_fst_suf_snd
    have "βG ≤s βH ⋅ hm β𝔥".
    from suf_len[OF this, unfolded lenmorph]
    have ineq1: "|βG| ≤ |βH| + |hm β𝔥|"
      using lenarg[OF lcp_diff, unfolded lenmorph] by linarith
        ― ‹2. inequality›
    from begin_block[unfolded q_factors, unfolded pow_Suc' marked.sucs.h.morph hm.morph, folded sucs_eq[of "[c]"], unfolded ‹𝔢[c] = [c] ⋅ tl p' ⋅ p› gm.morph lassoc cancel_right, unfolded rassoc]
    have "α = hm q' ⋅ hm [𝔡 b] ⋅ hm β𝔥 ⋅ hm (𝔣 ([c] @ t)) ⋅ gm [c] ⋅ gm (tl p')".
    from lenarg[OF this] lenarg[OF lcp_diff]
    have ineq2: "|hm [𝔡 b]| + |gm [c]| + |hm β𝔥| ≤ |αg|"
      unfolding lenmorph by linarith
        ― ‹conclusions›
    have concl1: "|hm [𝔡 b]| + |gm [c]| ≤ |αg|"
      using ineq2 by linarith
    have concl2: "|hm [𝔡 b]| + |gm [c]| ≤ |βH|"
      using ineq1 ineq2 lenarg[OF g.marked_lcs, unfolded lenmorph]
      by linarith
    from suf_comp_monotone[OF marked.suf_comp_lcs] sufI[OF g.marked_lcs[symmetric]]
    have "αg ⨝s βH"
      by blast
    have concl: "|hm [𝔡 b]| + |gm [c]| ≤ |αg ∧s βH|"
      by (rule disjE[OF ‹αg ⨝s βH›[unfolded suf_comp_or], unfolded lcs_suf_conv[symmetric] lcs_sym[of βH]])
        (use concl1 concl2 in argo)+

― ‹two periods of @{term "αg ∧s βH"}›
    have "αg ≤s αg ⋅ gm [c]"
      unfolding g.marked_version_conjugates by blast
    hence per1: "αg ∧s βH ≤s (αg ∧s βH) ⋅ gm [c]"
      using lcs_suf suf_keeps_root by blast
    have "βH ≤s βH ⋅ hm [𝔡 b]"
      using marked.revs.h.bin_lcp_pref_all[reversed].
    hence per2: "αg ∧s βH ≤s (αg ∧s βH) ⋅ hm [𝔡 b]"
      using lcs_suf' suf_keeps_root by blast
    from two_pers[reversed, OF per2 per1 concl]
    have "gm [c] ⋅ hm [𝔡 b] = hm [𝔡 b] ⋅ gm [c]".

    from marked.comm_sings_block[OF this]
    obtain n where "𝔣 [c] = [𝔡 b] @ Suc n" by blast
    from marked.sucs.h.sing_pow_mismatch_suf[OF ‹𝔣 [c] = [𝔡 b] @ Suc n›]
         ‹b ≠ c› marked.sucs.h.bin_mismatch_suf_inj
    have False
      unfolding inj_on_def by blast
    thus "coin_block [c]"
      by blast
  qed
qed

end

section "Infinite case"

locale  binary_codes_coincidence_infinite = binary_codes_coincidence_two_generators for a1 +
  assumes non_block: "¬ coin_block [a1]"

begin

subsection ‹Description of coincidence blocks›

lemma swap_coin_block: "coin_block [1-a1]"
proof-
  obtain u v where "g u =m h v"
    using coin_ex by blast
  from min_coinD[OF this, unfolded char_coincidence]
  obtain τ where "coin_block τ" and "u = (p ⋅ 𝔢 τ)<¯p"
    by blast
  from conjunct1[OF min_coinD'[OF ‹g u =m h v›], unfolded this(2)]
  have "τ ≠ ε"
    using rq_self[of p] marked.sucs.g.emp_to_emp emp_simps(1) by metis
  from append_butlast_last_id[OF this]
  have "coin_block [last τ]"
    using ‹coin_block τ› last_letter_block by metis
  with non_block
  show "coin_block [1-a1]"
    by (cases rule: bin_swap_exhaust[of "last τ" a1]) simp_all
qed

definition coincidence_exponent ("t") where
  "coincidence_exponent = (LEAST x. (q ≤s q ⋅ 𝔣([a1] ⋅ [1-a1]@Suc x)))"

lemma q_nemp: "q ≠ ε"
proof (rule notI)
  assume "q = ε"
  with coin_block_def
    marked.ne_g[OF suf_of_emp[OF begin_block[unfolded hm.emp_to_emp'[OF this]]]]  non_block
  show False by blast
qed

lemma p_suf: "p <s 𝔢 [1-a1]"
  using last_letter_fst_suf[of ε, unfolded emp_simps, OF swap_coin_block].

lemma coin_exp: "coin_block ([a1] ⋅ [1-a1]@Suc t)" and
  coin_exp_min: "j ≤ t ⟹ ¬ coin_block ([a1] ⋅ [1-a1]@j)"
proof-
  have "|q| ≤ |𝔣 ([1-a1]@|q|)|"
    using long_pow marked.sucs.h.pow_morph marked.sucs.h.sing_to_nemp by metis
  moreover have "q ≤s q ⋅ 𝔣 ([1-a1]@|q|)"
    unfolding marked.sucs.h.pow_morph using conjunct2[OF swap_coin_block[unfolded coin_block_def]] using per_exp_suf by blast
  ultimately have "q ≤s 𝔣 ([a1] ⋅ [1-a1]@|q|)"
    unfolding marked.sucs.h.morph using suf_prod_le suf_ext by blast
  from LeastI[of "λ x. (q ≤s q ⋅ 𝔣([a1] ⋅ [1-a1]@Suc x))",
      folded coincidence_exponent_def, of "|q| - 1"] suf_ext[OF this, of q]
  have "q ≤s q ⋅ 𝔣 ([a1] ⋅ [1 - a1] @ Suc t)"
    unfolding Suc_minus[OF nemp_len[OF q_nemp]] by blast
  thus "coin_block ([a1] ⋅ [1-a1]@Suc t)"
    unfolding pow_Suc' marked.sucs.g.morph coin_block_def
    using suf_ext[OF ssufD1[OF p_suf], of "p ⋅ 𝔢 [a1] ⋅ 𝔢 ([1 - a1] @ t)", unfolded rassoc] by blast
next
  fix j assume "j ≤ t"
  show "¬ coin_block ([a1] ⋅ [1-a1]@j)"
  proof (cases "j = 0", simp add: non_block)
    assume "j ≠ 0"
    hence "j - 1 < t" and "t ≠ 0"
      using ‹j ≤ t› ‹j ≠ 0› by simp_all
    thus "¬ coin_block ([a1] ⋅ [1-a1]@j)"
      using not_less_Least[of "j - 1" "λ x. q ≤s q ⋅ 𝔣 ([a1] ⋅ [1 - a1] @ Suc x)", folded coincidence_exponent_def]
      unfolding coin_block_def Suc_minus[OF ‹j ≠ 0›] by linarith
  qed
qed

lemma exp_min: "¬ q ≤s 𝔣 [1-a1]@t"
proof (cases "t = 0", simp add: q_nemp)
  assume "t ≠ 0"
  hence "t -1 < t" by simp
  show ?thesis
    using not_less_Least[of "t -1" "λ m. q ≤s  q ⋅ 𝔣 ([a1] ⋅ [1 - a1] @ Suc m)", folded coincidence_exponent_def, OF ‹t - 1 < t›, unfolded marked.sucs.h.morph Suc_minus[OF ‹t ≠ 0›]]
    unfolding marked.sucs.h.pow_morph using suf_ext by metis
qed

lemma q_suf_conv: "q ≤s 𝔣 ([a1]⋅[1-a1]@Suc k) ⟷ t ≤ k"
proof
  have psuf': "p ≤s p ⋅ 𝔢 ([a1] ⋅ [1 - a1] @ Suc k)" for k
    unfolding pow_Suc' using  marked.sucs.g.morph ssufD1[OF p_suf] suffix_appendI by metis
  assume "q ≤s 𝔣 ([a1] ⋅ [1 - a1] @ Suc k)"
  hence  "¬ Suc k  ≤ t"
    using coin_exp_min[of "Suc k"] psuf'[of k] suf_ext[of q _ q] unfolding coin_block_def by blast
  thus "t ≤ k"
    by linarith
next
  assume "t ≤ k"
  have "q ≤s q ⋅ 𝔣[1-a1]"
    using coin_block_def swap_coin_block by blast
  have "q ≤s 𝔣 [a1] ⋅ 𝔣 ([1-a1]@Suc t)"
    using coin_exp rich_block_suf_snd[of ε "1 - a1" t, unfolded emp_simps binA_simps] unfolding marked.sucs.h.morph  by blast
  from suf_prolong[OF per_exp_suf[OF ‹q ≤s q ⋅ 𝔣[1-a1]›, folded marked.sucs.h.pow_morph] this, of "k-t", folded marked.sucs.h.morph lassoc, folded add_exps[of "[1-a1]" "Suc t"]]
  show "q ≤s 𝔣 ([a1] ⋅ [1-a1]@Suc k)"
    using ‹t ≤k› by fastforce
qed

lemma coin_block_with_bad_letter: assumes "a1 ∈ set w"
  shows "coin_block w ⟷ [1-a1]@Suc t ≤s w"
proof-
  obtain i b where "[b] ⋅ [1-a1]@i ≤s w" and "b ≠ 1-a1"
    using  distinct_letter_in_suf[of w "1-a1", OF neq_set_not_root[OF bin_swap_neq, OF assms]].
  have "b = a1"
    using bin_neq_swap'''[OF ‹b ≠ 1-a1›, unfolded binA_simps].
  from ‹[b] ⋅ [1-a1]@i ≤s w›[unfolded this, unfolded suffix_def]
  obtain w' where w: "w = w' ⋅ [a1] ⋅ [1-a1]@i" by blast
  show ?thesis
  proof(cases)
    assume "i = 0"
    have "¬ [1 - a1] @ Suc t ≤s w' ⋅ [a1]"
      unfolding pow_Suc' using bin_swap_neq[of a1]
      by simp
    then show "coin_block w ⟷ [1-a1]@Suc t ≤s w"
      unfolding w ‹i = 0› cow_simps using last_letter_block non_block by meson
  next
    assume "i ≠ 0"
    have psuf: "p ≤s p ⋅ 𝔢 (w' ⋅ [a1] ⋅ [1 - a1] @ Suc k)" for k
      unfolding pow_Suc' using  marked.sucs.g.morph ssufD1[OF p_suf] suffix_appendI by metis
    have psuf': "p ≤s p ⋅ 𝔢 ([a1] ⋅ [1 - a1] @ Suc k)" for k
      unfolding pow_Suc' using  marked.sucs.g.morph ssufD1[OF p_suf] suffix_appendI by metis
    have equiv1: "coin_block (w'⋅[a1]⋅[1-a1]@Suc k) ⟷ q ≤s 𝔣 ([a1]⋅[1-a1]@Suc k)" for k
    proof
      show "coin_block (w' ⋅ [a1] ⋅ [1 - a1] @ Suc k) ⟹ q ≤s 𝔣 ([a1] ⋅ [1 - a1] @ Suc k)"
        using rich_block_suf_snd[of w' "1 - a1" k] suffix_append unfolding binA_simps marked.sucs.h.morph by blast
      show "q ≤s 𝔣 ([a1] ⋅ [1 - a1] @ Suc k) ⟹ coin_block (w' ⋅ [a1] ⋅ [1 - a1] @ Suc k)"
        unfolding coin_block_def marked.sucs.h.morph using psuf suffix_appendI by metis
    qed
    have "t ≤ k ⟷ [1-a1]@Suc t ≤s w'⋅[a1]⋅[1-a1]@Suc k" for k
      using sing_exp_pref_iff[reversed, OF bin_swap_neq', symmetric, of "Suc t" "Suc k" "1-a1", unfolded Suc_le_mono binA_simps rassoc].
    from equiv1[unfolded q_suf_conv this, of "i-1", unfolded Suc_minus[OF ‹i ≠ 0›], folded w]
    show ?thesis.
  qed
qed

section ‹Description of the basis›

text‹The infinite part of the basis›

inductive_set 𝒲 :: "binA list set" where
  "[a1] ⋅ [1-a1]@Suc t  ∈ 𝒲"
| "τ ∈ 𝒲 ⟹  i ≤ t ⟹ [a1] ⋅ [1-a1]@i ⋅ τ ∈ 𝒲"

lemma 𝒲_nemp: "x ∈ 𝒲 ⟹ x ≠ ε"
  by (rule 𝒲.cases[of x "x ≠ ε"], simp_all)

lemma 𝒲_nemp': "x ∈ ({[1 - a1]} ∪ 𝒲) ⟹ x ≠ ε"
  using 𝒲_nemp by blast

lemma 𝒲_hd: "x ∈  𝒲 ⟹  hd x = a1"
  by (induction x rule: 𝒲.induct, simp_all)

lemma 𝒲_set: "x ∈ 𝒲 ⟹  a1 ∈ set x"
  using 𝒲_hd 𝒲_nemp hd_in_set by blast

lemma 𝒲_butlast_hd_tl: "x ∈ 𝒲 ⟹  butlast x = [a1] ⋅ butlast (tl x)"
  by (induction x rule: 𝒲.induct, auto)

lemma 𝒲_suf: "x ∈ 𝒲 ⟹  [a1] ⋅[1-a1]@Suc t ≤s x"
  by (induction x rule: 𝒲.induct, simp_all add: suffix_Cons suffix_append)

lemma 𝒲_fac: "x ∈ 𝒲 ⟹  ¬ [1-a1]@Suc t ≤f butlast x"
proof (induction x rule: 𝒲.induct)
  show "¬ [1 - a1] @ Suc t ≤f butlast ([a1] ⋅ [1 - a1] @ Suc t)"
    using fac_len_eq[of "[1 - a1] @ Suc t" "butlast ([a1] ⋅ [1 - a1] @ Suc t)"]
    unfolding pow_Suc' lassoc butlast_snoc  sing_pow_len lenmorph sing_len
    unfolding pow_comm[of "[1-a1]"] add.commute[of t] cancel_right
    using bin_swap_neq by fast
  fix x' i
  assume "x' ∈ 𝒲" and notf: "¬ [1 - a1] @ Suc t ≤f butlast x'" and "i ≤ t"
  show "¬ [1 - a1] @ Suc t ≤f butlast ([a1] ⋅ [1 - a1] @ i ⋅ x')"
  proof
    assume "[1 - a1] @ Suc t ≤f butlast ([a1] ⋅ [1 - a1] @ i ⋅ x')"
    hence "[1 - a1] @ Suc t ≤f [a1] ⋅ [1 - a1] @ i ⋅ butlast x'"
      unfolding lassoc butlast_append using 𝒲_nemp[OF  ‹x' ∈ 𝒲›] by force
    then obtain pp ss where fac: "pp ⋅ [1 - a1] @ Suc t ⋅ ss = ([a1] ⋅ [1 - a1] @ i) ⋅ butlast x'" unfolding rassoc by fast
    from notf eqd[OF this[symmetric]]
    have "¬ |[a1] ⋅ [1 - a1] @ i| ≤ |pp|"
      unfolding fac_def by metis
    hence "|pp| ≤ i"
      unfolding lenmorph by simp
    have "pp ≠ ε"
      using fac emp_simps(2) bin_swap_neq[of a1] unfolding pow_Suc rassoc by force
    have "Suc i < |pp| + Suc t" and "Suc i -|pp| < Suc t"
      using nemp_len[OF ‹pp ≠ ε›] ‹i ≤ t› by linarith+
    have "(pp ⋅ [1 - a1] @ Suc t ⋅ ss)!(Suc i) = a1"
      unfolding fac 𝒲_butlast_hd_tl[OF ‹x' ∈ 𝒲›]
      using nth_append_length[of "[a1] ⋅ [1 - a1] @ i" a1] unfolding lenmorph sing_pow_len sing_len swap_len by force
    from this[unfolded lassoc nth_append[of _ ss]]
    have "(pp ⋅ [1 - a1] @ Suc t)!(Suc i) = a1"
      unfolding lenmorph sing_pow_len using ‹Suc i < |pp| + Suc t› by presburger
    from this[unfolded nth_append]
    have "([1 - a1] @ Suc t)!(Suc i - |pp|) = a1"
      using ‹|pp| ≤ i› by force
    thus False
      unfolding sing_pow_nth[OF ‹Suc i -|pp| < Suc t›]
      using bin_swap_neq by blast
  qed
qed

lemma pref_code_𝒲: "pref_code ({[1-a1]} ∪ 𝒲)"
proof
  show nemp: "ε ∉ {[1 - a1]} ∪ 𝒲"
    using 𝒲_nemp by auto
  show "u = v" if u_in: "u ∈ {[1 - a1]} ∪ 𝒲" and v_in: "v ∈ {[1 - a1]} ∪ 𝒲" and  "u ≤p v" for u v
  proof (rule bin_swap_exhaust[of "hd u" a1])
    assume "hd u = 1 - a1"
    hence "u = [1-a1]"
      using u_in[unfolded Un_def mem_Collect_eq]
        𝒲_hd[of u] bin_swap_neq' by blast
    from sing_pref_hd[OF ‹u ≤p v›[unfolded this]]
    have "hd v = 1 - a1".
    hence "v = [1-a1]"
      using v_in[unfolded Un_def mem_Collect_eq]
        𝒲_hd[of v] bin_swap_neq' by blast
    with ‹u = [1-a1]›
    show "u = v"
      by simp
  next
    assume "hd u = a1"
    have "u ≠ ε" "v ≠ ε"
      using  nemp u_in v_in by blast+
    from pref_hd_eq[OF ‹u ≤p v› ‹u ≠ ε›]
    have "hd v = a1"
      using ‹hd u = a1› by simp
    from  u_in ‹hd u = a1› bin_swap_neq[of a1]
    have "u ∈ 𝒲"
      unfolding Un_def mem_Collect_eq using singletonD[of u "[1-a1]"] list.sel(1)[of "1-a1" ε] by metis
    from ‹hd v = a1› v_in ‹hd u = a1› bin_swap_neq[of a1]
    have "v ∈ 𝒲"
      unfolding Un_def mem_Collect_eq using singletonD[of v "[1-a1]"] list.sel(1)[of "1-a1" ε] by metis
    from 𝒲_suf[OF ‹u ∈ 𝒲›]
    have "[1 - a1] @ Suc t ≤s u"
      using suf_extD by blast
    hence "¬ u ≤p butlast v"
      using 𝒲_fac[OF ‹v ∈ 𝒲›] unfolding fac_def suffix_def prefix_def by fastforce
    with ‹u ≤p v›
    show "u = v"
      using spref_butlast_pref by blast
  qed
qed

lemma 𝒲_coin_blocks:
  assumes  "x ∈ {[1 - a1]} ∪ 𝒲"  shows "x ∈ 𝒯"
proof-
  consider "x = [1-a1]" | "x ∈ 𝒲"
    using ‹x ∈ {[1 - a1]} ∪ 𝒲›  by blast
  thus "x ∈ 𝒯"
  proof (cases)
    assume "x = [1-a1]"
    show "x ∈ 𝒯"
      unfolding 𝒯_def' ‹x = [1-a1]› using swap_coin_block.
  next
    assume "x ∈ 𝒲"
    show "x ∈ 𝒯"
      unfolding 𝒯_def' coin_block_with_bad_letter[OF 𝒲_set[OF ‹x ∈ 𝒲›]] using suf_extD[OF 𝒲_suf[OF ‹x ∈ 𝒲›]].
  qed
qed

lemma 𝒲_gen_T: "⟨{[1-a1]} ∪ 𝒲⟩ = 𝒯"
proof
  from subsetI[OF 𝒲_coin_blocks, THEN hull_mono]
  show "⟨{[1 - a1]} ∪ 𝒲⟩ ⊆ 𝒯"
    unfolding 𝒯_hull.
next
  show "𝒯 ⊆ ⟨{[1 - a1]} ∪ 𝒲⟩"
  proof
    fix x assume "x ∈ 𝒯"
    from this[unfolded 𝒯_def'] have "coin_block x".
    thus "x ∈ ⟨{[1 - a1]} ∪ 𝒲⟩"
    proof (induction "|x|" arbitrary: x rule: less_induct)
      case less
      show ?case
      proof (cases "∃ px. px ≠ ε ∧ px <p x ∧ coin_block px")
        assume "∃ px. px ≠ ε ∧ px <p x ∧ coin_block px"
        from exE[OF this]
        obtain px where "px ≠ ε" and "px <p x" and "coin_block px" by metis
        from spref_exE[OF ‹px <p x›]
        obtain sx where "px⋅sx = x" and "sx ≠ ε".
        from 𝒯_pref[OF ‹coin_block px› ‹coin_block x›[folded ‹px⋅sx = x›]]
        have "coin_block sx".
        have "|px| < |x|" and "|sx| < |x|"
          using ‹px⋅sx = x› ‹px ≠ ε› ‹sx ≠ ε› by auto
        from less.hyps[OF this(1) ‹coin_block px›]
          less.hyps[OF this(2) ‹coin_block sx›]
        show "x ∈ ⟨{[1 - a1]} ∪ 𝒲⟩"
          using ‹px⋅sx = x› by auto
      next
        assume non_ex: "∄ px. px ≠ ε ∧ px <p x ∧ coin_block px"
        show "x ∈ ⟨{[1 - a1]} ∪ 𝒲⟩"
        proof (cases "a1 ∈ set x")
          assume "a1 ∉ set x"
          then obtain k where "x = [1 - a1]@k"
            using bin_without_letter by blast
          thus "x ∈ ⟨{[1 - a1]} ∪ 𝒲⟩"
            using gen_in[THEN power_in] by fast
        next
          assume "a1 ∈ set x"
          hence "x ≠ ε" by force
          have "hd x = a1"
          proof (rule ccontr)
            assume "hd x ≠ a1"
            hence "hd x = 1-a1"
              using bin_neq_iff by auto
            from non_ex swap_coin_block hd_tl[OF ‹x ≠ ε›, unfolded this]
            have "tl x = ε" by blast
            from ‹[1 - a1] ⋅ tl x = x›[unfolded this emp_simps]
            show False
              using neq_in_set_not_pow[OF bin_swap_neq[of a1] ‹a1 ∈ set x›, of 1, unfolded exp_simps] by simp
          qed
          define j where "j = (LEAST k. ¬ [a1]⋅[1-a1]@Suc k ≤p x)"
          hence "¬ [a1]⋅[1-a1]@(Suc t) <p x"
            using coin_exp non_ex by blast
          hence "¬ [a1]⋅[1-a1]@Suc(Suc t) ≤p x"
            unfolding pow_Suc'[of _ "Suc t"] lassoc
            using prefix_snocD by metis
          from Least_le[of "λ i. ¬ ([a1]⋅[1-a1]@Suc i) ≤p x", OF this, folded j_def]
          have "j ≤ Suc t".
          have "¬ [a1]⋅[1-a1]@ Suc j ≤p x"
            using LeastI[of "λ i. ¬ ([a1]⋅[1-a1]@Suc i) ≤p x", OF ‹¬ ([a1]⋅[1-a1]@Suc(Suc t)) ≤p x›, folded j_def].
          have "[a1]⋅[1-a1]@j ≤p x"
            using not_less_Least[of "j-1" "λ i. ¬ ([a1]⋅[1-a1]@Suc i) ≤p x"]
            unfolding j_def[symmetric] not_not
            by (cases "j = 0", simp_all add: hd_pref[OF ‹x ≠ ε›, unfolded ‹hd x = a1›])
          show "x ∈ ⟨{[1 - a1]} ∪ 𝒲⟩"
          proof(cases "j = Suc t")
            assume "j = Suc t"
            have "x = [a1]⋅[1-a1]@j"
              using ‹[a1]⋅[1-a1]@j ≤p x› ‹¬ [a1] ⋅ [1 - a1] @ Suc t <p x›
              unfolding ‹j = Suc t› by force
            from 𝒲.intros(1)[folded ‹j = Suc t›, folded this]
            show "x ∈ ⟨{[1 - a1]} ∪ 𝒲⟩" by auto
          next
            assume "j ≠ Suc t"
            hence "j ≤ t" using ‹j ≤ Suc t› by force
            from prefE[OF ‹[a1]⋅[1-a1]@j ≤p x›, unfolded rassoc]
            obtain x' where "x = [a1] ⋅ [1-a1]@j ⋅ x'".
            with coin_exp_min[OF ‹j ≤ t›] ‹coin_block x›
            have "x' ≠ ε"
              by auto
            from ‹¬ [a1] ⋅ [1-a1]@Suc j ≤p x› hd_tl[OF this]
            have "hd x' = a1"
              unfolding ‹x = [a1] ⋅ [1-a1]@j ⋅ x'› pow_Suc' pref_cancel_conv
              using bin_neq_iff'[of "hd x'" "1-a1", unfolded binA_simps] by fastforce
            from ‹[hd x'] ⋅ tl x' = x'›[unfolded this]
              ‹coin_block x›[unfolded coin_block_with_bad_letter[OF ‹a1 ∈ set x›]]
            have "[1-a1]@Suc t ≤s [a1] ⋅ [1 - a1] @ j ⋅ [a1] ⋅ tl x'"
              unfolding ‹x = [a1] ⋅ [1-a1]@j ⋅ x'› by presburger
            have "a1 ∉ set ([1-a1]@Suc t)"
              using neq_in_set_not_pow[OF bin_swap_neq, of a1] by blast
            hence "¬ [a1] ⋅ tl x' ≤s [1-a1]@Suc t"
              unfolding suffix_def using Cons_eq_appendI in_set_conv_decomp by metis
            with ruler[reversed, of x', OF _ ‹[1-a1]@Suc t ≤s x›]
            have "[1-a1]@Suc t ≤s x'"
              unfolding ‹x = [a1] ⋅ [1-a1]@j ⋅ x'› ‹[a1] ⋅ tl x' = x'› suffix_def by fastforce
            have "a1 ∈ set x'"
              using ‹hd x' = a1› ‹x' ≠ ε› hd_in_set by blast
            from coin_block_with_bad_letter[OF this]
            have "coin_block x'"
              using ‹[1-a1]@Suc t ≤s x'› by blast
            have "|x'| < |x|"
              using lenarg[OF ‹x = [a1] ⋅ [1-a1]@j ⋅ x'›] unfolding lenmorph by simp
            from less.hyps[OF this ‹coin_block x'›]
            obtain xs' where "xs' ∈ lists ({[1 - a1]} ∪ 𝒲)" and "concat xs' = x'" using hull_concat_listsE by blast
            have "xs' ≠ ε"
              using ‹concat xs' = x'› ‹x' ≠ ε› concat.simps(1) by blast
            from lists_hd_in_set[OF this ‹xs' ∈ lists ({[1 - a1]} ∪ 𝒲)›]
            have "hd xs' ∈ ({[1 - a1]} ∪ 𝒲)".
            from 𝒲_coin_blocks[OF this] 𝒲_nemp'[OF this]
            have "coin_block (hd xs')" and "hd xs' ≠ ε"
              unfolding 𝒯_def'.
            have "hd (hd xs') = a1"
              using  hd_concat[OF ‹xs' ≠ ε› ‹hd xs' ≠ ε›, symmetric]
              unfolding ‹concat xs' = x'› ‹hd x' = a1›.
            hence "hd xs' ∈ 𝒲"
              using ‹hd xs' ∈ ({[1 - a1]} ∪ 𝒲)›  bin_swap_neq[of a1] list.sel(1)[of "1-a1" ε]
              unfolding Un_def mem_Collect_eq singleton_iff by metis
            hence "[a1] ⋅ [1-a1]@j ⋅ hd xs' ∈ 𝒲"
              using ‹j ≤ t› 𝒲.intros(2) by blast
            with 𝒲_coin_blocks
            have "coin_block ([a1] ⋅ [1-a1]@j ⋅ hd xs')"
              unfolding 𝒯_def' Un_def by blast
            have "[a1] ⋅ [1-a1]@j ⋅ hd xs' ≤p x"
              using hd_concat_tl[OF ‹xs' ≠ ε›]
              unfolding ‹concat xs' = x'› ‹x = [a1] ⋅ [1-a1]@j ⋅ x'›
              by fastforce
            with non_ex ‹coin_block (hd xs')› ‹hd xs' ≠ ε›
            have "x = [a1] ⋅ [1-a1]@j ⋅ hd xs'"
              using ‹coin_block ([a1] ⋅ [1 - a1] @ j ⋅ hd xs')› strict_prefixI suf_nemp by metis
            from ‹[a1] ⋅ [1-a1]@j ⋅ hd xs' ∈ 𝒲›[folded this]
            show "x ∈ ⟨{[1 - a1]} ∪ 𝒲⟩"
              by auto
          qed
        qed
      qed
    qed
  qed
qed

lemma 𝒲_explicit: "𝒲 = {w ⋅ [a1] ⋅ [1-a1]@Suc t | w. w ∈ ⟨{[a1] ⋅ [1-a1]@i | i. i ≤ t}⟩}"
proof
  show "𝒲 ⊆ {w ⋅ [a1] ⋅ [1 - a1] @ Suc t |w. w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩}"
  proof
    fix x assume "x ∈ 𝒲"
    thus "x ∈ {w ⋅ [a1] ⋅ [1 - a1] @ Suc t |w. w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩}"
      unfolding mem_Collect_eq
    proof (induction x rule: 𝒲.induct, simp)
      case (2 τ i)
      then obtain w where "τ = w ⋅ [a1] ⋅ [1 - a1] @ Suc t" and "w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩"
        by blast
      from hull.prod_cl[OF _ this(2), of "[a1] ⋅ [1 - a1] @ i"] ‹i ≤ t›
      have "[a1] ⋅ [1 - a1] @ i ⋅ w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩"
        unfolding mem_Collect_eq by simp
      thus ?case
        using ‹τ = w ⋅ [a1] ⋅ [1 - a1] @ Suc t› by auto
    qed
  qed
next
  show "{w ⋅ [a1] ⋅ [1 - a1] @ Suc t |w. w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩} ⊆ 𝒲"
  proof
    fix x assume "x ∈ {w ⋅ [a1] ⋅ [1 - a1] @ Suc t |w. w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩}"
    then obtain w where "x = w ⋅ [a1] ⋅ [1 - a1] @ Suc t" and "w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩"
      unfolding mem_Collect_eq by blast
    show "x ∈ 𝒲"
      unfolding ‹x = w ⋅ [a1] ⋅ [1 - a1] @ Suc t›
      by (rule hull.induct[OF ‹w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩›], use 𝒲.intros(1) in force)
        (use 𝒲.intros(2) in force)
  qed
qed

theorem infinite_basis: "𝔅 𝒯 = ({[1-a1]} ∪ 𝒲)"
  using basis_of_hull[of "{[1-a1]} ∪ 𝒲"]
  unfolding 𝒲_gen_T  code.code_is_basis[OF pref_code.code, OF pref_code_𝒲].

end

section Intersection

lemma bin_inter_coin_set_fst: "⟨{x,y}⟩ ∩ ⟨{u,v}⟩ = ((bin_morph_of x y) ∘ fst) ` ℭ (bin_morph_of x y) (bin_morph_of u v)"
  using bin_morph_of_range coin_set_inter_fst by metis

lemma bin_inter_coin_set_snd: "⟨{x,y}⟩ ∩ ⟨{u,v}⟩ = ((bin_morph_of u v) ∘ snd) ` ℭ (bin_morph_of x y) (bin_morph_of u v)"
  using  bin_inter_coin_set_fst unfolding coin_set_eq.

theorem bin_inter_basis: assumes "binary_code x y" and "binary_code u v"
  shows  "𝔅 (⟨{x,y}⟩ ∩ ⟨{u,v}⟩) = ((bin_morph_of u v) ∘ snd) ` ℭm (bin_morph_of x y) (bin_morph_of u v)"
  unfolding bin_inter_coin_set_snd
  using  two_code_morphisms.range_inter_basis_snd(1)[OF two_code_morphisms.intro, OF binary_code.code_morph_of binary_code.code_morph_of, OF assms, folded coin_set_inter_snd] unfolding image_comp.

theorem binary_intersection_code:
  assumes "binary_code x y" and "binary_code u v"
  shows "code 𝔅 (⟨{x,y}⟩ ∩ ⟨{u,v}⟩)"
  using two_code_morphisms.range_inter_code[OF two_code_morphisms.intro[OF binary_code.code_morph_of[OF assms(1)] binary_code.code_morph_of[OF assms(2)]]]
  unfolding bin_morph_of_range.

theorem binary_intersection:
  assumes "binary_code x y" and "binary_code u v"
  obtains
    "𝔅 (⟨{x,y}⟩ ∩ ⟨{u,v}⟩) = {}"
  |
    β where  "𝔅 (⟨{x,y}⟩ ∩ ⟨{u,v}⟩) = {β}"
  |
    β γ where  "𝔅 (⟨{x,y}⟩ ∩ ⟨{u,v}⟩) = {β,γ}"
  |
    β γ δ 𝔱 where "δ ≠ ε" and  "γ ⋅ β ≠ ε" and "hd δ ≠ hd (γ ⋅ β)"
    "𝔅 (⟨{x,y}⟩ ∩ ⟨{u,v}⟩) = {β ⋅ γ} ∪ {β ⋅ (γ ⋅ β)@𝔱 ⋅ w ⋅ δ ⋅ γ | w. w ∈ ⟨{δ ⋅ (γ ⋅ β)@i | i. i ≤ 𝔱}⟩}"
  |
    β γ δ 𝔱 𝔮 where "δ ≠ ε"and  "γ ⋅ β ≠ ε" and "hd δ ≠ hd (γ ⋅ β)" and
    "1 ≤ 𝔮 ∧ 𝔮 ≤ 𝔱" and
    "𝔅 (⟨{x,y}⟩ ∩ ⟨{u,v}⟩) = {β ⋅ γ} ∪ {β ⋅ (γ ⋅ β)@𝔱 ⋅ w ⋅ δ<¯(β ⋅ (γ ⋅ β)@(𝔱-𝔮)) |
                w. w ∈ ⟨{δ ⋅ (γ ⋅ β)@i | i. i ≤ 𝔮 - 1}⟩}"
proof-
  define x' where "x' = (if |bin_lcp u v| ≤ |bin_lcp x y| then x else u)"
  define y' where "y' = (if |bin_lcp u v| ≤ |bin_lcp x y| then y else v)"
  define u' where "u' = (if |bin_lcp u v| ≤ |bin_lcp x y| then u else x)"
  define v' where "v' = (if |bin_lcp u v| ≤ |bin_lcp x y| then v else y)"
  have lcp_le: "|bin_lcp u' v'| ≤ |bin_lcp x' y'|"
    unfolding x'_def y'_def u'_def v'_def by simp
  have int': "⟨{x,y}⟩ ∩ ⟨{u,v}⟩ = ⟨{x',y'}⟩ ∩ ⟨{u',v'}⟩"
    unfolding x'_def y'_def u'_def v'_def using Int_commute by force
  have assms': "binary_code x' y'" "binary_code u' v'"
    using assms unfolding x'_def y'_def u'_def v'_def by simp_all

  define first_morphism ("g ")
    where "first_morphism ≡ bin_morph_of x' y'"
  define second_morphism ("h")
    where "second_morphism ≡ bin_morph_of u' v'"
  note mdefs = first_morphism_def second_morphism_def
  have ranges: "range g = ⟨{x',y'}⟩" "range h = ⟨{u',v'}⟩"
    unfolding mdefs bin_morph_of_range by blast+

  have nemp: "x' ≠ ε" "y' ≠ ε" "u' ≠ ε" "v' ≠ ε"
    using assms' binary_code.non_comm by blast+

  interpret two_binary_code_morphisms g h
    using two_binary_code_morphisms.intro
    unfolding binary_code_morphism_def first_morphism_def second_morphism_def
    using binary_code.code_morph_of assms' by blast

  interpret two_nonerasing_morphisms g h
    using code.two_nonerasing_morphisms_axioms.

  show thesis
  proof (cases)
    assume "ℭm g h = {}" ― ‹simple case: coincidence set is empty›
    have "⟨{x',y'}⟩ ∩ ⟨{u',v'}⟩ = {ε}"
      unfolding bin_inter_coin_set_snd image_comp[symmetric] mdefs[symmetric]
        code.min_coin_gen_snd[symmetric, unfolded ‹ℭm g h = {}›]
      by (simp add: emp_gen_set)
    from that(1)[unfolded int' this]
    show ?thesis
      unfolding emp_basis_iff by simp
  next
    assume "ℭm g h ≠ {}"
    then obtain r1 s1 where "g r1 =m h s1"
      unfolding min_coincidence_set_def by blast
    interpret binary_codes_coincidence g h
    proof
      show "∃r s. g r =m h s"
        using ‹g r1 =m h s1› by blast
      show "|h.bin_code_lcp| ≤ |g.bin_code_lcp|"
        unfolding bin_morph_ofD mdefs using lcp_le.
    qed
    show thesis
    proof (cases)
      assume "ℭm g h = {(r1,s1)}" ― ‹min. coincidence set contains 1 element›
      from that(2)[unfolded int']
      show thesis
        unfolding bin_inter_basis [OF assms', unfolded ‹ℭm g h = {(r1,s1)}›[unfolded mdefs] image_comp[symmetric]] by simp
    next
      assume "ℭm g h ≠ {(r1,s1)}" ― ‹min. coincidence set contains more than 1 element›
      then obtain r2 s2 where "(r2,s2) ∈ ℭm g h" and "(r2,s2) ≠ (r1,s1)"
        using ‹ℭm g h ≠ {}› by auto
      from min_coin_setD[OF this(1)] ‹g r1 =m h s1› this(2)
      interpret binary_codes_coincidence_two_generators g h
        by unfold_locales auto
      write g.marked_version ("gm") and
        h.marked_version ("hm") and
        fst_beginning_block ("p")  and
        snd_beginning_block ("q")  and
        h.bin_code_lcp ("αh") and
        marked.suc_snd ("𝔣")
      show thesis
      proof(cases)
        assume "∀ a. coin_block [a]"
        hence "⋀ a. coin_block [a]" by force
        define β where "β = (h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) 𝔞"
        define γ where "γ = (h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) 𝔟"
        have "range (bin_morph_of x' y') = ⟨{x',y'}⟩"
          using bin_morph_of_range by auto
        from that(3)[ of β γ, unfolded int' β_def γ_def mdefs[symmetric]]
        show thesis
          using inter_basis[unfolded simple_blocks_basis[OF ‹⋀ a. coin_block [a]›] bin_morph_of_range]
          unfolding ranges by blast
      next
        assume "¬ (∀ a. coin_block [a])"
        then obtain a1 where "¬ coin_block [a1]" by blast
        then interpret binary_codes_coincidence_infinite g h a1
          by unfold_locales
        write coincidence_exponent ("t")

        from inter_basis[unfolded ranges infinite_basis bin_morph_of_range, folded Setcompr_eq_image, unfolded mem_Collect_eq]
        have inter:"𝔅 (⟨{x', y'}⟩ ∩ ⟨{u', v'}⟩) = {(h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) x |x. x ∈ {[1 - a1]} ∪ 𝒲}".

        have "q ≤s q ⋅ 𝔣 [1 - a1]"
          using swap_coin_block[unfolded coin_block_def] by blast
        from conjug_eqE[OF rq_suf[OF this]] conjug_emp_emp'[OF this] marked.sucs.h.sing_to_nemp
        obtain q1 q2 k where q21: "𝔣 [1 - a1] = q2 ⋅ q1" and
          q_def: "q = (q1 ⋅ q2)@k ⋅ q1" and "q2 ≠ ε"
          by metis
        have "(h q1 ⋅ h q2) ⋅ (h q1 ⋅ αh) = (h q1 ⋅ αh) ⋅ (hm q2 ⋅ hm q1)"
          unfolding rassoc h.marked_version_conjugates[of "q2 ⋅ q1", unfolded hm.morph h.morph]..
        from conjug_eqE[OF this] h.nemp_to_nemp[OF ‹q2 ≠ ε›]
        obtain β γ k' where bg: "β ⋅ γ = h (q1 ⋅ q2)" and "γ ⋅ β = hm (q2 ⋅ q1)" and
          k': "β ⋅ (γ ⋅ β)@k'  = h q1 ⋅ αh" and "γ ≠ ε"
          unfolding hm.morph h.morph shift_pow by blast
        have bgb_q: "β ⋅ (γ ⋅ β)@(k' + k) = αh ⋅ hm q"
          unfolding add_exps lassoc ‹β ⋅ (γ ⋅ β)@k'  = h q1 ⋅ αh›
          unfolding ‹γ ⋅ β = hm (q2 ⋅ q1)› h.marked_version_conjugates[symmetric]
            rassoc cancel q_def shift_pow unfolding hm.morph hm.pow_morph..
        define δ where "δ = hm (𝔣 [a1])"
        have bg_def: "β ⋅ γ = h ((q ⋅ 𝔣 [1 - a1])<¯q )"
          unfolding bg q_def q21 rassoc shift_pow pow_comm
          unfolding lassoc[of "q1"]
          unfolding rq_triv..
        have bg_def': "(h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) [1-a1] = β ⋅ γ"
          using bg_def by simp
        have gb_def: "γ ⋅ β = hm (𝔣 [1 - a1])"
          unfolding  ‹γ ⋅ β = hm (q2 ⋅ q1)› q21..

        have "γ ⋅ β ≠ ε"
          using ‹γ ≠ ε› by blast
        have "δ ≠ ε"
          unfolding δ_def using hm.nonerasing  marked.sucs.h.sing_to_nemp by blast
        have "hd δ ≠ hd (γ ⋅ β)"
          unfolding δ_def gb_def
          using hm.hd_im_eq_hd_eq marked.sucs.h.bin_marked_sing marked.sucs.h.sing_to_nemp by blast

        have w_decode: "w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩ ⟹  hm (𝔣 w) ∈ ⟨{δ ⋅ (γ ⋅ β) @ i |i. i ≤ t}⟩"
          for w
        proof (induct w rule: hull.induct, unfold marked.sucs.h.emp_to_emp hm.emp_to_emp, fast)
          case (prod_cl w1 w2)
          then obtain i where "w1 = [a1] ⋅ [1-a1]@i" and "i ≤ t" by blast
          with prod_cl.hyps
          show ?case
            unfolding marked.sucs.h.morph marked.sucs.h.pow_morph hm.morph
                      hm.pow_morph ‹w1 = [a1] ⋅ [1-a1]@i› δ_def[symmetric] gb_def[symmetric]
            by blast
        qed

        have w_decode': "w ∈ ⟨{δ ⋅ (γ ⋅ β) @ i |i. i ≤ t}⟩ ⟹ ∃ w'. w' ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩ ∧ hm (𝔣 w') = w" for w
        proof (induct w rule: hull.induct, use marked.sucs.h.emp_to_emp hm.emp_to_emp in force)
          case (prod_cl w1 w2)
          then obtain w' j where  "w' ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩" and "hm (𝔣 w') = w2" and "w1 = δ ⋅ (γ ⋅ β) @ j" and "j ≤ t" by blast
          have "([a1] ⋅ [1 - a1] @ j) ⋅ w' ∈  ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩"
            using ‹w' ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩› ‹j ≤ t› by blast
          moreover have "hm (𝔣 (([a1] ⋅ [1 - a1] @ j) ⋅ w')) = w1 ⋅ w2"
            unfolding marked.sucs.h.morph marked.sucs.h.pow_morph hm.morph hm.pow_morph ‹hm (𝔣 w') = w2›
              δ_def[symmetric] gb_def[symmetric] ‹w1 = δ ⋅ (γ ⋅ β) @ j›..
          ultimately show " ∃w'. w' ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩ ∧ hm (𝔣 w') = w1 ⋅ w2" by blast
        qed

        show thesis
        proof (cases)
          assume "αh ⋅ hm q <s hm (𝔣 ([1-a1]@Suc t))"
          from ssuf_extD[OF this[unfolded bgb_q[symmetric] marked.sucs.h.pow_morph q21 gb_def hm.pow_morph]]
          have "k' + k < Suc t"
            unfolding marked.sucs.h.pow_morph[symmetric] using comp_pows_ssuf by blast
          have "¬ q ≤s 𝔣 ([1-a1]@t)"
            unfolding marked.sucs.h.pow_morph using exp_min.
          hence "t ≤ k"
            unfolding marked.sucs.h.pow_morph q21 q_def shift_pow
            using comp_pows_not_suf by blast
          hence "t = k" and "k' = 0"
            using ‹k' + k < Suc t› by force+

          from bgb_q[folded ‹t = k›, unfolded ‹k' = 0›]
          have "β ⋅ (γ ⋅ β) @ t = αh ⋅ hm q" by simp
          have "q ≤s 𝔣 [1 - a1] @ Suc t"
            unfolding q_def ‹t = k› q21 pow_Suc shift_pow by force

          have "β = h q1 ⋅ αh"
            using ‹β ⋅ (γ ⋅ β)@k'  = h q1 ⋅ αh›[unfolded ‹k' = 0› cow_simps].
          from gb_def[unfolded q21 hm.morph this h.marked_version_conjugates[symmetric]]
          have "γ ⋅ αh = hm q2"
            by force
          from h.marked_version_conjugates[of q2, folded this]
          have "h ((𝔣 [1 - a1] @ Suc t)<¯q) = αh ⋅ γ"
            unfolding q_def ‹t = k› q21 pow_Suc shift_pow rassoc rq_triv by force

          have apply_h0:  "h ((q ⋅ 𝔣 (w ⋅ [a1] ⋅ [1 - a1] @ Suc t))<¯q) = β ⋅ (γ ⋅ β)@t ⋅ hm (𝔣 w) ⋅ δ ⋅ γ" for w
          proof-
            have "β ⋅ (γ ⋅ β)@t ⋅ hm (𝔣 w) ⋅ δ ⋅ γ = αh ⋅ hm (q ⋅ 𝔣 (w ⋅ [a1])) ⋅ γ"
              unfolding hm.morph marked.sucs.h.morph δ_def lassoc cancel_right ‹β ⋅ (γ ⋅ β) @ t = αh ⋅ hm q›..
            also have "... = h (q ⋅ 𝔣 (w ⋅ [a1])) ⋅ h ((𝔣 [1 - a1] @ Suc t)<¯q)"
              unfolding lassoc h.marked_version_conjugates
              unfolding ‹h ((𝔣 [1 - a1] @ Suc t)<¯q) = αh ⋅ γ› rassoc..
            finally show ?thesis
              unfolding h.morph[symmetric] marked.sucs.h.morph marked.sucs.h.pow_morph
                rq_reassoc[OF ‹q ≤s 𝔣 [1 - a1] @ Suc t›, of "q ⋅ 𝔣 w ⋅ 𝔣 [a1]"]
              unfolding rassoc by argo
          qed

          have inf_part_equal:
            "{(h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) (w ⋅ [a1] ⋅ [1 - a1] @ Suc t)
            |w. w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩}
          = {β ⋅ (γ ⋅ β) @ t ⋅ w ⋅ δ ⋅ γ |w. w ∈ ⟨{δ ⋅ (γ ⋅ β) @ i |i. i ≤ t}⟩}" (is "?I = ?E")
          proof
            show "?I ⊆ ?E"
            proof
              fix x assume "x ∈ ?I"
              then obtain w where "x = h ((q ⋅ 𝔣 (w ⋅ [a1] ⋅ [1 - a1] @ Suc t))<¯q )" and
                "w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩"
                unfolding mem_Collect_eq o_apply by blast
              from this(1)[unfolded apply_h0] w_decode[OF this(2)]
              show "x ∈ ?E" by blast
            qed
          next
            show "?E ⊆ ?I"
            proof
              fix x assume "x ∈ ?E"
              then obtain w where x: "x = β ⋅ (γ ⋅ β) @ t ⋅ w ⋅ δ ⋅ γ" and
                " w ∈ ⟨{δ ⋅ (γ ⋅ β) @ i |i. i ≤ t}⟩" by blast
              from w_decode'[OF this(2)]
              obtain w'  where "w' ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩" and "hm (𝔣 w') = w" by blast
              from x[folded this(2), folded apply_h0[of w']] this(1)
              show "x ∈ ?I"
                unfolding o_apply by blast
            qed
          qed
          from that(4)[OF ‹δ ≠ ε› ‹γ ⋅ β ≠ ε› ‹hd δ ≠ hd (γ ⋅ β)›, unfolded int', of t,
              unfolded inter, folded inf_part_equal bg_def', unfolded 𝒲_explicit]
          show thesis
            by blast
        next
          assume "¬ αh ⋅ hm q <s hm (𝔣 ([1-a1]@Suc t))"
          note not_suf = this[unfolded marked.sucs.h.pow_morph q21]
          have "αh ⋅ hm q ≤s (αh ⋅ hm q) ⋅ hm ((q2 ⋅ q1) @ Suc t)"
            unfolding q_def shift_pow rassoc hm.morph[symmetric] pows_comm[of _ k]
            unfolding hm.morph lassoc suf_cancel_conv
            unfolding rassoc hm.morph[symmetric] shift_pow[symmetric]
            unfolding hm.morph lassoc suf_cancel_conv
            unfolding h.marked_version_conjugates by blast
          from ruler[reversed, of "αh ⋅ hm q" _ "hm ((q2 ⋅ q1) @ Suc t)", OF _ triv_suf,
              of "αh ⋅ hm q", OF this]
          have "hm ((q2⋅q1)@Suc t) ≤s αh ⋅ hm q"
            unfolding marked.sucs.h.pow_morph q21 using not_suf by force
          from this[unfolded q_def shift_pow hm.morph, unfolded hm.pow_morph, folded gb_def[unfolded q21], unfolded lassoc,
              folded k'[folded h.marked_version_conjugates], unfolded rassoc add_exps[symmetric]]
          have "Suc t ≤ k' + k"
            using comp_pows_suf'[OF ‹γ ≠ ε›] by blast
          from le_add_diff_inverse2[OF this]
          have split: "β ⋅ (γ ⋅ β) @ (k' + k) = β ⋅ (γ ⋅ β) @ (k' + k - Suc t) ⋅ (γ ⋅ β) @ Suc t"
            unfolding add_exps[symmetric] by argo

          have "αh ⋅ hm q = β ⋅ (γ ⋅ β) @ (k' + k)"
            unfolding q_def shift_pow hm.morph
            unfolding hm.pow_morph gb_def[symmetric, unfolded q21] lassoc k'[folded h.marked_version_conjugates, symmetric]
            unfolding rassoc add_exps..

          have q_suf: "q ≤s 𝔣 ([a1] ⋅ [1 - a1] @ Suc t)"
            unfolding q_suf_conv by blast
          have q_suf': "q ≤s q ⋅ 𝔣 ((w ⋅ [a1]) ⋅ [1 - a1] @ Suc t)" for w
            using suf_ext[OF q_suf, of "q ⋅ 𝔣 w"] unfolding marked.sucs.h.morph rassoc.

          note long = rich_block_suf_snd'[of ε "1-a1", unfolded emp_simps binA_simps, OF coin_exp]

          have delta_suf: "(β ⋅ (γ ⋅ β) @ (k' + k - Suc t)) ≤s δ"
            using long unfolding bgb_q[symmetric] δ_def marked.sucs.h.morph marked.sucs.h.pow_morph q21 hm.morph
            unfolding hm.pow_morph gb_def[unfolded q21,symmetric] split
            unfolding lassoc suf_cancel_conv.

          have apply_h0:  "h ((q ⋅ 𝔣 (w ⋅ [a1] ⋅ [1 - a1] @ Suc t))<¯q)
              = β ⋅ (γ ⋅ β) @ (k' + k) ⋅  hm (𝔣 w) ⋅ δ<¯(β ⋅ (γ ⋅ β) @ (k' + k - Suc t))" for w
            unfolding cancel_right[symmetric, of "h ((q ⋅ 𝔣 (w ⋅ [a1] ⋅ [1 - a1] @ Suc t))<¯q)" _ "(β ⋅ (γ ⋅ β) @ (k' + k - Suc t))"]
            unfolding rassoc rq_suf[OF delta_suf]
            unfolding cancel_right[symmetric, of _ "β ⋅ (γ ⋅ β) @ (k' + k) ⋅ hm (𝔣 w) ⋅ δ" "(γ ⋅ β) @ Suc t"]
            unfolding rassoc add_exps[symmetric] ‹k' + k - Suc t + Suc t = k' + k›  bgb_q[unfolded h.marked_version_conjugates]
            unfolding lassoc h.morph[symmetric]
            unfolding rassoc rq_suf[OF q_suf', unfolded rassoc, of w]
            unfolding h.marked_version_conjugates[symmetric] hm.morph marked.sucs.h.morph
            unfolding lassoc bgb_q unfolding rassoc δ_def gb_def hm.pow_morph marked.sucs.h.pow_morph..

          have inf_part_equal: "{(h ∘ (λx. (q ⋅ x)<¯q ) ∘ 𝔣) (w ⋅ [a1] ⋅ [1 - a1] @ Suc t) |w. w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩}
                = {β ⋅ (γ ⋅ β) @ (k' + k) ⋅ w ⋅ δ<¯(β ⋅ (γ ⋅ β) @ (k' + k - Suc t))  |w. w ∈ ⟨{δ ⋅ (γ ⋅ β) @ i |i. i ≤ t}⟩}" (is "?I = ?E")
          proof
            show "?I ⊆ ?E"
            proof
              fix x assume "x ∈ ?I"
              then obtain w where "x = h ((q ⋅ 𝔣 (w ⋅ [a1] ⋅ [1 - a1] @ Suc t))<¯q )" and
                "w ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩"
                unfolding mem_Collect_eq o_apply apply_h0 by blast

              from this(1)[unfolded apply_h0] w_decode[OF this(2)]
              show "x ∈ ?E" by blast
            qed
          next
            show "?E ⊆ ?I"
            proof
              fix x assume "x ∈ ?E"
              then obtain w where x: "x = β ⋅ (γ ⋅ β) @ (k' + k) ⋅ w ⋅ δ<¯(β ⋅ (γ ⋅ β) @ (k' + k - Suc t))" and
                " w ∈ ⟨{δ ⋅ (γ ⋅ β) @ i |i. i ≤ t}⟩" by blast
              from w_decode'[OF this(2)]
              obtain w'  where "w' ∈ ⟨{[a1] ⋅ [1 - a1] @ i |i. i ≤ t}⟩" and "hm (𝔣 w') = w" by blast
              from x[folded this(2), folded apply_h0[of w']] this(1)
              show "x∈ ?I"
                unfolding o_apply by blast
            qed
          qed
          have "1 ≤ Suc t ∧ Suc t ≤ k' + k" using ‹Suc t ≤ k' + k› by simp
          from that(5)[OF ‹δ ≠ ε› ‹γ ⋅ β ≠ ε› ‹hd δ ≠ hd (γ ⋅ β)› this]
          show thesis
            unfolding diff_Suc_1 unfolding int' unfolding inter 𝒲_explicit bg_def'[symmetric]
            unfolding inf_part_equal[symmetric] by blast
        qed
      qed
    qed
  qed
qed

end