proposition: Lemma UNPACK_spec {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 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: (concat_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: (concat_sss_compute_trans 1). { by apply: ZERO_spec. } apply: (concat_sss_compute_trans 2). { by apply: ZERO_spec. } apply: (concat_sss_compute_trans 3). { by apply: JMP_spec. } suff : forall v' w', w' = vec_change (vec_change v' X n) Y (m + vec_pos v' Y) -> vec_pos v' X = (n + n + 1) * 2 ^ m -> vec_pos v' A = 0 -> (offset, UNPACK X Y offset) // (1 + JZ_len + ZERO_len + ZERO_len + JMP_len + offset, v') ->> (UNPACK_len + offset, w'). { apply. - by rewrite !(vec_norm HXY) !(vec_norm HY) !(vec_norm HX) Nat.add_0_r. - by rewrite !(vec_norm HXY) !(vec_norm HX). - by rewrite !(vec_norm HY). } elim: m {H'X}. { move=> v' w' -> H'v' H''v'. apply: (concat_sss_compute_trans 5). { by apply: HALF_spec. } rewrite H'v' half_spec_odd. apply: sss_compute_refl'. congr pair. rewrite H''v' !Nat.add_0_l !(vec_norm HXY) !(vec_norm (nesym HX)). congr vec_change. by rewrite vec_change_same'. } move=> m IH v' w' -> H'v' H''v'. apply: (concat_sss_compute_trans 5). { by apply: HALF_spec. } rewrite H'v' half_spec_even ?(Nat.add_assoc _ _ offset). apply: mma_step. apply: IH. - do ? rewrite ?(vec_norm (nesym HY)) ?(vec_norm (nesym HX)) ?(vec_norm HXY). rewrite (vec_change_same' v' A 0 H''v'). congr vec_change. congr vec_change. lia. - by rewrite !(vec_norm HXY) !(vec_norm HX) H''v'. - by rewrite !(vec_norm HY). 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