sgl_fold_walk

import Definitions.Def_sgl_xor_walk
import Definitions.Def_sgl_ss_tapes

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

Three tapes advance in step; a fourth receives, cell by cell, a combination
of the three heads.  With the combiner as majority this is one level of the
ternary vote; with a constant mark it divides a tally by three.  The walk
stops at the first tape's blank, so the first tape's run measures the
strides.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- One stride: write the combination, advance all four heads. -/
def foldStep (f : Bool → Bool → Bool → Bool) (a b c out : Fin tapes)
    (T : Fin tapes → Tape) : Fin tapes → Tape :=
  fun i =>
    if i = out then
      moveDir HeadMove.right
        (Tape.write (T out)
          (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

/-- The stride's action. -/
def foldAction (f : Bool → Bool → Bool → Bool) (a b c out : Fin tapes) :
    (Fin tapes → TapeSymbol) → Fin tapes → TapeSymbol × HeadMove :=
  fun symbols i =>
    if i = out then
      (TapeSymbol.bit (f (cellBool (symbols a)) (cellBool (symbols b))
        (cellBool (symbols c))), 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 fold. -/
def foldBody (f : Bool → Bool → Bool → Bool) (a b c out : Fin tapes) :=
  (TypedMachine.test (notBlankAt a)).andThen fun v =>
    if v then
      (TypedMachine.act (foldAction f a b c out)).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 fold: one stride per mark on the first tape. -/
noncomputable def foldWalk (f : Bool → Bool → Bool → Bool)
    (a b c out : Fin tapes) := (foldBody f a b c out).repeatUntilFalse

theorem foldStep_eq (f : Bool → Bool → Bool → Bool) (a b c out : Fin tapes)
    (hoa : out ≠ a) (hob : out ≠ b) (hoc : out ≠ c)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (T : Fin tapes → Tape) :
    applyAction T (foldAction f a b c out) = foldStep f a b c out T := by
  funext i
  show applyAction T (foldAction f a b c out) i =
    (if i = out then
      moveDir HeadMove.right
        (Tape.write (T out)
          (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)
  by_cases hio : i = out
  · subst hio
    simp [applyAction, foldAction, moveDir]
  · rw [if_neg hio]
    by_cases hia : i = a
    · subst hia
      simp [applyAction, foldAction, hio, Tape.write_head_self, moveDir]
    · rw [if_neg hia]
      by_cases hib : i = b
      · subst hib
        simp [applyAction, foldAction, hio, hia,
          Tape.write_head_self, moveDir]
      · rw [if_neg hib]
        by_cases hic : i = c
        · subst hic
          simp [applyAction, foldAction, hio, hia, hib,
            Tape.write_head_self, moveDir]
        · rw [if_neg hic]
          simp [applyAction, foldAction, hio, hia, hib, hic,
            Tape.write_head_self, Tape.move]

set_option maxHeartbeats 1000000 in
/-- A round on a marked first tape. -/
theorem foldBody_mark (f : Bool → Bool → Bool → Bool) (a b c out : Fin tapes)
    (hoa : out ≠ a) (hob : out ≠ b) (hoc : out ≠ c)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (T : Fin tapes → Tape)
    (hmark : (T a).head ≠ TapeSymbol.blank) :
    HaltsExactly (foldBody f a b c out) ((foldBody f a b c out).startCfg T)
      (1 + 1 + (1 + 1 + 0)) true ∧
    (((foldBody f a b c out).step^[1 + 1 + (1 + 1 + 0)])
      ((foldBody f a b c out).startCfg T)).tape = foldStep f a b c out 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 (foldAction f a b c out) T
  have hactt : (((TypedMachine.act (foldAction f a b c out)).step^[1])
      ((TypedMachine.act (foldAction f a b c out)).startCfg T)).tape =
      foldStep f a b c out T := by
    rw [Function.iterate_one, ← foldStep_eq f a b c out hoa hob hoc hab hac
      hbc]
    funext j
    simp [TypedMachine.step, TypedMachine.act, TypedMachine.startCfg,
      applyAction]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) true
    ((TypedMachine.halt (tapes := tapes) true).startCfg
      (foldStep f a b c out T))
  have hinner := chainStepC hact hactt hhalt
  have hmain := chainStepD
    (M₂ := fun v =>
      if v then
        (TypedMachine.act (foldAction f a b c out)).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' : ((foldBody f a b c out).step^[1 + 1 + (1 + 1 + 0)])
      ((foldBody f a b c out).startCfg T) = _ := hfin
  rw [hfin']
  show (TypedConfiguration.inRight true
    ((((TypedMachine.act (foldAction f a b c out)).andThen fun _ =>
      TypedMachine.halt (tapes := tapes) true).step^[1 + 1 + 0])
      (((TypedMachine.act (foldAction f a b c out)).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) true).startCfg T))).tape =
    foldStep f a b c out T
  have hi := hinner.2
  rw [hi]
  show ((TypedMachine.halt (tapes := tapes) true).step^[0]
    ((TypedMachine.halt (tapes := tapes) true).startCfg
      (foldStep f a b c out T))).tape = foldStep f a b c out T
  rfl

set_option maxHeartbeats 1000000 in
/-- A round on a blank first tape. -/
theorem foldBody_blank (f : Bool → Bool → Bool → Bool) (a b c out : Fin tapes)
    (T : Fin tapes → Tape)
    (hblank : (T a).head = TapeSymbol.blank) :
    HaltsExactly (foldBody f a b c out) ((foldBody f a b c out).startCfg T)
      (1 + 1 + (1 + 1 + 0)) false ∧
    (((foldBody f a b c out).step^[1 + 1 + (1 + 1 + 0)])
      ((foldBody f a b c out).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 (foldAction f a b c out)).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' : ((foldBody f a b c out).step^[1 + 1 + (1 + 1 + 0)])
      ((foldBody f a b c out).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 fold walk.**  With marks under the first head for `m` strides and
a blank at exit, the walk halts false and leaves `foldStep`'s iterate. -/
theorem foldWalk_spec (f : Bool → Bool → Bool → Bool) (a b c out : Fin tapes)
    (hoa : out ≠ a) (hob : out ≠ b) (hoc : out ≠ c)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (m : Nat) (T : Fin tapes → Tape)
    (hmarks : ∀ r, r < m →
      ((((foldStep f a b c out)^[r]) T) a).head ≠ TapeSymbol.blank)
    (hexit : ((((foldStep f a b c out)^[m]) T) a).head = TapeSymbol.blank) :
    HaltsExactly (foldWalk f a b c out)
      ((foldWalk f a b c out).startCfg T) (m * 5 + 4) false ∧
    (((foldWalk f a b c out).step^[m * 5 + 4])
      ((foldWalk f a b c out).startCfg T)).tape =
      ((foldStep f a b c out)^[m]) T := by
  classical
  set body := foldBody f a b c out with hbody
  set cfg : Nat → TypedConfiguration tapes _ :=
    fun r => body.startCfg (((foldStep f a b c out)^[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⟩ := foldBody_mark f a b c out hoa hob hoc hab hac hbc
      (((foldStep f a b c out)^[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 =
        ((foldStep f a b c out)^[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 (((foldStep f a b c out)^[r + 1]) T) = _
    rw [← ht4]
    rfl
  have hexitr : HaltsExactly body (cfg m) 4 false := by
    have := (foldBody_blank f a b c out (((foldStep f a b c out)^[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 : (foldWalk f a b c out).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 ((foldWalk f a b c out).step^[4]
    (((foldWalk f a b c out).step^[m * (4 + 1)]) (cfg 0))).tape = _
  rw [show (foldWalk f a b c out) = 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 (foldBody_blank f a b c out (((foldStep f a b c out)^[m]) T)
    hexit).2


/-! ## The caller-facing form -/

/-- The written run: one combined cell per stride of the first tape, the
second and third padding with blanks — read as `false` — when exhausted. -/
def foldCells (f : Bool → Bool → Bool → Bool) :
    List TapeSymbol → List TapeSymbol → List TapeSymbol → List TapeSymbol
  | [], _, _ => []
  | 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

@[simp] theorem foldCells_nil (f : Bool → Bool → Bool → Bool)
    (bs ds : List TapeSymbol) : foldCells f [] bs ds = [] := rfl

theorem foldCells_length (f : Bool → Bool → Bool → Bool) :
    ∀ (cs bs ds : List TapeSymbol),
      (foldCells f cs bs ds).length = cs.length := by
  intro cs
  induction cs with
  | nil => intro bs ds; rfl
  | cons c cs ih => intro bs ds; simp [foldCells, ih]

/-- One stride, in `cellsTape` form. -/
theorem foldStep_tapes (f : Bool → Bool → Bool → Bool)
    (a b c out : Fin tapes)
    (hoa : out ≠ a) (hob : out ≠ b) (hoc : out ≠ c)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (T : Fin tapes → Tape) (ca : TapeSymbol)
    (La Ra Lb Rbs Lc Rcs Lo Ro : List TapeSymbol)
    (ha : T a = cellsTape La (ca :: Ra)) (hb : T b = cellsTape Lb Rbs)
    (hc : T c = cellsTape Lc Rcs) (ho : T out = cellsTape Lo Ro) :
    (foldStep f a b c out T) a = cellsTape (ca :: La) Ra ∧
    (foldStep f a b c out T) b =
      cellsTape (Rbs.headD TapeSymbol.blank :: Lb) Rbs.tail ∧
    (foldStep f a b c out T) c =
      cellsTape (Rcs.headD TapeSymbol.blank :: Lc) Rcs.tail ∧
    (foldStep f a b c out T) out = cellsTape
      (TapeSymbol.bit (f (cellBool ca)
        (cellBool (Rbs.headD TapeSymbol.blank))
        (cellBool (Rcs.headD TapeSymbol.blank))) :: Lo) Ro.tail := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · show (if a = out then _ else if a = a then _ else _) = _
    rw [if_neg (Ne.symm hoa), if_pos rfl, ha, cellsTape_moveRight_headD]
    rfl
  · show (if b = out then _ else if b = a then _
      else if b = b then _ else _) = _
    rw [if_neg (Ne.symm hob), if_neg (Ne.symm hab), if_pos rfl, hb,
      cellsTape_moveRight_headD]
  · show (if c = out then _ else if c = a then _ else if c = b then _
      else if c = c then _ else _) = _
    rw [if_neg (Ne.symm hoc), if_neg (Ne.symm hac), if_neg (Ne.symm hbc),
      if_pos rfl, hc, cellsTape_moveRight_headD]
  · show (if out = out then _ else _) = _
    rw [if_pos rfl, ha, hb, hc, ho]
    show moveDir HeadMove.right (Tape.write (cellsTape Lo Ro)
      (TapeSymbol.bit (f (cellBool (cellsTape La (ca :: Ra)).head)
        (cellBool (cellsTape Lb Rbs).head)
        (cellBool (cellsTape Lc Rcs).head)))) = _
    rw [show (cellsTape La (ca :: Ra)).head = ca from rfl,
      show (cellsTape Lb Rbs).head = Rbs.headD TapeSymbol.blank from rfl,
      show (cellsTape Lc Rcs).head = Rcs.headD TapeSymbol.blank from rfl,
      write_cellsTape]
    exact cellsTape_moveRight Lo _ Ro.tail

/-- **The fold, accumulated.** -/
theorem foldStep_iterate (f : Bool → Bool → Bool → Bool)
    (a b c out : Fin tapes)
    (hoa : out ≠ a) (hob : out ≠ b) (hoc : out ≠ c)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) :
    ∀ (cs : List TapeSymbol) (T : Fin tapes → Tape)
      (La Ra Lb Rbs Lc Rcs Lo Ro : List TapeSymbol),
      T a = cellsTape La (cs ++ Ra) → T b = cellsTape Lb Rbs →
      T c = cellsTape Lc Rcs → T out = cellsTape Lo Ro →
      (((foldStep f a b c out)^[cs.length]) T) a =
        cellsTape (cs.reverse ++ La) Ra ∧
      (((foldStep f a b c out)^[cs.length]) T) out =
        cellsTape ((foldCells f cs Rbs Rcs).reverse ++ Lo)
          (Ro.drop cs.length) ∧
      (∃ Lb', (((foldStep f a b c out)^[cs.length]) T) b =
        cellsTape Lb' (Rbs.drop cs.length)) ∧
      (∃ Lc', (((foldStep f a b c out)^[cs.length]) T) c =
        cellsTape Lc' (Rcs.drop cs.length)) := by
  intro cs
  induction cs with
  | nil =>
      intro T La Ra Lb Rbs Lc Rcs Lo Ro ha hb hc ho
      exact ⟨by simpa using ha, by simpa using ho, ⟨Lb, by simpa using hb⟩,
        ⟨Lc, by simpa using hc⟩⟩
  | cons c0 cs ih =>
      intro T La Ra Lb Rbs Lc Rcs Lo Ro ha hb hc ho
      rw [List.length_cons, Function.iterate_succ_apply]
      obtain ⟨ha', hb', hc', ho'⟩ := foldStep_tapes f a b c out hoa hob hoc
        hab hac hbc T c0 La (cs ++ Ra) Lb Rbs Lc Rcs Lo Ro
        (by rw [ha]; rfl) hb hc ho
      obtain ⟨ka, ko, ⟨Lb', kb⟩, ⟨Lc', kc⟩⟩ := ih (foldStep f a b c out T)
        (c0 :: La) Ra (Rbs.headD TapeSymbol.blank :: Lb) Rbs.tail
        (Rcs.headD TapeSymbol.blank :: Lc) Rcs.tail
        (TapeSymbol.bit (f (cellBool c0)
          (cellBool (Rbs.headD TapeSymbol.blank))
          (cellBool (Rcs.headD TapeSymbol.blank))) :: Lo) Ro.tail
        ha' hb' hc' ho'
      refine ⟨?_, ?_, ⟨Lb', ?_⟩, ⟨Lc', ?_⟩⟩
      · rw [ka]
        show cellsTape _ Ra = cellsTape _ Ra
        congr 1
        simp
      · rw [ko]
        show cellsTape _ _ = cellsTape _ _
        congr 1
        · show (foldCells f cs Rbs.tail Rcs.tail).reverse ++ _ :: Lo = _
          rw [show foldCells f (c0 :: cs) Rbs Rcs =
            TapeSymbol.bit (f (cellBool c0)
              (cellBool (Rbs.headD TapeSymbol.blank))
              (cellBool (Rcs.headD TapeSymbol.blank))) ::
              foldCells f cs Rbs.tail Rcs.tail from rfl]
          simp
        · cases Ro with
          | nil => simp
          | cons r rest => rfl
      · rw [kb]
        congr 1
        cases Rbs with
        | nil => simp
        | cons x rest => rfl
      · rw [kc]
        congr 1
        cases Rcs with
        | nil => simp
        | cons x rest => rfl

/-- The marks hypothesis: the first tape reads non-blank until its run ends. -/
theorem foldStep_marks (f : Bool → Bool → Bool → Bool)
    (a b c out : Fin tapes)
    (hoa : out ≠ a) (hob : out ≠ b) (hoc : out ≠ c)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) :
    ∀ (cs : List TapeSymbol) (T : Fin tapes → Tape)
      (La Ra Lb Rbs Lc Rcs Lo Ro : List TapeSymbol),
      (∀ x ∈ cs, x ≠ TapeSymbol.blank) →
      T a = cellsTape La (cs ++ Ra) → T b = cellsTape Lb Rbs →
      T c = cellsTape Lc Rcs → T out = cellsTape Lo Ro →
      ∀ r, r < cs.length →
        ((((foldStep f a b c out)^[r]) T) a).head ≠ TapeSymbol.blank := by
  intro cs
  induction cs with
  | nil => intro _ _ _ _ _ _ _ _ _ _ _ _ _ _ r hr; simp at hr
  | cons c0 cs ih =>
      intro T La Ra Lb Rbs Lc Rcs Lo Ro hnb ha hb hc ho r hr
      cases r with
      | zero =>
          rw [Function.iterate_zero_apply, ha]
          exact hnb c0 (by simp)
      | succ r =>
          obtain ⟨ha', hb', hc', ho'⟩ := foldStep_tapes f a b c out hoa hob
            hoc hab hac hbc T c0 La (cs ++ Ra) Lb Rbs Lc Rcs Lo Ro
            (by rw [ha]; rfl) hb hc ho
          rw [Function.iterate_succ_apply]
          exact ih (foldStep f a b c out T) _ Ra _ Rbs.tail _ Rcs.tail _
            Ro.tail (fun x hx => hnb x (by simp [hx])) ha' hb' hc' ho' r
            (by simpa using hr)

/-- Other tapes are untouched. -/
theorem foldStep_other (f : Bool → Bool → Bool → Bool)
    (a b c out : Fin tapes) :
    ∀ (m : Nat) (T : Fin tapes → Tape) (j : Fin tapes),
      j ≠ a → j ≠ b → j ≠ c → j ≠ out →
      (((foldStep f a b c out)^[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 hjo
      rw [Function.iterate_succ_apply]
      have hstep : (foldStep f a b c out T) j = T j := by
        show (if j = out then _ else if j = a then _ else if j = b then _
          else if j = c then _ else T j) = T j
        rw [if_neg hjo, if_neg hja, if_neg hjb, if_neg hjc]
      rw [ih (foldStep f a b c out T) j hja hjb hjc hjo, hstep]


/-! ## The caller-facing form -/

/-- The inputs advance every stride. -/

theorem foldStep_inputs (f : Bool → Bool → Bool → Bool)
    (a b c out : Fin tapes)
    (hoa : out ≠ a) (hob : out ≠ b) (hoc : out ≠ c)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (T : Fin tapes → Tape) :
    (foldStep f a b c out T) a = moveDir HeadMove.right (T a) ∧
    (foldStep f a b c out T) b = moveDir HeadMove.right (T b) ∧
    (foldStep f a b c out T) c = moveDir HeadMove.right (T c) ∧
    (foldStep f a b c out T) out =
      moveDir HeadMove.right
        (Tape.write (T out)
          (TapeSymbol.bit (f (cellBool (T a).head) (cellBool (T b).head)
            (cellBool (T c).head)))) := by
  refine ⟨?_, ?_, ?_, ?_⟩ <;> simp only [foldStep]
  · rw [if_neg (Ne.symm hoa), if_pos trivial]
  · rw [if_neg (Ne.symm hob), if_neg (Ne.symm hab), if_pos trivial]
  · rw [if_neg (Ne.symm hoc), if_neg (Ne.symm hac), if_neg (Ne.symm hbc),
      if_pos trivial]
  · rw [if_pos trivial]

/-- Other tapes are untouched. -/
theorem foldStep_other_one (f : Bool → Bool → Bool → Bool)
    (a b c out : Fin tapes) (T : Fin tapes → Tape) (j : Fin tapes)
    (hja : j ≠ a) (hjb : j ≠ b) (hjc : j ≠ c) (hjo : j ≠ out) :
    (foldStep f a b c out T) j = T j := by
  simp only [foldStep]
  rw [if_neg hjo, if_neg hja, if_neg hjb, if_neg hjc]

/-- The first input's evolution is a plain rightward walk. -/
theorem foldStep_a_iter (f : Bool → Bool → Bool → Bool)
    (a b c out : Fin tapes)
    (hoa : out ≠ a) (hob : out ≠ b) (hoc : out ≠ c)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) :
    ∀ (r : Nat) (T : Fin tapes → Tape),
      (((foldStep f a b c out)^[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 (foldStep f a b c out T),
        (foldStep_inputs f a b c out hoa hob hoc hab hac hbc T).1]
      rfl

end SipserGacsLautemann