proposition: Theorem MMA_mon_computable_to_TM_computable k (R : Vector.t nat k -> nat -> Prop) : MMA_mon_computable R -> TM_computable R.
proof: Proof. move=> /MMA_mon_computable_iff [k'] [M] [H1M [H2M H3M]]. have : forall l x q r, M = l ++ DEC x q :: r -> x <> pos0. { move=> > HM Hi. by move: HM Hi H1M => -> -> /Forall_app [_] /Forall_cons_iff []. } move=> {}H1M. apply /TM_computable.TM_computable_iff. exists k', Argument.Σ, true, false. split; [done|]. exists (Argument.P M). split. - move=> v m /H2M [c] [v'] [] /(simulation M H1M) => /(_ _ sync_init). move=> [[p' b's]] [Hst'] + Hc. move: (Hst') Hc => /stuck_step2I /[apply] /terminates2E /[apply]. move=> [n] Hn. exists p', b's. split. + apply /TM_facts.TM_eval_iff. exists (S n) => /=. by rewrite P_init. + move: Hst' => /syncE. rewrite (Vector.eta b's) /=. by move=> [_ []]. - move=> v q ts /TM_facts.TM_eval_iff [n HPn]. apply: H3M. apply /sss_terminates_iff. apply /(Sim.terminates_reflection (step2_det M) (fstep M H1M) (step1_intro M) sync_init). move: n HPn => [|n]. { done. } rewrite /= P_init. by apply: terminates2I. Qed.
imports: Undecidability.TM(TM) Undecidability.MinskyMachines(MM MMA.mma_defs Reductions.MMA_computable_to_MMA_mon_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL(CompoundFinTypes) Undecidability.Shared.Libs.PSL.EqDec List Lia PeanoNat Compare_dec Relations ssreflect ssrbool ssrfun