Set Rewrite Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Nicolas
m updated rule SIMP_FINITE_ID to math V2
imported>Tommy
m removed * on unimplemented rules
Line 2: Line 2:
{{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 13:
{{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_OR}}||<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_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_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_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
Line 34: Line 34:
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_EQUAL_TRUE_R}}||<math>  \lnot\, (E = \True ) \;\;\defi\;\;  (E = \False ) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_EQUAL_TRUE_R}}||<math>  \lnot\, (E = \True ) \;\;\defi\;\;  (E = \False ) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_EQUAL_TRUE_L}}||<math>  \lnot\, (\True  = E) \;\;\defi\;\;  (\False  = E) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_EQUAL_TRUE_L}}||<math>  \lnot\, (\True  = E) \;\;\defi\;\;  (\False  = E) </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_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>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FORALL}}||<math>  \forall \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \forall z \qdot  P(z) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_EXISTS}}||<math>  \exists \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \exists z \qdot  P(z) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_EXISTS}}||<math>  \exists \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \exists z \qdot  P(z) </math>||  ||  A
Line 43: Line 43:
{{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
Line 51: Line 51:
{{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>||  ||  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>||  ||  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>||  ||  M
{{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 60:
{{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 70:
{{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_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_TYPE_KINTER}}||<math>  \inter (\mathit{Ty}) \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  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 \qdot  x = E \mid  x \}  \;\;\defi\;\;  \{ E\} </math>|| where <math>x</math> non free in <math>E</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_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  x \}  \;\;\defi\;\;  \mathit{Ty} </math>|| where the type od <math>x</math> is <math>\mathit{Ty}</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_COMPSET_L}}||<math>  \{  x \qdot  P(x) \mid  E \}  \subseteq  S \;\;\defi\;\;  \forall x\qdot  P(x) \limp  E \in  S </math>|| where <math>x</math> non free in <math>S</math> ||  A
{{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_COMPSET_L}}||<math>  \{  x \qdot  P(x) \mid  E \}  \subseteq  S \;\;\defi\;\;  \forall x\qdot  P(x) \limp  E \in  S </math>|| where <math>x</math> non free in <math>S</math> ||  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_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>||  ||  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>||  ||  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>x, S, \{  x \qdot  P(x) \mid  x \}</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_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_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_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 n\in\nat\land 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
Line 104: Line 104:
{{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
{{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
{{RRRow}}|*||{{Rulename|SIMP_FINITE_SETMINUS}}||<math>  \finite (S \setminus T) \;\;\defi\;\;  \finite (S) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_SETMINUS}}||<math>  \finite (S \setminus T) \;\;\defi\;\;  \finite (S) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_DOMRES}}||<math>  \finite (S \domres  r)  \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_DOMRES}}||<math>  \finite (S \domres  r)  \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_RANRES}}||<math>  \finite (r \ranres  S)  \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_RANRES}}||<math>  \finite (r \ranres  S)  \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_DOMSUB}}||<math>  \finite (S \domsub  r) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_DOMSUB}}||<math>  \finite (S \domsub  r) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_RANSUB}}||<math>  \finite (r \ransub  S) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_RANSUB}}||<math>  \finite (r \ransub  S) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_RELIMAGE}}||<math>  \finite (r[S]) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_RELIMAGE}}||<math>  \finite (r[S]) \;\;\defi\;\;  \finite (r) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_CPROD}}||<math>  \finite (S \cprod  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_CPROD}}||<math>  \finite (S \cprod  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_OVERL}}||<math>  \finite (r \ovl  s)  \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_OVERL}}||<math>  \finite (r \ovl  s)  \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_REL}}||<math>  \finite (S \rel  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_REL}}||<math>  \finite (S \rel  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_FCOMP}}||<math>  \finite (r \fcomp s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_FCOMP}}||<math>  \finite (r \fcomp s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_BCOMP}}||<math>  \finite (r \bcomp  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_BCOMP}}||<math>  \finite (r \bcomp  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_DPROD}}||<math>  \finite (r \dprod  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_DPROD}}||<math>  \finite (r \dprod  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PPROD}}||<math>  \finite (r \pprod  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_PPROD}}||<math>  \finite (r \pprod  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_FINITE_COMPSET}}||<math>  \finite (\{ x \qdot  x \in  S \land  \ldots  \land  P \mid  x\} ) \;\;\defi\;\;  \finite (S) </math>|| where <math>x</math> non free in <math>S</math> ||  M
{{RRRow}}|||{{Rulename|SIMP_FINITE_COMPSET}}||<math>  \finite (\{ x \qdot  x \in  S \land  \ldots  \land  P \mid  x\} ) \;\;\defi\;\;  \finite (S) </math>|| where <math>x</math> non free in <math>S</math> ||  M
{{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_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_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_NATURAL}}||<math>  \finite (\nat ) \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_FINITE_NATURAL1}}||<math>  \finite (\natn ) \;\;\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_INTEGER}}||<math>  \finite (\intg ) \;\;\defi\;\;  \bfalse </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_LAMBDA}}||<math>  \finite (\lambda x \qdot  P \mid  E) \;\;\defi\;\;  \finite (\{ x \qdot  P \mid  x\} ) </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_TYPE_EQUAL_EMPTY}}||<math> \mathit{Ty} = \emptyset  \;\;\defi\;\;  \bfalse </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_TYPE_IN}}||<math>  t \in  \mathit{Ty} \;\;\defi\;\;  \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
Line 140: Line 140:
{{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\;\;  S \neq  \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|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 171: Line 171:
{{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
{{RRRow}}|*||{{Rulename|DISTRI_BINTER_BUNION}}||<math>  S \binter  (T \bunion  U) \;\;\defi\;\;  (S \binter  T) \bunion  (S \binter  U) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_BINTER_BUNION}}||<math>  S \binter  (T \bunion  U) \;\;\defi\;\;  (S \binter  T) \bunion  (S \binter  U) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_BINTER_SETMINUS}}||<math>  S \binter  (T \setminus U) \;\;\defi\;\;  (S \binter  T) \setminus (S \binter  U) </math>||  ||  M
{{RRRow}}|||{{Rulename|DISTRI_BINTER_SETMINUS}}||<math>  S \binter  (T \setminus U) \;\;\defi\;\;  (S \binter  T) \setminus (S \binter  U) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_SETMINUS_BUNION}}||<math>  S \setminus (T \bunion  U) \;\;\defi\;\;  S \setminus T \setminus U </math>||  ||  M
{{RRRow}}|||{{Rulename|DISTRI_SETMINUS_BUNION}}||<math>  S \setminus (T \bunion  U) \;\;\defi\;\;  S \setminus T \setminus U </math>||  ||  M
{{RRRow}}|*||{{Rulename|DERIV_TYPE_SETMINUS_BINTER}}||<math>  \mathit{Ty} \setminus (S \binter  T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \bunion  (\mathit{Ty} \setminus T) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  M
{{RRRow}}|*||{{Rulename|DERIV_TYPE_SETMINUS_BINTER}}||<math>  \mathit{Ty} \setminus (S \binter  T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \bunion  (\mathit{Ty} \setminus T) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  M
{{RRRow}}|*||{{Rulename|DERIV_TYPE_SETMINUS_BUNION}}||<math>  \mathit{Ty} \setminus (S \bunion  T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \binter  (\mathit{Ty} \setminus T) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  M
{{RRRow}}|*||{{Rulename|DERIV_TYPE_SETMINUS_BUNION}}||<math>  \mathit{Ty} \setminus (S \bunion  T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \binter  (\mathit{Ty} \setminus T) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  M
{{RRRow}}|*||{{Rulename|DERIV_TYPE_SETMINUS_SETMINUS}}||<math>  \mathit{Ty} \setminus (S \setminus T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \bunion  T </math>|| where <math>\mathit{Ty}</math> is a type expression ||  M
{{RRRow}}|*||{{Rulename|DERIV_TYPE_SETMINUS_SETMINUS}}||<math>  \mathit{Ty} \setminus (S \setminus T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \bunion  T </math>|| where <math>\mathit{Ty}</math> is a type expression ||  M
{{RRRow}}|*||{{Rulename|DISTRI_CPROD_BINTER}}||<math>  S \cprod  (T \binter  U) \;\;\defi\;\;  (S \cprod  T) \binter  (S \cprod  U) </math>||  ||  M
{{RRRow}}|||{{Rulename|DISTRI_CPROD_BINTER}}||<math>  S \cprod  (T \binter  U) \;\;\defi\;\;  (S \cprod  T) \binter  (S \cprod  U) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_CPROD_BUNION}}||<math>  S \cprod  (T \bunion  U) \;\;\defi\;\;  (S \cprod  T) \bunion  (S \cprod  U) </math>||  ||  M
{{RRRow}}|||{{Rulename|DISTRI_CPROD_BUNION}}||<math>  S \cprod  (T \bunion  U) \;\;\defi\;\;  (S \cprod  T) \bunion  (S \cprod  U) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_CPROD_SETMINUS}}||<math>  S \cprod  (T \setminus U) \;\;\defi\;\;  (S \cprod  T) \setminus (S \cprod  U) </math>||  ||  M
{{RRRow}}|||{{Rulename|DISTRI_CPROD_SETMINUS}}||<math>  S \cprod  (T \setminus U) \;\;\defi\;\;  (S \cprod  T) \setminus (S \cprod  U) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ}}||<math>  S \subseteq  T \;\;\defi\;\;  (\mathit{Ty} \setminus T) \subseteq  (\mathit{Ty} \setminus S) </math>|| where <math>\pow (\mathit{Ty})</math> is the type of <math>S</math> and <math>T</math> ||  M
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ}}||<math>  S \subseteq  T \;\;\defi\;\;  (\mathit{Ty} \setminus T) \subseteq  (\mathit{Ty} \setminus S) </math>|| where <math>\pow (\mathit{Ty})</math> is the type of <math>S</math> and <math>T</math> ||  M
{{RRRow}}|*||{{Rulename|DERIV_EQUAL}}||<math>  S = T \;\;\defi\;\;  S \subseteq  T \land  T \subseteq  S </math>|| where <math>\pow (\mathit{Ty})</math> is the type of <math>S</math> and <math>T</math> ||  M
{{RRRow}}|*||{{Rulename|DERIV_EQUAL}}||<math>  S = T \;\;\defi\;\;  S \subseteq  T \land  T \subseteq  S </math>|| where <math>\pow (\mathit{Ty})</math> is the type of <math>S</math> and <math>T</math> ||  M

Revision as of 10:17, 21 December 2009

  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_OR
 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_MULTI_EQV_NOT_NOT
 \lnot\, P \leqv \lnot\, P \;\;\defi\;\; \btrue 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 A
*
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_FORALL
 \forall \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \forall z \qdot P(z) A
*
SIMP_EXISTS
 \exists \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \exists z \qdot P(z) 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 M
*
DERIV_SUBSETEQ_BINTER
 S \subseteq A \binter \ldots \binter B \;\;\defi\;\; S \subseteq A \land \ldots \land S \subseteq B M
SIMP_SUBSET_BUNION
 A \bunion \ldots \bunion B \subset S \;\;\defi\;\; A \subset S \land \ldots \land B \subset S A
SIMP_SUBSET_BINTER
 S \subset A \binter \ldots \binter B \;\;\defi\;\; S \subset A \land \ldots \land S \subset 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_TYPE_KUNION
 \union (\mathit{Ty}) \;\;\defi\;\; \mathit{Ta} where \mathit{Ty} is a type expression and \mathit{Ty} = \pow (\mathit{Ta}) 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_TYPE_KINTER
 \inter (\mathit{Ty}) \;\;\defi\;\; \emptyset where \mathit{Ty} is a type expression 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 \qdot x = E \mid x \} \;\;\defi\;\; \{ E\} where x non free in E A
SIMP_COMPSET_IN
 \{ x \qdot x \in S \mid x \} \;\;\defi\;\; 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 x \} \;\;\defi\;\; \mathit{Ty} where the type od x is \mathit{Ty} A
SIMP_SUBSETEQ_COMPSET_L
 \{ x \qdot P(x) \mid E \} \subseteq S \;\;\defi\;\; \forall x\qdot P(x) \limp E \in S where x non free in S A
SIMP_SPECIAL_EQUAL_COMPSET
 \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) 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 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 x, S, \{ x \qdot P(x) \mid x \} A
SIMP_SPECIAL_OVERL
 r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s A
SIMP_MULTI_OVERL
 \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} A
SIMP_TYPE_OVERL_CPROD
 r \ovl (\mathit{Ty} \cprod S) \;\;\defi\;\; (\mathit{Ty} \cprod S) where \mathit{Ty} is a type expression 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 n\in\nat\land 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_BINTER_L
 \finite (S \binter T) \;\;\defi\;\; \finite (S) M
SIMP_FINITE_BINTER_R
 \finite (S \binter T) \;\;\defi\;\; \finite (T) M
SIMP_FINITE_SETMINUS
 \finite (S \setminus T) \;\;\defi\;\; \finite (S) M
SIMP_FINITE_DOMRES
 \finite (S \domres r) \;\;\defi\;\; \finite (r) M
SIMP_FINITE_RANRES
 \finite (r \ranres S) \;\;\defi\;\; \finite (r) M
SIMP_FINITE_DOMSUB
 \finite (S \domsub r) \;\;\defi\;\; \finite (r) M
SIMP_FINITE_RANSUB
 \finite (r \ransub S) \;\;\defi\;\; \finite (r) M
SIMP_FINITE_RELIMAGE
 \finite (r[S]) \;\;\defi\;\; \finite (r) M
SIMP_FINITE_CPROD
 \finite (S \cprod T) \;\;\defi\;\; \finite (S) \land \finite (T) M
SIMP_FINITE_OVERL
 \finite (r \ovl s) \;\;\defi\;\; \finite (r) \land \finite (s) M
*
SIMP_FINITE_REL
 \finite (S \rel T) \;\;\defi\;\; \finite (S) \land \finite (T) M
SIMP_FINITE_FCOMP
 \finite (r \fcomp s) \;\;\defi\;\; \finite (r) \land \finite (s) M
SIMP_FINITE_BCOMP
 \finite (r \bcomp s) \;\;\defi\;\; \finite (r) \land \finite (s) M
SIMP_FINITE_DPROD
 \finite (r \dprod s) \;\;\defi\;\; \finite (r) \land \finite (s) M
SIMP_FINITE_PPROD
 \finite (r \pprod s) \;\;\defi\;\; \finite (r) \land \finite (s) M
SIMP_FINITE_COMPSET
 \finite (\{ x \qdot x \in S \land \ldots \land P \mid x\} ) \;\;\defi\;\; \finite (S) where x non free in S M
SIMP_FINITE_RAN
 \finite (\ran (r)) \;\;\defi\;\; \finite (r) M
SIMP_FINITE_DOM
 \finite (\dom (r)) \;\;\defi\;\; \finite (r) M
SIMP_FINITE_QUNION
 \finite (\Union x \qdot P \mid E) \;\;\defi\;\; \forall x \qdot P \limp \finite (E) M
SIMP_FINITE_QINTER
 \finite (\Inter x \qdot P \mid E) \;\;\defi\;\; \exists x \qdot P \land \finite (E) M
SIMP_FINITE_ID
 \finite (\id) \;\;\defi\;\; \finite (S) where \id has type \pow(S \cprod S) 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_LAMBDA
 \finite (\lambda x \qdot P \mid E) \;\;\defi\;\; \finite (\{ x \qdot P \mid x\} ) A
*
SIMP_TYPE_EQUAL_EMPTY
 \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse where \mathit{Ty} is a type expression A
*
SIMP_TYPE_IN
 t \in \mathit{Ty} \;\;\defi\;\; \btrue where \mathit{Ty} is a type expression A
SIMP_SPECIAL_FORALL_BTRUE
 \forall x \qdot \btrue \;\;\defi\;\; \btrue A
SIMP_SPECIAL_FORALL_BFALSE
 \forall x \qdot \bfalse \;\;\defi\;\; \bfalse A
SIMP_SPECIAL_EXISTS_BTRUE
 \exists x \qdot \btrue \;\;\defi\;\; \btrue A
SIMP_SPECIAL_EXISTS_BFALSE
 \exists x \qdot \bfalse \;\;\defi\;\; \bfalse 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\;\; S \neq \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
*
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_SPECIAL_NOT_EQUAL
 \lnot\, S = \emptyset \;\;\defi\;\; \exists x \qdot x \in S M
*
DEF_IN_MAPSTO
 E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T M
*
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 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 M
*
DEF_IN_QUNION
 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 M
*
DEF_IN_KINTER
 E \in \inter (S) \;\;\defi\;\; \forall s \qdot s \in S \limp E \in s M
*
DEF_IN_QINTER
 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 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
Retrieved from ‘https://wiki.event-b.org/index.php?title=Set_Rewrite_Rules&oldid=9328’