fact: Definition wr (s : option Σ) (t : tape) : tape := match s, t with | None, t => t | Some a, niltape => midtape nil a nil | Some a, leftof r rs => midtape nil a (r :: rs) | Some a, midtape ls b rs => midtape ls a rs | Some a, rightof l ls => midtape (l :: ls) a nil end.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List