sgl_half_walk

import Definitions.Def_sgl_fold3_walk
import Definitions.Def_sgl_ss_tapes

/-!
# The one-to-two split walk

A run dealt alternately onto two outputs: the first output collects the
cells at even offsets — `⌈run/2⌉` of them — which is how the machine
ceil-halves a tally, the step a logarithm counts.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- One stride: deal the source head to the first free output. -/
def halfStep (src o1 o2 : Fin tapes) (T : Fin tapes → Tape) :
    Fin tapes → Tape :=
  fun i =>
    if (T o1).head = TapeSymbol.blank then
      if i = o1 then Tape.write (T o1) (T src).head
      else if i = src then moveDir HeadMove.right (T src)
      else T i
    else
      if i = o2 then
        moveDir HeadMove.right (Tape.write (T o2) (T src).head)
      else if i = o1 then moveDir HeadMove.right (T o1)
      else if i = src then moveDir HeadMove.right (T src)
      else T i

/-- The stride's action. -/
def halfAction (src o1 o2 : Fin tapes) :
    (Fin tapes → TapeSymbol) → Fin tapes → TapeSymbol × HeadMove :=
  fun symbols i =>
    if symbols o1 = TapeSymbol.blank then
      if i = o1 then (symbols src, HeadMove.stay)
      else if i = src then (symbols i, HeadMove.right)
      else (symbols i, HeadMove.stay)
    else
      if i = o2 then (symbols src, HeadMove.right)
      else if i = o1 then (symbols i, HeadMove.right)
      else if i = src then (symbols i, HeadMove.right)
      else (symbols i, HeadMove.stay)

/-- One round. -/
def halfBody (src o1 o2 : Fin tapes) :=
  (TypedMachine.test (notBlankAt src)).andThen fun v =>
    if v then
      (TypedMachine.act (halfAction src o1 o2)).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) true
    else
      (TypedMachine.act (fun symbols i => (symbols i, HeadMove.stay))).andThen
        fun _ => TypedMachine.halt (tapes := tapes) false

/-- The halving walk. -/
noncomputable def halfWalk (src o1 o2 : Fin tapes) :=
  (halfBody src o1 o2).repeatUntilFalse

theorem halfStep_eq (src o1 o2 : Fin tapes)
    (h12 : o1 ≠ o2) (hs1 : src ≠ o1) (hs2 : src ≠ o2)
    (T : Fin tapes → Tape) :
    applyAction T (halfAction src o1 o2) = halfStep src o1 o2 T := by
  funext i
  simp only [halfStep]
  by_cases hpa : (T o1).head = TapeSymbol.blank
  · rw [if_pos hpa]
    by_cases hio : i = o1
    · subst hio
      simp [applyAction, halfAction, hpa, moveDir, Tape.move]
    · rw [if_neg hio]
      by_cases his : i = src
      · subst his
        simp [applyAction, halfAction, hpa, hio, Tape.write_head_self,
          moveDir]
      · rw [if_neg his]
        simp [applyAction, halfAction, hpa, hio, his,
          Tape.write_head_self, Tape.move]
  · rw [if_neg hpa]
    by_cases hio : i = o2
    · subst hio
      simp [applyAction, halfAction, hpa, moveDir]
    · rw [if_neg hio]
      by_cases hja : i = o1
      · subst hja
        simp [applyAction, halfAction, hpa, hio, Tape.write_head_self,
          moveDir]
      · rw [if_neg hja]
        by_cases his : i = src
        · subst his
          simp [applyAction, halfAction, hpa, hio, hja,
            Tape.write_head_self, moveDir]
        · rw [if_neg his]
          simp [applyAction, halfAction, hpa, hio, hja, his,
            Tape.write_head_self, Tape.move]

/-- The source advances every stride. -/
theorem halfStep_src (src o1 o2 : Fin tapes)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (T : Fin tapes → Tape) :
    (halfStep src o1 o2 T) src = moveDir HeadMove.right (T src) := by
  simp only [halfStep]
  by_cases hpa : (T o1).head = TapeSymbol.blank
  · rw [if_pos hpa, if_neg hs1, if_pos trivial]
  · rw [if_neg hpa, if_neg hs2, if_neg hs1, if_pos trivial]

