proposition: Theorem reduction : SBTM_HALT ⪯ PCTM_HALT.
proof: Proof. apply reduces_dependent; exists. intros (M,(i,t)). exists (sbtm2pctm M i,t); split. + intros (k & Hk). apply sbtm2pctm_sound in Hk as (t' & Ht'). exists (0,t'); split; auto; left; auto. + apply sbtm2pctm_complete. Qed.
imports: List Bool Undecidability.Synthetic(Definitions ReducibilityFacts) Undecidability.Shared.Libs.DLW(pos sss) Undecidability.TM(SBTM PCTM pctm_sbtm)