proposition: Lemma PREP2_spec k (Σ : finType) i s b n : { PREP2 | forall v (t : Vector.t (tape Σ) n), (i, PREP2) // (i, ([] ::: Vector.map (fun n => repeat true n) v) +++ (@encode_bsm Σ _ t)) ->> (i + length PREP2, ([] ::: Vector.const [] k +++ (@encode_bsm Σ _ (Vector.map (encNatTM s b) v +++ t)))) }.
proof: Proof. unshelve eexists (BSM_cast (@PREP2' Σ s b 0 k i n) _). 1: abstract lia. intros v t. match goal with [ |- sss_compute _ _ (_, ?st) _ ] => evar (ev : vec (list bool) (S k + 4)); enough (st = ev) as ->; subst ev end. 1: match goal with [ |- sss_compute _ _ _ (_, ?st) ] => evar (ev : vec (list bool) (S k + 4)); enough (st = ev) as ->; subst ev end. 1: rewrite <- BSM_cast_spec. 1: rewrite BSM_cast_length. 1: eapply PREP2_spec_strong. - eapply vec_list_inj. rewrite <- !vec_app_spec. cbn. rewrite vec_list_cast, !vec_list_vec_app, !vec_list_const. f_equal. f_equal. 1: now rewrite NPeano.Nat.add_0_r. eapply vec_list_encode_bsm. Unshelve. 3: exact [| |]. 2: exact v. 2: exact t. rewrite <- !vec_map_spec, !vec_list_vec_app, !vec_list_vec_map, !vec_list_vec_app. cbn. now rewrite app_nil_r. - eapply vec_list_inj. rewrite <- !vec_app_spec, <- !vec_map_spec, !vec_app_cons, vec_list_cast. cbn. f_equal. rewrite !vec_list_vec_app. f_equal. 1: cbn. 1: now simpl_list. eapply vec_list_encode_bsm. f_equal. eapply vec_pos_ext. intros. now rewrite vec_pos_set. 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)