sgl_fold3_walk

import Definitions.Def_sgl_fold_walk
import Definitions.Def_sgl_ss_tapes

/-!
# The three-to-three fold walk

Three input tapes advance in step; each stride combines their heads and
deposits the result round-robin onto three output tapes.  The round-robin
needs no state: a stride writes to the first output whose head is blank,
and after the third write all three outputs advance together, exposing
fresh blanks.  Output `k` therefore collects every third combined value —
exactly the distribution the next cascade level consumes.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- Every third element, starting at the first. -/
def third0 : List TapeSymbol → List TapeSymbol
  | x :: _ :: _ :: r => x :: third0 r
  | x :: _ :: [] => [x]
  | x :: [] => [x]
  | [] => []

/-- Every third element, starting at the second. -/
def third1 : List TapeSymbol → List TapeSymbol
  | _ :: y :: _ :: r => y :: third1 r
  | _ :: y :: [] => [y]
  | _ :: [] => []
  | [] => []

/-- Every third element, starting at the third. -/
def third2 : List TapeSymbol → List TapeSymbol
  | _ :: _ :: z :: r => z :: third2 r
  | _ :: _ :: [] => []
  | _ :: [] => []
  | [] => []

/-- One stride: combine the three input heads, deposit round-robin. -/
def fold3Step (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes) (T : Fin tapes → Tape) : Fin tapes → Tape :=
  fun i =>
    if (T a2).head = TapeSymbol.blank then
      if i = a2 then
        Tape.write (T a2)
          (TapeSymbol.bit (f (cellBool (T a).head) (cellBool (T b).head)
            (cellBool (T c).head)))
      else if i = a then moveDir HeadMove.right (T a)
      else if i = b then moveDir HeadMove.right (T b)
      else if i = c then moveDir HeadMove.right (T c)
      else T i
    else if (T b2).head = TapeSymbol.blank then
      if i = b2 then
        Tape.write (T b2)
          (TapeSymbol.bit (f (cellBool (T a).head) (cellBool (T b).head)
            (cellBool (T c).head)))
      else if i = a then moveDir HeadMove.right (T a)
      else if i = b then moveDir HeadMove.right (T b)
      else if i = c then moveDir HeadMove.right (T c)
      else T i
    else
      if i = c2 then
        moveDir HeadMove.right (Tape.write (T c2)
          (TapeSymbol.bit (f (cellBool (T a).head) (cellBool (T b).head)
            (cellBool (T c).head))))
      else if i = a2 then moveDir HeadMove.right (T a2)
      else if i = b2 then moveDir HeadMove.right (T b2)
      else if i = a then moveDir HeadMove.right (T a)
      else if i = b then moveDir HeadMove.right (T b)
      else if i = c then moveDir HeadMove.right (T c)
      else T i

/-- The stride's action. -/
def fold3Action (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes) :
    (Fin tapes → TapeSymbol) → Fin tapes → TapeSymbol × HeadMove :=
  fun symbols i =>
    if symbols a2 = TapeSymbol.blank then
      if i = a2 then
        (TapeSymbol.bit (f (cellBool (symbols a)) (cellBool (symbols b))
          (cellBool (symbols c))), HeadMove.stay)
      else if i = a then (symbols i, HeadMove.right)
      else if i = b then (symbols i, HeadMove.right)
      else if i = c then (symbols i, HeadMove.right)
      else (symbols i, HeadMove.stay)
    else if symbols b2 = TapeSymbol.blank then
      if i = b2 then
        (TapeSymbol.bit (f (cellBool (symbols a)) (cellBool (symbols b))
          (cellBool (symbols c))), HeadMove.stay)
      else if i = a then (symbols i, HeadMove.right)
      else if i = b then (symbols i, HeadMove.right)
      else if i = c then (symbols i, HeadMove.right)
      else (symbols i, HeadMove.stay)
    else
      if i = c2 then
        (TapeSymbol.bit (f (cellBool (symbols a)) (cellBool (symbols b))
          (cellBool (symbols c))), HeadMove.right)
      else if i = a2 then (symbols i, HeadMove.right)
      else if i = b2 then (symbols i, HeadMove.right)
      else if i = a then (symbols i, HeadMove.right)
      else if i = b then (symbols i, HeadMove.right)
      else if i = c then (symbols i, HeadMove.right)
      else (symbols i, HeadMove.stay)

/-- One round of the cascade level. -/
def fold3Body (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes) :=
  (TypedMachine.test (notBlankAt a)).andThen fun v =>
    if v then
      (TypedMachine.act (fold3Action f a b c a2 b2 c2)).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 cascade level: one stride per mark on the first input tape. -/
noncomputable def fold3Walk (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes) :=
  (fold3Body f a b c a2 b2 c2).repeatUntilFalse


