Relation Rewrite Rules - Revision history

Guillaume: Rules DEF_EQUAL_FUN_IMAGE and SIMP_SPECIAL_IN_*ID have been implemented in Rodin 3.9

2024-06-03T15:13:55Z

Rules DEF_EQUAL_FUN_IMAGE and SIMP_SPECIAL_IN_*ID have been implemented in Rodin 3.9

← Older revision		Revision as of 15:13, 3 June 2024
Line 111:		Line 111:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|\|\|{{Rulename\|DEF_EQUAL_FUNIMAGE}}\|\|<math> f(x) = y \;\;\defi\;\; x \mapsto y \in f </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_EQUAL_FUNIMAGE}}\|\|<math> f(x) = y \;\;\defi\;\; x \mapsto y \in f </math>\|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M
	{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M		{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M
Line 220:		Line 220:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_ID}}\|\|<math> E \mapsto E \in \id \;\;\defi\;\; \btrue</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_IN_ID}}\|\|<math> E \mapsto E \in \id \;\;\defi\;\; \btrue</math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_ID}}\|\|<math>E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_ID}}\|\|<math>E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse</math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_DOMRES_ID}}\|\|<math>E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_IN_DOMRES_ID}}\|\|<math>E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S</math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID}}\|\|<math>E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID}}\|\|<math>E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r</math> \|\| \|\| A

	\|}		\|}

Guillaume: Add four rules related to set membership and identity

2024-03-08T16:17:24Z

Add four rules related to set membership and identity

← Older revision		Revision as of 16:17, 8 March 2024
Line 220:		Line 220:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_ID}}\|\|<math> E \mapsto E \in \id \;\;\defi\;\; \btrue</math> \|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_ID}}\|\|<math>E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse</math> \|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_DOMRES_ID}}\|\|<math>E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S</math> \|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID}}\|\|<math>E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r</math> \|\| \|\| A

	\|}		\|}

Guillaume: Add rule DEF_EQUAL_FUNIMAGE

2024-02-05T14:31:19Z

Add rule DEF_EQUAL_FUNIMAGE

← Older revision		Revision as of 14:31, 5 February 2024
Line 111:		Line 111:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
			{{RRRow}}\|\|\|{{Rulename\|DEF_EQUAL_FUNIMAGE}}\|\|<math> f(x) = y \;\;\defi\;\; x \mapsto y \in f </math>\|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M
	{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M		{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M

Guillaume: Rule DEF_BCOMP has been implemented in Rodin 3.8

2023-04-06T09:32:25Z

Rule DEF_BCOMP has been implemented in Rodin 3.8

← Older revision		Revision as of 09:32, 6 April 2023
Line 111:		Line 111:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M
	{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M		{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_DOM}}\|\|<math> \dom (\emptyset ) \;\;\defi\;\; \emptyset </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_DOM}}\|\|<math> \dom (\emptyset ) \;\;\defi\;\; \emptyset </math>\|\| \|\| A

imported>Laurent: mark rules as implemented

2014-02-19T16:45:39Z

mark rules as implemented

← Older revision		Revision as of 16:45, 19 February 2014
Line 209:		Line 209:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_DOM_TOTALREL}}\|\|<math> \dom (r) \;\;\defi\;\; E </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DERIV_DOM_TOTALREL}}\|\|<math> \dom (r) \;\;\defi\;\; E </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> \|\| M
	{{RRRow}}\| \|\|{{Rulename\|DERIV_RAN_SURJREL}}\|\|<math> \ran (r) \;\;\defi\;\; F </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> \|\| M		{{RRRow}}\| \|\|{{Rulename\|DERIV_RAN_SURJREL}}\|\|<math> \ran (r) \;\;\defi\;\; F </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> \|\| M
	{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ1_SURJ}}\|\|<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_PRJ1_SURJ}}\|\|<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ2_SURJ}}\|\|<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_PRJ2_SURJ}}\|\|<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DERIV_ID_BIJ}}\|\|<math>\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}</math> is a type and <math>\mathit{op}</math> is any arrow \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_ID_BIJ}}\|\|<math>\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}</math> is a type and <math>\mathit{op}</math> is any arrow \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_MAPSTO_PRJ1_PRJ2}}\|\|<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MAPSTO_PRJ1_PRJ2}}\|\|<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DERIV_EXPAND_PRJS}}\|\|<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> \|\| \|\| M		{{RRRow}}\| \|\|{{Rulename\|DERIV_EXPAND_PRJS}}\|\|<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> \|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_DOM_SUCC}}\|\|<math>\dom(\usucc) \;\;\defi\;\; \intg</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_DOM_SUCC}}\|\|<math>\dom(\usucc) \;\;\defi\;\; \intg</math> \|\| \|\| A

