proposition: Lemma sbtm2pctm_sound k t : steps M k (i,t) = None -> exists t', (1,sbtm2pctm) // (1,t) ->> (0,t').
proof: Proof. intros H. generalize (steps_Q k i t); rewrite H. intros (t' & H1); exists t'. unfold sbtm2pctm. pctm sss JMP with (2 + 9 * pos2nat i). revert H1; apply subcode_sss_compute; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils pos subcode sss) Undecidability.Synthetic(ReducibilityFacts) Undecidability.TM(SBTM pctm_defs)