The following rules has been added to the Simplification Rewriter:
r[∅] = ∅
dom(∅) = ∅
ran(∅) = ∅
The User Manual has been updated.
This is available in the CVS.
Cheers,
Son
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Logged In: YES
user_id=1041912
Originator: NO
In the same vein, the post tactic should also simplify
dom(∅) to ∅
ran(∅) to ∅
etc. (there are surely many more similar simplifications.)
Logged In: YES
user_id=1320217
Originator: NO
The following rules has been added to the Simplification Rewriter:
r[∅] = ∅
dom(∅) = ∅
ran(∅) = ∅
The User Manual has been updated.
This is available in the CVS.
Cheers,
Son
Added rule ∅[A] == ∅ to the AutoRewriter, as proposed by Son in exploratory project _exploratory/tshoang/org.eventb.contributer.seqprover.fr1798741.