proposition: Lemma SBTM_HALT_semi_decision : { f : { M : SBTM & config M } -> nat -> bool | semi_decider f SBTM_HALT }.
proof: Proof. exists (fun '(existT _ M x) k => match steps M k x with | Some _ => false | None => true end). intros [M x]. split. + intros [k Hk]. exists k. now rewrite Hk. + intros [k Hk]. exists k. now destruct (steps M k x) as [?|]. Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts) Undecidability.TM.SBTM