sgl_clog_loop

import Definitions.Def_sgl_half_walk
import Definitions.Def_sgl_copy_back
import Definitions.Def_sgl_left_loop
import Definitions.Def_sgl_casc_loop

/-!
# One halving pass

Advance the two output heads — planting rewind anchors — deal the tally
across them, and rewind the first output: it now carries `⌈m/2⌉` marks,
run-shaped up to a blank-reading tail.  The second output is scratch.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- One halving pass. -/
noncomputable def halvePass (src o1 o2 : Fin tapes) :=
  (moveUpTo o1 1 HeadMove.right).andThen fun _ =>
  (moveUpTo o2 1 HeadMove.right).andThen fun _ =>
  (halfWalk src o1 o2).andThen fun _ =>
  rewindRun o1

/-- Marks are marks. -/
theorem replicate_marks_nonblank (n : Nat) :
    ∀ x ∈ List.replicate n (TapeSymbol.bit true), x ≠ TapeSymbol.blank := by
  intro x hx
  rw [List.eq_of_mem_replicate hx]
  simp

set_option maxHeartbeats 4000000 in
/-- **The pass halves the tally, rounding up.** -/
theorem halvePass_spec (src o1 o2 : Fin tapes)
    (h12 : o1 ≠ o2) (hs1 : src ≠ o1) (hs2 : src ≠ o2)
    (m : Nat) (T : Fin tapes → Tape)
    (Ls L1 L2 Rs : List TapeSymbol)
    (hRs : Rs.headD TapeSymbol.blank = TapeSymbol.blank)
    (hsrc : T src = cellsTape Ls
      (List.replicate m (TapeSymbol.bit true) ++ Rs))
    (h1 : T o1 = cellsTape L1 []) (h2 : T o2 = cellsTape L2 []) :
    ∃ cost : Nat,
      cost ≤ 8 * m + 25 ∧
      HaltsExactly (halvePass src o1 o2)
        ((halvePass src o1 o2).startCfg T) cost true ∧
      (∃ Rf : List TapeSymbol,
        (Rf = TapeSymbol.blank :: [] ∨ Rf = []) ∧
        (((halvePass src o1 o2).step^[cost])
          ((halvePass src o1 o2).startCfg T)).tape o1 =
          cellsTape (TapeSymbol.blank :: L1)
            (List.replicate ((m + 1) / 2) (TapeSymbol.bit true) ++ Rf)) ∧
      (∃ Lsf : List TapeSymbol,
        (((halvePass src o1 o2).step^[cost])
          ((halvePass src o1 o2).startCfg T)).tape src =
          cellsTape Lsf Rs) ∧
      (∃ L2f : List TapeSymbol,
        (((halvePass src o1 o2).step^[cost])
          ((halvePass src o1 o2).startCfg T)).tape o2 =
          cellsTape L2f []) ∧
      (∀ j, j ≠ src → j ≠ o1 → j ≠ o2 →
        (((halvePass src o1 o2).step^[cost])
          ((halvePass src o1 o2).startCfg T)).tape j = T j) := by
  classical
  -- advance the outputs
  have g1 := moveUpTo_spec o1 1 HeadMove.right (by omega) T
  have t1 := moveUpTo_tape o1 1 HeadMove.right (by omega) T
  generalize hU1 : Function.update T o1
    ((moveDir HeadMove.right)^[1] (T o1)) = U1 at t1
  have hU1o1 : U1 o1 = cellsTape (TapeSymbol.blank :: L1) [] := by
    rw [← hU1, Function.update_self, Function.iterate_one, h1,
      cellsTape_moveRight_headD]
    rfl
  have g2 := moveUpTo_spec o2 1 HeadMove.right (by omega) U1
  have t2 := moveUpTo_tape o2 1 HeadMove.right (by omega) U1
  generalize hU2 : Function.update U1 o2
    ((moveDir HeadMove.right)^[1] (U1 o2)) = U2 at t2
  have hU2o2 : U2 o2 = cellsTape (TapeSymbol.blank :: L2) [] := by
    rw [← hU2, Function.update_self, Function.iterate_one, ← hU1,
      Function.update_of_ne h12.symm, h2, cellsTape_moveRight_headD]
    rfl
  have hU2o1 : U2 o1 = cellsTape (TapeSymbol.blank :: L1) [] := by
    rw [← hU2, Function.update_of_ne h12]
    exact hU1o1
  have hU2src : U2 src = cellsTape Ls
      (List.replicate m (TapeSymbol.bit true) ++ Rs) := by
    rw [← hU2, Function.update_of_ne hs2, ← hU1,
      Function.update_of_ne hs1, hsrc]
  -- the walk
  obtain ⟨hmk, hex⟩ := half_marks src o1 o2 hs1 hs2
    (List.replicate m (TapeSymbol.bit true)) Ls Rs U2
    (replicate_marks_nonblank m) hRs hU2src
  rw [List.length_replicate] at hmk hex
  obtain ⟨g3, t3⟩ := halfWalk_spec src o1 o2 h12 hs1 hs2 m U2 hmk hex
  rcases Nat.even_or_odd m with ⟨t, ht⟩ | ⟨t, ht⟩
  · -- even: m = t + t
    have ht2 : m = 2 * t := by omega
    subst ht2
    obtain ⟨ka, k1, k2⟩ := half_iterate_marks src o1 o2 h12 hs1 hs2 t U2
      Ls Rs (TapeSymbol.blank :: L1)
      (TapeSymbol.blank :: L2) hU2src hU2o1 hU2o2
    have hmid : (((halfStep src o1 o2)^[2 * t]) U2) o1 =
        cellsTape ((List.replicate t (TapeSymbol.bit true)).reverse ++
          TapeSymbol.blank :: L1) (TapeSymbol.blank :: []) := by
      rw [k1, List.reverse_replicate]
      rfl
    obtain ⟨g4, t4⟩ := rewindRun_spec o1
      (List.replicate t (TapeSymbol.bit true)) L1 []
      TapeSymbol.blank (((halfStep src o1 o2)^[2 * t]) U2)
      (replicate_marks_nonblank t) hmid
    rw [List.length_replicate] at g4 t4
    have ch34 := chainStepC g3 t3 g4
    have ch23 := chainStepC g2 t2 ch34.1
    have ch12 := chainStepC g1 t1 ch23.1
    have htp : (((halvePass src o1 o2).step^[1 + 1 + (1 + 1 +
        (2 * t * 5 + 4 + 1 + (t * 4 + 3 + 1 + 1)))])
        ((halvePass src o1 o2).startCfg T)).tape =
        Function.update (((halfStep src o1 o2)^[2 * t]) U2) o1
          (cellsTape (TapeSymbol.blank :: L1)
            (List.replicate t (TapeSymbol.bit true) ++
              TapeSymbol.blank :: [])) := by
      unfold halvePass
      rw [ch12.2, ch23.2, ch34.2]
      show (((rewindRun (tapes := tapes) o1).step^[t * 4 + 3 + 1 + 1])
        ((rewindRun (tapes := tapes) o1).startCfg
          (((halfStep src o1 o2)^[2 * t]) U2))).tape = _
      rw [t4]
    refine ⟨_, ?_, ch12.1, ⟨TapeSymbol.blank :: [], Or.inl rfl, ?_⟩,
      ⟨List.replicate (2 * t) (TapeSymbol.bit true) ++ Ls, ?_⟩,
      ⟨List.replicate t (TapeSymbol.bit true) ++ TapeSymbol.blank :: L2,
        ?_⟩, ?_⟩
    · omega
    · rw [htp, Function.update_self,
        show (2 * t + 1) / 2 = t by omega]
    · rw [htp, Function.update_of_ne hs1, ka]
    · rw [htp, Function.update_of_ne h12.symm, k2]
    · intro j hjs hj1 hj2
      rw [htp, Function.update_of_ne hj1,
        halfStep_other src o1 o2 (2 * t) U2 j hjs hj1 hj2,
        ← hU2, Function.update_of_ne hj2, ← hU1,
        Function.update_of_ne hj1]
  · -- odd: m = 2t + 1
    subst ht
    have hsrc' : U2 src = cellsTape Ls
        (List.replicate (2 * t) (TapeSymbol.bit true) ++
          (TapeSymbol.bit true :: Rs)) := by
      rw [hU2src]
      congr 1
      rw [show List.replicate (2 * t + 1) (TapeSymbol.bit true) =
        List.replicate (2 * t) (TapeSymbol.bit true) ++
          [TapeSymbol.bit true] from List.replicate_succ']
      simp
    obtain ⟨ka, k1, k2⟩ := half_iterate_marks src o1 o2 h12 hs1 hs2 t U2
      Ls (TapeSymbol.bit true :: Rs)
      (TapeSymbol.blank :: L1) (TapeSymbol.blank :: L2) hsrc' hU2o1 hU2o2
    have hph0 : ((((halfStep src o1 o2)^[2 * t]) U2) o1).head =
        TapeSymbol.blank := by
      rw [k1]; rfl
    obtain ⟨p01, _⟩ := halfStep_phase0 src o1 o2 h12 hs1 hs2
      (((halfStep src o1 o2)^[2 * t]) U2) hph0
    have hlast : ((halfStep src o1 o2)^[2 * t + 1]) U2 =
        halfStep src o1 o2 (((halfStep src o1 o2)^[2 * t]) U2) := by
      rw [Function.iterate_succ_apply']
    have hmid : (((halfStep src o1 o2)^[2 * t + 1]) U2) o1 =
        cellsTape ((List.replicate t (TapeSymbol.bit true)).reverse ++
          TapeSymbol.blank :: L1) (TapeSymbol.bit true :: []) := by
      rw [hlast, p01, k1, ka, write_cellsTape, List.reverse_replicate]
      rfl
    obtain ⟨g4, t4⟩ := rewindRun_spec o1
      (List.replicate t (TapeSymbol.bit true)) L1 []
      (TapeSymbol.bit true) (((halfStep src o1 o2)^[2 * t + 1]) U2)
      (replicate_marks_nonblank t) hmid
    rw [List.length_replicate] at g4 t4
    have ch34 := chainStepC g3 t3 g4
    have ch23 := chainStepC g2 t2 ch34.1
    have ch12 := chainStepC g1 t1 ch23.1
    have htp : (((halvePass src o1 o2).step^[1 + 1 + (1 + 1 +
        ((2 * t + 1) * 5 + 4 + 1 + (t * 4 + 3 + 1 + 1)))])
        ((halvePass src o1 o2).startCfg T)).tape =
        Function.update (((halfStep src o1 o2)^[2 * t + 1]) U2) o1
          (cellsTape (TapeSymbol.blank :: L1)
            (List.replicate t (TapeSymbol.bit true) ++
              TapeSymbol.bit true :: [])) := by
      unfold halvePass
      rw [ch12.2, ch23.2, ch34.2]
      show (((rewindRun (tapes := tapes) o1).step^[t * 4 + 3 + 1 + 1])
        ((rewindRun (tapes := tapes) o1).startCfg
          (((halfStep src o1 o2)^[2 * t + 1]) U2))).tape = _
      rw [t4]
    have hsrcfin : (((halfStep src o1 o2)^[2 * t + 1]) U2) src =
        cellsTape (TapeSymbol.bit true ::
          (List.replicate (2 * t) (TapeSymbol.bit true) ++ Ls)) Rs := by
      rw [hlast, halfStep_src src o1 o2 hs1 hs2, ka,
        cellsTape_moveRight_headD]
      rfl
    have ho2fin : (((halfStep src o1 o2)^[2 * t + 1]) U2) o2 =
        cellsTape (List.replicate t (TapeSymbol.bit true) ++
          TapeSymbol.blank :: L2) [] := by
      have hph0' := halfStep_phase0 src o1 o2 h12 hs1 hs2
        (((halfStep src o1 o2)^[2 * t]) U2) hph0
      rw [hlast, hph0'.2, k2]
    refine ⟨_, ?_, ch12.1, ⟨[], Or.inr rfl, ?_⟩,
      ⟨TapeSymbol.bit true ::
        (List.replicate (2 * t) (TapeSymbol.bit true) ++ Ls), ?_⟩,
      ⟨List.replicate t (TapeSymbol.bit true) ++ TapeSymbol.blank :: L2,
        ?_⟩, ?_⟩
    · omega
    · rw [htp, Function.update_self, replicate_absorb,
        show (2 * t + 1 + 1) / 2 = t + 1 by omega]
    · rw [htp, Function.update_of_ne hs1, hsrcfin]
    · rw [htp, Function.update_of_ne h12.symm, ho2fin]
    · intro j hjs hj1 hj2
      rw [htp, Function.update_of_ne hj1,
        halfStep_other src o1 o2 (2 * t + 1) U2 j hjs hj1 hj2,
        ← hU2, Function.update_of_ne hj2, ← hU1,
        Function.update_of_ne hj1]


/-- Append one mark at a tape's head, advancing past it. -/
def appendMark (dt : Fin tapes) : TypedMachine tapes Bool :=
  TypedMachine.act (fun symbols i =>
    if i = dt then (TapeSymbol.bit true, HeadMove.right)
    else (symbols i, HeadMove.stay))

theorem appendMark_spec (dt : Fin tapes) (T : Fin tapes → Tape) :
    HaltsExactly (appendMark dt) ((appendMark dt).startCfg T) 1 true ∧
    (((appendMark dt).step^[1]) ((appendMark dt).startCfg T)).tape =
      Function.update T dt
        (moveDir HeadMove.right
          (Tape.write (T dt) (TapeSymbol.bit true))) := by
  refine ⟨TypedMachine.act_spec _ T, ?_⟩
  rw [Function.iterate_one]
  funext j
  by_cases hj : j = dt
  · subst hj
    rw [Function.update_self]
    simp [appendMark, TypedMachine.step, TypedMachine.act,
      TypedMachine.startCfg, applyAction, moveDir]
  · rw [Function.update_of_ne hj]
    simp [appendMark, TypedMachine.step, TypedMachine.act,
      TypedMachine.startCfg, applyAction, hj, Tape.write_head_self,
      Tape.move]

/-- Appending onto an accumulated tally keeps the accumulated form. -/
theorem appendMark_tally (dt : Fin tapes) (T : Fin tapes → Tape)
    (j : Nat) (Ld Rd : List TapeSymbol)
    (hdt : T dt = cellsTape
      (List.replicate j (TapeSymbol.bit true) ++ TapeSymbol.blank :: Ld)
      Rd) :
    Function.update T dt
      (moveDir HeadMove.right (Tape.write (T dt) (TapeSymbol.bit true)))
      dt =
      cellsTape
        (List.replicate (j + 1) (TapeSymbol.bit true) ++
          TapeSymbol.blank :: Ld) Rd.tail := by
  rw [Function.update_self, hdt, write_cellsTape,
    cellsTape_moveRight_headD]
  rfl


/-! ## One round of the logarithm loop -/

/-- The continue branch: step back onto the run, halve it onto the partner,
and record the pass. -/
noncomputable def clogGo (live dead scr dt : Fin tapes) :=
  (moveUpTo live 1 HeadMove.left).andThen fun _ =>
  (halvePass live dead scr).andThen fun _ =>
  appendMark dt

/-- The exit branch: step back onto the run and stop. -/
noncomputable def clogStop (live : Fin tapes) :=
  (moveUpTo live 1 HeadMove.left).andThen fun _ =>
  TypedMachine.halt (tapes := tapes) false

/-- One round on a named live tape: peek one cell right; if a second mark is
there, halve, else stop. -/
noncomputable def clogStep (live dead scr dt : Fin tapes) :=
  (moveUpTo live 1 HeadMove.right).andThen fun _ =>
  (TypedMachine.test (notBlankAt live)).andThen fun w =>
    TypedMachine.either (clogGo live dead scr dt) (clogStop live) w

set_option maxHeartbeats 4000000 in
/-- **A halving round.**  Two or more marks: the tally halves onto the
partner, the pass is recorded, and the roles are ready to swap. -/
theorem clogStep_go (live dead scr dt : Fin tapes)
    (hld : live ≠ dead) (hls : live ≠ scr) (hlt : live ≠ dt)
    (hds : dead ≠ scr) (hdt : dead ≠ dt) (hst : scr ≠ dt)
    (j i : Nat) (T : Fin tapes → Tape)
    (Ll Ld Lc Ldt Rl Rdt : List TapeSymbol)
    (hRl : Rl = TapeSymbol.blank :: [] ∨ Rl = [])
    (hlive : T live = cellsTape Ll
      (List.replicate (j + 2) (TapeSymbol.bit true) ++ Rl))
    (hdead : T dead = cellsTape Ld [])
    (hscr : T scr = cellsTape Lc [])
    (hdtt : T dt = cellsTape
      (List.replicate i (TapeSymbol.bit true) ++ TapeSymbol.blank :: Ldt)
      Rdt) :
    ∃ cost : Nat,
      cost ≤ 8 * j + 50 ∧
      HaltsExactly (clogStep live dead scr dt)
        ((clogStep live dead scr dt).startCfg T) cost true ∧
      (∃ Rf : List TapeSymbol,
        (Rf = TapeSymbol.blank :: [] ∨ Rf = []) ∧
        (((clogStep live dead scr dt).step^[cost])
          ((clogStep live dead scr dt).startCfg T)).tape dead =
          cellsTape (TapeSymbol.blank :: Ld)
            (List.replicate ((j + 3) / 2) (TapeSymbol.bit true) ++ Rf)) ∧
      (∃ Lf : List TapeSymbol,
        (((clogStep live dead scr dt).step^[cost])
          ((clogStep live dead scr dt).startCfg T)).tape live =
          cellsTape Lf Rl) ∧
      (∃ Lcf : List TapeSymbol,
        (((clogStep live dead scr dt).step^[cost])
          ((clogStep live dead scr dt).startCfg T)).tape scr =
          cellsTape Lcf []) ∧
      (((clogStep live dead scr dt).step^[cost])
        ((clogStep live dead scr dt).startCfg T)).tape dt =
        cellsTape
          (List.replicate (i + 1) (TapeSymbol.bit true) ++
            TapeSymbol.blank :: Ldt) Rdt.tail ∧
      (∀ k, k ≠ live → k ≠ dead → k ≠ scr → k ≠ dt →
        (((clogStep live dead scr dt).step^[cost])
          ((clogStep live dead scr dt).startCfg T)).tape k = T k) := by
  classical
  -- peek right
  have g1 := moveUpTo_spec live 1 HeadMove.right (by omega) T
  have t1 := moveUpTo_tape live 1 HeadMove.right (by omega) T
  generalize hU1 : Function.update T live
    ((moveDir HeadMove.right)^[1] (T live)) = U1 at t1
  have hU1live : U1 live = cellsTape
      (TapeSymbol.bit true :: Ll)
      (List.replicate (j + 1) (TapeSymbol.bit true) ++ Rl) := by
    rw [← hU1, Function.update_self, Function.iterate_one, hlive,
      show List.replicate (j + 2) (TapeSymbol.bit true) ++ Rl =
        TapeSymbol.bit true ::
          (List.replicate (j + 1) (TapeSymbol.bit true) ++ Rl) from rfl,
      cellsTape_moveRight_headD]
    rfl
  have hmark : (U1 live).head ≠ TapeSymbol.blank := by
    rw [hU1live]
    show (List.replicate (j + 1) (TapeSymbol.bit true) ++ Rl).headD
      TapeSymbol.blank ≠ TapeSymbol.blank
    rw [show List.replicate (j + 1) (TapeSymbol.bit true) ++ Rl =
      TapeSymbol.bit true ::
        (List.replicate j (TapeSymbol.bit true) ++ Rl) from rfl]
    simp
  -- the test
  have htest := TypedMachine.test_spec (notBlankAt live) U1
  rw [notBlankAt_true live U1 hmark] at htest
  have htestt : (((TypedMachine.test (notBlankAt live)).step^[1])
      ((TypedMachine.test (notBlankAt live)).startCfg U1)).tape = U1 := by
    rw [Function.iterate_one]
    funext k
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  -- step back
  have g2 := moveUpTo_spec live 1 HeadMove.left (by omega) U1
  have t2 := moveUpTo_tape live 1 HeadMove.left (by omega) U1
  generalize hU2 : Function.update U1 live
    ((moveDir HeadMove.left)^[1] (U1 live)) = U2 at t2
  have hU2live : U2 live = cellsTape Ll
      (List.replicate (j + 2) (TapeSymbol.bit true) ++ Rl) := by
    rw [← hU2, Function.update_self, Function.iterate_one, hU1live,
      cellsTape_moveLeft_headD]
    rfl
  have hU2dead : U2 dead = cellsTape Ld [] := by
    rw [← hU2, Function.update_of_ne hld.symm, ← hU1,
      Function.update_of_ne hld.symm, hdead]
  have hU2scr : U2 scr = cellsTape Lc [] := by
    rw [← hU2, Function.update_of_ne hls.symm, ← hU1,
      Function.update_of_ne hls.symm, hscr]
  have hU2dt : U2 dt = cellsTape
      (List.replicate i (TapeSymbol.bit true) ++ TapeSymbol.blank :: Ldt)
      Rdt := by
    rw [← hU2, Function.update_of_ne hlt.symm, ← hU1,
      Function.update_of_ne hlt.symm, hdtt]
  -- the halving pass
  obtain ⟨cp, hcpb, gp, ⟨Rf, hRf, hpo1⟩, ⟨Lsf, hpsrc⟩, ⟨L2f, hpo2⟩, hpoth⟩ :=
    halvePass_spec live dead scr hds hld hls (j + 2) U2 Ll Ld Lc Rl
      (by rcases hRl with h | h
          · rw [h]; rfl
          · rw [h]; rfl) hU2live hU2dead hU2scr
  generalize hV : (((halvePass live dead scr).step^[cp])
    ((halvePass live dead scr).startCfg U2)).tape = V
    at hpo1 hpsrc hpo2 hpoth
  have hVdt : V dt = cellsTape
      (List.replicate i (TapeSymbol.bit true) ++ TapeSymbol.blank :: Ldt)
      Rdt := by
    rw [hpoth dt hlt.symm hdt.symm hst.symm, hU2dt]
  -- record the pass
  obtain ⟨gm, tm⟩ := appendMark_spec dt V
  have hmt := appendMark_tally dt V i Ldt Rdt hVdt
  -- assemble the continue branch
  have chgo := chainStepC g2 t2 (chainStepC gp hV gm).1
  have hgotape : (((clogGo live dead scr dt).step^[1 + 1 + (cp + 1 + 1)])
      ((clogGo live dead scr dt).startCfg U1)).tape =
      Function.update V dt (moveDir HeadMove.right
        (Tape.write (V dt) (TapeSymbol.bit true))) := by
    unfold clogGo
    rw [chgo.2, (chainStepC gp hV gm).2]
    show (((appendMark dt).step^[1]) ((appendMark dt).startCfg V)).tape = _
    rw [tm]
  -- the dispatch
  have heith : HaltsExactly
      (TypedMachine.either (clogGo live dead scr dt) (clogStop live) true)
      ((TypedMachine.either (clogGo live dead scr dt)
        (clogStop live) true).startCfg U1) (1 + 1 + (cp + 1 + 1)) true := by
    have := HaltsExactly.either_inl (clogStop live) true chgo.1
    exact this
  have heithtape : (((TypedMachine.either (clogGo live dead scr dt)
      (clogStop live) true).step^[1 + 1 + (cp + 1 + 1)])
      ((TypedMachine.either (clogGo live dead scr dt)
        (clogStop live) true).startCfg U1)).tape =
      (((clogGo live dead scr dt).step^[1 + 1 + (cp + 1 + 1)])
        ((clogGo live dead scr dt).startCfg U1)).tape := by
    show ((((clogGo live dead scr dt).either (clogStop live)
      true).step^[1 + 1 + (cp + 1 + 1)])
      (⟨Sum.inl (clogGo live dead scr dt).start, U1⟩ :
        TypedConfiguration tapes _)).tape = _
    rw [TypedMachine.either_step_inl]
    rfl
  have hmain := chainStepD
    (M₂ := fun w =>
      TypedMachine.either (clogGo live dead scr dt) (clogStop live) w)
    htest htestt heith
  have hch := chainStepC g1 t1 hmain.1
  have htp : (((clogStep live dead scr dt).step^[1 + 1 +
      (1 + 1 + (1 + 1 + (cp + 1 + 1)))])
      ((clogStep live dead scr dt).startCfg T)).tape =
      Function.update V dt (moveDir HeadMove.right
        (Tape.write (V dt) (TapeSymbol.bit true))) := by
    unfold clogStep
    rw [hch.2, hmain.2]
    show (((TypedMachine.either (clogGo live dead scr dt)
      (clogStop live) true).step^[1 + 1 + (cp + 1 + 1)])
      ((TypedMachine.either (clogGo live dead scr dt)
        (clogStop live) true).startCfg U1)).tape = _
    rw [heithtape, hgotape]
  refine ⟨_, ?_, hch.1, ⟨Rf, hRf, ?_⟩, ⟨Lsf, ?_⟩, ⟨L2f, ?_⟩, ?_, ?_⟩
  · omega
  · rw [htp, Function.update_of_ne hdt, hpo1]
  · rw [htp, Function.update_of_ne hlt, hpsrc]
  · rw [htp, Function.update_of_ne hst, hpo2]
  · rw [htp, hmt]
  · intro k hkl hkd hks hkt
    rw [htp, Function.update_of_ne hkt, hpoth k hkl hkd hks,
      ← hU2, Function.update_of_ne hkl, ← hU1, Function.update_of_ne hkl]


set_option maxHeartbeats 4000000 in
/-- **The last round.**  A single mark: the round reports `false`, leaving
the tally where it was. -/
theorem clogStep_stop (live dead scr dt : Fin tapes)
    (hld : live ≠ dead) (hls : live ≠ scr) (hlt : live ≠ dt)
    (T : Fin tapes → Tape) (Ll Rl : List TapeSymbol)
    (hRl : Rl = TapeSymbol.blank :: [] ∨ Rl = [])
    (hlive : T live = cellsTape Ll
      (List.replicate 1 (TapeSymbol.bit true) ++ Rl)) :
    HaltsExactly (clogStep live dead scr dt)
      ((clogStep live dead scr dt).startCfg T) (1 + 1 + (1 + 1 + (1 + 1 + 0)))
      false ∧
    (((clogStep live dead scr dt).step^[1 + 1 + (1 + 1 + (1 + 1 + 0))])
      ((clogStep live dead scr dt).startCfg T)).tape =
      Function.update T live
        (cellsTape Ll
          (List.replicate 1 (TapeSymbol.bit true) ++
            TapeSymbol.blank :: [])) := by
  classical
  -- peek right
  have g1 := moveUpTo_spec live 1 HeadMove.right (by omega) T
  have t1 := moveUpTo_tape live 1 HeadMove.right (by omega) T
  generalize hU1 : Function.update T live
    ((moveDir HeadMove.right)^[1] (T live)) = U1 at t1
  have hU1live : U1 live = cellsTape (TapeSymbol.bit true :: Ll) Rl := by
    rw [← hU1, Function.update_self, Function.iterate_one, hlive,
      show List.replicate 1 (TapeSymbol.bit true) ++ Rl =
        TapeSymbol.bit true :: Rl from rfl, cellsTape_moveRight_headD]
    rfl
  have hblank : (U1 live).head = TapeSymbol.blank := by
    rw [hU1live]
    show Rl.headD TapeSymbol.blank = TapeSymbol.blank
    rcases hRl with h | h
    · rw [h]; rfl
    · rw [h]; rfl
  -- the test
  have htest := TypedMachine.test_spec (notBlankAt live) U1
  rw [notBlankAt_false live U1 hblank] at htest
  have htestt : (((TypedMachine.test (notBlankAt live)).step^[1])
      ((TypedMachine.test (notBlankAt live)).startCfg U1)).tape = U1 := by
    rw [Function.iterate_one]
    funext k
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  -- step back and stop
  have g2 := moveUpTo_spec live 1 HeadMove.left (by omega) U1
  have t2 := moveUpTo_tape live 1 HeadMove.left (by omega) U1
  generalize hU2 : Function.update U1 live
    ((moveDir HeadMove.left)^[1] (U1 live)) = U2 at t2
  have hU2live : U2 live = cellsTape Ll
      (List.replicate 1 (TapeSymbol.bit true) ++ TapeSymbol.blank :: []) := by
    rw [← hU2, Function.update_self, Function.iterate_one, hU1live,
      cellsTape_moveLeft_headD]
    show cellsTape _ _ = cellsTape _ _
    congr 1
    rcases hRl with h | h
    · rw [h]; rfl
    · rw [h]; rfl
  have hU2eq : U2 = Function.update T live
      (cellsTape Ll (List.replicate 1 (TapeSymbol.bit true) ++
        TapeSymbol.blank :: [])) := by
    funext k
    by_cases hk : k = live
    · subst hk
      rw [Function.update_self]
      exact hU2live
    · rw [Function.update_of_ne hk, ← hU2, Function.update_of_ne hk,
        ← hU1, Function.update_of_ne hk]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) false
    ((TypedMachine.halt (tapes := tapes) false).startCfg U2)
  have chstop := chainStepC g2 t2 hhalt
  have heith : HaltsExactly
      (TypedMachine.either (clogGo live dead scr dt) (clogStop live) false)
      ((TypedMachine.either (clogGo live dead scr dt)
        (clogStop live) false).startCfg U1) (1 + 1 + 0) false :=
    HaltsExactly.either_inr (clogGo live dead scr dt) false chstop.1
  have heithtape : (((TypedMachine.either (clogGo live dead scr dt)
      (clogStop live) false).step^[1 + 1 + 0])
      ((TypedMachine.either (clogGo live dead scr dt)
        (clogStop live) false).startCfg U1)).tape =
      (((clogStop live).step^[1 + 1 + 0])
        ((clogStop live).startCfg U1)).tape := by
    show ((((clogGo live dead scr dt).either (clogStop live)
      false).step^[1 + 1 + 0])
      (⟨Sum.inr (clogStop live).start, U1⟩ :
        TypedConfiguration tapes _)).tape = _
    rw [TypedMachine.either_step_inr]
    rfl
  have hstoptape : (((clogStop live).step^[1 + 1 + 0])
      ((clogStop live).startCfg U1)).tape = U2 := by
    unfold clogStop
    rw [chstop.2]
    show ((TypedMachine.halt (tapes := tapes) false).step^[0]
      ((TypedMachine.halt (tapes := tapes) false).startCfg U2)).tape = U2
    rfl
  have hmain := chainStepD
    (M₂ := fun w =>
      TypedMachine.either (clogGo live dead scr dt) (clogStop live) w)
    htest htestt heith
  have hch := chainStepC g1 t1 hmain.1
  refine ⟨hch.1, ?_⟩
  unfold clogStep
  rw [hch.2, hmain.2]
  show (((TypedMachine.either (clogGo live dead scr dt)
    (clogStop live) false).step^[1 + 1 + 0])
    ((TypedMachine.either (clogGo live dead scr dt)
      (clogStop live) false).startCfg U1)).tape = _
  rw [heithtape, hstoptape, hU2eq]


/-! ## The logarithm loop -/

/-- The loop body: whichever tally is live, halve it. -/
noncomputable def clogBody (tA tB scr dt : Fin tapes) :=
  (TypedMachine.test (notBlankAt tA)).andThen fun v =>
    if v then clogStep tA tB scr dt else clogStep tB tA scr dt

/-- The loop. -/
noncomputable def clogLoop (tA tB scr dt : Fin tapes) :=
  (clogBody tA tB scr dt).repeatUntilFalse

/-- The loop invariant: the live tally has `k ≥ 1` marks at its run start,
the partner and the scratch wait at their frontiers, and `i` passes are
recorded. -/
def ClogInv (tA tB scr dt : Fin tapes) (k i : Nat) (par : Bool)
    (Ldt : List TapeSymbol) (T : Fin tapes → Tape) : Prop :=
  1 ≤ k ∧
  (∃ Rdt, T dt = cellsTape
    (List.replicate i (TapeSymbol.bit true) ++ TapeSymbol.blank :: Ldt)
    Rdt) ∧
  (∃ Lc, T scr = cellsTape Lc []) ∧
  (if par then
    ((∃ Ll Rl, (Rl = TapeSymbol.blank :: [] ∨ Rl = []) ∧
      T tA = cellsTape Ll
        (List.replicate k (TapeSymbol.bit true) ++ Rl)) ∧
     (∃ Ld, T tB = cellsTape Ld []))
   else
    ((∃ Ll Rl, (Rl = TapeSymbol.blank :: [] ∨ Rl = []) ∧
      T tB = cellsTape Ll
        (List.replicate k (TapeSymbol.bit true) ++ Rl)) ∧
     (∃ Ld, T tA = cellsTape Ld [])))

set_option maxHeartbeats 4000000 in
/-- **A round of the loop.**  Two or more marks: the invariant reappears one
halving down, with the roles swapped and a pass recorded. -/
theorem clogRound (tA tB scr dt : Fin tapes)
    (hAB : tA ≠ tB) (hAs : tA ≠ scr) (hAt : tA ≠ dt)
    (hBs : tB ≠ scr) (hBt : tB ≠ dt) (hst : scr ≠ dt)
    (j i : Nat) (par : Bool) (Ldt : List TapeSymbol)
    (T : Fin tapes → Tape)
    (hInv : ClogInv tA tB scr dt (j + 2) i par Ldt T) :
    ∃ cb : Nat,
      cb ≤ 8 * j + 60 ∧
      HaltsExactly (clogBody tA tB scr dt)
        ((clogBody tA tB scr dt).startCfg T) cb true ∧
      ClogInv tA tB scr dt ((j + 3) / 2) (i + 1) (!par) Ldt
        ((((clogBody tA tB scr dt).step^[cb])
          ((clogBody tA tB scr dt).startCfg T)).tape) ∧
      (∀ k, k ≠ tA → k ≠ tB → k ≠ scr → k ≠ dt →
        (((clogBody tA tB scr dt).step^[cb])
          ((clogBody tA tB scr dt).startCfg T)).tape k = T k) := by
  classical
  obtain ⟨hk, ⟨Rdt, hdtt⟩, ⟨Lc, hscr⟩, hpar⟩ := hInv
  have htestt : (((TypedMachine.test (notBlankAt tA)).step^[1])
      ((TypedMachine.test (notBlankAt tA)).startCfg T)).tape = T := by
    rw [Function.iterate_one]
    funext k
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  cases par with
  | true =>
      obtain ⟨⟨Ll, Rl, hRl, hlive⟩, ⟨Ld, hdead⟩⟩ := hpar
      have hmark : (T tA).head ≠ TapeSymbol.blank := by
        rw [hlive]
        show (List.replicate (j + 2) (TapeSymbol.bit true) ++ Rl).headD
          TapeSymbol.blank ≠ TapeSymbol.blank
        rw [show List.replicate (j + 2) (TapeSymbol.bit true) ++ Rl =
          TapeSymbol.bit true ::
            (List.replicate (j + 1) (TapeSymbol.bit true) ++ Rl) from rfl]
        simp
      have htest := TypedMachine.test_spec (notBlankAt tA) T
      rw [notBlankAt_true tA T hmark] at htest
      obtain ⟨cs, hcsb, gs, ⟨Rf, hRf, hfd⟩, ⟨Lf, hfl⟩, ⟨Lcf, hfc⟩, hfdt,
        hfoth⟩ := clogStep_go tA tB scr dt hAB hAs hAt hBs hBt hst j i T
        Ll Ld Lc Ldt Rl Rdt hRl hlive hdead hscr hdtt
      have hmain := chainStepD
        (M₂ := fun v =>
          if v then clogStep tA tB scr dt else clogStep tB tA scr dt)
        htest htestt (by simpa using gs)
      have htp : (((clogBody tA tB scr dt).step^[1 + 1 + cs])
          ((clogBody tA tB scr dt).startCfg T)).tape =
          (((clogStep tA tB scr dt).step^[cs])
            ((clogStep tA tB scr dt).startCfg T)).tape := by
        unfold clogBody
        rw [hmain.2]
        rfl
      refine ⟨_, by omega, hmain.1, ?_,
        fun k h1 h2 h3 h4 => by rw [htp, hfoth k h1 h2 h3 h4]⟩
      refine ⟨by omega, ⟨Rdt.tail, by rw [htp, hfdt]⟩,
        ⟨Lcf, by rw [htp, hfc]⟩, ?_⟩
      show if (!true) = true then _ else _
      simp only [Bool.not_true, if_neg (by decide : ¬false = true)]
      exact ⟨⟨TapeSymbol.blank :: Ld, Rf, hRf, by rw [htp, hfd]⟩,
        ⟨Lf, by
          rw [htp, hfl]
          rcases hRl with h | h
          · rw [h]; rfl
          · rw [h]⟩⟩
  | false =>
      obtain ⟨⟨Ll, Rl, hRl, hlive⟩, ⟨Ld, hdead⟩⟩ := hpar
      have hblank : (T tA).head = TapeSymbol.blank := by
        rw [hdead]; rfl
      have htest := TypedMachine.test_spec (notBlankAt tA) T
      rw [notBlankAt_false tA T hblank] at htest
      obtain ⟨cs, hcsb, gs, ⟨Rf, hRf, hfd⟩, ⟨Lf, hfl⟩, ⟨Lcf, hfc⟩, hfdt,
        hfoth⟩ := clogStep_go tB tA scr dt hAB.symm hBs hBt hAs hAt hst j i T
        Ll Ld Lc Ldt Rl Rdt hRl hlive hdead hscr hdtt
      have hmain := chainStepD
        (M₂ := fun v =>
          if v then clogStep tA tB scr dt else clogStep tB tA scr dt)
        htest htestt (by simpa using gs)
      have htp : (((clogBody tA tB scr dt).step^[1 + 1 + cs])
          ((clogBody tA tB scr dt).startCfg T)).tape =
          (((clogStep tB tA scr dt).step^[cs])
            ((clogStep tB tA scr dt).startCfg T)).tape := by
        unfold clogBody
        rw [hmain.2]
        rfl
      refine ⟨_, by omega, hmain.1, ?_,
        fun k h1 h2 h3 h4 => by rw [htp, hfoth k h2 h1 h3 h4]⟩
      refine ⟨by omega, ⟨Rdt.tail, by rw [htp, hfdt]⟩,
        ⟨Lcf, by rw [htp, hfc]⟩, ?_⟩
      show if (!false) = true then _ else _
      simp only [Bool.not_false, if_pos rfl]
      exact ⟨⟨TapeSymbol.blank :: Ld, Rf, hRf, by rw [htp, hfd]⟩,
        ⟨Lf, by
          rw [htp, hfl]
          rcases hRl with h | h
          · rw [h]; rfl
          · rw [h]⟩⟩


set_option maxHeartbeats 4000000 in
/-- The exit round: a single mark reports `false`. -/
theorem clogRound_exit (tA tB scr dt : Fin tapes)
    (hAB : tA ≠ tB) (hAs : tA ≠ scr) (hAt : tA ≠ dt)
    (hBs : tB ≠ scr) (hBt : tB ≠ dt) (hst : scr ≠ dt)
    (i : Nat) (par : Bool) (Ldt : List TapeSymbol)
    (T : Fin tapes → Tape)
    (hInv : ClogInv tA tB scr dt 1 i par Ldt T) :
    HaltsExactly (clogBody tA tB scr dt)
      ((clogBody tA tB scr dt).startCfg T)
      (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 0)))) false ∧
    (∃ Rdt, (((clogBody tA tB scr dt).step^[
        1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 0)))])
        ((clogBody tA tB scr dt).startCfg T)).tape dt =
      cellsTape
        (List.replicate i (TapeSymbol.bit true) ++ TapeSymbol.blank :: Ldt)
        Rdt) ∧
    (∀ k, k ≠ tA → k ≠ tB → k ≠ scr → k ≠ dt →
      (((clogBody tA tB scr dt).step^[
        1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 0)))])
        ((clogBody tA tB scr dt).startCfg T)).tape k = T k) := by
  classical
  obtain ⟨hk, ⟨Rdt, hdtt⟩, ⟨Lc, hscr⟩, hpar⟩ := hInv
  have htestt : (((TypedMachine.test (notBlankAt tA)).step^[1])
      ((TypedMachine.test (notBlankAt tA)).startCfg T)).tape = T := by
    rw [Function.iterate_one]
    funext k
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  cases par with
  | true =>
      obtain ⟨⟨Ll, Rl, hRl, hlive⟩, ⟨Ld, hdead⟩⟩ := hpar
      have hmark : (T tA).head ≠ TapeSymbol.blank := by
        rw [hlive]
        show (List.replicate 1 (TapeSymbol.bit true) ++ Rl).headD
          TapeSymbol.blank ≠ TapeSymbol.blank
        simp
      have htest := TypedMachine.test_spec (notBlankAt tA) T
      rw [notBlankAt_true tA T hmark] at htest
      obtain ⟨gs, ts⟩ := clogStep_stop tA tB scr dt hAB hAs hAt T Ll Rl
        hRl hlive
      have hmain := chainStepD
        (M₂ := fun v =>
          if v then clogStep tA tB scr dt else clogStep tB tA scr dt)
        htest htestt (by simpa using gs)
      have htp : (((clogBody tA tB scr dt).step^[
          1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 0)))])
          ((clogBody tA tB scr dt).startCfg T)).tape =
          (((clogStep tA tB scr dt).step^[1 + 1 + (1 + 1 + (1 + 1 + 0))])
            ((clogStep tA tB scr dt).startCfg T)).tape := by
        unfold clogBody
        rw [hmain.2]
        rfl
      refine ⟨hmain.1, ⟨Rdt, ?_⟩,
        fun k h1 _ _ _ => by rw [htp, ts, Function.update_of_ne h1]⟩
      rw [htp, ts, Function.update_of_ne hAt.symm, hdtt]
  | false =>
      obtain ⟨⟨Ll, Rl, hRl, hlive⟩, ⟨Ld, hdead⟩⟩ := hpar
      have hblank : (T tA).head = TapeSymbol.blank := by
        rw [hdead]; rfl
      have htest := TypedMachine.test_spec (notBlankAt tA) T
      rw [notBlankAt_false tA T hblank] at htest
      obtain ⟨gs, ts⟩ := clogStep_stop tB tA scr dt hAB.symm hBs hBt T Ll Rl
        hRl hlive
      have hmain := chainStepD
        (M₂ := fun v =>
          if v then clogStep tA tB scr dt else clogStep tB tA scr dt)
        htest htestt (by simpa using gs)
      have htp : (((clogBody tA tB scr dt).step^[
          1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 0)))])
          ((clogBody tA tB scr dt).startCfg T)).tape =
          (((clogStep tB tA scr dt).step^[1 + 1 + (1 + 1 + (1 + 1 + 0))])
            ((clogStep tB tA scr dt).startCfg T)).tape := by
        unfold clogBody
        rw [hmain.2]
        rfl
      refine ⟨hmain.1, ⟨Rdt, ?_⟩,
        fun k _ h2 _ _ => by rw [htp, ts, Function.update_of_ne h2]⟩
      rw [htp, ts, Function.update_of_ne hBt.symm, hdtt]

