proposition: Lemma maybe_index_try_step l r p : maybe_reachable maybe_index_try_step_time ([§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 NP_spec. rewrite /maybe_index_try_step_time. move: p => [i [|c]] /=. { by apply: maybe_reachable_refl'. } move H: (nth_error P i) => oi. case: oi H; first last. { move=> _ /=. rewrite ?nat_norm ?app_norm. by apply: maybe_reachable_refl'. } move=> [j n] /nth_error_Some_In_iP /=. 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. apply: (maybe_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: (maybe_first_goto_1 (maybe_goto_1_time + maybe_increase_time + 1)); first by lia. rewrite Hcn. have ? : (d - S c) * (1 + n) = S c. { rewrite -Hd. by apply: divides_frac_diff. } have := maybe_increase r ([§1] ++ l) (d - S c) 0 Hijn. apply: (maybe_reachable_trans' (maybe_goto_1_time + 1)); first by lia. { rewrite ?app_norm. do 4 f_equal. by lia. } apply: (maybe_first_step (index_yes_spec_1 (i, (j, n)))); [by lia | by auto with M | by rewrite ?app_norm; reflexivity | ]. apply: maybe_reachable_refl'. rewrite ?app_norm. do 4 f_equal. by lia. - apply: (maybe_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: (maybe_first_goto_1 (maybe_goto_1_time + 1)); first by lia. rewrite Hcn. apply: (maybe_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: (maybe_first_goto_1 0); [by lia | by apply: maybe_reachable_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