proposition: Lemma maybe_index_try_stop l m z T : maybe_index_try_stop_time <= T -> maybe_reachable T ([§1] ++ l, §0^1 ++ [§1] ++ §0^m, '#?0) z.
proof: Proof. Proof using NP_spec. move /maybe_reachable_mon'. apply; first by reflexivity. rewrite /maybe_index_try_stop_time. have [? | Hm]: CP - 1 <= m \/ m < CP - 1 by lia. { have := maybe_index_try_run l (§0^(m - (CP - 1))) z. apply: maybe_reachable_mon'; [by nia | by rewrite ?app_norm; do 6 f_equal; lia ]. } set T' := ((G + CP + 2) * (2 * goto_time CP TP + 3)). have [n [?]] := transition_le_gt (fun n => CM.value (Nat.iter n (CM1.step P) cm_start)) (m + 1) 0 NP ltac:(lia) ltac:(rewrite /cm_start /=; lia) ltac:(rewrite /cm_end -/CP; lia). have := CM_facts.run_value_monotone P cm_start n. set p := (Nat.iter n (CM1.step P) cm_start). have -> : Nat.iter (1 + n) (CM1.step P) cm_start = CM1.step P p by done. move=> H1p [? ?]. rewrite /cm_start /= in H1p. have := iter_cm_step HTP l (§0^(m - (CM.value p - 1))) n. rewrite -/p. move=> /(_ ltac:(lia)) /reachable_n_maybe_reachable. apply: (maybe_reachable_trans' (2*maybe_goto_1_time + 1 + T')); [ by nia | rewrite ?app_norm; do 6 f_equal; by lia | ]. have Hp : CM.value p < CM.value (CM.step P p) by lia. have [[pj pn] [/nth_error_Some_In_iP HpiP] /= Hpn] := CM_facts.inc_value_mod Hp. apply: (maybe_first_step (index_try_spec (CM.state p, (pj, pn))) l (§0^(CM.value p - 1) ++ [§1] ++ §0^(m - (CM.value p - 1)))); [by nia | by auto with M | by rewrite ?app_norm; do 4 f_equal; lia |]. rewrite ?app_norm. have ->: (1 + (CM.value p - 1)) = CM.value p by lia. apply: (maybe_first_goto_1 (maybe_goto_1_time + T')); [by lia | rewrite Hpn]. set k := (m - (CM.value p - 1)). have ?: (k + 1) * (1 + pn) <= CM.value p. { suff: (CM.value (CM1.step P p) - CM.value p) * (1 + pn) = CM.value p by nia. suff: CM.value (CM1.step P p) = (CM.value p) * (pn + 2) / (pn + 1). { move=> ->. by have := divides_frac_diff Hpn. } rewrite /CM1.step. have {1}->: CM1.value p = S (CM1.value p - 1) by lia. move: HpiP => /nth_error_Some_In_iP ->. by rewrite Hpn. } have -> : CM.value p = (k+1)*(1+pn)+(CM.value p - (k+1)*(1+pn)) by lia. have := do_increase HTP [] (§0^((1 + pn) + (CM.value p - (k + 1) * (1 + pn))) ++ [§1] ++ l) k 0 HpiP ltac:(lia). move /reachable_n_maybe_reachable. apply: (maybe_reachable_trans' (maybe_goto_1_time + goto_time CP TP + 1)); first by nia. { rewrite ?app_norm. do 4 f_equal. by lia. } apply: (maybe_first_step (index_yes_spec_n1 (CM1.state p, (pj, pn))) (§0^(k * (2 + pn)) ++ [§1]) (§0^(CM.value p - (k + 1) * (1 + pn)) ++ [§1] ++ l)); [by lia | by auto with M | by rewrite ?app_norm; do 4 f_equal; lia |]. rewrite ?app_norm. apply: (maybe_first_goto_1 0); first by lia. rewrite ?app_norm. right. eexists. constructor; first by apply: reach_refl. by move=> ? /increase_try_step_shape [|]. 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