proposition: Theorem reduction n : BSMn_HALTING n ⪯ @MMA_HALTING (1+n).
proof: Proof. apply reduces_dependent; exists. intros (i,(P,v)). exists (gc_code (bsm_mma_compiler _) (i, P) 1, 0##vec_map stack_enc v). apply (compiler_t_term_equiv (bsm_mma_compiler n) (i,P) 1); simpl; split; auto. intros; rew vec. Qed.
imports: Undecidability.Shared.Libs.DLW(utils list_bool pos vec sss compiler_correction) Undecidability.StackMachines(bsm_defs) Undecidability.MinskyMachines.MMA(mma_defs mma_utils_bsm bsm_mma) Undecidability.Synthetic(Definitions ReducibilityFacts)