proposition: Lemma app_depth_r_subst_many_repeat n s ts : app_depth_r (subst_many s n ts) = app_depth_r (subst_many s 0 ((repeat (var 0) n) ++ ts)).
proof: Proof. elim: s n ts. - move=> x n ts /=. have [?|?] : x < n \/ n <= x by lia. + rewrite app_nth1. { by rewrite map_length seq_length. } rewrite app_nth1. { by rewrite repeat_length. } rewrite map_nth (@nth_indep _ _ x (var x) (var 0)). { by rewrite repeat_length. } by rewrite nth_repeat seq_nth. + rewrite app_nth2 map_length seq_length. { done. } by rewrite app_nth2 repeat_length. - by move=> ? _ ? + ?? /= => ->. - move=> s IH n ts /=. by rewrite [LHS]IH [RHS]IH app_assoc -repeat_app. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun