# 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):

Conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_rules

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 do not occur in | A | |

* | SIMP_EXISTS |
Quantified identifiers other than do not occur in | 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 is a type expression | A | |

* | SIMP_SUBSETEQ_SING |
where is a single expression | 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 is a type expression | A | |

* | SIMP_MULTI_BINTER |
A | ||

* | SIMP_MULTI_EQUAL_BINTER |
A | ||

* | SIMP_SPECIAL_BUNION |
A | ||

* | SIMP_TYPE_BUNION |
where is a type expression | 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 is a type expression | A | |

* | SIMP_TYPE_SETMINUS_SETMINUS |
where is a type expression | 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 non free in and non free in | A | ||

* | SIMP_COMPSET_IN |
where non free in | A | |

* | SIMP_COMPSET_SUBSETEQ |
where non free in | A | |

* | SIMP_SPECIAL_COMPSET_BFALSE |
A | ||

* | SIMP_SPECIAL_COMPSET_BTRUE |
where the type of is and is a maplet combination of locally-bound, pairwise-distinct bound identifiers | A | |

* | SIMP_SUBSETEQ_COMPSET_L |
where is fresh | A | |

* | SIMP_IN_COMPSET |
where , , are not free in | 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 non free in | M | ||

* | SIMP_SPECIAL_OVERL |
A | ||

* | SIMP_SPECIAL_KBOOL_BTRUE |
A | ||

* | SIMP_SPECIAL_KBOOL_BFALSE |
A | ||

DISTRI_SUBSETEQ_BUNION_SING |
where is a single expression | M | ||

* | DEF_FINITE |
M | ||

* | SIMP_SPECIAL_FINITE |
A | ||

* | SIMP_FINITE_SETENUM |
A | ||

* | SIMP_FINITE_BUNION |
A | ||

SIMP_FINITE_UNION |
M | |||

SIMP_FINITE_QUNION |
M | |||

* | SIMP_FINITE_POW |
A | ||

* | DERIV_FINITE_CPROD |
A | ||

* | SIMP_FINITE_CONVERSE |
A | ||

* | SIMP_FINITE_UPTO |
A | ||

* | SIMP_FINITE_ID |
where has type | A | |

* | SIMP_FINITE_ID_DOMRES |
A | ||

* | SIMP_FINITE_PRJ1 |
where has type | A | |

* | SIMP_FINITE_PRJ2 |
where has type | 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 is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., is syntactically injective) and all identifiers bound by the comprehension set that occur in also occur in | A | |

* | SIMP_TYPE_IN |
where is a type expression | 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 is a type expression | A | |

* | SIMP_MULTI_SUBSET |
A | ||

* | SIMP_EQUAL_CONSTR |
where is a datatype constructor | A | |

* | SIMP_EQUAL_CONSTR_DIFF |
where and are different datatype constructors | A | |

* | SIMP_DESTR_CONSTR |
where is the datatype destructor for the i-th argument of datatype constructor | 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 is not free in or | M | |

* | DEF_IN_BUNION |
M | ||

* | DEF_IN_BINTER |
M | ||

* | DEF_IN_SETMINUS |
M | ||

* | DEF_IN_SETENUM |
M | ||

* | DEF_IN_KUNION |
where is fresh | M | |

* | DEF_IN_QUNION |
where is fresh | M | |

* | DEF_IN_KINTER |
where is fresh | M | |

* | DEF_IN_QINTER |
where is fresh | 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 is a type expression | M | |

* | DERIV_TYPE_SETMINUS_BUNION |
where is a type expression | M | |

* | DERIV_TYPE_SETMINUS_SETMINUS |
where is a type expression | M | |

DISTRI_CPROD_BINTER |
M | |||

DISTRI_CPROD_BUNION |
M | |||

DISTRI_CPROD_SETMINUS |
M | |||

* | DERIV_SUBSETEQ |
where is the type of and | M | |

* | DERIV_EQUAL |
where is the type of and | M | |

* | DERIV_SUBSETEQ_SETMINUS_L |
M | ||

* | DERIV_SUBSETEQ_SETMINUS_R |
M | ||

* | DEF_PARTITION |
AM | ||

SIMP_EMPTY_PARTITION |
A | |||

SIMP_SINGLE_PARTITION |
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_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 such that and and are syntactically equal. | A | |

* | SIMP_TYPE_OVERL_CPROD |
where is a type expression | A | |

* | SIMP_SPECIAL_DOMRES_L |
A | ||

* | SIMP_SPECIAL_DOMRES_R |
A | ||

* | SIMP_TYPE_DOMRES |
where is a type expression | 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 is a type expression | 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 is a type expression | 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 is a type expression | 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 is a type expression equal to | A | |

* | SIMP_TYPE_FCOMP_L |
where is a type expression equal to | A | |

* | SIMP_FCOMP_ID |
A | ||

* | SIMP_SPECIAL_BCOMP |
A | ||

* | SIMP_TYPE_BCOMP_ID |
A | ||

* | SIMP_TYPE_BCOMP_L |
where is a type expression equal to | A | |

* | SIMP_TYPE_BCOMP_R |
where is a type expression equal to | 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 is a type expression | 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 is a single expression | A | |

* | SIMP_MULTI_RELIMAGE_SING_MAPSTO |
where is a single expression | 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 has type | A | |

* | SIMP_RAN_ID |
where has type | 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 has type | A | |

* | SIMP_DOM_PRJ2 |
where has type | A | |

* | SIMP_RAN_PRJ1 |
where has type | A | |

* | SIMP_RAN_PRJ2 |
where has type | 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 where is one of , , , , , , . | AM | |

* | SIMP_FUNIMAGE_DOMSUB |
with hypothesis where is one of , , , , , , . | AM | |

* | SIMP_FUNIMAGE_RANRES |
with hypothesis where is one of , , , , , , . | AM | |

* | SIMP_FUNIMAGE_RANSUB |
with hypothesis where is one of , , , , , , . | AM | |

* | SIMP_FUNIMAGE_SETMINUS |
with hypothesis where is one of , , , , , , . | AM | |

DEF_BCOMP |
M | |||

DERIV_ID_SING |
where is a single expression | 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 is a type expression equal to | A | |

* | SIMP_TYPE_RAN |
where is a type expression equal to | 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 , where is one of | M | |

DERIV_RAN_SURJREL |
with hypothesis , where is one of | M | ||

* | DERIV_PRJ1_SURJ |
where and are types and is one of | A | |

* | DERIV_PRJ2_SURJ |
where and are types and is one of | A | |

* | DERIV_ID_BIJ |
where is a type and is any arrow | 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 |

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 is a single expression | A | |

* | SIMP_MAX_SING |
where is a single expression | 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_LIT_MIN |
where and are literals and | A | |

* | SIMP_LIT_MAX |
where and are literals and | A | |

* | SIMP_SPECIAL_CARD |
A | ||

* | SIMP_CARD_SING |
where is a single expression | A | |

* | SIMP_SPECIAL_EQUAL_CARD |
A | ||

* | SIMP_CARD_POW |
A | ||

* | SIMP_CARD_BUNION |
A | ||

SIMP_CARD_SETMINUS |
with hypotheses and either or | A | ||

SIMP_CARD_SETMINUS_SETENUM |
with hypotheses for all | A | ||

* | SIMP_CARD_CONVERSE |
A | ||

* | SIMP_CARD_ID |
where has type | A | |

* | SIMP_CARD_ID_DOMRES |
A | ||

* | SIMP_CARD_PRJ1 |
where has type | A | |

* | SIMP_CARD_PRJ2 |
where has type | A | |

* | SIMP_CARD_PRJ1_DOMRES |
A | ||

* | SIMP_CARD_PRJ2_DOMRES |
A | ||

* | SIMP_CARD_LAMBDA |
where is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., is syntactically injective) and all identifiers bound by the comprehension set that occur in also occur in | A | |

* | SIMP_LIT_CARD_UPTO |
where and are literals and | A | |

SIMP_TYPE_CARD |
where is a carrier set containing elements | 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 is a non-negative literal | A | |

* | SIMP_SPECIAL_IN_NATURAL1 |
A | ||

* | SIMP_LIT_IN_NATURAL1 |
where is a positive literal | A | |

* | SIMP_LIT_UPTO |
where and are literals and | A | |

* | SIMP_LIT_IN_MINUS_NATURAL |
where is a positive literal | A | |

* | SIMP_LIT_IN_MINUS_NATURAL1 |
where is a non-negative literal | A | |

* | DEF_IN_NATURAL |
M | ||

* | DEF_IN_NATURAL1 |
M | ||

* | SIMP_LIT_EQUAL_KBOOL_TRUE |
A | ||

* | SIMP_LIT_EQUAL_KBOOL_FALSE |
A | ||

DEF_EQUAL_MIN |
where non free in | M | ||

DEF_EQUAL_MAX |
where non free in | M | ||

* | SIMP_SPECIAL_PLUS |
A | ||

* | SIMP_SPECIAL_MINUS_R |
A | ||

* | SIMP_SPECIAL_MINUS_L |
A | ||

* | SIMP_MINUS_MINUS |
A | ||

* | SIMP_MINUS_UNMINUS |
where is a unary minus expression or a negative literal | 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 ( here) is one of | M | |

* | SIMP_MULTI_ARITHREL_PLUS_R |
where the root relation ( here) is one of | M | |

* | SIMP_MULTI_ARITHREL_PLUS_L |
where the root relation ( here) is one of | M | |

* | SIMP_MULTI_ARITHREL_MINUS_MINUS_R |
where the root relation ( here) is one of | M | |

* | SIMP_MULTI_ARITHREL_MINUS_MINUS_L |
where the root relation ( here) is one of | 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 is a literal | A | |

* | SIMP_LIT_EQUAL |
where and are literals | A | |

* | SIMP_LIT_LE |
where and are literals | A | |

* | SIMP_LIT_LT |
where and are literals | A | |

* | SIMP_LIT_GE |
where and are literals | A | |

* | SIMP_LIT_GT |
where and are literals | 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 | ||

* | 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 |
and must be of Integer type | M |