proposition: Lemma JMP_spec p v offset : (offset, JMP p) // (0 + offset, v) ->> (p, v).
proof: Proof. apply: mma_step. apply: mma_step. rewrite /= (vec_change_eq erefl) vec_change_idem vec_change_same. by apply: sss_compute_refl. 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