Empty Set Rewrite Rules - Revision history

imported>Josselin: Marked rules as implemented

2014-05-12T16:39:40Z

Marked rules as implemented

imported>Laurent: Generalize rules SIMP_BINTER_*

2013-05-24T13:46:53Z

Generalize rules SIMP_BINTER_*

← Older revision		Revision as of 13:46, 24 May 2013
Line 10:		Line 10:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \cdots \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \cdots \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SING_EQUAL_EMPTY}}\|\|<math> A \binter \{ a \} = \emptyset \;\;\defi\;\; \lnot\, a \in A </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SING_EQUAL_EMPTY}}\|\|<math>A\binter\cdots\binter\{a\}\binter\cdots\binter B = \emptyset \;\;\defi\;\; \lnot\, a \in A\binter\cdots\binter B</math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}\|\|<math> (A \setminus B) \binter C = \emptyset \;\;\defi\;\; (A \binter C) \setminus B = \emptyset</math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}\|\|<math>A\binter\cdots\binter(B\setminus C)\binter\cdots\binter D = \emptyset \;\;\defi\;\; (A\binter\cdots\binter B\binter\cdots\binter D) \setminus C = \emptyset</math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \cdots \land B = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \cdots \land B = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A

imported>Laurent: Change \ldots to \cdots for tall operators

2013-05-24T13:39:45Z

Change \ldots to \cdots for tall operators

imported>Laurent: Fix variants for equality with type

2013-05-24T13:36:35Z

Fix variants for equality with type

← Older revision		Revision as of 13:36, 24 May 2013
Line 3:		Line 3:
	Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].		Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].

	All rewrite rules that match the pattern <math>\textbf{P}=\emptyset</math> are also applicable to predicates of the form <math>\textbf{P}\subseteq\emptyset</math> and <math>\emptyset=\textbf{P}</math>, as these predicates are equivalent. All rewrite rules that match the pattern <math>\textbf{P}=\mathit{Ty}</math> are also applicable to predicates of the form <math>\~~textbf~~{P}\subseteq\~~mathit~~{Ty}</math> and <math>\mathit{Ty}=\textbf{P}</math>, as these predicates are equivalent.		All rewrite rules that match the pattern <math>\textbf{P}=\emptyset</math> are also applicable to predicates of the form <math>\textbf{P}\subseteq\emptyset</math> and <math>\emptyset=\textbf{P}</math>, as these predicates are equivalent. All rewrite rules that match the pattern <math>\textbf{P}=\mathit{Ty}</math> are also applicable to predicates of the form <math>\mathit{Ty}\subseteq\textbf{P}</math> and <math>\mathit{Ty}=\textbf{P}</math>, as these predicates are equivalent.

	{{RRHeader}}		{{RRHeader}}

imported>Josselin: Added rules SIMP_BINTER_SING_EQUAL_EMPTY, SIMP_BINTER_SETMINUS_EQUAL_EMPTY

2013-05-22T13:27:06Z

Added rules SIMP_BINTER_SING_EQUAL_EMPTY, SIMP_BINTER_SETMINUS_EQUAL_EMPTY

← Older revision		Revision as of 13:27, 22 May 2013
Line 10:		Line 10:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \ldots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \ldots \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \ldots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \ldots \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A
			{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SING_EQUAL_EMPTY}}\|\|<math> A \binter \{ a \} = \emptyset \;\;\defi\;\; \lnot\, a \in A </math>\|\| \|\| A
			{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}\|\|<math> (A \setminus B) \binter C = \emptyset \;\;\defi\;\; (A \binter C) \setminus B = \emptyset</math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \ldots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \ldots \land B = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \ldots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \ldots \land B = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A

imported>Josselin: Update introduction

2013-05-22T08:23:21Z

Update introduction

← Older revision		Revision as of 08:23, 22 May 2013
Line 3:		Line 3:
	Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].		Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].

	All rewrite rules that match the pattern <math>\textbf{P}=\emptyset</math> are also applicable to predicates of the form <math>\textbf{P}\subseteq\emptyset</math> and <math>\emptyset=\textbf{P}</math>, as these predicates are equivalent.		All rewrite rules that match the pattern <math>\textbf{P}=\emptyset</math> are also applicable to predicates of the form <math>\textbf{P}\subseteq\emptyset</math> and <math>\emptyset=\textbf{P}</math>, as these predicates are equivalent. All rewrite rules that match the pattern <math>\textbf{P}=\mathit{Ty}</math> are also applicable to predicates of the form <math>\textbf{P}\subseteq\mathit{Ty}</math> and <math>\mathit{Ty}=\textbf{P}</math>, as these predicates are equivalent.

	{{RRHeader}}		{{RRHeader}}

imported>Josselin: Removed rules SIMP_PRJ1_EQUAL_TYPE and SIMP_PRJ2_EQUAL_TYPE

2013-05-22T08:17:07Z

Removed rules SIMP_PRJ1_EQUAL_TYPE and SIMP_PRJ2_EQUAL_TYPE

← Older revision		Revision as of 08:17, 22 May 2013
Line 56:		Line 56:
	{{RRRow}}\|\|\|{{Rulename\|SIMP_ID_EQUAL_EMPTY}}\|\|<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_ID_EQUAL_EMPTY}}\|\|<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_EMPTY}}\|\|<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_EMPTY}}\|\|<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_TYPE}}\|\|<math> \prjone = \mathit{Ty} \;\;\defi\;\; \finite(\mathit{Ta}) \land \card(\mathit{Ta})=1 </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb} \cprod \mathit{Ta}</math> \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ2_EQUAL_EMPTY}}\|\|<math> \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ2_EQUAL_EMPTY}}\|\|<math> \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ2_EQUAL_TYPE}}\|\|<math> \prjtwo = \mathit{Ty} \;\;\defi\;\; \finite(\mathit{Tb}) \land \card(\mathit{Tb})=1 </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb} \cprod \mathit{Tb}</math> \|\| A
	\|}		\|}

imported>Josselin: Fixed rule SIMP_PPROD_EQUAL_TYPE (the condition did not typecheck)

2013-05-22T08:14:22Z

Fixed rule SIMP_PPROD_EQUAL_TYPE (the condition did not typecheck)

← Older revision		Revision as of 08:14, 22 May 2013
Line 53:		Line 53:
	{{RRRow}}\|\|\|{{Rulename\|SIMP_DPROD_EQUAL_TYPE}}\|\|<math> p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_DPROD_EQUAL_TYPE}}\|\|<math> p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PPROD_EQUAL_EMPTY}}\|\|<math> p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PPROD_EQUAL_EMPTY}}\|\|<math> p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PPROD_EQUAL_TYPE}}\|\|<math> p \pprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Tc} \cprod \mathit{Td} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>(\mathit{Ta} \cprod \mathit{Tb}) \cprod (\mathit{Tc} \cprod \mathit{Td})</math> \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PPROD_EQUAL_TYPE}}\|\|<math> p \pprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tc} \land q = \mathit{Tb} \cprod \mathit{Td} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>(\mathit{Ta} \cprod \mathit{Tb}) \cprod (\mathit{Tc} \cprod \mathit{Td})</math> \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_ID_EQUAL_EMPTY}}\|\|<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_ID_EQUAL_EMPTY}}\|\|<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_EMPTY}}\|\|<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_EMPTY}}\|\|<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A

imported>Josselin: Fixed side condition (SIMP_TYPE_EQUAL_RELDOMRAN)

2013-05-22T08:03:18Z

Fixed side condition (SIMP_TYPE_EQUAL_RELDOMRAN)

← Older revision		Revision as of 08:03, 22 May 2013
Line 31:		Line 31:
	{{RRRow}}\|\|\|{{Rulename\|SIMP_TYPE_EQUAL_REL}}\|\|<math> A \rel B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ta} \land B = \mathit{Tb} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_TYPE_EQUAL_REL}}\|\|<math> A \rel B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ta} \land B = \mathit{Tb} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</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_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_TYPE_EQUAL_RELDOMRAN}}\|\|<math> A \trel B = \mathit{Ty} \;\;\defi\;\; \bfalse </math>\|\| where <math>\mathit{Ty}</math> is a type expression, idem for operator <math>\srel, \strel, \tfun, \tinj, \tsur, \tbij</math> \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_TYPE_EQUAL_RELDOMRAN}}\|\|<math> A \trel B = \mathit{Ty} \;\;\defi\;\; \bfalse </math>\|\| where <math>\mathit{Ty}</math> is a type expression, idem for operator <math>\srel, \strel, \tfun, \tinj, \psur, \tsur, \tbij</math> \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_SREL_EQUAL_EMPTY}}\|\|<math> A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land \lnot\,B = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_SREL_EQUAL_EMPTY}}\|\|<math> A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land \lnot\,B = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_STREL_EQUAL_EMPTY}}\|\|<math> A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv \lnot\,B = \emptyset) </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_STREL_EQUAL_EMPTY}}\|\|<math> A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv \lnot\,B = \emptyset) </math>\|\| \|\| A

