fact: Definition encode_tape (t : TM.tape (finType_CS bool)) : tape := match t with | TM.niltape => ([], false, []) | TM.leftof a rs => ([], false, flat_map encode_symbol (a :: rs)) | TM.rightof a ls => (false :: flat_map (fun a' => rev (encode_symbol a')) (a :: ls), false, []) | TM.midtape ls a rs => (a :: flat_map (fun a' => rev (encode_symbol a')) ls, true, flat_map encode_symbol rs) end.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun