proposition: Lemma pump_app_r: forall re1 re2 s1 s2, RexPump re2 s2 -> s1 \in re1 -> length s1 <= pumping_constant re1 -> RexPump (re1 ;; re2) (s1 ++ s2).
proof: Proof. intros. inversion H; subst; clear H. rewrite app_assoc. apply rex_pump_def with (x:=s1++x) (y:=y) (z:=z). - reflexivity. - assumption. - simpl. repeat rewrite app_length in *. rewrite Plus.plus_assoc_reverse. apply Plus.plus_le_compat; auto. - intros m. apply accept_app with (s1:=s1) (s2:=x ++ pow y m ++ z); auto. repeat rewrite <- app_assoc. reflexivity. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang