Inference Rules

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_BUNION_R	$\frac{\textbf{H} \;\;\vdash \;\;\finite\,(S) \;\land\;\ldots \;\land\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\bunion\;\ldots \;\bunion\; T)}$		M
*	FIN_KUNION_R	$\frac{\textbf{H} \;\;\vdash \;\; \finite\,(S) \;\land\; (\forall s\, \qdot\, s \in S \limp \finite\,(s))}{\textbf{H} \;\;\vdash \;\; \finite\,(\union(S))}$	where $s$ is fresh	M
*	FIN_QUNION_R	$\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)}$		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.