proposition: Fact pctm_compute_JMP P i j t st : (i,[BR j j]) <sc P -> P // (j,t) ->> st -> P // (i,t) ->> st.
proof: Proof. intros; eapply sss_progress_compute, pctm_progress_JMP; eauto. Qed.
imports: List Bool Arith Lia Undecidability.Shared.Libs.DLW(subcode sss) Undecidability.TM(SBTM)