proposition: Lemma maybe_increase_next l r i j n c k m : In (i, (j, n)) iP -> c / (1+n) <= k -> maybe_reachable (maybe_increase_time+1) (§0^m ++ [§1] ++ §0^k ++ l, §0^c ++ [§1] ++ r, '#+i) ([§1] ++ r, §0^(m + c + (c / (1+n)) + (c mod (1+n))) ++ [§1] ++ §0^(k - (c / (1+n))) ++ l, '#?j).
proof: Proof. Proof using NP_spec. have := Nat.div_mod c (1+n) ltac:(lia). move: (c / (1+n)) => k'. have ->: (1 + n) * k' = k' * (1 + n) by lia. move=> ? Hijn ?. have := maybe_increase (§0^(k-k') ++ l) (§0^(c mod (1 + n)) ++ [§1] ++ r) k' m Hijn. apply: (maybe_reachable_trans' 1); first by lia. { rewrite ?app_norm. do 4 f_equal; last by lia. do 2 f_equal. by lia. } have ? := Nat.mod_upper_bound c (1+n) ltac:(lia). have [Hc | Hc]: c mod (1 + n) = 0 \/ c mod (1 + n) = 1 + (c mod (1 + n) - 1) by lia. { rewrite Hc. apply: (maybe_first_step (index_yes_spec_1 (i, (j, n))) (§0^(m + k' * (2 + n)) ++ [§1] ++ §0^(k - k') ++ l) r); [ by lia | by auto with M | done | ]. apply: maybe_reachable_refl'. rewrite ?nat_norm ?app_norm. do 4 f_equal. by lia. } rewrite Hc. apply: terminal_maybe_reachable. move=> ? /(index_yes_step_shape Hijn) [| /zero_prefix_lt]; 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