proposition: Lemma PREP2'_length (Σ : finType) (s b : Σ) k (k' : nat) (i : nat) n : | @PREP2' Σ s b k k' i n| = k' * PREP2''_length s b.
proof: Proof. induction k' in k, i |- *. - cbn. reflexivity. - cbn - [mult]. destruct PREP2_spec' as (? & ? & ?). cbn. rewrite app_length. cbn in e. rewrite e. rewrite BSM_cast_length. cbn in IHk'. rewrite IHk'. 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)