Relation Rewrite Rules

Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_Rules.

	Name	Rule	Side Condition	A/M
*	SIMP_DOM_SETENUM	$\dom (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ x, \ldots , y\}$		A
*	SIMP_DOM_CONVERSE	$\dom (r^{-1} ) \;\;\defi\;\; \ran (r)$		A
*	SIMP_RAN_SETENUM	$\ran (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ a, \ldots , b\}$		A
*	SIMP_RAN_CONVERSE	$\ran (r^{-1} ) \;\;\defi\;\; \dom (r)$		A
*	SIMP_SPECIAL_OVERL	$r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s$		A
	SIMP_MULTI_OVERL	$r_1 \ovl \cdots \ovl r_n \defi r_1 \ovl \cdots \ovl r_{i-1} \ovl r_{i+1} \ovl \cdots \ovl r_n$	there is a $j$ such that $1\leq i < j \leq n$ and $r_i$ and $r_j$ are syntactically equal.	A
*	SIMP_TYPE_OVERL_CPROD	$r\ovl\cdots\ovl\mathit{Ty}\ovl\cdots\ovl s \;\defi\;\; \mathit{Ty}\ovl\cdots\ovl s$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_SPECIAL_DOMRES_L	$\emptyset \domres r \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_DOMRES_R	$S \domres \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_DOMRES	$\mathit{Ty} \domres r \;\;\defi\;\; r$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_DOMRES_DOM	$\dom (r) \domres r \;\;\defi\;\; r$		A
*	SIMP_MULTI_DOMRES_RAN	$\ran (r) \domres r^{-1} \;\;\defi\;\; r^{-1}$		A
	SIMP_DOMRES_DOMRES_ID	$S \domres (T \domres \id) \;\;\defi\;\; (S \binter T) \domres \id$		A
	SIMP_DOMRES_DOMSUB_ID	$S \domres (T \domsub \id) \;\;\defi\;\; (S \setminus T) \domres \id$		A
*	SIMP_SPECIAL_RANRES_R	$r \ranres \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_RANRES_L	$\emptyset \ranres S \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_RANRES	$r \ranres \mathit{Ty} \;\;\defi\;\; r$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_RANRES_RAN	$r \ranres \ran (r) \;\;\defi\;\; r$		A
*	SIMP_MULTI_RANRES_DOM	$r^{-1} \ranres \dom (r) \;\;\defi\;\; r^{-1}$		A
	SIMP_RANRES_ID	$\id \ranres S \;\;\defi\;\; S \domres \id$		A
	SIMP_RANSUB_ID	$\id \ransub S \;\;\defi\;\; S \domsub \id$		A
	SIMP_RANRES_DOMRES_ID	$(S \domres \id) \ranres T \;\;\defi\;\; (S \binter T) \domres \id$		A
	SIMP_RANRES_DOMSUB_ID	$(S \domsub \id) \ranres T \;\;\defi\;\; (T \setminus S) \domres \id$		A
*	SIMP_SPECIAL_DOMSUB_L	$\emptyset \domsub r \;\;\defi\;\; r$		A
*	SIMP_SPECIAL_DOMSUB_R	$S \domsub \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_DOMSUB	$\mathit{Ty} \domsub r \;\;\defi\;\; \emptyset$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_DOMSUB_DOM	$\dom (r) \domsub r \;\;\defi\;\; \emptyset$		A
	SIMP_MULTI_DOMSUB_RAN	$\ran (r) \domsub r^{-1} \;\;\defi\;\; \emptyset$		A
	SIMP_DOMSUB_DOMRES_ID	$S \domsub (T \domres \id ) \;\;\defi\;\; (T \setminus S) \domres \id$		A
	SIMP_DOMSUB_DOMSUB_ID	$S \domsub (T \domsub \id ) \;\;\defi\;\; (S \bunion T) \domsub \id$		A
*	SIMP_SPECIAL_RANSUB_R	$r \ransub \emptyset \;\;\defi\;\; r$		A
*	SIMP_SPECIAL_RANSUB_L	$\emptyset \ransub S \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_RANSUB	$r \ransub \mathit{Ty} \;\;\defi\;\; \emptyset$	where $\mathit{Ty}$ is a type expression	A
	SIMP_MULTI_RANSUB_DOM	$r^{-1} \ransub \dom (r) \;\;\defi\;\; \emptyset$		A