imported>Laurent: Add rule about properties of identity.

2014-02-18T09:30:15Z

Add rule about properties of identity.

← Older revision		Revision as of 09:30, 18 February 2014
Line 211:		Line 211:
	{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ1_SURJ}}\|\|<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A		{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ1_SURJ}}\|\|<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ2_SURJ}}\|\|<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A		{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ2_SURJ}}\|\|<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A
			{{RRRow}}\| \|\|{{Rulename\|DERIV_ID_BIJ}}\|\|<math>\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}</math> is a type and <math>\mathit{op}</math> is any arrow \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_MAPSTO_PRJ1_PRJ2}}\|\|<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> \|\| \|\| A		{{RRRow}}\| \|\|{{Rulename\|SIMP_MAPSTO_PRJ1_PRJ2}}\|\|<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DERIV_EXPAND_PRJS}}\|\|<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> \|\| \|\| M		{{RRRow}}\| \|\|{{Rulename\|DERIV_EXPAND_PRJS}}\|\|<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> \|\| \|\| M

imported>Laurent: Refactor rules about projections

2014-02-18T09:25:55Z

Refactor rules about projections

← Older revision		Revision as of 09:25, 18 February 2014
Line 209:		Line 209:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_DOM_TOTALREL}}\|\|<math> \dom (r) \;\;\defi\;\; E </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DERIV_DOM_TOTALREL}}\|\|<math> \dom (r) \;\;\defi\;\; E </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> \|\| M
	{{RRRow}}\| \|\|{{Rulename\|DERIV_RAN_SURJREL}}\|\|<math> \ran (r) \;\;\defi\;\; F </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> \|\| M		{{RRRow}}\| \|\|{{Rulename\|DERIV_RAN_SURJREL}}\|\|<math> \ran (r) \;\;\defi\;\; F </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> \|\| M
	{{RRRow}}\|b\|\|{{Rulename\|~~prjone-functional~~}}\|\|<math> \prjone \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{op}</math> is one of <math> \pfun, \tfun, \~~trel~~ </math> \|\| A		{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ1_SURJ}}\|\|<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A
	{{RRRow}}\|b\|\|{{Rulename\|~~prjtwo-functional~~}}\|\|<math> \prjtwo \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{op}</math> is one of <math> \pfun, \tfun, \~~trel~~ </math> \|\| A		{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ2_SURJ}}\|\|<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A
	{{RRRow}}\|\|\|{{Rulename\|~~prj-expand~~}}\|\|<math> x \;\;\defi\;\; \prjone(x) \mapsto \prjtwo(x) </math> \|\| \|\| M		{{RRRow}}\| \|\|{{Rulename\|SIMP_MAPSTO_PRJ1_PRJ2}}\|\|<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> \|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|DERIV_EXPAND_PRJS}}\|\|<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> \|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_DOM_SUCC}}\|\|<math>\dom(\usucc) \;\;\defi\;\; \intg</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_DOM_SUCC}}\|\|<math>\dom(\usucc) \;\;\defi\;\; \intg</math> \|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_RAN_SUCC}}\|\|<math>\ran(\usucc) \;\;\defi\;\; \intg</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_RAN_SUCC}}\|\|<math>\ran(\usucc) \;\;\defi\;\; \intg</math> \|\| \|\| A

