Set Rewrite Rules - Revision history

Guillaume: Rules SIMP_{EMPTY,SINGLE}_PARTITION were implemented

2023-04-13T14:33:15Z

Rules SIMP_{EMPTY,SINGLE}_PARTITION were implemented

← Older revision		Revision as of 14:33, 13 April 2023
Line 203:		Line 203:
	\land& s_{n-1}\binter s_n = \emptyset		\land& s_{n-1}\binter s_n = \emptyset
	\end{array}</math>\|\| \|\| AM		\end{array}</math>\|\| \|\| AM
	{{RRRow}}\| \|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DEF_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>\|\| also works for <math>k = \operatorname{card}(S)</math> \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>\|\| also works for <math>k = \operatorname{card}(S)</math> \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|SIMP_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>\|\| \|\| M

Guillaume: Rules DEF_EQUAL_CARD and SIMP_EQUAL_CARD are implemented as of Rodin 3.8

2023-04-06T09:31:27Z

Rules DEF_EQUAL_CARD and SIMP_EQUAL_CARD are implemented as of Rodin 3.8

← Older revision		Revision as of 09:31, 6 April 2023
Line 205:		Line 205:
	{{RRRow}}\| \|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A		{{RRRow}}\| \|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A		{{RRRow}}\| \|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DEF_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>\|\| also works for <math>k = \operatorname{card}(S)</math> \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>\|\| also works for <math>k = \operatorname{card}(S)</math> \|\| M
	{{RRRow}}\| \|\|{{Rulename\|SIMP_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|SIMP_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>\|\| \|\| M
	\|}		\|}

Guillaume: Add rules for cardinal equality

2022-11-25T15:18:09Z

Add rules for cardinal equality

← Older revision		Revision as of 15:18, 25 November 2022
Line 205:		Line 205:
	{{RRRow}}\| \|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A		{{RRRow}}\| \|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A		{{RRRow}}\| \|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|DEF_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>\|\| also works for <math>k = \operatorname{card}(S)</math> \|\| M
			{{RRRow}}\| \|\|{{Rulename\|SIMP_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>\|\| \|\| M
	\|}		\|}

Guillaume: Move rewrite rules for KUNION and QUNION to the commented-out section for disabled rules, as they are false

2022-10-21T15:30:03Z

Move rewrite rules for KUNION and QUNION to the commented-out section for disabled rules, as they are false

← Older revision		Revision as of 15:30, 21 October 2022
Line 105:		Line 105:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_SETENUM}}\|\|<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_SETENUM}}\|\|<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BUNION}}\|\|<math> \finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BUNION}}\|\|<math> \finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T) </math>\|\| \|\| A
	~~{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_UNION}}\|\|<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp \finite(x))</math>\|\| \|\| M~~
	{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_QUNION}}\|\|<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp \finite(E))</math>\|\| this equivalence is false: for example, the union of an infinite set of empty sets is finite; the right-to-left implication is true \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_POW}}\|\|<math> \finite (\pow (S)) \;\;\defi\;\; \finite (S) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_POW}}\|\|<math> \finite (\pow (S)) \;\;\defi\;\; \finite (S) </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_FINITE_CPROD}}\|\|<math> \finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T)) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_FINITE_CPROD}}\|\|<math> \finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T)) </math>\|\| \|\| A
Line 112:		Line 110:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_UPTO}}\|\|<math> \finite (a \upto b) \;\;\defi\;\; \btrue </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_UPTO}}\|\|<math> \finite (a \upto b) \;\;\defi\;\; \btrue </math>\|\| \|\| A
	<!-- Disabled rules (some are false, need more thinking to check which)		<!-- Disabled rules (some are false, need more thinking to check which)
			{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_UNION}}\|\|<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp \finite(x))</math>\|\| \|\| M
			{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_QUNION}}\|\|<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp \finite(E))</math>\|\| this equivalence is false: for example, the union of an infinite set of empty sets is finite; the right-to-left implication is true \|\| M
	{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_BINTER_L}}\|\|<math> \finite (S \binter T) \;\;\defi\;\; \finite (S) </math>\|\| \|\| M		{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_BINTER_L}}\|\|<math> \finite (S \binter T) \;\;\defi\;\; \finite (S) </math>\|\| \|\| M
	{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_BINTER_R}}\|\|<math> \finite (S \binter T) \;\;\defi\;\; \finite (T) </math>\|\| \|\| M		{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_BINTER_R}}\|\|<math> \finite (S \binter T) \;\;\defi\;\; \finite (T) </math>\|\| \|\| M

Guillaume: add note about finiteness of infinite union

2022-10-17T09:26:18Z

add note about finiteness of infinite union

