proposition: Theorem uniform_termination x: exists z, reachable_n uniform_termination_time x z /\ terminal M z.
proof: Proof. Proof using NP_spec. apply: universal_maybe_reachable_terminal => z. rewrite /uniform_termination_time. move: x => [[l r] [X|n X Y]]. { have [[[[[l' r'] n'] X'] Y']] := maybe_basic_state_grow l r 0 X. apply: (maybe_reachable_trans' ((G + (CP + 1)) * maybe_goto_1_grow_time + (NP * step_time CP TP + 2))); [ by lia | done | ]. have [[[[[l'' r''] n''] X''] Y'']] := maybe_goto_1_grow_iter l' (§0^1 ++ r') (G + (CP + 1)) n' X' Y'. apply: (maybe_reachable_trans' (NP * step_time CP TP + 2)); [ by lia | done | ]. apply: maybe_goto_1_far; by lia. } have [[[[[l'' r''] n''] X''] Y'']] := maybe_goto_1_grow_iter l r (G + (CP + 1)) n X Y. apply: (maybe_reachable_trans' (NP * step_time CP TP + 2)); [ by lia | done | ]. 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