theorem halfStep_other_one (src o1 o2 : Fin tapes)
    (T : Fin tapes → Tape) (j : Fin tapes)
    (hjs : j ≠ src) (hj1 : j ≠ o1) (hj2 : j ≠ o2) :
    (halfStep src o1 o2 T) j = T j := by
  simp only [halfStep]
  by_cases hpa : (T o1).head = TapeSymbol.blank
  · rw [if_pos hpa, if_neg hj1, if_neg hjs]
  · rw [if_neg hpa, if_neg hj2, if_neg hj1, if_neg hjs]

theorem halfStep_other (src o1 o2 : Fin tapes) :
    ∀ (m : Nat) (T : Fin tapes → Tape) (j : Fin tapes),
      j ≠ src → j ≠ o1 → j ≠ o2 →
      (((halfStep src o1 o2)^[m]) T) j = T j := by
  intro m
  induction m with
  | zero => intro T j _ _ _; rfl
  | succ m ih =>
      intro T j hjs hj1 hj2
      rw [Function.iterate_succ_apply,
        ih (halfStep src o1 o2 T) j hjs hj1 hj2,
        halfStep_other_one src o1 o2 T j hjs hj1 hj2]

/-- Phase 0. -/
theorem halfStep_phase0 (src o1 o2 : Fin tapes)
    (h12 : o1 ≠ o2) (hs1 : src ≠ o1) (hs2 : src ≠ o2)
    (T : Fin tapes → Tape)
    (hpa : (T o1).head = TapeSymbol.blank) :
    (halfStep src o1 o2 T) o1 = Tape.write (T o1) (T src).head ∧
    (halfStep src o1 o2 T) o2 = T o2 := by
  refine ⟨?_, ?_⟩ <;> simp only [halfStep]
  · rw [if_pos hpa, if_pos trivial]
  · rw [if_pos hpa, if_neg (Ne.symm h12), if_neg (Ne.symm hs2)]

/-- Phase 1. -/
theorem halfStep_phase1 (src o1 o2 : Fin tapes)
    (h12 : o1 ≠ o2) (hs1 : src ≠ o1) (hs2 : src ≠ o2)
    (T : Fin tapes → Tape)
    (hpa : (T o1).head ≠ TapeSymbol.blank) :
    (halfStep src o1 o2 T) o1 = moveDir HeadMove.right (T o1) ∧
    (halfStep src o1 o2 T) o2 =
      moveDir HeadMove.right (Tape.write (T o2) (T src).head) := by
  refine ⟨?_, ?_⟩ <;> simp only [halfStep]
  · rw [if_neg hpa, if_neg h12, if_pos trivial]
  · rw [if_neg hpa, if_pos trivial]

set_option maxHeartbeats 2000000 in
/-- **One pair.** -/
theorem halfGroup (src o1 o2 : Fin tapes)
    (h12 : o1 ≠ o2) (hs1 : src ≠ o1) (hs2 : src ≠ o2)
    (T : Fin tapes → Tape)
    (x0 x1 : TapeSymbol) (Ls Rs L1 L2 : List TapeSymbol)
    (hnb0 : x0 ≠ TapeSymbol.blank)
    (hsrc : T src = cellsTape Ls (x0 :: x1 :: Rs))
    (h1 : T o1 = cellsTape L1 [])
    (h2 : T o2 = cellsTape L2 []) :
    (((halfStep src o1 o2)^[2]) T) src =
      cellsTape (x1 :: x0 :: Ls) Rs ∧
    (((halfStep src o1 o2)^[2]) T) o1 = cellsTape (x0 :: L1) [] ∧
    (((halfStep src o1 o2)^[2]) T) o2 = cellsTape (x1 :: L2) [] := by
  have hph0 : (T o1).head = TapeSymbol.blank := by rw [h1]; rfl
  obtain ⟨p01, p02⟩ := halfStep_phase0 src o1 o2 h12 hs1 hs2 T hph0
  have s1src : (halfStep src o1 o2 T) src =
      cellsTape (x0 :: Ls) (x1 :: Rs) := by
    rw [halfStep_src src o1 o2 hs1 hs2, hsrc, cellsTape_moveRight_headD]
    rfl
  have s1o1 : (halfStep src o1 o2 T) o1 = cellsTape L1 [x0] := by
    rw [p01, h1, hsrc, write_cellsTape]
    rfl
  have s1o2 : (halfStep src o1 o2 T) o2 = cellsTape L2 [] := by
    rw [p02, h2]
  set S1 := halfStep src o1 o2 T with hS1
  have hph1 : (S1 o1).head ≠ TapeSymbol.blank := by
    rw [s1o1]
    exact hnb0
  obtain ⟨p11, p12⟩ := halfStep_phase1 src o1 o2 h12 hs1 hs2 S1 hph1
  have hit2 : ((halfStep src o1 o2)^[2]) T = halfStep src o1 o2 S1 := by
    rw [hS1]
    rw [show (2 : Nat) = 1 + 1 from rfl, Function.iterate_succ_apply',
      Function.iterate_one]
  rw [hit2]
  refine ⟨?_, ?_, ?_⟩
  · rw [halfStep_src src o1 o2 hs1 hs2, s1src, cellsTape_moveRight_headD]
    rfl
  · rw [p11, s1o1, cellsTape_moveRight_headD]
    rfl
  · rw [p12, s1src, s1o2, write_cellsTape, cellsTape_moveRight_headD]
    rfl


