proposition: Theorem bounded_M_to_terminating_P : CM.halting P (Nat.iter NM (CM.step P) cm_start).
proof: Proof. Proof using NM NM_spec capped_P. rewrite /CM.halting. move HNM: (Nat.iter NM (CM.step P) cm_start) => cm_end. have : CM.step P cm_end = cm_end \/ CM.step P cm_end <> cm_end by do 2 (decide equality). case; first done. move=> He. exfalso. have /CM_facts.acyclicity : not (CM.halting P (Nat.iter NM (CM.step P) cm_start)) by rewrite HNM. set f := (fun i : nat => Nat.iter i (CM1.step P) cm_start). have ->: 2 + NM = S NM + 1 by lia. rewrite seq_app map_app. move /(@NoDup_remove CM1.Config) => [+ _]. rewrite app_nil_r. have [L [H1L H2L]] := NM_spec ([§1], [§0] ++ [§1] ++ §0^(CM.value cm_end - 1), '#?0). set g : _ -> SM.Config := (fun X => ([§1], §0^(CM.value X) ++ [§1] ++ §0^(CM.value cm_end - (CM.value X)), '#? (CM.state X))). have /(NoDup_map (f := g)) /[apply]: injective g. { move=> [p1 v1] [p2 v2]. rewrite /g /=. by move=> [] /zero_prefix_eq => -> ->. } set L' := (map g (map f (seq 0 (1 + NM)))). move=> HL'. have /(NoDup_incl_length HL') : incl L' L. { move=> x + /ltac:(apply: H1L). rewrite /L' in_map_iff. move=> [X] [<-]. rewrite in_map_iff. move=> [i] [<-]. rewrite in_seq. move=> [_ ?]. rewrite /f /g. have [N HN] := search_bound (CM.value cm_end) NM ltac:(rewrite HNM; lia). have := CM_facts.run_value_monotone P cm_start i. set Y := (Nat.iter i (CM1.step P) cm_start). have ? : CM.value Y <= CM.value cm_end. { rewrite /Y -HNM. apply: CM_facts.value_monotone. by lia. } move=> H1Y. rewrite /cm_start /= in H1Y. have /= := iter_cm_step HN [] (§0^(CM.value cm_end - CM.value Y)) i. rewrite -/Y ?app_norm. move /(_ ltac:(lia)) /reachable_n_reachable. congr (SM.reachable). do 5 f_equal. by lia. } rewrite /L' ?map_length seq_length. by lia. Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun