proposition: Lemma sbtm2pctm_complete t : (1,sbtm2pctm) // (1,t) ↓ -> exists k, steps M k (i,t) = None.
proof: Proof. unfold sbtm2pctm. intros H. apply Q_steps. apply subcode_sss_terminates_inv with (1 := pctm_sss_fun) (P := (1,[JMP (2 + 9 * pos2nat i)])) (st1 := (2+9*pos2nat i,t)) in H; auto. * revert H; apply subcode_sss_terminates; auto. * split; [ | simpl; lia ]. pctm sss JMP with (2+9*pos2nat i). - apply subcode_refl. - pctm sss stop. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils pos subcode sss) Undecidability.Synthetic(ReducibilityFacts) Undecidability.TM(SBTM pctm_defs)