proposition: Lemma skipn_app_app {X : Type} (l1 l2 l3 : list X) : skipn (length (l1 ++ l2)) (l1 ++ l3) = skipn (length l2) l3.
proof: Proof. rewrite skipn_app, app_length, skipn_all2 by lia. cbn. f_equal. lia. Qed.
imports: Undecidability.StackMachines.BSM Undecidability.StackMachines.Util.BSM_computable Undecidability.TM.TM Undecidability.TM.Util.TM_facts Undecidability.TM.Util.TM_computable Undecidability.TM(TM Arbitrary_to_Binary mTM_to_TM HaltTM_1_to_HaltKOSBTM HaltKOSBTM_to_HaltBSM) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Undecidability(bsm_utils bsm_defs) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes)