proposition: Lemma encode_bsm_nil (Σ : finType) n : { '(str2, n') | forall (t : Vector.t (tape Σ) n), (encode_bsm Σ (niltape ::: t))@[Fin2] = str2 ++ (skipn n' ((encode_bsm Σ t)@[Fin2]))}.
proof: Proof. eexists ((encode_sym _ ++ true :: false :: encode_sym _ ++ true :: false :: encode_sym _), _). intros t. cbn. rewrite skipn_app'. 2: now rewrite length_encode_sym. assert (Hreorder : forall l1 l2 l3 l4, l1 ++ true :: false :: l2 ++ true :: false :: l3 ++ true :: l4 = (l1 ++ true :: false :: l2 ++ true :: false :: l3) ++ true :: l4). { intros. now repeat (rewrite <- app_assoc; cbn). } apply Hreorder. 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)