fact: Definition mv (m : move) (t : tape) := match m with | Lmove => match left t, curr t with | l :: ls, None => (ls, Some l, right t) | l :: ls, Some c => (ls, Some l, c :: right t) | [], Some c => ([], None, c :: right t) | _, _ => t end | Rmove => match curr t, right t with | None, r :: rs => (left t, Some r, rs) | Some c, r :: rs => (c :: left t, Some r, rs) | Some c, [] => (c :: left t, None, []) | _ , _ => t end | Nmove => t end.
imports: List Bool Nat