Inference Rules

From Event-B
Revision as of 14:52, 30 March 2011 by imported>Nicolas (NEG_IN_L and NEG_IN_R back to implemented status, after checking implementation)
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 \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


*
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}} 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 \mathbf{Q} is WD strict, 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 \mathbf{Q} is WD strict, 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 \mathbf{Q} is WD strict, 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 \mathbf{Q} is WD strict, 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_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))} 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}} where \mathbf{P} is WD strict 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))} where \mathbf{P} is WD strict 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}} where \mathbf{P} is WD strict 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))} where \mathbf{P} is WD strict 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

See also Extension Proof Rules#Inference Rules.

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