proposition: Lemma fail_increase {C N: nat} : bound_reachable_n C N -> forall l r i j n k, In (i, (j, n)) iP -> (k+1) * (2+n) - (G + 1) <= C -> reachable_n (increase_time C N) ([§1] ++ §0^k ++ [§1] ++ l, §0^((k+1)*(1+n)) ++ r, '#+i) ([§1] ++ l, §0^((k+1)*(1+n) + k) ++ [§1] ++ r, goto 0 ($-i) ($-i)).
proof: Proof. Proof using capped_P. move=> HN l r i j n k Hijn HC. rewrite /increase_time. have := do_increase HN ([§1] ++ l) (§0^(1 + n) ++ r) k 0 Hijn ltac:(lia). apply: (reachable_n_trans' (2 * goto_time C N + 3)); first by ((suff: k+1 <= C + G + 1 by nia); lia). { rewrite ?app_norm ?nat_norm. do 4 f_equal. by lia. } apply: (first_step (index_yes_spec_n1 (i, (j, n))) (§0^(k * (2 + n)) ++ [§1] ++ [§1] ++ l) r); [by lia | by auto with M | by rewrite ?app_norm |]. rewrite ?app_norm. apply: (first_goto_1 HN (goto_time C N + 2)); [ by eauto with M | by lia | by lia | ]. apply: (first_step (increase_try_spec_1 (i, (j, n))) l (§0^(n + k * (2 + n)) ++ [§1] ++ r)); [by lia | by auto with M | by rewrite ?app_norm | ]. apply: reachable_n_refl'. rewrite ?app_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