proposition: Lemma search_bound (C n: nat) : C <= CM.value (Nat.iter n (CM1.step P) cm_start) -> {N | bound_reachable_n C N}.
proof: Proof. Proof using capped_P. elim: C. { rewrite /bound_reachable_n. move=> _. exists 1. move=> m l r ?. have ->: m = 0 by lia. apply: (first_step bound_try_spec_1 r l); [by lia | by auto with M | by rewrite ?app_norm | by apply: reach_refl ]. } move=> C IH HC. have [N HN] := IH ltac:(lia). exists (n * step_time C N + increase_time C N + 3 * goto_time C N + 3). rewrite /bound_reachable_n. move=> [|[|m]] l r Hm. - apply: (first_step bound_try_spec_1 r l); [by lia | by auto with M | done | by apply: reach_refl ]. - apply: (first_step bound_try_spec_01 r l); [by lia | by auto with M | done | by apply: reach_refl ]. - apply: (first_step bound_try_spec_00 (§0^m ++ [§1] ++ r) l); [by lia | by auto with M | by rewrite ?app_norm | ]. have := transition_le_gt (fun n => CM.value (Nat.iter n (CM1.step P) cm_start)) (S m) 0 n. move=> /(_ ltac:(lia) ltac:(rewrite /cm_start /=; lia) ltac:(lia)) [n' [?]]. 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 HN l (§0^(m - (CM.value p' - 1)) ++ [§1] ++ r) n'. rewrite -/p'. move /(_ ltac:(lia)). apply: (reachable_n_trans' (increase_time C N + 3 * goto_time C N + 2)); [by nia | by rewrite ?app_norm; do 6 f_equal; lia |]. have Hp' : CM.value p' < CM.value (CM.step P p') by lia. have [[p'j p'n] [/nth_error_Some_In_iP Hp'iP] /= Hp'n] := CM_facts.inc_value_mod Hp'. apply: (first_step (index_try_spec (CM.state p', (p'j, p'n))) l (§0^(CM.value p' - 1) ++ [§1] ++ §0^(m - (CM.value p' - 1)) ++ [§1] ++ r)); [by lia | 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: (first_goto_1 HN (increase_time C N + 2 * goto_time C N + 1)); [ by eauto with M | by lia | by lia | ]. set k := (m - (CM.value p' - 1)). have ?: (k + 1) * (1 + p'n) <= CM.value p'. { suff: (CM.value (CM1.step P p') - CM.value p') * (1 + p'n) = CM.value p' by nia. suff: CM.value (CM1.step P p') = (CM.value p') * (p'n + 2) / (p'n + 1). { move=> ->. by have := divides_frac_diff Hp'n. } rewrite /CM1.step. have {1}->: CM1.value p' = S (CM1.value p' - 1) by lia. move: Hp'iP => /nth_error_Some_In_iP ->. by rewrite Hp'n. } have -> : CM.value p' = (k+1)*(1+p'n)+(CM.value p' - (k+1)*(1+p'n)) by lia. move: (Hp'iP) => /(fail_increase HN r (§0^(CM.value p' - (k + 1) * (1 + p'n)) ++ [§1] ++ l)) => /(_ k). have ? := iP_capped Hp'iP. have ? : 4 <= G by (rewrite /G; lia). have ? : (k + 1) * (2 + p'n) - (G + 1) <= C by lia. move /(_ ltac:(lia)). apply: (reachable_n_trans' (2 * goto_time C N + 1)); first by lia. { rewrite ?app_norm. have ->: ((k + 1) * (1 + p'n) + (CM.value p' - (k + 1) * (1 + p'n))) = CM.value p' by lia. by rewrite Hp'n. } apply: (first_goto_1 HN (goto_time C N + 1)); [ by eauto with M | by lia | by lia |]. apply: (first_step (increase_no_spec (CM.state p', (p'j, p'n))) (§0^(CM.value p' - (k + 1) * (1 + p'n)) ++ [§1] ++ l) (§0^((k + 1) * (1 + p'n) + k) ++ [§1] ++ r)); [by lia | by auto with M | done | ]. apply: (first_goto_1 HN 0); [by eauto with M | by move: ((k + 1) * (1 + p'n)); lia | by lia |]. apply: reachable_n_refl'. rewrite ?app_norm ?nat_norm. do 4 f_equal. 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