proposition: Lemma MOVE_spec X Ys v offset : let x := vec_pos v X in match Ys with | [] => True | [Y] => X <> Y | [Y1; Y2] => X <> Y1 /\ X <> Y2 | _ => False end -> (offset, MOVE X Ys offset) // (offset, v) ->> ((MOVE_len (length Ys))+offset, vec_change (fold_right (fun Y w => vec_change w Y (vec_pos w Y + x)) v Ys) X 0).
proof: Proof. move=> /= HXYs. apply: (concat_sss_compute_trans 0). { by apply: JMP_spec. } move En: (vec_pos v X) => n. move Ew: (vec_change _ X 0) => w. elim: n v En w Ew. - move=> v En w <-. apply: mma_step. rewrite /= nth_error_app2 map_length. { done. } rewrite Nat.sub_diag /= En. apply: sss_compute_refl'. congr pair. { rewrite /MOVE_len. lia. } move: Ys HXYs => [|Y1 [|Y2 [|Y3 ?]]] /= *. all: rewrite !vec_change_same'; by [|lia]. - move=> n IH v En w <-. apply: mma_step. rewrite /= nth_error_app2 map_length. { done. } rewrite Nat.sub_diag /= En. move: Ys HXYs IH => [|Y1 [|Y2 [|Y3 ?]]] /= HXYs IH; last done. + apply: IH. * by rewrite vec_change_eq. * by rewrite vec_change_idem. + apply: mma_step. apply: IH. { by rewrite !(vec_norm HXYs). } rewrite !(vec_norm HXYs). do ? congr vec_change. lia. + apply: mma_step. apply: mma_step. have [HXY1 HXY2] := HXYs. apply: IH. { by rewrite !(vec_norm HXY1) !(vec_norm HXY2). } have [<-|HY1Y2] := pos_eq_dec Y1 Y2. * rewrite !(vec_norm HXY1). do ? congr vec_change. lia. * do 2 rewrite ?(vec_norm HXY1) ?(vec_norm HXY2) ?(vec_norm HY1Y2). do ? 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