All Rewrite Rules
This page groups together all the rewrite rules implemented (or planned for implementation) in the Rodin prover. The rules themselves can be found in the following locations (for editing purposes):
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.
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_NOT_L |
![]() |
A | |
* | SIMP_MULTI_IMP_NOT_R |
![]() |
A | |
* | SIMP_MULTI_IMP_AND |
![]() |
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_SPECIAL_NOT_BTRUE |
![]() |
A | |
* | SIMP_SPECIAL_NOT_BFALSE |
![]() |
A | |
* | SIMP_NOT_NOT |
![]() |
AM | |
* | 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_EXISTS_OR |
![]() |
A | |
* | SIMP_EXISTS_IMP |
![]() |
A | |
* | SIMP_FORALL |
![]() |
Quantified identifiers other than ![]() ![]() |
A |
* | SIMP_EXISTS |
![]() |
Quantified identifiers other than ![]() ![]() |
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 |
![]() |
A | |
* | DERIV_SUBSETEQ_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_KUNION_POW |
![]() |
A | |
* | SIMP_KUNION_POW1 |
![]() |
A | |
* | SIMP_SPECIAL_KUNION |
![]() |
A | |
* | SIMP_SPECIAL_QUNION |
![]() |
A | |
* | SIMP_SPECIAL_KINTER |
![]() |
A | |
* | SIMP_KINTER_POW |
![]() |
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_COMPSET_SUBSETEQ |
![]() |
where ![]() ![]() |
A |
* | SIMP_SPECIAL_COMPSET_BFALSE |
![]() |
A | |
* | SIMP_SPECIAL_COMPSET_BTRUE |
![]() |
where the type of ![]() ![]() ![]() |
A |
* | SIMP_SUBSETEQ_COMPSET_L |
![]() |
where ![]() |
A |
* | SIMP_IN_COMPSET |
![]() |
where ![]() ![]() ![]() ![]() |
A |
* | SIMP_IN_COMPSET_ONEPOINT |
![]() |
Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate | A |
SIMP_SUBSETEQ_COMPSET_R |
![]() |
where ![]() ![]() |
M | |
* | SIMP_SPECIAL_OVERL |
![]() |
A | |
* | SIMP_SPECIAL_KBOOL_BTRUE |
![]() |
A | |
* | SIMP_SPECIAL_KBOOL_BFALSE |
![]() |
A | |
DISTRI_SUBSETEQ_BUNION_SING |
![]() |
where ![]() |
M | |
* | DEF_FINITE |
![]() |
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_ID |
![]() |
where ![]() ![]() |
A |
* | SIMP_FINITE_ID_DOMRES |
![]() |
A | |
* | SIMP_FINITE_PRJ1 |
![]() |
where ![]() ![]() |
A |
* | SIMP_FINITE_PRJ2 |
![]() |
where ![]() ![]() |
A |
* | SIMP_FINITE_PRJ1_DOMRES |
![]() |
A | |
* | SIMP_FINITE_PRJ2_DOMRES |
![]() |
A | |
* | SIMP_FINITE_NATURAL |
![]() |
A | |
* | SIMP_FINITE_NATURAL1 |
![]() |
A | |
* | SIMP_FINITE_INTEGER |
![]() |
A | |
* | SIMP_FINITE_BOOL |
![]() |
A | |
* | SIMP_FINITE_LAMBDA |
![]() |
where ![]() ![]() ![]() ![]() |
A |
* | SIMP_TYPE_IN |
![]() |
where ![]() |
A |
* | SIMP_SPECIAL_EQV_BTRUE |
![]() |
A | |
* | SIMP_SPECIAL_EQV_BFALSE |
![]() |
A | |
* | DEF_SUBSET |
![]() |
A | |
* | SIMP_SPECIAL_SUBSET_R |
![]() |
A | |
* | SIMP_SPECIAL_SUBSET_L |
![]() |
A | |
* | SIMP_TYPE_SUBSET_L |
![]() |
where ![]() |
A |
* | SIMP_MULTI_SUBSET |
![]() |
A | |
* | SIMP_EQUAL_CONSTR |
![]() |
where ![]() |
A |
* | SIMP_EQUAL_CONSTR_DIFF |
![]() |
where ![]() ![]() |
A |
* | SIMP_DESTR_CONSTR |
![]() |
where ![]() ![]() |
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_EXISTS |
![]() |
M | |
* | DEF_IN_MAPSTO |
![]() |
AM | |
* | DEF_IN_POW |
![]() |
M | |
* | DEF_IN_POW1 |
![]() |
M | |
* | DEF_SUBSETEQ |
![]() |
where ![]() ![]() ![]() |
M |
* | DEF_IN_BUNION |
![]() |
M | |
* | DEF_IN_BINTER |
![]() |
M | |
* | DEF_IN_SETMINUS |
![]() |
M | |
* | DEF_IN_SETENUM |
![]() |
M | |
* | DEF_IN_KUNION |
![]() |
where ![]() |
M |
* | DEF_IN_QUNION |
![]() |
where ![]() |
M |
* | DEF_IN_KINTER |
![]() |
where ![]() |
M |
* | DEF_IN_QINTER |
![]() |
where ![]() |
M |
* | DEF_IN_UPTO |
![]() |
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 | |
* | DEF_PARTITION |
![]() |
AM | |
* | SIMP_EMPTY_PARTITION |
![]() |
A | |
* | SIMP_SINGLE_PARTITION |
![]() |
A | |
* | DEF_EQUAL_CARD |
![]() |
also works for ![]() |
M |
* | SIMP_EQUAL_CARD |
![]() |
M |
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.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | SIMP_DOM_SETENUM |
![]() |
A | |
* | SIMP_DOM_CONVERSE |
![]() |
A | |
* | SIMP_RAN_SETENUM |
![]() |
A | |
* | SIMP_RAN_CONVERSE |
![]() |
A | |
* | SIMP_SPECIAL_OVERL |
![]() |
A | |
* | SIMP_MULTI_OVERL |
![]() |
there is a ![]() ![]() ![]() ![]() |
A |
* | SIMP_TYPE_OVERL_CPROD |
![]() |
where ![]() |
A |
* | SIMP_SPECIAL_DOMRES_L |
![]() |
A | |
* | SIMP_SPECIAL_DOMRES_R |
![]() |
A | |
* | SIMP_TYPE_DOMRES |
![]() |
where ![]() |
A |
* | SIMP_MULTI_DOMRES_DOM |
![]() |
A | |
* | SIMP_MULTI_DOMRES_RAN |
![]() |
A | |
* | SIMP_DOMRES_DOMRES_ID |
![]() |
A | |
* | SIMP_DOMRES_DOMSUB_ID |
![]() |
A | |
* | SIMP_SPECIAL_RANRES_R |
![]() |
A | |
* | SIMP_SPECIAL_RANRES_L |
![]() |
A | |
* | SIMP_TYPE_RANRES |
![]() |
where ![]() |
A |
* | SIMP_MULTI_RANRES_RAN |
![]() |
A | |
* | SIMP_MULTI_RANRES_DOM |
![]() |
A | |
* | SIMP_RANRES_ID |
![]() |
A | |
* | SIMP_RANSUB_ID |
![]() |
A | |
* | SIMP_RANRES_DOMRES_ID |
![]() |
A | |
* | SIMP_RANRES_DOMSUB_ID |
![]() |
A | |
* | SIMP_SPECIAL_DOMSUB_L |
![]() |
A | |
* | SIMP_SPECIAL_DOMSUB_R |
![]() |
A | |
* | SIMP_TYPE_DOMSUB |
![]() |
where ![]() |
A |
* | SIMP_MULTI_DOMSUB_DOM |
![]() |
A | |
* | SIMP_MULTI_DOMSUB_RAN |
![]() |
A | |
* | SIMP_DOMSUB_DOMRES_ID |
![]() |
A | |
* | SIMP_DOMSUB_DOMSUB_ID |
![]() |
A | |
* | SIMP_SPECIAL_RANSUB_R |
![]() |
A | |
* | SIMP_SPECIAL_RANSUB_L |
![]() |
A | |
* | SIMP_TYPE_RANSUB |
![]() |
where ![]() |
A |
* | SIMP_MULTI_RANSUB_DOM |
![]() |
A | |
* | SIMP_MULTI_RANSUB_RAN |
![]() |
A | |
* | SIMP_RANSUB_DOMRES_ID |
![]() |
A | |
* | SIMP_RANSUB_DOMSUB_ID |
![]() |
A | |
* | SIMP_SPECIAL_FCOMP |
![]() |
A | |
* | SIMP_TYPE_FCOMP_ID |
![]() |
A | |
* | SIMP_TYPE_FCOMP_R |
![]() |
where ![]() ![]() |
A |
* | SIMP_TYPE_FCOMP_L |
![]() |
where ![]() ![]() |
A |
* | SIMP_FCOMP_ID |
![]() |
A | |
* | SIMP_SPECIAL_BCOMP |
![]() |
A | |
* | SIMP_TYPE_BCOMP_ID |
![]() |
A | |
* | SIMP_TYPE_BCOMP_L |
![]() |
where ![]() ![]() |
A |
* | SIMP_TYPE_BCOMP_R |
![]() |
where ![]() ![]() |
A |
* | SIMP_BCOMP_ID |
![]() |
A | |
* | SIMP_SPECIAL_DPROD_R |
![]() |
A | |
* | SIMP_SPECIAL_DPROD_L |
![]() |
A | |
* | SIMP_DPROD_CPROD |
![]() |
A | |
* | SIMP_SPECIAL_PPROD_R |
![]() |
A | |
* | SIMP_SPECIAL_PPROD_L |
![]() |
A | |
* | SIMP_PPROD_CPROD |
![]() |
A | |
* | SIMP_SPECIAL_RELIMAGE_R |
![]() |
A | |
* | SIMP_SPECIAL_RELIMAGE_L |
![]() |
A | |
* | SIMP_TYPE_RELIMAGE |
![]() |
where ![]() |
A |
* | SIMP_MULTI_RELIMAGE_DOM |
![]() |
A | |
* | SIMP_RELIMAGE_ID |
![]() |
A | |
* | SIMP_RELIMAGE_DOMRES_ID |
![]() |
A | |
* | SIMP_RELIMAGE_DOMSUB_ID |
![]() |
A | |
* | SIMP_MULTI_RELIMAGE_CPROD_SING |
![]() |
where ![]() |
A |
* | SIMP_MULTI_RELIMAGE_SING_MAPSTO |
![]() |
where ![]() |
A |
* | SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB |
![]() |
A | |
* | SIMP_MULTI_RELIMAGE_CONVERSE_RANRES |
![]() |
A | |
* | SIMP_RELIMAGE_CONVERSE_DOMSUB |
![]() |
A | |
DERIV_RELIMAGE_RANSUB |
![]() |
M | ||
DERIV_RELIMAGE_RANRES |
![]() |
M | ||
* | SIMP_MULTI_RELIMAGE_DOMSUB |
![]() |
A | |
DERIV_RELIMAGE_DOMSUB |
![]() |
M | ||
DERIV_RELIMAGE_DOMRES |
![]() |
M | ||
* | SIMP_SPECIAL_CONVERSE |
![]() |
A | |
* | SIMP_CONVERSE_ID |
![]() |
A | |
* | SIMP_CONVERSE_CPROD |
![]() |
A | |
* | SIMP_CONVERSE_SETENUM |
![]() |
A | |
* | SIMP_CONVERSE_COMPSET |
![]() |
A | |
* | SIMP_DOM_ID |
![]() |
where ![]() ![]() |
A |
* | SIMP_RAN_ID |
![]() |
where ![]() ![]() |
A |
* | SIMP_FCOMP_ID_L |
![]() |
A | |
* | SIMP_FCOMP_ID_R |
![]() |
A | |
* | SIMP_SPECIAL_REL_R |
![]() |
idem for operators ![]() |
A |
* | SIMP_SPECIAL_REL_L |
![]() |
idem for operators ![]() |
A |
* | SIMP_FUNIMAGE_PRJ1 |
![]() |
A | |
* | SIMP_FUNIMAGE_PRJ2 |
![]() |
A | |
* | SIMP_DOM_PRJ1 |
![]() |
where ![]() ![]() |
A |
* | SIMP_DOM_PRJ2 |
![]() |
where ![]() ![]() |
A |
* | SIMP_RAN_PRJ1 |
![]() |
where ![]() ![]() |
A |
* | SIMP_RAN_PRJ2 |
![]() |
where ![]() ![]() |
A |
* | SIMP_FUNIMAGE_LAMBDA |
![]() |
A | |
* | SIMP_DOM_LAMBDA |
![]() |
A | |
* | SIMP_RAN_LAMBDA |
![]() |
A | |
* | SIMP_IN_FUNIMAGE |
![]() |
A | |
* | SIMP_IN_FUNIMAGE_CONVERSE_L |
![]() |
A | |
* | SIMP_IN_FUNIMAGE_CONVERSE_R |
![]() |
A | |
* | SIMP_MULTI_FUNIMAGE_SETENUM_LL |
![]() |
A | |
* | SIMP_MULTI_FUNIMAGE_SETENUM_LR |
![]() |
A | |
* | SIMP_MULTI_FUNIMAGE_OVERL_SETENUM |
![]() |
A | |
* | SIMP_MULTI_FUNIMAGE_BUNION_SETENUM |
![]() |
A | |
* | SIMP_FUNIMAGE_CPROD |
![]() |
A | |
* | SIMP_FUNIMAGE_ID |
![]() |
A | |
* | SIMP_FUNIMAGE_FUNIMAGE_CONVERSE |
![]() |
A | |
* | SIMP_FUNIMAGE_CONVERSE_FUNIMAGE |
![]() |
A | |
* | SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM |
![]() |
A | |
* | SIMP_FUNIMAGE_DOMRES |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | SIMP_FUNIMAGE_DOMSUB |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | SIMP_FUNIMAGE_RANRES |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | SIMP_FUNIMAGE_RANSUB |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | SIMP_FUNIMAGE_SETMINUS |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | DEF_EQUAL_FUNIMAGE |
![]() |
M | |
* | DEF_BCOMP |
![]() |
M | |
DERIV_ID_SING |
![]() |
where ![]() |
M | |
* | SIMP_SPECIAL_DOM |
![]() |
A | |
* | SIMP_SPECIAL_RAN |
![]() |
A | |
* | SIMP_CONVERSE_CONVERSE |
![]() |
A | |
* | DERIV_RELIMAGE_FCOMP |
![]() |
M | |
* | DERIV_FCOMP_DOMRES |
![]() |
M | |
* | DERIV_FCOMP_DOMSUB |
![]() |
M | |
* | DERIV_FCOMP_RANRES |
![]() |
M | |
* | DERIV_FCOMP_RANSUB |
![]() |
M | |
DERIV_FCOMP_SING |
![]() |
A | ||
* | SIMP_SPECIAL_EQUAL_RELDOMRAN |
![]() |
idem for operators ![]() |
A |
* | SIMP_TYPE_DOM |
![]() |
where ![]() ![]() |
A |
* | SIMP_TYPE_RAN |
![]() |
where ![]() ![]() |
A |
* | SIMP_MULTI_DOM_CPROD |
![]() |
A | |
* | SIMP_MULTI_RAN_CPROD |
![]() |
A | |
* | SIMP_MULTI_DOM_DOMRES |
![]() |
A | |
* | SIMP_MULTI_DOM_DOMSUB |
![]() |
A | |
* | SIMP_MULTI_RAN_RANRES |
![]() |
A | |
* | SIMP_MULTI_RAN_RANSUB |
![]() |
A | |
* | DEF_IN_DOM |
![]() |
M | |
* | DEF_IN_RAN |
![]() |
M | |
* | DEF_IN_CONVERSE |
![]() |
M | |
* | DEF_IN_DOMRES |
![]() |
M | |
* | DEF_IN_RANRES |
![]() |
M | |
* | DEF_IN_DOMSUB |
![]() |
M | |
* | DEF_IN_RANSUB |
![]() |
M | |
* | DEF_IN_RELIMAGE |
![]() |
M | |
* | DEF_IN_FCOMP |
![]() |
M | |
* | DEF_OVERL |
![]() |
M | |
* | DEF_IN_ID |
![]() |
M | |
* | DEF_IN_DPROD |
![]() |
M | |
* | DEF_IN_PPROD |
![]() |
M | |
* | DEF_IN_REL |
![]() |
M | |
* | DEF_IN_RELDOM |
![]() |
M | |
* | DEF_IN_RELRAN |
![]() |
M | |
* | DEF_IN_RELDOMRAN |
![]() |
M | |
* | DEF_IN_FCT |
![]() |
M | |
* | DEF_IN_TFCT |
![]() |
M | |
* | DEF_IN_INJ |
![]() |
M | |
* | DEF_IN_TINJ |
![]() |
M | |
* | DEF_IN_SURJ |
![]() |
M | |
* | DEF_IN_TSURJ |
![]() |
M | |
* | DEF_IN_BIJ |
![]() |
M | |
DISTRI_BCOMP_BUNION |
![]() |
M | ||
* | DISTRI_FCOMP_BUNION_R |
![]() |
M | |
* | DISTRI_FCOMP_BUNION_L |
![]() |
M | |
DISTRI_DPROD_BUNION |
![]() |
M | ||
DISTRI_DPROD_BINTER |
![]() |
M | ||
DISTRI_DPROD_SETMINUS |
![]() |
M | ||
DISTRI_DPROD_OVERL |
![]() |
M | ||
DISTRI_PPROD_BUNION |
![]() |
M | ||
DISTRI_PPROD_BINTER |
![]() |
M | ||
DISTRI_PPROD_SETMINUS |
![]() |
M | ||
DISTRI_PPROD_OVERL |
![]() |
M | ||
DISTRI_OVERL_BUNION_L |
![]() |
M | ||
DISTRI_OVERL_BINTER_L |
![]() |
M | ||
* | DISTRI_DOMRES_BUNION_R |
![]() |
M | |
* | DISTRI_DOMRES_BUNION_L |
![]() |
M | |
* | DISTRI_DOMRES_BINTER_R |
![]() |
M | |
* | DISTRI_DOMRES_BINTER_L |
![]() |
M | |
DISTRI_DOMRES_SETMINUS_R |
![]() |
M | ||
DISTRI_DOMRES_SETMINUS_L |
![]() |
M | ||
DISTRI_DOMRES_DPROD |
![]() |
M | ||
DISTRI_DOMRES_OVERL |
![]() |
M | ||
* | DISTRI_DOMSUB_BUNION_R |
![]() |
M | |
* | DISTRI_DOMSUB_BUNION_L |
![]() |
M | |
* | DISTRI_DOMSUB_BINTER_R |
![]() |
M | |
* | DISTRI_DOMSUB_BINTER_L |
![]() |
M | |
DISTRI_DOMSUB_DPROD |
![]() |
M | ||
DISTRI_DOMSUB_OVERL |
![]() |
M | ||
* | DISTRI_RANRES_BUNION_R |
![]() |
M | |
* | DISTRI_RANRES_BUNION_L |
![]() |
M | |
* | DISTRI_RANRES_BINTER_R |
![]() |
M | |
* | DISTRI_RANRES_BINTER_L |
![]() |
M | |
DISTRI_RANRES_SETMINUS_R |
![]() |
M | ||
DISTRI_RANRES_SETMINUS_L |
![]() |
M | ||
* | DISTRI_RANSUB_BUNION_R |
![]() |
M | |
* | DISTRI_RANSUB_BUNION_L |
![]() |
M | |
* | DISTRI_RANSUB_BINTER_R |
![]() |
M | |
* | DISTRI_RANSUB_BINTER_L |
![]() |
M | |
* | DISTRI_CONVERSE_BUNION |
![]() |
M | |
DISTRI_CONVERSE_BINTER |
![]() |
M | ||
DISTRI_CONVERSE_SETMINUS |
![]() |
M | ||
DISTRI_CONVERSE_BCOMP |
![]() |
M | ||
DISTRI_CONVERSE_FCOMP |
![]() |
M | ||
DISTRI_CONVERSE_PPROD |
![]() |
M | ||
DISTRI_CONVERSE_DOMRES |
![]() |
M | ||
DISTRI_CONVERSE_DOMSUB |
![]() |
M | ||
DISTRI_CONVERSE_RANRES |
![]() |
M | ||
DISTRI_CONVERSE_RANSUB |
![]() |
M | ||
* | DISTRI_DOM_BUNION |
![]() |
M | |
* | DISTRI_RAN_BUNION |
![]() |
M | |
* | DISTRI_RELIMAGE_BUNION_R |
![]() |
M | |
* | DISTRI_RELIMAGE_BUNION_L |
![]() |
M | |
* | DERIV_DOM_TOTALREL |
![]() |
with hypothesis ![]() ![]() ![]() |
M |
DERIV_RAN_SURJREL |
![]() |
with hypothesis ![]() ![]() ![]() |
M | |
* | DERIV_PRJ1_SURJ |
![]() |
where ![]() ![]() ![]() ![]() |
A |
* | DERIV_PRJ2_SURJ |
![]() |
where ![]() ![]() ![]() ![]() |
A |
* | DERIV_ID_BIJ |
![]() |
where ![]() ![]() |
A |
* | SIMP_MAPSTO_PRJ1_PRJ2 |
![]() |
A | |
DERIV_EXPAND_PRJS |
![]() |
M | ||
* | SIMP_DOM_SUCC |
![]() |
A | |
* | SIMP_RAN_SUCC |
![]() |
A | |
* | DERIV_MULTI_IN_BUNION |
![]() |
A | |
* | DERIV_MULTI_IN_SETMINUS |
![]() |
A | |
* | DEF_PRED |
![]() |
A | |
* | SIMP_SPECIAL_IN_ID |
![]() |
A | |
* | SIMP_SPECIAL_IN_SETMINUS_ID |
![]() |
A | |
* | SIMP_SPECIAL_IN_DOMRES_ID |
![]() |
A | |
* | SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID |
![]() |
A |
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.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | SIMP_SPECIAL_MOD_0 |
![]() |
A | |
* | SIMP_SPECIAL_MOD_1 |
![]() |
A | |
* | SIMP_MIN_SING |
![]() |
where ![]() |
A |
* | SIMP_MAX_SING |
![]() |
where ![]() |
A |
* | SIMP_MIN_NATURAL |
![]() |
A | |
* | SIMP_MIN_NATURAL1 |
![]() |
A | |
* | SIMP_MIN_BUNION_SING |
![]() |
A | |
* | SIMP_MAX_BUNION_SING |
![]() |
A | |
* | SIMP_MIN_UPTO |
![]() |
A | |
* | SIMP_MAX_UPTO |
![]() |
A | |
* | SIMP_MIN_IN |
![]() |
A | |
* | SIMP_MAX_IN |
![]() |
A | |
* | SIMP_LIT_MIN |
![]() |
where ![]() ![]() ![]() |
A |
* | SIMP_LIT_MAX |
![]() |
where ![]() ![]() ![]() |
A |
* | SIMP_SPECIAL_CARD |
![]() |
A | |
* | SIMP_CARD_SING |
![]() |
where ![]() |
A |
* | SIMP_SPECIAL_EQUAL_CARD |
![]() |
A | |
* | SIMP_CARD_POW |
![]() |
A | |
* | SIMP_CARD_BUNION |
![]() |
A | |
SIMP_CARD_SETMINUS |
![]() |
with hypotheses ![]() ![]() ![]() |
A | |
SIMP_CARD_SETMINUS_SETENUM |
![]() |
with hypotheses ![]() ![]() |
A | |
* | SIMP_CARD_CONVERSE |
![]() |
A | |
* | SIMP_CARD_ID |
![]() |
where ![]() ![]() |
A |
* | SIMP_CARD_ID_DOMRES |
![]() |
A | |
* | SIMP_CARD_PRJ1 |
![]() |
where ![]() ![]() |
A |
* | SIMP_CARD_PRJ2 |
![]() |
where ![]() ![]() |
A |
* | SIMP_CARD_PRJ1_DOMRES |
![]() |
A | |
* | SIMP_CARD_PRJ2_DOMRES |
![]() |
A | |
* | SIMP_CARD_LAMBDA |
![]() |
where ![]() ![]() ![]() ![]() |
A |
* | SIMP_LIT_CARD_UPTO |
![]() |
where ![]() ![]() ![]() |
A |
SIMP_TYPE_CARD |
![]() |
where ![]() ![]() |
A | |
* | SIMP_LIT_GE_CARD_1 |
![]() |
A | |
* | SIMP_LIT_LE_CARD_1 |
![]() |
A | |
* | SIMP_LIT_LE_CARD_0 |
![]() |
A | |
* | SIMP_LIT_GE_CARD_0 |
![]() |
A | |
* | SIMP_LIT_GT_CARD_0 |
![]() |
A | |
* | SIMP_LIT_LT_CARD_0 |
![]() |
A | |
* | SIMP_LIT_EQUAL_CARD_1 |
![]() |
A | |
* | SIMP_CARD_NATURAL |
![]() |
A | |
* | SIMP_CARD_NATURAL1 |
![]() |
A | |
* | SIMP_LIT_IN_NATURAL |
![]() |
where ![]() |
A |
* | SIMP_SPECIAL_IN_NATURAL1 |
![]() |
A | |
* | SIMP_LIT_IN_NATURAL1 |
![]() |
where ![]() |
A |
* | SIMP_LIT_UPTO |
![]() |
where ![]() ![]() ![]() |
A |
* | SIMP_LIT_IN_MINUS_NATURAL |
![]() |
where ![]() |
A |
* | SIMP_LIT_IN_MINUS_NATURAL1 |
![]() |
where ![]() |
A |
* | DEF_IN_NATURAL |
![]() |
M | |
* | DEF_IN_NATURAL1 |
![]() |
M | |
* | SIMP_LIT_EQUAL_KBOOL_TRUE |
![]() |
A | |
* | SIMP_LIT_EQUAL_KBOOL_FALSE |
![]() |
A | |
* | SIMP_KBOOL_LIT_EQUAL_TRUE |
![]() |
A | |
* | DEF_EQUAL_MIN |
![]() |
where ![]() ![]() |
M |
* | DEF_EQUAL_MAX |
![]() |
where ![]() ![]() |
M |
* | SIMP_SPECIAL_PLUS |
![]() |
A | |
* | SIMP_SPECIAL_MINUS_R |
![]() |
A | |
* | SIMP_SPECIAL_MINUS_L |
![]() |
A | |
* | SIMP_MINUS_MINUS |
![]() |
A | |
* | SIMP_MINUS_UNMINUS |
![]() |
where ![]() |
M |
* | SIMP_MULTI_MINUS |
![]() |
A | |
* | SIMP_MULTI_MINUS_PLUS_L |
![]() |
M | |
* | SIMP_MULTI_MINUS_PLUS_R |
![]() |
M | |
* | SIMP_MULTI_MINUS_PLUS_PLUS |
![]() |
M | |
* | SIMP_MULTI_PLUS_MINUS |
![]() |
M | |
* | SIMP_MULTI_ARITHREL_PLUS_PLUS |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_PLUS_R |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_PLUS_L |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_MINUS_MINUS_R |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_MINUS_MINUS_L |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_SPECIAL_PROD_0 |
![]() |
A | |
* | SIMP_SPECIAL_PROD_1 |
![]() |
A | |
* | SIMP_SPECIAL_PROD_MINUS_EVEN |
![]() |
if an even number of ![]() |
A |
* | SIMP_SPECIAL_PROD_MINUS_ODD |
![]() |
if an odd number of ![]() |
A |
* | SIMP_LIT_MINUS |
![]() |
where ![]() |
A |
* | SIMP_LIT_EQUAL |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_LE |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_LT |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_GE |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_GT |
![]() |
where ![]() ![]() |
A |
* | SIMP_DIV_MINUS |
![]() |
A | |
* | SIMP_SPECIAL_DIV_1 |
![]() |
A | |
* | SIMP_SPECIAL_DIV_0 |
![]() |
A | |
* | SIMP_SPECIAL_EXPN_1_R |
![]() |
A | |
* | SIMP_SPECIAL_EXPN_1_L |
![]() |
A | |
* | SIMP_SPECIAL_EXPN_0 |
![]() |
A | |
* | DEF_EXPN_STEP |
![]() |
with an additional PO ![]() |
M |
* | SIMP_MULTI_LE |
![]() |
A | |
* | SIMP_MULTI_LT |
![]() |
A | |
* | SIMP_MULTI_GE |
![]() |
A | |
* | SIMP_MULTI_GT |
![]() |
A | |
* | SIMP_MULTI_DIV |
![]() |
A | |
* | SIMP_MULTI_DIV_PROD |
![]() |
A | |
* | SIMP_MULTI_MOD |
![]() |
A | |
DISTRI_PROD_PLUS |
![]() |
M | ||
DISTRI_PROD_MINUS |
![]() |
M | ||
DERIV_NOT_EQUAL |
![]() |
![]() ![]() |
M |