proposition: Theorem MMA_computable_to_MMA_mon_computable k (R : Vector.t nat k -> nat -> Prop) : MMA_computable R -> MMA_mon_computable R.
proof: Proof. move=> /MMA_computable_iff [k'] [P] [H1P H2P]. apply /MMA_mon_computable_iff. exists (k'+1), (@P' _ _ P). split; [by apply: P'_mon|split]. - move=> v m /H1P [c] [v'] [] /=. rewrite (vec_append_splitat v'). move=> /simulation /[apply] ?. eexists _, _. split; [eassumption|]. rewrite /= length_P' /=. lia. - move=> v /sss_terminates_iff Hv. apply: H2P. apply /sss_terminates_iff. move: Hv. apply /(Sim.terminates_reflection step2_det fstep step1_intro). rewrite -vec_append_const. by apply: sync_intro. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect