proposition: Lemma eval_clean_zero: forall x A B z, eval A B x z -> RegExp.is_zero (clean x) = true -> z==0.
proof: Proof. induction x; simpl; intros A B z Hz H; try discriminate; eval_inversion. reflexivity. case_eq (RegExp.is_zero (clean x1)); intro Hx1. rewrite (IHx1 _ _ _ H1 Hx1); apply dot_ann_left. case_eq (RegExp.is_zero (clean x2)); intro Hx2. rewrite (IHx2 _ _ _ H2 Hx2); apply dot_ann_right. rewrite Hx1, Hx2 in H; discriminate. case_eq (RegExp.is_zero (clean x1)); intro Hx1; case_eq (RegExp.is_zero (clean x2)); intro Hx2; rewrite Hx1, Hx2, ?Hx1 in H; try discriminate. rewrite (IHx1 _ _ _ H1 Hx1), (IHx2 _ _ _ H2 Hx2); apply plus_idem. case_eq (RegExp.is_zero (clean x)); intro Hx; rewrite Hx in H; discriminate. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)