sgl_offset_input

import Definitions.Def_sgl_round_spec

/-!
# The delegate's input at an offset

The offset is fed to the delegate as the fourth input, in unary, exactly as
the mission's predicate names it.  A round's content is that input rendered in
cells, which is the bridge between the scheduler's tapes and the statement the
delegate's correctness is given for.
-/

namespace SipserGacsLautemann

variable {states : Nat}

/-- The delegate's input at a given offset. -/
def offsetInput (input : Fin 3 → List Bool) (m : Nat) : Fin 4 → List Bool :=
  fun j => if j = 0 then input 0 else if j = 1 then input 1
    else if j = 2 then input 2 else List.replicate m true

/-- A round's content is the delegate's input, in cells. -/
theorem roundContent_offsetInput (input : Fin 3 → List Bool) (m : Nat)
    (j : Fin 4) :
    roundContent (fun i => (input i).map TapeSymbol.bit) m j =
      (offsetInput input m j).map TapeSymbol.bit := by
  fin_cases j
  · rfl
  · rfl
  · rfl
  · show List.replicate m (TapeSymbol.bit true) = _
    show _ = (List.replicate m true).map TapeSymbol.bit
    rw [List.map_replicate]

end SipserGacsLautemann