proposition: Theorem MMA2_MMA2_HALTS_ON_ZERO : MMA2_HALTING ⪯ MMA2_HALTS_ON_ZERO.
proof: Proof. apply reduces_dependent; exists. intros (P,v). destruct mma2_simulator with 1 1 P as (Q & HQ). exists (Q,v); apply HQ. Qed.
imports: List Arith Relations Lia Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Shared.Libs.DLW(utils pos vec sss subcode) Undecidability.MinskyMachines(mma_defs mma_simul)