← Older revision		Revision as of 09:26, 17 October 2022
Line 105:		Line 105:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_SETENUM}}\|\|<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_SETENUM}}\|\|<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BUNION}}\|\|<math> \finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BUNION}}\|\|<math> \finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T) </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_UNION}}\|\|<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp finite(x))</math>\|\| \|\| M		{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_UNION}}\|\|<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp \finite(x))</math>\|\| \|\| M
	{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_QUNION}}\|\|<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp finite(E))</math>\|\| \|\| M		{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_QUNION}}\|\|<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp \finite(E))</math>\|\| this equivalence is false: for example, the union of an infinite set of empty sets is finite; the right-to-left implication is true \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_POW}}\|\|<math> \finite (\pow (S)) \;\;\defi\;\; \finite (S) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_POW}}\|\|<math> \finite (\pow (S)) \;\;\defi\;\; \finite (S) </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_FINITE_CPROD}}\|\|<math> \finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T)) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_FINITE_CPROD}}\|\|<math> \finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T)) </math>\|\| \|\| A

imported>Laurent: Add rules SIMP_EMPTY_PARTITION and SIMP_SINGLE_PARTITION

2013-10-02T17:16:56Z

Add rules SIMP_EMPTY_PARTITION and SIMP_SINGLE_PARTITION

← Older revision		Revision as of 17:16, 2 October 2013
Line 203:		Line 203:
	\land& s_{n-1}\binter s_n = \emptyset		\land& s_{n-1}\binter s_n = \emptyset
	\end{array}</math>\|\| \|\| AM		\end{array}</math>\|\| \|\| AM
			{{RRRow}}\| \|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A
	\|}		\|}

imported>Josselin: Removed SIMP_TYPE_EQUAL_EMPTY (moved to Empty Set Rewrite Rules)

2013-05-02T15:19:22Z

Removed SIMP_TYPE_EQUAL_EMPTY (moved to Empty Set Rewrite Rules)

← Older revision		Revision as of 15:19, 2 May 2013
Line 143:		Line 143:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BOOL}}\|\|<math> \finite (\Bool ) \;\;\defi\;\; \btrue </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BOOL}}\|\|<math> \finite (\Bool ) \;\;\defi\;\; \btrue </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_LAMBDA}}\|\|<math> \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \finite(\{x\qdot P\mid E\} ) </math>\|\| where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_LAMBDA}}\|\|<math> \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \finite(\{x\qdot P\mid E\} ) </math>\|\| where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> \|\| A
	~~{{RRRow}}\|*\|\|{{Rulename\|SIMP_TYPE_EQUAL_EMPTY}}\|\|<math> \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A~~
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_TYPE_IN}}\|\|<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_TYPE_IN}}\|\|<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQV_BTRUE}}\|\|<math> P \leqv \btrue \;\;\defi\;\; P </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQV_BTRUE}}\|\|<math> P \leqv \btrue \;\;\defi\;\; P </math>\|\| \|\| A

imported>Josselin: Removed SIMP_SPECIAL_EQUAL_COMPSET (moved to Empty Set Rewrite Rules)

2013-05-02T15:17:40Z

Removed SIMP_SPECIAL_EQUAL_COMPSET (moved to Empty Set Rewrite Rules)

← Older revision		Revision as of 15:17, 2 May 2013
Line 94:		Line 94:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COMPSET_BTRUE}}\|\|<math> \{ x \qdot \btrue \mid E \} \;\;\defi\;\; \mathit{Ty} </math>\|\| where the type of <math>E</math> is <math>\mathit{Ty}</math> and <math>E</math> is a maplet combination of locally-bound, pairwise-distinct bound identifiers \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COMPSET_BTRUE}}\|\|<math> \{ x \qdot \btrue \mid E \} \;\;\defi\;\; \mathit{Ty} </math>\|\| where the type of <math>E</math> is <math>\mathit{Ty}</math> and <math>E</math> is a maplet combination of locally-bound, pairwise-distinct bound identifiers \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SUBSETEQ_COMPSET_L}}\|\|<math> \{ x \qdot P(x) \mid E(x) \} \subseteq S \;\;\defi\;\; \forall y\qdot P(y) \limp E(y) \in S </math>\|\| where <math>y</math> is fresh \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SUBSETEQ_COMPSET_L}}\|\|<math> \{ x \qdot P(x) \mid E(x) \} \subseteq S \;\;\defi\;\; \forall y\qdot P(y) \limp E(y) \in S </math>\|\| where <math>y</math> is fresh \|\| 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_IN_COMPSET}}\|\|<math> F \in \{ x,y,\ldots \qdot P(x,y,\ldots) \mid E(x,y,\ldots) \} \;\;\defi\;\; \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F </math>\|\| where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_IN_COMPSET}}\|\|<math> F \in \{ x,y,\ldots \qdot P(x,y,\ldots) \mid E(x,y,\ldots) \} \;\;\defi\;\; \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F </math>\|\| where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_IN_COMPSET_ONEPOINT}}\|\|<math> E \in \{ x \qdot P(x) \mid x \} \;\;\defi\;\; P(E) </math>\|\| Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_IN_COMPSET_ONEPOINT}}\|\|<math> E \in \{ x \qdot P(x) \mid x \} \;\;\defi\;\; P(E) </math>\|\| Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate \|\| A

