Inference Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Laurent
Added AUTO_MH
imported>Laurent
m Fixed rule names to make them easy to extract
Line 3: Line 3:
{{RRHeader}}
{{RRHeader}}


{{RRRow}}|*||<font size="-2"> HYP </font>|| <math>\frac{}{\textbf{H},\textbf{P} \;\;\vdash \;\; \textbf{P}} </math>||  || A
{{RRRow}}|*||{{Rulename|HYP}}|| <math>\frac{}{\textbf{H},\textbf{P} \;\;\vdash \;\; \textbf{P}} </math>||  || A


{{RRRow}}|*||<font size="-2"> HYP_OR </font>|| <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} \lor \ldots \lor \textbf{R}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> CNTR </font>|| <math>\frac{}{\textbf{H},\;\textbf{P},\;\neg\,\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math> ||  || A
{{RRRow}}|*||{{Rulename|CNTR}}|| <math>\frac{}{\textbf{H},\;\textbf{P},\;\neg\,\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> FALSE_HYP </font>|| <math>\frac{}{\textbf{H},\bfalse \;\;\vdash \;\; \textbf{P}}</math> ||  || A
{{RRRow}}|*||{{Rulename|FALSE_HYP}}|| <math>\frac{}{\textbf{H},\bfalse \;\;\vdash \;\; \textbf{P}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> TRUE_GOAL </font>|| <math>\frac{}{\textbf{H} \;\;\vdash \;\; \btrue}</math> ||  || A
{{RRRow}}|*||{{Rulename|TRUE_GOAL}}|| <math>\frac{}{\textbf{H} \;\;\vdash \;\; \btrue}</math> ||  || A


{{RRRow}}|*||<font size="-2"> FUN_GOAL </font>|| <math>\frac{}{\textbf{H},\; f\in \textbf{E}\;\mathit{op}\; \textbf{F} \;\;\vdash\;\; f\in T_1\pfun T_2}</math> || where <math>T_1</math> and <math>T_2</math> denote types and <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|FUN_GOAL}}|| <math>\frac{}{\textbf{H},\; f\in \textbf{E}\;\mathit{op}\; \textbf{F} \;\;\vdash\;\; f\in T_1\pfun T_2}</math> || where <math>T_1</math> and <math>T_2</math> denote types and <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}}|*||<font size="-2"> DBL_HYP </font>|| <math>\frac{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H},\;\textbf{P},\;\textbf{P}  \;\;\vdash \;\; \textbf{Q}}</math> ||  || A
{{RRRow}}|*||{{Rulename|DBL_HYP}}|| <math>\frac{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H},\;\textbf{P},\;\textbf{P}  \;\;\vdash \;\; \textbf{Q}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> AND_L </font>|| <math>\frac{\textbf{H},\textbf{P},\textbf{Q} \; \; \vdash \; \;  \textbf{R}}{\textbf{H},\; \textbf{P} \land \textbf{Q} \; \; \vdash \; \;   
{{RRRow}}|*||{{Rulename|AND_L}}|| <math>\frac{\textbf{H},\textbf{P},\textbf{Q} \; \; \vdash \; \;  \textbf{R}}{\textbf{H},\; \textbf{P} \land \textbf{Q} \; \; \vdash \; \;   
\textbf{R}}</math> ||  || A
\textbf{R}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> AND_R </font>|| <math>\frac{\textbf{H} \; \; \vdash \; \;  \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \;  \textbf{P} \; \land \; \textbf{Q}}</math> ||  || A
{{RRRow}}|*||{{Rulename|AND_R}}|| <math>\frac{\textbf{H} \; \; \vdash \; \;  \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \;  \textbf{P} \; \land \; \textbf{Q}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> IMP_L1 </font>|| <math>\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} }</math> ||  || A
{{RRRow}}|*||{{Rulename|IMP_L1}}|| <math>\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} }</math> ||  || A


