proposition: Theorem reduction : PCTM_HALT ⪯ BSMn_HALTING 2.
proof: Proof. apply reduces_dependent; exists. intros (P,((l,b),r)). set (Q := gc_code pctm_bsm2_compiler (1,P) 1). set (w1 := l##(b::r)##vec_nil). exists (existT _ 1 (existT _ Q w1)); simpl. apply compiler_t_term_equiv; split; auto. Qed.
imports: List Bool Undecidability.Synthetic(Definitions ReducibilityFacts) Undecidability.Shared.Libs.DLW(pos vec sss compiler_correction) Undecidability.TM(PCTM) Undecidability.StackMachines(bsm_defs bsm_pctm BSM_sss)