Inference Rules - Revision history

Guillaume: Rule FIN_COMPSET_R has been implemented in Rodin 3.9

2024-06-03T15:10:06Z

Rule FIN_COMPSET_R has been implemented in Rodin 3.9

← Older revision		Revision as of 15:10, 3 June 2024
Line 161:		Line 161:
	\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)}</math> \|\| \|\| M		\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)}</math> \|\| \|\| M

	{{RRRow}}\|\|\|{{Rulename\|FIN_COMPSET_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash		{{RRRow}}\|*\|\|{{Rulename\|FIN_COMPSET_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
	\;\;\finite\,(\{x \,\mid\, P(x)\})}{\textbf{H} \;\;\vdash \;\; \finite\,(\{x \,\qdot\, P(x) \,\mid\, F(x)\})}</math> \|\| \|\| M		\;\;\finite\,(\{x \,\mid\, P(x)\})}{\textbf{H} \;\;\vdash \;\; \finite\,(\{x \,\qdot\, P(x) \,\mid\, F(x)\})}</math> \|\| \|\| M

Guillaume: Add rule for finiteness of explicit set comprehension

2024-02-01T10:22:11Z

Add rule for finiteness of explicit set comprehension

← Older revision		Revision as of 10:22, 1 February 2024
Line 160:		Line 160:
	{{RRRow}}\|*\|\|{{Rulename\|FIN_SETMINUS_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash		{{RRRow}}\|*\|\|{{Rulename\|FIN_SETMINUS_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
	\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)}</math> \|\| \|\| M		\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)}</math> \|\| \|\| M

			{{RRRow}}\|\|\|{{Rulename\|FIN_COMPSET_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
			\;\;\finite\,(\{x \,\mid\, P(x)\})}{\textbf{H} \;\;\vdash \;\; \finite\,(\{x \,\qdot\, P(x) \,\mid\, F(x)\})}</math> \|\| \|\| M

	{{RRRow}}\| \|\|{{Rulename\|FIN_REL}}\|\| <math>\frac{}{\textbf{H},\; r\in S\;\mathit{op}\;T,\; \finite\,(S),\; \finite\,(T) \;\;\vdash \;\; \finite\,(r)}</math> \|\| where <math>\mathit{op}</math> denotes a set of relations (any arrow) \|\| A		{{RRRow}}\| \|\|{{Rulename\|FIN_REL}}\|\| <math>\frac{}{\textbf{H},\; r\in S\;\mathit{op}\;T,\; \finite\,(S),\; \finite\,(T) \;\;\vdash \;\; \finite\,(r)}</math> \|\| where <math>\mathit{op}</math> denotes a set of relations (any arrow) \|\| A

Guillaume: Rules EQV_LR and EQV_RL were implemented

2023-04-13T14:32:07Z

Rules EQV_LR and EQV_RL were implemented

← Older revision		Revision as of 14:32, 13 April 2023
Line 95:		Line 95:
	{{RRRow}}\|*\|\|{{Rulename\|HM}}\|\| <math>\frac{\textbf{H} \;\;\vdash\;\;\neg\,\textbf{Q} \qquad \textbf{H},\; \neg\,\textbf{P} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> \|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|HM}}\|\| <math>\frac{\textbf{H} \;\;\vdash\;\;\neg\,\textbf{Q} \qquad \textbf{H},\; \neg\,\textbf{P} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> \|\| \|\| M

	{{RRRow}}\|\|\|{{Rulename\|EQV_LR}}\|\| <math>\frac{\textbf{H(Q)},\; \textbf{P} \leqv \textbf{Q}		{{RRRow}}\|*\|\|{{Rulename\|EQV_LR}}\|\| <math>\frac{\textbf{H(Q)},\; \textbf{P} \leqv \textbf{Q}
	\;\;\vdash\;\; \textbf{G(Q)}}{\textbf{H(P)},\;\textbf{P} \leqv \textbf{Q}		\;\;\vdash\;\; \textbf{G(Q)}}{\textbf{H(P)},\;\textbf{P} \leqv \textbf{Q}
	\;\;\vdash \;\; \textbf{G(P)}}</math> \|\| \|\| M		\;\;\vdash \;\; \textbf{G(P)}}</math> \|\| \|\| M

	{{RRRow}}\|\|\|{{Rulename\|EQV_RL}}\|\| <math>\frac{\textbf{H(P)},\; \textbf{P} \leqv \textbf{Q}		{{RRRow}}\|*\|\|{{Rulename\|EQV_RL}}\|\| <math>\frac{\textbf{H(P)},\; \textbf{P} \leqv \textbf{Q}
	\;\;\vdash\;\; \textbf{G(P)}}{\textbf{H(Q)},\;\textbf{P} \leqv \textbf{Q}		\;\;\vdash\;\; \textbf{G(P)}}{\textbf{H(Q)},\;\textbf{P} \leqv \textbf{Q}
	\;\;\vdash \;\; \textbf{G(Q)}}</math> \|\| \|\| M		\;\;\vdash \;\; \textbf{G(Q)}}</math> \|\| \|\| M

Guillaume: Add star to proof rules implemented in Rodin 3.8

2023-04-06T09:30:14Z

Add star to proof rules implemented in Rodin 3.8

Guillaume: Fix inference rule FIN_KUNION_R

2022-10-21T15:26:39Z

Fix inference rule FIN_KUNION_R

← Older revision		Revision as of 15:26, 21 October 2022
Line 151:		Line 151:

	{{RRRow}}\| \|\|{{Rulename\|FIN_KUNION_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash		{{RRRow}}\| \|\|{{Rulename\|FIN_KUNION_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
	\;\;\forall s\, \qdot\, s \in S \limp \finite\,(s)}{\textbf{H} \;\;\vdash		\;\; \finite\,(S) \;\land\; (\forall s\, \qdot\, s \in S \limp \finite\,(s))}{\textbf{H} \;\;\vdash
	\;\; \finite\,(\union(S))}</math> \|\| where <math>s</math> is fresh \|\| M		\;\; \finite\,(\union(S))}</math> \|\| where <math>s</math> is fresh \|\| M

Guillaume: Add rules for finiteness of union

2022-10-17T09:20:11Z

Add rules for finiteness of union

@@ Line 145: / Line 145: @@
 \;\;\exists s\, \qdot\, P \land \finite\,(E)}{\textbf{H} \;\;\vdash
 \;\; \finite\,(\Inter s\,\qdot\,P\,\mid\,E)}</math> ||  || M
 {{RRRow}}|*||{{Rulename|FIN_SETMINUS_R}}|| <math>\frac{\textbf{H} \;\;\vdash

imported>Nicolas: Removed induction on integers (was wrong), reviewed induciton on naturals

2014-06-23T16:00:15Z

Removed induction on integers (was wrong), reviewed induciton on naturals

← Older revision		Revision as of 16:00, 23 June 2014
Line 229:		Line 229:
	{{RRRow}}\|*\|\|{{Rulename\|SIM_OV_TFUN}}\|\| <math> \frac{\textbf{H}\vdash x\in A\qquad \textbf{H}\vdash y\in B}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto y\right\}\in A\tfun B} </math> \|\| where <math>\mathit{op}</math> is one of <math>\tfun</math>, <math>\tinj</math>, <math>\tsur</math>, <math>\tbij</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIM_OV_TFUN}}\|\| <math> \frac{\textbf{H}\vdash x\in A\qquad \textbf{H}\vdash y\in B}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto y\right\}\in A\tfun B} </math> \|\| where <math>\mathit{op}</math> is one of <math>\tfun</math>, <math>\tinj</math>, <math>\tsur</math>, <math>\tbij</math> \|\| A

	{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, \textbf{P}(n) \;\;\vdash \;\; \textbf{P}(n+1)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> \|\| M		{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H}, x=0 \;\;\vdash \;\; \textbf{P}(x) \qquad \textbf{H}, n\in\nat, \textbf{P}(n) \;\;\vdash \;\; \textbf{P}(n+1)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math>; <math>n</math> is introduced as a fresh identifier \|\| M

	{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT_COMPL}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, k\in\~~nat,~~ k < n \limp \textbf{P}(k) \;\;\vdash \;\; \textbf{P}(n)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> ~~\|\| M~~		{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT_COMPL}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, \forall k\qdot 0\leq k\land k < n \limp \textbf{P}(k) \;\;\vdash \;\; \textbf{P}(n)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math>; <math>n</math> is introduced as a fresh identifier \|\| M

	~~{{RRRow}}\| \|\|{{Rulename\|INDUC_INT}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, \textbf{P}(n), \textbf{P}(-n) \;\;\vdash \;\~~; ~~\textbf{P}(n+1)\land\textbf{P}(-n-1)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg~~</math> ~~appears free in <math>\textbf{P}</math> \|\| M~~

	~~{{RRRow}}\| \|\|{{Rulename\|INDUC_INT_COMPL}}\|\| <math>\frac{\qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H},~~ n\in\nat, k\in\nat, k < n \limp \textbf{P}(k)\land\textbf{P}(-k) \;\;\vdash \;\; \textbf{P}(n)\land\textbf{P}(-n)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> \|\| M

imported>Nicolas: Added INDUC_* inference rules

2014-06-23T13:47:49Z

Added INDUC_* inference rules

← Older revision		Revision as of 13:47, 23 June 2014
Line 228:		Line 228:

	{{RRRow}}\|*\|\|{{Rulename\|SIM_OV_TFUN}}\|\| <math> \frac{\textbf{H}\vdash x\in A\qquad \textbf{H}\vdash y\in B}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto y\right\}\in A\tfun B} </math> \|\| where <math>\mathit{op}</math> is one of <math>\tfun</math>, <math>\tinj</math>, <math>\tsur</math>, <math>\tbij</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIM_OV_TFUN}}\|\| <math> \frac{\textbf{H}\vdash x\in A\qquad \textbf{H}\vdash y\in B}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto y\right\}\in A\tfun B} </math> \|\| where <math>\mathit{op}</math> is one of <math>\tfun</math>, <math>\tinj</math>, <math>\tsur</math>, <math>\tbij</math> \|\| A

			{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, \textbf{P}(n) \;\;\vdash \;\; \textbf{P}(n+1)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> \|\| M

			{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT_COMPL}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, k\in\nat, k < n \limp \textbf{P}(k) \;\;\vdash \;\; \textbf{P}(n)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> \|\| M

			{{RRRow}}\| \|\|{{Rulename\|INDUC_INT}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, \textbf{P}(n), \textbf{P}(-n) \;\;\vdash \;\; \textbf{P}(n+1)\land\textbf{P}(-n-1)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> \|\| M

			{{RRRow}}\| \|\|{{Rulename\|INDUC_INT_COMPL}}\|\| <math>\frac{\qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, k\in\nat, k < n \limp \textbf{P}(k)\land\textbf{P}(-k) \;\;\vdash \;\; \textbf{P}(n)\land\textbf{P}(-n)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> \|\| M


	\|}		\|}

imported>Laurent: Split EQV into EQV_LR and EQV_RL

2014-06-13T14:24:55Z

Split EQV into EQV_LR and EQV_RL

← Older revision		Revision as of 14:24, 13 June 2014
Line 95:		Line 95:
	{{RRRow}}\|*\|\|{{Rulename\|HM}}\|\| <math>\frac{\textbf{H} \;\;\vdash\;\;\neg\,\textbf{Q} \qquad \textbf{H},\; \neg\,\textbf{P} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> \|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|HM}}\|\| <math>\frac{\textbf{H} \;\;\vdash\;\;\neg\,\textbf{Q} \qquad \textbf{H},\; \neg\,\textbf{P} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> \|\| \|\| M

	{{RRRow}}\|\|\|{{Rulename\|~~EQV~~}}\|\| <math>\frac{\textbf{H(Q)},\; \textbf{P} \leqv \textbf{Q}		{{RRRow}}\|\|\|{{Rulename\|EQV_LR}}\|\| <math>\frac{\textbf{H(Q)},\; \textbf{P} \leqv \textbf{Q}
	\;\;\vdash\;\; \textbf{G(Q)}}{\textbf{H(P)},\;\textbf{P} \leqv \textbf{Q}		\;\;\vdash\;\; \textbf{G(Q)}}{\textbf{H(P)},\;\textbf{P} \leqv \textbf{Q}
	\;\;\vdash \;\; \textbf{G(P)}}</math> \|\| \|\| M		\;\;\vdash \;\; \textbf{G(P)}}</math> \|\| \|\| M

			{{RRRow}}\|\|\|{{Rulename\|EQV_RL}}\|\| <math>\frac{\textbf{H(P)},\; \textbf{P} \leqv \textbf{Q}
			\;\;\vdash\;\; \textbf{G(P)}}{\textbf{H(Q)},\;\textbf{P} \leqv \textbf{Q}
			\;\;\vdash \;\; \textbf{G(Q)}}</math> \|\| \|\| M

	{{RRRow}}\|*\|\|{{Rulename\|OV_SETENUM_L}}\|\| <math>\frac{\textbf{H},\; G=E		{{RRRow}}\|*\|\|{{Rulename\|OV_SETENUM_L}}\|\| <math>\frac{\textbf{H},\; G=E

imported>Laurent at 10:14, 29 August 2013

2013-08-29T10:14:21Z

← Older revision		Revision as of 10:14, 29 August 2013
Line 262:		Line 262:


	The conventions used in this table are described in [[~~Variants~~ in HYP, CNTR and GenMP]].		The conventions used in this table are described in [[Variations in HYP, CNTR and GenMP]].

	{\|class="RRHeader" text-align="left" border="1" cellspacing="4" cellpadding="8" rules="all" frame="box" style="margin:1em 1em 1em 0; border-style:solid; border-color:#AAAAAA; display:table; {{{style\|}}}"		{\|class="RRHeader" text-align="left" border="1" cellspacing="4" cellpadding="8" rules="all" frame="box" style="margin:1em 1em 1em 0; border-style:solid; border-color:#AAAAAA; display:table; {{{style\|}}}"

← Older revision		Revision as of 15:10, 3 June 2024
Line 161:		Line 161:
	\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)}</math> \|\| \|\| M		\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)}</math> \|\| \|\| M

	{{RRRow}}\|\|\|{{Rulename\|FIN_COMPSET_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash		{{RRRow}}\|*\|\|{{Rulename\|FIN_COMPSET_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
	\;\;\finite\,(\{x \,\mid\, P(x)\})}{\textbf{H} \;\;\vdash \;\; \finite\,(\{x \,\qdot\, P(x) \,\mid\, F(x)\})}</math> \|\| \|\| M		\;\;\finite\,(\{x \,\mid\, P(x)\})}{\textbf{H} \;\;\vdash \;\; \finite\,(\{x \,\qdot\, P(x) \,\mid\, F(x)\})}</math> \|\| \|\| M

← Older revision		Revision as of 14:32, 13 April 2023
Line 95:		Line 95:
	{{RRRow}}\|*\|\|{{Rulename\|HM}}\|\| <math>\frac{\textbf{H} \;\;\vdash\;\;\neg\,\textbf{Q} \qquad \textbf{H},\; \neg\,\textbf{P} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> \|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|HM}}\|\| <math>\frac{\textbf{H} \;\;\vdash\;\;\neg\,\textbf{Q} \qquad \textbf{H},\; \neg\,\textbf{P} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> \|\| \|\| M

	{{RRRow}}\|\|\|{{Rulename\|EQV_LR}}\|\| <math>\frac{\textbf{H(Q)},\; \textbf{P} \leqv \textbf{Q}		{{RRRow}}\|*\|\|{{Rulename\|EQV_LR}}\|\| <math>\frac{\textbf{H(Q)},\; \textbf{P} \leqv \textbf{Q}
	\;\;\vdash\;\; \textbf{G(Q)}}{\textbf{H(P)},\;\textbf{P} \leqv \textbf{Q}		\;\;\vdash\;\; \textbf{G(Q)}}{\textbf{H(P)},\;\textbf{P} \leqv \textbf{Q}
	\;\;\vdash \;\; \textbf{G(P)}}</math> \|\| \|\| M		\;\;\vdash \;\; \textbf{G(P)}}</math> \|\| \|\| M

	{{RRRow}}\|\|\|{{Rulename\|EQV_RL}}\|\| <math>\frac{\textbf{H(P)},\; \textbf{P} \leqv \textbf{Q}		{{RRRow}}\|*\|\|{{Rulename\|EQV_RL}}\|\| <math>\frac{\textbf{H(P)},\; \textbf{P} \leqv \textbf{Q}
	\;\;\vdash\;\; \textbf{G(P)}}{\textbf{H(Q)},\;\textbf{P} \leqv \textbf{Q}		\;\;\vdash\;\; \textbf{G(P)}}{\textbf{H(Q)},\;\textbf{P} \leqv \textbf{Q}
	\;\;\vdash \;\; \textbf{G(Q)}}</math> \|\| \|\| M		\;\;\vdash \;\; \textbf{G(Q)}}</math> \|\| \|\| M

← Older revision		Revision as of 16:00, 23 June 2014
Line 229:		Line 229:
	{{RRRow}}\|*\|\|{{Rulename\|SIM_OV_TFUN}}\|\| <math> \frac{\textbf{H}\vdash x\in A\qquad \textbf{H}\vdash y\in B}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto y\right\}\in A\tfun B} </math> \|\| where <math>\mathit{op}</math> is one of <math>\tfun</math>, <math>\tinj</math>, <math>\tsur</math>, <math>\tbij</math> \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIM_OV_TFUN}}\|\| <math> \frac{\textbf{H}\vdash x\in A\qquad \textbf{H}\vdash y\in B}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto y\right\}\in A\tfun B} </math> \|\| where <math>\mathit{op}</math> is one of <math>\tfun</math>, <math>\tinj</math>, <math>\tsur</math>, <math>\tbij</math> \|\| A

	{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, \textbf{P}(n) \;\;\vdash \;\; \textbf{P}(n+1)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> \|\| M		{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H}, x=0 \;\;\vdash \;\; \textbf{P}(x) \qquad \textbf{H}, n\in\nat, \textbf{P}(n) \;\;\vdash \;\; \textbf{P}(n+1)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math>; <math>n</math> is introduced as a fresh identifier \|\| M

	{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT_COMPL}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, k\in\~~nat,~~ k < n \limp \textbf{P}(k) \;\;\vdash \;\; \textbf{P}(n)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> ~~\|\| M~~		{{RRRow}}\| \|\|{{Rulename\|INDUC_NAT_COMPL}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, \forall k\qdot 0\leq k\land k < n \limp \textbf{P}(k) \;\;\vdash \;\; \textbf{P}(n)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math>; <math>n</math> is introduced as a fresh identifier \|\| M

	~~{{RRRow}}\| \|\|{{Rulename\|INDUC_INT}}\|\| <math>\frac{\textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, \textbf{P}(n), \textbf{P}(-n) \;\;\vdash \;\~~; ~~\textbf{P}(n+1)\land\textbf{P}(-n-1)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg~~</math> ~~appears free in <math>\textbf{P}</math> \|\| M~~

	~~{{RRRow}}\| \|\|{{Rulename\|INDUC_INT_COMPL}}\|\| <math>\frac{\qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H},~~ n\in\nat, k\in\nat, k < n \limp \textbf{P}(k)\land\textbf{P}(-k) \;\;\vdash \;\; \textbf{P}(n)\land\textbf{P}(-n)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math> \|\| <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math> \|\| M

← Older revision		Revision as of 14:24, 13 June 2014
Line 95:		Line 95:
	{{RRRow}}\|*\|\|{{Rulename\|HM}}\|\| <math>\frac{\textbf{H} \;\;\vdash\;\;\neg\,\textbf{Q} \qquad \textbf{H},\; \neg\,\textbf{P} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> \|\| \|\| M		{{RRRow}}\|*\|\|{{Rulename\|HM}}\|\| <math>\frac{\textbf{H} \;\;\vdash\;\;\neg\,\textbf{Q} \qquad \textbf{H},\; \neg\,\textbf{P} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> \|\| \|\| M

	{{RRRow}}\|\|\|{{Rulename\|~~EQV~~}}\|\| <math>\frac{\textbf{H(Q)},\; \textbf{P} \leqv \textbf{Q}		{{RRRow}}\|\|\|{{Rulename\|EQV_LR}}\|\| <math>\frac{\textbf{H(Q)},\; \textbf{P} \leqv \textbf{Q}
	\;\;\vdash\;\; \textbf{G(Q)}}{\textbf{H(P)},\;\textbf{P} \leqv \textbf{Q}		\;\;\vdash\;\; \textbf{G(Q)}}{\textbf{H(P)},\;\textbf{P} \leqv \textbf{Q}
	\;\;\vdash \;\; \textbf{G(P)}}</math> \|\| \|\| M		\;\;\vdash \;\; \textbf{G(P)}}</math> \|\| \|\| M

			{{RRRow}}\|\|\|{{Rulename\|EQV_RL}}\|\| <math>\frac{\textbf{H(P)},\; \textbf{P} \leqv \textbf{Q}
			\;\;\vdash\;\; \textbf{G(P)}}{\textbf{H(Q)},\;\textbf{P} \leqv \textbf{Q}
			\;\;\vdash \;\; \textbf{G(Q)}}</math> \|\| \|\| M

	{{RRRow}}\|*\|\|{{Rulename\|OV_SETENUM_L}}\|\| <math>\frac{\textbf{H},\; G=E		{{RRRow}}\|*\|\|{{Rulename\|OV_SETENUM_L}}\|\| <math>\frac{\textbf{H},\; G=E

← Older revision		Revision as of 09:30, 6 April 2023
Line 138:		Line 138:
	\;\; \finite\,(S \;\binter\;\ldots \;\binter\; T)}</math> \|\| \|\| M		\;\; \finite\,(S \;\binter\;\ldots \;\binter\; T)}</math> \|\| \|\| M

	{{RRRow}}\| \|\|{{Rulename\|FIN_KINTER_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash		{{RRRow}}\|*\|\|{{Rulename\|FIN_KINTER_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
	\;\;\exists s\, \qdot\, s \in S \land \finite\,(s)}{\textbf{H} \;\;\vdash		\;\;\exists s\, \qdot\, s \in S \land \finite\,(s)}{\textbf{H} \;\;\vdash
	\;\; \finite\,(\inter(S))}</math> \|\| where <math>s</math> is fresh \|\| M		\;\; \finite\,(\inter(S))}</math> \|\| where <math>s</math> is fresh \|\| M

	{{RRRow}}\| \|\|{{Rulename\|FIN_QINTER_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash		{{RRRow}}\|*\|\|{{Rulename\|FIN_QINTER_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
	\;\;\exists s\, \qdot\, P \land \finite\,(E)}{\textbf{H} \;\;\vdash		\;\;\exists s\, \qdot\, P \land \finite\,(E)}{\textbf{H} \;\;\vdash
	\;\; \finite\,(\Inter s\,\qdot\,P\,\mid\,E)}</math> \|\| \|\| M		\;\; \finite\,(\Inter s\,\qdot\,P\,\mid\,E)}</math> \|\| \|\| M

	{{RRRow}}\| \|\|{{Rulename\|FIN_BUNION_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash		{{RRRow}}\|*\|\|{{Rulename\|FIN_BUNION_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
	\;\;\finite\,(S) \;\land\;\ldots \;\land\; \finite\,(T)}{\textbf{H} \;\;\vdash		\;\;\finite\,(S) \;\land\;\ldots \;\land\; \finite\,(T)}{\textbf{H} \;\;\vdash
	\;\; \finite\,(S \;\bunion\;\ldots \;\bunion\; T)}</math> \|\| \|\| M		\;\; \finite\,(S \;\bunion\;\ldots \;\bunion\; T)}</math> \|\| \|\| M

	{{RRRow}}\| \|\|{{Rulename\|FIN_KUNION_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash		{{RRRow}}\|*\|\|{{Rulename\|FIN_KUNION_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
	\;\; \finite\,(S) \;\land\; (\forall s\, \qdot\, s \in S \limp \finite\,(s))}{\textbf{H} \;\;\vdash		\;\; \finite\,(S) \;\land\; (\forall s\, \qdot\, s \in S \limp \finite\,(s))}{\textbf{H} \;\;\vdash
	\;\; \finite\,(\union(S))}</math> \|\| where <math>s</math> is fresh \|\| M		\;\; \finite\,(\union(S))}</math> \|\| where <math>s</math> is fresh \|\| M

	{{RRRow}}\| \|\|{{Rulename\|FIN_QUNION_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash		{{RRRow}}\|*\|\|{{Rulename\|FIN_QUNION_R}}\|\| <math>\frac{\textbf{H} \;\;\vdash
	\;\; \finite(\{s\qdot P\mid E\})\;\land\;(\forall s\, \qdot\, P \limp \finite\,(E))}{\textbf{H} \;\;\vdash		\;\; \finite(\{s\qdot P\mid E\})\;\land\;(\forall s\, \qdot\, P \limp \finite\,(E))}{\textbf{H} \;\;\vdash
	\;\; \finite\,(\Union s\,\qdot\,P\,\mid\,E)}</math> \|\| \|\| M		\;\; \finite\,(\Union s\,\qdot\,P\,\mid\,E)}</math> \|\| \|\| M