{{RRRow}}|*||<font size="-2"> IMP_R </font>|| <math>\frac{\textbf{H}, \textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H} \;\;\vdash \;\; \textbf{P} \limp \textbf{Q}}</math> ||  || A
{{RRRow}}|*||{{Rulename|IMP_R}}|| <math>\frac{\textbf{H}, \textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H} \;\;\vdash \;\; \textbf{P} \limp \textbf{Q}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> IMP_AND_L </font>|| <math>\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}}</math> ||  || A
{{RRRow}}|*||{{Rulename|IMP_AND_L}}|| <math>\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}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> IMP_OR_L </font>|| <math>\frac{
{{RRRow}}|*||{{Rulename|IMP_OR_L}}|| <math>\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}}</math> ||  || A
\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}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> AUTO_MH </font>|| <math>\frac{
{{RRRow}}|*||{{Rulename|AUTO_MH}}|| <math>\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}}</math> ||  || A
\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}}</math> ||  || A


{{RRRow}}|*||<font size="-2"> NEG_IN_L </font>|| <math>\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} }</math> ||  || A
{{RRRow}}|*||{{Rulename|NEG_IN_L}}|| <math>\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} }</math> ||  || A


{{RRRow}}|*||<font size="-2"> NEG_IN_R </font>|| <math>\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} }</math> ||  || A
{{RRRow}}|*||{{Rulename|NEG_IN_R}}|| <math>\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} }</math> ||  || A


{{RRRow}}|*||<font size="-2"> XST_L </font>|| <math>\frac{\textbf{H},\;  \textbf{P(x)} \; \; \vdash \; \;  \textbf{Q}
{{RRRow}}|*||{{Rulename|XST_L}}|| <math>\frac{\textbf{H},\;  \textbf{P(x)} \; \; \vdash \; \;  \textbf{Q}
}{
}{
\textbf{H},\;  \exists \, \textbf{x}\, \qdot\, \textbf{P(x)} \; \; \vdash \; \;  \textbf{Q}
\textbf{H},\;  \exists \, \textbf{x}\, \qdot\, \textbf{P(x)} \; \; \vdash \; \;  \textbf{Q}
}</math> ||  || A
}</math> ||  || A


{{RRRow}}|*||<font size="-2"> ALL_R </font>|| <math>\frac{\textbf{H}\; \; \vdash \; \;  \textbf{P(x)} }{ \textbf{H} \; \; \vdash \; \;  \forall \textbf{x}\, \qdot\, \textbf{P(x)} }</math> ||  || A
{{RRRow}}|*||{{Rulename|ALL_R}}|| <math>\frac{\textbf{H}\; \; \vdash \; \;  \textbf{P(x)} }{ \textbf{H} \; \; \vdash \; \;  \forall \textbf{x}\, \qdot\, \textbf{P(x)} }</math> ||  || A


{{RRRow}}|*||<font size="-2"> EQL_LR </font>|| <math>\frac{\textbf{H(E)} \; \; \vdash \; \;  \; \;  \textbf{P(E)} }{\textbf{H(x)},\; x=E \; \; \vdash \; \;  \textbf{P(x)} }</math> || <math>x</math> is a variable which is not free in <math>E</math> || A
{{RRRow}}|*||{{Rulename|EQL_LR}}|| <math>\frac{\textbf{H(E)} \; \; \vdash \; \;  \; \;  \textbf{P(E)} }{\textbf{H(x)},\; x=E \; \; \vdash \; \;  \textbf{P(x)} }</math> || <math>x</math> is a variable which is not free in <math>E</math> || A


{{RRRow}}|*||<font size="-2"> EQL_RL </font>|| <math>\frac{\textbf{H(E)} \; \; \vdash \; \;  \; \;  \textbf{P(E)} }{\textbf{H(x)},\; E=x \; \; \vdash \; \;  \textbf{P(x)} }</math> || <math>x</math> is a variable which is not free in <math>E</math> || A
{{RRRow}}|*||{{Rulename|EQL_RL}}|| <math>\frac{\textbf{H(E)} \; \; \vdash \; \;  \; \;  \textbf{P(E)} }{\textbf{H(x)},\; E=x \; \; \vdash \; \;  \textbf{P(x)} }</math> || <math>x</math> is a variable which is not free in <math>E</math> || A