imported>Josselin: Removed rules SIMP_SPECIAL_EQUAL_REL and SIMP_SPECIAL_EQUAL_RELDOM (moved to Empty Set Rewrite Rules)

2013-05-02T15:23:48Z

Removed rules SIMP_SPECIAL_EQUAL_REL and SIMP_SPECIAL_EQUAL_RELDOM (moved to Empty Set Rewrite Rules)

← Older revision		Revision as of 15:23, 2 May 2013
Line 85:		Line 85:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_REL_R}}\|\|<math> S \rel \emptyset \;\;\defi\;\; \{ \emptyset \} </math>\|\| idem for operators <math>\srel \pfun \pinj \psur</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_REL_R}}\|\|<math> S \rel \emptyset \;\;\defi\;\; \{ \emptyset \} </math>\|\| idem for operators <math>\srel \pfun \pinj \psur</math> \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_REL_L}}\|\|<math> \emptyset \rel S \;\;\defi\;\; \{ \emptyset \} </math>\|\| idem for operators <math>\trel \pfun \tfun \pinj \tinj</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_REL_L}}\|\|<math> \emptyset \rel S \;\;\defi\;\; \{ \emptyset \} </math>\|\| idem for operators <math>\trel \pfun \tfun \pinj \tinj</math> \|\| A
	~~{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_REL}}\|\|<math> A \rel B = \emptyset \;\;\defi\;\; \bfalse </math>\|\| idem for operators <math>\pfun \pinj</math> \|\| A~~
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_RELDOM}}\|\|<math> A \trel B = \emptyset \;\;\defi\;\; \lnot\, A = \emptyset \land B = \emptyset </math>\|\| idem for operator <math>\tfun</math> \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_PRJ1}}\|\|<math> \prjone (E \mapsto F) \;\;\defi\;\; E </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_PRJ1}}\|\|<math> \prjone (E \mapsto F) \;\;\defi\;\; E </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_PRJ2}}\|\|<math> \prjtwo (E \mapsto F) \;\;\defi\;\; F </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_PRJ2}}\|\|<math> \prjtwo (E \mapsto F) \;\;\defi\;\; F </math>\|\| \|\| A

imported>Laurent: FIx incorrect rule SIMP_SPECIAL_EQUAL_RELDOM (see bug #661)

2013-04-26T13:33:28Z

FIx incorrect rule SIMP_SPECIAL_EQUAL_RELDOM (see bug #661)

← Older revision		Revision as of 13:33, 26 April 2013
Line 86:		Line 86:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_REL_L}}\|\|<math> \emptyset \rel S \;\;\defi\;\; \{ \emptyset \} </math>\|\| idem for operators <math>\trel \pfun \tfun \pinj \tinj</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_REL_L}}\|\|<math> \emptyset \rel S \;\;\defi\;\; \{ \emptyset \} </math>\|\| idem for operators <math>\trel \pfun \tfun \pinj \tinj</math> \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_REL}}\|\|<math> A \rel B = \emptyset \;\;\defi\;\; \bfalse </math>\|\| idem for operators <math>\pfun \pinj</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_REL}}\|\|<math> A \rel B = \emptyset \;\;\defi\;\; \bfalse </math>\|\| idem for operators <math>\pfun \pinj</math> \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_RELDOM}}\|\|<math> A \trel B = \emptyset \;\;\defi\;\; \lnot\, A = \emptyset \land B = \emptyset </math>\|\| idem for ~~operators~~ <math>\tfun ~~\tinj \tsur \tbij~~</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_RELDOM}}\|\|<math> A \trel B = \emptyset \;\;\defi\;\; \lnot\, A = \emptyset \land B = \emptyset </math>\|\| idem for operator <math>\tfun</math> \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_PRJ1}}\|\|<math> \prjone (E \mapsto F) \;\;\defi\;\; E </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_PRJ1}}\|\|<math> \prjone (E \mapsto F) \;\;\defi\;\; E </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_PRJ2}}\|\|<math> \prjtwo (E \mapsto F) \;\;\defi\;\; F </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_PRJ2}}\|\|<math> \prjtwo (E \mapsto F) \;\;\defi\;\; F </math>\|\| \|\| A

