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
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
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
CASE	$\frac{\textbf{H}, \; \textbf{P} \; \; \vdash \; \; \textbf{R} \ \ \ \ \ldots \ \ \ \ \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{P},\; \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{Q},\; \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_L	$\frac{\textbf{H},\; G=E ,\;\textbf{P}(F)\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,(G=E) ,\;\textbf{P}(f(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl\{E \mapsto F\})(G)) \;\;\vdash \;\; \textbf{Q}}$	the $\ovl$ operator must appear at the "top level"	M
OV_R	$\frac{\textbf{H},\; G=E \;\;\vdash\;\;\textbf{Q}(F) \qquad \textbf{H},\; \neg\,(G=E) \;\;\vdash\;\;\textbf{Q}(f(G))}{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G)) \ \ \ \ \ }$	the $\ovl$ operator must appear at the "top level"	M
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}(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"	M
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}(f(G))}{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f\ovl g)(G)) \ \ \ \ \ }$	the $\ovl$ operator must appear at the "top level"	M
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^{-1}$ must appear at the "top level". Moreover $A$ and $B$ denote some type. Similar left distribution rules exist	M
DIS_SETMINUS_R	$\frac{\textbf{H} \;\;\vdash\;\; f \in A \pfun B \qquad\textbf{H} \;\;\vdash\;\;\textbf{Q}(f^{-1}[S] \setminus f^{-1}[T]) }{\textbf{H} \;\;\vdash \;\; \textbf{Q}(f^{-1}[S \setminus T]) \ \ \ \ \ }$	the occurrence of $f^{-1}$ must appear at the "top level". Moreover $A$ and $B$ denote some type. Similar left distribution rules exist	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". A similar left simplification rule exists.	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". A similar left simplification rule exists.	M
FIN_SUBSETEQ_R	$\frac{\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 \;\; 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]) \ \ \ \ \ \ \ }$	the user has to write the set corresponding to $S \pfun T$ in the editing area of the Proof Control Window	M
FIN_REL_RAN_R	$\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\ran(r)) \ \ \ \ \ \ \ }$	the user has to write the set corresponding to $S \pfun T$ in the editing area of the Proof Control Window	M
FIN_REL_DOM_R	$\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(r)) \ \ \ \ \ \ \ }$	the user has to write the set corresponding to $S \pfun T$ in the editing area of the Proof Control Window	M
FIN_FUN1_R	$\frac{\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 \;\; 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 \;\; 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 \;\; 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 \;\; 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}(a-b+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
CARD_SUBSETEQ	$\frac{\textbf{H} \;\;\vdash \;\; \textbf{P}(S \subseteq T) }{\textbf{H} \;\;\vdash\;\; \textbf{P}(\card\,(S) \leq \card(T))}$		M

Some rules are not yet implemented:

• SUBSET_INTER, IN_INTER, NOTIN_INTER.