fact: Definition encode_tape (t : tape) : TM.tape (finType_CS bool) := match t with | (ls, a, rs) => TM.midtape ls a rs end.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun