Set 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_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	$E \in \{ x \qdot P(x) \mid x \} \;\;\defi\;\; P(E)$		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 (S)) \;\;\defi\;\; \finite (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_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
*	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
	SUBST_FORALL_AND	$\begin{array}{ll} \forall x, \ldots, y, \ldots, z \qdot P(y) \land \ldots \land y = E \land \ldots \land Q(y) \limp R(y) \;\;\defi\;\;\\ \forall x, \ldots, \ldots,z \qdot P(E) \land \ldots \land \ldots \land Q(E) \limp R(E) \end{array}$		A