proposition: Lemma vec_pos_shift_counter x a v w : vec_pos (0 ## Vector.append v (Vector.append w (a ## vec_nil))) (shift_counter x) = vec_pos (a ## Vector.append v w) x.
proof: Proof. rewrite /shift_counter [in RHS](eq_sym (pos_lr_both _ _ x)). case: (pos_both (1 + k) k' x) => [Y|Y]. - have [->|[Y' ->]] := pos_S_inv Y. + by rewrite !vec_app_eq /= !vec_pos_app_right. + by rewrite !vec_app_eq /= !vec_pos_app_left. - by rewrite !vec_app_eq /= !vec_pos_app_right !vec_pos_app_left. 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