proposition: Lemma pow1_plus_xy: forall (a:ascii) z x n y, pow1 a (length x + n) ++ z = x ++ y -> x = pow1 a (length x) /\ y = pow1 a n ++ z.
proof: Proof. induction x; intros. - simpl in *. rewrite H. auto. - simpl in *. inversion H; subst; clear H. apply IHx in H2. destruct H2. split; auto. rewrite <- H. reflexivity. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util