proposition: Lemma eval_clean: forall A B x y, eval A B x y -> exists2 z, eval A B (clean0 x) z & y==z.
proof: Proof. intros A B x y H; induction H; simpl. exists 1; auto. exists 0; auto. destruct_tests. exists 0; auto. destruct IHeval1 as [z Hz Hxz]; clear IHeval2. rewrite Hxz, (eval_zero_inv Hz); apply dot_ann_left. exists 0; auto. destruct IHeval2 as [z Hz Hyz]; clear IHeval1. rewrite Hyz, (eval_zero_inv Hz); apply dot_ann_right. destruct IHeval1; destruct IHeval2; eauto with compat. destruct_tests. destruct IHeval2 as [y'' Hy'' Hy]; exists y''; auto. destruct IHeval1 as [z Hz Hxz]. rewrite Hxz, (eval_zero_inv Hz), Hy. apply plus_neutral_left. destruct IHeval1 as [y'' Hy'' Hy]; exists y''; auto. destruct IHeval2 as [z Hz Hxz]. rewrite Hxz, (eval_zero_inv Hz), Hy. apply plus_neutral_right. destruct IHeval1; destruct IHeval2; eauto with compat. eexists; auto. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)