fact: Definition mv (m : move) (t : tape) := match m, t with | Lmove, rightof l ls => midtape ls l nil | Lmove, midtape nil m rs => leftof m rs | Lmove, midtape (l :: ls) m rs => midtape ls l (m :: rs) | Rmove, leftof r rs => midtape nil r rs | Rmove, midtape ls m nil => rightof m ls | Rmove, midtape ls m (r :: rs) => midtape (m :: ls) r rs | _, _ => t end.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List