Difference between revisions of "Inference Rules"

From Event-B
Jump to navigationJump to search
imported>Billaude
(Add inference rules used in MapOvrGoal, MembershipGoal (so far), GeneralizedModusPonens and the AutoRewriterL3.)
imported>Nicolas
m (Removed induction on integers (was wrong), reviewed induciton on naturals)
 
(18 intermediate revisions by 4 users not shown)
Line 10: Line 10:
 
{{RRHeader}}
 
{{RRHeader}}
  
{{RRRow}}|*||{{Rulename|HYP}}|| <math>\frac{}{\textbf{H},\textbf{P} \;\;\vdash \;\; \textbf{P}} </math>|| || A
+
{{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> || || A
+
{{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},\;\neg\,\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math> || || A
+
{{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 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   
Line 217: Line 221:
 
{{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 x\in A}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto\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_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 x\in A}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto\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_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 x\in A}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto\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_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
  
{{RRRow}}|*||{{Rulename|SIM_OV_TFUN}}|| <math> \frac{\textbf{H}\vdash x\in A\qquad \textbf{H}\vdash x\in A}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto\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
 
  
 
|}
 
|}
Line 230: Line 239:
 
Those following rules have been implemented in the reasoner GeneralizedModusPonens.
 
Those following rules have been implemented in the reasoner GeneralizedModusPonens.
 
{{RRHeader}}
 
{{RRHeader}}
{{RRRow}}|*||{{Rulename|GENMP_HYP_HYP}}|| <math> \frac{P,\varphi(\btrue) \vdash G}{P,\varphi(P) \vdash G} </math> ||  || A
+
{{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{\lnot P,\varphi(\bfalse) \vdash G}{\lnot P,\varphi(P) \vdash G} </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)} </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{\lnot P \vdash \varphi(\bfalse)}{\lnot P \vdash \varphi(P)} </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 G}{H,\varphi(G)\vdash G} </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\neg G}{H,\varphi(G)\vdash\neg G} </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 G_i\lor\cdots\lor G_n}{H,\varphi(G_i)\vdash G_1\lor\cdots\lor G_i\lor\cdots\lor G_n} </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\neg G_i\lor\cdots\lor G_n}{H,\varphi(G_i)\vdash G_1\lor\cdots\lor\neg G_i\lor\cdots\lor G_n} </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
  
 
|}
 
|}
Line 248: Line 257:
 
{{RRRow}}|*||{{Rulename|DOM_SUBSET}}|| <math> A\subseteq B\vdash \dom(A)\subseteq\dom(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|RAN_SUBSET}}|| <math> A\subseteq B\vdash \ran(A)\subseteq\ran(B)</math> ||  || A
{{RRRow}}|*||{{Rulename|EQUAL_SUBSET_LR}}|| <math> A=B\vdash A\subseteq B</math> ||  || A
+
{{RRRow}}|*||{{Rulename|EQUAL_SUBSETEQ_LR}}|| <math> A=B\vdash A\subseteq B</math> ||  || A
{{RRRow}}|*||{{Rulename|EQUAL_SUBSET_RL}}|| <math> A=B\vdash B\subseteq A</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_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_RAN_CPROD}}|| <math> y\in\ran(A\cprod B)\vdash y\in B</math> ||  || A
Line 257: Line 266:
 
{{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|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|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]].
 