imported>Billaude: The four last rules already exist, but were not implemented. Instead of being manual, they are automatic.

2011-09-30T12:48:42Z

The four last rules already exist, but were not implemented. Instead of being manual, they are automatic.

← Older revision		Revision as of 12:48, 30 September 2011
Line 129:		Line 129:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_DOM_CPROD}}\|\|<math> \dom (E \cprod E) \;\;\defi\;\; E </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_DOM_CPROD}}\|\|<math> \dom (E \cprod E) \;\;\defi\;\; E </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_RAN_CPROD}}\|\|<math> \ran (E \cprod E) \;\;\defi\;\; E </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_RAN_CPROD}}\|\|<math> \ran (E \cprod E) \;\;\defi\;\; E </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_MULTI_DOM_DOMRES}}\|\|<math>\dom(A\domres f) \;\;\defi\;\; \dom(f)\binter A</math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_DOM_DOMRES}}\|\|<math>\dom(A\domres f) \;\;\defi\;\; \dom(f)\binter A</math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_MULTI_DOM_DOMSUB}}\|\|<math>\dom(A\domsub f) \;\;\defi\;\; \dom(f)\setminus A</math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_DOM_DOMSUB}}\|\|<math>\dom(A\domsub f) \;\;\defi\;\; \dom(f)\setminus A</math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_MULTI_RAN_RANRES}}\|\|<math>\ran(f\ranres A) \;\;\defi\;\; \ran(f)\binter A</math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_RAN_RANRES}}\|\|<math>\ran(f\ranres A) \;\;\defi\;\; \ran(f)\binter A</math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_MULTI_RAN_RANSUB}}\|\|<math>\ran(f\ransub A) \;\;\defi\;\; \ran(f)\setminus A</math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_RAN_RANSUB}}\|\|<math>\ran(f\ransub A) \;\;\defi\;\; \ran(f)\setminus A</math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_DOM}}\|\|<math> E \in \dom (r) \;\;\defi\;\; \exists y \qdot E \mapsto y \in r </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_DOM}}\|\|<math> E \in \dom (r) \;\;\defi\;\; \exists y \qdot E \mapsto y \in r </math>\|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_RAN}}\|\|<math> F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_RAN}}\|\|<math> F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r </math>\|\| \|\| M
Line 219:		Line 219:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A
	~~{{RRRow}}\|*\|\|{{Rulename\|DERIV_DOM_DOMRES}}\|\|<math> \dom(A\domres f)\;\;\defi\;\; \dom(f)\binter A</math> \|\| \|\| A~~
	~~{{RRRow}}\|*\|\|{{Rulename\|DERIV_DOM_DOMSUB}}\|\|<math> \dom(A\domsub f)\;\;\defi\;\; \dom(f)\setminus A</math> \|\| \|\| A~~
	~~{{RRRow}}\|*\|\|{{Rulename\|DERIV_RAN_RANRES}}\|\|<math> \ran(f\ranres A)\;\;\defi\;\; \ran(f)\binter A</math> \|\| \|\| A~~
	~~{{RRRow}}\|*\|\|{{Rulename\|DERIV_RAN_RANSUB}}\|\|<math> \ran(f\ransub A)\;\;\defi\;\; \ran(f)\setminus A</math> \|\| \|\| A~~

	\|}		\|}

