proposition: Lemma JZ_spec X p v offset : (offset, JZ X p offset) // (offset, v) ->> (if vec_pos v X is 0 then p else JZ_len+offset, v).
proof: Proof. case EX: (vec_pos v X) => [|n]. - apply: (compose_sss_compute_trans 0). { by apply: DEC_spec. } rewrite EX. apply: (compose_sss_compute_trans 1). { by apply: JMP_spec. } by apply: sss_compute_refl. - apply: (compose_sss_compute_trans 0). { by apply: DEC_spec. } rewrite EX. apply: (compose_sss_compute_trans 2). { by apply: INC_spec. } apply: sss_compute_refl'. congr pair. by rewrite vec_change_idem vec_change_eq // vec_change_same'. 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