Empty Set Rewrite Rules
From Event-B
Revision as of 13:27, 22 May 2013 by imported>Josselin (Added rules SIMP_BINTER_SING_EQUAL_EMPTY, SIMP_BINTER_SETMINUS_EQUAL_EMPTY)
Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_Rules.
All rewrite rules that match the pattern are also applicable to predicates of the form
and
, as these predicates are equivalent. All rewrite rules that match the pattern
are also applicable to predicates of the form
and
, as these predicates are equivalent.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | DEF_SPECIAL_NOT_EQUAL |
![]() |
where ![]() ![]() |
M |
SIMP_SETENUM_EQUAL_EMPTY |
![]() |
A | ||
* | SIMP_SPECIAL_EQUAL_COMPSET |
![]() |
A | |
SIMP_BINTER_EQUAL_TYPE |
![]() |
where ![]() |
A | |
SIMP_BINTER_SING_EQUAL_EMPTY |
![]() |
A | ||
SIMP_BINTER_SETMINUS_EQUAL_EMPTY |
![]() |
A | ||
SIMP_BUNION_EQUAL_EMPTY |
![]() |
A | ||
SIMP_SETMINUS_EQUAL_EMPTY |
![]() |
A | ||
SIMP_SETMINUS_EQUAL_TYPE |
![]() |
where ![]() |
A | |
SIMP_POW_EQUAL_EMPTY |
![]() |
A | ||
SIMP_POW1_EQUAL_EMPTY |
![]() |
A | ||
SIMP_KINTER_EQUAL_TYPE |
![]() |
where ![]() |
A | |
SIMP_KUNION_EQUAL_EMPTY |
![]() |
A | ||
SIMP_QINTER_EQUAL_TYPE |
![]() |
where ![]() |
A | |
SIMP_QUNION_EQUAL_EMPTY |
![]() |
A | ||
SIMP_NATURAL_EQUAL_EMPTY |
![]() |
A | ||
SIMP_NATURAL1_EQUAL_EMPTY |
![]() |
A | ||
* | SIMP_TYPE_EQUAL_EMPTY |
![]() |
where ![]() |
A |
SIMP_CPROD_EQUAL_EMPTY |
![]() |
A | ||
SIMP_CPROD_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A | |
SIMP_UPTO_EQUAL_EMPTY |
![]() |
A | ||
SIMP_UPTO_EQUAL_INTEGER |
![]() |
A | ||
SIMP_UPTO_EQUAL_NATURAL |
![]() |
A | ||
SIMP_UPTO_EQUAL_NATURAL1 |
![]() |
A | ||
* | SIMP_SPECIAL_EQUAL_REL |
![]() |
idem for operators ![]() |
A |
SIMP_TYPE_EQUAL_REL |
![]() |
where ![]() ![]() |
A | |
* | SIMP_SPECIAL_EQUAL_RELDOM |
![]() |
idem for operator ![]() |
A |
SIMP_TYPE_EQUAL_RELDOMRAN |
![]() |
where ![]() ![]() |
A | |
SIMP_SREL_EQUAL_EMPTY |
![]() |
A | ||
SIMP_STREL_EQUAL_EMPTY |
![]() |
A | ||
SIMP_DOM_EQUAL_EMPTY |
![]() |
A | ||
SIMP_RAN_EQUAL_EMPTY |
![]() |
A | ||
SIMP_FCOMP_EQUAL_EMPTY |
![]() |
A | ||
SIMP_BCOMP_EQUAL_EMPTY |
![]() |
A | ||
SIMP_DOMRES_EQUAL_EMPTY |
![]() |
A | ||
SIMP_DOMRES_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A | |
SIMP_DOMSUB_EQUAL_EMPTY |
![]() |
A | ||
SIMP_DOMSUB_EQUAL_TYPE |
![]() |
where ![]() |
A | |
SIMP_RANRES_EQUAL_EMPTY |
![]() |
A | ||
SIMP_RANRES_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A | |
SIMP_RANSUB_EQUAL_EMPTY |
![]() |
A | ||
SIMP_RANSUB_EQUAL_TYPE |
![]() |
where ![]() |
A | |
SIMP_CONVERSE_EQUAL_EMPTY |
![]() |
A | ||
SIMP_CONVERSE_EQUAL_TYPE |
![]() |
where ![]() |
A | |
SIMP_RELIMAGE_EQUAL_EMPTY |
![]() |
A | ||
SIMP_OVERL_EQUAL_EMPTY |
![]() |
A | ||
SIMP_DPROD_EQUAL_EMPTY |
![]() |
A | ||
SIMP_DPROD_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A | |
SIMP_PPROD_EQUAL_EMPTY |
![]() |
A | ||
SIMP_PPROD_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A | |
SIMP_ID_EQUAL_EMPTY |
![]() |
A | ||
SIMP_PRJ1_EQUAL_EMPTY |
![]() |
A | ||
SIMP_PRJ2_EQUAL_EMPTY |
![]() |
A |