proposition: Lemma normalizer {n} {m} {R} `{T: Transitive (Classes.X (typ n) (typ m)) R} `{H: subrelation _ (equal _ _) R} norm (Hnorm: forall x, RegExp.equal x (norm x)): forall a b a' b', (let na := norm (erase a) in eval n m na a') -> (let nb := norm (erase b) in eval n m nb b') -> R a' b' -> R (feval a) (feval b).
proof: Proof. intros until b'; intros Ha Hb Hab. transitivity a'. apply H. eapply equal_eval; eauto using eval_erase_feval. rewrite Hab. apply H. symmetry. eapply equal_eval; eauto using eval_erase_feval. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)