sgl_sched13

import Definitions.Def_sgl_prologue13b

/-!
# The thirteen-tape assignment

Three inputs, four working tapes, clock, counter, guide — the ten the loop
knows — plus the seed and the ping-pong pair the prologue used and the loop
never touches.  The prologue's idle walker is the first working tape: a
stay-direction walk moves nothing, so the tape it never moves stays virgin,
which is exactly what the loop wants from it.
-/

namespace SipserGacsLautemann

/-- The loop's layout on thirteen tapes. -/
def sched13 : RoundLayout 13 where
  src := fun i => ⟨i.val, by omega⟩
  dst := fun j => ⟨3 + j.val, by omega⟩
  clk := ⟨7, by omega⟩
  cnt := ⟨8, by omega⟩

/-- The guide. -/
def sched13g : Fin 13 := ⟨9, by omega⟩

/-- The prologue's ten roles on these tapes. -/
def p13Idx : Fin 10 → Fin 13
  | 0 => ⟨0, by omega⟩
  | 1 => ⟨1, by omega⟩
  | 2 => ⟨2, by omega⟩
  | 3 => ⟨7, by omega⟩
  | 4 => ⟨9, by omega⟩
  | 5 => ⟨8, by omega⟩
  | 6 => ⟨10, by omega⟩
  | 7 => ⟨11, by omega⟩
  | 8 => ⟨12, by omega⟩
  | 9 => ⟨3, by omega⟩

theorem p13Idx_injective : Function.Injective p13Idx := by
  intro a b hab
  fin_cases a <;> fin_cases b <;> simp_all [p13Idx] <;>
    exact absurd (congrArg Fin.val hab) (by decide)

theorem sched13_wf : sched13.Wf := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · intro a b hab
    have := congrArg Fin.val hab
    simp [sched13] at this
    exact Fin.ext (by omega)
  · intro j hc
    have := congrArg Fin.val hc
    simp [sched13] at this
    omega
  · intro j hc
    have := congrArg Fin.val hc
    simp [sched13] at this
    omega
  · intro i j hc
    have := congrArg Fin.val hc
    simp [sched13] at this
    omega
  · intro hc
    have := congrArg Fin.val hc
    simp [sched13] at this

theorem sched13_src_clk : ∀ i, sched13.src i ≠ sched13.clk := by
  intro i hc
  have := congrArg Fin.val hc
  simp [sched13] at this
  omega

theorem sched13_src_cnt : ∀ i, sched13.src i ≠ sched13.cnt := by
  intro i hc
  have := congrArg Fin.val hc
  simp [sched13] at this
  omega

theorem sched13g_clk : sched13g ≠ sched13.clk := by
  intro hc
  have := congrArg Fin.val hc
  simp [sched13g, sched13] at this

theorem sched13g_cnt : sched13g ≠ sched13.cnt := by
  intro hc
  have := congrArg Fin.val hc
  simp [sched13g, sched13] at this

theorem sched13g_dst : ∀ j, sched13g ≠ sched13.dst j := by
  intro j hc
  have := congrArg Fin.val hc
  simp [sched13g, sched13] at this
  omega

theorem sched13g_src : ∀ i, sched13g ≠ sched13.src i := by
  intro i hc
  have := congrArg Fin.val hc
  simp [sched13g, sched13] at this
  omega

end SipserGacsLautemann