Set Rewrite Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Frederic New page: {{RRHeader}} {{RRRow}}|<font size="-2"> SIMP_SPECIAL_AND_BTRUE </font>||<math> P \land \ldots \land \btrue \land \ldots \land Q \;\;\defi\;\; P \land \ldots \land Q </math>|| ... |
imported>Frederic No edit summary |
||
Line 16: | Line 16: | ||
{{RRRow}}|<font size="-2"> SIMP_MULTI_IMP_AND_NOT_R </font>||<math> P \land \ldots \land Q \land \ldots \land R \limp \lnot\, Q \;\;\defi\;\; \lnot\,(P \land \ldots \land Q \land \ldots \land R) </math>|| || A | {{RRRow}}|<font size="-2"> SIMP_MULTI_IMP_AND_NOT_R </font>||<math> P \land \ldots \land Q \land \ldots \land R \limp \lnot\, Q \;\;\defi\;\; \lnot\,(P \land \ldots \land Q \land \ldots \land R) </math>|| || A | ||
{{RRRow}}|<font size="-2"> SIMP_MULTI_IMP_AND_NOT_L </font>||<math> P \land \ldots \land \lnot\, Q \land \ldots \land R \limp Q \;\;\defi\;\; \lnot\,(P \land \ldots \land \lnot\, Q \land \ldots \land R) </math>|| || A | {{RRRow}}|<font size="-2"> SIMP_MULTI_IMP_AND_NOT_L </font>||<math> P \land \ldots \land \lnot\, Q \land \ldots \land R \limp Q \;\;\defi\;\; \lnot\,(P \land \ldots \land \lnot\, Q \land \ldots \land R) </math>|| || A | ||
{{RRRow}}|<font size="-2"> SIMP_MULTI_EQV </font>||<math> P \leqv P \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|<font size="-2"> SIMP_MULTI_EQV </font>||<math> P \leqv P \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|<font size="-2"> SIMP_MULTI_EQV_NOT </font>||<math> P \leqv \lnot\, P \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|<font size="-2"> SIMP_MULTI_EQV_NOT </font>||<math> P \leqv \lnot\, P \;\;\defi\;\; \bfalse </math>|| || A | ||
Line 124: | Line 122: | ||
{{RRRow}}|<font size="-2"> SIMP_FINITE_QUNION </font>||<math> \finite (\Union x \qdot P \mid E) \;\;\defi\;\; \forall x \qdot P \limp \finite (E) </math>|| || M | {{RRRow}}|<font size="-2"> SIMP_FINITE_QUNION </font>||<math> \finite (\Union x \qdot P \mid E) \;\;\defi\;\; \forall x \qdot P \limp \finite (E) </math>|| || M | ||
{{RRRow}}|<font size="-2"> SIMP_FINITE_QINTER </font>||<math> \finite (\Inter x \qdot P \mid E) \;\;\defi\;\; \exists x \qdot P \land \finite (E) </math>|| || M | {{RRRow}}|<font size="-2"> SIMP_FINITE_QINTER </font>||<math> \finite (\Inter x \qdot P \mid E) \;\;\defi\;\; \exists x \qdot P \land \finite (E) </math>|| || M | ||
{{RRRow}}|<font size="-2"> SIMP_FINITE_ID </font>||<math> \finite (\id (S)) \;\;\defi\;\; \finite (S) </math>|| || A | |||
{{RRRow}}|<font size="-2"> SIMP_FINITE_NATURAL </font>||<math> \finite (\nat ) \;\;\defi\;\; \bfalse </math>|| || A | |||
{{RRRow}}|<font size="-2"> SIMP_FINITE_NATURAL1 </font>||<math> \finite (\natn ) \;\;\defi\;\; \bfalse </math>|| || A | |||
{{RRRow}}|<font size="-2"> SIMP_FINITE_INTEGER </font>||<math> \finite (\intg ) \;\;\defi\;\; \bfalse </math>|| || A | |||
{{RRRow}}|<font size="-2"> SIMP_FINITE_LAMBDA </font>||<math> \finite (\lambda x \qdot P \mid E) \;\;\defi\;\; \finite (\{ x \qdot P \mid x\} ) </math>|| || A | |||
{{RRRow}}|<font size="-2"> SIMP_TYPE_EQUAL_EMPTY </font>||<math> \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|<font size="-2"> SIMP_TYPE_EQUAL_EMPTY </font>||<math> \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
{{RRRow}}|<font size="-2"> SIMP_TYPE_IN </font>||<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|<font size="-2"> SIMP_TYPE_IN </font>||<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression || A |
Revision as of 10:18, 30 January 2009
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
SIMP_SPECIAL_AND_BTRUE | ![]() |
A | ||
SIMP_SPECIAL_AND_BFALSE | ![]() |
A | ||
SIMP_MULTI_AND | ![]() |
A | ||
SIMP_MULTI_AND_NOT | ![]() |
A | ||
SIMP_SPECIAL_OR_BTRUE | ![]() |
A | ||
SIMP_SPECIAL_OR_BFALSE | ![]() |
A | ||
SIMP_MULTI_OR | ![]() |
A | ||
SIMP_MULTI_OR_NOT | ![]() |
A | ||
SIMP_SPECIAL_IMP_BTRUE_R | ![]() |
A | ||
SIMP_SPECIAL_IMP_BTRUE_L | ![]() |
A | ||
SIMP_SPECIAL_IMP_BFALSE_R | ![]() |
A | ||
SIMP_SPECIAL_IMP_BFALSE_L | ![]() |
A | ||
SIMP_MULTI_IMP | ![]() |
A | ||
SIMP_MULTI_IMP_OR | ![]() |
A | ||
SIMP_MULTI_IMP_AND_NOT_R | ![]() |
A | ||
SIMP_MULTI_IMP_AND_NOT_L | ![]() |
A | ||
SIMP_MULTI_EQV | ![]() |
A | ||
SIMP_MULTI_EQV_NOT | ![]() |
A | ||
SIMP_MULTI_EQV_NOT_NOT | ![]() |
A | ||
SIMP_SPECIAL_NOT_BTRUE | ![]() |
A | ||
SIMP_SPECIAL_NOT_BFALSE | ![]() |
A | ||
SIMP_NOT_NOT | ![]() |
A | ||
SIMP_NOTEQUAL | ![]() |
A | ||
SIMP_NOTIN | ![]() |
A | ||
SIMP_NOTSUBSET | ![]() |
A | ||
SIMP_NOTSUBSETEQ | ![]() |
A | ||
SIMP_NOT_LE | ![]() |
A | ||
SIMP_NOT_GE | ![]() |
A | ||
SIMP_NOT_LT | ![]() |
A | ||
SIMP_NOT_GT | ![]() |
A | ||
SIMP_SPECIAL_NOT_EQUAL_FALSE_R | ![]() |
A | ||
SIMP_SPECIAL_NOT_EQUAL_FALSE_L | ![]() |
A | ||
SIMP_SPECIAL_NOT_EQUAL_TRUE_R | ![]() |
A | ||
SIMP_SPECIAL_NOT_EQUAL_TRUE_L | ![]() |
A | ||
SIMP_FORALL_AND | ![]() |
A | ||
SIMP_EXIST_AND | ![]() |
A | ||
SIMP_FORALL | ![]() |
A | ||
SIMP_EXIST | ![]() |
A | ||
SIMP_MULTI_EQUAL | ![]() |
A | ||
SIMP_MULTI_NOTEQUAL | ![]() |
A | ||
SIMP_EQUAL_MAPSTO | ![]() |
A | ||
SIMP_EQUAL_SING | ![]() |
A | ||
SIMP_SPECIAL_EQUAL_TRUE | ![]() |
A | ||
SIMP_TYPE_SUBSETEQ | ![]() |
where ![]() |
A | |
SIMP_SUBSETEQ_SING | ![]() |
where ![]() |
A | |
SIMP_SPECIAL_SUBSETEQ | ![]() |
A | ||
SIMP_MULTI_SUBSETEQ | ![]() |
A | ||
SIMP_SUBSETEQ_BUNION | ![]() |
A | ||
SIMP_SUBSETEQ_BINTER | ![]() |
A | ||
DERIV_SUBSETEQ_BUNION | ![]() |
M | ||
DERIV_SUBSETEQ_BINTER | ![]() |
M | ||
SIMP_SUBSET_BUNION | ![]() |
A | ||
SIMP_SUBSET_BINTER | ![]() |
A | ||
SIMP_SPECIAL_IN | ![]() |
A | ||
SIMP_MULTI_IN | ![]() |
A | ||
SIMP_IN_SING | ![]() |
A | ||
SIMP_MULTI_SETENUM | ![]() |
A | ||
SIMP_SPECIAL_BINTER | ![]() |
A | ||
SIMP_TYPE_BINTER | ![]() |
where ![]() |
A | |
SIMP_MULTI_BINTER | ![]() |
A | ||
SIMP_MULTI_EQUAL_BINTER | ![]() |
A | ||
SIMP_SPECIAL_BUNION | ![]() |
A | ||
SIMP_TYPE_BUNION | ![]() |
where ![]() |
A | |
SIMP_MULTI_BUNION | ![]() |
A | ||
SIMP_MULTI_EQUAL_BUNION | ![]() |
A | ||
SIMP_MULTI_SETMINUS | ![]() |
A | ||
SIMP_SPECIAL_SETMINUS_R | ![]() |
A | ||
SIMP_SPECIAL_SETMINUS_L | ![]() |
A | ||
SIMP_TYPE_SETMINUS | ![]() |
where ![]() |
A | |
SIMP_TYPE_SETMINUS_SETMINUS | ![]() |
where ![]() |
A | |
SIMP_TYPE_KUNION | ![]() |
where ![]() ![]() |
A | |
SIMP_KUNION_POW | ![]() |
A | ||
SIMP_KUNION_POW1 | ![]() |
A | ||
SIMP_SPECIAL_KUNION | ![]() |
A | ||
SIMP_SPECIAL_KUNION | ![]() |
A | ||
SIMP_SPECIAL_KINTER | ![]() |
A | ||
SIMP_TYPE_KINTER | ![]() |
where ![]() |
A | |
SIMP_SPECIAL_POW | ![]() |
A | ||
SIMP_SPECIAL_POW1 | ![]() |
A | ||
SIMP_SPECIAL_CPROD_R | ![]() |
A | ||
SIMP_SPECIAL_CPROD_L | ![]() |
A | ||
SIMP_COMPSET_EQUAL | ![]() |
where ![]() ![]() |
A | |
SIMP_COMPSET_IN | ![]() |
where ![]() ![]() |
A | |
SIMP_SPECIAL_COMPSET_BFALSE | ![]() |
A | ||
SIMP_SPECIAL_COMPSET_BTRUE | ![]() |
where the type od ![]() ![]() |
A | |
SIMP_SUBSETEQ_COMPSET_L | ![]() |
where ![]() ![]() |
A | |
SIMP_SPECIAL_EQUAL_COMPSET | ![]() |
A | ||
SIMP_IN_COMPSET | ![]() |
A | ||
SIMP_SUBSETEQ_COMPSET_R | ![]() |
where ![]() ![]() |
A | |
SIMP_SPECIAL_OVERL | ![]() |
A | ||
SIMP_MULTI_OVERL | ![]() |
A | ||
SIMP_TYPE_OVERL_CPROD | ![]() |
where ![]() |
A | |
SIMP_SPECIAL_KBOOL_BTRUE | ![]() |
A | ||
SIMP_SPECIAL_KBOOL_BFALSE | ![]() |
A | ||
DISTRI_SUBSETEQ_BUNION_SING | ![]() |
where ![]() |
M | |
SIMP_SPECIAL_FINITE | ![]() |
A | ||
SIMP_FINITE_SETENUM | ![]() |
A | ||
SIMP_FINITE_BUNION | ![]() |
A | ||
SIMP_FINITE_POW | ![]() |
A | ||
DERIV_FINITE_CPROD | ![]() |
A | ||
SIMP_FINITE_CONVERSE | ![]() |
A | ||
SIMP_FINITE_UPTO | ![]() |
A | ||
SIMP_FINITE_BINTER_L | ![]() |
M | ||
SIMP_FINITE_BINTER_R | ![]() |
M | ||
SIMP_FINITE_SETMINUS | ![]() |
M | ||
SIMP_FINITE_DOMRES | ![]() |
M | ||
SIMP_FINITE_RANRES | ![]() |
M | ||
SIMP_FINITE_DOMSUB | ![]() |
M | ||
SIMP_FINITE_RANSUB | ![]() |
M | ||
SIMP_FINITE_RELIMAGE | ![]() |
M | ||
SIMP_FINITE_CPROD | ![]() |
M | ||
SIMP_FINITE_OVERL | ![]() |
M | ||
SIMP_FINITE_REL | ![]() |
M | ||
SIMP_FINITE_FCOMP | ![]() |
M | ||
SIMP_FINITE_BCOMP | ![]() |
M | ||
SIMP_FINITE_DPROD | ![]() |
M | ||
SIMP_FINITE_PPROD | ![]() |
M | ||
SIMP_FINITE_COMPSET | ![]() |
where ![]() ![]() |
M | |
SIMP_FINITE_RAN | ![]() |
M | ||
SIMP_FINITE_DOM | ![]() |
M | ||
SIMP_FINITE_QUNION | ![]() |
M | ||
SIMP_FINITE_QINTER | ![]() |
M | ||
SIMP_FINITE_ID | ![]() |
A | ||
SIMP_FINITE_NATURAL | ![]() |
A | ||
SIMP_FINITE_NATURAL1 | ![]() |
A | ||
SIMP_FINITE_INTEGER | ![]() |
A | ||
SIMP_FINITE_LAMBDA | ![]() |
A | ||
SIMP_TYPE_EQUAL_EMPTY | ![]() |
where ![]() |
A | |
SIMP_TYPE_IN | ![]() |
where ![]() |
A | |
SIMP_SPECIAL_FORALL_BTRUE | ![]() |
A | ||
SIMP_SPECIAL_FORALL_BFALSE | ![]() |
A | ||
SIMP_SPECIAL_EXIST_BTRUE | ![]() |
A | ||
SIMP_SPECIAL_EXIST_BFALSE | ![]() |
A | ||
SIMP_SPECIAL_EQV_BTRUE | ![]() |
A | ||
SIMP_SPECIAL_EQV_BFALSE | ![]() |
A | ||
SIMP_SPECIAL_SUBSET_R | ![]() |
A | ||
SIMP_SPECIAL_SUBSET_L | ![]() |
A | ||
SIMP_TYPE_SUBSET_L | ![]() |
where ![]() |
A | |
SIMP_MULTI_SUBSET | ![]() |
A | ||
DISTRI_AND_OR | ![]() |
M | ||
DISTRI_OR_AND | ![]() |
M | ||
DEF_OR | ![]() |
M | ||
DERIV_IMP | ![]() |
M | ||
DERIV_IMP_IMP | ![]() |
M | ||
DISTRI_IMP_AND | ![]() |
M | ||
DISTRI_IMP_OR | ![]() |
M | ||
DEF_EQV | ![]() |
M | ||
DISTRI_NOT_AND | ![]() |
M | ||
DISTRI_NOT_OR | ![]() |
M | ||
DERIV_NOT_IMP | ![]() |
M | ||
DERIV_NOT_FORALL | ![]() |
M | ||
DERIV_NOT_EXIST | ![]() |
M | ||
DEF_SPECIAL_NOT_EQUAL | ![]() |
M | ||
DEF_IN_MAPSTO | ![]() |
M | ||
DEF_IN_POW | ![]() |
M | ||
DEF_SUBSETEQ | ![]() |
M | ||
DEF_IN_BUNION | ![]() |
M | ||
DEF_IN_BINTER | ![]() |
M | ||
DEF_IN_SETMINUS | ![]() |
M | ||
DEF_IN_SETENUM | ![]() |
M | ||
DEF_IN_KUNION | ![]() |
M | ||
DEF_IN_QUNION | ![]() |
M | ||
DEF_IN_KINTER | ![]() |
M | ||
DEF_IN_QINTER | ![]() |
M | ||
DISTRI_BUNION_BINTER | ![]() |
M | ||
DISTRI_BINTER_BUNION | ![]() |
M | ||
DISTRI_BINTER_SETMINUS | ![]() |
M | ||
DISTRI_SETMINUS_BUNION | ![]() |
M | ||
DERIV_TYPE_SETMINUS_BINTER | ![]() |
where ![]() |
M | |
DERIV_TYPE_SETMINUS_BUNION | ![]() |
where ![]() |
M | |
DERIV_TYPE_SETMINUS_SETMINUS | ![]() |
where ![]() |
M | |
DISTRI_CPROD_BINTER | ![]() |
M | ||
DISTRI_CPROD_BUNION | ![]() |
M | ||
DISTRI_CPROD_SETMINUS | ![]() |
M | ||
DERIV_SUBSETEQ | ![]() |
where ![]() ![]() ![]() |
M | |
DERIV_EQUAL | ![]() |
where ![]() ![]() ![]() |
M | |
DERIV_SUBSETEQ_SETMINUS_L | ![]() |
M | ||
DERIV_SUBSETEQ_SETMINUS_R | ![]() |
M |