imported>Josselin: Removed DEF_SPECIAL_NOT_EQUAL (moved to Empty Set Rewrite Rules)

2013-05-02T15:14:05Z

Removed DEF_SPECIAL_NOT_EQUAL (moved to Empty Set Rewrite Rules)

← Older revision		Revision as of 15:14, 2 May 2013
Line 169:		Line 169:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_NOT_FORALL}}\|\|<math> \lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DERIV_NOT_FORALL}}\|\|<math> \lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P </math>\|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_NOT_EXISTS}}\|\|<math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DERIV_NOT_EXISTS}}\|\|<math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P </math>\|\| \|\| M
	~~{{RRRow}}\|*\|\|{{Rulename\|DEF_SPECIAL_NOT_EQUAL}}\|\|<math> \lnot\, S = \emptyset \;\;\defi\;\; \exists x \qdot x \in S </math>\|\| where <math>x</math> is not free in <math>S</math> \|\| M~~
	{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_MAPSTO}}\|\|<math> E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T </math>\|\| \|\| AM		{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_MAPSTO}}\|\|<math> E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T </math>\|\| \|\| AM
	{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_POW}}\|\|<math> E \in \pow (S) \;\;\defi\;\; E \subseteq S </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_POW}}\|\|<math> E \in \pow (S) \;\;\defi\;\; E \subseteq S </math>\|\| \|\| M

imported>Billaude: DEF_IN_MAPSTO rule is now automatic with the AutoRewriterL3.

2011-09-29T14:51:18Z

DEF_IN_MAPSTO rule is now automatic with the AutoRewriterL3.

← Older revision		Revision as of 14:51, 29 September 2011
Line 170:		Line 170:
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_NOT_EXISTS}}\|\|<math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DERIV_NOT_EXISTS}}\|\|<math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P </math>\|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|DEF_SPECIAL_NOT_EQUAL}}\|\|<math> \lnot\, S = \emptyset \;\;\defi\;\; \exists x \qdot x \in S </math>\|\| where <math>x</math> is not free in <math>S</math> \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_SPECIAL_NOT_EQUAL}}\|\|<math> \lnot\, S = \emptyset \;\;\defi\;\; \exists x \qdot x \in S </math>\|\| where <math>x</math> is not free in <math>S</math> \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_MAPSTO}}\|\|<math> E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_MAPSTO}}\|\|<math> E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T </math>\|\| \|\| AM
	{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_POW}}\|\|<math> E \in \pow (S) \;\;\defi\;\; E \subseteq S </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_POW}}\|\|<math> E \in \pow (S) \;\;\defi\;\; E \subseteq S </math>\|\| \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_POW1}}\|\|<math> E \in \pown (S) \;\;\defi\;\; E \in \pow (S) \land S \neq \emptyset </math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_IN_POW1}}\|\|<math> E \in \pown (S) \;\;\defi\;\; E \in \pow (S) \land S \neq \emptyset </math>\|\| \|\| M

← Older revision		Revision as of 14:33, 13 April 2023
Line 203:		Line 203:
	\land& s_{n-1}\binter s_n = \emptyset		\land& s_{n-1}\binter s_n = \emptyset
	\end{array}</math>\|\| \|\| AM		\end{array}</math>\|\| \|\| AM
	{{RRRow}}\| \|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DEF_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>\|\| also works for <math>k = \operatorname{card}(S)</math> \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>\|\| also works for <math>k = \operatorname{card}(S)</math> \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|SIMP_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>\|\| \|\| M

← Older revision		Revision as of 09:31, 6 April 2023
Line 205:		Line 205:
	{{RRRow}}\| \|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A		{{RRRow}}\| \|\|{{Rulename\|SIMP_EMPTY_PARTITION}}\|\|<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A		{{RRRow}}\| \|\|{{Rulename\|SIMP_SINGLE_PARTITION}}\|\|<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|DEF_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>\|\| also works for <math>k = \operatorname{card}(S)</math> \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DEF_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>\|\| also works for <math>k = \operatorname{card}(S)</math> \|\| M
	{{RRRow}}\| \|\|{{Rulename\|SIMP_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>\|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|SIMP_EQUAL_CARD}}\|\|<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>\|\| \|\| M
	\|}		\|}

