proposition: Theorem reduction n : @MMA_HALTING (3+n) ⪯ @MMA_HALTING (2+n).
proof: Proof. apply reduces_dependent; exists. intros (P,v). set (w := 0##gc_enc godel_coding_235 (fst (vec_split _ _ v))##vec_tail (vec_tail (vec_tail v))). exists (gc_code (mma3_mma2_compiler n) (1, P) 1, w). apply (compiler_t_term_equiv (mma3_mma2_compiler _)); simpl. msplit 2; auto. intro; now rewrite !vec_pos_tail. Qed.
imports: Undecidability.Shared.Libs.DLW(utils_tac godel_coding pos vec sss compiler_correction) Undecidability.MinskyMachines.MMA(mma_defs mma3_mma2_compiler) Undecidability.Synthetic(Definitions ReducibilityFacts)