set_option maxHeartbeats 4000000 in
/-- **The logarithm loop.**  From a tally of `k ≥ 1` marks the loop halves
until one mark remains, recording `Nat.clog 2 k` passes. -/
theorem clogLoop_run (tA tB scr dt : Fin tapes)
    (hAB : tA ≠ tB) (hAs : tA ≠ scr) (hAt : tA ≠ dt)
    (hBs : tB ≠ scr) (hBt : tB ≠ dt) (hst : scr ≠ dt)
    (Ldt : List TapeSymbol) :
    ∀ (k : Nat), ∀ (i : Nat) (par : Bool) (T : Fin tapes → Tape),
      ClogInv tA tB scr dt k i par Ldt T →
      ∃ cost : Nat,
        cost ≤ 20 * k + 60 * (Nat.clog 2 k + 1) ∧
        HaltsExactly (clogLoop tA tB scr dt)
          ((clogLoop tA tB scr dt).startCfg T) cost false ∧
        (∃ Rdt, (((clogLoop tA tB scr dt).step^[cost])
            ((clogLoop tA tB scr dt).startCfg T)).tape dt =
          cellsTape
            (List.replicate (i + Nat.clog 2 k) (TapeSymbol.bit true) ++
              TapeSymbol.blank :: Ldt) Rdt) ∧
        (∀ q, q ≠ tA → q ≠ tB → q ≠ scr → q ≠ dt →
          (((clogLoop tA tB scr dt).step^[cost])
            ((clogLoop tA tB scr dt).startCfg T)).tape q = T q) := by
  intro k
  induction k using Nat.strong_induction_on with
  | _ k ih =>
      intro i par T hInv
      match k, hInv with
      | 0, hInv => exact absurd hInv.1 (by omega)
      | 1, hInv =>
          obtain ⟨gexit, ⟨Rdt, hdtt⟩, hxoth⟩ := clogRound_exit tA tB scr dt
            hAB hAs hAt hBs hBt hst i par Ldt T hInv
          refine ⟨1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 0))), ?_, ?_,
            ⟨Rdt, ?_⟩, ?_⟩
          · have : Nat.clog 2 1 = 0 := Nat.clog_of_right_le_one (by omega) 2
            omega
          · constructor
            · show (clogLoop tA tB scr dt).result
                (((clogBody tA tB scr dt).repeatUntilFalse.step^[
                  1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 0)))])
                  ((clogBody tA tB scr dt).startCfg T)).state = some false
              exact (clogBody tA tB scr dt).repeatUntilFalse_exit _ _ gexit
            · intro s hs
              show (clogLoop tA tB scr dt).result
                (((clogBody tA tB scr dt).repeatUntilFalse.step^[s])
                  ((clogBody tA tB scr dt).startCfg T)).state = none
              exact TypedMachine.repeatUntilFalse_pre_fresh _ _ _ _ gexit s hs
          · have hz : Nat.clog 2 1 = 0 :=
              Nat.clog_of_right_le_one (by omega) 2
            rw [hz, Nat.add_zero]
            show (((clogBody tA tB scr dt).repeatUntilFalse.step^[
              1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 0)))])
              ((clogBody tA tB scr dt).startCfg T)).tape dt = _
            rw [TypedMachine.repeatUntilFalse_iterate_fresh _ _ _
              gexit.fresh]
            exact hdtt
          · intro q h1 h2 h3 h4
            show (((clogBody tA tB scr dt).repeatUntilFalse.step^[
              1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 0)))])
              ((clogBody tA tB scr dt).startCfg T)).tape q = _
            rw [TypedMachine.repeatUntilFalse_iterate_fresh _ _ _
              gexit.fresh]
            exact hxoth q h1 h2 h3 h4
      | (j + 2), hInv =>
          obtain ⟨cb, hcbb, ground, hInv', hroth⟩ := clogRound tA tB scr dt
            hAB hAs hAt hBs hBt hst j i par Ldt T hInv
          have hlt : (j + 3) / 2 < j + 2 := by omega
          obtain ⟨cost', hcost', hrest, ⟨Rdt, hdtt⟩, hoth⟩ := ih
            ((j + 3) / 2) hlt
            (i + 1) (!par)
            ((((clogBody tA tB scr dt).step^[cb])
              ((clogBody tA tB scr dt).startCfg T)).tape) hInv'
          have hclog : Nat.clog 2 (j + 2) = Nat.clog 2 ((j + 3) / 2) + 1 := by
            have h := Nat.clog_of_two_le (b := 2) (n := j + 2) (by omega)
              (by omega)
            rw [h, show (j + 2 + 2 - 1) / 2 = (j + 3) / 2 by omega]
          refine ⟨cb + 1 + cost', ?_, ?_, ⟨Rdt, ?_⟩, ?_⟩
          · have hhalf : (j + 3) / 2 ≤ j + 2 := by omega
            rw [hclog]
            have h20 : 20 * ((j + 3) / 2) ≤ 20 * (j + 2) := by omega
            omega
          · exact repeatUntilFalse_shift (clogBody tA tB scr dt)
              ((clogLoop tA tB scr dt).startCfg T) cb cost' false ground
              hrest
          · have hsh : (((clogLoop tA tB scr dt).step^[cb + 1 + cost'])
                ((clogLoop tA tB scr dt).startCfg T)) =
                (((clogLoop tA tB scr dt).step^[cost'])
                  ((clogLoop tA tB scr dt).startCfg
                    ((((clogBody tA tB scr dt).step^[cb])
                      ((clogBody tA tB scr dt).startCfg T)).tape))) :=
              repeatUntilFalse_shift_tape (clogBody tA tB scr dt)
                ((clogLoop tA tB scr dt).startCfg T) cb cost' ground
            rw [hsh, hclog, show i + (Nat.clog 2 ((j + 3) / 2) + 1) =
              i + 1 + Nat.clog 2 ((j + 3) / 2) by omega]
            exact hdtt
          · intro q h1 h2 h3 h4
            have hsh : (((clogLoop tA tB scr dt).step^[cb + 1 + cost'])
                ((clogLoop tA tB scr dt).startCfg T)) =
                (((clogLoop tA tB scr dt).step^[cost'])
                  ((clogLoop tA tB scr dt).startCfg
                    ((((clogBody tA tB scr dt).step^[cb])
                      ((clogBody tA tB scr dt).startCfg T)).tape))) :=
              repeatUntilFalse_shift_tape (clogBody tA tB scr dt)
                ((clogLoop tA tB scr dt).startCfg T) cb cost' ground
            rw [hsh, hoth q h1 h2 h3 h4, hroth q h1 h2 h3 h4]

end SipserGacsLautemann