proposition: Lemma eval_dot_inv: forall n p u v c, eval n p (RegExp.dot u v) c -> exists m, exists a, exists b, c = a*b /\ eval n m u a /\ eval m p v b.
proof: Proof. intros. dependent destruction H. eauto 6. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)