imported>Josselin: Renamed rule SIMP_TYPE_EQUAL_RELDOM into SIMP_TYPE_EQUAL_RELDOMRAN

2013-05-22T07:51:17Z

Renamed rule SIMP_TYPE_EQUAL_RELDOM into SIMP_TYPE_EQUAL_RELDOMRAN

← Older revision		Revision as of 07:51, 22 May 2013
Line 31:		Line 31:
	{{RRRow}}\|\|\|{{Rulename\|SIMP_TYPE_EQUAL_REL}}\|\|<math> A \rel B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ta} \land B = \mathit{Tb} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_TYPE_EQUAL_REL}}\|\|<math> A \rel B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ta} \land B = \mathit{Tb} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</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_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_TYPE_EQUAL_RELDOM~~}}\|\|<math> A \trel B = \mathit{Ty} \;\;\defi\;\; \bfalse </math>\|\| where <math>\mathit{Ty}</math> is a type expression, idem for operator <math>\srel, \strel, \tfun, \tinj, \tsur, \tbij</math> \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_TYPE_EQUAL_RELDOMRAN}}\|\|<math> A \trel B = \mathit{Ty} \;\;\defi\;\; \bfalse </math>\|\| where <math>\mathit{Ty}</math> is a type expression, idem for operator <math>\srel, \strel, \tfun, \tinj, \tsur, \tbij</math> \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_SREL_EQUAL_EMPTY}}\|\|<math> A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land \lnot\,B = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_SREL_EQUAL_EMPTY}}\|\|<math> A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land \lnot\,B = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_STREL_EQUAL_EMPTY}}\|\|<math> A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv \lnot\,B = \emptyset) </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_STREL_EQUAL_EMPTY}}\|\|<math> A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv \lnot\,B = \emptyset) </math>\|\| \|\| A

← Older revision		Revision as of 13:46, 24 May 2013
Line 10:		Line 10:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \cdots \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \cdots \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SING_EQUAL_EMPTY}}\|\|<math> A \binter \{ a \} = \emptyset \;\;\defi\;\; \lnot\, a \in A </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SING_EQUAL_EMPTY}}\|\|<math>A\binter\cdots\binter\{a\}\binter\cdots\binter B = \emptyset \;\;\defi\;\; \lnot\, a \in A\binter\cdots\binter B</math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}\|\|<math> (A \setminus B) \binter C = \emptyset \;\;\defi\;\; (A \binter C) \setminus B = \emptyset</math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}\|\|<math>A\binter\cdots\binter(B\setminus C)\binter\cdots\binter D = \emptyset \;\;\defi\;\; (A\binter\cdots\binter B\binter\cdots\binter D) \setminus C = \emptyset</math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \cdots \land B = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \cdots \land B = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A

← Older revision		Revision as of 13:27, 22 May 2013
Line 10:		Line 10:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \ldots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \ldots \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \ldots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \ldots \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A
			{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SING_EQUAL_EMPTY}}\|\|<math> A \binter \{ a \} = \emptyset \;\;\defi\;\; \lnot\, a \in A </math>\|\| \|\| A
			{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}\|\|<math> (A \setminus B) \binter C = \emptyset \;\;\defi\;\; (A \binter C) \setminus B = \emptyset</math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \ldots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \ldots \land B = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \ldots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \ldots \land B = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A

← Older revision		Revision as of 08:17, 22 May 2013
Line 56:		Line 56:
	{{RRRow}}\|\|\|{{Rulename\|SIMP_ID_EQUAL_EMPTY}}\|\|<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_ID_EQUAL_EMPTY}}\|\|<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_EMPTY}}\|\|<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_EMPTY}}\|\|<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_TYPE}}\|\|<math> \prjone = \mathit{Ty} \;\;\defi\;\; \finite(\mathit{Ta}) \land \card(\mathit{Ta})=1 </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb} \cprod \mathit{Ta}</math> \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ2_EQUAL_EMPTY}}\|\|<math> \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ2_EQUAL_EMPTY}}\|\|<math> \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ2_EQUAL_TYPE}}\|\|<math> \prjtwo = \mathit{Ty} \;\;\defi\;\; \finite(\mathit{Tb}) \land \card(\mathit{Tb})=1 </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb} \cprod \mathit{Tb}</math> \|\| A
	\|}		\|}