*	SIMP_MULTI_RANSUB_RAN	$r \ransub \ran (r) \;\;\defi\;\; \emptyset$		A
	SIMP_RANSUB_DOMRES_ID	$(S \domres \id) \ransub T \;\;\defi\;\; (S \setminus T) \domres \id$		A
	SIMP_RANSUB_DOMSUB_ID	$(S \domsub \id) \ransub T \;\;\defi\;\; (S \bunion T) \domsub \id$		A
*	SIMP_SPECIAL_FCOMP	$r \fcomp \ldots \fcomp \emptyset \fcomp \ldots \fcomp s \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_FCOMP_ID	$r \fcomp \ldots \fcomp \id \fcomp \ldots \fcomp s \;\;\defi\;\; r \fcomp \ldots \fcomp s$		A
*	SIMP_TYPE_FCOMP_R	$r \fcomp \mathit{Ty} \;\;\defi\;\; \dom (r) \cprod \mathit{Tb}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_TYPE_FCOMP_L	$\mathit{Ty} \fcomp r \;\;\defi\;\; \mathit{Ta} \cprod \ran (r)$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
	SIMP_FCOMP_ID	$r \fcomp \ldots \fcomp S \domres \id \fcomp T \domres \id \fcomp \ldots s \;\;\defi\;\; r \fcomp \ldots \fcomp (S \binter T) \domres \id \fcomp \ldots \fcomp s$		A
*	SIMP_SPECIAL_BCOMP	$r \bcomp \ldots \bcomp \emptyset \bcomp \ldots \bcomp s \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_BCOMP_ID	$r \bcomp \ldots \bcomp \id \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp s$		A
*	SIMP_TYPE_BCOMP_L	$\mathit{Ty} \bcomp r \;\;\defi\;\; \dom (r) \cprod \mathit{Tb}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_TYPE_BCOMP_R	$r \bcomp \mathit{Ty} \;\;\defi\;\; \mathit{Ta} \cprod \ran (r)$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
	SIMP_BCOMP_ID	$r \bcomp \ldots \bcomp S \domres \id \bcomp T \domres \id \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp (S \binter T) \domres \id \bcomp \ldots \bcomp s$		A
*	SIMP_SPECIAL_DPROD_R	$r \dprod \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_DPROD_L	$\emptyset \dprod r \;\;\defi\;\; \emptyset$		A
*	SIMP_DPROD_CPROD	$(\mathit{S} \cprod \mathit{T}) \dprod (\mathit{U} \cprod \mathit{V}) \;\;\defi\;\; \mathit{S} \binter \mathit{U} \cprod (\mathit{T} \cprod \mathit{V})$		A
*	SIMP_SPECIAL_PPROD_R	$r \pprod \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_PPROD_L	$\emptyset \pprod r \;\;\defi\;\; \emptyset$		A
*	SIMP_PPROD_CPROD	$(\mathit{S} \cprod \mathit{T}) \pprod (\mathit{U} \cprod \mathit{V}) \;\;\defi\;\; (\mathit{S} \cprod \mathit{U}) \cprod (\mathit{T} \cprod \mathit{V})$		A
*	SIMP_SPECIAL_RELIMAGE_R	$r[\emptyset ] \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_RELIMAGE_L	$\emptyset [S] \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_RELIMAGE	$r[Ty] \;\;\defi\;\; \ran (r)$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_RELIMAGE_DOM	$r[\dom (r)] \;\;\defi\;\; \ran (r)$		A
	SIMP_RELIMAGE_ID	$\id[T] \;\;\defi\;\; T$		A
	SIMP_RELIMAGE_DOMRES_ID	$(S \domres \id)[T] \;\;\defi\;\; S \binter T$		A
	SIMP_RELIMAGE_DOMSUB_ID	$(S \domsub \id)[T] \;\;\defi\;\; T \setminus S$		A
*	SIMP_MULTI_RELIMAGE_CPROD_SING	$(\{ E\} \cprod S)[\{ E\} ] \;\;\defi\;\; S$	where $E$ is a single expression	A
*	SIMP_MULTI_RELIMAGE_SING_MAPSTO	$\{ E \mapsto F\} [\{ E\} ] \;\;\defi\;\; \{ F\}$	where $E$ is a single expression	A
*	SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB	$(r \ransub S)^{-1} [S] \;\;\defi\;\; \emptyset$		A
*	SIMP_MULTI_RELIMAGE_CONVERSE_RANRES	$(r \ranres S)^{-1} [S] \;\;\defi\;\; r^{-1} [S]$		A
*	SIMP_RELIMAGE_CONVERSE_DOMSUB	$(S \domsub r)^{-1} [T] \;\;\defi\;\; r^{-1} [T] \setminus S$		A
	DERIV_RELIMAGE_RANSUB	$(r \ransub S)[T] \;\;\defi\;\; r[T] \setminus S$		M
	DERIV_RELIMAGE_RANRES	$(r \ranres S)[T] \;\;\defi\;\; r[T] \binter S$		M
*	SIMP_MULTI_RELIMAGE_DOMSUB	$(S \domsub r)[S] \;\;\defi\;\; \emptyset$		A
	DERIV_RELIMAGE_DOMSUB	$(S \domsub r)[T] \;\;\defi\;\; r[T \setminus S]$		M
	DERIV_RELIMAGE_DOMRES	$(S \domres r)[T] \;\;\defi\;\; r[S \binter T]$		M
*	SIMP_SPECIAL_CONVERSE	$\emptyset ^{-1} \;\;\defi\;\; \emptyset$		A
*	SIMP_CONVERSE_ID	$\id^{-1} \;\;\defi\;\; \id$		A
*	SIMP_CONVERSE_CPROD	$(\mathit{S} \cprod \mathit{T})^{-1} \;\;\defi\;\; \mathit{T} \cprod \mathit{S}$		A
*	SIMP_CONVERSE_SETENUM	$\{ x \mapsto a, \ldots , y \mapsto b\} ^{-1} \;\;\defi\;\; \{ a \mapsto x, \ldots , b \mapsto y\}$		A
*	SIMP_CONVERSE_COMPSET	$\{ X \qdot P \mid x\mapsto y\} ^{-1} \;\;\defi\;\; \{ X \qdot P \mid y\mapsto x\}$		A
*	SIMP_DOM_ID	$\dom (\id) \;\;\defi\;\; S$	where $\id$ has type $\pow(S \cprod S)$	A
*	SIMP_RAN_ID	$\ran (\id) \;\;\defi\;\; S$	where $\id$ has type $\pow(S \cprod S)$	A
*	SIMP_FCOMP_ID_L	$(S \domres \id) \fcomp r \;\;\defi\;\; S \domres r$		A
*	SIMP_FCOMP_ID_R	$r \fcomp (S \domres \id) \;\;\defi\;\; r \ranres S$		A
*	SIMP_SPECIAL_REL_R	$S \rel \emptyset \;\;\defi\;\; \{ \emptyset \}$	idem for operators $\srel \pfun \pinj \psur$	A
*	SIMP_SPECIAL_REL_L	$\emptyset \rel S \;\;\defi\;\; \{ \emptyset \}$	idem for operators $\trel \pfun \tfun \pinj \tinj$	A
*	SIMP_SPECIAL_EQUAL_REL	$A \rel B = \emptyset \;\;\defi\;\; \bfalse$	idem for operators $\pfun \pinj$	A
*	SIMP_SPECIAL_EQUAL_RELDOM	$A \trel B = \emptyset \;\;\defi\;\; \lnot\, A = \emptyset \land B = \emptyset$	idem for operators $\tfun \tinj \tsur \tbij$	A
*	SIMP_FUNIMAGE_PRJ1	$\prjone (E \mapsto F) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_PRJ2	$\prjtwo (E \mapsto F) \;\;\defi\;\; F$		A
*	SIMP_DOM_PRJ1	$\dom (\prjone) \;\;\defi\;\; S \cprod T$	where $\prjone$ has type $\pow(S \cprod T \cprod S)$	A
*	SIMP_DOM_PRJ2	$\dom (\prjtwo) \;\;\defi\;\; S \cprod T$	where $\prjtwo$ has type $\pow(S \cprod T \cprod T)$	A
*	SIMP_RAN_PRJ1	$\ran (\prjone) \;\;\defi\;\; S$	where $\prjone$ has type $\pow(S \cprod T \cprod S)$	A
*	SIMP_RAN_PRJ2	$\ran (\prjtwo) \;\;\defi\;\; T$	where $\prjtwo$ has type $\pow(S \cprod T \cprod T)$	A
*	SIMP_FUNIMAGE_LAMBDA	$(\lambda x \qdot P(x) \mid E(x))(y) \;\;\defi\;\; E(y)$		A
*	SIMP_DOM_LAMBDA	$\dom(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid E\}$		A
*	SIMP_RAN_LAMBDA	$\ran(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid F\}$		A
*	SIMP_IN_FUNIMAGE	$E\mapsto F(E)\in F \;\;\defi\;\; \btrue$		A
*	SIMP_IN_FUNIMAGE_CONVERSE_L	$F^{-1}(E)\mapsto E\in F \;\;\defi\;\; \btrue$		A
*	SIMP_IN_FUNIMAGE_CONVERSE_R	$F(E)\mapsto E\in F^{-1} \;\;\defi\;\; \btrue$		A
*	SIMP_MULTI_FUNIMAGE_SETENUM_LL	$\{ A \mapsto E, \ldots , B \mapsto E\} (x) \;\;\defi\;\; E$		A
*	SIMP_MULTI_FUNIMAGE_SETENUM_LR	$\{ E, \ldots , x \mapsto y, \ldots , F\} (x) \;\;\defi\;\; y$		A
*	SIMP_MULTI_FUNIMAGE_OVERL_SETENUM	$(r \ovl \ldots \ovl \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y$		A
*	SIMP_MULTI_FUNIMAGE_BUNION_SETENUM	$(r \bunion \ldots \bunion \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y$		A
*	SIMP_FUNIMAGE_CPROD	$(S \cprod \{ F\} )(x) \;\;\defi\;\; F$		A
*	SIMP_FUNIMAGE_ID	$\id (x) \;\;\defi\;\; x$		A
*	SIMP_FUNIMAGE_FUNIMAGE_CONVERSE	$f(f^{-1} (E)) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_CONVERSE_FUNIMAGE	$f^{-1}(f(E)) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM	$\{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_DOMRES	$(E \domres F)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
*	SIMP_FUNIMAGE_DOMSUB	$(E \domsub F)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
*	SIMP_FUNIMAGE_RANRES	$(F\ranres E)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
*	SIMP_FUNIMAGE_RANSUB	$(F \ransub E)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
*	SIMP_FUNIMAGE_SETMINUS	$(F \setminus E)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
	DEF_BCOMP	$r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r$		M
	DERIV_ID_SING	$\{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\}$	where $E$ is a single expression	M
*	SIMP_SPECIAL_DOM	$\dom (\emptyset ) \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_RAN	$\ran (\emptyset ) \;\;\defi\;\; \emptyset$		A
*	SIMP_CONVERSE_CONVERSE	$r^{-1-1} \;\;\defi\;\; r$		A
*	DERIV_RELIMAGE_FCOMP	$(p \fcomp q)[s] \;\;\defi\;\; q[p[s]]$		M
*	DERIV_FCOMP_DOMRES	$(s \domres p) \fcomp q \;\;\defi\;\; s \domres (p \fcomp q)$		M
*	DERIV_FCOMP_DOMSUB	$(s \domsub p) \fcomp q \;\;\defi\;\; s \domsub (p \fcomp q)$		M
*	DERIV_FCOMP_RANRES	$p \fcomp (q \ranres s) \;\;\defi\;\; (p \fcomp q) \ranres s$		M
*	DERIV_FCOMP_RANSUB	$p \fcomp (q \ransub s) \;\;\defi\;\; (p \fcomp q) \ransub s$		M
*	SIMP_SPECIAL_EQUAL_RELDOMRAN	$\emptyset \strel \emptyset \;\;\defi\;\; \{ \emptyset \}$	idem for operators $\tsur \tbij$	A
*	SIMP_TYPE_DOM	$\dom (\mathit{Ty}) \;\;\defi\;\; \mathit{Ta}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_TYPE_RAN	$\ran (\mathit{Ty}) \;\;\defi\;\; \mathit{Tb}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_MULTI_DOM_CPROD	$\dom (E \cprod E) \;\;\defi\;\; E$		A
*	SIMP_MULTI_RAN_CPROD	$\ran (E \cprod E) \;\;\defi\;\; E$		A
*	DEF_IN_DOM	$E \in \dom (r) \;\;\defi\;\; \exists y \qdot E \mapsto y \in r$		M
*	DEF_IN_RAN	$F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r$		M
*	DEF_IN_CONVERSE	$E \mapsto F \in r^{-1} \;\;\defi\;\; F \mapsto E \in r$		M
*	DEF_IN_DOMRES	$E \mapsto F \in S \domres r \;\;\defi\;\; E \in S \land E \mapsto F \in r$		M
*	DEF_IN_RANRES	$E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \in T$		M
*	DEF_IN_DOMSUB	$E \mapsto F \in S \domsub r \;\;\defi\;\; E \notin S \land E \mapsto F \in r$		M
*	DEF_IN_RANSUB	$E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \notin T$		M
*	DEF_IN_RELIMAGE	$F \in r[w] \;\;\defi\;\; \exists x \qdot x \in w \land x \mapsto F \in r$		M
*	DEF_IN_FCOMP	$E \mapsto F \in (p \fcomp q) \;\;\defi\;\; \exists x \qdot E \mapsto x \in p \land x \mapsto F \in q$		M
*	DEF_OVERL	$p \ovl q \;\;\defi\;\; (\dom (q) \domsub p) \bunion q$		M
*	DEF_IN_ID	$E \mapsto F \in \id \;\;\defi\;\; E = F$		M
*	DEF_IN_DPROD	$E \mapsto (F \mapsto G) \in p \dprod q \;\;\defi\;\; E \mapsto F \in p \land E \mapsto G \in q$		M
*	DEF_IN_PPROD	$(E \mapsto G) \mapsto (F \mapsto H) \in p \pprod q \;\;\defi\;\; E \mapsto F \in p \land G \mapsto H \in q$		M
*	DEF_IN_REL	$r \in S \rel T \;\;\defi\;\; r\subseteq S\cprod T$		M
*	DEF_IN_RELDOM	$r \in S \trel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S$		M
*	DEF_IN_RELRAN	$r \in S \srel T \;\;\defi\;\; r \in S \rel T \land \ran (r) = T$		M
*	DEF_IN_RELDOMRAN	$r \in S \strel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S \land \ran (r) = T$		M
*	DEF_IN_FCT	$\begin{array}{rcl} f \in S \pfun T & \defi & f \in S \rel T \\ & \land & (\forall x,y,z \qdot x \mapsto y \in f \land x \mapsto z \in f \limp y = z) \\ \end{array}$		M
*	DEF_IN_TFCT	$f \in S \tfun T \;\;\defi\;\; f \in S \pfun T \land \dom (f) = S$		M
*	DEF_IN_INJ	$f \in S \pinj T \;\;\defi\;\; f \in S \pfun T \land f^{-1} \in T \pfun S$		M
*	DEF_IN_TINJ	$f \in S \tinj T \;\;\defi\;\; f \in S \pinj T \land \dom (f) = S$		M
*	DEF_IN_SURJ	$f \in S \psur T \;\;\defi\;\; f \in S \pfun T \land \ran (f) = T$		M
*	DEF_IN_TSURJ	$f \in S \tsur T \;\;\defi\;\; f \in S \psur T \land \dom (f) = S$		M
*	DEF_IN_BIJ	$f \in S \tbij T \;\;\defi\;\; f \in S \tinj T \land \ran (f) = T$		M
	DISTRI_BCOMP_BUNION	$r \bcomp (s \bunion t) \;\;\defi\;\; (r \bcomp s) \bunion (r \bcomp t)$		M
*	DISTRI_FCOMP_BUNION_R	$p \fcomp (q \bunion r) \;\;\defi\;\; (p \fcomp q) \bunion (p \fcomp r)$		M
*	DISTRI_FCOMP_BUNION_L	$(q \bunion r) \fcomp p \;\;\defi\;\; (q \fcomp p) \bunion (r \fcomp p)$		M
	DISTRI_DPROD_BUNION	$r \dprod (s \bunion t) \;\;\defi\;\; (r \dprod s) \bunion (r \dprod t)$		M
	DISTRI_DPROD_BINTER	$r \dprod (s \binter t) \;\;\defi\;\; (r \dprod s) \binter (r \dprod t)$		M
	DISTRI_DPROD_SETMINUS	$r \dprod (s \setminus t) \;\;\defi\;\; (r \dprod s) \setminus (r \dprod t)$		M
	DISTRI_DPROD_OVERL	$r \dprod (s \ovl t) \;\;\defi\;\; (r \dprod s) \ovl (r \dprod t)$		M
	DISTRI_PPROD_BUNION	$r \pprod (s \bunion t) \;\;\defi\;\; (r \pprod s) \bunion (r \pprod t)$		M
	DISTRI_PPROD_BINTER	$r \pprod (s \binter t) \;\;\defi\;\; (r \pprod s) \binter (r \pprod t)$		M
	DISTRI_PPROD_SETMINUS	$r \pprod (s \setminus t) \;\;\defi\;\; (r \pprod s) \setminus (r \pprod t)$		M
	DISTRI_PPROD_OVERL	$r \pprod (s \ovl t) \;\;\defi\;\; (r \pprod s) \ovl (r \pprod t)$		M
	DISTRI_OVERL_BUNION_L	$(p \bunion q) \ovl r \;\;\defi\;\; (p \ovl r) \bunion (q \ovl r)$		M
	DISTRI_OVERL_BINTER_L	$(p \binter q) \ovl r \;\;\defi\;\; (p \ovl r) \binter (q \ovl r)$		M
*	DISTRI_DOMRES_BUNION_R	$s \domres (p \bunion q) \;\;\defi\;\; (s \domres p) \bunion (s \domres q)$		M
*	DISTRI_DOMRES_BUNION_L	$(s \bunion t) \domres r \;\;\defi\;\; (s \domres r) \bunion (t \domres r)$		M
*	DISTRI_DOMRES_BINTER_R	$s \domres (p \binter q) \;\;\defi\;\; (s \domres p) \binter (s \domres q)$		M
*	DISTRI_DOMRES_BINTER_L	$(s \binter t) \domres r \;\;\defi\;\; (s \domres r) \binter (t \domres r)$		M
	DISTRI_DOMRES_SETMINUS_R	$s \domres (p \setminus q) \;\;\defi\;\; (s \domres p) \setminus (s \domres q)$		M
	DISTRI_DOMRES_SETMINUS_L	$(s \setminus t) \domres r \;\;\defi\;\; (s \domres r) \setminus (t \domres r)$		M
	DISTRI_DOMRES_DPROD	$s \domres (p \dprod q) \;\;\defi\;\; (s \domres p) \dprod (s \domres q)$		M
	DISTRI_DOMRES_OVERL	$s \domres (r \ovl q) \;\;\defi\;\; (s \domres r) \ovl (s \domres q)$		M
*	DISTRI_DOMSUB_BUNION_R	$s \domsub (p \bunion q) \;\;\defi\;\; (s \domsub p) \bunion (s \domsub q)$		M
*	DISTRI_DOMSUB_BUNION_L	$(s \bunion t) \domsub r \;\;\defi\;\; (s \domsub r) \binter (t \domsub r)$		M
*	DISTRI_DOMSUB_BINTER_R	$s \domsub (p \binter q) \;\;\defi\;\; (s \domsub p) \binter (s \domsub q)$		M
*	DISTRI_DOMSUB_BINTER_L	$(s \binter t) \domsub r \;\;\defi\;\; (s \domsub r) \bunion (t \domsub r)$		M
	DISTRI_DOMSUB_DPROD	$A \domsub (r \dprod s) \;\;\defi\;\; (A \domsub r) \dprod (A \domsub s)$		M
	DISTRI_DOMSUB_OVERL	$A \domsub (r \ovl s) \;\;\defi\;\; (A \domsub r) \ovl (A \domsub s)$		M
*	DISTRI_RANRES_BUNION_R	$r \ranres (s \bunion t) \;\;\defi\;\; (r \ranres s) \bunion (r \ranres t)$		M
*	DISTRI_RANRES_BUNION_L	$(p \bunion q) \ranres s \;\;\defi\;\; (p \ranres s) \bunion (q \ranres s)$		M
*	DISTRI_RANRES_BINTER_R	$r \ranres (s \binter t) \;\;\defi\;\; (r \ranres s) \binter (r \ranres t)$		M
*	DISTRI_RANRES_BINTER_L	$(p \binter q) \ranres s \;\;\defi\;\; (p \ranres s) \binter (q \ranres s)$		M
	DISTRI_RANRES_SETMINUS_R	$r \ranres (s \setminus t) \;\;\defi\;\; (r \ranres s) \setminus (r \ranres t)$		M
	DISTRI_RANRES_SETMINUS_L	$(p \setminus q) \ranres s \;\;\defi\;\; (p \ranres s) \setminus (q \ranres s)$		M
*	DISTRI_RANSUB_BUNION_R	$r \ransub (s\bunion t) \;\;\defi\;\; (r \ransub s) \binter (r \ransub t)$		M
*	DISTRI_RANSUB_BUNION_L	$(p \bunion q) \ransub s \;\;\defi\;\; (p \ransub s) \bunion (q \ransub s)$		M
*	DISTRI_RANSUB_BINTER_R	$r \ransub (s \binter t) \;\;\defi\;\; (r \ransub s) \bunion (r \ransub t)$		M
*	DISTRI_RANSUB_BINTER_L	$(p \binter q) \ransub s \;\;\defi\;\; (p \ransub s) \binter (q \ransub s)$		M
*	DISTRI_CONVERSE_BUNION	$(p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1}$		M
	DISTRI_CONVERSE_BINTER	$(p \binter q)^{-1} \;\;\defi\;\; p^{-1} \binter q^{-1}$		M
	DISTRI_CONVERSE_SETMINUS	$(r \setminus s)^{-1} \;\;\defi\;\; r^{-1} \setminus s^{-1}$		M
	DISTRI_CONVERSE_BCOMP	$(r \bcomp s)^{-1} \;\;\defi\;\; (s^{-1} \bcomp r^{-1} )$		M
	DISTRI_CONVERSE_FCOMP	$(p \fcomp q)^{-1} \;\;\defi\;\; (q^{-1} \fcomp p^{-1} )$		M
	DISTRI_CONVERSE_PPROD	$(r \pprod s)^{-1} \;\;\defi\;\; r^{-1} \pprod s^{-1}$		M
	DISTRI_CONVERSE_DOMRES	$(s \domres r)^{-1} \;\;\defi\;\; r^{-1} \ranres s$		M
	DISTRI_CONVERSE_DOMSUB	$(s \domsub r)^{-1} \;\;\defi\;\; r^{-1} \ransub s$		M
	DISTRI_CONVERSE_RANRES	$(r \ranres s)^{-1} \;\;\defi\;\; s \domres r^{-1}$		M
	DISTRI_CONVERSE_RANSUB	$(r \ransub s)^{-1} \;\;\defi\;\; s \domsub r^{-1}$		M
*	DISTRI_DOM_BUNION	$\dom (r \bunion s) \;\;\defi\;\; \dom (r) \bunion \dom (s)$		M
*	DISTRI_RAN_BUNION	$\ran (r \bunion s) \;\;\defi\;\; \ran (r) \bunion \ran (s)$		M
*	DISTRI_RELIMAGE_BUNION_R	$r[S \bunion T] \;\;\defi\;\; r[S] \bunion r[T]$		M
*	DISTRI_RELIMAGE_BUNION_L	$(p \bunion q)[S] \;\;\defi\;\; p[S] \bunion q[S]$		M
*	DERIV_DOM_TOTALREL	$\dom (r) \;\;\defi\;\; E$	with hypothesis $r \in E \ \mathit{op}\ F$, where $\mathit{op}$ is one of $\trel, \strel, \tfun, \tinj, \tsur, \tbij$	M
	DERIV_RAN_SURJREL	$\ran (r) \;\;\defi\;\; F$	with hypothesis $r \in E \ \mathit{op}\ F$, where $\mathit{op}$ is one of $\srel,\strel, \psur, \tsur, \tbij$	M
b	prjone-functional	$\prjone \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue$	where $\mathit{op}$ is one of $\pfun, \tfun, \trel$	A
b	prjtwo-functional	$\prjtwo \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue$	where $\mathit{op}$ is one of $\pfun, \tfun, \trel$	A
	prj-expand	$x \;\;\defi\;\; \prjone(x) \mapsto \prjtwo(x)$		M