proposition: Theorem reduction : CM1_HALT ⪯ SMNdl_UB.
proof: Proof. unshelve eexists (fun '(exist _ P HP) => exist _ (Argument.MN (M P)) _). - constructor; [apply: Argument.deterministic_MN | apply: Argument.length_preserving_MN]. + by apply: deterministic_M. + by apply: flip_consistent_M. + by apply: length_preserving_M. - move=> [P HP]. constructor. + move=> [nP] /(terminating_P_to_bounded_M P HP). move /Argument.bounded_MN => bounded_MN. eexists. apply: bounded_MN. by apply: flip_consistent_M. + move=> [nMN] /= /Argument.bounded_MX /(bounded_M_to_terminating_P P HP) H'P. eexists. by eassumption. Qed.
imports: Relation_Operators Lia PeanoNat List Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(Nat_facts List_facts Enumerable) Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.CM1_to_SMX ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions Undecidability.CounterMachines.CM1