fact: Definition canonize_tape (t : TM.tape (finType_CS bool)) := match t with | TM.niltape => TM.midtape [] false [] | TM.leftof r rs => TM.midtape [] false (r :: rs) | TM.rightof l ls => TM.midtape (l :: ls) false [] | _ => t end.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun