proposition: Lemma PACK_spec X Y v offset : let x := vec_pos v X in let y := vec_pos v Y in A <> X -> A <> Y -> X <> Y -> (offset, PACK X Y offset) // (offset, v) ->> (PACK_len+offset, vec_change (vec_change (vec_change v X ((x+x+1) * (2 ^ y))) Y 0) A 0).
proof: Proof. move=> /= HX HY HXY. apply: (concat_sss_compute_trans 0). { by apply: DOUBLE_spec. } apply: mma_step. apply: (concat_sss_compute_trans 2). { by apply: JMP_spec. } move Ev': (v' in _ // (_, v') ->> _) => v'. have HAv' : vec_pos v' A = 0. { by rewrite -Ev' (vec_change_neq (nesym HX)) vec_change_eq. } have : let x := vec_pos v' X in let y := vec_pos v' Y in forall w, w = vec_change (vec_change (vec_change v' A 0) Y 0) X (x * (2 ^ y)) -> (offset, PACK X Y offset) // (DOUBLE_len + JMP_len + (1 + (DOUBLE_len + offset)), v') ->> (1 + DOUBLE_len + JMP_len + (1 + (DOUBLE_len + offset)), w). { move En: (vec_pos v' Y) => n /=. elim: n (v') En HAv'. - move=> v'' En HAv'' w ->. rewrite ?(Nat.add_assoc _ _ offset). apply: mma_step. rewrite /= En. apply: sss_compute_refl'. congr pair. rewrite (vec_change_same' _ A) // (vec_change_same' _ Y) // vec_change_same' //=. lia. - move=> n IH v'' En HAv'' w ->. rewrite ?(Nat.add_assoc _ _ offset). apply: mma_step. rewrite /= En. apply: (concat_sss_compute_trans 3). { by apply: DOUBLE_spec. } apply: IH. + by rewrite !(vec_change_neq HY) !(vec_change_neq HXY) vec_change_eq. + by rewrite vec_change_eq. + rewrite !(vec_norm HY) !(vec_norm HX) !(vec_norm HXY) /=. congr vec_change. congr vec_change. lia. } move=> /(_ _ erefl) /sss_compute_trans. apply. apply: sss_compute_refl'. congr pair. rewrite -Ev' /=. do ? rewrite ?(vec_norm HY) ?(vec_norm HX) ?(vec_norm HXY). congr vec_change. congr vec_change. lia. 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