proposition: Lemma DOUBLE_spec X v offset : let x := vec_pos v X in A <> X -> (offset, DOUBLE X offset) // (offset, v) ->> (DOUBLE_len+offset, vec_change (vec_change v X (x+x)) A 0).
proof: Proof. move=> /= /[dup] HX /nesym H'X. apply: (concat_sss_compute_trans 0). { by apply: ZERO_spec. } apply: (concat_sss_compute_trans 1). { by apply: MOVE_spec. } apply: (concat_sss_compute_trans 2). { by apply: MOVE_spec. } apply: sss_compute_refl'. by rewrite /= !(vec_norm HX). 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