proposition: Lemma eval_clean: forall A B x y, eval A B x y -> exists2 z, eval A B (clean x) z & y==z.
proof: Proof. intros A B x y H; induction H; simpl; try (eexists; [ eauto || fail |]); trivial. RegExp.destruct_tests. exists 0; auto. destruct IHeval1 as [z Hz Hxz]; clear IHeval2. rewrite Hxz, (eval_zero_inv Hz); auto with algebra. exists 0; auto. destruct IHeval2 as [z Hz Hyz]; clear IHeval1. rewrite Hyz, (eval_zero_inv Hz); auto with algebra. destruct IHeval1; destruct IHeval2; eauto with compat. RegExp.destruct_tests. destruct IHeval2 as [y'' Hy'' Hy]; exists y''; auto. destruct IHeval1 as [z Hz Hxz]. rewrite Hxz, (eval_zero_inv Hz), Hy. auto with algebra. destruct IHeval1 as [y'' Hy'' Hy]; exists y''; auto. destruct IHeval2 as [z Hz Hxz]. rewrite Hxz, (eval_zero_inv Hz), Hy. auto with algebra. destruct IHeval1; destruct IHeval2; eauto with compat. RegExp.destruct_tests. exists 1; auto. destruct IHeval as [z Hz Hxz]. rewrite Hxz. eval_inversion. apply star_zero. destruct IHeval as [x'' Hx'' Hx]; eauto with compat. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)