proposition: Theorem reduction : KrivineMclosed_HALT ⪯ (@MMA_HALTING 5).
proof: Proof. exists (fun '(exist _ t _) => (Argument.PROG 1, Argument.input t)). move=> [t /= /eclosed_closed Ht]. split. - move=> /Argument.simulation. by apply. - move=> /(Argument.inverse_simulation nil nil). by apply. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions