proposition: Lemma maybe_increase l r i j n k m : In (i, (j, n)) iP -> maybe_reachable maybe_increase_time (§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 NP_spec. rewrite /maybe_increase_time. move=> Hijn. move: l r k m. have H : forall k m l r, maybe_reachable ((k+1)*(2 * maybe_goto_1_time + 3)) (§0^m ++ [§1] ++ §0^k ++ l, §0^(k * (1+n)) ++ r, '#+i) (§0^(m + k * (2+n)) ++ [§1] ++ l, r, '#+i). { elim. { move=> m l r. rewrite ?app_norm ?nat_norm. by apply: maybe_reachable_refl'. } move=> k IH m l r. have ? := iP_capped Hijn. pose N' := (k+1)*(2 * maybe_goto_1_time + 3). apply: (maybe_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: (maybe_first_goto_1 (N' + maybe_goto_1_time + 2)); first by lia. apply: (maybe_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: (maybe_first_goto_1 (N' + 1)); first by lia. apply: (maybe_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. apply: maybe_reachable_mon'; first by lia. rewrite ?app_norm. by do 5 f_equal; lia. } move=> l r k m. have [? | ?] : k <= G + CP \/ G + CP < k by lia. { have := H k m l r. by apply: maybe_reachable_mon'; first by nia. } pose k' := G + CP. have := H k' m (§0^(k-k') ++ l) (§0^((k-k') * (1 + n)) ++ r). apply: (maybe_reachable_trans' (maybe_goto_1_time + 1)); first by lia. { rewrite ?app_norm. (do 4 f_equal); last by lia. do 2 f_equal. by lia. } apply: (maybe_first_step (index_yes_spec_n1 (i, (j, n))) (§0^(m + k' * (2 + n)) ++ [§1] ++ §0^(k - k') ++ l) (§0^((k - k' - 1) * (1 + n)) ++ r)); [ by lia | by auto with M | by rewrite ?app_norm; do 4 f_equal; nia | ]. rewrite ?app_norm /k'. have ? := CP_pos. rewrite /maybe_goto_1_time. apply: maybe_goto_1_far; 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