proposition: Lemma maybe_bounded_try l r : maybe_reachable maybe_bounded_try_time (r, l, '?|) (l, r, '+|).
proof: Proof. Proof using NP_spec. rewrite /maybe_bounded_try_time. move: l => [|a l]. { right. eexists. constructor; first by apply: reach_refl. by move=> ? /bound_try_step_shape [? ?]. } case: a. { right. eexists. constructor; first by apply: reach_refl. by move=> ? /bound_try_step_shape [? ?]. } move: r => [|b r]. { right. eexists. constructor; first by apply: reach_refl. by move=> ? /bound_try_step_shape [[|[|]] ?]. } case: b. { move: r=> [|b r]. { right. eexists. constructor; first by apply: reach_refl. by move=> ? /bound_try_step_shape [[|[|]] ?]. } case: b. { have [[m ->]|] := list_symbol_shape r. { apply: (maybe_first_step bound_try_spec_00 (§0^m) l); [ by lia | by auto with M | by rewrite ?app_norm | ]. rewrite ?app_norm. apply: maybe_index_try_stop. by lia. } move=> [m [+ ->]] => {}r. have [| ?]: m + 2 <= CP \/ CP < m + 2 by lia. { move /(HTP (m+2) l r) => + /ltac:(left). apply: reachable_n_mon'; first by lia. rewrite ?app_norm. do 5 f_equal; by lia. } apply: (maybe_first_step bound_try_spec_00 (§0^m ++ [§1] ++ r) l); [ by lia | by auto with M | by rewrite ?app_norm; do 4 f_equal; lia | ]. have := maybe_index_try_run l (§0^(m - (CP - 1)) ++ [§1] ++ r) (§1 :: l, §0 :: §0 :: §0^m ++ [§1] ++ r, '+|). apply: maybe_reachable_mon'; first by (rewrite /maybe_index_try_stop_time; nia). rewrite ?app_norm. do 7 f_equal. by lia. } apply: (maybe_first_step bound_try_spec_01 r l); [ by lia | by auto with M | by rewrite ?app_norm |]. apply: maybe_reachable_refl'. by rewrite ?app_norm. } apply: (maybe_first_step bound_try_spec_1 r l); [ by lia | by auto with M | by rewrite ?app_norm |]. apply: maybe_reachable_refl'. by rewrite ?app_norm. 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