See also [[Extension Proof Rules#Inference Rules]].

Latest revision as of 16:00, 23 June 2014

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
\frac{}{\textbf{H},\textbf{P} \;\;\vdash \;\; \textbf{P}^{\dagger}} see below for \textbf{P}^{\dagger} A


*
HYP_OR
\frac{}{\textbf{H},\textbf{Q} \;\;\vdash \;\; \textbf{P} \lor \ldots \lor  \textbf{Q}^{\dagger} \lor \ldots \lor \textbf{R}} see below for \textbf{Q}^{\dagger} A


*
CNTR
\frac{}{\textbf{H},\;\textbf{P},\;\textbf{nP}^{\dagger} \;\;\vdash \;\; \textbf{Q}} see below for \textbf{nP}^{\dagger} A


*
FALSE_HYP
\frac{}{\textbf{H},\bfalse \;\;\vdash \;\; \textbf{P}} A


*
TRUE_GOAL
\frac{}{\textbf{H} \;\;\vdash \;\; \btrue} A


*
FUN_GOAL
\frac{}{\textbf{H},\; f\in E\;\mathit{op}\;F \;\;\vdash\;\; f\in T_1\pfun T_2} where T_1 and T_2 denote types and \mathit{op} is one of \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij. A


*
FUN_IMAGE_GOAL
\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))} where \mathit{op} denotes a set of relations (any arrow) and \mathbf{P} is WD strict M


FUN_GOAL_REC
\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} where T_1 and T_2 denote types, \mathit{op} denotes a set of relations (any arrow) and \mathit{opf} is one of \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij. A


*
DBL_HYP
\frac{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H},\;\textbf{P},\;\textbf{P}  \;\;\vdash \;\; \textbf{Q}} A


*
AND_L
\frac{\textbf{H},\textbf{P},\textbf{Q} \; \; \vdash \; \;  \textbf{R}}{\textbf{H},\; \textbf{P} \land \textbf{Q} \; \; \vdash \; \;  
\textbf{R}} A


*
AND_R
\frac{\textbf{H} \; \; \vdash \; \;  \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \;  \textbf{P} \; \land \; \textbf{Q}} A


IMP_L1
\frac{\textbf{H},\; \textbf{Q},\; \textbf{P} \land \ldots \land \textbf{R} \limp \textbf{S} \;\;\vdash \;\; \textbf{T}}{\textbf{H},\; \textbf{Q},\; \textbf{P} \land \ldots \land \textbf{Q} \land \ldots \land \textbf{R} \limp \textbf{S} \;\;\vdash \;\; \textbf{T} } A


*
IMP_R
\frac{\textbf{H}, \textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H} \;\;\vdash \;\; \textbf{P} \limp \textbf{Q}} A


*
IMP_AND_L
\frac{\textbf{H},\textbf{P} \limp \textbf{Q},  \textbf{P} \limp \textbf{R}\;\;\vdash \;\; \textbf{S}}{\textbf{H},\;\textbf{P} \limp  \textbf{Q} \land \textbf{R}  \;\;\vdash \;\; \textbf{S}} A


*
IMP_OR_L
\frac{
\textbf{H},\textbf{P} \limp \textbf{R},  \textbf{Q} \limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P} \lor  \textbf{Q} \limp \textbf{R}  \;\;\vdash \;\; \textbf{S}} A


*
AUTO_MH
\frac{
\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}} A


*
NEG_IN_L
\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} } A


*
NEG_IN_R
\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} } A


*
XST_L
\frac{\textbf{H},\;  \textbf{P(x)} \; \; \vdash \; \;  \textbf{Q}
}{
\textbf{H},\;  \exists \, \textbf{x}\, \qdot\, \textbf{P(x)} \; \; \vdash \; \;  \textbf{Q}
} A


*
ALL_R
\frac{\textbf{H}\; \; \vdash \; \;  \textbf{P(x)} }{ \textbf{H} \; \; \vdash \; \;  \forall \textbf{x}\, \qdot\, \textbf{P(x)} } A


*
EQL_LR
\frac{\textbf{H(E)} \; \; \vdash \; \; \textbf{P(E)} }{\textbf{H(x)},\; x=E \; \; \vdash \; \;  \textbf{P(x)} } x is a variable which is not free in E A


*
EQL_RL
\frac{\textbf{H(E)} \; \; \vdash \; \; \textbf{P(E)} }{\textbf{H(x)},\; E=x \; \; \vdash \; \;  \textbf{P(x)} } x is a variable which is not free in E A


