proposition: Lemma maybe_increase_fail l r i j n c k m : In (i, (j, n)) iP -> k < c / (1+n) -> maybe_reachable (maybe_increase_time + 3*maybe_goto_1_time + 3) (§0^m ++ [§1] ++ §0^k ++ [§1] ++ l, §0^c ++ [§1] ++ r, '#+i) ([§1] ++ r, §0^(c+m+k+1) ++ [§1] ++ l, '+|).
proof: Proof. Proof using NP_spec. have := Nat.div_mod c (1+n) ltac:(lia). move: (c / (1 + n)) => k'. move: (c mod (1 + n)) => k'' -> Hijn ?. have := maybe_increase ([§1] ++ l) (§0^((1 + n) * (k'-k) + k'') ++ [§1] ++ r) k m Hijn. apply: (maybe_reachable_trans' (3*maybe_goto_1_time + 3)); first by lia. { rewrite ?app_norm. do 4 f_equal. by lia. } apply: (maybe_first_step (index_yes_spec_n1 (i, (j, n))) (§0^((m + k * (2 + n))) ++ [§1] ++ [§1] ++ l) (§0^((1 + n) * (k' - k - 1) + k'') ++ [§1] ++ r)); [ by lia | by auto with M | by rewrite ?app_norm; do 4 f_equal; nia |]. rewrite ?app_norm. apply: (maybe_first_goto_1 (2*maybe_goto_1_time + 2)); first by lia. apply: (maybe_first_step (increase_try_spec_1 (i, (j, n)))); [by lia | by auto with M | by rewrite ?app_norm; reflexivity |]. rewrite ?app_norm. apply: (maybe_first_goto_1 (maybe_goto_1_time + 1)); first by lia. apply: (maybe_first_step (increase_no_spec (i, (j, n)))); [ by lia | by auto with M | by rewrite ?app_norm; reflexivity |]. rewrite ?app_norm. apply: (maybe_first_goto_1 0); first by lia. apply: maybe_reachable_refl'. rewrite ?app_norm. do 4 f_equal. by nia. 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