← Older revision		Revision as of 08:14, 22 May 2013
Line 53:		Line 53:
	{{RRRow}}\|\|\|{{Rulename\|SIMP_DPROD_EQUAL_TYPE}}\|\|<math> p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_DPROD_EQUAL_TYPE}}\|\|<math> p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PPROD_EQUAL_EMPTY}}\|\|<math> p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PPROD_EQUAL_EMPTY}}\|\|<math> p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PPROD_EQUAL_TYPE}}\|\|<math> p \pprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Tc} \cprod \mathit{Td} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>(\mathit{Ta} \cprod \mathit{Tb}) \cprod (\mathit{Tc} \cprod \mathit{Td})</math> \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PPROD_EQUAL_TYPE}}\|\|<math> p \pprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tc} \land q = \mathit{Tb} \cprod \mathit{Td} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>(\mathit{Ta} \cprod \mathit{Tb}) \cprod (\mathit{Tc} \cprod \mathit{Td})</math> \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_ID_EQUAL_EMPTY}}\|\|<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_ID_EQUAL_EMPTY}}\|\|<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_EMPTY}}\|\|<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_PRJ1_EQUAL_EMPTY}}\|\|<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A

← Older revision		Revision as of 13:39, 24 May 2013
Line 9:		Line 9:
	{{RRRow}}\|\|\|{{Rulename\|SIMP_SETENUM_EQUAL_EMPTY}}\|\|<math> \{ A, \ldots , B\} = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_SETENUM_EQUAL_EMPTY}}\|\|<math> \{ A, \ldots , B\} = \emptyset \;\;\defi\;\; \bfalse </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQUAL_COMPSET}}\|\|<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \~~ldots~~ \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \~~ldots~~ \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_EQUAL_TYPE}}\|\|<math> A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \cdots \land B = \mathit{Ty} </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SING_EQUAL_EMPTY}}\|\|<math> A \binter \{ a \} = \emptyset \;\;\defi\;\; \lnot\, a \in A </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SING_EQUAL_EMPTY}}\|\|<math> A \binter \{ a \} = \emptyset \;\;\defi\;\; \lnot\, a \in A </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}\|\|<math> (A \setminus B) \binter C = \emptyset \;\;\defi\;\; (A \binter C) \setminus B = \emptyset</math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}\|\|<math> (A \setminus B) \binter C = \emptyset \;\;\defi\;\; (A \binter C) \setminus B = \emptyset</math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \~~ldots~~ \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \~~ldots~~ \land B = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_BUNION_EQUAL_EMPTY}}\|\|<math> A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \cdots \land B = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_EMPTY}}\|\|<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_TYPE}}\|\|<math> A \setminus B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land B = \emptyset </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_SETMINUS_EQUAL_TYPE}}\|\|<math> A \setminus B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land B = \emptyset </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A
Line 51:		Line 51:
	{{RRRow}}\|\|\|{{Rulename\|SIMP_CONVERSE_EQUAL_TYPE}}\|\|<math> r^{-1} = \mathit{Ty} \;\;\defi\;\; r = \mathit{Ty}^{-1}</math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_CONVERSE_EQUAL_TYPE}}\|\|<math> r^{-1} = \mathit{Ty} \;\;\defi\;\; r = \mathit{Ty}^{-1}</math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_RELIMAGE_EQUAL_EMPTY}}\|\|<math> r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset</math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_RELIMAGE_EQUAL_EMPTY}}\|\|<math> r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset</math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_OVERL_EQUAL_EMPTY}}\|\|<math> r \ovl \~~ldots~~ \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \~~ldots~~ \land s = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_OVERL_EQUAL_EMPTY}}\|\|<math> r \ovl \cdots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \cdots \land s = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_DPROD_EQUAL_EMPTY}}\|\|<math> p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset </math>\|\| \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_DPROD_EQUAL_EMPTY}}\|\|<math> p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset </math>\|\| \|\| A
	{{RRRow}}\|\|\|{{Rulename\|SIMP_DPROD_EQUAL_TYPE}}\|\|<math> p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> \|\| A		{{RRRow}}\|\|\|{{Rulename\|SIMP_DPROD_EQUAL_TYPE}}\|\|<math> p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math>\|\| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> \|\| A