SUBSET_INTER
\frac{\textbf{H},\;\textbf{T} \subseteq \textbf{U} \;\;\vdash \;\; 
\textbf{G}(\textbf{S} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{V})}
{\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})} where \mathbf{T} and \mathbf{U} are not bound by \mathbf{G} A


IN_INTER
\frac{\textbf{H},\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; 
\textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{U})}
{\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})} where \mathbf{E} and \mathbf{T} are not bound by \mathbf{G} A


NOTIN_INTER
\frac{\textbf{H},\;\lnot\;\textbf{E} \in \textbf{T} \;\;\vdash \;\; 
\textbf{G}(\emptyset)}
{\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})} where \mathbf{E} and \mathbf{T} are not bound by \mathbf{G} A


*
FIN_L_LOWER_BOUND_L
\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)} The goal is discharged A


*
FIN_L_LOWER_BOUND_R
\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \geq n)} The goal is discharged A


*
FIN_L_UPPER_BOUND_L
\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \geq x)} The goal is discharged A


*
FIN_L_UPPER_BOUND_R
\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \leq n)} The goal is discharged A


*
CONTRADICT_L
\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \neg\,\textbf{P}}{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}} M


*
CONTRADICT_R
\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \bfalse}{\textbf{H} \;\;\vdash \;\; \textbf{Q}} M


*
CASE
\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} } M


*
IMP_CASE
\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} } M


*
MH
\frac{\textbf{H} \;\;\vdash\;\;\textbf{P} \qquad \textbf{H},\; \textbf{Q} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}} M


*
HM
\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}} M


EQV_LR
\frac{\textbf{H(Q)},\; \textbf{P} \leqv \textbf{Q} 
\;\;\vdash\;\; \textbf{G(Q)}}{\textbf{H(P)},\;\textbf{P} \leqv \textbf{Q} 
\;\;\vdash \;\; \textbf{G(P)}} M


EQV_RL
\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)}} M


*
OV_SETENUM_L
\frac{\textbf{H},\; G=E  
,\;\textbf{P}(F)\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,(G=E)  
,\;\textbf{P}((\{E\}) \domsub f)(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl\{E 
\mapsto F\})(G)) \;\;\vdash \;\; \textbf{Q}} where \mathbf{P} is WD strict A


*
OV_SETENUM_R
\frac{\textbf{H},\; G=E \;\;\vdash\;\;\textbf{Q}(F) 
\qquad \textbf{H},\; \neg\,(G=E)  \;\;\vdash\;\;\textbf{Q}((\{E\}) \domsub f)(G))}{\textbf{H} 
\;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G))} where \mathbf{Q} is WD strict A


*
OV_L
\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}} where \mathbf{P} is WD strict A


*
OV_R
\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))} where \mathbf{Q} is WD strict A


*
DIS_BINTER_R
\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])} where A and B denote types. M


*
DIS_BINTER_L
\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}} where A and B denote types. M


*
DIS_SETMINUS_R
\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])} where A and B denote types. M


*
DIS_SETMINUS_L
\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}} where A and B denote types. M


*
SIM_REL_IMAGE_R
\frac{\textbf{H} \; \; \vdash \; \; {WD}(\textbf{Q}(\{ f(E)\} )) \qquad\textbf{H} \; \; \vdash \; \; \textbf{Q}(\{ f(E)\} ) }{\textbf{H} \; \; \vdash \; \;  \textbf{Q}(f[\{ E\} ])} M


*
SIM_REL_IMAGE_L
\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} } M


*
SIM_FCOMP_R
\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))} M


*
SIM_FCOMP_L
\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}} M


*
FIN_SUBSETEQ_R
\frac{\textbf{H} \;\;\vdash\;\;{WD}(T) \qquad\textbf{H} \;\;\vdash \;\; S \subseteq T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(S)} the user has to write the set corresponding to T in the editing area of the Proof Control Window M


*
FIN_BINTER_R
\frac{\textbf{H} \;\;\vdash 
\;\;\finite\,(S) \;\lor\;\ldots \;\lor\; \finite\,(T)}{\textbf{H} \;\;\vdash 
\;\; \finite\,(S \;\binter\;\ldots \;\binter\; T)} M


FIN_KINTER_R
\frac{\textbf{H} \;\;\vdash 
\;\;\exists s\, \qdot\, s \in S \land \finite\,(s)}{\textbf{H} \;\;\vdash 
\;\; \finite\,(\inter(S))} where s is fresh M


FIN_QINTER_R
\frac{\textbf{H} \;\;\vdash 
\;\;\exists s\, \qdot\, P \land \finite\,(E)}{\textbf{H} \;\;\vdash 
\;\; \finite\,(\Inter s\,\qdot\,P\,\mid\,E)} M


*
FIN_SETMINUS_R
\frac{\textbf{H} \;\;\vdash 
\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)} M


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


*
FIN_REL_R
\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)} the user has to write the set corresponding to S \rel T in the editing area of the Proof Control Window M


*
FIN_REL_IMG_R
\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(r[s])} M


*
FIN_REL_RAN_R
\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\ran(r))} M


*
FIN_REL_DOM_R
\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(r))} M


FIN_FUN_DOM
\frac{}{\textbf{H},\; f\in S\;\mathit{op}\;T,\; \finite\,(S) \;\;\vdash \;\; \finite\,(f)} where \mathit{op} is one of \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij A


FIN_FUN_RAN
\frac{}{\textbf{H},\; f\in S\;\mathit{op}\;T,\; \finite\,(T) \;\;\vdash \;\; \finite\,(f)} where \mathit{op} is one of \pinj, \tinj, \tbij A


*
FIN_FUN1_R
\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)} the user has to write the set corresponding to S  \pfun T in the editing area of the Proof Control Window M


*
FIN_FUN2_R
\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\pfun T) \qquad\textbf{H} \;\;\vdash \;\; f^{-1} \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(f)} the user has to write the set corresponding to S  \pfun T in the editing area of the Proof Control Window M


*
FIN_FUN_IMG_R
\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[s])} the user has to write the set corresponding to S  \pfun T in the editing area of the Proof Control Window M


*
FIN_FUN_RAN_R
\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\,(\ran(f))} the user has to write the set corresponding to S  \pfun T in the editing area of the Proof Control Window M


*
FIN_FUN_DOM_R
\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\pfun T) \qquad\textbf{H} \;\;\vdash \;\; f^{-1} \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(f))} the user has to write the set corresponding to S  \pfun T in the editing area of the Proof Control Window M


*
LOWER_BOUND_L
\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)} S must not contain any bound variable M


*
LOWER_BOUND_R
\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \geq n)} S must not contain any bound variable M


*
UPPER_BOUND_L
\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \geq x)} S must not contain any bound variable M


*
UPPER_BOUND_R
\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \leq n)} S must not contain any bound variable M


*
FIN_LT_0
\frac{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)  \qquad \textbf{H} \;\;\vdash \;\; S \subseteq \intg \setminus \natn }{\textbf{H} \;\;\vdash \;\; \finite(S)} M


*
FIN_GE_0
\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)} M


CARD_INTERV
\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))} where \mathbf{Q} is WD strict M


CARD_EMPTY_INTERV
\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}} where \mathbf{P} is WD strict M


*
DERIV_LE_CARD
\frac{\textbf{H}  \;\;\vdash\;\; S \subseteq T}{\textbf{H} \;\;\vdash\;\; \card(S) \leq \card(T)} S and T bear the same type M


*
DERIV_GE_CARD
\frac{\textbf{H}  \;\;\vdash\;\; T \subseteq S}{\textbf{H} \;\;\vdash\;\; \card(S) \geq \card(T)} S and T bear the same type M


*
DERIV_LT_CARD
\frac{\textbf{H}  \;\;\vdash\;\; S \subset T}{\textbf{H} \;\;\vdash\;\; \card(S) < \card(T)} S and T bear the same type M


*
DERIV_GT_CARD
\frac{\textbf{H}  \;\;\vdash\;\; T \subset S}{\textbf{H} \;\;\vdash\;\; \card(S) > \card(T)} S and T bear the same type M


*
DERIV_EQUAL_CARD
\frac{\textbf{H}  \;\;\vdash\;\; S = T}{\textbf{H} \;\;\vdash\;\; \card(S) = \card(T)} S and T bear the same type M


SIMP_CARD_SETMINUS_L
\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}} M
SIMP_CARD_SETMINUS_R
\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))} M


SIMP_CARD_CPROD_L
\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}} M
SIMP_CARD_CPROD_R
\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))} M


*
FORALL_INST
\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}} x is instantiated with E M


*
FORALL_INST_MP
\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}} x is instantiated with E and a Modus Ponens is applied M


*
FORALL_INST_MT
\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}} x is instantiated with E and a Modus Tollens is applied M


*
CUT
\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}} hypothesis \textbf{P} is added M


*
EXISTS_INST
\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(E)}{\textbf{H} \;\;\vdash\;\; \exists x \qdot \textbf{P}(x)} x is instantiated with E M


*
DISTINCT_CASE
\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}} case distinction on predicate \textbf{P} M


*
ONE_POINT_L
\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}} The rule can be applied with \forall as well as with \exists A


*
ONE_POINT_R
\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} } The rule can be applied with \forall as well as with \exists A


*
SIM_OV_REL
 \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} where \mathit{op} is one of \rel, \trel, \srel, \strel, \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij A


*
SIM_OV_TREL
 \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} where \mathit{op} is one of \trel, \strel, \tfun,\tinj, \tsur, \tbij A


*
SIM_OV_PFUN
 \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} where \mathit{op} is one of \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij A


*
SIM_OV_TFUN
 \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} where \mathit{op} is one of \tfun, \tinj, \tsur, \tbij A


INDUC_NAT
\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)} x of type \intg appears free in \textbf{P}; n is introduced as a fresh identifier M


INDUC_NAT_COMPL
\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)} x of type \intg appears free in \textbf{P}; n 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
 \frac{P,\varphi(\btrue) \vdash G}{P,\varphi(P^{\dagger}) \vdash G} see below for  P^{\dagger} A
*
GENMP_NOT_HYP_HYP
 \frac{nP^{\dagger},\varphi(\bfalse) \vdash G}{nP^{\dagger},\varphi(P) \vdash G} see below for  P^{\dagger} A
*
GENMP_HYP_GOAL
 \frac{P \vdash \varphi(\btrue)}{P \vdash \varphi(P^{\dagger})} see below for  P^{\dagger} A
*
GENMP_NOT_HYP_GOAL
 \frac{nP^{\dagger} \vdash \varphi(\bfalse)}{nP^{\dagger} \vdash \varphi(P)} see below for  P^{\dagger} A
*
GENMP_GOAL_HYP
 \frac{H,\varphi(\bfalse)\vdash \lnot nG^{\dagger}}{H,\varphi(G)\vdash \lnot nG^{\dagger}} see below for  nG^{\dagger} A
*
GENMP_NOT_GOAL_HYP
 \frac{H,\varphi(\btrue)\vdash \lnot G}{H,\varphi(G^{\dagger})\vdash \lnot G} see below for  G^{\dagger} A
*
GENMP_OR_GOAL_HYP
 \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} see below for  nG_i^{\dagger} A
*
GENMP_OR_NOT_GOAL_HYP
 \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} see below for  G_i^{\dagger} A


Thos following rules have been implemented in the MembershipGoal reasoner.

  Name Rule Side Condition A/M


*
SUBSET_SUBSETEQ
 A\subset B\vdash A\subseteq B A
*
DOM_SUBSET
 A\subseteq B\vdash \dom(A)\subseteq\dom(B) A
*
RAN_SUBSET
 A\subseteq B\vdash \ran(A)\subseteq\ran(B) A
