proposition: Lemma PREP2_spec_strong (Σ : finType) i s b k' k'' v (v' : Vector.t nat k'') n (t : Vector.t (tape Σ) n) : (i, @PREP2' Σ s b k'' k' i n) // (i, ([] ::: Vector.map (fun n => repeat true n) v +++ Vector.const [] k'') +++ (@encode_bsm Σ _ (Vector.map (encNatTM s b) v' +++ t))) ->> (i + length(@PREP2' Σ s b k'' k' i n), ([] ::: Vector.const [] (k' + k'') +++ (@encode_bsm Σ _ (Vector.map (encNatTM s b) (v +++ v') +++ t)))).
proof: Proof. induction k' in k'', v, v', i |- *. - cbn. bsm sss stop. f_equal. 1: lia. f_equal. revert v. apply (Vector.case0). reflexivity. - unshelve edestruct (vector_inv_back v) as [(y, vl) Hv]. 1: abstract lia. cbn - [minus mult]. assert (k' < S k') as Hlt by lia. match goal with [ |- context[proj1_sig ?y]] => destruct y as [PREPIT [HlP HPREP]]; cbn [proj1_sig] end. eapply subcode_sss_compute_trans with (P := (i, _)). { cbn - [minus mult]. eexists [], _. cbn - [mult minus]. split. 1: reflexivity. now rewrite NPeano.Nat.add_0_r. } 1: cbn - [minus mult]. 1: cbn - [minus mult] in HPREP. 1: specialize HPREP with (m := v@[Fin.of_nat_lt Hlt]). 1: cbn [mult] in HPREP. Arguments Fin.of_nat_lt _ {_ _}. 1: refine (HPREP _ _ _). { rewrite <- !vec_pos_spec, <- !vec_map_spec, <- !vec_app_spec. eapply nth_error_vec_list. rewrite @vec_list_vec_app with (n := S k') (m := k''), vec_list_vec_map. rewrite nth_error_app1. 2: rewrite map_length, vec_list_length; lia. eapply map_nth_error. erewrite nth_error_vec_list. all:eapply (nth_error_nth' _ 0); rewrite vec_list_length; lia. } pose proof (@vec_list_vec_map nat (list bool)) as Heq. specialize (Heq) with (n := (S (k' + k''))). match goal with [ |- sss_compute _ _ (_, ?st) _ ] => evar (ev : vec (list bool) (S (S (k' + k'' + 4)))); enough (st = ev) as ->; subst ev end. 1: match goal with [ |- sss_compute _ _ _ (_, ?st) ] => evar (ev : vec (list bool) (S (S (k' + k'' + 4)))); enough (st = ev) as ->; subst ev end. 1: match goal with [ |- sss_compute _ _ _ (?st, _) ] => evar (ev : nat); enough (st = ev) as ->; subst ev end. 1: cbn - [minus mult] in HlP. 1: rewrite <- HlP. 1: eapply subcode_sss_compute with (P := (i + |PREPIT|, _)). { exists PREPIT, []. split. 2:reflexivity. now simpl_list. } 1: specialize IHk' with (v := vl) (v' := y ::: v') (k'' := S k''). 1: apply BSM_cast_spec. 1: eapply IHk'. + rewrite !app_length, BSM_cast_length, !PREP2'_length. setoid_rewrite PREP2'_length. clear. lia. + cbn. f_equal. eapply vec_list_inj. rewrite <- !vec_map_spec, <- !vec_app_spec. cbn [vec_list]. rewrite !vec_list_cast, !vec_list_vec_app, !vec_list_const. rewrite app_comm_cons. f_equal. 1: now replace (k' + S k'') with (S (k' + k'')) by lia. f_equal. subst v. rewrite !vec_app_spec. setoid_rewrite vec_map_spec. rewrite !Vector_map_app. pose proof (@Vector_map_app) as Vm. specialize Vm with (k1 := S k') (k2 := k''). cbn in Vm. rewrite Vm. clear Vm. eapply vec_list_inj, vec_list_encode_bsm. rewrite <- !vec_map_spec, <- !vec_app_spec. rewrite !vec_list_vec_app. setoid_rewrite <- vec_map_spec. rewrite !vec_list_vec_map. cbn[vec_list map]. pose proof (@vec_list_vec_app (tape Σ) (S (k' + k'')) n). cbn [plus] in H. rewrite H. clear H. pose proof (@vec_list_vec_app (tape Σ) (S k') k''). cbn [plus] in H. rewrite H. clear H. rewrite !vec_list_vec_map. cbn[vec_list map]. simpl_list. rewrite !vec_list_cast, vec_list_vec_app. cbn. simpl_list. reflexivity. + eapply vec_list_inj. rewrite <- !vec_map_spec, <- !vec_app_spec. cbn [vec_list]. rewrite !vec_list_cast. pose proof (@vec_list_vec_app (list bool) (S (k' + k'')) 4). cbn [plus] in H. rewrite !H. clear H. pose proof (@vec_list_vec_app (list bool) (S (k' + S k'')) 4). cbn [plus] in H. rewrite !H. clear H. cbn [vec_list app]. f_equal. rewrite !vec_list_vec_app. cbn [Vector.map]. rewrite vec_app_cons. f_equal. 2:{ f_equal. f_equal. f_equal. subst v. f_equal. rewrite <- vec_pos_spec. eapply nth_error_vec_list. rewrite vec_list_cast, <- vec_app_spec, vec_list_vec_app, nth_error_app2; rewrite !vec_list_length, ?Nat.sub_diag; try lia. reflexivity. } rewrite vec_list_vec_change. pose proof (@vec_list_vec_app (list bool) (S k') k''). cbn [plus] in H. rewrite !H. clear H. setoid_rewrite <- vec_map_spec. rewrite !vec_list_vec_map, !vec_list_const. rewrite update_app_left. 2: rewrite Fin.to_nat_of_nat; cbn; rewrite map_length, vec_list_length; lia. subst v. rewrite vec_list_cast. rewrite <- vec_app_spec. rewrite vec_list_vec_app. cbn [vec_list]. rewrite Fin.to_nat_of_nat. cbn. rewrite map_app, update_app_right. 2: rewrite map_length, vec_list_length; lia. rewrite map_length, vec_list_length, Nat.sub_diag. cbn. now simpl_list. 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)