proposition: Lemma JMP_spec A p v offset : (offset, JMP A p offset) // (offset, v) ->> (p, v).
proof: Proof. rewrite /=. apply: (compose_sss_compute_trans 0). { by apply: INC_spec. } rewrite /=. apply: (compose_sss_compute_trans 1). { by apply: DEC_spec. } rewrite /= (vec_change_eq _ _ erefl) vec_change_idem vec_change_same. by apply sss_compute_refl. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun