Set Rewrite Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Laurent
Added side condition to SIMP_IN_COMPSET
Guillaume (talk | contribs)
Rules SIMP_{EMPTY,SINGLE}_PARTITION were implemented
 
(66 intermediate revisions by 8 users not shown)
Line 1: Line 1:
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
Rules without a <tt>*</tt> are planned to be implemented in future versions.
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
{{RRHeader}}
{{RRHeader}}
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BTRUE}}||<math>  P \land  \ldots  \land  \btrue  \land  \ldots  \land  Q \;\;\defi\;\;  P \land  \ldots  \land  Q </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BTRUE}}||<math>  P \land  \ldots  \land  \btrue  \land  \ldots  \land  Q \;\;\defi\;\;  P \land  \ldots  \land  Q </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BFALSE}}||<math>  P \land  \ldots  \land  \bfalse  \land  \ldots  \land  Q \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BFALSE}}||<math>  P \land  \ldots  \land  \bfalse  \land  \ldots  \land  Q \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_AND}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  Q \land  \ldots  \land  R \;\;\defi\;\;  P \land  \ldots  \land  Q \land  \ldots  \land  R </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_AND}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  Q \land  \ldots  \land  R \;\;\defi\;\;  P \land  \ldots  \land  Q \land  \ldots  \land  R </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_AND_NOT}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  \lnot\, Q \land  \ldots  \land  R \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_AND_NOT}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  \lnot\, Q \land  \ldots  \land  R \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BTRUE}}||<math>  P \lor  \ldots  \lor  \btrue  \lor  \ldots  \lor  Q \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BTRUE}}||<math>  P \lor  \ldots  \lor  \btrue  \lor  \ldots  \lor  Q \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BFALSE}}||<math>  P \lor  \ldots  \lor  \bfalse  \lor  \ldots  \lor  Q \;\;\defi\;\;  P \lor  \ldots  \lor  Q </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BFALSE}}||<math>  P \lor  \ldots  \lor  \bfalse  \lor  \ldots  \lor  Q \;\;\defi\;\;  P \lor  \ldots  \lor  Q </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_OR}}||<math>  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  Q \lor  \ldots  \lor  R \;\;\defi\;\;  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  R </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_OR}}||<math>  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  Q \lor  \ldots  \lor  R \;\;\defi\;\;  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  R </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_OR_NOT}}||<math>  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  \lnot\, Q \land  \ldots  \land  R \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_OR_NOT}}||<math>  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  \lnot\, Q \land  \ldots  \land  R \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_R}}||<math>  P \limp  \btrue  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_R}}||<math>  P \limp  \btrue  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_L}}||<math>  \btrue  \limp  P \;\;\defi\;\;  P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_L}}||<math>  \btrue  \limp  P \;\;\defi\;\;  P </math>||  ||  A
Line 13: Line 17:
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BFALSE_L}}||<math>  \bfalse  \limp  P \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BFALSE_L}}||<math>  \bfalse  \limp  P \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP}}||<math>  P \limp  P \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP}}||<math>  P \limp  P \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_IMP_OR}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  R \limp  Q \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_NOT_L}}||<math>\lnot P\limp P\;\;\defi\;\; P</math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_IMP_AND_NOT_R}}||<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}}|*||{{Rulename|SIMP_MULTI_IMP_NOT_R}}||<math>P\limp\lnot P\;\;\defi\;\;\lnot P</math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_IMP_AND_NOT_L}}||<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}}|*||{{Rulename|SIMP_MULTI_IMP_AND}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  R \limp  Q \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_AND_NOT_R}}||<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}}|*||{{Rulename|SIMP_MULTI_IMP_AND_NOT_L}}||<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}}|*||{{Rulename|SIMP_MULTI_EQV}}||<math>  P \leqv  P \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQV}}||<math>  P \leqv  P \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_EQV_NOT}}||<math>  P \leqv  \lnot\, P \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQV_NOT}}||<math>  P \leqv  \lnot\, P \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_EQV_NOT_NOT}}||<math>  \lnot\, P \leqv  \lnot\, P \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BTRUE}}||<math>  \lnot\, \btrue  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BTRUE}}||<math>  \lnot\, \btrue  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BFALSE}}||<math>  \lnot\, \bfalse  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BFALSE}}||<math>  \lnot\, \bfalse  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_NOT_NOT}}||<math>  \lnot\, \lnot\, P \;\;\defi\;\;  P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_NOT_NOT}}||<math>  \lnot\, \lnot\, P \;\;\defi\;\;  P </math>||  ||  AM
{{RRRow}}|*||{{Rulename|SIMP_NOTEQUAL}}||<math>  E \neq  F \;\;\defi\;\;  \lnot\, E = F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_NOTEQUAL}}||<math>  E \neq  F \;\;\defi\;\;  \lnot\, E = F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_NOTIN}}||<math>  E \notin  F \;\;\defi\;\;  \lnot\, E \in  F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_NOTIN}}||<math>  E \notin  F \;\;\defi\;\;  \lnot\, E \in  F </math>||  ||  A
Line 36: Line 41:
{{RRRow}}|*||{{Rulename|SIMP_FORALL_AND}}||<math>  \forall x \qdot  P \land  Q \;\;\defi\;\;  (\forall x \qdot  P) \land  (\forall x \qdot  Q) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FORALL_AND}}||<math>  \forall x \qdot  P \land  Q \;\;\defi\;\;  (\forall x \qdot  P) \land  (\forall x \qdot  Q) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_EXISTS_OR}}||<math>  \exists x \qdot  P \lor  Q \;\;\defi\;\;  (\exists x \qdot  P) \lor  (\exists x \qdot  Q) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_EXISTS_OR}}||<math>  \exists x \qdot  P \lor  Q \;\;\defi\;\;  (\exists x \qdot  P) \lor  (\exists x \qdot  Q) </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_FORALL}}||<math>  \forall \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \forall z \qdot  P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_EXISTS_IMP}}||<math>\exists x\qdot P\limp Q\;\;\defi\;\;(\forall x\qdot P)\limp(\exists x\qdot Q)</math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_EXISTS}}||<math>  \exists \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \exists z \qdot  P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_FORALL}}||<math>  \forall \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \forall z \qdot  P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_EXISTS}}||<math>  \exists \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \exists z \qdot  P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL}}||<math>  E = E \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL}}||<math>  E = E \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_NOTEQUAL}}||<math>  E \neq  E \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_NOTEQUAL}}||<math>  E \neq  E \;\;\defi\;\;  \bfalse </math>||  ||  A
Line 43: Line 49:
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_SING}}||<math>  \{ E\}  = \{ F\}  \;\;\defi\;\;  E = F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_SING}}||<math>  \{ E\}  = \{ F\}  \;\;\defi\;\;  E = F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_TRUE}}||<math>  \True  = \False  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_TRUE}}||<math>  \True  = \False  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_TYPE_SUBSETEQ}}||<math>  S \subseteq  \mathit{Ty} \;\;\defi\;\;  \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SUBSETEQ}}||<math>  S \subseteq  \mathit{Ty} \;\;\defi\;\;  \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_SING}}||<math>  \{ E\}  \subseteq  S \;\;\defi\;\;  E \in  S </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_SING}}||<math>  \{ E\}  \subseteq  S \;\;\defi\;\;  E \in  S </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSETEQ}}||<math>  \emptyset  \subseteq  S \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSETEQ}}||<math>  \emptyset  \subseteq  S \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SUBSETEQ}}||<math>  S \subseteq  S \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SUBSETEQ}}||<math>  S \subseteq  S \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BUNION}}||<math>  S \subseteq  A \bunion  \ldots  \bunion  S \bunion  \ldots  \bunion  B \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BUNION}}||<math>  S \subseteq  A \bunion  \ldots  \bunion  S \bunion  \ldots  \bunion  B \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BINTER}}||<math>  A \binter  \ldots  \binter  S \binter  \ldots  \binter  B \subseteq  S \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BINTER}}||<math>  A \binter  \ldots  \binter  S \binter  \ldots  \binter  B \subseteq  S \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BUNION}}||<math>  A \bunion  \ldots  \bunion  B \subseteq  S \;\;\defi\;\;  A \subseteq  S \land  \ldots  \land  B \subseteq  S </math>||  ||  M
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BUNION}}||<math>  A \bunion  \ldots  \bunion  B \subseteq  S \;\;\defi\;\;  A \subseteq  S \land  \ldots  \land  B \subseteq  S </math>||  ||  A
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BINTER}}||<math>  S \subseteq  A \binter  \ldots  \binter  B \;\;\defi\;\;  S \subseteq  A \land  \ldots  \land  S \subseteq  B </math>||  ||  M
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BINTER}}||<math>  S \subseteq  A \binter  \ldots  \binter  B \;\;\defi\;\;  S \subseteq  A \land  \ldots  \land  S \subseteq  B </math>||  ||  A
<!--
{{RRRow}}|||{{Rulename|SIMP_SUBSET_BUNION}}||<math>  A \bunion  \ldots  \bunion  B  \subset  S \;\;\defi\;\;  A  \subset  S \land  \ldots  \land  B  \subset  S </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_SUBSET_BUNION}}||<math>  A \bunion  \ldots  \bunion  B  \subset  S \;\;\defi\;\;  A  \subset  S \land  \ldots  \land  B  \subset  S </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_SUBSET_BINTER}}||<math>  S  \subset  A \binter  \ldots  \binter  B \;\;\defi\;\;  S  \subset  A \land  \ldots  \land  S  \subset  B </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_SUBSET_BINTER}}||<math>  S  \subset  A \binter  \ldots  \binter  B \;\;\defi\;\;  S  \subset  A \land  \ldots  \land  S  \subset  B </math>||  ||  A
-->
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN}}||<math>  E \in  \emptyset  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN}}||<math>  E \in  \emptyset  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IN}}||<math>  B \in  \{ A, \ldots , B, \ldots , C\}  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IN}}||<math>  B \in  \{ A, \ldots , B, \ldots , C\}  \;\;\defi\;\;  \btrue </math>||  ||  A
Line 60: Line 68:
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BINTER}}||<math>  S \binter  \ldots  \binter  \mathit{Ty} \binter  \ldots  \binter  T \;\;\defi\;\;  S \binter  \ldots  \binter  T </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BINTER}}||<math>  S \binter  \ldots  \binter  \mathit{Ty} \binter  \ldots  \binter  T \;\;\defi\;\;  S \binter  \ldots  \binter  T </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_BINTER}}||<math>  S \binter  \ldots  \binter  T \binter  \ldots  \binter  T \binter  \ldots  \binter  U \;\;\defi\;\;  S \binter  \ldots  \binter  T \binter  \ldots  \binter  U </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_BINTER}}||<math>  S \binter  \ldots  \binter  T \binter  \ldots  \binter  T \binter  \ldots  \binter  U \;\;\defi\;\;  S \binter  \ldots  \binter  T \binter  \ldots  \binter  U </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_EQUAL_BINTER}}||<math>  S \binter  \ldots  \binter  T \binter  \ldots  \binter  U = T \;\;\defi\;\;  T \subseteq  S \binter  \ldots  \binter  U </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL_BINTER}}||<math>  S \binter  \ldots  \binter  T \binter  \ldots  \binter  U = T \;\;\defi\;\;  T \subseteq  S \binter  \ldots  \binter  U </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_BUNION}}||<math>  S \bunion  \ldots  \bunion  \emptyset  \bunion  \ldots  \bunion  T \;\;\defi\;\;  S \bunion  \ldots  \bunion  T </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_BUNION}}||<math>  S \bunion  \ldots  \bunion  \emptyset  \bunion  \ldots  \bunion  T \;\;\defi\;\;  S \bunion  \ldots  \bunion  T </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BUNION}}||<math>  S \bunion  \ldots  \bunion  \mathit{Ty} \bunion  \ldots  \bunion  T \;\;\defi\;\;  \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BUNION}}||<math>  S \bunion  \ldots  \bunion  \mathit{Ty} \bunion  \ldots  \bunion  T \;\;\defi\;\;  \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_BUNION}}||<math>  S \bunion  \ldots  \bunion T \bunion  \ldots  \bunion T \bunion \ldots  \bunion  U \;\;\defi\;\;  S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_BUNION}}||<math>  S \bunion  \ldots  \bunion T \bunion  \ldots  \bunion T \bunion \ldots  \bunion  U \;\;\defi\;\;  S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_EQUAL_BUNION}}||<math>  S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U = T \;\;\defi\;\;  S \bunion  \ldots  \bunion  U \subseteq  T </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL_BUNION}}||<math>  S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U = T \;\;\defi\;\;  S \bunion  \ldots  \bunion  U \subseteq  T </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SETMINUS}}||<math>  S \setminus S \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SETMINUS}}||<math>  S \setminus S \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SETMINUS_R}}||<math>  S \setminus \emptyset  \;\;\defi\;\;  S </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SETMINUS_R}}||<math>  S \setminus \emptyset  \;\;\defi\;\;  S </math>||  ||  A
Line 70: Line 78:
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS}}||<math>  S \setminus \mathit{Ty} \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS}}||<math>  S \setminus \mathit{Ty} \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS_SETMINUS}}||<math> \mathit{Ty} \setminus (\mathit{Ty} \setminus S) \;\;\defi\;\;  S </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS_SETMINUS}}||<math> \mathit{Ty} \setminus (\mathit{Ty} \setminus S) \;\;\defi\;\;  S </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|||{{Rulename|SIMP_TYPE_KUNION}}||<math>  \union (\mathit{Ty}) \;\;\defi\;\;  \mathit{Ta} </math>|| where <math>\mathit{Ty}</math> is a type expression and <math>\mathit{Ty} = \pow (\mathit{Ta})</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_KUNION_POW}}||<math>  \union (\pow (S)) \;\;\defi\;\;  S </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_KUNION_POW}}||<math>  \union (\pow (S)) \;\;\defi\;\;  S </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_KUNION_POW1}}||<math>  \union (\pown (S)) \;\;\defi\;\;  S </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_KUNION_POW1}}||<math>  \union (\pown (S)) \;\;\defi\;\;  S </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KUNION}}||<math>  \union (\{ \emptyset \} ) \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KUNION}}||<math>  \union \{ \emptyset \} ) \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_QUNION}}||<math>  \Union  x\qdot  \bfalse  \mid  E \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_QUNION}}||<math>  \Union  x\qdot  \bfalse  \mid  E \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KINTER}}||<math>  \inter (\{ \emptyset \} ) \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KINTER}}||<math>  \inter (\{ \emptyset \} ) \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_KINTER_POW}}||<math>  \inter (\pow (S)) \;\;\defi\;\;  \emptyset </math>|| ||  A
{{RRRow}}|||{{Rulename|SIMP_TYPE_KINTER}}||<math>  \inter (\mathit{Ty}) \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_POW}}||<math>  \pow (\emptyset ) \;\;\defi\;\;  \{ \emptyset \} </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_POW}}||<math>  \pow (\emptyset ) \;\;\defi\;\;  \{ \emptyset \} </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_POW1}}||<math>  \pown (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_POW1}}||<math>  \pown (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_CPROD_R}}||<math>  S \cprod  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_CPROD_R}}||<math>  S \cprod  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_CPROD_L}}||<math>  \emptyset  \cprod  S \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_CPROD_L}}||<math>  \emptyset  \cprod  S \;\;\defi\;\;  \emptyset </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_COMPSET_EQUAL}}||<math>  \{ x, y \qdot x = E(y) \land P(y) \mid F(x, y) \}  \;\;\defi\;\;  \{ y \qdot P(y) \mid F(E(y), y) \} </math>|| where <math>x</math> non free in <math>E</math> and non free in <math>P</math> ||  A
{{RRRow}}|||{{Rulename|SIMP_COMPSET_EQUAL}}||<math>  \{ x \qdot x = E \mid x \}  \;\;\defi\;\;  \{ E\} </math>|| where <math>x</math> non free in <math>E</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_COMPSET_IN}}||<math>  \{  x \qdot  x \in  S \mid  x \}  \;\;\defi\;\;  S </math>|| where <math>x</math> non free in <math>S</math> ||  A
{{RRRow}}|||{{Rulename|SIMP_COMPSET_IN}}||<math>  \{  x \qdot  x \in  S \mid  x \}  \;\;\defi\;\;  S </math>|| where <math>x</math> non free in <math>S</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_COMPSET_SUBSETEQ}}||<math>  \{  x \qdot  x \subseteq S \mid  x \}  \;\;\defi\;\;  \pow (S)  </math>|| where <math>x</math> non free in <math>S</math> ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_COMPSET_BFALSE}}||<math>  \{  x \qdot  \bfalse \mid  x \}  \;\;\defi\;\;  \emptyset </math>|| ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COMPSET_BFALSE}}||<math>  \{  x \qdot  \bfalse \mid  x \}  \;\;\defi\;\;  \emptyset </math>|| ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_COMPSET_BTRUE}}||<math>  \{  x \qdot  \btrue \mid  x \}  \;\;\defi\;\;  \mathit{Ty} </math>|| where the type od <math>x</math> is <math>\mathit{Ty}</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COMPSET_BTRUE}}||<math>  \{  x \qdot  \btrue  \mid  E \}  \;\;\defi\;\;  \mathit{Ty} </math>|| where the type of <math>E</math> is <math>\mathit{Ty}</math> and <math>E</math> is a maplet combination of locally-bound, pairwise-distinct bound identifiers ||  A
{{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_COMPSET_L}}||<math>  \{  x \qdot  P(x) \mid  E(x) \}  \subseteq  S \;\;\defi\;\;  \forall y\qdot  P(y) \limp  E(y) \in  S </math>|| where <math>y</math> is fresh ||  A
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_COMPSET_L}}||<math>  \{  x \qdot  P(x) \mid  E(x) \}  \subseteq S \;\;\defi\;\;  \forall y\qdot  P(y) \limp  E(y) \in  S </math>|| where <math>y</math> is fresh ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EQUAL_COMPSET}}||<math>  \{  x \qdot  P(x) \mid  E \}  = \emptyset \;\;\defi\;\;  \forall x\qdot  \lnot\, P(x) </math>|| ||  A
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET}}||<math>  F \in  \{  x,y,\ldots \qdot  P(x,y,\ldots) \mid  E(x,y,\ldots) \}  \;\;\defi\;\;  \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F </math>|| where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET}}||<math>  F \in  \{  x,y,\ldots \qdot  P(x,y,\ldots) \mid  E(x,y,\ldots) \}  \;\;\defi\;\;  \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F </math>|| where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET_ONEPOINT}}||<math>  E \in  \{  x \qdot  P(x) \mid  x \}  \;\;\defi\;\;  P(E) </math>|| Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate ||  A
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET_ONEPOINT}}||<math>  E \in  \{  x \qdot  P(x) \mid  x \}  \;\;\defi\;\;  P(E) </math>|| Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate ||  A
{{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_COMPSET_R}}||<math>  S \subseteq  \{  x \qdot  P(x) \mid  x \}  \;\;\defi\;\;  \forall y\qdot  y \in  S \limp  P(y) </math>|| where <math>y</math> non free in <math>x, S, \{  x \qdot  P(x) \mid  x \}</math> ||  A
{{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_COMPSET_R}}||<math>  S \subseteq  \{  x \qdot  P(x) \mid  x \}  \;\;\defi\;\;  \forall y\qdot  y \in  S \limp  P(y) </math>|| where <math>y</math> non free in <math>S, \{  x \qdot  P(x) \mid  x \}</math> ||  M
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_OVERL}}||<math>  r \ovl  \ldots  \ovl  \emptyset  \ovl  \ldots  \ovl  s \;\;\defi\;\;  r \ovl  \ldots  \ovl  s </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OVERL}}||<math>  r \ovl  \ldots  \ovl  \emptyset  \ovl  \ldots  \ovl  s \;\;\defi\;\;  r \ovl  \ldots  \ovl  s </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_OVERL}}||<math>\begin{array}{cl} & r \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  u \\ \defi &  r \ovl  \ldots  \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  u \end{array}</math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_TYPE_OVERL_CPROD}}||<math>  r \ovl  (\mathit{Ty} \cprod  S) \;\;\defi\;\;  (\mathit{Ty} \cprod  S) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BTRUE}}||<math>  \bool (\btrue ) \;\;\defi\;\;  \True </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BTRUE}}||<math>  \bool (\btrue ) \;\;\defi\;\;  \True </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BFALSE}}||<math>  \bool (\bfalse ) \;\;\defi\;\;  \False </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BFALSE}}||<math>  \bool (\bfalse ) \;\;\defi\;\;  \False </math>||  ||  A
{{RRRow}}|||{{Rulename|DISTRI_SUBSETEQ_BUNION_SING}}||<math>  S \bunion  \{ F\}  \subseteq  T \;\;\defi\;\;  S \subseteq  T \land  F \in  T </math>|| where <math>F</math> is a single expression ||  M
{{RRRow}}|||{{Rulename|DISTRI_SUBSETEQ_BUNION_SING}}||<math>  S \bunion  \{ F\}  \subseteq  T \;\;\defi\;\;  S \subseteq  T \land  F \in  T </math>|| where <math>F</math> is a single expression ||  M
{{RRRow}}| ||{{Rulename|DEF_FINITE}}||<math>  \finite(S) \;\;\defi\;\;  \exists n,f\qdot n\in\nat\land f\in 1\upto n \tbij S </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_FINITE}}||<math>  \finite(S) \;\;\defi\;\;  \exists n,f\qdot f\in 1\upto n \tbij S </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_FINITE}}||<math>  \finite (\emptyset ) \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_FINITE}}||<math>  \finite (\emptyset ) \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_SETENUM}}||<math>  \finite (\{ a, \ldots , b\} ) \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_SETENUM}}||<math>  \finite (\{ a, \ldots , b\} ) \;\;\defi\;\;  \btrue </math>||  ||  A
Line 104: Line 109:
{{RRRow}}|*||{{Rulename|SIMP_FINITE_CONVERSE}}||<math>  \finite (r^{-1} ) \;\;\defi\;\;  \finite (r) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_CONVERSE}}||<math>  \finite (r^{-1} ) \;\;\defi\;\;  \finite (r) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_UPTO}}||<math>  \finite (a \upto  b) \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_UPTO}}||<math>  \finite (a \upto  b) \;\;\defi\;\;  \btrue </math>||  ||  A
<!-- Disabled rules (some are false, need more thinking to check which)
{{RRRow}}|||{{Rulename|SIMP_FINITE_UNION}}||<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp \finite(x))</math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_QUNION}}||<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp \finite(E))</math>|| this equivalence is false: for example, the union of an infinite set of empty sets is finite; the right-to-left implication is true ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_L}}||<math>  \finite (S \binter  T) \;\;\defi\;\;  \finite (S) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_L}}||<math>  \finite (S \binter  T) \;\;\defi\;\;  \finite (S) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_R}}||<math>  \finite (S \binter  T) \;\;\defi\;\;  \finite (T) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_R}}||<math>  \finite (S \binter  T) \;\;\defi\;\;  \finite (T) </math>||  ||  M
Line 122: Line 130:
{{RRRow}}|||{{Rulename|SIMP_FINITE_RAN}}||<math>  \finite (\ran (r)) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_RAN}}||<math>  \finite (\ran (r)) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_DOM}}||<math>  \finite (\dom (r)) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_DOM}}||<math>  \finite (\dom (r)) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_QUNION}}||<math>  \finite (\Union  x \qdot  P \mid  E) \;\;\defi\;\;  \forall x \qdot  P \limp  \finite (E) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_QINTER}}||<math>  \finite (\Inter  x \qdot  P \mid  E) \;\;\defi\;\;  \exists x \qdot  P \land  \finite (E) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_QINTER}}||<math>  \finite (\Inter  x \qdot  P \mid  E) \;\;\defi\;\;  \exists x \qdot  P \land  \finite (E) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_ID}}||<math>  \finite (\id) \;\;\defi\;\;  \finite (S) </math>|| where <math>\id</math> has type <math>\pow(S \cprod S)</math> ||  A
-->
{{RRRow}}|||{{Rulename|SIMP_FINITE_NATURAL}}||<math>  \finite (\nat ) \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_ID}}||<math>  \finite (\id) \;\;\defi\;\;  \finite (S) </math>|| where <math>\id</math> has type <math>\pow(S \cprod S)</math> ||  A
{{RRRow}}|||{{Rulename|SIMP_FINITE_NATURAL1}}||<math>  \finite (\natn ) \;\;\defi\;\;  \bfalse </math>|| ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_ID_DOMRES}}||<math>  \finite (E \domres \id) \;\;\defi\;\;  \finite (E) </math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_FINITE_INTEGER}}||<math>  \finite (\intg ) \;\;\defi\;\;  \bfalse </math>|| ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ1}}||<math>  \finite (\prjone) \;\;\defi\;\;  \finite (S \cprod T) </math>|| where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> ||  A
{{RRRow}}|||{{Rulename|SIMP_FINITE_LAMBDA}}||<math>  \finite (\lambda x \qdot P \mid E) \;\;\defi\;\;  \finite (\{ x \qdot P \mid x\} ) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ2}}||<math>  \finite (\prjtwo) \;\;\defi\;\;  \finite (S \cprod T) </math>|| where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_EQUAL_EMPTY}}||<math> \mathit{Ty} = \emptyset  \;\;\defi\;\;  \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ1_DOMRES}}||<math>  \finite (E \domres \prjone) \;\;\defi\;\; \finite (E) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ2_DOMRES}}||<math> \finite (E \domres \prjtwo) \;\;\defi\;\;  \finite (E) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_NATURAL}}||<math>  \finite (\nat ) \;\;\defi\;\; \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_NATURAL1}}||<math> \finite (\natn ) \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_INTEGER}}||<math> \finite (\intg ) \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_BOOL}}||<math>  \finite (\Bool ) \;\;\defi\;\;  \btrue </math>|| ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_LAMBDA}}||<math> \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\;  \finite(\{x\qdot P\mid E\} ) </math>|| where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_IN}}||<math>  t \in  \mathit{Ty} \;\;\defi\;\;  \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_IN}}||<math>  t \in  \mathit{Ty} \;\;\defi\;\;  \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_FORALL_BTRUE}}||<math>  \forall x \qdot  \btrue  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_FORALL_BFALSE}}||<math>  \forall x \qdot  \bfalse  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EXISTS_BTRUE}}||<math>  \exists x \qdot  \btrue  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EXISTS_BFALSE}}||<math>  \exists x \qdot  \bfalse  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BTRUE}}||<math>  P \leqv  \btrue  \;\;\defi\;\;  P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BTRUE}}||<math>  P \leqv  \btrue  \;\;\defi\;\;  P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BFALSE}}||<math>  P \leqv  \bfalse  \;\;\defi\;\;  \lnot\, P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BFALSE}}||<math>  P \leqv  \bfalse  \;\;\defi\;\;  \lnot\, P </math>||  ||  A
{{RRRow}}|*||{{Rulename|DEF_SUBSET}}||<math>  A  \subset  B  \;\;\defi\;\;  A \subseteq B \land \lnot A = B </math>||  ||  A
{{RRRow}}|*||{{Rulename|DEF_SUBSET}}||<math>  A  \subset  B  \;\;\defi\;\;  A \subseteq B \land \lnot A = B </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_SUBSET_R}}||<math>  S  \subset  \emptyset  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSET_R}}||<math>  S  \subset  \emptyset  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_SUBSET_L}}||<math> \emptyset   \subset S \;\;\defi\;\;  S \neq  \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSET_L}}||<math>\emptyset\subset S \;\;\defi\;\;  \lnot\; S = \emptyset</math>||  ||  A
{{RRRow}}|||{{Rulename|SIMP_TYPE_SUBSET_L}}||<math>  S  \subset  \mathit{Ty} \;\;\defi\;\;  S \neq  \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SUBSET_L}}||<math>  S  \subset  \mathit{Ty} \;\;\defi\;\;  S \neq  \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
{{RRRow}}|||{{Rulename|SIMP_MULTI_SUBSET}}||<math>  S  \subset  S \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SUBSET}}||<math>  S  \subset  S \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_CONSTR}}||<math>  \operatorname{constr} (a_1, \ldots, a_n) = \operatorname{constr} (b_1, \ldots, b_n)  \;\;\defi\;\;  a_1 = b_1 \land \ldots \land  a_n = b_n  </math>|| where <math>\operatorname{constr}</math> is a datatype constructor ||  A
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_CONSTR_DIFF}}||<math>  \operatorname{constr_1} (\ldots) = \operatorname{constr_2} (\ldots)  \;\;\defi\;\;  \bfalse </math>|| where <math>\operatorname{constr_1}</math> and <math>\operatorname{constr_2}</math> are different datatype constructors ||  A
{{RRRow}}|*||{{Rulename|SIMP_DESTR_CONSTR}}||<math>  \operatorname{destr} (\operatorname{constr} (a_1, \ldots, a_n))  \;\;\defi\;\;  a_i  </math>|| where <math>\operatorname{destr}</math> is the datatype destructor for the i-th argument of datatype constructor <math>\operatorname{constr}</math> ||  A
{{RRRow}}|*||{{Rulename|DISTRI_AND_OR}}||<math>  P \land  (Q \lor  R) \;\;\defi\;\;  (P \land  Q) \lor  (P \land  R) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_AND_OR}}||<math>  P \land  (Q \lor  R) \;\;\defi\;\;  (P \land  Q) \lor  (P \land  R) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_OR_AND}}||<math>  P \lor  (Q \land  R) \;\;\defi\;\;  (P \lor  Q) \land  (P \lor  R) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_OR_AND}}||<math>  P \lor  (Q \land  R) \;\;\defi\;\;  (P \lor  Q) \land  (P \lor  R) </math>||  ||  M
Line 155: Line 167:
{{RRRow}}|*||{{Rulename|DERIV_NOT_FORALL}}||<math>  \lnot\, \forall x \qdot  P \;\;\defi\;\;  \exists x \qdot  \lnot\, P </math>||  ||  M
{{RRRow}}|*||{{Rulename|DERIV_NOT_FORALL}}||<math>  \lnot\, \forall x \qdot  P \;\;\defi\;\;  \exists x \qdot  \lnot\, P </math>||  ||  M
{{RRRow}}|*||{{Rulename|DERIV_NOT_EXISTS}}||<math>  \lnot\, \exists x \qdot  P \;\;\defi\;\;  \forall x \qdot  \lnot\, P </math>||  ||  M
{{RRRow}}|*||{{Rulename|DERIV_NOT_EXISTS}}||<math>  \lnot\, \exists x \qdot  P \;\;\defi\;\;  \forall x \qdot  \lnot\, P </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_SPECIAL_NOT_EQUAL}}||<math>  \lnot\, S = \emptyset  \;\;\defi\;\;  \exists x \qdot  x \in  S </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_MAPSTO}}||<math>  E \mapsto  F \in  S \cprod  T \;\;\defi\;\;  E \in  S \land  F \in  T </math>||  ||  AM
{{RRRow}}|*||{{Rulename|DEF_IN_MAPSTO}}||<math>  E \mapsto  F \in  S \cprod  T \;\;\defi\;\;  E \in  S \land  F \in  T </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_POW}}||<math>  E \in  \pow (S) \;\;\defi\;\;  E \subseteq  S </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_POW}}||<math>  E \in  \pow (S) \;\;\defi\;\;  E \subseteq  S </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_POW1}}||<math>  E \in  \pown (S) \;\;\defi\;\; E \in  \pow (S) \land S \neq \emptyset </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_POW1}}||<math>  E \in  \pown (S) \;\;\defi\;\; E \in  \pow (S) \land S \neq \emptyset </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_SUBSETEQ}}||<math> S \subseteq T  \;\;\defi\;\;  \forall x \qdot  x \in  S \limp  x \in  T </math>|| ||  M
{{RRRow}}|*||{{Rulename|DEF_SUBSETEQ}}||<math> S \subseteq T  \;\;\defi\;\;  \forall x \qdot  x \in  S \limp  x \in  T </math>|| where <math>x</math> is not free in <math>S</math> or <math>T</math> ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_BUNION}}||<math>  E \in  S \bunion  T \;\;\defi\;\;  E \in  S \lor  E \in  T </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_BUNION}}||<math>  E \in  S \bunion  T \;\;\defi\;\;  E \in  S \lor  E \in  T </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_BINTER}}||<math>  E \in  S \binter  T \;\;\defi\;\;  E \in  S \land  E \in  T </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_BINTER}}||<math>  E \in  S \binter  T \;\;\defi\;\;  E \in  S \land  E \in  T </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_SETMINUS}}||<math>  E \in  S \setminus T \;\;\defi\;\;  E \in  S \land  \lnot\,(E \in  T) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_SETMINUS}}||<math>  E \in  S \setminus T \;\;\defi\;\;  E \in  S \land  \lnot\,(E \in  T) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_SETENUM}}||<math>  E \in  \{ A, \ldots , B\}  \;\;\defi\;\;  E = A \lor  \ldots  \lor  E = B </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_SETENUM}}||<math>  E \in  \{ A, \ldots , B\}  \;\;\defi\;\;  E = A \lor  \ldots  \lor  E = B </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_KUNION}}||<math>  E \in  \union (S) \;\;\defi\;\;  \exists s \qdot  s \in  S \land  E \in  s </math>|| ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_KUNION}}||<math>  E \in  \union (S) \;\;\defi\;\;  \exists s \qdot  s \in  S \land  E \in  s </math>|| where <math>s</math> is fresh ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_QUNION}}||<math>  E \in  (\Union x \qdot x \in  S \land  P \mid T) \;\;\defi\;\;  \exists x \qdot x \in  S \land  P \land E \in T </math>|| ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_QUNION}}||<math>  E \in  (\Union x \qdot P(x) \mid T(x)) \;\;\defi\;\;  \exists s \qdot P(s) \land E \in T(s) </math>|| where <math>s</math> is fresh ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_KINTER}}||<math>  E \in  \inter (S) \;\;\defi\;\;  \forall s \qdot  s \in  S \limp  E \in  s </math>|| ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_KINTER}}||<math>  E \in  \inter (S) \;\;\defi\;\;  \forall s \qdot  s \in  S \limp  E \in  s </math>|| where <math>s</math> is fresh ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_QINTER}}||<math>  E \in  (\Inter x \qdot x \in  S \land  P \mid T) \;\;\defi\;\;  \forall x \qdot x \in  S \land  P \limp E \in T </math>|| ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_QINTER}}||<math>  E \in  (\Inter x \qdot P(x) \mid T(x)) \;\;\defi\;\;  \forall s \qdot P(s) \limp E \in T(s) </math>|| where <math>s</math> is fresh ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_UPTO}}||<math>  E \in  a \upto b \;\;\defi\;\; a \leq E \land E \leq b  </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_UPTO}}||<math>  E \in  a \upto b \;\;\defi\;\; a \leq E \land E \leq b  </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_BUNION_BINTER}}||<math>  S \bunion  (T \binter  U) \;\;\defi\;\;  (S \bunion  T) \binter  (S \bunion  U) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_BUNION_BINTER}}||<math>  S \bunion  (T \binter  U) \;\;\defi\;\;  (S \bunion  T) \binter  (S \bunion  U) </math>||  ||  M
Line 192: Line 203:
\land& s_{n-1}\binter s_n = \emptyset
\land& s_{n-1}\binter s_n = \emptyset
\end{array}</math>||  ||  AM
\end{array}</math>||  ||  AM
{{RRRow}}|*||{{Rulename|SIMP_EMPTY_PARTITION}}||<math>\operatorname{partition}(S)  \;\;\defi\;\;  S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SINGLE_PARTITION}}||<math>\operatorname{partition}(S, T)  \;\;\defi\;\;  S = T </math>||  ||  A
{{RRRow}}|*||{{Rulename|DEF_EQUAL_CARD}}||<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>|| also works for <math>k = \operatorname{card}(S)</math> || M
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_CARD}}||<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>|| || M
|}
|}



Latest revision as of 14:33, 13 April 2023

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
  P \land  \ldots  \land  \btrue  \land  \ldots  \land  Q \;\;\defi\;\;  P \land  \ldots  \land  Q A
*
SIMP_SPECIAL_AND_BFALSE
  P \land  \ldots  \land  \bfalse  \land  \ldots  \land  Q \;\;\defi\;\;  \bfalse A
*
SIMP_MULTI_AND
  P \land  \ldots  \land  Q \land  \ldots  \land  Q \land  \ldots  \land  R \;\;\defi\;\;  P \land  \ldots  \land  Q \land  \ldots  \land  R A
*
SIMP_MULTI_AND_NOT
  P \land  \ldots  \land  Q \land  \ldots  \land  \lnot\, Q \land  \ldots  \land  R \;\;\defi\;\;  \bfalse A
*
SIMP_SPECIAL_OR_BTRUE
  P \lor  \ldots  \lor  \btrue  \lor  \ldots  \lor  Q \;\;\defi\;\;  \btrue A
*
SIMP_SPECIAL_OR_BFALSE
  P \lor  \ldots  \lor  \bfalse  \lor  \ldots  \lor  Q \;\;\defi\;\;  P \lor  \ldots  \lor  Q A
*
SIMP_MULTI_OR
  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  Q \lor  \ldots  \lor  R \;\;\defi\;\;  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  R A
*
SIMP_MULTI_OR_NOT
  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  \lnot\, Q \land  \ldots  \land  R \;\;\defi\;\;  \btrue A
*
SIMP_SPECIAL_IMP_BTRUE_R
  P \limp  \btrue  \;\;\defi\;\;  \btrue A
*
SIMP_SPECIAL_IMP_BTRUE_L
  \btrue  \limp  P \;\;\defi\;\;  P A
*
SIMP_SPECIAL_IMP_BFALSE_R
  P \limp  \bfalse  \;\;\defi\;\;  \lnot\, P A
*
SIMP_SPECIAL_IMP_BFALSE_L
  \bfalse  \limp  P \;\;\defi\;\;  \btrue A
*
SIMP_MULTI_IMP
  P \limp  P \;\;\defi\;\;  \btrue A
*
SIMP_MULTI_IMP_NOT_L
\lnot P\limp P\;\;\defi\;\; P A
*
SIMP_MULTI_IMP_NOT_R
P\limp\lnot P\;\;\defi\;\;\lnot P A
*
SIMP_MULTI_IMP_AND
  P \land  \ldots  \land  Q \land  \ldots  \land  R \limp  Q \;\;\defi\;\;  \btrue A
*
SIMP_MULTI_IMP_AND_NOT_R
  P \land  \ldots  \land  Q \land  \ldots  \land  R \limp  \lnot\, Q \;\;\defi\;\;  \lnot\,(P \land  \ldots  \land  Q \land  \ldots  \land  R) A
*
SIMP_MULTI_IMP_AND_NOT_L
  P \land  \ldots  \land  \lnot\, Q \land  \ldots  \land  R \limp  Q \;\;\defi\;\;  \lnot\,(P \land  \ldots  \land  \lnot\, Q \land  \ldots  \land  R) A
*
SIMP_MULTI_EQV
  P \leqv  P \;\;\defi\;\;  \btrue A
*
SIMP_MULTI_EQV_NOT
  P \leqv  \lnot\, P \;\;\defi\;\;  \bfalse A
*
SIMP_SPECIAL_NOT_BTRUE
  \lnot\, \btrue  \;\;\defi\;\;  \bfalse A
*
SIMP_SPECIAL_NOT_BFALSE
  \lnot\, \bfalse  \;\;\defi\;\;  \btrue A
*
SIMP_NOT_NOT
  \lnot\, \lnot\, P \;\;\defi\;\;  P AM
*
SIMP_NOTEQUAL
  E \neq  F \;\;\defi\;\;  \lnot\, E = F A
*
SIMP_NOTIN
  E \notin  F \;\;\defi\;\;  \lnot\, E \in  F A
*
SIMP_NOTSUBSET
  E  \not\subset  F \;\;\defi\;\;  \lnot\, E  \subset  F A
*
SIMP_NOTSUBSETEQ
  E  \not\subseteq  F \;\;\defi\;\;  \lnot\, E \subseteq  F A
*
SIMP_NOT_LE
  \lnot\, a \leq  b \;\;\defi\;\;  a > b A
*
SIMP_NOT_GE
  \lnot\, a \geq  b \;\;\defi\;\;  a < b A
*
SIMP_NOT_LT
  \lnot\, a < b \;\;\defi\;\;  a \geq  b A
*
SIMP_NOT_GT
  \lnot\, a > b \;\;\defi\;\;  a \leq  b A
*
SIMP_SPECIAL_NOT_EQUAL_FALSE_R
  \lnot\, (E = \False ) \;\;\defi\;\;  (E = \True ) A
*
SIMP_SPECIAL_NOT_EQUAL_FALSE_L
  \lnot\, (\False  = E) \;\;\defi\;\;  (\True  = E) A
*
SIMP_SPECIAL_NOT_EQUAL_TRUE_R
  \lnot\, (E = \True ) \;\;\defi\;\;  (E = \False ) A
*
SIMP_SPECIAL_NOT_EQUAL_TRUE_L
  \lnot\, (\True  = E) \;\;\defi\;\;  (\False  = E) A
*
SIMP_FORALL_AND
  \forall x \qdot  P \land  Q \;\;\defi\;\;  (\forall x \qdot  P) \land  (\forall x \qdot  Q) A
*
SIMP_EXISTS_OR
  \exists x \qdot  P \lor  Q \;\;\defi\;\;  (\exists x \qdot  P) \lor  (\exists x \qdot  Q) A
*
SIMP_EXISTS_IMP
\exists x\qdot P\limp Q\;\;\defi\;\;(\forall x\qdot P)\limp(\exists x\qdot Q) A
*
SIMP_FORALL
  \forall \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \forall z \qdot  P(z) Quantified identifiers other than z do not occur in P A
*
SIMP_EXISTS
  \exists \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \exists z \qdot  P(z) Quantified identifiers other than z do not occur in P A
*
SIMP_MULTI_EQUAL
  E = E \;\;\defi\;\;  \btrue A
*
SIMP_MULTI_NOTEQUAL
  E \neq  E \;\;\defi\;\;  \bfalse A
*
SIMP_EQUAL_MAPSTO
  E \mapsto  F = G \mapsto  H \;\;\defi\;\;  E = G \land  F = H A
*
SIMP_EQUAL_SING
  \{ E\}  = \{ F\}  \;\;\defi\;\;  E = F A
*
SIMP_SPECIAL_EQUAL_TRUE
  \True  = \False  \;\;\defi\;\;  \bfalse A
*
SIMP_TYPE_SUBSETEQ
  S \subseteq  \mathit{Ty} \;\;\defi\;\;  \btrue where \mathit{Ty} is a type expression A
*
SIMP_SUBSETEQ_SING
  \{ E\}  \subseteq  S \;\;\defi\;\;  E \in  S where E is a single expression A
*
SIMP_SPECIAL_SUBSETEQ
  \emptyset  \subseteq  S \;\;\defi\;\;  \btrue A
*
SIMP_MULTI_SUBSETEQ
  S \subseteq  S \;\;\defi\;\;  \btrue A
*
SIMP_SUBSETEQ_BUNION
  S \subseteq  A \bunion  \ldots  \bunion  S \bunion  \ldots  \bunion  B \;\;\defi\;\;  \btrue A
*
SIMP_SUBSETEQ_BINTER
  A \binter  \ldots  \binter  S \binter  \ldots  \binter  B \subseteq  S \;\;\defi\;\;  \btrue A
*
DERIV_SUBSETEQ_BUNION
  A \bunion  \ldots  \bunion  B \subseteq  S \;\;\defi\;\;  A \subseteq  S \land  \ldots  \land  B \subseteq  S A
*
DERIV_SUBSETEQ_BINTER
  S \subseteq  A \binter  \ldots  \binter  B \;\;\defi\;\;  S \subseteq  A \land  \ldots  \land  S \subseteq  B A
*
SIMP_SPECIAL_IN
  E \in  \emptyset  \;\;\defi\;\;  \bfalse A
*
SIMP_MULTI_IN
  B \in  \{ A, \ldots , B, \ldots , C\}  \;\;\defi\;\;  \btrue A
*
SIMP_IN_SING
  E \in  \{ F\}  \;\;\defi\;\;  E = F A
*
SIMP_MULTI_SETENUM
  \{ A, \ldots , B, \ldots , B, \ldots , C\}  \;\;\defi\;\;  \{ A, \ldots , B, \ldots , C\} A
*
SIMP_SPECIAL_BINTER
  S \binter  \ldots  \binter  \emptyset  \binter  \ldots  \binter  T \;\;\defi\;\;  \emptyset A
*
SIMP_TYPE_BINTER
  S \binter  \ldots  \binter  \mathit{Ty} \binter  \ldots  \binter  T \;\;\defi\;\;  S \binter  \ldots  \binter  T where \mathit{Ty} is a type expression A
*
SIMP_MULTI_BINTER
  S \binter  \ldots  \binter  T \binter  \ldots  \binter  T \binter  \ldots  \binter  U \;\;\defi\;\;  S \binter  \ldots  \binter  T \binter  \ldots  \binter  U A
*
SIMP_MULTI_EQUAL_BINTER
  S \binter  \ldots  \binter  T \binter  \ldots  \binter  U = T \;\;\defi\;\;  T \subseteq  S \binter  \ldots  \binter  U A
*
SIMP_SPECIAL_BUNION
  S \bunion  \ldots  \bunion  \emptyset  \bunion  \ldots  \bunion  T \;\;\defi\;\;  S \bunion  \ldots  \bunion  T A
*
SIMP_TYPE_BUNION
  S \bunion  \ldots  \bunion  \mathit{Ty} \bunion  \ldots  \bunion  T \;\;\defi\;\;  \mathit{Ty} where \mathit{Ty} is a type expression A
*
SIMP_MULTI_BUNION
  S \bunion  \ldots  \bunion T \bunion  \ldots  \bunion T \bunion \ldots  \bunion  U \;\;\defi\;\;  S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U A
*
SIMP_MULTI_EQUAL_BUNION
  S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U = T \;\;\defi\;\;  S \bunion  \ldots  \bunion  U \subseteq  T A
*
SIMP_MULTI_SETMINUS
  S \setminus S \;\;\defi\;\;  \emptyset A
*
SIMP_SPECIAL_SETMINUS_R
  S \setminus \emptyset  \;\;\defi\;\;  S A
*
SIMP_SPECIAL_SETMINUS_L
  \emptyset  \setminus S \;\;\defi\;\;  \emptyset A
*
SIMP_TYPE_SETMINUS
  S \setminus \mathit{Ty} \;\;\defi\;\;  \emptyset where \mathit{Ty} is a type expression A
*
SIMP_TYPE_SETMINUS_SETMINUS
 \mathit{Ty} \setminus (\mathit{Ty} \setminus S) \;\;\defi\;\;  S where \mathit{Ty} is a type expression A
*
SIMP_KUNION_POW
  \union (\pow (S)) \;\;\defi\;\;  S A
*
SIMP_KUNION_POW1
  \union (\pown (S)) \;\;\defi\;\;  S A
*
SIMP_SPECIAL_KUNION
  \union (\{ \emptyset \} ) \;\;\defi\;\;  \emptyset A
*
SIMP_SPECIAL_QUNION
  \Union  x\qdot  \bfalse  \mid  E \;\;\defi\;\;  \emptyset A
*
SIMP_SPECIAL_KINTER
  \inter (\{ \emptyset \} ) \;\;\defi\;\;  \emptyset A
*
SIMP_KINTER_POW
  \inter (\pow (S)) \;\;\defi\;\;  \emptyset A
*
SIMP_SPECIAL_POW
  \pow (\emptyset ) \;\;\defi\;\;  \{ \emptyset \} A
*
SIMP_SPECIAL_POW1
  \pown (\emptyset ) \;\;\defi\;\;  \emptyset A
*
SIMP_SPECIAL_CPROD_R
  S \cprod  \emptyset  \;\;\defi\;\;  \emptyset A
*
SIMP_SPECIAL_CPROD_L
  \emptyset  \cprod  S \;\;\defi\;\;  \emptyset A
SIMP_COMPSET_EQUAL
  \{ x, y \qdot x = E(y) \land P(y) \mid F(x, y) \}  \;\;\defi\;\;  \{ y \qdot P(y) \mid F(E(y), y) \} where x non free in E and non free in P A
*
SIMP_COMPSET_IN
  \{  x \qdot  x \in  S \mid  x \}  \;\;\defi\;\;  S where x non free in S A
*
SIMP_COMPSET_SUBSETEQ
  \{  x \qdot  x \subseteq  S \mid  x \}  \;\;\defi\;\;  \pow (S)  where x non free in S A
*
SIMP_SPECIAL_COMPSET_BFALSE
  \{  x \qdot  \bfalse  \mid  x \}  \;\;\defi\;\;  \emptyset A
*
SIMP_SPECIAL_COMPSET_BTRUE
  \{  x \qdot  \btrue  \mid  E \}  \;\;\defi\;\;  \mathit{Ty} where the type of E is \mathit{Ty} and E is a maplet combination of locally-bound, pairwise-distinct bound identifiers A
*
SIMP_SUBSETEQ_COMPSET_L
  \{  x \qdot  P(x) \mid  E(x) \}  \subseteq  S \;\;\defi\;\;  \forall y\qdot  P(y) \limp  E(y) \in  S where y is fresh A
*
SIMP_IN_COMPSET
  F \in  \{  x,y,\ldots \qdot  P(x,y,\ldots) \mid  E(x,y,\ldots) \}  \;\;\defi\;\;  \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F where x, y, \ldots are not free in F A
*
SIMP_IN_COMPSET_ONEPOINT
  E \in  \{  x \qdot  P(x) \mid  x \}  \;\;\defi\;\;  P(E) Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate A
SIMP_SUBSETEQ_COMPSET_R
  S \subseteq  \{  x \qdot  P(x) \mid  x \}  \;\;\defi\;\;  \forall y\qdot  y \in  S \limp  P(y) where y non free in S, \{  x \qdot  P(x) \mid  x \} M
*
SIMP_SPECIAL_OVERL
  r \ovl  \ldots  \ovl  \emptyset  \ovl  \ldots  \ovl  s \;\;\defi\;\;  r \ovl  \ldots  \ovl  s A
*
SIMP_SPECIAL_KBOOL_BTRUE
  \bool (\btrue ) \;\;\defi\;\;  \True A
*
SIMP_SPECIAL_KBOOL_BFALSE
  \bool (\bfalse ) \;\;\defi\;\;  \False A
DISTRI_SUBSETEQ_BUNION_SING
  S \bunion  \{ F\}  \subseteq  T \;\;\defi\;\;  S \subseteq  T \land  F \in  T where F is a single expression M
*
DEF_FINITE
  \finite(S) \;\;\defi\;\;  \exists n,f\qdot f\in 1\upto n \tbij S M
*
SIMP_SPECIAL_FINITE
  \finite (\emptyset ) \;\;\defi\;\;  \btrue A
*
SIMP_FINITE_SETENUM
  \finite (\{ a, \ldots , b\} ) \;\;\defi\;\;  \btrue A
*
SIMP_FINITE_BUNION
  \finite (S \bunion  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) A
*
SIMP_FINITE_POW
  \finite (\pow (S)) \;\;\defi\;\;  \finite (S) A
*
DERIV_FINITE_CPROD
  \finite (S \cprod  T) \;\;\defi\;\;  S = \emptyset  \lor  T = \emptyset  \lor  (\finite (S) \land  \finite (T)) A
*
SIMP_FINITE_CONVERSE
  \finite (r^{-1} ) \;\;\defi\;\;  \finite (r) A
*
SIMP_FINITE_UPTO
  \finite (a \upto  b) \;\;\defi\;\;  \btrue A
*
SIMP_FINITE_ID
  \finite (\id) \;\;\defi\;\;  \finite (S) where \id has type \pow(S \cprod S) A
*
SIMP_FINITE_ID_DOMRES
  \finite (E \domres \id) \;\;\defi\;\;  \finite (E) A
*
SIMP_FINITE_PRJ1
  \finite (\prjone) \;\;\defi\;\;  \finite (S \cprod T) where \prjone has type \pow(S \cprod T \cprod S) A
*
SIMP_FINITE_PRJ2
  \finite (\prjtwo) \;\;\defi\;\;  \finite (S \cprod T) where \prjtwo has type \pow(S \cprod T \cprod T) A
*
SIMP_FINITE_PRJ1_DOMRES
  \finite (E \domres \prjone) \;\;\defi\;\;  \finite (E) A
*
SIMP_FINITE_PRJ2_DOMRES
  \finite (E \domres \prjtwo) \;\;\defi\;\;  \finite (E) A
*
SIMP_FINITE_NATURAL
  \finite (\nat ) \;\;\defi\;\;  \bfalse A
*
SIMP_FINITE_NATURAL1
  \finite (\natn ) \;\;\defi\;\;  \bfalse A
*
SIMP_FINITE_INTEGER
  \finite (\intg ) \;\;\defi\;\;  \bfalse A
*
SIMP_FINITE_BOOL
  \finite (\Bool ) \;\;\defi\;\;  \btrue A
*
SIMP_FINITE_LAMBDA
  \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\;  \finite(\{x\qdot P\mid E\} ) where E is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., E is syntactically injective) and all identifiers bound by the comprehension set that occur in F also occur in E A
*
SIMP_TYPE_IN
  t \in  \mathit{Ty} \;\;\defi\;\;  \btrue where \mathit{Ty} is a type expression A
*
SIMP_SPECIAL_EQV_BTRUE
  P \leqv  \btrue  \;\;\defi\;\;  P A
*
SIMP_SPECIAL_EQV_BFALSE
  P \leqv  \bfalse  \;\;\defi\;\;  \lnot\, P A
*
DEF_SUBSET
  A  \subset  B  \;\;\defi\;\;  A \subseteq B \land \lnot A = B A
*
SIMP_SPECIAL_SUBSET_R
  S  \subset  \emptyset  \;\;\defi\;\;  \bfalse A
*
SIMP_SPECIAL_SUBSET_L
\emptyset\subset S \;\;\defi\;\;  \lnot\; S = \emptyset A
*
SIMP_TYPE_SUBSET_L
  S  \subset  \mathit{Ty} \;\;\defi\;\;  S \neq  \mathit{Ty} where \mathit{Ty} is a type expression A
*
SIMP_MULTI_SUBSET
  S  \subset  S \;\;\defi\;\;  \bfalse A
*
SIMP_EQUAL_CONSTR
  \operatorname{constr} (a_1, \ldots, a_n) = \operatorname{constr} (b_1, \ldots, b_n)  \;\;\defi\;\;  a_1 = b_1 \land \ldots \land  a_n = b_n  where \operatorname{constr} is a datatype constructor A
