proposition: Lemma PACK_spec A 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 A 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=> /= /[dup] HX /nesym H'X /[dup] HY /nesym H'Y HXY. apply: (compose_sss_compute_trans 0). { by apply: ZERO_spec. } apply: (compose_sss_compute_trans 1). { by apply: MOVE2_spec. } apply: (compose_sss_compute_trans 2). { by apply: INC_spec. } apply: (compose_sss_compute_trans 3). { by apply: MOVE_spec. } apply: (compose_sss_compute_trans 4). { by apply: JMP_spec. } rewrite !(vec_norm HX) !Nat.add_0_l. have -> : S ((v#>X) + (v#>X)) = (v#>X) + (v#>X) + 1 by lia. move: ((v#>X) + (v#>X) + 1). elim /(induction_ltof1 _ (fun w => vec_pos w Y)) : v => v IH x. case EY: (vec_pos v Y) => [|n]. { apply: (compose_sss_compute_trans 7). { by apply: DEC_spec. } rewrite !(vec_norm HY) !(vec_norm HXY) EY. apply: sss_compute_refl'. congr pair. by rewrite (vec_change_same' EY) /= Nat.mul_1_r. } apply: (compose_sss_compute_trans 7). { by apply: DEC_spec. } rewrite !(vec_norm HY) !(vec_norm HXY) EY. apply: (compose_sss_compute_trans 5). { by apply: MOVE2_spec. } apply: (compose_sss_compute_trans 6). { by apply: MOVE_spec. } do 2 rewrite ?(vec_norm HX) ?(vec_norm HY) ?(vec_norm HXY). apply: sss_compute_trans. { apply: IH. by rewrite /= !(vec_norm HY) EY. } apply: sss_compute_refl'. congr pair. rewrite ?(vec_norm HX) ?(vec_norm HY) ?(vec_norm HXY). rewrite /=. do 2 congr vec_change. lia. 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