{{RRRow}}| ||<font size="-2"> SUBSET_INTER </font>|| <math>\frac{\textbf{H},\;\textbf{T} \subseteq \textbf{U} \;\;\vdash \;\;  
{{RRRow}}| ||{{Rulename|SUBSET_INTER}}|| <math>\frac{\textbf{H},\;\textbf{T} \subseteq \textbf{U} \;\;\vdash \;\;  
\textbf{G}(\textbf{S} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{V})}
\textbf{G}(\textbf{S} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{V})}
{\textbf{H},\;\textbf{T} \subseteq \textbf{U} \;\;\vdash \;\;  
{\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})}</math> || the <math>\binter</math> operator must appear at the "top level" || A
\textbf{G}(\textbf{S} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{U} \binter \dots \binter \textbf{V})}</math> || the <math>\binter</math> operator must appear at the "top level" || A


{{RRRow}}| ||<font size="-2"> IN_INTER </font>|| <math>\frac{\textbf{H},\;\textbf{E} \in \textbf{T} \;\;\vdash \;\;  
{{RRRow}}| ||{{Rulename|IN_INTER}}|| <math>\frac{\textbf{H},\;\textbf{E} \in \textbf{T} \;\;\vdash \;\;  
\textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{U})}
\textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{U})}
{\textbf{H},\;\textbf{E} \in \textbf{T} \;\;\vdash \;\;  
{\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})}</math> || the <math>\binter</math> operator must appear at the "top level" || A
\textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{U})}</math> || the <math>\binter</math> operator must appear at the "top level" || A


{{RRRow}}| ||<font size="-2"> NOTIN_INTER </font>|| <math>\frac{\textbf{H},\;\lnot\;\textbf{E} \in \textbf{T} \;\;\vdash \;\;  
{{RRRow}}| ||{{Rulename|NOTIN_INTER}}|| <math>\frac{\textbf{H},\;\lnot\;\textbf{E} \in \textbf{T} \;\;\vdash \;\;  
\textbf{G}(\emptyset)}
\textbf{G}(\emptyset)}
{\textbf{H},\;\lnot\;\textbf{E} \in \textbf{T} \;\;\vdash \;\;  
{\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})}</math> || the <math>\binter</math> operator must appear at the "top level" || A
\textbf{G}(\textbf{S} \binter \dots \binter \{\textbf{E}\} \binter \dots \binter \textbf{T} \binter \dots \binter \textbf{U})}</math> || the <math>\binter</math> operator must appear at the "top level" || A


{{RRRow}}|*||<font size="-2"> CONTRADICT_L </font>|| <math>\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \neg\,\textbf{P}}{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math> ||  || M
{{RRRow}}|*||{{Rulename|CONTRADICT_L}}|| <math>\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \neg\,\textbf{P}}{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math> ||  || M


{{RRRow}}|*||<font size="-2"> CONTRADICT_R </font>|| <math>\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \bfalse}{\textbf{H} \;\;\vdash \;\; \textbf{Q}}</math> ||  || M
{{RRRow}}|*||{{Rulename|CONTRADICT_R}}|| <math>\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \bfalse}{\textbf{H} \;\;\vdash \;\; \textbf{Q}}</math> ||  || M


{{RRRow}}|*||<font size="-2"> CASE </font>|| <math>\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} }</math> ||  || M
{{RRRow}}|*||{{Rulename|CASE}}|| <math>\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} }</math> ||  || M


{{RRRow}}|*||<font size="-2"> MH </font>|| <math>\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} \ \ \ \ \ }</math> ||  || M
{{RRRow}}|*||{{Rulename|MH}}|| <math>\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} \ \ \ \ \ }</math> ||  || M


{{RRRow}}|*||<font size="-2"> HM </font>|| <math>\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} \ \ \ \ \ }</math> ||  || M
{{RRRow}}|*||{{Rulename|HM}}|| <math>\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} \ \ \ \ \ }</math> ||  || M


{{RRRow}}|*||<font size="-2"> EQV </font>|| <math>\frac{\textbf{H(Q)}, \textbf{P} \leqv \textbf{Q}  
{{RRRow}}|*||{{Rulename|EQV}}|| <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}}|*||<font size="-2"> OV_L </font>|| <math>\frac{\textbf{H},\; G=E   
{{RRRow}}|*||{{Rulename|OV_L}}|| <math>\frac{\textbf{H},\; G=E   
,\;\textbf{P}(F)\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,(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  
,\;\textbf{P}(f(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl\{E  
\mapsto F\})(G)) \;\;\vdash \;\; \textbf{Q}}</math> || the <math>\ovl</math> operator must appear at the "top level" || M
\mapsto F\})(G)) \;\;\vdash \;\; \textbf{Q}}</math> || the <math>\ovl</math> operator must appear at the "top level" || M