*
SIMP_EQUAL_CONSTR_DIFF
  \operatorname{constr_1} (\ldots) = \operatorname{constr_2} (\ldots)  \;\;\defi\;\;  \bfalse where \operatorname{constr_1} and \operatorname{constr_2} are different datatype constructors A
*
SIMP_DESTR_CONSTR
  \operatorname{destr} (\operatorname{constr} (a_1, \ldots, a_n))  \;\;\defi\;\;  a_i  where \operatorname{destr} is the datatype destructor for the i-th argument of datatype constructor \operatorname{constr} A
*
DISTRI_AND_OR
  P \land  (Q \lor  R) \;\;\defi\;\;  (P \land  Q) \lor  (P \land  R) M
*
DISTRI_OR_AND
  P \lor  (Q \land  R) \;\;\defi\;\;  (P \lor  Q) \land  (P \lor  R) M
*
DEF_OR
  P \lor  Q \lor  \ldots  \lor  R \;\;\defi\;\;  \lnot\, P \limp  (Q \lor  \ldots  \lor  R) M
*
DERIV_IMP
  P \limp  Q \;\;\defi\;\;  \lnot\, Q \limp  \lnot\, P M
*
DERIV_IMP_IMP
  P \limp  (Q \limp  R) \;\;\defi\;\;  P \land  Q \limp  R M
*
DISTRI_IMP_AND
  P \limp  (Q \land  R) \;\;\defi\;\;  (P \limp  Q) \land  (P \limp  R) M
*
DISTRI_IMP_OR
  (P \lor  Q) \limp  R \;\;\defi\;\;  (P \limp  R) \land  (Q \limp  R) M
*
DEF_EQV
  P \leqv  Q \;\;\defi\;\;  (P \limp  Q) \land  (Q \limp  P) M
*
DISTRI_NOT_AND
  \lnot\,(P \land  Q) \;\;\defi\;\;  \lnot\, P \lor  \lnot\, Q M
*
DISTRI_NOT_OR
  \lnot\,(P \lor  Q) \;\;\defi\;\;  \lnot\, P \land  \lnot\, Q M
*
DERIV_NOT_IMP
  \lnot\,(P \limp  Q) \;\;\defi\;\;  P \land  \lnot\, Q M
*
DERIV_NOT_FORALL
  \lnot\, \forall x \qdot  P \;\;\defi\;\;  \exists x \qdot  \lnot\, P M
*
DERIV_NOT_EXISTS
  \lnot\, \exists x \qdot  P \;\;\defi\;\;  \forall x \qdot  \lnot\, P M
*
DEF_IN_MAPSTO
  E \mapsto  F \in  S \cprod  T \;\;\defi\;\;  E \in  S \land  F \in  T AM
*
DEF_IN_POW
  E \in  \pow (S) \;\;\defi\;\;  E \subseteq  S M
*
DEF_IN_POW1
  E \in  \pown (S) \;\;\defi\;\; E \in  \pow (S) \land S \neq \emptyset M
*
DEF_SUBSETEQ
 S \subseteq T  \;\;\defi\;\;  \forall x \qdot  x \in  S \limp  x \in  T where x is not free in S or T M
*
DEF_IN_BUNION
  E \in  S \bunion  T \;\;\defi\;\;  E \in  S \lor  E \in  T M
*
DEF_IN_BINTER
  E \in  S \binter  T \;\;\defi\;\;  E \in  S \land  E \in  T M
*
DEF_IN_SETMINUS
  E \in  S \setminus T \;\;\defi\;\;  E \in  S \land  \lnot\,(E \in  T) M
*
DEF_IN_SETENUM
  E \in  \{ A, \ldots , B\}  \;\;\defi\;\;  E = A \lor  \ldots  \lor  E = B M
*
DEF_IN_KUNION
  E \in  \union (S) \;\;\defi\;\;  \exists s \qdot  s \in  S \land  E \in  s where s is fresh M
*
DEF_IN_QUNION
  E \in  (\Union x \qdot P(x) \mid T(x)) \;\;\defi\;\;  \exists s \qdot P(s) \land E \in T(s) where s is fresh M
*
DEF_IN_KINTER
  E \in  \inter (S) \;\;\defi\;\;  \forall s \qdot  s \in  S \limp  E \in  s where s is fresh M
*
DEF_IN_QINTER
  E \in  (\Inter x \qdot P(x) \mid T(x)) \;\;\defi\;\;  \forall s \qdot P(s) \limp E \in T(s) where s is fresh M
*
DEF_IN_UPTO
  E \in  a \upto b \;\;\defi\;\; a \leq E \land E \leq b  M
*
DISTRI_BUNION_BINTER
  S \bunion  (T \binter  U) \;\;\defi\;\;  (S \bunion  T) \binter  (S \bunion  U) M
*
DISTRI_BINTER_BUNION
  S \binter  (T \bunion  U) \;\;\defi\;\;  (S \binter  T) \bunion  (S \binter  U) M
DISTRI_BINTER_SETMINUS
  S \binter  (T \setminus U) \;\;\defi\;\;  (S \binter  T) \setminus (S \binter  U) M
DISTRI_SETMINUS_BUNION
  S \setminus (T \bunion  U) \;\;\defi\;\;  S \setminus T \setminus U M
*
DERIV_TYPE_SETMINUS_BINTER
  \mathit{Ty} \setminus (S \binter  T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \bunion  (\mathit{Ty} \setminus T) where \mathit{Ty} is a type expression M
*
DERIV_TYPE_SETMINUS_BUNION
  \mathit{Ty} \setminus (S \bunion  T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \binter  (\mathit{Ty} \setminus T) where \mathit{Ty} is a type expression M
*
DERIV_TYPE_SETMINUS_SETMINUS
  \mathit{Ty} \setminus (S \setminus T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \bunion  T where \mathit{Ty} is a type expression M
DISTRI_CPROD_BINTER
  S \cprod  (T \binter  U) \;\;\defi\;\;  (S \cprod  T) \binter  (S \cprod  U) M
DISTRI_CPROD_BUNION
  S \cprod  (T \bunion  U) \;\;\defi\;\;  (S \cprod  T) \bunion  (S \cprod  U) M
DISTRI_CPROD_SETMINUS
  S \cprod  (T \setminus U) \;\;\defi\;\;  (S \cprod  T) \setminus (S \cprod  U) M
*
DERIV_SUBSETEQ
  S \subseteq  T \;\;\defi\;\;  (\mathit{Ty} \setminus T) \subseteq  (\mathit{Ty} \setminus S) where \pow (\mathit{Ty}) is the type of S and T M
*
DERIV_EQUAL
  S = T \;\;\defi\;\;  S \subseteq  T \land  T \subseteq  S where \pow (\mathit{Ty}) is the type of S and T M
*
DERIV_SUBSETEQ_SETMINUS_L
  A \setminus B \subseteq  S \;\;\defi\;\;  A \subseteq  B \bunion  S M
*
DERIV_SUBSETEQ_SETMINUS_R
  S \subseteq  A \setminus B \;\;\defi\;\;  S \subseteq  A \land  S \binter  B = \emptyset M
*
DEF_PARTITION
  \operatorname{partition} (s, s_1, s_2, \ldots, s_n) \;\;\defi\;\; 
 		  	\begin{array}{ll}
		  		& s = s_1\bunion s_2\bunion\cdots\bunion s_n\\
				\land& s_1\binter s_2 = \emptyset\\
				\vdots\\
				\land& s_1\binter s_n = \emptyset\\
				\vdots\\
				\land& s_{n-1}\binter s_n = \emptyset
			\end{array} AM
*
SIMP_EMPTY_PARTITION
\operatorname{partition}(S)  \;\;\defi\;\;  S = \emptyset A
*
SIMP_SINGLE_PARTITION
\operatorname{partition}(S, T)  \;\;\defi\;\;  S = T A
*
DEF_EQUAL_CARD
\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S also works for k = \operatorname{card}(S) M
*
SIMP_EQUAL_CARD
\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T M