proposition: Lemma vec_change_shift_counter {x a v w a' v' w' n} : Vector.append (a' ## v') w' = vec_change (Vector.append (a ## v) w) x n -> vec_change (0 ## Vector.append v (Vector.append w (a ## vec_nil))) (shift_counter x) n = (0 ## Vector.append v' (Vector.append w' (a' ## vec_nil))).
proof: Proof. rewrite /shift_counter [in (vec_change _ x _)](eq_sym (pos_lr_both _ _ x)). case: (pos_both (1 + k) k' x) => [Y|Y]. - have [->|[Y' ->]] := pos_S_inv Y. + rewrite !vec_app_eq !vec_app_cons /= !vec_change_app_right /= -!vec_app_eq. by move=> /Vector.cons_inj [<-] /vec_append_inj [<- <-]. + rewrite !vec_app_eq !vec_app_cons /= !vec_change_app_left -!vec_app_eq. by move=> /Vector.cons_inj [<-] /vec_append_inj [<- <-]. - rewrite !vec_app_eq !vec_app_cons /= !vec_change_app_right !vec_change_app_left -!vec_app_eq. by move=> /Vector.cons_inj [<-] /vec_append_inj [-> ->]. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect