Inference Rules

From Event-B
Revision as of 12:27, 9 September 2010 by imported>Nicolas (moved datatype rules to extension proof rules page)
Jump to navigationJump to search 
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}} A


*
HYP_OR
 \frac{}{\textbf{H},\textbf{Q} \;\;\vdash \;\; \textbf{P} \lor \ldots \lor \textbf{Q} \lor \ldots \lor \textbf{R}} A


*
CNTR
 \frac{}{\textbf{H},\;\textbf{P},\;\neg\,\textbf{P} \;\;\vdash \;\; \textbf{Q}} 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 f(E) occurs at the top level 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\} \; \; \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\} \; \; \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})} the \binter operator must appear at the "top level" 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})} the \binter operator must appear at the "top level" 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})} the \binter operator must appear at the "top level" 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


*
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
 \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


*
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}} the \ovl operator must appear at the "top level" 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))} the \ovl operator must appear at the "top level" 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}} the \ovl operator must appear at the "top level" 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))} the \ovl operator must appear at the "top level" 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])} the occurrence of f must appear at the "top level". Moreover A and B denote some type. 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}} the occurrence of f must appear at the "top level". Moreover A and B denote some type. 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])} the occurrence of f must appear at the "top level". Moreover A and B denote some type. 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}} the occurrence of f must appear at the "top level". Moreover A and B denote some type. 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\} ])} the occurrence of f must appear at the "top level". 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} } the occurrence of f must appear at the "top level". 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))} the occurrence of f \fcomp g must appear at the "top level". 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}} the occurrence of f \fcomp g must appear at the "top level". 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_SETMINUS_R
 \frac{\textbf{H} \;\;\vdash \;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)} M


*
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_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))} \card (a \upto b) must appear at "top-level" 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}} \card (a \upto b) must appear at "top-level" 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}} \card (S \setminus T) must appear at "top-level" 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))} \card (S \setminus T) must appear at "top-level" 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}} \card (S \cprod T) must appear at "top-level" 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))} \card (S \cprod T) must appear at "top-level" 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


*
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

See also Extension Proof Rules#Inference Rules.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Inference_Rules&oldid=5741’