*
EQUAL_SUBSETEQ_LR
 A=B\vdash A\subseteq B A
*
EQUAL_SUBSETEQ_RL
 A=B\vdash B\subseteq A A
*
IN_DOM_CPROD
 x\in\dom(A\cprod B)\vdash x\in A A
*
IN_RAN_CPROD
 y\in\ran(A\cprod B)\vdash y\in B A
*
IN_DOM_REL
 x\mapsto y\in f\vdash x\in\dom(f) A
*
IN_RAN_REL
 x\mapsto y\in f\vdash y\in\ran(f) A
*
SETENUM_SUBSET
 \left\{a,\cdots,x,\cdots, z\right\}\subseteq A\vdash x\in A A
*
OVR_RIGHT_SUBSET
 f\ovl\cdots\ovl g\ovl\cdots\ovl h\subseteq A\vdash g\ovl\cdots\ovl h\subseteq A A
*
RELSET_SUBSET_CPROD
 f\in A\;op\;B\vdash f\subseteq A\cprod B where \mathit{op} is one of \rel, \trel, \srel, \strel, \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij A
*
DERIV_IN_SUBSET
 x\in A,\;\; A\subseteq B\vdash x\in B A


The conventions used in this table are described in Variations in HYP, CNTR and GenMP.

\textbf{P} \textbf{P}^{\dagger} \textbf{nP}^{\dagger} Side Condition
 a = b  a = b, \ \ b = a
 a \le b , \ \ b \ge a
 a \ge b , \ \ b \le a
 \lnot a = b, \ \ \lnot b = a
 a > b, \ \ b < a
 a < b, \ \ b > a
where a and b are integers
 a < b  a < b, \ \ b > a
 a \le b, \ \ b \ge a
 \lnot a = b, \ \ \lnot b = a
 a \ge b, \ \ b \le a
 a > b, \ \ b < a
 a = b, \ \ b = a
 a > b  a > b, \ \ b < a
 a \ge b, \ \ b \le a
 \lnot a = b, \ \ \lnot b = a
 a \le b, \ \ b \ge a
 a < b, \ \ b > a
 a = b, \ \ b = a
 a \le b  a \le b, \ \ b \ge a  a > b, \ \ b < a
 a \ge b  a \ge b, \ \ b \le a  a < b, \ \ b > a
 \lnot a = b  \lnot a = b, \ \ \lnot b = a  a = b, \ \ b = a
 A = B  A = B, \ \ B = A
 A \subseteq B, \ \ B \subseteq A
 \lnot A \subset B, \ \ \lnot B \subset A
 \lnot A = B, \ \ \lnot B = A
 \lnot A \subseteq B, \ \ \lnot B \subseteq A
 \ \ A \subset B, \ \ B \subset A
where A and B are sets
 A \subseteq B  A \subseteq B, \lnot B \subset A  \lnot A \subseteq B, B \subset A
 A \subset B  A \subset B, \ \ A \subseteq B
 \lnot B \subset A, \ \ \lnot B \subseteq A
 \lnot A = B, \ \ \lnot B = A
 \lnot A \subset B, \ \ \lnot A \subseteq B
 B \subset A, \ \ B \subseteq A
 A = B, \ \ B = A
 \lnot A = B  \lnot A = B, \ \ \lnot B = A  A = B, \ \ B = A
 \lnot A \subseteq B  \lnot A \subseteq B, \ \ \lnot A \subset B
 \lnot A = B, \ \ \lnot B = A
 A \subseteq B, \ \ A \subset B
 A = B, \ \ B = A
 \lnot A \subset B  \lnot A \subset B  A \subset B
 e = f  e = f, \ \ f = e  \lnot e = f, \ \ \lnot f = e where e and f are scalars
 \lnot e = f  \lnot e = f, \ \ \lnot  f = e  e = f, \ \ f = e
 \textbf{P}  \textbf{P}  \lnot \textbf{P}
 \lnot \textbf{P}  \textbf{P}


See also Extension Proof Rules#Inference Rules.