proposition: Lemma PROG_start_spec offset v w : (offset, PROG offset) // (JMP_len + offset, v) ->> (offset, w) -> (offset, PROG offset) // (offset, v) -+> (offset, w).
proof: Proof. move=> ?. apply: sss_progress_compute_trans. { apply: sss_compute_progress. { by apply: (concat_sss_compute_trans 0); [apply JMP_spec | apply: sss_compute_refl]. } case. rewrite /JMP_len /=. lia. } done. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun