proposition: Lemma eval_sequal: forall x y, sequal x y -> forall A B x', eval A B x x' -> exists2 y', eval A B y y' & x'==y'.
proof: Proof. intros x y H. cut ((forall A B x', eval A B x x' -> exists2 y', eval A B y y' & x'==y') /\ (forall A B y', eval A B y y' -> exists2 x', eval A B x x' & y'==x')); [tauto| ]. induction H; (apply and_idem || split); intros A B xe Hx; eval_inversion; try solve [split_IHeval; eexists; [eauto; fail | eval_injection; auto with algebra ]]. destruct (eval_type_inj_left H4 H5) as [HB | Hz]; [ destruct HB | rewrite Hz in H; discriminate ]. eexists; eauto. rewrite (eval_inj H4 H5); symmetry; apply dot_distr_left. destruct (eval_type_inj_right H2 H3) as [HB | Hz]; [ destruct HB | rewrite Hz in H; discriminate ]. eexists; eauto. rewrite (eval_inj H3 H2); symmetry; apply dot_distr_right. eexists; eauto. eval_injection. apply star_destruct_left; unfold leq. destruct (proj1 IHsequal _ _ (x0*x4+x4)) as [ y1 ? Hy1 ]; auto. rewrite Hy1. eval_injection. reflexivity. destruct (proj2 IHsequal _ _ _ Hx) as [ x' Hx' ]. eval_inversion. destruct (eval_type_inj_left H4 H6) as [HB | Hz]; [ destruct HB | rewrite Hz in H; discriminate ]. eexists; eauto. eval_injection. symmetry; apply star_destruct_left; unfold leq. auto. eexists; eauto. eval_injection. apply star_destruct_right; unfold leq. destruct (proj1 IHsequal _ _ (x3*x0+x3)) as [ y1 ? Hy1 ]; auto. rewrite Hy1. eval_injection. reflexivity. destruct (proj2 IHsequal _ _ _ Hx) as [ x' Hx' ]. eval_inversion. destruct (eval_type_inj_right H4 H5) as [HB | Hz]; [ destruct HB | rewrite Hz in H; discriminate ]. eexists; eauto. eval_injection. symmetry; apply star_destruct_right; unfold leq. auto. split_IHeval; eauto using Graph.equal_trans. split_IHeval; eauto using Graph.equal_trans. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)