proposition: Lemma do_cm_step {C N: nat} : bound_reachable_n C N -> forall l r p, CM.value (CM1.step P p) <= G + C -> reachable_n (step_time C N) ([§1] ++ l, §0^(CM.value p) ++ [§1] ++ (§0^(CM.value (CM1.step P p) - CM.value p)) ++ r, '#?(CM.state p)) ([§1] ++ l, §0^(CM.value (CM1.step P p)) ++ [§1] ++ r, '#?(CM.state (CM1.step P p))).
proof: Proof. Proof using capped_P. move=> HN l r [i [|c]] /= HpC; first by apply: reach_refl. move H: (nth_error P i) HpC => oi. case: oi H; first last. { move=> _ _ /=. rewrite ?nat_norm ?app_norm. by apply: reach_refl. } move=> [j n] /nth_error_Some_In_iP. rewrite /step_time. move Hm: (S c mod (n + 1)) => m. move: m Hm => [|m] Hcn /= Hijn. - have := CM_facts.mod_frac_lt Hcn. move Hd: (S c * (n + 2) / (n + 1)) => d Hcd HC. apply: (first_step (index_try_spec (i, (j, n))) l (§0^c ++ [§1] ++ §0^(d - S c) ++ r)); [ by lia | by auto with M | by rewrite ?app_norm | ]. rewrite ?app_norm. apply: (first_goto_1 HN (increase_time C N)); [ by eauto with M | by lia | by lia |]. rewrite Hcn. have ? := divides_frac_diff Hcn. have := do_increase HN r ([§1] ++ l) (d - S c) 0 Hijn ltac:(lia). apply: (reachable_n_trans' 1); [ by rewrite /increase_time; nia | by rewrite ?app_norm; do 4 f_equal; lia |]. apply: (first_step (index_yes_spec_1 (i, (j, n))) (§0^((d - S c) * (2 + n)) ++ [§1] ++ r) l); [ by lia | by auto with M | by rewrite ?app_norm | ]. apply: reachable_n_refl'. rewrite ?app_norm. by do 4 f_equal; lia. - move=> ?. apply: (first_step (index_try_spec (i, (j, n))) l (§0^c ++ [§1] ++ r)); [by lia | by auto with M | by rewrite ?app_norm ?nat_norm | ]. rewrite ?app_norm. apply: (first_goto_1 HN (increase_time C N)); [ by eauto with M | by lia | by lia | rewrite Hcn /increase_time ]. apply: (first_step (index_no_spec (i, (j, n))) ([§1] ++ r) (§0^c ++ [§1] ++ l)); [ by lia | by auto with M | done |]. rewrite ?app_norm. apply: (first_goto_1 HN 0); [ by eauto with M | by lia | by lia | by apply: reach_refl]. 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