# Relation Rewrite Rules

Name Rule Side Condition A/M
*
SIMP_DOM_COMPSET
$\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_COMPSET
$\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 (\mathit{Ty} \cprod S) \;\;\defi\;\; (\mathit{Ty} \cprod 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_ID
$S \domres (T \domres \id) \;\;\defi\;\; (S \binter 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
$(S \domres \id) \ranres T \;\;\defi\;\; (S \binter T) \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_DOMSUB_ID
$S \domsub (T \domres \id ) \;\;\defi\;\; (T \setminus S) \domres \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_RAN
$r \ransub \ran (r) \;\;\defi\;\; \emptyset$ A
SIMP_RANSUB_ID
$(S \domres \id) \ransub T \;\;\defi\;\; (S \setminus T) \domres \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_TYPE_DPROD
$\mathit{Ta} \dprod \mathit{Tb} \;\;\defi\;\; Tc \cprod (Td \cprod Te)$ where $\mathit{Ta}$ and $\mathit{Tb}$ are type expressions and $\mathit{Ta} = \mathit{Tc} \cprod \mathit{Td}$ and $\mathit{Tb} = \mathit{Tc} \cprod \mathit{Te}$ A
SIMP_SPECIAL_PPROD_R
$r \pprod \emptyset \;\;\defi\;\; \emptyset$ A
SIMP_SPECIAL_PPROD_L
$\emptyset \pprod r \;\;\defi\;\; \emptyset$ A
SIMP_TYPE_PPROD
$\mathit{Ta} \pprod \mathit{Tb} \;\;\defi\;\; (Tc \cprod Te) \cprod (Td \cprod Tf)$ where $\mathit{Ta}$ and $\mathit{Tb}$ are type expressions and $\mathit{Ta} = \mathit{Tc} \cprod \mathit{Td}$ and $\mathit{Tb} = \mathit{Te} \cprod \mathit{Tf}$ 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_TYPE_RELIMAGE_ID
$\id[T] \;\;\defi\;\; T$ A
SIMP_RELIMAGE_ID
$(S \domres \id)[T] \;\;\defi\;\; S \binter T$ 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_TYPE_CONVERSE
$\mathit{Ty}^{-1} \;\;\defi\;\; \mathit{Tb} \cprod \mathit{Ta}$ where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$ 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_SPECIAL_ID
$\emptyset \domres \id \;\;\defi\;\; \emptyset$ 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_SPECIAL_PRJ1
$\emptyset \domres \prjone \;\;\defi\;\; \emptyset$ A
SIMP_SPECIAL_PRJ2
$\emptyset \domres \prjtwo \;\;\defi\;\; \emptyset$ 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_SPECIAL_LAMBDA
$(\lambda x \qdot \bfalse \mid E) \;\;\defi\;\; \emptyset$ A
SIMP_FUNIMAGE_LAMBDA
$(\lambda x \qdot P(x) \mid E(x))(y) \;\;\defi\;\; E(y)$ A
SIMP_DOM_LAMBDA
$\dom (\lambda x \qdot P \mid E) \;\;\defi\;\; \{ x\qdot P \mid x\}$ A
SIMP_RAN_LAMBDA
$\ran (\lambda x \qdot P \mid E) \;\;\defi\;\; \{ x\qdot P \mid E\}$ A
SIMP_MULTI_FUNIMAGE_SETENUM_LL
$\{ A \mapsto E, \ldots , B \mapsto E\} (x) \;\;\defi\;\; E$ A
SIMP_MULTI_FUNIMAGE_SETENUM_LR
$\{ A \mapsto E, \ldots , x \mapsto y, \ldots , B \mapsto F\} (x) \;\;\defi\;\; y$ A
*
SIMP_MULTI_FUNIMAGE_OVERL_SETENUM
$(r \ovl \ldots \ovl \{ A \mapsto E, \ldots , x \mapsto y, \ldots , B \mapsto F\} )(x) \;\;\defi\;\; y$ A
SIMP_MULTI_FUNIMAGE_BUNION_SETENUM
$(r \bunion \ldots \bunion \{ A \mapsto E, \ldots , x \mapsto y, \ldots , B \mapsto 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} \rel \mathit{Tb}$ A
SIMP_TYPE_RAN
$\ran (\mathit{Ty}) \;\;\defi\;\; \mathit{Tb}$ where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \rel \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_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
*
DISTRI_DOM_BUNION
$\dom (p \bunion q) \;\;\defi\;\; \dom (p) \bunion \dom (q)$ M
*
DISTRI_RAN_BUNION
$\ran (p \bunion q) \;\;\defi\;\; \ran (p) \bunion \ran (q)$ 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
prjone-total
$z \in \dom (\prjone) \;\;\defi\;\; \btrue$ A
prjtwo-total
$z \in \dom (\prjtwo) \;\;\defi\;\; \btrue$ A
prjone-functional
$\prjone \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue$ where \mathit{op} is one of $\pfun, \tfun, \trel$ A
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