proposition: Theorem reduction {n} : @MMA_HALTING n ⪯ HaltTM n.
proof: Proof. exists (fun '(M, cs) => existT2 _ _ (finType_CS bool) (Argument.P M) (Argument.encode_counters cs)). move=> [M cs]. split. - by apply: Argument.simulation. - by move=> [p'] [ts] /Argument.inverse_simulation. Qed.
imports: Undecidability.MinskyMachines(MM MMA.mma_defs) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL.EqDec List Vector Lia PeanoNat Compare_dec ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions