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