{{RRRow}}|*||<font size="-2"> OV_R </font>|| <math>\frac{\textbf{H},\; G=E \;\;\vdash\;\;\textbf{Q}(F)  
{{RRRow}}|*||{{Rulename|OV_R}}|| <math>\frac{\textbf{H},\; G=E \;\;\vdash\;\;\textbf{Q}(F)  
\qquad \textbf{H},\; \neg\,(G=E)  \;\;\vdash\;\;\textbf{Q}(f(G))}{\textbf{H}  
\qquad \textbf{H},\; \neg\,(G=E)  \;\;\vdash\;\;\textbf{Q}(f(G))}{\textbf{H}  
\;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G)) \ \ \ \ \ }</math> || the <math>\ovl</math> operator must appear at the "top level" || M
\;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G)) \ \ \ \ \ }</math> || the <math>\ovl</math> operator must appear at the "top level" || M


{{RRRow}}|*||<font size="-2"> OV_L </font>|| <math>\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} \ \ \ \ \ }</math> || the <math>\ovl</math> operator must appear at the "top level" || M
{{RRRow}}|*||{{Rulename|OV_L}}|| <math>\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} \ \ \ \ \ }</math> || the <math>\ovl</math> operator must appear at the "top level" || M


{{RRRow}}|*||<font size="-2"> OV_R </font>|| <math>\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)) \ \ \ \ \ }</math> || the <math>\ovl</math> operator must appear at the "top level" || M
{{RRRow}}|*||{{Rulename|OV_R}}|| <math>\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)) \ \ \ \ \ }</math> || the <math>\ovl</math> operator must appear at the "top level" || M


{{RRRow}}|*||<font size="-2"> DIS_BINTER_R </font>|| <math>\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]) \ \ \ \ \ }</math> || the occurrence of <math>f</math> must appear at the "top level". Moreover <math>A</math> and <math>B</math> denote some type. Similar left distribution rules exist || M
{{RRRow}}|*||{{Rulename|DIS_BINTER_R}}|| <math>\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]) \ \ \ \ \ }</math> || the occurrence of <math>f</math> must appear at the "top level". Moreover <math>A</math> and <math>B</math> denote some type. Similar left distribution rules exist || M


{{RRRow}}|*||<font size="-2"> DIS_SETMINUS_R </font>|| <math>\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]) \ \ \ \ \ }</math> || the occurrence of <math>f</math> must appear at the "top level". Moreover <math>A</math> and <math>B</math> denote some type. Similar left distribution rules exist || M
{{RRRow}}|*||{{Rulename|DIS_SETMINUS_R}}|| <math>\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]) \ \ \ \ \ }</math> || the occurrence of <math>f</math> must appear at the "top level". Moreover <math>A</math> and <math>B</math> denote some type. Similar left distribution rules exist || M


{{RRRow}}|*||<font size="-2"> SIM_REL_IMAGE_R </font>|| <math>\frac{\textbf{H} \; \; \vdash \; \; {WD}(\textbf{Q}(\{ f(E)\} )) \qquad\textbf{H} \; \; \vdash \; \; \textbf{Q}(\{ f(E)\} ) }{\textbf{H} \; \; \vdash \; \;  \textbf{Q}(f[\{ E\} ])} </math> || the occurrence of <math>f</math> must appear at the "top level". A similar left simplification rule exists. || M
{{RRRow}}|*||{{Rulename|SIM_REL_IMAGE_R}}|| <math>\frac{\textbf{H} \; \; \vdash \; \; {WD}(\textbf{Q}(\{ f(E)\} )) \qquad\textbf{H} \; \; \vdash \; \; \textbf{Q}(\{ f(E)\} ) }{\textbf{H} \; \; \vdash \; \;  \textbf{Q}(f[\{ E\} ])} </math> || the occurrence of <math>f</math> must appear at the "top level". A similar left simplification rule exists. || M


{{RRRow}}|*||<font size="-2"> SIM_FCOMP_R </font>|| <math>\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)) \ \ \ \ \ }</math> || the occurrence of <math>f \fcomp g</math> must appear at the "top level". A similar left simplification rule exists. || M
{{RRRow}}|*||{{Rulename|SIM_FCOMP_R}}|| <math>\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)) \ \ \ \ \ }</math> || the occurrence of <math>f \fcomp g</math> must appear at the "top level". A similar left simplification rule exists. || M


{{RRRow}}|*||<font size="-2"> FIN_SUBSETEQ_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; S \subseteq T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(S) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_SUBSETEQ_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; S \subseteq T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(S) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> FIN_BINTER_R </font>|| <math>\frac{\textbf{H} \;\;\vdash  
{{RRRow}}|*||{{Rulename|FIN_BINTER_R}}|| <math>\frac{\textbf{H} \;\;\vdash  
\;\;\finite\,(S) \;\lor\;\ldots \;\lor\; \finite\,(T)}{\textbf{H} \;\;\vdash  
\;\;\finite\,(S) \;\lor\;\ldots \;\lor\; \finite\,(T)}{\textbf{H} \;\;\vdash  
\;\; \finite\,(S \;\binter\;\ldots \;\binter\; T)}</math> ||  || M
\;\; \finite\,(S \;\binter\;\ldots \;\binter\; T)}</math> ||  || M


{{RRRow}}|*||<font size="-2"> FIN_SETMINUS_R </font>|| <math>\frac{\textbf{H} \;\;\vdash  
{{RRRow}}|*||{{Rulename|FIN_SETMINUS_R}}|| <math>\frac{\textbf{H} \;\;\vdash  
\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T) \ \ \ \ \ \ \ }</math> ||  || M
\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T) \ \ \ \ \ \ \ }</math> ||  || M


{{RRRow}}|*||<font size="-2"> FIN_REL_R </font>|| <math>\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)}</math> || the user has to write the set corresponding to <math>S \rel T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_REL_R}}|| <math>\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)}</math> || the user has to write the set corresponding to <math>S \rel T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> FIN_REL_IMG_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(r[s]) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_REL_IMG_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(r[s]) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> FIN_REL_RAN_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\ran(r)) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_REL_RAN_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\ran(r)) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> FIN_REL_DOM_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(r)) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_REL_DOM_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(r)) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> FIN_FUN1_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(f) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_FUN1_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(f) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> FIN_FUN2_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; f^{-1} \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(f) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_FUN2_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; f^{-1} \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(f) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> FIN_FUN_IMG_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(s) }{\textbf{H} \;\;\vdash \;\; \finite\,(f[s]) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_FUN_IMG_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(s) }{\textbf{H} \;\;\vdash \;\; \finite\,(f[s]) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> FIN_FUN_RAN_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(\ran(f)) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_FUN_RAN_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(\ran(f)) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> FIN_FUN_DOM_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; f^{-1} \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(f)) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M
{{RRRow}}|*||{{Rulename|FIN_FUN_DOM_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; f^{-1} \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(f)) \ \ \ \ \ \ \ }</math> || the user has to write the set corresponding to <math>S  \pfun T</math> in the editing area of the Proof Control Window || M


{{RRRow}}|*||<font size="-2"> LOWER_BOUND_L </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)}</math> || <math>S</math> must not contain any bound variable || M
{{RRRow}}|*||{{Rulename|LOWER_BOUND_L}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)}</math> || <math>S</math> must not contain any bound variable || M


{{RRRow}}|*||<font size="-2"> LOWER_BOUND_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \geq n)}</math> || <math>S</math> must not contain any bound variable || M
{{RRRow}}|*||{{Rulename|LOWER_BOUND_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \geq n)}</math> || <math>S</math> must not contain any bound variable || M


{{RRRow}}|*||<font size="-2"> UPPER_BOUND_L </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \geq x)}</math> || <math>S</math> must not contain any bound variable || M
{{RRRow}}|*||{{Rulename|UPPER_BOUND_L}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \geq x)}</math> || <math>S</math> must not contain any bound variable || M


{{RRRow}}|*||<font size="-2"> UPPER_BOUND_R </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \leq n)}</math> || <math>S</math> must not contain any bound variable || M
{{RRRow}}|*||{{Rulename|UPPER_BOUND_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S)  }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \leq n)}</math> || <math>S</math> must not contain any bound variable || M


