proposition: Lemma reduction : KrivineMclosed_HALT ⪯ HaltUTM.
proof: Proof. unshelve eexists. { intros [tm _]. assert (cs := KM_MMA.input tm). assert (ts := MMA_TM.encode_counters cs). assert (t := MTM_TM.ts' ts). assert (t' := TM_BTM.ts' t). exact (Vector.hd t'). } move=> [tm Htm]. apply: (iff_trans (KM_MMA_iff Htm)). apply: (iff_trans MMA_TM_iff). apply: (iff_trans MTM_TM_iff). by apply: TM_BTM_iff. Qed.
imports: Undecidability(TM.UTM TM.TM LambdaCalculus.Krivine MinskyMachines.MMA Shared.Libs.PSL.FiniteTypes.FinTypesDef) Coq(Vector ssreflect ssrbool ssrfun) Undecidability.Synthetic.Definitions