← Older revision		Revision as of 15:30, 21 October 2022
Line 105:		Line 105:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_SETENUM}}\|\|<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_SETENUM}}\|\|<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BUNION}}\|\|<math> \finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BUNION}}\|\|<math> \finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T) </math>\|\| \|\| A
	~~{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_UNION}}\|\|<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp \finite(x))</math>\|\| \|\| M~~
	{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_QUNION}}\|\|<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp \finite(E))</math>\|\| this equivalence is false: for example, the union of an infinite set of empty sets is finite; the right-to-left implication is true \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_POW}}\|\|<math> \finite (\pow (S)) \;\;\defi\;\; \finite (S) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_POW}}\|\|<math> \finite (\pow (S)) \;\;\defi\;\; \finite (S) </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_FINITE_CPROD}}\|\|<math> \finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T)) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_FINITE_CPROD}}\|\|<math> \finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T)) </math>\|\| \|\| A
Line 112:		Line 110:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_UPTO}}\|\|<math> \finite (a \upto b) \;\;\defi\;\; \btrue </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_UPTO}}\|\|<math> \finite (a \upto b) \;\;\defi\;\; \btrue </math>\|\| \|\| A
	<!-- Disabled rules (some are false, need more thinking to check which)		<!-- Disabled rules (some are false, need more thinking to check which)
			{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_UNION}}\|\|<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp \finite(x))</math>\|\| \|\| M
			{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_QUNION}}\|\|<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp \finite(E))</math>\|\| this equivalence is false: for example, the union of an infinite set of empty sets is finite; the right-to-left implication is true \|\| M
	{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_BINTER_L}}\|\|<math> \finite (S \binter T) \;\;\defi\;\; \finite (S) </math>\|\| \|\| M		{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_BINTER_L}}\|\|<math> \finite (S \binter T) \;\;\defi\;\; \finite (S) </math>\|\| \|\| M
	{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_BINTER_R}}\|\|<math> \finite (S \binter T) \;\;\defi\;\; \finite (T) </math>\|\| \|\| M		{{RRRow}}\|\|\|{{Rulename\|SIMP_FINITE_BINTER_R}}\|\|<math> \finite (S \binter T) \;\;\defi\;\; \finite (T) </math>\|\| \|\| M

← Older revision		Revision as of 09:26, 17 October 2022
Line 105:		Line 105:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_SETENUM}}\|\|<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_SETENUM}}\|\|<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BUNION}}\|\|<math> \finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BUNION}}\|\|<math> \finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T) </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_UNION}}\|\|<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp finite(x))</math>\|\| \|\| M		{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_UNION}}\|\|<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp \finite(x))</math>\|\| \|\| M
	{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_QUNION}}\|\|<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp finite(E))</math>\|\| \|\| M		{{RRRow}}\| \|\|{{Rulename\|SIMP_FINITE_QUNION}}\|\|<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp \finite(E))</math>\|\| this equivalence is false: for example, the union of an infinite set of empty sets is finite; the right-to-left implication is true \|\| M
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_POW}}\|\|<math> \finite (\pow (S)) \;\;\defi\;\; \finite (S) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_POW}}\|\|<math> \finite (\pow (S)) \;\;\defi\;\; \finite (S) </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|DERIV_FINITE_CPROD}}\|\|<math> \finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T)) </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|DERIV_FINITE_CPROD}}\|\|<math> \finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T)) </math>\|\| \|\| A

← Older revision		Revision as of 15:19, 2 May 2013
Line 143:		Line 143:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BOOL}}\|\|<math> \finite (\Bool ) \;\;\defi\;\; \btrue </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_BOOL}}\|\|<math> \finite (\Bool ) \;\;\defi\;\; \btrue </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_LAMBDA}}\|\|<math> \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \finite(\{x\qdot P\mid E\} ) </math>\|\| where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_FINITE_LAMBDA}}\|\|<math> \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \finite(\{x\qdot P\mid E\} ) </math>\|\| where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> \|\| A
	~~{{RRRow}}\|*\|\|{{Rulename\|SIMP_TYPE_EQUAL_EMPTY}}\|\|<math> \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A~~
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_TYPE_IN}}\|\|<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_TYPE_IN}}\|\|<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>\|\| where <math>\mathit{Ty}</math> is a type expression \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQV_BTRUE}}\|\|<math> P \leqv \btrue \;\;\defi\;\; P </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_EQV_BTRUE}}\|\|<math> P \leqv \btrue \;\;\defi\;\; P </math>\|\| \|\| A