{{RRRow}}|*||<font size="-2"> FIN_LT_0 </font>|| <math>\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)}</math> ||  || M
{{RRRow}}|*||{{Rulename|FIN_LT_0}}|| <math>\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)}</math> ||  || M


{{RRRow}}|*||<font size="-2"> FIN_GE_0 </font>|| <math>\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)}</math> ||  || M
{{RRRow}}|*||{{Rulename|FIN_GE_0}}|| <math>\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)}</math> ||  || M


{{RRRow}}|*||<font size="-2"> CARD_INTERV </font>|| <math>\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))}</math> || <math>\card (a \upto b)</math> must appear at "top-level" || M
{{RRRow}}|*||{{Rulename|CARD_INTERV}}|| <math>\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))}</math> || <math>\card (a \upto b)</math> must appear at "top-level" || M


{{RRRow}}|*||<font size="-2"> CARD_EMPTY_INTERV </font>|| <math>\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}}</math> || <math>\card (a \upto b)</math> must appear at "top-level" || M
{{RRRow}}|*||{{Rulename|CARD_EMPTY_INTERV}}|| <math>\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}}</math> || <math>\card (a \upto b)</math> must appear at "top-level" || M


{{RRRow}}|*||<font size="-2"> CARD_SUBSETEQ </font>|| <math>\frac{\textbf{H}  \;\;\vdash \;\; \textbf{P}(S \subseteq T)  }{\textbf{H} \;\;\vdash\;\; \textbf{P}(\card\,(S) \leq \card(T))}</math> ||  || M
{{RRRow}}|*||{{Rulename|CARD_SUBSETEQ}}|| <math>\frac{\textbf{H}  \;\;\vdash \;\; \textbf{P}(S \subseteq T)  }{\textbf{H} \;\;\vdash\;\; \textbf{P}(\card\,(S) \leq \card(T))}</math> ||  || M


{{RRRow}}|*||<font size="-2"> FORALL_INST </font>|| <math>\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}}</math> || <math>x</math> is instantiated with <math>E</math> || M
{{RRRow}}|*||{{Rulename|FORALL_INST}}|| <math>\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}}</math> || <math>x</math> is instantiated with <math>E</math> || M


{{RRRow}}|*||<font size="-2"> FORALL_INST_MP </font>|| <math>\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}}</math> || <math>x</math> is instantiated with <math>E</math> and a Modus Ponens is applied|| M
{{RRRow}}|*||{{Rulename|FORALL_INST_MP}}|| <math>\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}}</math> || <math>x</math> is instantiated with <math>E</math> and a Modus Ponens is applied|| M


{{RRRow}}|*||<font size="-2"> CUT </font>|| <math>\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}}</math> || hypothesis <math>\textbf{P}</math> is added || M
{{RRRow}}|*||{{Rulename|CUT}}|| <math>\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}}</math> || hypothesis <math>\textbf{P}</math> is added || M


{{RRRow}}|*||<font size="-2"> EXISTS_INST </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} , [x \bcmeq E]\textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \exists x \qdot \textbf{P}  \;\;\vdash\;\; \textbf{G}}</math> || <math>x</math> is instantiated with <math>E</math> || M
{{RRRow}}|*||{{Rulename|EXISTS_INST}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} , [x \bcmeq E]\textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \exists x \qdot \textbf{P}  \;\;\vdash\;\; \textbf{G}}</math> || <math>x</math> is instantiated with <math>E</math> || M


{{RRRow}}|*||<font size="-2"> DISTINCT_CASE </font>|| <math>\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}}</math> || case distinction on predicate <math>\textbf{P}</math> || M
{{RRRow}}|*||{{Rulename|DISTINCT_CASE}}|| <math>\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}}</math> || case distinction on predicate <math>\textbf{P}</math> || M


|}
|}

Revision as of 10:25, 8 July 2009

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 \textbf{E}\;\mathit{op}\; \textbf{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


*
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


*
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} \ \ \ \ \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 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^{-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. 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


*
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} , [x \bcmeq E]\textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \exists x \qdot \textbf{P} \;\;\vdash\;\; \textbf{G}} 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
Retrieved from ‘https://wiki.event-b.org/index.php?title=Inference_Rules&oldid=5699’