proposition: Lemma do_increase {C N: nat} : bound_reachable_n C N -> forall l r i j n k m, In (i, (j, n)) iP -> m + k * (2+n) - (G + 1) <= C -> reachable_n ((k+1)*(2*(goto_time C N)+3)) (§0^m ++ [§1] ++ §0^k ++ l, §0^(k * (1+n)) ++ r, '#+i) (§0^(m + k * (2+n)) ++ [§1] ++ l, r, '#+i).
proof: Proof. Proof using capped_P. move=> HN l r i j n k m Hijn. elim: k m l r. { move=> m l r _. rewrite ?app_norm ?nat_norm. by apply: reach_refl. } move=> k IH m l r HmkC. have ? := iP_capped Hijn. pose N' := (k+1)*(2 * goto_time C N + 3). apply: (first_step (index_yes_spec_n1 (i, (j, n))) (§0^m ++ [§1] ++ §0^(1+k) ++ l) (§0^(k * (1 + n)) ++ r)); [by lia | by auto with M | by rewrite ?app_norm |]. rewrite ?app_norm. apply: (first_goto_1 HN (N' + goto_time C N + 2)); [ by eauto with M | by lia | by lia |]. apply: (first_step (increase_try_spec_0 (i, (j, n))) (§0^k ++ l) (§0^(n + m) ++ [§1] ++ §0^(k * (1 + n)) ++ r)); [by lia | by auto with M | by rewrite ?app_norm |]. rewrite ?app_norm. apply: (first_goto_1 HN (N' + 1)); [ by eauto with M | by lia | by lia |]. apply: (first_step (increase_yes_spec (i, (j, n))) (§0^(k * (1 + n)) ++ r) (§0^(1 + (n + m)) ++ [§1] ++ §0^k ++ l)); [by lia | by auto with M | by rewrite ?app_norm |]. have := IH (m + n + 2) l r ltac:(lia). apply: reachable_n_mon'; [by lia | by rewrite ?app_norm; do 5 f_equal; 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