proposition: Lemma UNPACK_spec {A X Y m n v offset} : let x := vec_pos v X in x = (n + n + 1) * (2 ^ m) -> A <> X -> A <> Y -> X <> Y -> (offset, UNPACK A X Y offset) // (offset, v) ->> (UNPACK_len + offset, vec_change (vec_change (vec_change v X n) Y m) A 0).
proof: Proof. move=> /= H'X HX HY HXY. apply: (compose_sss_compute_trans 0). { by apply: JZ_spec. } have ->: vec_pos v X = S (vec_pos v X - 1). { rewrite H'X. have := Nat.pow_nonzero 2 m. lia. } apply: (compose_sss_compute_trans 1). { by apply: ZERO_spec. } apply: (compose_sss_compute_trans 2). { by apply: JMP_spec. } suff: forall w, vec_pos w X = (n + n + 1) * 2 ^ m -> (offset, UNPACK A X Y offset) // ((JZ_len+ZERO_len+JMP_len+INC_len) + offset, w) ->> (UNPACK_len + offset, vec_change (vec_change (vec_change w X n) Y (m+vec_pos w Y)) A 0). { move=> H. apply: sss_compute_trans. { apply: H. by rewrite !(vec_norm HXY). } apply: sss_compute_refl'. congr pair. by rewrite !(vec_norm HXY) Nat.add_0_r. } elim: m {H'X}. { move=> w H'X. apply: (compose_sss_compute_trans 4). { by apply: HALF_spec. } rewrite H'X half_spec_odd Nat.add_0_l !(vec_norm HXY). by apply: sss_compute_refl. } move=> m IH w H'X. apply: (compose_sss_compute_trans 4). { by apply: HALF_spec. } rewrite H'X half_spec_even. apply: (compose_sss_compute_trans 3). { by apply: INC_spec. } apply: sss_compute_trans. { apply: IH. by rewrite !(vec_norm HXY) !(vec_norm HX). } apply: sss_compute_refl'. congr pair. do ? rewrite ?(vec_norm HXY) ?(vec_norm HX) ?(vec_norm HY). by rewrite Nat.add_succ_comm. 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