← Older revision		Revision as of 15:13, 3 June 2024
Line 111:		Line 111:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|\|\|{{Rulename\|DEF_EQUAL_FUNIMAGE}}\|\|<math> f(x) = y \;\;\defi\;\; x \mapsto y \in f </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_EQUAL_FUNIMAGE}}\|\|<math> f(x) = y \;\;\defi\;\; x \mapsto y \in f </math>\|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M
	{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M		{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M
Line 220:		Line 220:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_ID}}\|\|<math> E \mapsto E \in \id \;\;\defi\;\; \btrue</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_IN_ID}}\|\|<math> E \mapsto E \in \id \;\;\defi\;\; \btrue</math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_ID}}\|\|<math>E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_ID}}\|\|<math>E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse</math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_DOMRES_ID}}\|\|<math>E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_IN_DOMRES_ID}}\|\|<math>E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S</math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID}}\|\|<math>E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID}}\|\|<math>E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r</math> \|\| \|\| A

	\|}		\|}

← Older revision		Revision as of 16:17, 8 March 2024
Line 220:		Line 220:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_MULTI_IN_SETMINUS}}\|\|<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> \|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DEF_PRED}}\|\|<math> \upred\;\;\defi\;\; \usucc^{-1}</math> \|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_ID}}\|\|<math> E \mapsto E \in \id \;\;\defi\;\; \btrue</math> \|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_ID}}\|\|<math>E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse</math> \|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_DOMRES_ID}}\|\|<math>E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S</math> \|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID}}\|\|<math>E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r</math> \|\| \|\| A

	\|}		\|}

← Older revision		Revision as of 14:31, 5 February 2024
Line 111:		Line 111:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
			{{RRRow}}\|\|\|{{Rulename\|DEF_EQUAL_FUNIMAGE}}\|\|<math> f(x) = y \;\;\defi\;\; x \mapsto y \in f </math>\|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M
	{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M		{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M

← Older revision		Revision as of 09:32, 6 April 2023
Line 111:		Line 111:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_RANSUB}}\|\|<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FUNIMAGE_SETMINUS}}\|\|<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> \|\| with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. \|\| AM
	{{RRRow}}\|\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_BCOMP}}\|\|<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>\|\| \|\| M
	{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M		{{RRRow}}\|\|\|{{Rulename\|DERIV_ID_SING}}\|\|<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>\|\| where <math>E</math> is a single expression \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_DOM}}\|\|<math> \dom (\emptyset ) \;\;\defi\;\; \emptyset </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_DOM}}\|\|<math> \dom (\emptyset ) \;\;\defi\;\; \emptyset </math>\|\| \|\| A

← Older revision		Revision as of 16:45, 19 February 2014
Line 209:		Line 209:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_DOM_TOTALREL}}\|\|<math> \dom (r) \;\;\defi\;\; E </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DERIV_DOM_TOTALREL}}\|\|<math> \dom (r) \;\;\defi\;\; E </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> \|\| M
	{{RRRow}}\| \|\|{{Rulename\|DERIV_RAN_SURJREL}}\|\|<math> \ran (r) \;\;\defi\;\; F </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> \|\| M		{{RRRow}}\| \|\|{{Rulename\|DERIV_RAN_SURJREL}}\|\|<math> \ran (r) \;\;\defi\;\; F </math> \|\| with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> \|\| M
	{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ1_SURJ}}\|\|<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_PRJ1_SURJ}}\|\|<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DERIV_PRJ2_SURJ}}\|\|<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_PRJ2_SURJ}}\|\|<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DERIV_ID_BIJ}}\|\|<math>\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}</math> is a type and <math>\mathit{op}</math> is any arrow \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_ID_BIJ}}\|\|<math>\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue </math> \|\| where <math>\mathit{Ty}</math> is a type and <math>\mathit{op}</math> is any arrow \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_MAPSTO_PRJ1_PRJ2}}\|\|<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MAPSTO_PRJ1_PRJ2}}\|\|<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> \|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DERIV_EXPAND_PRJS}}\|\|<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> \|\| \|\| M		{{RRRow}}\| \|\|{{Rulename\|DERIV_EXPAND_PRJS}}\|\|<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> \|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_DOM_SUCC}}\|\|<math>\dom(\usucc) \;\;\defi\;\; \intg</math> \|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_DOM_SUCC}}\|\|<math>\dom(\usucc) \;\;\defi\;\; \intg</math> \|\| \|\| A