proposition: Lemma maybe_index_yes_futile l m i z : maybe_reachable maybe_index_yes_futile_time (l, §0^m, '#+i) z.
proof: Proof. Proof using NP_spec. rewrite /maybe_index_yes_futile_time. have [? | /in_iPI [j [n Hijn]]] : length P <= i \/ i < length P by lia. { apply: terminal_maybe_reachable. by apply: large_index_terminal. } have [? | ?] : m <= n \/ n < m by lia. { apply: (maybe_reachable_mon' (n := 0)); [by lia | by reflexivity |]. apply: maybe_index_yes_near_futile; by eassumption. } have [[m' ->]|]:= list_symbol_shape l. { apply: (maybe_first_step (index_yes_spec_n1 (i, (j, n))) (§0^m') (§0^(m-(n+1)))); [ by lia | by auto with M | by rewrite ?app_norm; do 5 f_equal; lia |]. rewrite ?app_norm. apply: maybe_goto_1_futile. by lia. } move=> [k1 [+ ->]] => {}l. have [[k2 ->]|] := list_symbol_shape l. { have [| ?]: m / (1+n) <= k2 \/ k2 < m / (1+n) by lia. { have := Nat.div_mod m (1+n) ltac:(lia). move Hk: (m / (1+n)) => k Hm ?. have := maybe_increase (§0^(k2-k)) (§0^(m mod (1 + n))) k k1 Hijn. apply: (maybe_reachable_trans' 0); first by lia. { rewrite ?app_norm. do 5 f_equal; by lia. } apply: (maybe_reachable_mon' (n := 0)); [by lia | by reflexivity |]. move: (Hijn) => /maybe_index_yes_near_futile. apply. have := Nat.mod_upper_bound m (1+n) ltac:(lia). by lia. } have := maybe_increase [] (§0^(m - k2 * (1+n))) k2 k1 Hijn. apply: (maybe_reachable_trans' (maybe_goto_1_time + 1)); first by lia. { rewrite ?app_norm. do 5 f_equal. have ? := div_mul_le m (1+n). by nia. } move: (m - k2 * (1 + n)). move: (k1 + k2 * (2 + n)) => k1' m'. have [? | ?]: m' <= n \/ n < m' by lia. { apply: (maybe_reachable_mon' (n := 0)); [by lia | by reflexivity |]. apply: maybe_index_yes_near_futile; by eassumption. } apply: (maybe_first_step (index_yes_spec_n1 (i, (j, n))) (§0^k1' ++ [§1]) (§0^(m' - (n+1)))); [ by lia | by auto with M | by rewrite ?app_norm; do 4 f_equal; lia |]. rewrite ?app_norm. apply: (maybe_first_goto_1 0); first by lia. by apply: terminal_maybe_reachable => ? /increase_try_step_shape [|]. } move=> [k2 [+ ->]] => {}l. have [| ?] : m / (1+n) <= k2 \/ k2 < m / (1+n) by lia. { have := Nat.div_mod m (1+n) ltac:(lia). move Hk: (m / (1+n)) => k Hm ?. have := maybe_increase (§0^(k2-k) ++ [§1] ++ l) (§0^(m mod (1 + n))) k k1 Hijn. apply: (maybe_reachable_trans' 0); first by lia. { rewrite ?app_norm. do 5 f_equal; last by lia. f_equal. by lia. } apply: (maybe_reachable_mon' (n := 0)); first by lia. { by reflexivity. } move: (Hijn) => /maybe_index_yes_near_futile. apply. have := Nat.mod_upper_bound m (1+n) ltac:(lia). by lia. } have := maybe_increase ([§1] ++ l) (§0^(m - k2 * (1+n))) k2 k1 Hijn. apply: (maybe_reachable_trans' (2*maybe_goto_1_time + maybe_index_try_stop_time + 5)); first by lia. { rewrite ?app_norm. do 5 f_equal. have ? := div_mul_le m (1+n). by nia. } move: (m - k2 * (1 + n)). move: (k1 + k2 * (2 + n)) => k1' m'. have [? | ?]: m' <= n \/ n < m' by lia. { apply: (maybe_reachable_mon' (n := 0)); [by lia | by reflexivity |]. apply: maybe_index_yes_near_futile; by eassumption. } apply: (maybe_first_step (index_yes_spec_n1 (i, (j, n))) (§0^k1' ++ [§1] ++ [§1] ++ l) (§0^(m' - (n+1)))); [ by lia | by auto with M | by rewrite ?app_norm; do 4 f_equal; lia |]. rewrite ?app_norm. apply: (maybe_first_goto_1 (maybe_goto_1_time + maybe_index_try_stop_time + 4)); first by lia. apply: (maybe_first_step (increase_try_spec_1 (i, (j, n))) l (§0^(n + k1') ++ [§1] ++ §0^(m' - (n + 1)))); [ by lia | by auto with M | by rewrite ?app_norm |]. rewrite ?app_norm. apply: (maybe_first_goto_1 (maybe_index_try_stop_time + 3)); first by lia. apply: (maybe_first_step (increase_no_spec (i, (j, n))) (§0^(m' - (n + 1))) (§0^(1 + (n + k1')) ++ [§1] ++ l)); [ by lia | by auto with M | by rewrite ?app_norm |]. rewrite ?app_norm. apply: maybe_goto_1_futile. 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