proposition: Lemma PREP_spec k n Σ s b : { PREP | forall v : Vector.t nat k, (0, PREP) // (0, Vector.append ([] ::: Vector.map (fun n0 : nat => repeat true n0) v) (Vector.const [] 4)) ->> (length PREP, Vector.append (Vector.const [] (1 + k)) ((@encode_bsm Σ _ (Vector.append (niltape ::: Vector.map (encNatTM s b) v) (Vector.const niltape n))))) }.
proof: Proof. destruct (PREP1_spec k Σ n) as [PREP1 H1]. destruct (@PREP2_spec k Σ (length PREP1) s b n) as [PREP2 H2]. destruct (@PREP3_spec (1 + k) (k + n) Σ (length PREP1 + length PREP2)) as [PREP3 H3]. exists (PREP1 ++ PREP2 ++ PREP3). intros v. eapply subcode_sss_compute_trans. 2: eapply H1. 1: auto. eapply subcode_sss_compute_trans. 2: eapply H2. 1: auto. eapply subcode_sss_compute_trans. 2: specialize H3 with (v := [] ## Vector.const [] k); apply H3. 1: auto. bsm sss stop. f_equal. rewrite !app_length. now rewrite Nat.add_assoc. 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)