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