theorem fold3Step_eq (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (h2ab : a2 ≠ b2) (h2ac : a2 ≠ c2) (h2bc : b2 ≠ c2)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c)
    (T : Fin tapes → Tape) :
    applyAction T (fold3Action f a b c a2 b2 c2) =
      fold3Step f a b c a2 b2 c2 T := by
  funext i
  simp only [fold3Step]
  by_cases hpa : (T a2).head = TapeSymbol.blank
  · rw [if_pos hpa]
    by_cases hia : i = a2
    · subst hia
      simp [applyAction, fold3Action, hpa, moveDir, Tape.move]
    · rw [if_neg hia]
      by_cases hi1 : i = a
      · subst hi1
        simp [applyAction, fold3Action, hpa, hia, Tape.write_head_self,
          moveDir]
      · rw [if_neg hi1]
        by_cases hi2 : i = b
        · subst hi2
          simp [applyAction, fold3Action, hpa, hia, hi1,
            Tape.write_head_self, moveDir]
        · rw [if_neg hi2]
          by_cases hi3 : i = c
          · subst hi3
            simp [applyAction, fold3Action, hpa, hia, hi1, hi2,
              Tape.write_head_self, moveDir]
          · rw [if_neg hi3]
            simp [applyAction, fold3Action, hpa, hia, hi1, hi2, hi3,
              Tape.write_head_self, Tape.move]
  · rw [if_neg hpa]
    by_cases hpb : (T b2).head = TapeSymbol.blank
    · rw [if_pos hpb]
      by_cases hib : i = b2
      · subst hib
        simp [applyAction, fold3Action, hpa, hpb, moveDir, Tape.move]
      · rw [if_neg hib]
        by_cases hi1 : i = a
        · subst hi1
          simp [applyAction, fold3Action, hpa, hpb, hib,
            Tape.write_head_self, moveDir]
        · rw [if_neg hi1]
          by_cases hi2 : i = b
          · subst hi2
            simp [applyAction, fold3Action, hpa, hpb, hib, hi1,
              Tape.write_head_self, moveDir]
          · rw [if_neg hi2]
            by_cases hi3 : i = c
            · subst hi3
              simp [applyAction, fold3Action, hpa, hpb, hib, hi1, hi2,
                Tape.write_head_self, moveDir]
            · rw [if_neg hi3]
              simp [applyAction, fold3Action, hpa, hpb, hib, hi1, hi2,
                hi3, Tape.write_head_self, Tape.move]
    · rw [if_neg hpb]
      by_cases hic : i = c2
      · subst hic
        simp [applyAction, fold3Action, hpa, hpb, moveDir]
      · rw [if_neg hic]
        by_cases hja : i = a2
        · subst hja
          simp [applyAction, fold3Action, hpa, hpb, hic,
            Tape.write_head_self, moveDir]
        · rw [if_neg hja]
          by_cases hjb : i = b2
          · subst hjb
            simp [applyAction, fold3Action, hpa, hpb, hic, hja,
              Tape.write_head_self, moveDir]
          · rw [if_neg hjb]
            by_cases hi1 : i = a
            · subst hi1
              simp [applyAction, fold3Action, hpa, hpb, hic, hja, hjb,
                Tape.write_head_self, moveDir]
            · rw [if_neg hi1]
              by_cases hi2 : i = b
              · subst hi2
                simp [applyAction, fold3Action, hpa, hpb, hic, hja, hjb,
                  hi1, Tape.write_head_self, moveDir]
              · rw [if_neg hi2]
                by_cases hi3 : i = c
                · subst hi3
                  simp [applyAction, fold3Action, hpa, hpb, hic, hja,
                    hjb, hi1, hi2, Tape.write_head_self, moveDir]
                · rw [if_neg hi3]
                  simp [applyAction, fold3Action, hpa, hpb, hic, hja,
                    hjb, hi1, hi2, hi3, Tape.write_head_self, Tape.move]


set_option maxHeartbeats 1000000 in
/-- A round on a marked first input. -/
theorem fold3Body_mark (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (h2ab : a2 ≠ b2) (h2ac : a2 ≠ c2) (h2bc : b2 ≠ c2)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c)
    (T : Fin tapes → Tape)
    (hmark : (T a).head ≠ TapeSymbol.blank) :
    HaltsExactly (fold3Body f a b c a2 b2 c2)
      ((fold3Body f a b c a2 b2 c2).startCfg T) (1 + 1 + (1 + 1 + 0)) true ∧
    (((fold3Body f a b c a2 b2 c2).step^[1 + 1 + (1 + 1 + 0)])
      ((fold3Body f a b c a2 b2 c2).startCfg T)).tape =
      fold3Step f a b c a2 b2 c2 T := by
  have htest := TypedMachine.test_spec (notBlankAt a) T
  rw [notBlankAt_true a T hmark] at htest
  have htestt : (((TypedMachine.test (notBlankAt a)).step^[1])
      ((TypedMachine.test (notBlankAt a)).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 (fold3Action f a b c a2 b2 c2) T
  have hactt : (((TypedMachine.act (fold3Action f a b c a2 b2 c2)).step^[1])
      ((TypedMachine.act (fold3Action f a b c a2 b2 c2)).startCfg T)).tape =
      fold3Step f a b c a2 b2 c2 T := by
    rw [Function.iterate_one, ← fold3Step_eq f a b c a2 b2 c2 hab hac hbc
      h2ab h2ac h2bc ha2a ha2b ha2c hb2a hb2b hb2c hc2a hc2b hc2c]
    funext j
    simp [TypedMachine.step, TypedMachine.act, TypedMachine.startCfg,
      applyAction]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) true
    ((TypedMachine.halt (tapes := tapes) true).startCfg
      (fold3Step f a b c a2 b2 c2 T))
  have hinner := chainStepC hact hactt hhalt
  have hmain := chainStepD
    (M₂ := fun v =>
      if v then
        (TypedMachine.act (fold3Action f a b c a2 b2 c2)).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' : ((fold3Body f a b c a2 b2 c2).step^[1 + 1 + (1 + 1 + 0)])
      ((fold3Body f a b c a2 b2 c2).startCfg T) = _ := hfin
  rw [hfin']
  show (TypedConfiguration.inRight true
    ((((TypedMachine.act (fold3Action f a b c a2 b2 c2)).andThen fun _ =>
      TypedMachine.halt (tapes := tapes) true).step^[1 + 1 + 0])
      (((TypedMachine.act (fold3Action f a b c a2 b2 c2)).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) true).startCfg T))).tape =
    fold3Step f a b c a2 b2 c2 T
  have hi := hinner.2
  rw [hi]
  show ((TypedMachine.halt (tapes := tapes) true).step^[0]
    ((TypedMachine.halt (tapes := tapes) true).startCfg
      (fold3Step f a b c a2 b2 c2 T))).tape = fold3Step f a b c a2 b2 c2 T
  rfl

set_option maxHeartbeats 1000000 in
/-- A round on a blank first input. -/
theorem fold3Body_blank (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (T : Fin tapes → Tape)
    (hblank : (T a).head = TapeSymbol.blank) :
    HaltsExactly (fold3Body f a b c a2 b2 c2)
      ((fold3Body f a b c a2 b2 c2).startCfg T) (1 + 1 + (1 + 1 + 0)) false ∧
    (((fold3Body f a b c a2 b2 c2).step^[1 + 1 + (1 + 1 + 0)])
      ((fold3Body f a b c a2 b2 c2).startCfg T)).tape = T := by
  have htest := TypedMachine.test_spec (notBlankAt a) T
  rw [notBlankAt_false a T hblank] at htest
  have htestt : (((TypedMachine.test (notBlankAt a)).step^[1])
      ((TypedMachine.test (notBlankAt a)).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 (fold3Action f a b c a2 b2 c2)).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' : ((fold3Body f a b c a2 b2 c2).step^[1 + 1 + (1 + 1 + 0)])
      ((fold3Body f a b c a2 b2 c2).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 cascade level.** -/
theorem fold3Walk_spec (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (h2ab : a2 ≠ b2) (h2ac : a2 ≠ c2) (h2bc : b2 ≠ c2)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c)
    (m : Nat) (T : Fin tapes → Tape)
    (hmarks : ∀ r, r < m →
      ((((fold3Step f a b c a2 b2 c2)^[r]) T) a).head ≠ TapeSymbol.blank)
    (hexit : ((((fold3Step f a b c a2 b2 c2)^[m]) T) a).head =
      TapeSymbol.blank) :
    HaltsExactly (fold3Walk f a b c a2 b2 c2)
      ((fold3Walk f a b c a2 b2 c2).startCfg T) (m * 5 + 4) false ∧
    (((fold3Walk f a b c a2 b2 c2).step^[m * 5 + 4])
      ((fold3Walk f a b c a2 b2 c2).startCfg T)).tape =
      ((fold3Step f a b c a2 b2 c2)^[m]) T := by
  classical
  set body := fold3Body f a b c a2 b2 c2 with hbody
  set cfg : Nat → TypedConfiguration tapes _ :=
    fun r => body.startCfg (((fold3Step f a b c a2 b2 c2)^[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⟩ := fold3Body_mark f a b c a2 b2 c2 hab hac hbc h2ab
      h2ac h2bc ha2a ha2b ha2c hb2a hb2b hb2c hc2a hc2b hc2c
      (((fold3Step f a b c a2 b2 c2)^[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 =
        ((fold3Step f a b c a2 b2 c2)^[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 (((fold3Step f a b c a2 b2 c2)^[r + 1]) T) = _
    rw [← ht4]
    rfl
  have hexitr : HaltsExactly body (cfg m) 4 false := by
    have := (fold3Body_blank f a b c a2 b2 c2
      (((fold3Step f a b c a2 b2 c2)^[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 : (fold3Walk f a b c a2 b2 c2).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 ((fold3Walk f a b c a2 b2 c2).step^[4]
    (((fold3Walk f a b c a2 b2 c2).step^[m * (4 + 1)]) (cfg 0))).tape = _
  rw [show (fold3Walk f a b c a2 b2 c2) = 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 (fold3Body_blank f a b c a2 b2 c2
    (((fold3Step f a b c a2 b2 c2)^[m]) T) hexit).2


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

/-- The inputs advance every stride, whatever the phase. -/
theorem fold3Step_inputs (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c)
    (T : Fin tapes → Tape) :
    (fold3Step f a b c a2 b2 c2 T) a = moveDir HeadMove.right (T a) ∧
    (fold3Step f a b c a2 b2 c2 T) b = moveDir HeadMove.right (T b) ∧
    (fold3Step f a b c a2 b2 c2 T) c = moveDir HeadMove.right (T c) := by
  refine ⟨?_, ?_, ?_⟩ <;> simp only [fold3Step] <;>
    by_cases hpa : (T a2).head = TapeSymbol.blank
  · rw [if_pos hpa, if_neg (Ne.symm ha2a), if_pos trivial]
  · rw [if_neg hpa]
    by_cases hpb : (T b2).head = TapeSymbol.blank
    · rw [if_pos hpb, if_neg (Ne.symm hb2a), if_pos trivial]
    · rw [if_neg hpb, if_neg (Ne.symm hc2a), if_neg (Ne.symm ha2a),
        if_neg (Ne.symm hb2a), if_pos trivial]
  · rw [if_pos hpa, if_neg (Ne.symm ha2b), if_neg (Ne.symm hab), if_pos trivial]
  · rw [if_neg hpa]
    by_cases hpb : (T b2).head = TapeSymbol.blank
    · rw [if_pos hpb, if_neg (Ne.symm hb2b), if_neg (Ne.symm hab),
        if_pos trivial]
    · rw [if_neg hpb, if_neg (Ne.symm hc2b), if_neg (Ne.symm ha2b),
        if_neg (Ne.symm hb2b), if_neg (Ne.symm hab), if_pos trivial]
  · rw [if_pos hpa, if_neg (Ne.symm ha2c), if_neg (Ne.symm hac),
      if_neg (Ne.symm hbc), if_pos trivial]
  · rw [if_neg hpa]
    by_cases hpb : (T b2).head = TapeSymbol.blank
    · rw [if_pos hpb, if_neg (Ne.symm hb2c), if_neg (Ne.symm hac),
        if_neg (Ne.symm hbc), if_pos trivial]
    · rw [if_neg hpb, if_neg (Ne.symm hc2c), if_neg (Ne.symm ha2c),
        if_neg (Ne.symm hb2c), if_neg (Ne.symm hac), if_neg (Ne.symm hbc),
        if_pos trivial]

/-- Tapes other than the six are untouched by a stride. -/
theorem fold3Step_other_one (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes) (T : Fin tapes → Tape) (j : Fin tapes)
    (hja : j ≠ a) (hjb : j ≠ b) (hjc : j ≠ c)
    (hja2 : j ≠ a2) (hjb2 : j ≠ b2) (hjc2 : j ≠ c2) :
    (fold3Step f a b c a2 b2 c2 T) j = T j := by
  simp only [fold3Step]
  by_cases hpa : (T a2).head = TapeSymbol.blank
  · rw [if_pos hpa, if_neg hja2, if_neg hja, if_neg hjb, if_neg hjc]
  · rw [if_neg hpa]
    by_cases hpb : (T b2).head = TapeSymbol.blank
    · rw [if_pos hpb, if_neg hjb2, if_neg hja, if_neg hjb, if_neg hjc]
    · rw [if_neg hpb, if_neg hjc2, if_neg hja2, if_neg hjb2, if_neg hja,
        if_neg hjb, if_neg hjc]

theorem fold3Step_other (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes) :
    ∀ (m : Nat) (T : Fin tapes → Tape) (j : Fin tapes),
      j ≠ a → j ≠ b → j ≠ c → j ≠ a2 → j ≠ b2 → j ≠ c2 →
      (((fold3Step f a b c a2 b2 c2)^[m]) T) j = T j := by
  intro m
  induction m with
  | zero => intro T j _ _ _ _ _ _; rfl
  | succ m ih =>
      intro T j hja hjb hjc hja2 hjb2 hjc2
      rw [Function.iterate_succ_apply,
        ih (fold3Step f a b c a2 b2 c2 T) j hja hjb hjc hja2 hjb2 hjc2,
        fold3Step_other_one f a b c a2 b2 c2 T j hja hjb hjc hja2 hjb2 hjc2]

/-- Phase 0: the first output's head is blank; it receives the value and
stays; the other outputs are untouched. -/
theorem fold3Step_phase0 (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (h2ab : a2 ≠ b2) (h2ac : a2 ≠ c2) (h2bc : b2 ≠ c2)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c)
    (T : Fin tapes → Tape)
    (hpa : (T a2).head = TapeSymbol.blank) :
    (fold3Step f a b c a2 b2 c2 T) a2 =
      Tape.write (T a2)
        (TapeSymbol.bit (f (cellBool (T a).head) (cellBool (T b).head)
          (cellBool (T c).head))) ∧
    (fold3Step f a b c a2 b2 c2 T) b2 = T b2 ∧
    (fold3Step f a b c a2 b2 c2 T) c2 = T c2 := by
  refine ⟨?_, ?_, ?_⟩ <;> simp only [fold3Step]
  · rw [if_pos hpa, if_pos trivial]
  · rw [if_pos hpa, if_neg (Ne.symm h2ab), if_neg hb2a, if_neg hb2b,
      if_neg hb2c]
  · rw [if_pos hpa, if_neg (Ne.symm h2ac), if_neg hc2a, if_neg hc2b,
      if_neg hc2c]

/-- Phase 1: first output occupied, second blank. -/
theorem fold3Step_phase1 (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (h2ab : a2 ≠ b2) (h2ac : a2 ≠ c2) (h2bc : b2 ≠ c2)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c)
    (T : Fin tapes → Tape)
    (hpa : (T a2).head ≠ TapeSymbol.blank)
    (hpb : (T b2).head = TapeSymbol.blank) :
    (fold3Step f a b c a2 b2 c2 T) a2 = T a2 ∧
    (fold3Step f a b c a2 b2 c2 T) b2 =
      Tape.write (T b2)
        (TapeSymbol.bit (f (cellBool (T a).head) (cellBool (T b).head)
          (cellBool (T c).head))) ∧
    (fold3Step f a b c a2 b2 c2 T) c2 = T c2 := by
  refine ⟨?_, ?_, ?_⟩ <;> simp only [fold3Step]
  · rw [if_neg hpa, if_pos hpb, if_neg h2ab, if_neg ha2a, if_neg ha2b,
      if_neg ha2c]
  · rw [if_neg hpa, if_pos hpb, if_pos trivial]
  · rw [if_neg hpa, if_pos hpb, if_neg (Ne.symm h2bc), if_neg hc2a,
      if_neg hc2b, if_neg hc2c]

/-- Phase 2: both leading outputs occupied — write the third and advance all
three outputs. -/
theorem fold3Step_phase2 (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (h2ab : a2 ≠ b2) (h2ac : a2 ≠ c2) (h2bc : b2 ≠ c2)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c)
    (T : Fin tapes → Tape)
    (hpa : (T a2).head ≠ TapeSymbol.blank)
    (hpb : (T b2).head ≠ TapeSymbol.blank) :
    (fold3Step f a b c a2 b2 c2 T) a2 = moveDir HeadMove.right (T a2) ∧
    (fold3Step f a b c a2 b2 c2 T) b2 = moveDir HeadMove.right (T b2) ∧
    (fold3Step f a b c a2 b2 c2 T) c2 =
      moveDir HeadMove.right (Tape.write (T c2)
        (TapeSymbol.bit (f (cellBool (T a).head) (cellBool (T b).head)
          (cellBool (T c).head)))) := by
  refine ⟨?_, ?_, ?_⟩ <;> simp only [fold3Step]
  · rw [if_neg hpa, if_neg hpb, if_neg h2ac, if_pos trivial]
  · rw [if_neg hpa, if_neg hpb, if_neg h2bc, if_neg (Ne.symm h2ab),
      if_pos trivial]
  · rw [if_neg hpa, if_neg hpb, if_pos trivial]


/-! ## Three strides make a group -/

set_option maxHeartbeats 2000000 in
/-- **One group.**  From an aligned state — outputs at their frontiers —
three strides consume one cell of each input and deposit one combined cell
on each output, realigning. -/
theorem fold3Group (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (h2ab : a2 ≠ b2) (h2ac : a2 ≠ c2) (h2bc : b2 ≠ c2)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c)
    (T : Fin tapes → Tape)
    (x0 x1 x2 y0 y1 y2 z0 z1 z2 : TapeSymbol)
    (La Ra Lb Rb Lc Rc La2 Lb2 Lc2 : List TapeSymbol)
    (ha : T a = cellsTape La (x0 :: x1 :: x2 :: Ra))
    (hb : T b = cellsTape Lb (y0 :: y1 :: y2 :: Rb))
    (hc : T c = cellsTape Lc (z0 :: z1 :: z2 :: Rc))
    (ha2 : T a2 = cellsTape La2 [])
    (hb2 : T b2 = cellsTape Lb2 [])
    (hc2 : T c2 = cellsTape Lc2 []) :
    (((fold3Step f a b c a2 b2 c2)^[3]) T) a =
      cellsTape (x2 :: x1 :: x0 :: La) Ra ∧
    (((fold3Step f a b c a2 b2 c2)^[3]) T) b =
      cellsTape (y2 :: y1 :: y0 :: Lb) Rb ∧
    (((fold3Step f a b c a2 b2 c2)^[3]) T) c =
      cellsTape (z2 :: z1 :: z0 :: Lc) Rc ∧
    (((fold3Step f a b c a2 b2 c2)^[3]) T) a2 =
      cellsTape (TapeSymbol.bit (f (cellBool x0) (cellBool y0)
        (cellBool z0)) :: La2) [] ∧
    (((fold3Step f a b c a2 b2 c2)^[3]) T) b2 =
      cellsTape (TapeSymbol.bit (f (cellBool x1) (cellBool y1)
        (cellBool z1)) :: Lb2) [] ∧
    (((fold3Step f a b c a2 b2 c2)^[3]) T) c2 =
      cellsTape (TapeSymbol.bit (f (cellBool x2) (cellBool y2)
        (cellBool z2)) :: Lc2) [] := by
  have hI := fold3Step_inputs f a b c a2 b2 c2 hab hac hbc ha2a ha2b ha2c
    hb2a hb2b hb2c hc2a hc2b hc2c
  -- stride 1: phase 0
  have hph0 : (T a2).head = TapeSymbol.blank := by rw [ha2]; rfl
  obtain ⟨p0a2, p0b2, p0c2⟩ := fold3Step_phase0 f a b c a2 b2 c2 h2ab h2ac
    h2bc ha2a ha2b ha2c hb2a hb2b hb2c hc2a hc2b hc2c T hph0
  have s1a : (fold3Step f a b c a2 b2 c2 T) a =
      cellsTape (x0 :: La) (x1 :: x2 :: Ra) := by
    rw [(hI T).1, ha, cellsTape_moveRight_headD]
    rfl
  have s1b : (fold3Step f a b c a2 b2 c2 T) b =
      cellsTape (y0 :: Lb) (y1 :: y2 :: Rb) := by
    rw [(hI T).2.1, hb, cellsTape_moveRight_headD]
    rfl
  have s1c : (fold3Step f a b c a2 b2 c2 T) c =
      cellsTape (z0 :: Lc) (z1 :: z2 :: Rc) := by
    rw [(hI T).2.2, hc, cellsTape_moveRight_headD]
    rfl
  have s1a2 : (fold3Step f a b c a2 b2 c2 T) a2 =
      cellsTape La2 [TapeSymbol.bit (f (cellBool x0) (cellBool y0)
        (cellBool z0))] := by
    rw [p0a2, ha, hb, hc, ha2, write_cellsTape]
    rfl
  have s1b2 : (fold3Step f a b c a2 b2 c2 T) b2 = cellsTape Lb2 [] := by
    rw [p0b2, hb2]
  have s1c2 : (fold3Step f a b c a2 b2 c2 T) c2 = cellsTape Lc2 [] := by
    rw [p0c2, hc2]
  -- stride 2: phase 1
  set S1 := fold3Step f a b c a2 b2 c2 T with hS1
  have hph1a : (S1 a2).head ≠ TapeSymbol.blank := by
    rw [s1a2]; simp [cellsTape]
  have hph1b : (S1 b2).head = TapeSymbol.blank := by rw [s1b2]; rfl
  obtain ⟨p1a2, p1b2, p1c2⟩ := fold3Step_phase1 f a b c a2 b2 c2 h2ab h2ac
    h2bc ha2a ha2b ha2c hb2a hb2b hb2c hc2a hc2b hc2c S1 hph1a hph1b
  have s2a : (fold3Step f a b c a2 b2 c2 S1) a =
      cellsTape (x1 :: x0 :: La) (x2 :: Ra) := by
    rw [(hI S1).1, s1a, cellsTape_moveRight_headD]
    rfl
  have s2b : (fold3Step f a b c a2 b2 c2 S1) b =
      cellsTape (y1 :: y0 :: Lb) (y2 :: Rb) := by
    rw [(hI S1).2.1, s1b, cellsTape_moveRight_headD]
    rfl
  have s2c : (fold3Step f a b c a2 b2 c2 S1) c =
      cellsTape (z1 :: z0 :: Lc) (z2 :: Rc) := by
    rw [(hI S1).2.2, s1c, cellsTape_moveRight_headD]
    rfl
  have s2a2 : (fold3Step f a b c a2 b2 c2 S1) a2 =
      cellsTape La2 [TapeSymbol.bit (f (cellBool x0) (cellBool y0)
        (cellBool z0))] := by
    rw [p1a2, s1a2]
  have s2b2 : (fold3Step f a b c a2 b2 c2 S1) b2 =
      cellsTape Lb2 [TapeSymbol.bit (f (cellBool x1) (cellBool y1)
        (cellBool z1))] := by
    rw [p1b2, s1a, s1b, s1c, s1b2, write_cellsTape]
    rfl
  have s2c2 : (fold3Step f a b c a2 b2 c2 S1) c2 = cellsTape Lc2 [] := by
    rw [p1c2, s1c2]
  -- stride 3: phase 2
  set S2 := fold3Step f a b c a2 b2 c2 S1 with hS2
  have hph2a : (S2 a2).head ≠ TapeSymbol.blank := by
    rw [s2a2]; simp [cellsTape]
  have hph2b : (S2 b2).head ≠ TapeSymbol.blank := by
    rw [s2b2]; simp [cellsTape]
  obtain ⟨p2a2, p2b2, p2c2⟩ := fold3Step_phase2 f a b c a2 b2 c2 h2ab h2ac
    h2bc ha2a ha2b ha2c hb2a hb2b hb2c hc2a hc2b hc2c S2 hph2a hph2b
  have hit3 : ((fold3Step f a b c a2 b2 c2)^[3]) T =
      fold3Step f a b c a2 b2 c2 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 [(hI S2).1, s2a, cellsTape_moveRight_headD]
    rfl
  · rw [(hI S2).2.1, s2b, cellsTape_moveRight_headD]
    rfl
  · rw [(hI S2).2.2, s2c, cellsTape_moveRight_headD]
    rfl
  · rw [p2a2, s2a2, cellsTape_moveRight_headD]
    rfl
  · rw [p2b2, s2b2, cellsTape_moveRight_headD]
    rfl
  · rw [p2c2, s2a, s2b, s2c, s2c2, write_cellsTape,
      cellsTape_moveRight_headD]
    rfl


/-- A list of length `3(n+1)` starts with a triple. -/
theorem triple_dest (l : List TapeSymbol) (n : Nat)
    (hl : l.length = 3 * (n + 1)) :
    ∃ u0 u1 u2 l', l = u0 :: u1 :: u2 :: l' ∧ l'.length = 3 * n := by
  rcases l with _ | ⟨u0, _ | ⟨u1, _ | ⟨u2, l'⟩⟩⟩
  · simp at hl
  · simp at hl; omega
  · simp at hl; omega
  · exact ⟨u0, u1, u2, l', rfl, by simp at hl; omega⟩

set_option maxHeartbeats 4000000 in
/-- **The cascade level, accumulated.**  Over `t` groups the inputs are
consumed and each output collects every third combined cell. -/
theorem fold3_iterate (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (h2ab : a2 ≠ b2) (h2ac : a2 ≠ c2) (h2bc : b2 ≠ c2)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c) :
    ∀ (t : Nat) (as bs cs : List TapeSymbol) (T : Fin tapes → Tape)
      (La Ra Lb Rb Lc Rc La2 Lb2 Lc2 : List TapeSymbol),
      as.length = 3 * t → bs.length = 3 * t → cs.length = 3 * t →
      T a = cellsTape La (as ++ Ra) → T b = cellsTape Lb (bs ++ Rb) →
      T c = cellsTape Lc (cs ++ Rc) →
      T a2 = cellsTape La2 [] → T b2 = cellsTape Lb2 [] →
      T c2 = cellsTape Lc2 [] →
      (((fold3Step f a b c a2 b2 c2)^[3 * t]) T) a =
        cellsTape (as.reverse ++ La) Ra ∧
      (((fold3Step f a b c a2 b2 c2)^[3 * t]) T) b =
        cellsTape (bs.reverse ++ Lb) Rb ∧
      (((fold3Step f a b c a2 b2 c2)^[3 * t]) T) c =
        cellsTape (cs.reverse ++ Lc) Rc ∧
      (((fold3Step f a b c a2 b2 c2)^[3 * t]) T) a2 =
        cellsTape ((third0 (foldCells f as bs cs)).reverse ++ La2) [] ∧
      (((fold3Step f a b c a2 b2 c2)^[3 * t]) T) b2 =
        cellsTape ((third1 (foldCells f as bs cs)).reverse ++ Lb2) [] ∧
      (((fold3Step f a b c a2 b2 c2)^[3 * t]) T) c2 =
        cellsTape ((third2 (foldCells f as bs cs)).reverse ++ Lc2) [] := by
  intro t
  induction t with
  | zero =>
      intro as bs cs T La Ra Lb Rb Lc Rc La2 Lb2 Lc2 hla hlb hlc ha hb hc
        ha2 hb2 hc2
      have hae : as = [] := List.length_eq_zero_iff.mp (by simpa using hla)
      have hbe : bs = [] := List.length_eq_zero_iff.mp (by simpa using hlb)
      have hce : cs = [] := List.length_eq_zero_iff.mp (by simpa using hlc)
      subst hae
      subst hbe
      subst hce
      simp only [List.nil_append] at ha hb hc
      simp only [Nat.mul_zero, Function.iterate_zero_apply, List.reverse_nil,
        List.nil_append, foldCells_nil, third0, third1, third2]
      exact ⟨ha, hb, hc, ha2, hb2, hc2⟩
  | succ t ih =>
      intro as bs cs T La Ra Lb Rb Lc Rc La2 Lb2 Lc2 hla hlb hlc ha hb hc
        ha2 hb2 hc2
      obtain ⟨x0, x1, x2, as', rfl, hla'⟩ := triple_dest as t hla
      obtain ⟨y0, y1, y2, bs', rfl, hlb'⟩ := triple_dest bs t hlb
      obtain ⟨z0, z1, z2, cs', rfl, hlc'⟩ := triple_dest cs t hlc
      obtain ⟨ga, gb, gc, ga2, gb2, gc2⟩ := fold3Group f a b c a2 b2 c2
        hab hac hbc h2ab h2ac h2bc ha2a ha2b ha2c hb2a hb2b hb2c hc2a hc2b
        hc2c T x0 x1 x2 y0 y1 y2 z0 z1 z2 La (as' ++ Ra) Lb (bs' ++ Rb)
        Lc (cs' ++ Rc) La2 Lb2 Lc2
        (by rw [ha]; rfl) (by rw [hb]; rfl) (by rw [hc]; rfl) ha2 hb2 hc2
      obtain ⟨ka, kb, kc, ka2, kb2, kc2⟩ := ih as' bs' cs'
        (((fold3Step f a b c a2 b2 c2)^[3]) T)
        (x2 :: x1 :: x0 :: La) Ra (y2 :: y1 :: y0 :: Lb) Rb
        (z2 :: z1 :: z0 :: Lc) Rc
        (TapeSymbol.bit (f (cellBool x0) (cellBool y0) (cellBool z0)) :: La2)
        (TapeSymbol.bit (f (cellBool x1) (cellBool y1) (cellBool z1)) :: Lb2)
        (TapeSymbol.bit (f (cellBool x2) (cellBool y2) (cellBool z2)) :: Lc2)
        hla' hlb' hlc' ga gb gc ga2 gb2 gc2
      have hsplit : ((fold3Step f a b c a2 b2 c2)^[3 * (t + 1)]) T =
          ((fold3Step f a b c a2 b2 c2)^[3 * t])
            (((fold3Step f a b c a2 b2 c2)^[3]) T) := by
        rw [show 3 * (t + 1) = 3 * t + 3 by ring,
          Function.iterate_add_apply]
      rw [hsplit]
      refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
      · rw [ka]; simp
      · rw [kb]; simp
      · rw [kc]; simp
      · rw [ka2]
        show cellsTape _ _ = cellsTape _ _
        congr 1
        show (third0 (foldCells f as' bs' cs')).reverse ++ _ :: La2 = _
        rw [show foldCells f (x0 :: x1 :: x2 :: as') (y0 :: y1 :: y2 :: bs')
          (z0 :: z1 :: z2 :: cs') =
          TapeSymbol.bit (f (cellBool x0) (cellBool y0) (cellBool z0)) ::
          TapeSymbol.bit (f (cellBool x1) (cellBool y1) (cellBool z1)) ::
          TapeSymbol.bit (f (cellBool x2) (cellBool y2) (cellBool z2)) ::
          foldCells f as' bs' cs' from rfl]
        rw [show third0 (TapeSymbol.bit (f (cellBool x0) (cellBool y0)
          (cellBool z0)) ::
          TapeSymbol.bit (f (cellBool x1) (cellBool y1) (cellBool z1)) ::
          TapeSymbol.bit (f (cellBool x2) (cellBool y2) (cellBool z2)) ::
          foldCells f as' bs' cs') =
          TapeSymbol.bit (f (cellBool x0) (cellBool y0) (cellBool z0)) ::
          third0 (foldCells f as' bs' cs') from rfl]
        simp
      · rw [kb2]
        show cellsTape _ _ = cellsTape _ _
        congr 1
        show (third1 (foldCells f as' bs' cs')).reverse ++ _ :: Lb2 = _
        rw [show foldCells f (x0 :: x1 :: x2 :: as') (y0 :: y1 :: y2 :: bs')
          (z0 :: z1 :: z2 :: cs') =
          TapeSymbol.bit (f (cellBool x0) (cellBool y0) (cellBool z0)) ::
          TapeSymbol.bit (f (cellBool x1) (cellBool y1) (cellBool z1)) ::
          TapeSymbol.bit (f (cellBool x2) (cellBool y2) (cellBool z2)) ::
          foldCells f as' bs' cs' from rfl]
        rw [show third1 (TapeSymbol.bit (f (cellBool x0) (cellBool y0)
          (cellBool z0)) ::
          TapeSymbol.bit (f (cellBool x1) (cellBool y1) (cellBool z1)) ::
          TapeSymbol.bit (f (cellBool x2) (cellBool y2) (cellBool z2)) ::
          foldCells f as' bs' cs') =
          TapeSymbol.bit (f (cellBool x1) (cellBool y1) (cellBool z1)) ::
          third1 (foldCells f as' bs' cs') from rfl]
        simp
      · rw [kc2]
        show cellsTape _ _ = cellsTape _ _
        congr 1
        show (third2 (foldCells f as' bs' cs')).reverse ++ _ :: Lc2 = _
        rw [show foldCells f (x0 :: x1 :: x2 :: as') (y0 :: y1 :: y2 :: bs')
          (z0 :: z1 :: z2 :: cs') =
          TapeSymbol.bit (f (cellBool x0) (cellBool y0) (cellBool z0)) ::
          TapeSymbol.bit (f (cellBool x1) (cellBool y1) (cellBool z1)) ::
          TapeSymbol.bit (f (cellBool x2) (cellBool y2) (cellBool z2)) ::
          foldCells f as' bs' cs' from rfl]
        rw [show third2 (TapeSymbol.bit (f (cellBool x0) (cellBool y0)
          (cellBool z0)) ::
          TapeSymbol.bit (f (cellBool x1) (cellBool y1) (cellBool z1)) ::
          TapeSymbol.bit (f (cellBool x2) (cellBool y2) (cellBool z2)) ::
          foldCells f as' bs' cs') =
          TapeSymbol.bit (f (cellBool x2) (cellBool y2) (cellBool z2)) ::
          third2 (foldCells f as' bs' cs') from rfl]
        simp


/-- The first input's evolution is a plain rightward walk. -/
theorem fold3_a_iter (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c) :
    ∀ (r : Nat) (T : Fin tapes → Tape),
      (((fold3Step f a b c a2 b2 c2)^[r]) T) a =
        ((Tape.move · HeadMove.right)^[r]) (T a) := 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 (fold3Step f a b c a2 b2 c2 T),
        (fold3Step_inputs f a b c a2 b2 c2 hab hac hbc ha2a ha2b ha2c
          hb2a hb2b hb2c hc2a hc2b hc2c T).1]
      rfl

/-- The marks hypothesis: the first input reads non-blank until its run
ends, and blank at its end. -/
theorem fold3_marks (f : Bool → Bool → Bool → Bool)
    (a b c a2 b2 c2 : Fin tapes)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (ha2a : a2 ≠ a) (ha2b : a2 ≠ b) (ha2c : a2 ≠ c)
    (hb2a : b2 ≠ a) (hb2b : b2 ≠ b) (hb2c : b2 ≠ c)
    (hc2a : c2 ≠ a) (hc2b : c2 ≠ b) (hc2c : c2 ≠ c)
    (cs La Ra : List TapeSymbol) (T : Fin tapes → Tape)
    (hnb : ∀ x ∈ cs, x ≠ TapeSymbol.blank)
    (ha : T a = cellsTape La (cs ++ TapeSymbol.blank :: Ra)) :
    (∀ r, r < cs.length →
      ((((fold3Step f a b c a2 b2 c2)^[r]) T) a).head ≠
        TapeSymbol.blank) ∧
    ((((fold3Step f a b c a2 b2 c2)^[cs.length]) T) a).head =
      TapeSymbol.blank := by
  have hev := fold3_a_iter f a b c a2 b2 c2 hab hac hbc ha2a ha2b ha2c
    hb2a hb2b hb2c hc2a hc2b hc2c
  constructor
  · intro r hr
    rw [hev r T, ha]
    obtain ⟨L', hL'⟩ := moveRight_iterate_exists r La
      (cs ++ TapeSymbol.blank :: Ra)
    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 :: Ra).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, ha]
    obtain ⟨L', hL'⟩ := moveRight_iterate_exists cs.length La
      (cs ++ TapeSymbol.blank :: Ra)
    rw [hL']
    rw [List.drop_append_of_le_length (by omega)]
    rw [List.drop_length]
    rfl


/-- Lengths of the three residue classes, on triple-length lists. -/
theorem third_lengths : ∀ (t : Nat) (l : List TapeSymbol),
    l.length = 3 * t →
    (third0 l).length = t ∧ (third1 l).length = t ∧
      (third2 l).length = t := by
  intro t
  induction t with
  | zero =>
      intro l hl
      have : l = [] := List.length_eq_zero_iff.mp (by simpa using hl)
      subst this
      exact ⟨rfl, rfl, rfl⟩
  | succ t ih =>
      intro l hl
      obtain ⟨u0, u1, u2, l', rfl, hl'⟩ := triple_dest l t hl
      obtain ⟨h0, h1, h2⟩ := ih l' hl'
      refine ⟨?_, ?_, ?_⟩
      · show (u0 :: third0 l').length = t + 1
        simp [h0]
      · show (u1 :: third1 l').length = t + 1
        simp [h1]
      · show (u2 :: third2 l').length = t + 1
        simp [h2]

/-- Residue-class members come from the list. -/
theorem third_mem : ∀ (l : List TapeSymbol) (x : TapeSymbol),
    (x ∈ third0 l → x ∈ l) ∧ (x ∈ third1 l → x ∈ l) ∧
      (x ∈ third2 l → x ∈ l) := by
  intro l
  induction l using third0.induct with
  | case1 a d e r ih =>
      intro x
      obtain ⟨i0, i1, i2⟩ := ih x
      refine ⟨?_, ?_, ?_⟩
      · intro hx
        rcases List.mem_cons.mp hx with h | h
        · simp [h]
        · have := i0 h
          simp [this]
      · intro hx
        rcases List.mem_cons.mp hx with h | h
        · simp [h]
        · have := i1 h
          simp [this]
      · intro hx
        rcases List.mem_cons.mp hx with h | h
        · simp [h]
        · have := i2 h
          simp [this]
  | case2 a d =>
      intro x
      refine ⟨?_, ?_, ?_⟩
      · intro hx
        rcases List.mem_cons.mp hx with h | h
        · simp [h]
        · simp at h
      · intro hx
        rcases List.mem_cons.mp hx with h | h
        · simp [h]
        · simp at h
      · intro hx
        simp [third2] at hx
  | case3 a =>
      intro x
      refine ⟨?_, ?_, ?_⟩
      · intro hx
        rcases List.mem_cons.mp hx with h | h
        · simp [h]
        · simp at h
      · intro hx
        simp [third1] at hx
      · intro hx
        simp [third2] at hx
  | case4 =>
      intro x
      refine ⟨?_, ?_, ?_⟩ <;> intro hx <;> simp [third0, third1, third2] at hx

/-- Every combined cell is a bit. -/
theorem foldCells_nonblank (f : Bool → Bool → Bool → Bool) :
    ∀ (cs bs ds : List TapeSymbol), ∀ x ∈ foldCells f cs bs ds,
      x ≠ TapeSymbol.blank := by
  intro cs
  induction cs with
  | nil => intro bs ds x hx; simp [foldCells] at hx
  | cons c cs ih =>
      intro bs ds x hx
      rw [show foldCells f (c :: cs) bs ds =
        TapeSymbol.bit (f (cellBool c) (cellBool (bs.headD TapeSymbol.blank))
          (cellBool (ds.headD TapeSymbol.blank))) ::
          foldCells f cs bs.tail ds.tail from rfl] at hx
      rcases List.mem_cons.mp hx with h | h
      · rw [h]; simp
      · exact ih bs.tail ds.tail x h

end SipserGacsLautemann