proposition: Lemma maybe_increase_try_grow l r m i : exists '(l', r', n, X, Y), maybe_reachable 1 (l, §0^m ++ r, '$?i) (l', §0^(m+1) ++ r', goto n X Y).
proof: Proof. pose dummy := ([§0], [§0], 0, +|, +|). have [? | /in_iPI [j] [n] ?]: length P <= i \/ i < length P by lia. { exists dummy. apply: terminal_maybe_reachable. by apply: large_increase_terminal. } move: l => [|a [|b l]]. - exists dummy. by apply: terminal_maybe_reachable => ? /increase_try_step_shape [|]. - exists dummy. by apply: terminal_maybe_reachable => ? /increase_try_step_shape [|]. - case: a. { exists dummy. by apply: terminal_maybe_reachable => ? /increase_try_step_shape [|]. } case: b. * exists (([§1] ++ l), r, 0, ($+i), ($+i)). apply: (maybe_first_step (increase_try_spec_0 (i, (j, n))) l (§0^m ++ r)); [by lia | by auto with M | done |]. rewrite ?app_norm. apply: maybe_reachable_refl'. do 4 f_equal. by lia. * exists (([§1] ++ l), r, 0, ($-i), ($-i)). apply: (maybe_first_step (increase_try_spec_1 (i, (j, n))) l (§0^m ++ r)); [by lia | by auto with M | done |]. rewrite ?app_norm. apply: maybe_reachable_refl'. 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