sgl_split_walk

import Definitions.Def_sgl_fold3_walk
import Definitions.Def_sgl_ss_tapes

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

One tape's run is dealt round-robin onto three outputs — the same
first-blank dispatch as the cascade's fold, with a single source.  Output
`k` collects every third cell; in particular the third output's run has
exactly `⌊run/3⌋` cells, which is how the machine divides a tally by three.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- One stride: deal the source head to the first free output. -/
def splitStep (src o1 o2 o3 : 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 (T o2).head = TapeSymbol.blank then
      if i = o2 then Tape.write (T o2) (T src).head
      else if i = src then moveDir HeadMove.right (T src)
      else T i
    else
      if i = o3 then
        moveDir HeadMove.right (Tape.write (T o3) (T src).head)
      else if i = o1 then moveDir HeadMove.right (T o1)
      else if i = o2 then moveDir HeadMove.right (T o2)
      else if i = src then moveDir HeadMove.right (T src)
      else T i

/-- The stride's action. -/
def splitAction (src o1 o2 o3 : 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 symbols o2 = TapeSymbol.blank then
      if i = o2 then (symbols src, HeadMove.stay)
      else if i = src then (symbols i, HeadMove.right)
      else (symbols i, HeadMove.stay)
    else
      if i = o3 then (symbols src, HeadMove.right)
      else if i = o1 then (symbols i, HeadMove.right)
      else if i = o2 then (symbols i, HeadMove.right)
      else if i = src then (symbols i, HeadMove.right)
      else (symbols i, HeadMove.stay)

/-- One round of the split. -/
def splitBody (src o1 o2 o3 : Fin tapes) :=
  (TypedMachine.test (notBlankAt src)).andThen fun v =>
    if v then
      (TypedMachine.act (splitAction src o1 o2 o3)).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 split: one stride per source mark. -/
noncomputable def splitWalk (src o1 o2 o3 : Fin tapes) :=
  (splitBody src o1 o2 o3).repeatUntilFalse

theorem splitStep_eq (src o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3)
    (T : Fin tapes → Tape) :
    applyAction T (splitAction src o1 o2 o3) =
      splitStep src o1 o2 o3 T := by
  funext i
  simp only [splitStep]
  by_cases hpa : (T o1).head = TapeSymbol.blank
  · rw [if_pos hpa]
    by_cases hio : i = o1
    · subst hio
      simp [applyAction, splitAction, hpa, moveDir, Tape.move]
    · rw [if_neg hio]
      by_cases his : i = src
      · subst his
        simp [applyAction, splitAction, hpa, hio, Tape.write_head_self,
          moveDir]
      · rw [if_neg his]
        simp [applyAction, splitAction, hpa, hio, his,
          Tape.write_head_self, Tape.move]
  · rw [if_neg hpa]
    by_cases hpb : (T o2).head = TapeSymbol.blank
    · rw [if_pos hpb]
      by_cases hio : i = o2
      · subst hio
        simp [applyAction, splitAction, hpa, hpb, moveDir, Tape.move]
      · rw [if_neg hio]
        by_cases his : i = src
        · subst his
          simp [applyAction, splitAction, hpa, hpb, hio,
            Tape.write_head_self, moveDir]
        · rw [if_neg his]
          simp [applyAction, splitAction, hpa, hpb, hio, his,
            Tape.write_head_self, Tape.move]
    · rw [if_neg hpb]
      by_cases hio : i = o3
      · subst hio
        simp [applyAction, splitAction, hpa, hpb, moveDir]
      · rw [if_neg hio]
        by_cases hja : i = o1
        · subst hja
          simp [applyAction, splitAction, hpa, hpb, hio,
            Tape.write_head_self, moveDir]
        · rw [if_neg hja]
          by_cases hjb : i = o2
          · subst hjb
            simp [applyAction, splitAction, hpa, hpb, hio, hja,
              Tape.write_head_self, moveDir]
          · rw [if_neg hjb]
            by_cases his : i = src
            · subst his
              simp [applyAction, splitAction, hpa, hpb, hio, hja, hjb,
                Tape.write_head_self, moveDir]
            · rw [if_neg his]
              simp [applyAction, splitAction, hpa, hpb, hio, hja, hjb,
                his, Tape.write_head_self, Tape.move]


set_option maxHeartbeats 1000000 in
/-- A round on a marked source. -/
theorem splitBody_mark (src o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3)
    (T : Fin tapes → Tape)
    (hmark : (T src).head ≠ TapeSymbol.blank) :
    HaltsExactly (splitBody src o1 o2 o3)
      ((splitBody src o1 o2 o3).startCfg T) (1 + 1 + (1 + 1 + 0)) true ∧
    (((splitBody src o1 o2 o3).step^[1 + 1 + (1 + 1 + 0)])
      ((splitBody src o1 o2 o3).startCfg T)).tape =
      splitStep src o1 o2 o3 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 (splitAction src o1 o2 o3) T
  have hactt : (((TypedMachine.act (splitAction src o1 o2 o3)).step^[1])
      ((TypedMachine.act (splitAction src o1 o2 o3)).startCfg T)).tape =
      splitStep src o1 o2 o3 T := by
    rw [Function.iterate_one, ← splitStep_eq src o1 o2 o3 h12 h13 h23 hs1
      hs2 hs3]
    funext j
    simp [TypedMachine.step, TypedMachine.act, TypedMachine.startCfg,
      applyAction]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) true
    ((TypedMachine.halt (tapes := tapes) true).startCfg
      (splitStep src o1 o2 o3 T))
  have hinner := chainStepC hact hactt hhalt
  have hmain := chainStepD
    (M₂ := fun v =>
      if v then
        (TypedMachine.act (splitAction src o1 o2 o3)).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' : ((splitBody src o1 o2 o3).step^[1 + 1 + (1 + 1 + 0)])
      ((splitBody src o1 o2 o3).startCfg T) = _ := hfin
  rw [hfin']
  show (TypedConfiguration.inRight true
    ((((TypedMachine.act (splitAction src o1 o2 o3)).andThen fun _ =>
      TypedMachine.halt (tapes := tapes) true).step^[1 + 1 + 0])
      (((TypedMachine.act (splitAction src o1 o2 o3)).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) true).startCfg T))).tape =
    splitStep src o1 o2 o3 T
  have hi := hinner.2
  rw [hi]
  show ((TypedMachine.halt (tapes := tapes) true).step^[0]
    ((TypedMachine.halt (tapes := tapes) true).startCfg
      (splitStep src o1 o2 o3 T))).tape = splitStep src o1 o2 o3 T
  rfl

set_option maxHeartbeats 1000000 in
/-- A round on a blank source. -/
theorem splitBody_blank (src o1 o2 o3 : Fin tapes)
    (T : Fin tapes → Tape)
    (hblank : (T src).head = TapeSymbol.blank) :
    HaltsExactly (splitBody src o1 o2 o3)
      ((splitBody src o1 o2 o3).startCfg T) (1 + 1 + (1 + 1 + 0)) false ∧
    (((splitBody src o1 o2 o3).step^[1 + 1 + (1 + 1 + 0)])
      ((splitBody src o1 o2 o3).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 (splitAction src o1 o2 o3)).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' : ((splitBody src o1 o2 o3).step^[1 + 1 + (1 + 1 + 0)])
      ((splitBody src o1 o2 o3).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 split walk.** -/
theorem splitWalk_spec (src o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3)
    (m : Nat) (T : Fin tapes → Tape)
    (hmarks : ∀ r, r < m →
      ((((splitStep src o1 o2 o3)^[r]) T) src).head ≠ TapeSymbol.blank)
    (hexit : ((((splitStep src o1 o2 o3)^[m]) T) src).head =
      TapeSymbol.blank) :
    HaltsExactly (splitWalk src o1 o2 o3)
      ((splitWalk src o1 o2 o3).startCfg T) (m * 5 + 4) false ∧
    (((splitWalk src o1 o2 o3).step^[m * 5 + 4])
      ((splitWalk src o1 o2 o3).startCfg T)).tape =
      ((splitStep src o1 o2 o3)^[m]) T := by
  classical
  set body := splitBody src o1 o2 o3 with hbody
  set cfg : Nat → TypedConfiguration tapes _ :=
    fun r => body.startCfg (((splitStep src o1 o2 o3)^[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⟩ := splitBody_mark src o1 o2 o3 h12 h13 h23 hs1 hs2 hs3
      (((splitStep src o1 o2 o3)^[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 =
        ((splitStep src o1 o2 o3)^[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 (((splitStep src o1 o2 o3)^[r + 1]) T) = _
    rw [← ht4]
    rfl
  have hexitr : HaltsExactly body (cfg m) 4 false := by
    have := (splitBody_blank src o1 o2 o3
      (((splitStep src o1 o2 o3)^[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 : (splitWalk src o1 o2 o3).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 ((splitWalk src o1 o2 o3).step^[4]
    (((splitWalk src o1 o2 o3).step^[m * (4 + 1)]) (cfg 0))).tape = _
  rw [show (splitWalk src o1 o2 o3) = 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 (splitBody_blank src o1 o2 o3
    (((splitStep src o1 o2 o3)^[m]) T) hexit).2


/-! ## Strides, phase by phase -/

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

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

theorem splitStep_other (src o1 o2 o3 : Fin tapes) :
    ∀ (m : Nat) (T : Fin tapes → Tape) (j : Fin tapes),
      j ≠ src → j ≠ o1 → j ≠ o2 → j ≠ o3 →
      (((splitStep src o1 o2 o3)^[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 hj3
      rw [Function.iterate_succ_apply,
        ih (splitStep src o1 o2 o3 T) j hjs hj1 hj2 hj3,
        splitStep_other_one src o1 o2 o3 T j hjs hj1 hj2 hj3]

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

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

/-- Phase 2. -/
theorem splitStep_phase2 (src o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3)
    (T : Fin tapes → Tape)
    (hpa : (T o1).head ≠ TapeSymbol.blank)
    (hpb : (T o2).head ≠ TapeSymbol.blank) :
    (splitStep src o1 o2 o3 T) o1 = moveDir HeadMove.right (T o1) ∧
    (splitStep src o1 o2 o3 T) o2 = moveDir HeadMove.right (T o2) ∧
    (splitStep src o1 o2 o3 T) o3 =
      moveDir HeadMove.right (Tape.write (T o3) (T src).head) := by
  refine ⟨?_, ?_, ?_⟩ <;> simp only [splitStep]
  · rw [if_neg hpa, if_neg hpb, if_neg h13, if_pos trivial]
  · rw [if_neg hpa, if_neg hpb, if_neg h23, if_neg (Ne.symm h12),
      if_pos trivial]
  · rw [if_neg hpa, if_neg hpb, if_pos trivial]

set_option maxHeartbeats 2000000 in
/-- **One group of the split.** -/
theorem splitGroup (src o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3)
    (T : Fin tapes → Tape)
    (x0 x1 x2 : TapeSymbol) (Ls Rs L1 L2 L3 : List TapeSymbol)
    (hnb0 : x0 ≠ TapeSymbol.blank) (hnb1 : x1 ≠ TapeSymbol.blank)
    (hsrc : T src = cellsTape Ls (x0 :: x1 :: x2 :: Rs))
    (h1 : T o1 = cellsTape L1 [])
    (h2 : T o2 = cellsTape L2 [])
    (h3 : T o3 = cellsTape L3 []) :
    (((splitStep src o1 o2 o3)^[3]) T) src =
      cellsTape (x2 :: x1 :: x0 :: Ls) Rs ∧
    (((splitStep src o1 o2 o3)^[3]) T) o1 = cellsTape (x0 :: L1) [] ∧
    (((splitStep src o1 o2 o3)^[3]) T) o2 = cellsTape (x1 :: L2) [] ∧
    (((splitStep src o1 o2 o3)^[3]) T) o3 = cellsTape (x2 :: L3) [] := by
  -- stride 1: phase 0
  have hph0 : (T o1).head = TapeSymbol.blank := by rw [h1]; rfl
  obtain ⟨p01, p02, p03⟩ := splitStep_phase0 src o1 o2 o3 h12 h13 h23 hs1
    hs2 hs3 T hph0
  have s1src : (splitStep src o1 o2 o3 T) src =
      cellsTape (x0 :: Ls) (x1 :: x2 :: Rs) := by
    rw [splitStep_src src o1 o2 o3 hs1 hs2 hs3, hsrc,
      cellsTape_moveRight_headD]
    rfl
  have s1o1 : (splitStep src o1 o2 o3 T) o1 = cellsTape L1 [x0] := by
    rw [p01, h1, hsrc, write_cellsTape]
    rfl
  have s1o2 : (splitStep src o1 o2 o3 T) o2 = cellsTape L2 [] := by
    rw [p02, h2]
  have s1o3 : (splitStep src o1 o2 o3 T) o3 = cellsTape L3 [] := by
    rw [p03, h3]
  set S1 := splitStep src o1 o2 o3 T with hS1
  -- stride 2: phase 1
  have hph1a : (S1 o1).head ≠ TapeSymbol.blank := by
    rw [s1o1]
    exact hnb0
  have hph1b : (S1 o2).head = TapeSymbol.blank := by
    rw [s1o2]; rfl
  obtain ⟨p11, p12, p13⟩ := splitStep_phase1 src o1 o2 o3 h12 h13 h23 hs1
    hs2 hs3 S1 hph1a hph1b
  have s2src : (splitStep src o1 o2 o3 S1) src =
      cellsTape (x1 :: x0 :: Ls) (x2 :: Rs) := by
    rw [splitStep_src src o1 o2 o3 hs1 hs2 hs3, s1src,
      cellsTape_moveRight_headD]
    rfl
  have s2o1 : (splitStep src o1 o2 o3 S1) o1 = cellsTape L1 [x0] := by
    rw [p11, s1o1]
  have s2o2 : (splitStep src o1 o2 o3 S1) o2 = cellsTape L2 [x1] := by
    rw [p12, s1o2, s1src, write_cellsTape]
    rfl
  have s2o3 : (splitStep src o1 o2 o3 S1) o3 = cellsTape L3 [] := by
    rw [p13, s1o3]
  set S2 := splitStep src o1 o2 o3 S1 with hS2
  -- stride 3: phase 2
  have hph2a : (S2 o1).head ≠ TapeSymbol.blank := by
    rw [s2o1]
    exact hnb0
  have hph2b : (S2 o2).head ≠ TapeSymbol.blank := by
    rw [s2o2]
    exact hnb1
  obtain ⟨p21, p22, p23⟩ := splitStep_phase2 src o1 o2 o3 h12 h13 h23 hs1
    hs2 hs3 S2 hph2a hph2b
  have hit3 : ((splitStep src o1 o2 o3)^[3]) T =
      splitStep src o1 o2 o3 S2 := by
    rw [hS2, hS1]
    rw [show (3 : Nat) = 2 + 1 from rfl, Function.iterate_succ_apply',
      show (2 : Nat) = 1 + 1 from rfl, Function.iterate_succ_apply',
      Function.iterate_one]
  rw [hit3]
  refine ⟨?_, ?_, ?_, ?_⟩
  · rw [splitStep_src src o1 o2 o3 hs1 hs2 hs3, s2src,
      cellsTape_moveRight_headD]
    rfl
  · rw [p21, s2o1, cellsTape_moveRight_headD]
    rfl
  · rw [p22, s2o2, cellsTape_moveRight_headD]
    rfl
  · rw [p23, s2src, s2o3, write_cellsTape, cellsTape_moveRight_headD]
    rfl


set_option maxHeartbeats 4000000 in
/-- **The split, accumulated.** -/
theorem split_iterate (src o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3) :
    ∀ (t : Nat) (cs : List TapeSymbol) (T : Fin tapes → Tape)
      (Ls Rs L1 L2 L3 : List TapeSymbol),
      cs.length = 3 * t →
      (∀ x ∈ cs, x ≠ TapeSymbol.blank) →
      T src = cellsTape Ls (cs ++ Rs) →
      T o1 = cellsTape L1 [] → T o2 = cellsTape L2 [] →
      T o3 = cellsTape L3 [] →
      (((splitStep src o1 o2 o3)^[3 * t]) T) src =
        cellsTape (cs.reverse ++ Ls) Rs ∧
      (((splitStep src o1 o2 o3)^[3 * t]) T) o1 =
        cellsTape ((third0 cs).reverse ++ L1) [] ∧
      (((splitStep src o1 o2 o3)^[3 * t]) T) o2 =
        cellsTape ((third1 cs).reverse ++ L2) [] ∧
      (((splitStep src o1 o2 o3)^[3 * t]) T) o3 =
        cellsTape ((third2 cs).reverse ++ L3) [] := by
  intro t
  induction t with
  | zero =>
      intro cs T Ls Rs L1 L2 L3 hlen hnb hsrc h1 h2 h3
      have : cs = [] := List.length_eq_zero_iff.mp (by simpa using hlen)
      subst this
      simp only [Nat.mul_zero, Function.iterate_zero_apply,
        List.reverse_nil, List.nil_append, third0, third1, third2]
      exact ⟨by simpa using hsrc, h1, h2, h3⟩
  | succ t ih =>
      intro cs T Ls Rs L1 L2 L3 hlen hnb hsrc h1 h2 h3
      obtain ⟨x0, x1, x2, cs', rfl, hlen'⟩ := triple_dest cs t hlen
      obtain ⟨ga, g1, g2, g3⟩ := splitGroup src o1 o2 o3 h12 h13 h23 hs1
        hs2 hs3 T x0 x1 x2 Ls (cs' ++ Rs) L1 L2 L3
        (hnb x0 (by simp)) (hnb x1 (by simp))
        (by rw [hsrc]; rfl) h1 h2 h3
      obtain ⟨ka, k1, k2, k3⟩ := ih cs'
        (((splitStep src o1 o2 o3)^[3]) T)
        (x2 :: x1 :: x0 :: Ls) Rs (x0 :: L1) (x1 :: L2) (x2 :: L3)
        hlen' (fun x hx => hnb x (by simp [hx])) ga g1 g2 g3
      have hsplit : ((splitStep src o1 o2 o3)^[3 * (t + 1)]) T =
          ((splitStep src o1 o2 o3)^[3 * t])
            (((splitStep src o1 o2 o3)^[3]) T) := by
        rw [show 3 * (t + 1) = 3 * t + 3 by ring,
          Function.iterate_add_apply]
      rw [hsplit]
      refine ⟨?_, ?_, ?_, ?_⟩
      · rw [ka]; simp
      · rw [k1]
        show cellsTape _ _ = cellsTape _ _
        congr 1
        show (third0 cs').reverse ++ x0 :: L1 = _
        rw [show third0 (x0 :: x1 :: x2 :: cs') = x0 :: third0 cs'
          from rfl]
        simp
      · rw [k2]
        show cellsTape _ _ = cellsTape _ _
        congr 1
        show (third1 cs').reverse ++ x1 :: L2 = _
        rw [show third1 (x0 :: x1 :: x2 :: cs') = x1 :: third1 cs'
          from rfl]
        simp
      · rw [k3]
        show cellsTape _ _ = cellsTape _ _
        congr 1
        show (third2 cs').reverse ++ x2 :: L3 = _
        rw [show third2 (x0 :: x1 :: x2 :: cs') = x2 :: third2 cs'
          from rfl]
        simp

/-- The source's evolution is a plain rightward walk. -/
theorem split_src_iter (src o1 o2 o3 : Fin tapes)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3) :
    ∀ (r : Nat) (T : Fin tapes → Tape),
      (((splitStep src o1 o2 o3)^[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 (splitStep src o1 o2 o3 T),
        splitStep_src src o1 o2 o3 hs1 hs2 hs3 T]
      rfl

/-- The marks hypothesis for the split walk. -/
theorem split_marks (src o1 o2 o3 : Fin tapes)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3)
    (cs Ls Rs : List TapeSymbol) (T : Fin tapes → Tape)
    (hnb : ∀ x ∈ cs, x ≠ TapeSymbol.blank)
    (hsrc : T src = cellsTape Ls (cs ++ TapeSymbol.blank :: Rs)) :
    (∀ r, r < cs.length →
      ((((splitStep src o1 o2 o3)^[r]) T) src).head ≠ TapeSymbol.blank) ∧
    ((((splitStep src o1 o2 o3)^[cs.length]) T) src).head =
      TapeSymbol.blank := by
  have hev := split_src_iter src o1 o2 o3 hs1 hs2 hs3
  constructor
  · intro r hr
    rw [hev r T, hsrc]
    obtain ⟨L', hL'⟩ := moveRight_iterate_exists r Ls
      (cs ++ TapeSymbol.blank :: 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 ++ TapeSymbol.blank :: 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 ++ TapeSymbol.blank :: Rs)
    rw [hL']
    rw [List.drop_append_of_le_length (by omega)]
    rw [List.drop_length]
    rfl


/-- The source's evolution is a plain rightward walk. -/
theorem splitStep_src_iter (src o1 o2 o3 : Fin tapes)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3) :
    ∀ (r : Nat) (T : Fin tapes → Tape),
      (((splitStep src o1 o2 o3)^[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 (splitStep src o1 o2 o3 T),
        splitStep_src src o1 o2 o3 hs1 hs2 hs3 T]
      rfl

/-- The marks hypothesis, from the source's shape. -/
theorem splitStep_marks (src o1 o2 o3 : Fin tapes)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3)
    (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 →
      ((((splitStep src o1 o2 o3)^[r]) T) src).head ≠ TapeSymbol.blank) ∧
    ((((splitStep src o1 o2 o3)^[cs.length]) T) src).head =
      TapeSymbol.blank := by
  have hev := splitStep_src_iter src o1 o2 o3 hs1 hs2 hs3
  constructor
  · intro r hr
    rw [hev r T, hsrc]
    obtain ⟨L', hL'⟩ := moveRight_iterate_exists r Ls (cs ++ Rs)
    rw [hL', 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', List.drop_append_of_le_length (by omega), List.drop_length]
    show Rs.headD TapeSymbol.blank = TapeSymbol.blank
    exact hRs


set_option maxHeartbeats 4000000 in
/-- **Groups of three.**  Over `t` groups the source loses `3t` marks and
each collector gains `t`. -/
theorem splitStep_iterate (src o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3) :
    ∀ (t : Nat) (T : Fin tapes → Tape) (Ls Rs L1 L2 L3 : List TapeSymbol),
      T src = cellsTape Ls
        (List.replicate (3 * t) (TapeSymbol.bit true) ++ Rs) →
      T o1 = cellsTape L1 [] → T o2 = cellsTape L2 [] →
      T o3 = cellsTape L3 [] →
      (((splitStep src o1 o2 o3)^[3 * t]) T) src =
        cellsTape (List.replicate (3 * t) (TapeSymbol.bit true) ++ Ls) Rs ∧
      (((splitStep src o1 o2 o3)^[3 * t]) T) o1 =
        cellsTape (List.replicate t (TapeSymbol.bit true) ++ L1) [] ∧
      (((splitStep src o1 o2 o3)^[3 * t]) T) o2 =
        cellsTape (List.replicate t (TapeSymbol.bit true) ++ L2) [] ∧
      (((splitStep src o1 o2 o3)^[3 * t]) T) o3 =
        cellsTape (List.replicate t (TapeSymbol.bit true) ++ L3) [] := by
  intro t
  induction t with
  | zero =>
      intro T Ls Rs L1 L2 L3 hsrc h1 h2 h3
      simp only [Nat.mul_zero, Function.iterate_zero_apply,
        List.replicate_zero, List.nil_append]
      exact ⟨by simpa using hsrc, h1, h2, h3⟩
  | succ t ih =>
      intro T Ls Rs L1 L2 L3 hsrc h1 h2 h3
      have hsrc' : T src = cellsTape Ls
          (TapeSymbol.bit true :: TapeSymbol.bit true ::
            TapeSymbol.bit true ::
            (List.replicate (3 * t) (TapeSymbol.bit true) ++ Rs)) := by
        rw [hsrc]
        congr 1
      obtain ⟨ga, g1, g2, g3⟩ := splitGroup src o1 o2 o3 h12 h13 h23 hs1
        hs2 hs3 T (TapeSymbol.bit true) (TapeSymbol.bit true)
        (TapeSymbol.bit true) Ls
        (List.replicate (3 * t) (TapeSymbol.bit true) ++ Rs) L1 L2 L3
        (by simp) (by simp) hsrc' h1 h2 h3
      obtain ⟨ka, k1, k2, k3⟩ := ih (((splitStep src o1 o2 o3)^[3]) T)
        (TapeSymbol.bit true :: TapeSymbol.bit true ::
          TapeSymbol.bit true :: Ls) Rs
        (TapeSymbol.bit true :: L1) (TapeSymbol.bit true :: L2)
        (TapeSymbol.bit true :: L3) ga g1 g2 g3
      have hsplit : ((splitStep src o1 o2 o3)^[3 * (t + 1)]) T =
          ((splitStep src o1 o2 o3)^[3 * t])
            (((splitStep src o1 o2 o3)^[3]) T) := by
        rw [show 3 * (t + 1) = 3 * t + 3 by ring,
          Function.iterate_add_apply]
      rw [hsplit]
      refine ⟨?_, ?_, ?_, ?_⟩
      · rw [ka]
        show cellsTape _ Rs = cellsTape _ Rs
        congr 1
        rw [show 3 * (t + 1) = 3 * t + 3 by ring]
        simp [List.replicate_add]
      · rw [k1]
        show cellsTape _ [] = cellsTape _ []
        congr 1
        rw [show List.replicate (t + 1) (TapeSymbol.bit true) =
          List.replicate t (TapeSymbol.bit true) ++ [TapeSymbol.bit true]
          from List.replicate_succ']
        simp
      · rw [k2]
        show cellsTape _ [] = cellsTape _ []
        congr 1
        rw [show List.replicate (t + 1) (TapeSymbol.bit true) =
          List.replicate t (TapeSymbol.bit true) ++ [TapeSymbol.bit true]
          from List.replicate_succ']
        simp
      · rw [k3]
        show cellsTape _ [] = cellsTape _ []
        congr 1
        rw [show List.replicate (t + 1) (TapeSymbol.bit true) =
          List.replicate t (TapeSymbol.bit true) ++ [TapeSymbol.bit true]
          from List.replicate_succ']
        simp


/-- The leftover strides of an incomplete group spare the third collector. -/
theorem splitStep_third_untouched (src o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3)
    (T : Fin tapes → Tape) (L1 L2 : List TapeSymbol)
    (h1 : T o1 = cellsTape L1 []) (h2 : T o2 = cellsTape L2 [])
    (hnb : (T src).head ≠ TapeSymbol.blank) :
    (splitStep src o1 o2 o3 T) o3 = T o3 ∧
    (splitStep src o1 o2 o3 (splitStep src o1 o2 o3 T)) o3 = T o3 := by
  have hp0 : (T o1).head = TapeSymbol.blank := by rw [h1]; rfl
  obtain ⟨q1, q2, q3⟩ := splitStep_phase0 src o1 o2 o3 h12 h13 h23 hs1 hs2
    hs3 T hp0
  refine ⟨q3, ?_⟩
  have hp1a : ((splitStep src o1 o2 o3 T) o1).head ≠ TapeSymbol.blank := by
    rw [q1, h1, write_cellsTape]
    show (T src).head ≠ TapeSymbol.blank
    exact hnb
  have hp1b : ((splitStep src o1 o2 o3 T) o2).head = TapeSymbol.blank := by
    rw [q2, h2]
    rfl
  obtain ⟨-, -, r3⟩ := splitStep_phase1 src o1 o2 o3 h12 h13 h23 hs1 hs2 hs3
    (splitStep src o1 o2 o3 T) hp1a hp1b
  rw [r3, q3]


set_option maxHeartbeats 4000000 in
/-- **The split walk thirds a tally.**  Whatever the count, the third
collector ends with a third of it, rounded down. -/
theorem splitWalk_third (src o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (hs1 : src ≠ o1) (hs2 : src ≠ o2) (hs3 : src ≠ o3)
    (m : Nat) (T : Fin tapes → Tape) (Ls L1 L2 L3 : List TapeSymbol)
    (hsrc : T src = cellsTape Ls
      (List.replicate m (TapeSymbol.bit true) ++ TapeSymbol.blank :: []))
    (h1 : T o1 = cellsTape L1 []) (h2 : T o2 = cellsTape L2 [])
    (h3 : T o3 = cellsTape L3 []) :
    HaltsExactly (splitWalk src o1 o2 o3)
      ((splitWalk src o1 o2 o3).startCfg T) (m * 5 + 4) false ∧
    (((splitWalk src o1 o2 o3).step^[m * 5 + 4])
      ((splitWalk src o1 o2 o3).startCfg T)).tape o3 =
      cellsTape (List.replicate (m / 3) (TapeSymbol.bit true) ++ L3) [] ∧
    (∃ L, (((splitWalk src o1 o2 o3).step^[m * 5 + 4])
      ((splitWalk src o1 o2 o3).startCfg T)).tape src =
      cellsTape L (TapeSymbol.blank :: [])) ∧
    (∃ L c, (((splitWalk src o1 o2 o3).step^[m * 5 + 4])
      ((splitWalk src o1 o2 o3).startCfg T)).tape o1 =
      cellsTape L c ∧ c.length ≤ 1) ∧
    (∃ L c, (((splitWalk src o1 o2 o3).step^[m * 5 + 4])
      ((splitWalk src o1 o2 o3).startCfg T)).tape o2 =
      cellsTape L c ∧ c.length ≤ 1) ∧
    (∀ j, j ≠ src → j ≠ o1 → j ≠ o2 → j ≠ o3 →
      (((splitWalk src o1 o2 o3).step^[m * 5 + 4])
        ((splitWalk src o1 o2 o3).startCfg T)).tape j = T j) := by
  classical
  set t := m / 3 with hst
  set r := m % 3 with hsr
  have hm : m = 3 * t + r := by omega
  have hr3 : r < 3 := by rw [hsr]; omega
  obtain ⟨hmk, hex⟩ := splitStep_marks src o1 o2 o3 hs1 hs2 hs3
    (List.replicate m (TapeSymbol.bit true)) Ls (TapeSymbol.blank :: []) T
    (by
      intro x hx
      rw [List.eq_of_mem_replicate hx]
      simp) rfl hsrc
  rw [List.length_replicate] at hmk hex
  obtain ⟨g1, t1⟩ := splitWalk_spec src o1 o2 o3 h12 h13 h23 hs1 hs2 hs3 m T
    hmk hex
  -- the complete groups
  obtain ⟨ka, k1, k2, k3⟩ := splitStep_iterate src o1 o2 o3 h12 h13 h23 hs1
    hs2 hs3 t T Ls
    (List.replicate r (TapeSymbol.bit true) ++ TapeSymbol.blank :: [])
    L1 L2 L3
    (by rw [hsrc, hm, List.replicate_add, List.append_assoc])
    h1 h2 h3
  generalize hA : ((splitStep src o1 o2 o3)^[3 * t]) T = A
    at ka k1 k2 k3
  -- the leftovers spare the third collector
  have hAsrc : A src = cellsTape
      (List.replicate (3 * t) (TapeSymbol.bit true) ++ Ls)
      (List.replicate r (TapeSymbol.bit true) ++
        TapeSymbol.blank :: []) := ka
  have hfinal : ((splitStep src o1 o2 o3)^[m]) T o3 = A o3 := by
    rw [hm]
    clear_value r
    interval_cases r
    · simp only [Nat.add_zero]
      rw [hA]
    · rw [show 3 * t + 1 = 1 + 3 * t by ring, Function.iterate_add_apply,
        hA, Function.iterate_one]
      exact (splitStep_third_untouched src o1 o2 o3 h12 h13 h23 hs1 hs2 hs3
        A _ _ k1 k2
        (by
          rw [hAsrc]
          show (List.replicate 1 (TapeSymbol.bit true) ++
            TapeSymbol.blank :: []).headD TapeSymbol.blank ≠
            TapeSymbol.blank
          simp)).1
    · rw [show 3 * t + 2 = 2 + 3 * t by ring, Function.iterate_add_apply,
        hA]
      exact (splitStep_third_untouched src o1 o2 o3 h12 h13 h23 hs1 hs2 hs3
        A _ _ k1 k2
        (by
          rw [hAsrc]
          show (List.replicate 2 (TapeSymbol.bit true) ++
            TapeSymbol.blank :: []).headD TapeSymbol.blank ≠
            TapeSymbol.blank
          simp)).2
  -- the source ends parked on its terminator
  have hsrcfin : ∃ L, ((splitStep src o1 o2 o3)^[m]) T src =
      cellsTape L (TapeSymbol.blank :: []) := by
    rw [splitStep_src_iter src o1 o2 o3 hs1 hs2 hs3 m T, hsrc]
    obtain ⟨L', hL'⟩ := moveRight_iterate_exists m Ls
      (List.replicate m (TapeSymbol.bit true) ++ TapeSymbol.blank :: [])
    refine ⟨L', ?_⟩
    rw [hL', List.drop_append_of_le_length
      (by rw [List.length_replicate]),
      show List.drop m (List.replicate m (TapeSymbol.bit true)) = []
        from by simp]
    rfl
  -- the two discard collectors end with at most one cell ahead
  have hcolfin : ∀ o : Fin tapes, o = o1 ∨ o = o2 →
      ∃ L c, ((splitStep src o1 o2 o3)^[m]) T o = cellsTape L c ∧
        c.length ≤ 1 := by
    intro o ho
    rw [hm]
    clear_value r
    interval_cases r
    · simp only [Nat.add_zero]
      rcases ho with rfl | rfl
      · exact ⟨List.replicate t (TapeSymbol.bit true) ++ L1, [],
          by rw [hA]; exact k1, by simp⟩
      · exact ⟨List.replicate t (TapeSymbol.bit true) ++ L2, [],
          by rw [hA]; exact k2, by simp⟩
    · rw [show 3 * t + 1 = 1 + 3 * t by ring, Function.iterate_add_apply,
        hA, Function.iterate_one]
      have hp0 : (A o1).head = TapeSymbol.blank := by rw [k1]; rfl
      obtain ⟨q1, q2, -⟩ := splitStep_phase0 src o1 o2 o3 h12 h13 h23 hs1
        hs2 hs3 A hp0
      rcases ho with rfl | rfl
      · refine ⟨List.replicate t (TapeSymbol.bit true) ++ L1,
          [(A src).head], ?_, by simp⟩
        rw [q1, k1, write_cellsTape]
        rfl
      · exact ⟨List.replicate t (TapeSymbol.bit true) ++ L2, [],
          by rw [q2]; exact k2, by simp⟩
    · rw [show 3 * t + 2 = 2 + 3 * t by ring, Function.iterate_add_apply,
        hA]
      have hp0 : (A o1).head = TapeSymbol.blank := by rw [k1]; rfl
      obtain ⟨q1, q2, -⟩ := splitStep_phase0 src o1 o2 o3 h12 h13 h23 hs1
        hs2 hs3 A hp0
      have hp1a : ((splitStep src o1 o2 o3 A) o1).head ≠
          TapeSymbol.blank := by
        rw [q1, k1, write_cellsTape]
        show (A src).head ≠ TapeSymbol.blank
        rw [hAsrc]
        show (List.replicate 2 (TapeSymbol.bit true) ++
          TapeSymbol.blank :: []).headD TapeSymbol.blank ≠ TapeSymbol.blank
        simp
      have hp1b : ((splitStep src o1 o2 o3 A) o2).head =
          TapeSymbol.blank := by
        rw [q2, k2]; rfl
      obtain ⟨r1, r2, -⟩ := splitStep_phase1 src o1 o2 o3 h12 h13 h23 hs1
        hs2 hs3 (splitStep src o1 o2 o3 A) hp1a hp1b
      rcases ho with rfl | rfl
      · refine ⟨List.replicate t (TapeSymbol.bit true) ++ L1,
          [(A src).head], ?_, by simp⟩
        show (splitStep src o o2 o3 (splitStep src o o2 o3 A)) o = _
        rw [r1, q1, k1, write_cellsTape]
        rfl
      · refine ⟨List.replicate t (TapeSymbol.bit true) ++ L2,
          [((splitStep src o1 o o3 A) src).head], ?_, by simp⟩
        show (splitStep src o1 o o3 (splitStep src o1 o o3 A)) o = _
        rw [r2, q2, k2, write_cellsTape]
        rfl
  refine ⟨g1, ?_, ?_, ?_, ?_, ?_⟩
  · rw [t1, hfinal, k3]
  · rw [t1]
    exact hsrcfin
  · rw [t1]
    exact hcolfin o1 (Or.inl rfl)
  · rw [t1]
    exact hcolfin o2 (Or.inr rfl)
  · intro j hjs hj1 hj2 hj3
    rw [t1]
    exact splitStep_other src o1 o2 o3 m T j hjs hj1 hj2 hj3

end SipserGacsLautemann