proposition: Lemma MOVE2_spec X Y Z v offset : X <> Y -> X <> Z -> (offset, MOVE2 X Y Z offset) // (offset, v) ->> (MOVE2_len+offset, vec_change (vec_change (vec_change v Z (vec_pos v Z + vec_pos v X)) Y (vec_pos ((vec_change v Z (vec_pos v Z + vec_pos v X))) Y + vec_pos v X)) X 0).
proof: Proof. move=> HXY HXZ. apply: (compose_sss_compute_trans 0). { by apply: JMP_spec. } elim /(induction_ltof1 _ (fun w => vec_pos w X)) : v => v IH. case EX: (vec_pos v X) => [|n]. { apply: (compose_sss_compute_trans 3). { by apply: DEC_spec. } rewrite EX !Nat.add_0_r !vec_change_same (vec_change_same' EX). by apply: sss_compute_refl. } apply: (compose_sss_compute_trans 3). { by apply: DEC_spec. } rewrite EX. apply: (compose_sss_compute_trans 1). { by apply: INC_spec. } apply: (compose_sss_compute_trans 2). { by apply: INC_spec. } apply: sss_compute_trans. { apply: IH. by rewrite /= !(vec_norm HXY) !(vec_norm HXZ) EX. } apply: sss_compute_refl'. congr pair. have [<-|HYZ] := pos_eq_dec Y Z. - by rewrite !(vec_norm HXY) -!Nat.add_succ_comm. - do 2 rewrite ?(vec_norm HXY) ?(vec_norm HXZ) ?(vec_norm HYZ). 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