Inference Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Laurent Implementation of rule EXISTS_INST has been confirmed correct |
Add rule for finiteness of explicit set comprehension |
||
(64 intermediate revisions by 9 users not shown) | |||
Line 1: | Line 1: | ||
<font color=red>CAUTION! Any modification to this page shall be announced on the [[#Mailing_lists |User]] mailing list!</font> | |||
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin. | |||
Rules without a <tt>*</tt> are planned to be implemented in future versions. | |||
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Inference_Rules]]. | |||
<!-- | |||
Rules that are marked with a <tt>b</tt> in the first column are currently broken in Rodin 1.1 (see [http://sourceforge.net/tracker/?func=detail&aid=2895507&group_id=108850&atid=651669 bug 2895507]). | Rules that are marked with a <tt>b</tt> in the first column are currently broken in Rodin 1.1 (see [http://sourceforge.net/tracker/?func=detail&aid=2895507&group_id=108850&atid=651669 bug 2895507]). | ||
--> | |||
{{RRHeader}} | {{RRHeader}} | ||
{{RRRow}}|*||{{Rulename|HYP}}|| <math>\frac{}{\textbf{H},\textbf{P} \;\;\vdash \;\; \textbf{P}} </math>|| | {{RRRow}}|*||{{Rulename|HYP}}|| <math>\frac{}{\textbf{H},\textbf{P} \;\;\vdash \;\; \textbf{P}^{\dagger}} </math>|| see below for <math>\textbf{P}^{\dagger}</math> || A | ||
{{RRRow}}|*||{{Rulename|HYP_OR}}|| <math>\frac{}{\textbf{H},\textbf{Q} \;\;\vdash \;\; \textbf{P} \lor \ldots \lor \textbf{Q} \lor \ldots \lor \textbf{R}}</math> || | {{RRRow}}|*||{{Rulename|HYP_OR}}|| <math>\frac{}{\textbf{H},\textbf{Q} \;\;\vdash \;\; \textbf{P} \lor \ldots \lor \textbf{Q}^{\dagger} \lor \ldots \lor \textbf{R}}</math> || see below for <math>\textbf{Q}^{\dagger}</math> || A | ||
{{RRRow}}|*||{{Rulename|CNTR}}|| <math>\frac{}{\textbf{H},\;\textbf{P},\; | {{RRRow}}|*||{{Rulename|CNTR}}|| <math>\frac{}{\textbf{H},\;\textbf{P},\;\textbf{nP}^{\dagger} \;\;\vdash \;\; \textbf{Q}}</math> || see below for <math>\textbf{nP}^{\dagger}</math> || A | ||
{{RRRow}}|*||{{Rulename|FALSE_HYP}}|| <math>\frac{}{\textbf{H},\bfalse \;\;\vdash \;\; \textbf{P}}</math> || || A | {{RRRow}}|*||{{Rulename|FALSE_HYP}}|| <math>\frac{}{\textbf{H},\bfalse \;\;\vdash \;\; \textbf{P}}</math> || || A | ||
Line 15: | Line 20: | ||
{{RRRow}}|*||{{Rulename|TRUE_GOAL}}|| <math>\frac{}{\textbf{H} \;\;\vdash \;\; \btrue}</math> || || A | {{RRRow}}|*||{{Rulename|TRUE_GOAL}}|| <math>\frac{}{\textbf{H} \;\;\vdash \;\; \btrue}</math> || || A | ||
{{RRRow}}|*||{{Rulename|FUN_GOAL}}|| <math>\frac{}{\textbf{H},\; f\in \textbf{E}\;\mathit{op}\; \textbf{ | {{RRRow}}|*||{{Rulename|FUN_GOAL}}|| <math>\frac{}{\textbf{H},\; f\in E\;\mathit{op}\;F \;\;\vdash\;\; f\in T_1\pfun T_2}</math> || where <math>T_1</math> and <math>T_2</math> denote types and <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>. || A | ||
{{RRRow}}|*||{{Rulename|FUN_IMAGE_GOAL}}|| <math>\frac{\textbf{H},\; f\in S_1\;\mathit{op}\;S_2,\; f(E)\in S_2\;\;\vdash\;\; \mathbf{P}(f(E))}{\textbf{H},\; f\in S_1\;\mathit{op}\;S_2\;\;\vdash\;\; \mathbf{P}(f(E))}</math> || where <math>\mathit{op}</math> denotes a set of relations (any arrow) and <math>\mathbf{P}</math> is WD strict || M | |||
{{RRRow}}| ||{{Rulename|FUN_GOAL_REC}}|| <math>\frac{}{\textbf{H},\; f\in S_1\;\mathit{op_1}\;(S_2\;\mathit{op_2}\;(\ldots(S_n\;\mathit{op_n}(U\;\mathit{opf}\;V\;))\ldots)) \;\vdash\;\; f(E_1)(E_2)...(E_n)\in T_1\pfun T_2}</math> || where <math>T_1</math> and <math>T_2</math> denote types, <math>\mathit{op}</math> denotes a set of relations (any arrow) and <math>\mathit{opf}</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>. || A | |||
{{RRRow}}|*||{{Rulename|DBL_HYP}}|| <math>\frac{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H},\;\textbf{P},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math> || || A | {{RRRow}}|*||{{Rulename|DBL_HYP}}|| <math>\frac{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H},\;\textbf{P},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math> || || A | ||
Line 36: | Line 45: | ||
\textbf{H},\textbf{P},\;\textbf{Q}\limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P},\; \textbf{P} \land \textbf{Q} \limp \textbf{R} \;\;\vdash \;\; \textbf{S}}</math> || || A | \textbf{H},\textbf{P},\;\textbf{Q}\limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P},\; \textbf{P} \land \textbf{Q} \limp \textbf{R} \;\;\vdash \;\; \textbf{S}}</math> || || A | ||
{{RRRow}}|*||{{Rulename|NEG_IN_L}}|| <math>\frac{\textbf{H},\; E \in \{ a,\ldots , c\} \; \; \vdash \; \; \textbf{P} }{\textbf{H},\; E \in \{ a,\ldots , b, \ldots , c\} , \neg \, (E=b) \; \; \vdash \; \; \textbf{P} }</math> || || A | {{RRRow}}|*||{{Rulename|NEG_IN_L}}|| <math>\frac{\textbf{H},\; E \in \{ a,\ldots , c\},\; \neg\, (E=b) \; \; \vdash \; \; \textbf{P} }{\textbf{H},\; E \in \{ a,\ldots , b, \ldots , c\} , \neg \, (E=b) \; \; \vdash \; \; \textbf{P} }</math> || || A | ||
{{RRRow}}|*||{{Rulename|NEG_IN_R}}|| <math>\frac{\textbf{H},\; E \in \{ a,\ldots , c\} \; \; \vdash \; \; \textbf{P} }{\textbf{H},\; E \in \{ a,\ldots , b, \ldots , c\} , \neg \, (b=E) \; \; \vdash \; \; \textbf{P} }</math> || || A | {{RRRow}}|*||{{Rulename|NEG_IN_R}}|| <math>\frac{\textbf{H},\; E \in \{ a,\ldots , c\},\; \neg\, (b=E) \; \; \vdash \; \; \textbf{P} }{\textbf{H},\; E \in \{ a,\ldots , b, \ldots , c\} , \neg \, (b=E) \; \; \vdash \; \; \textbf{P} }</math> || || A | ||
{{RRRow}}|*||{{Rulename|XST_L}}|| <math>\frac{\textbf{H},\; \textbf{P(x)} \; \; \vdash \; \; \textbf{Q} | {{RRRow}}|*||{{Rulename|XST_L}}|| <math>\frac{\textbf{H},\; \textbf{P(x)} \; \; \vdash \; \; \textbf{Q} | ||
Line 54: | Line 63: | ||
\textbf{G}(\textbf{S} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{V})} | \textbf{G}(\textbf{S} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{V})} | ||
{\textbf{H},\;\textbf{T} \subseteq \textbf{U} \;\;\vdash \;\; | {\textbf{H},\;\textbf{T} \subseteq \textbf{U} \;\;\vdash \;\; | ||
\textbf{G}(\textbf{S} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{U} \binter \dots \binter \textbf{V})}</math> || | \textbf{G}(\textbf{S} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{U} \binter \dots \binter \textbf{V})}</math> || where <math>\mathbf{T}</math> and <math>\mathbf{U}</math> are not bound by <math>\mathbf{G}</math> || A | ||
{{RRRow}}| ||{{Rulename|IN_INTER}}|| <math>\frac{\textbf{H},\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; | {{RRRow}}| ||{{Rulename|IN_INTER}}|| <math>\frac{\textbf{H},\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; | ||
\textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{U})} | \textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{U})} | ||
{\textbf{H},\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; | {\textbf{H},\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; | ||
\textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{U})}</math> || | \textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{U})}</math> || where <math>\mathbf{E}</math> and <math>\mathbf{T}</math> are not bound by <math>\mathbf{G}</math> || A | ||
{{RRRow}}| ||{{Rulename|NOTIN_INTER}}|| <math>\frac{\textbf{H},\;\lnot\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; | {{RRRow}}| ||{{Rulename|NOTIN_INTER}}|| <math>\frac{\textbf{H},\;\lnot\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; | ||
\textbf{G}(\emptyset)} | \textbf{G}(\emptyset)} | ||
{\textbf{H},\;\lnot\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; | {\textbf{H},\;\lnot\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; | ||
\textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{U})}</math> || | \textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{U})}</math> || where <math>\mathbf{E}</math> and <math>\mathbf{T}</math> are not bound by <math>\mathbf{G}</math> || A | ||
{{RRRow}}|*||{{Rulename|FIN_L_LOWER_BOUND_L}}|| <math>\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)}</math> || The goal is discharged || A | {{RRRow}}|*||{{Rulename|FIN_L_LOWER_BOUND_L}}|| <math>\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)}</math> || The goal is discharged || A | ||
Line 79: | Line 88: | ||
{{RRRow}}|*||{{Rulename|CASE}}|| <math>\frac{\textbf{H}, \; \textbf{P} \; \; \vdash \; \; \textbf{R} \qquad\ldots\qquad \textbf{H}, \; \textbf{Q} \; \; \vdash \; \; \textbf{R} }{\textbf{H},\; \textbf{P} \lor \ldots \lor \textbf{Q} \; \; \vdash \; \; \textbf{R} }</math> || || M | {{RRRow}}|*||{{Rulename|CASE}}|| <math>\frac{\textbf{H}, \; \textbf{P} \; \; \vdash \; \; \textbf{R} \qquad\ldots\qquad \textbf{H}, \; \textbf{Q} \; \; \vdash \; \; \textbf{R} }{\textbf{H},\; \textbf{P} \lor \ldots \lor \textbf{Q} \; \; \vdash \; \; \textbf{R} }</math> || || M | ||
{{RRRow}}|*||{{Rulename|IMP_CASE}}|| <math>\frac{\textbf{H}, \; \lnot\textbf{P} \; \; \vdash \; \; \textbf{R} \qquad \textbf{H}, \; \textbf{Q} \; \; \vdash \; \; \textbf{R} }{\textbf{H},\; \textbf{P} \limp\textbf{Q} \; \; \vdash \; \; \textbf{R} }</math> || || M | |||
{{RRRow}}|*||{{Rulename|MH}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;\textbf{P} \qquad \textbf{H},\; \textbf{Q} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> || || M | {{RRRow}}|*||{{Rulename|MH}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;\textbf{P} \qquad \textbf{H},\; \textbf{Q} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> || || M | ||
Line 84: | 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| | {{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| | {{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 | |||
,\;\textbf{P}(F)\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,(G=E) | ,\;\textbf{P}(F)\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,(G=E) | ||
,\;\textbf{P}(f(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl\{E | ,\;\textbf{P}((\{E\}) \domsub f)(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl\{E | ||
\mapsto F\})(G)) \;\;\vdash \;\; \textbf{Q}}</math> || | \mapsto F\})(G)) \;\;\vdash \;\; \textbf{Q}}</math> || where <math>\mathbf{P}</math> is WD strict || A | ||
{{RRRow}}|*||{{Rulename| | {{RRRow}}|*||{{Rulename|OV_SETENUM_R}}|| <math>\frac{\textbf{H},\; G=E \;\;\vdash\;\;\textbf{Q}(F) | ||
\qquad \textbf{H},\; \neg\,(G=E) \;\;\vdash\;\;\textbf{Q}(f(G))}{\textbf{H} | \qquad \textbf{H},\; \neg\,(G=E) \;\;\vdash\;\;\textbf{Q}((\{E\}) \domsub f)(G))}{\textbf{H} | ||
\;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G))}</math> || | \;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G))}</math> || where <math>\mathbf{Q}</math> is WD strict || A | ||
{{RRRow}}|*||{{Rulename|OV_L}}|| <math>\frac{\textbf{H},\; G \in \dom(g) ,\;\textbf{P}(g(G))\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,G \in \dom(g) ,\;\textbf{P}(f(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl g)(G)) \;\;\vdash \;\; \textbf{Q}}</math> || | {{RRRow}}|*||{{Rulename|OV_L}}|| <math>\frac{\textbf{H},\; G \in \dom(g) ,\;\textbf{P}(g(G))\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,G \in \dom(g) ,\;\textbf{P}((\dom(g) \domsub f)(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl g)(G)) \;\;\vdash \;\; \textbf{Q}}</math> || where <math>\mathbf{P}</math> is WD strict || A | ||
{{RRRow}}|*||{{Rulename|OV_R}}|| <math>\frac{\textbf{H},\; G \in \dom(g) \;\;\vdash\;\;\textbf{Q}(g(G)) \qquad \textbf{H},\; \neg\, G \in \dom(g) \;\;\vdash\;\;\textbf{Q}(f(G))}{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f\ovl g)(G))}</math> || | {{RRRow}}|*||{{Rulename|OV_R}}|| <math>\frac{\textbf{H},\; G \in \dom(g) \;\;\vdash\;\;\textbf{Q}(g(G)) \qquad \textbf{H},\; \neg\, G \in \dom(g) \;\;\vdash\;\;\textbf{Q}((\dom(g) \domsub f)(G))}{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f\ovl g)(G))}</math> || where <math>\mathbf{Q}</math> is WD strict || A | ||
{{RRRow}}|*||{{Rulename|DIS_BINTER_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; f^{-1} \in A \pfun B \qquad\textbf{H} \;\;\vdash\;\;\textbf{Q}(f[S] \binter f[T]) }{\textbf{H} \;\;\vdash \;\; \textbf{Q}(f[S \binter T])}</math> || | {{RRRow}}|*||{{Rulename|DIS_BINTER_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; f^{-1} \in A \pfun B \qquad\textbf{H} \;\;\vdash\;\;\textbf{Q}(f[S] \binter f[T]) }{\textbf{H} \;\;\vdash \;\; \textbf{Q}(f[S \binter T])}</math> || where <math>A</math> and <math>B</math> denote types. || M | ||
{{RRRow}}|*||{{Rulename|DIS_BINTER_L}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; f^{-1} \in A \pfun B \qquad\textbf{H},\;\textbf{Q}(f[S] \binter f[T]) \;\;\vdash\;\;\textbf{G}}{\textbf{H},\; \textbf{Q}(f[S \binter T]) \;\;\vdash \;\; \textbf{G}}</math> || | {{RRRow}}|*||{{Rulename|DIS_BINTER_L}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; f^{-1} \in A \pfun B \qquad\textbf{H},\;\textbf{Q}(f[S] \binter f[T]) \;\;\vdash\;\;\textbf{G}}{\textbf{H},\; \textbf{Q}(f[S \binter T]) \;\;\vdash \;\; \textbf{G}}</math> || where <math>A</math> and <math>B</math> denote types. || M | ||
{{RRRow}}|*||{{Rulename|DIS_SETMINUS_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; f^{-1} \in A \pfun B \qquad\textbf{H} \;\;\vdash\;\;\textbf{Q}(f[S] \setminus f[T]) }{\textbf{H} \;\;\vdash \;\; \textbf{Q}(f[S \setminus T])}</math> || | {{RRRow}}|*||{{Rulename|DIS_SETMINUS_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; f^{-1} \in A \pfun B \qquad\textbf{H} \;\;\vdash\;\;\textbf{Q}(f[S] \setminus f[T]) }{\textbf{H} \;\;\vdash \;\; \textbf{Q}(f[S \setminus T])}</math> || where <math>A</math> and <math>B</math> denote types. || M | ||
{{RRRow}}|*||{{Rulename|DIS_SETMINUS_L}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; f^{-1} \in A \pfun B \qquad\textbf{H},\;\textbf{Q}(f[S] \setminus f[T]) \;\;\vdash\;\; \textbf{G}}{\textbf{H},\; \textbf{Q}(f[S \setminus T]) \;\;\vdash \;\; \textbf{G}}</math> || | {{RRRow}}|*||{{Rulename|DIS_SETMINUS_L}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; f^{-1} \in A \pfun B \qquad\textbf{H},\;\textbf{Q}(f[S] \setminus f[T]) \;\;\vdash\;\; \textbf{G}}{\textbf{H},\; \textbf{Q}(f[S \setminus T]) \;\;\vdash \;\; \textbf{G}}</math> || where <math>A</math> and <math>B</math> denote types. || M | ||
{{RRRow}}|*||{{Rulename|SIM_REL_IMAGE_R}}|| <math>\frac{\textbf{H} \; \; \vdash \; \; {WD}(\textbf{Q}(\{ f(E)\} )) \qquad\textbf{H} \; \; \vdash \; \; \textbf{Q}(\{ f(E)\} ) }{\textbf{H} \; \; \vdash \; \; \textbf{Q}(f[\{ E\} ])} </math> || | {{RRRow}}|*||{{Rulename|SIM_REL_IMAGE_R}}|| <math>\frac{\textbf{H} \; \; \vdash \; \; {WD}(\textbf{Q}(\{ f(E)\} )) \qquad\textbf{H} \; \; \vdash \; \; \textbf{Q}(\{ f(E)\} ) }{\textbf{H} \; \; \vdash \; \; \textbf{Q}(f[\{ E\} ])} </math> || || M | ||
{{RRRow}}|*||{{Rulename|SIM_REL_IMAGE_L}}|| <math>\frac{\textbf{H} \; \; \vdash \; \; {WD}(\textbf{Q}(\{ f(E)\} )) \qquad\textbf{H},\; \textbf{Q}(\{ f(E)\}) \;\;\vdash\;\; \textbf{G}}{\textbf{H},\; \textbf{Q}(f[\{ E\} ]) \;\;\vdash\;\; \textbf{G} } </math> || | {{RRRow}}|*||{{Rulename|SIM_REL_IMAGE_L}}|| <math>\frac{\textbf{H} \; \; \vdash \; \; {WD}(\textbf{Q}(\{ f(E)\} )) \qquad\textbf{H},\; \textbf{Q}(\{ f(E)\}) \;\;\vdash\;\; \textbf{G}}{\textbf{H},\; \textbf{Q}(f[\{ E\} ]) \;\;\vdash\;\; \textbf{G} } </math> || || M | ||
{{RRRow}}|*||{{Rulename|SIM_FCOMP_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(\textbf{Q}(g(f(x)))) \qquad\textbf{H} \;\;\vdash\;\;\textbf{Q}(g(f(x))) }{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f \fcomp g)(x))}</math> || | {{RRRow}}|*||{{Rulename|SIM_FCOMP_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(\textbf{Q}(g(f(x)))) \qquad\textbf{H} \;\;\vdash\;\;\textbf{Q}(g(f(x))) }{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f \fcomp g)(x))}</math> || || M | ||
{{RRRow}}|*||{{Rulename|SIM_FCOMP_L}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(\textbf{Q}(g(f(x)))) \qquad\textbf{H},\; \textbf{Q}(g(f(x))) \;\;\vdash\;\; \textbf{G}}{\textbf{H},\; \textbf{Q}((f \fcomp g)(x)) \;\;\vdash \;\; \textbf{G}}</math> || | {{RRRow}}|*||{{Rulename|SIM_FCOMP_L}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(\textbf{Q}(g(f(x)))) \qquad\textbf{H},\; \textbf{Q}(g(f(x))) \;\;\vdash\;\; \textbf{G}}{\textbf{H},\; \textbf{Q}((f \fcomp g)(x)) \;\;\vdash \;\; \textbf{G}}</math> || || M | ||
{{RRRow}}|*||{{Rulename|FIN_SUBSETEQ_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(T) \qquad\textbf{H} \;\;\vdash \;\; S \subseteq T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(S)}</math> || the user has to write the set corresponding to <math>T</math> in the editing area of the Proof Control Window || M | {{RRRow}}|*||{{Rulename|FIN_SUBSETEQ_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(T) \qquad\textbf{H} \;\;\vdash \;\; S \subseteq T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(S)}</math> || the user has to write the set corresponding to <math>T</math> in the editing area of the Proof Control Window || M | ||
Line 122: | Line 137: | ||
\;\;\finite\,(S) \;\lor\;\ldots \;\lor\; \finite\,(T)}{\textbf{H} \;\;\vdash | \;\;\finite\,(S) \;\lor\;\ldots \;\lor\; \finite\,(T)}{\textbf{H} \;\;\vdash | ||
\;\; \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 | |||
\;\;\exists s\, \qdot\, s \in S \land \finite\,(s)}{\textbf{H} \;\;\vdash | |||
\;\; \finite\,(\inter(S))}</math> || where <math>s</math> is fresh || M | |||
{{RRRow}}|*||{{Rulename|FIN_QINTER_R}}|| <math>\frac{\textbf{H} \;\;\vdash | |||
\;\;\exists s\, \qdot\, P \land \finite\,(E)}{\textbf{H} \;\;\vdash | |||
\;\; \finite\,(\Inter s\,\qdot\,P\,\mid\,E)}</math> || || M | |||
{{RRRow}}|*||{{Rulename|FIN_BUNION_R}}|| <math>\frac{\textbf{H} \;\;\vdash | |||
\;\;\finite\,(S) \;\land\;\ldots \;\land\; \finite\,(T)}{\textbf{H} \;\;\vdash | |||
\;\; \finite\,(S \;\bunion\;\ldots \;\bunion\; T)}</math> || || M | |||
{{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\,(\union(S))}</math> || where <math>s</math> is fresh || M | |||
{{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\,(\Union s\,\qdot\,P\,\mid\,E)}</math> || || M | |||
{{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_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\rel T) \qquad\textbf{H} \;\;\vdash \;\; r \;\in\; S \rel T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(r)}</math> || the user has to write the set corresponding to <math>S \rel T</math> in the editing area of the Proof Control Window || M | {{RRRow}}|*||{{Rulename|FIN_REL_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\rel T) \qquad\textbf{H} \;\;\vdash \;\; r \;\in\; S \rel T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(r)}</math> || the user has to write the set corresponding to <math>S \rel T</math> in the editing area of the Proof Control Window || M | ||
Line 133: | Line 173: | ||
{{RRRow}}|*||{{Rulename|FIN_REL_DOM_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(r))}</math> || || M | {{RRRow}}|*||{{Rulename|FIN_REL_DOM_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(r))}</math> || || M | ||
{{RRRow}}| ||{{Rulename|FIN_FUN_DOM}}|| <math>\frac{}{\textbf{H},\; f\in S\;\mathit{op}\;T,\; \finite\,(S) \;\;\vdash \;\; \finite\,(f)}</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> || A | |||
{{RRRow}}| ||{{Rulename|FIN_FUN_RAN}}|| <math>\frac{}{\textbf{H},\; f\in S\;\mathit{op}\;T,\; \finite\,(T) \;\;\vdash \;\; \finite\,(f)}</math> || where <math>\mathit{op}</math> is one of <math>\pinj</math>, <math>\tinj</math>, <math>\tbij</math> || A | |||
{{RRRow}}|*||{{Rulename|FIN_FUN1_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\pfun T) \qquad\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(f)}</math> || the user has to write the set corresponding to <math>S \pfun T</math> in the editing area of the Proof Control Window || M | {{RRRow}}|*||{{Rulename|FIN_FUN1_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\pfun T) \qquad\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(f)}</math> || the user has to write the set corresponding to <math>S \pfun T</math> in the editing area of the Proof Control Window || M | ||
Line 156: | Line 200: | ||
{{RRRow}}|*||{{Rulename|FIN_GE_0}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \leq n) \qquad \textbf{H} \;\;\vdash \;\; S \subseteq \nat }{\textbf{H} \;\;\vdash \;\; \finite(S)}</math> || || M | {{RRRow}}|*||{{Rulename|FIN_GE_0}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \leq n) \qquad \textbf{H} \;\;\vdash \;\; S \subseteq \nat }{\textbf{H} \;\;\vdash \;\; \finite(S)}</math> || || M | ||
{{RRRow}}|||{{Rulename|CARD_INTERV}}|| <math>\frac{\textbf{H},\, a \leq b \;\;\vdash \;\; \textbf{Q}(b-a+1) \qquad \textbf{H},\, b < a \;\;\vdash \;\; \textbf{Q}(0) }{\textbf{H} \;\;\vdash\;\; \textbf{Q}(\card\,(a\upto b))}</math> || <math>\ | {{RRRow}}|||{{Rulename|CARD_INTERV}}|| <math>\frac{\textbf{H},\, a \leq b \;\;\vdash \;\; \textbf{Q}(b-a+1) \qquad \textbf{H},\, b < a \;\;\vdash \;\; \textbf{Q}(0) }{\textbf{H} \;\;\vdash\;\; \textbf{Q}(\card\,(a\upto b))}</math> || where <math>\mathbf{Q}</math> is WD strict || M | ||
{{RRRow}}| | {{RRRow}}| ||{{Rulename|CARD_EMPTY_INTERV}}|| <math>\frac{\textbf{H},\, a \leq b,\,\textbf{P}(b-a+1) \;\;\vdash \;\; \textbf{Q} \qquad \textbf{H},\, b < a ,\, \textbf{P}(0)\;\;\vdash \;\; \textbf{Q} }{\textbf{H},\,\textbf{P}(\card\,(a\upto b)) \;\;\vdash\;\; \textbf{Q}}</math> || where <math>\mathbf{P}</math> is WD strict || M | ||
{{RRRow}}|*||{{Rulename|DERIV_LE_CARD}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; S \subseteq T}{\textbf{H} \;\;\vdash\;\; \card(S) \leq \card(T)}</math> || <math>S</math> and <math>T</math> bear the same type || M | {{RRRow}}|*||{{Rulename|DERIV_LE_CARD}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; S \subseteq T}{\textbf{H} \;\;\vdash\;\; \card(S) \leq \card(T)}</math> || <math>S</math> and <math>T</math> bear the same type || M | ||
Line 169: | Line 213: | ||
{{RRRow}}|*||{{Rulename|DERIV_EQUAL_CARD}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; S = T}{\textbf{H} \;\;\vdash\;\; \card(S) = \card(T)}</math> || <math>S</math> and <math>T</math> bear the same type || M | {{RRRow}}|*||{{Rulename|DERIV_EQUAL_CARD}}|| <math>\frac{\textbf{H} \;\;\vdash\;\; S = T}{\textbf{H} \;\;\vdash\;\; \card(S) = \card(T)}</math> || <math>S</math> and <math>T</math> bear the same type || M | ||
{{RRRow}}| ||{{Rulename|SIMP_CARD_SETMINUS_L}}||<math>\frac{\textbf{H},\, \textbf{P}(\card (S \setminus T)) \;\;\vdash\;\; \finite(S) \qquad \textbf{H},\, \textbf{P}(\card(S) - \card(S\binter T)) \;\;\vdash\;\; \textbf{G}}{\textbf{H},\, \textbf{P}(\card (S \setminus T)) \;\;\vdash\;\; \textbf{G}} </math>|| || M | |||
{{RRRow}}| ||{{Rulename|SIMP_CARD_SETMINUS_R}}||<math>\frac{\textbf{H} \;\;\vdash\;\; \finite(S) \qquad \textbf{H} \;\;\vdash\;\; \textbf{P}(\card(S) - \card(S\binter T))}{\textbf{H} \;\;\vdash\;\; \textbf{P}(\card (S \setminus T))} </math>|| || M | |||
{{RRRow}}| ||{{Rulename|SIMP_CARD_CPROD_L}}||<math>\frac{\textbf{H},\, \textbf{P}(\card (S \cprod T)) \;\;\vdash\;\; \finite(S) \qquad \textbf{H},\, \textbf{P}(\card (S \cprod T)) \;\;\vdash\;\; \finite(T) \qquad \textbf{H},\, \textbf{P}(\card(S) * \card(T)) \;\;\vdash\;\; \textbf{G}}{\textbf{H},\, \textbf{P}(\card (S \cprod T)) \;\;\vdash\;\; \textbf{G}} </math>|| || M | |||
{{RRRow}}| ||{{Rulename|SIMP_CARD_CPROD_R}}||<math>\frac{\textbf{H} \;\;\vdash\;\; \finite(S) \qquad \textbf{H} \;\;\vdash\;\; \finite(T) \qquad \textbf{H} \;\;\vdash\;\; \textbf{P}(\card(S) * \card(T))}{\textbf{H} \;\;\vdash\;\; \textbf{P}(\card (S \cprod T))} </math>|| || M | |||
{{RRRow}}|*||{{Rulename|FORALL_INST}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} , [x \bcmeq E]\textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \forall x \qdot \textbf{P} \;\;\vdash\;\; \textbf{G}}</math> || <math>x</math> is instantiated with <math>E</math> || M | {{RRRow}}|*||{{Rulename|FORALL_INST}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} , [x \bcmeq E]\textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \forall x \qdot \textbf{P} \;\;\vdash\;\; \textbf{G}}</math> || <math>x</math> is instantiated with <math>E</math> || M | ||
{{RRRow}}|*||{{Rulename|FORALL_INST_MP}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H}, {WD}(E) \;\;\vdash \;\; [x \bcmeq E]\textbf{P} \qquad \textbf{H}, {WD}(E), [x \bcmeq E]\textbf{Q} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \forall x \qdot \textbf{P} \limp \textbf{Q} \;\;\vdash\;\; \textbf{G}}</math> || <math>x</math> is instantiated with <math>E</math> and a Modus Ponens is applied|| M | {{RRRow}}|*||{{Rulename|FORALL_INST_MP}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H}, {WD}(E) \;\;\vdash \;\; [x \bcmeq E]\textbf{P} \qquad \textbf{H}, {WD}(E), [x \bcmeq E]\textbf{Q} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \forall x \qdot \textbf{P} \limp \textbf{Q} \;\;\vdash\;\; \textbf{G}}</math> || <math>x</math> is instantiated with <math>E</math> and a Modus Ponens is applied|| M | ||
{{RRRow}}|*||{{Rulename|FORALL_INST_MT}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H}, {WD}(E) \;\;\vdash \;\; [x \bcmeq E]\lnot\textbf{Q} \qquad \textbf{H}, {WD}(E), [x \bcmeq E]\lnot\textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \forall x \qdot \textbf{P} \limp \textbf{Q} \;\;\vdash\;\; \textbf{G}}</math> || <math>x</math> is instantiated with <math>E</math> and a Modus Tollens is applied|| M | |||
{{RRRow}}|*||{{Rulename|CUT}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(\textbf{P}) \qquad \textbf{H}, {WD}(\textbf{P}) \;\;\vdash \;\; \textbf{\textbf{P}} \qquad \textbf{H}, {WD}(\textbf{P}), \textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H} \;\;\vdash\;\; \textbf{G}}</math> || hypothesis <math>\textbf{P}</math> is added || M | {{RRRow}}|*||{{Rulename|CUT}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(\textbf{P}) \qquad \textbf{H}, {WD}(\textbf{P}) \;\;\vdash \;\; \textbf{\textbf{P}} \qquad \textbf{H}, {WD}(\textbf{P}), \textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H} \;\;\vdash\;\; \textbf{G}}</math> || hypothesis <math>\textbf{P}</math> is added || M | ||
Line 180: | Line 232: | ||
{{RRRow}}|*||{{Rulename|DISTINCT_CASE}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(\textbf{P}) \qquad \textbf{H}, {WD}(\textbf{P}), \textbf{P} \;\;\vdash \;\; \textbf{\textbf{G}} \qquad \textbf{H}, {WD}(\textbf{P}), \lnot \textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H} \;\;\vdash\;\; \textbf{G}}</math> || case distinction on predicate <math>\textbf{P}</math> || M | {{RRRow}}|*||{{Rulename|DISTINCT_CASE}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(\textbf{P}) \qquad \textbf{H}, {WD}(\textbf{P}), \textbf{P} \;\;\vdash \;\; \textbf{\textbf{G}} \qquad \textbf{H}, {WD}(\textbf{P}), \lnot \textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H} \;\;\vdash\;\; \textbf{G}}</math> || case distinction on predicate <math>\textbf{P}</math> || M | ||
{{RRRow}}| ||{{Rulename|ONE_POINT_L}}||<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H}, \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} \;\;\vdash \;\; \textbf{G}}{ \textbf{H}, \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} \;\;\vdash\;\; \textbf{G}}</math>|| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> || A | {{RRRow}}|*||{{Rulename|ONE_POINT_L}}||<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H}, \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} \;\;\vdash \;\; \textbf{G}}{ \textbf{H}, \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} \;\;\vdash\;\; \textbf{G}}</math>|| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> || A | ||
{{RRRow}}| ||{{Rulename|ONE_POINT_R}}||<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H} \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }</math>|| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> || A | {{RRRow}}|*||{{Rulename|ONE_POINT_R}}||<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H} \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }</math>|| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> || A | ||
{{RRRow}}|*||{{Rulename|SIM_OV_REL}}|| <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\rel B} </math> || where <math>\mathit{op}</math> is one of <math>\rel</math>, <math>\trel</math>, <math>\srel</math>, <math>\strel</math>, <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math> || A | |||
{{RRRow}}|*||{{Rulename|SIM_OV_TREL}}|| <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\trel B} </math> || where <math>\mathit{op}</math> is one of <math>\trel</math>, <math>\strel</math>, <math>\tfun</math>,<math>\tinj</math>, <math>\tsur</math>, <math>\tbij</math> || A | |||
{{RRRow}}|*||{{Rulename|SIM_OV_PFUN}}|| <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\pfun 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> || 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}, 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, \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 | |||
|} | |||
Those following rules have been implemented in the reasoner GeneralizedModusPonens. | |||
{{RRHeader}} | |||
{{RRRow}}|*||{{Rulename|GENMP_HYP_HYP}}|| <math> \frac{P,\varphi(\btrue) \vdash G}{P,\varphi(P^{\dagger}) \vdash G} </math> || see below for <math> P^{\dagger} </math> || A | |||
{{RRRow}}|*||{{Rulename|GENMP_NOT_HYP_HYP}}|| <math> \frac{nP^{\dagger},\varphi(\bfalse) \vdash G}{nP^{\dagger},\varphi(P) \vdash G} </math> || see below for <math> P^{\dagger} </math> || A | |||
{{RRRow}}|*||{{Rulename|GENMP_HYP_GOAL}}|| <math> \frac{P \vdash \varphi(\btrue)}{P \vdash \varphi(P^{\dagger})} </math> || see below for <math> P^{\dagger} </math> || A | |||
{{RRRow}}|*||{{Rulename|GENMP_NOT_HYP_GOAL}}|| <math> \frac{nP^{\dagger} \vdash \varphi(\bfalse)}{nP^{\dagger} \vdash \varphi(P)} </math> || see below for <math> P^{\dagger} </math> || A | |||
{{RRRow}}|*||{{Rulename|GENMP_GOAL_HYP}}|| <math> \frac{H,\varphi(\bfalse)\vdash \lnot nG^{\dagger}}{H,\varphi(G)\vdash \lnot nG^{\dagger}} </math> || see below for <math> nG^{\dagger} </math> || A | |||
{{RRRow}}|*||{{Rulename|GENMP_NOT_GOAL_HYP}}|| <math> \frac{H,\varphi(\btrue)\vdash \lnot G}{H,\varphi(G^{\dagger})\vdash \lnot G} </math> || see below for <math> G^{\dagger} </math> || A | |||
{{RRRow}}|*||{{Rulename|GENMP_OR_GOAL_HYP}}|| <math> \frac{H,\varphi(\bfalse)\vdash G_1\lor\cdots\lor \lnot nG_i^{\dagger}\lor\cdots\lor G_n}{H,\varphi(G_i)\vdash G_1\lor\cdots\lor \lnot nG_i^{\dagger}\lor\cdots\lor G_n} </math> || see below for <math> nG_i^{\dagger} </math> || A | |||
{{RRRow}}|*||{{Rulename|GENMP_OR_NOT_GOAL_HYP}}|| <math> \frac{H,\varphi(\btrue)\vdash G_1\lor\cdots\lor\ \lnot G_i\lor\cdots\lor G_n}{H,\varphi(G_i^{\dagger})\vdash G_1\lor\cdots\lor\ \lnot G_i\lor\cdots\lor G_n} </math> || see below for <math> G_i^{\dagger} </math> || A | |||
|} | |} | ||
Thos following rules have been implemented in the MembershipGoal reasoner. | |||
{{RRHeader}} | |||
{{RRRow}}|*||{{Rulename|SUBSET_SUBSETEQ}}|| <math> A\subset B\vdash A\subseteq B </math> || || A | |||
{{RRRow}}|*||{{Rulename|DOM_SUBSET}}|| <math> A\subseteq B\vdash \dom(A)\subseteq\dom(B)</math> || || A | |||
{{RRRow}}|*||{{Rulename|RAN_SUBSET}}|| <math> A\subseteq B\vdash \ran(A)\subseteq\ran(B)</math> || || A | |||
{{RRRow}}|*||{{Rulename|EQUAL_SUBSETEQ_LR}}|| <math> A=B\vdash A\subseteq B</math> || || A | |||
{{RRRow}}|*||{{Rulename|EQUAL_SUBSETEQ_RL}}|| <math> A=B\vdash B\subseteq A</math> || || A | |||
{{RRRow}}|*||{{Rulename|IN_DOM_CPROD}}|| <math> x\in\dom(A\cprod B)\vdash x\in A</math> || || A | |||
{{RRRow}}|*||{{Rulename|IN_RAN_CPROD}}|| <math> y\in\ran(A\cprod B)\vdash y\in B</math> || || A | |||
{{RRRow}}|*||{{Rulename|IN_DOM_REL}}|| <math> x\mapsto y\in f\vdash x\in\dom(f)</math> || || A | |||
{{RRRow}}|*||{{Rulename|IN_RAN_REL}}|| <math> x\mapsto y\in f\vdash y\in\ran(f)</math> || || A | |||
{{RRRow}}|*||{{Rulename|SETENUM_SUBSET}}|| <math> \left\{a,\cdots,x,\cdots, z\right\}\subseteq A\vdash x\in A</math> || || A | |||
{{RRRow}}|*||{{Rulename|OVR_RIGHT_SUBSET}}|| <math> f\ovl\cdots\ovl g\ovl\cdots\ovl h\subseteq A\vdash g\ovl\cdots\ovl h\subseteq A</math> || || A | |||
{{RRRow}}|*||{{Rulename|RELSET_SUBSET_CPROD}}|| <math> f\in A\;op\;B\vdash f\subseteq A\cprod B</math> || where <math>\mathit{op}</math> is one of <math>\rel</math>, <math>\trel</math>, <math>\srel</math>, <math>\strel</math>, <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math> || A | |||
{{RRRow}}|*||{{Rulename|DERIV_IN_SUBSET}}|| <math> x\in A,\;\; A\subseteq B\vdash x\in B </math> || || A | |||
|} | |||
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|}}}" | |||
! <math>\textbf{P}</math> !! <math>\textbf{P}^{\dagger}</math> !! <math>\textbf{nP}^{\dagger}</math> !! Side Condition | |||
{{RRRow}}| <math> a = b </math> || <math> a = b, \ \ b = a </math> <br /> <math> a \le b , \ \ b \ge a </math> <br /> <math> a \ge b , \ \ b \le a </math> || <math> \lnot a = b, \ \ \lnot b = a </math> <br /> <math> a > b, \ \ b < a </math> <br /> <math> a < b, \ \ b > a </math> || where a and b are integers | |||
{{RRRow}}| <math> a < b </math> || <math> a < b, \ \ b > a </math> <br /> <math> a \le b, \ \ b \ge a </math> <br /> <math> \lnot a = b, \ \ \lnot b = a </math> || <math> a \ge b, \ \ b \le a </math> <br /> <math> a > b, \ \ b < a </math> <br /> <math> a = b, \ \ b = a </math> || | |||
{{RRRow}}| <math> a > b </math> || <math> a > b, \ \ b < a </math> <br /> <math> a \ge b, \ \ b \le a </math> <br /> <math> \lnot a = b, \ \ \lnot b = a </math> || <math> a \le b, \ \ b \ge a </math> <br /> <math> a < b, \ \ b > a </math> <br /> <math> a = b, \ \ b = a </math> || | |||
{{RRRow}}| <math> a \le b </math> || <math> a \le b, \ \ b \ge a </math> || <math> a > b, \ \ b < a </math> || | |||
{{RRRow}}| <math> a \ge b </math> || <math> a \ge b, \ \ b \le a </math> || <math> a < b, \ \ b > a </math> || | |||
{{RRRow}}| <math> \lnot a = b </math> || <math> \lnot a = b, \ \ \lnot b = a </math> || <math> a = b, \ \ b = a </math> || | |||
{{RRRow}}| <math> A = B </math> || <math> A = B, \ \ B = A </math> <br /> <math> A \subseteq B, \ \ B \subseteq A </math> <br /> <math> \lnot A \subset B, \ \ \lnot B \subset A </math> || <math> \lnot A = B, \ \ \lnot B = A </math> <br /> <math> \lnot A \subseteq B, \ \ \lnot B \subseteq A </math> <br /> <math> \ \ A \subset B, \ \ B \subset A </math> || where A and B are sets | |||
{{RRRow}}| <math> A \subseteq B </math> || <math> A \subseteq B, \lnot B \subset A </math> || <math> \lnot A \subseteq B, B \subset A </math> || | |||
{{RRRow}}| <math> A \subset B </math> || <math> A \subset B, \ \ A \subseteq B </math> <br /> <math> \lnot B \subset A, \ \ \lnot B \subseteq A </math> <br /> <math> \lnot A = B, \ \ \lnot B = A</math> || <math> \lnot A \subset B, \ \ \lnot A \subseteq B </math> <br /> <math> B \subset A, \ \ B \subseteq A </math> <br /> <math> A = B, \ \ B = A </math>|| | |||
{{RRRow}}| <math> \lnot A = B </math> || <math> \lnot A = B, \ \ \lnot B = A </math> || <math> A = B, \ \ B = A </math> || | |||
{{RRRow}}| <math> \lnot A \subseteq B </math> || <math> \lnot A \subseteq B, \ \ \lnot A \subset B </math> <br /> <math> \lnot A = B, \ \ \lnot B = A </math> || <math> A \subseteq B, \ \ A \subset B </math> <br /> <math> A = B, \ \ B = A </math> || | |||
{{RRRow}}| <math> \lnot A \subset B </math> || <math> \lnot A \subset B </math> || <math> A \subset B </math> || | |||
{{RRRow}}| <math> e = f </math> || <math> e = f, \ \ f = e </math> ||<math> \lnot e = f, \ \ \lnot f = e </math> || where e and f are scalars | |||
{{RRRow}}| <math> \lnot e = f </math> || <math> \lnot e = f, \ \ \lnot f = e </math> || <math> e = f, \ \ f = e </math> || | |||
{{RRRow}}| <math> \textbf{P} </math> || <math> \textbf{P} </math> || <math> \lnot \textbf{P} </math> || | |||
{{RRRow}}| <math> \lnot \textbf{P} </math> || || <math> \textbf{P} </math> || | |||
|} | |||
See also [[Extension Proof Rules#Inference Rules]]. | |||
[[Category:User documentation|The Proving Perspective]] | [[Category:User documentation|The Proving Perspective]] | ||
[[Category:Rodin Platform|The Proving Perspective]] | [[Category:Rodin Platform|The Proving Perspective]] | ||
[[Category:User manual|The Proving Perspective]] | [[Category:User manual|The Proving Perspective]] |
Revision as of 10:22, 1 February 2024
CAUTION! Any modification to this page shall be announced on the User mailing list!
Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Inference_Rules.
Name | Rule | Side Condition | A/M
| |
---|---|---|---|---|
* | HYP |
see below for | A
| |
* | HYP_OR |
see below for | A
| |
* | CNTR |
see below for | A
| |
* | FALSE_HYP |
A
| ||
* | TRUE_GOAL |
A
| ||
* | FUN_GOAL |
where and denote types and is one of , , , , , , . | A
| |
* | FUN_IMAGE_GOAL |
where denotes a set of relations (any arrow) and is WD strict | M
| |
FUN_GOAL_REC |
where and denote types, denotes a set of relations (any arrow) and is one of , , , , , , . | A
| ||
* | DBL_HYP |
A
| ||
* | AND_L |
A
| ||
* | AND_R |
A
| ||
IMP_L1 |
A
| |||
* | IMP_R |
A
| ||
* | IMP_AND_L |
A
| ||
* | IMP_OR_L |
A
| ||
* | AUTO_MH |
A
| ||
* | NEG_IN_L |
A
| ||
* | NEG_IN_R |
A
| ||
* | XST_L |
A
| ||
* | ALL_R |
A
| ||
* | EQL_LR |
is a variable which is not free in | A
| |
* | EQL_RL |
is a variable which is not free in | A
| |
SUBSET_INTER |
where and are not bound by | A
| ||
IN_INTER |
where and are not bound by | A
| ||
NOTIN_INTER |
where and are not bound by | A
| ||
* | FIN_L_LOWER_BOUND_L |
The goal is discharged | A
| |
* | FIN_L_LOWER_BOUND_R |
The goal is discharged | A
| |
* | FIN_L_UPPER_BOUND_L |
The goal is discharged | A
| |
* | FIN_L_UPPER_BOUND_R |
The goal is discharged | A
| |
* | CONTRADICT_L |
M
| ||
* | CONTRADICT_R |
M
| ||
* | CASE |
M
| ||
* | IMP_CASE |
M
| ||
* | MH |
M
| ||
* | HM |
M
| ||
* | EQV_LR |
M
| ||
* | EQV_RL |
M
| ||
* | OV_SETENUM_L |
where is WD strict | A
| |
* | OV_SETENUM_R |
where is WD strict | A
| |
* | OV_L |
where is WD strict | A
| |
* | OV_R |
where is WD strict | A
| |
* | DIS_BINTER_R |
where and denote types. | M
| |
* | DIS_BINTER_L |
where and denote types. | M
| |
* | DIS_SETMINUS_R |
where and denote types. | M
| |
* | DIS_SETMINUS_L |
where and denote types. | M
| |
* | SIM_REL_IMAGE_R |
M
| ||
* | SIM_REL_IMAGE_L |
M
| ||
* | SIM_FCOMP_R |
M
| ||
* | SIM_FCOMP_L |
M
| ||
* | FIN_SUBSETEQ_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_BINTER_R |
M
| ||
* | FIN_KINTER_R |
where is fresh | M
| |
* | FIN_QINTER_R |
M
| ||
* | FIN_BUNION_R |
M
| ||
* | FIN_KUNION_R |
where is fresh | M
| |
* | FIN_QUNION_R |
M
| ||
* | FIN_SETMINUS_R |
M
| ||
FIN_COMPSET_R |
M
| |||
FIN_REL |
where denotes a set of relations (any arrow) | A
| ||
* | FIN_REL_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_REL_IMG_R |
M
| ||
* | FIN_REL_RAN_R |
M
| ||
* | FIN_REL_DOM_R |
M
| ||
FIN_FUN_DOM |
where is one of , , , , , , | A
| ||
FIN_FUN_RAN |
where is one of , , | A
| ||
* | FIN_FUN1_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_FUN2_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_FUN_IMG_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_FUN_RAN_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_FUN_DOM_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | LOWER_BOUND_L |
must not contain any bound variable | M
| |
* | LOWER_BOUND_R |
must not contain any bound variable | M
| |
* | UPPER_BOUND_L |
must not contain any bound variable | M
| |
* | UPPER_BOUND_R |
must not contain any bound variable | M
| |
* | FIN_LT_0 |
M
| ||
* | FIN_GE_0 |
M
| ||
CARD_INTERV |
where is WD strict | M
| ||
CARD_EMPTY_INTERV |
where is WD strict | M
| ||
* | DERIV_LE_CARD |
and bear the same type | M
| |
* | DERIV_GE_CARD |
and bear the same type | M
| |
* | DERIV_LT_CARD |
and bear the same type | M
| |
* | DERIV_GT_CARD |
and bear the same type | M
| |
* | DERIV_EQUAL_CARD |
and bear the same type | M
| |
SIMP_CARD_SETMINUS_L |
M | |||
SIMP_CARD_SETMINUS_R |
M
| |||
SIMP_CARD_CPROD_L |
M | |||
SIMP_CARD_CPROD_R |
M
| |||
* | FORALL_INST |
is instantiated with | M
| |
* | FORALL_INST_MP |
is instantiated with and a Modus Ponens is applied | M
| |
* | FORALL_INST_MT |
is instantiated with and a Modus Tollens is applied | M
| |
* | CUT |
hypothesis is added | M
| |
* | EXISTS_INST |
is instantiated with | M
| |
* | DISTINCT_CASE |
case distinction on predicate | M
| |
* | ONE_POINT_L |
The rule can be applied with as well as with | A
| |
* | ONE_POINT_R |
The rule can be applied with as well as with | A
| |
* | SIM_OV_REL |
where is one of , , , , , , , , , , | A
| |
* | SIM_OV_TREL |
where is one of , , ,, , | A
| |
* | SIM_OV_PFUN |
where is one of , , , , , , | A
| |
* | SIM_OV_TFUN |
where is one of , , , | A
| |
INDUC_NAT |
of type appears free in ; is introduced as a fresh identifier | M
| ||
INDUC_NAT_COMPL |
of type appears free in ; is introduced as a fresh identifier | M
|
Those following rules have been implemented in the reasoner GeneralizedModusPonens.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | GENMP_HYP_HYP |
see below for | A | |
* | GENMP_NOT_HYP_HYP |
see below for | A | |
* | GENMP_HYP_GOAL |
see below for | A | |
* | GENMP_NOT_HYP_GOAL |
see below for | A | |
* | GENMP_GOAL_HYP |
see below for | A | |
* | GENMP_NOT_GOAL_HYP |
see below for | A | |
* | GENMP_OR_GOAL_HYP |
see below for | A | |
* | GENMP_OR_NOT_GOAL_HYP |
see below for | A |
Thos following rules have been implemented in the MembershipGoal reasoner.
Name | Rule | Side Condition | A/M
| |
---|---|---|---|---|
* | SUBSET_SUBSETEQ |
A | ||
* | DOM_SUBSET |
A | ||
* | RAN_SUBSET |
A | ||
* | EQUAL_SUBSETEQ_LR |
A | ||
* | EQUAL_SUBSETEQ_RL |
A | ||
* | IN_DOM_CPROD |
A | ||
* | IN_RAN_CPROD |
A | ||
* | IN_DOM_REL |
A | ||
* | IN_RAN_REL |
A | ||
* | SETENUM_SUBSET |
A | ||
* | OVR_RIGHT_SUBSET |
A | ||
* | RELSET_SUBSET_CPROD |
where is one of , , , , , , , , , , | A | |
* | DERIV_IN_SUBSET |
A |
The conventions used in this table are described in Variations in HYP, CNTR and GenMP.
Side Condition | |||
---|---|---|---|
|
|
where a and b are integers | |
|
|
||
|
|
||
|
|
where A and B are sets | |
|
|
||
|
|
||
where e and f are scalars | |||
See also Extension Proof Rules#Inference Rules.