proposition: Lemma JZ_spec X p v offset : let x := vec_pos v X in (offset, JZ X p offset) // (offset, v) ->> (if x is 0 then p else JZ_len+offset, v).
proof: Proof. move=> /=. case EX: (vec_pos v X) => [|n]. - apply: (mma_step 0). rewrite /= EX. apply: (concat_sss_compute_trans 1). { by apply: JMP_spec. } by apply: sss_compute_refl. - apply: (mma_step 0). rewrite /= EX. apply: mma_step. apply: sss_compute_refl'. by rewrite (vec_change_eq erefl) vec_change_idem -EX vec_change_same. 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