set_option maxHeartbeats 1000000 in
/-- A round on a marked source. -/
theorem halfBody_mark (src o1 o2 : Fin tapes)
    (h12 : o1 ≠ o2) (hs1 : src ≠ o1) (hs2 : src ≠ o2)
    (T : Fin tapes → Tape)
    (hmark : (T src).head ≠ TapeSymbol.blank) :
    HaltsExactly (halfBody src o1 o2)
      ((halfBody src o1 o2).startCfg T) (1 + 1 + (1 + 1 + 0)) true ∧
    (((halfBody src o1 o2).step^[1 + 1 + (1 + 1 + 0)])
      ((halfBody src o1 o2).startCfg T)).tape = halfStep src o1 o2 T := by
  have htest := TypedMachine.test_spec (notBlankAt src) T
  rw [notBlankAt_true src T hmark] at htest
  have htestt : (((TypedMachine.test (notBlankAt src)).step^[1])
      ((TypedMachine.test (notBlankAt src)).startCfg T)).tape = T := by
    rw [Function.iterate_one]
    funext j
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  have hact := TypedMachine.act_spec (halfAction src o1 o2) T
  have hactt : (((TypedMachine.act (halfAction src o1 o2)).step^[1])
      ((TypedMachine.act (halfAction src o1 o2)).startCfg T)).tape =
      halfStep src o1 o2 T := by
    rw [Function.iterate_one, ← halfStep_eq src o1 o2 h12 hs1 hs2]
    funext j
    simp [TypedMachine.step, TypedMachine.act, TypedMachine.startCfg,
      applyAction]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) true
    ((TypedMachine.halt (tapes := tapes) true).startCfg
      (halfStep src o1 o2 T))
  have hinner := chainStepC hact hactt hhalt
  have hmain := chainStepD
    (M₂ := fun v =>
      if v then
        (TypedMachine.act (halfAction src o1 o2)).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.act (fun symbols i =>
          (symbols i, HeadMove.stay))).andThen
          fun _ => TypedMachine.halt (tapes := tapes) false)
    htest htestt (by simpa using hinner.1)
  refine ⟨hmain.1, ?_⟩
  have hfin := hmain.2
  have hfin' : ((halfBody src o1 o2).step^[1 + 1 + (1 + 1 + 0)])
      ((halfBody src o1 o2).startCfg T) = _ := hfin
  rw [hfin']
  show (TypedConfiguration.inRight true
    ((((TypedMachine.act (halfAction src o1 o2)).andThen fun _ =>
      TypedMachine.halt (tapes := tapes) true).step^[1 + 1 + 0])
      (((TypedMachine.act (halfAction src o1 o2)).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) true).startCfg T))).tape =
    halfStep src o1 o2 T
  have hi := hinner.2
  rw [hi]
  show ((TypedMachine.halt (tapes := tapes) true).step^[0]
    ((TypedMachine.halt (tapes := tapes) true).startCfg
      (halfStep src o1 o2 T))).tape = halfStep src o1 o2 T
  rfl

set_option maxHeartbeats 1000000 in
/-- A round on a blank source. -/
theorem halfBody_blank (src o1 o2 : Fin tapes)
    (T : Fin tapes → Tape)
    (hblank : (T src).head = TapeSymbol.blank) :
    HaltsExactly (halfBody src o1 o2)
      ((halfBody src o1 o2).startCfg T) (1 + 1 + (1 + 1 + 0)) false ∧
    (((halfBody src o1 o2).step^[1 + 1 + (1 + 1 + 0)])
      ((halfBody src o1 o2).startCfg T)).tape = T := by
  have htest := TypedMachine.test_spec (notBlankAt src) T
  rw [notBlankAt_false src T hblank] at htest
  have htestt : (((TypedMachine.test (notBlankAt src)).step^[1])
      ((TypedMachine.test (notBlankAt src)).startCfg T)).tape = T := by
    rw [Function.iterate_one]
    funext j
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  have hact := TypedMachine.act_spec
    (fun symbols i => (symbols i, HeadMove.stay)) T
  have hactt : (((TypedMachine.act (fun symbols i =>
      (symbols i, HeadMove.stay))).step^[1])
      ((TypedMachine.act (fun symbols i =>
        (symbols i, HeadMove.stay))).startCfg T)).tape = T := by
    rw [Function.iterate_one]
    funext j
    simp [TypedMachine.step, TypedMachine.act, TypedMachine.startCfg,
      applyAction, Tape.write_head_self, Tape.move]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) false
    ((TypedMachine.halt (tapes := tapes) false).startCfg T)
  have hinner := chainStepC hact hactt hhalt
  have hmain := chainStepD
    (M₂ := fun v =>
      if v then
        (TypedMachine.act (halfAction src o1 o2)).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.act (fun symbols i =>
          (symbols i, HeadMove.stay))).andThen
          fun _ => TypedMachine.halt (tapes := tapes) false)
    htest htestt (by simpa using hinner.1)
  refine ⟨hmain.1, ?_⟩
  have hfin := hmain.2
  have hfin' : ((halfBody src o1 o2).step^[1 + 1 + (1 + 1 + 0)])
      ((halfBody src o1 o2).startCfg T) = _ := hfin
  rw [hfin']
  show (TypedConfiguration.inRight false
    ((((TypedMachine.act (fun symbols i =>
      (symbols i, HeadMove.stay))).andThen fun _ =>
      TypedMachine.halt (tapes := tapes) false).step^[1 + 1 + 0])
      (((TypedMachine.act (fun symbols i =>
        (symbols i, HeadMove.stay))).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) false).startCfg T))).tape = T
  have hi := hinner.2
  rw [hi]
  show ((TypedMachine.halt (tapes := tapes) false).step^[0]
    ((TypedMachine.halt (tapes := tapes) false).startCfg T)).tape = T
  rfl

set_option maxHeartbeats 4000000 in
/-- **The halving walk.** -/
theorem halfWalk_spec (src o1 o2 : Fin tapes)
    (h12 : o1 ≠ o2) (hs1 : src ≠ o1) (hs2 : src ≠ o2)
    (m : Nat) (T : Fin tapes → Tape)
    (hmarks : ∀ r, r < m →
      ((((halfStep src o1 o2)^[r]) T) src).head ≠ TapeSymbol.blank)
    (hexit : ((((halfStep src o1 o2)^[m]) T) src).head =
      TapeSymbol.blank) :
    HaltsExactly (halfWalk src o1 o2)
      ((halfWalk src o1 o2).startCfg T) (m * 5 + 4) false ∧
    (((halfWalk src o1 o2).step^[m * 5 + 4])
      ((halfWalk src o1 o2).startCfg T)).tape =
      ((halfStep src o1 o2)^[m]) T := by
  classical
  set body := halfBody src o1 o2 with hbody
  set cfg : Nat → TypedConfiguration tapes _ :=
    fun r => body.startCfg (((halfStep src o1 o2)^[r]) T) with hcfg
  have hround : ∀ r, r < m →
      HaltsExactly body (cfg r) 4 true ∧
        cfg (r + 1) = ⟨body.start, ((body.step^[4]) (cfg r)).tape⟩ := by
    intro r hr
    obtain ⟨hh, ht⟩ := halfBody_mark src o1 o2 h12 hs1 hs2
      (((halfStep src o1 o2)^[r]) T) (hmarks r hr)
    have hh4 : HaltsExactly body (cfg r) 4 true := by
      rw [hcfg, hbody]; simpa using hh
    have ht4 : ((body.step^[4]) (cfg r)).tape =
        ((halfStep src o1 o2)^[r + 1]) T := by
      rw [hcfg, hbody]
      rw [show (4 : Nat) = 1 + 1 + (1 + 1 + 0) from rfl]
      rw [ht, Function.iterate_succ_apply']
    refine ⟨hh4, ?_⟩
    show body.startCfg (((halfStep src o1 o2)^[r + 1]) T) = _
    rw [← ht4]
    rfl
  have hexitr : HaltsExactly body (cfg m) 4 false := by
    have := (halfBody_blank src o1 o2
      (((halfStep src o1 o2)^[m]) T) hexit).1
    rw [hcfg, hbody]; simpa using this
  have hspec := TypedMachine.repeatUntilFalse_spec body cfg (fun _ => 4) m 4
    hround hexitr
  have hcost : loopCost (fun _ => 4) m + 4 = m * 5 + 4 := by
    rw [loopCost_const]
  rw [hcost] at hspec
  have hrun := TypedMachine.repeatUntilFalse_rounds body cfg (fun _ => 4) m
    hround
  rw [loopCost_const] at hrun
  refine ⟨by rw [hcfg] at hspec; exact hspec, ?_⟩
  have hstart : (halfWalk src o1 o2).startCfg T = cfg 0 := by
    rw [hcfg]; rfl
  rw [hstart, show m * 5 + 4 = 4 + m * (4 + 1) by omega,
    Function.iterate_add_apply]
  show ((halfWalk src o1 o2).step^[4]
    (((halfWalk src o1 o2).step^[m * (4 + 1)]) (cfg 0))).tape = _
  rw [show (halfWalk src o1 o2) = body.repeatUntilFalse from rfl, hrun]
  have htp : ((body.repeatUntilFalse.step^[4]) (cfg m)).tape =
      ((body.step^[4]) (cfg m)).tape := by
    rw [body.repeatUntilFalse_iterate_fresh (cfg m) 4 hexitr.fresh]
  rw [htp, hcfg, hbody]
  exact (halfBody_blank src o1 o2
    (((halfStep src o1 o2)^[m]) T) hexit).2

set_option maxHeartbeats 4000000 in
/-- **Pairs, accumulated: the outputs collect the alternating halves.** -/
theorem half_iterate (src o1 o2 : Fin tapes)
    (h12 : o1 ≠ o2) (hs1 : src ≠ o1) (hs2 : src ≠ o2) :
    ∀ (t : Nat) (cs : List TapeSymbol) (T : Fin tapes → Tape)
      (Ls Rs L1 L2 : List TapeSymbol),
      cs.length = 2 * t →
      (∀ x ∈ cs, x ≠ TapeSymbol.blank) →
      T src = cellsTape Ls (cs ++ Rs) →
      T o1 = cellsTape L1 [] → T o2 = cellsTape L2 [] →
      (((halfStep src o1 o2)^[2 * t]) T) src =
        cellsTape (cs.reverse ++ Ls) Rs ∧
      (∃ M1, (((halfStep src o1 o2)^[2 * t]) T) o1 =
        cellsTape M1 [] ∧ M1.length = t + L1.length) ∧
      (∃ M2, (((halfStep src o1 o2)^[2 * t]) T) o2 =
        cellsTape M2 [] ∧ M2.length = t + L2.length ∧
        (∀ x ∈ M2, x ∈ cs ∨ x ∈ L2)) ∧
      (∃ M1, (((halfStep src o1 o2)^[2 * t]) T) o1 =
        cellsTape M1 [] ∧ (∀ x ∈ M1, x ∈ cs ∨ x ∈ L1)) := by
  intro t
  induction t with
  | zero =>
      intro cs T Ls Rs L1 L2 hlen hnb hsrc h1 h2
      have : cs = [] := List.length_eq_zero_iff.mp (by simpa using hlen)
      subst this
      refine ⟨by simpa using hsrc, ⟨L1, h1, by simp⟩,
        ⟨L2, h2, by simp, fun x hx => Or.inr hx⟩,
        ⟨L1, h1, fun x hx => Or.inr hx⟩⟩
  | succ t ih =>
      intro cs T Ls Rs L1 L2 hlen hnb hsrc h1 h2
      rcases cs with _ | ⟨x0, _ | ⟨x1, cs'⟩⟩
      · simp at hlen
      · simp at hlen; omega
      · have hlen' : cs'.length = 2 * t := by simp at hlen; omega
        obtain ⟨ga, g1, g2⟩ := halfGroup src o1 o2 h12 hs1 hs2 T x0 x1
          Ls (cs' ++ Rs) L1 L2 (hnb x0 (by simp))
          (by rw [hsrc]; rfl) h1 h2
        obtain ⟨ka, ⟨M1, k1, hM1len⟩, ⟨M2, k2, hM2len, hM2mem⟩,
          ⟨M1', k1', hM1mem⟩⟩ := ih cs'
          (((halfStep src o1 o2)^[2]) T)
          (x1 :: x0 :: Ls) Rs (x0 :: L1) (x1 :: L2)
          hlen' (fun x hx => hnb x (by simp [hx])) ga g1 g2
        have hsplit : ((halfStep src o1 o2)^[2 * (t + 1)]) T =
            ((halfStep src o1 o2)^[2 * t])
              (((halfStep src o1 o2)^[2]) T) := by
          rw [show 2 * (t + 1) = 2 * t + 2 by ring,
            Function.iterate_add_apply]
        rw [hsplit]
        refine ⟨by rw [ka]; simp, ⟨M1, k1, by simp at hM1len ⊢; omega⟩,
          ⟨M2, k2, by simp at hM2len ⊢; omega, ?_⟩, ⟨M1', k1', ?_⟩⟩
        · intro x hx
          rcases hM2mem x hx with h | h
          · exact Or.inl (by simp [h])
          · rcases List.mem_cons.mp h with h' | h'
            · exact Or.inl (by simp [h'])
            · exact Or.inr h'
        · intro x hx
          rcases hM1mem x hx with h | h
          · exact Or.inl (by simp [h])
          · rcases List.mem_cons.mp h with h' | h'
            · exact Or.inl (by simp [h'])
            · exact Or.inr h'


/-- The source's evolution is a plain rightward walk. -/
theorem half_src_iter (src o1 o2 : Fin tapes)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) :
    ∀ (r : Nat) (T : Fin tapes → Tape),
      (((halfStep src o1 o2)^[r]) T) src =
        ((Tape.move · HeadMove.right)^[r]) (T src) := by
  intro r
  induction r with
  | zero => intro T; rfl
  | succ r ih =>
      intro T
      rw [Function.iterate_succ_apply, Function.iterate_succ_apply,
        ih (halfStep src o1 o2 T), halfStep_src src o1 o2 hs1 hs2 T]
      rfl

/-- The marks hypothesis, for any blank-headed tail. -/
theorem half_marks (src o1 o2 : Fin tapes)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2)
    (cs Ls Rs : List TapeSymbol) (T : Fin tapes → Tape)
    (hnb : ∀ x ∈ cs, x ≠ TapeSymbol.blank)
    (hRs : Rs.headD TapeSymbol.blank = TapeSymbol.blank)
    (hsrc : T src = cellsTape Ls (cs ++ Rs)) :
    (∀ r, r < cs.length →
      ((((halfStep src o1 o2)^[r]) T) src).head ≠ TapeSymbol.blank) ∧
    ((((halfStep src o1 o2)^[cs.length]) T) src).head =
      TapeSymbol.blank := by
  have hev := half_src_iter src o1 o2 hs1 hs2
  constructor
  · intro r hr
    rw [hev r T, hsrc]
    obtain ⟨L', hL'⟩ := moveRight_iterate_exists r Ls (cs ++ Rs)
    rw [hL']
    rw [List.drop_append_of_le_length (by omega)]
    have hlen : (cs.drop r).length = cs.length - r := List.length_drop
    cases hcons : cs.drop r with
    | nil => rw [hcons] at hlen; simp at hlen; omega
    | cons hd tl =>
        show ((hd :: tl ++ Rs).headD TapeSymbol.blank) ≠ TapeSymbol.blank
        have hmem : hd ∈ cs := by
          have : hd ∈ cs.drop r := by rw [hcons]; simp
          exact List.mem_of_mem_drop this
        exact hnb hd hmem
  · rw [hev cs.length T, hsrc]
    obtain ⟨L', hL'⟩ := moveRight_iterate_exists cs.length Ls (cs ++ Rs)
    rw [hL']
    rw [List.drop_append_of_le_length (by omega), List.drop_length]
    show Rs.headD TapeSymbol.blank = TapeSymbol.blank
    exact hRs

/-- A run of marks absorbs a following mark. -/
theorem replicate_absorb (n : Nat) (l : List TapeSymbol) :
    List.replicate n (TapeSymbol.bit true) ++ TapeSymbol.bit true :: l =
      List.replicate (n + 1) (TapeSymbol.bit true) ++ l := by
  rw [List.replicate_succ' (n := n), List.append_assoc]
  rfl

/-- **Mark tallies, dealt in pairs.** -/
theorem half_iterate_marks (src o1 o2 : Fin tapes)
    (h12 : o1 ≠ o2) (hs1 : src ≠ o1) (hs2 : src ≠ o2) :
    ∀ (t : Nat) (T : Fin tapes → Tape) (Ls Rs L1 L2 : List TapeSymbol),
      T src = cellsTape Ls
        (List.replicate (2 * t) (TapeSymbol.bit true) ++ Rs) →
      T o1 = cellsTape L1 [] → T o2 = cellsTape L2 [] →
      (((halfStep src o1 o2)^[2 * t]) T) src =
        cellsTape (List.replicate (2 * t) (TapeSymbol.bit true) ++ Ls)
          Rs ∧
      (((halfStep src o1 o2)^[2 * t]) T) o1 =
        cellsTape (List.replicate t (TapeSymbol.bit true) ++ L1) [] ∧
      (((halfStep src o1 o2)^[2 * t]) T) o2 =
        cellsTape (List.replicate t (TapeSymbol.bit true) ++ L2) [] := by
  intro t
  induction t with
  | zero =>
      intro T Ls Rs L1 L2 hsrc h1 h2
      simp only [Nat.mul_zero, Function.iterate_zero_apply,
        List.replicate_zero, List.nil_append]
      exact ⟨by simpa using hsrc, h1, h2⟩
  | succ t ih =>
      intro T Ls Rs L1 L2 hsrc h1 h2
      have hsrc' : T src = cellsTape Ls
          (TapeSymbol.bit true :: TapeSymbol.bit true ::
            (List.replicate (2 * t) (TapeSymbol.bit true) ++ Rs)) := by
        rw [hsrc]
        congr 1
      obtain ⟨ga, g1, g2⟩ := halfGroup src o1 o2 h12 hs1 hs2 T
        (TapeSymbol.bit true) (TapeSymbol.bit true) Ls
        (List.replicate (2 * t) (TapeSymbol.bit true) ++ Rs) L1 L2
        (by simp) hsrc' h1 h2
      obtain ⟨ka, k1, k2⟩ := ih (((halfStep src o1 o2)^[2]) T)
        (TapeSymbol.bit true :: TapeSymbol.bit true :: Ls) Rs
        (TapeSymbol.bit true :: L1) (TapeSymbol.bit true :: L2)
        ga g1 g2
      have hsplit : ((halfStep src o1 o2)^[2 * (t + 1)]) T =
          ((halfStep src o1 o2)^[2 * t])
            (((halfStep src o1 o2)^[2]) T) := by
        rw [show 2 * (t + 1) = 2 * t + 2 by ring,
          Function.iterate_add_apply]
      rw [hsplit]
      refine ⟨?_, ?_, ?_⟩
      · rw [ka]
        show cellsTape _ Rs = cellsTape _ Rs
        congr 1
        rw [replicate_absorb, replicate_absorb,
          show 2 * t + 1 + 1 = 2 * (t + 1) by ring]
      · rw [k1]
        show cellsTape _ [] = cellsTape _ []
        congr 1
        rw [replicate_absorb]
      · rw [k2]
        show cellsTape _ [] = cellsTape _ []
        congr 1
        rw [replicate_absorb]

end SipserGacsLautemann