Inference Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Laurent Fixed broken rules (ill-defined, ill-typed or plain wrong) |
imported>Laurent m FIxed spacing in formulas |
||
Line 78: | Line 78: | ||
{{RRRow}}|*||{{Rulename|CONTRADICT_R}}|| <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}}|*||{{Rulename|CASE}}|| <math>\frac{\textbf{H}, \; \textbf{P} \; \; \vdash \; \; \textbf{R} \ | {{RRRow}}|*||{{Rulename|CASE}}|| <math>\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} }</math> || || M | ||
{{RRRow}}|b||{{Rulename|MH}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;\textbf{P} \qquad \textbf{H},\; \textbf{Q} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R} | {{RRRow}}|b||{{Rulename|MH}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;\textbf{P} \qquad \textbf{H},\; \textbf{Q} \;\;\vdash \;\; \textbf{R} }{\textbf{H},\;\textbf{P} \limp \textbf{Q} \;\;\vdash \;\; \textbf{R}}</math> || || M | ||
{{RRRow}}|b||{{Rulename|HM}}|| <math>\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} | {{RRRow}}|b||{{Rulename|HM}}|| <math>\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}}</math> || || M | ||
{{RRRow}}|*||{{Rulename|EQV}}|| <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)} | \;\;\vdash \;\; \textbf{G(P)}}</math> || || M | ||
{{RRRow}}|*||{{Rulename|OV_L}}|| <math>\frac{\textbf{H},\; G=E | {{RRRow}}|*||{{Rulename|OV_L}}|| <math>\frac{\textbf{H},\; G=E | ||
Line 95: | Line 95: | ||
{{RRRow}}|*||{{Rulename|OV_R}}|| <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)) | \;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G))}</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} | {{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}}|*||{{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)) | {{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}}|*||{{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]) | {{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. || M | ||
{{RRRow}}|*||{{Rulename|DIS_BINTER_L}}|| <math>\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} | {{RRRow}}|*||{{Rulename|DIS_BINTER_L}}|| <math>\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}}</math> || the occurrence of <math>f</math> must appear at the "top level". Moreover <math>A</math> and <math>B</math> denote some type. || 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]) | {{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. || M | ||
{{RRRow}}|*||{{Rulename|DIS_SETMINUS_L}}|| <math>\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} | {{RRRow}}|*||{{Rulename|DIS_SETMINUS_L}}|| <math>\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}}</math> || the occurrence of <math>f</math> must appear at the "top level". Moreover <math>A</math> and <math>B</math> denote some type. || 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". || 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". || M | ||
Line 113: | Line 113: | ||
{{RRRow}}|*||{{Rulename|SIM_REL_IMAGE_L}}|| <math>\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} } </math> || the occurrence of <math>f</math> must appear at the "top level". || M | {{RRRow}}|*||{{Rulename|SIM_REL_IMAGE_L}}|| <math>\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} } </math> || the occurrence of <math>f</math> must appear at the "top level". || 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)) | {{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". || M | ||
{{RRRow}}|*||{{Rulename|SIM_FCOMP_L}}|| <math>\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} | {{RRRow}}|*||{{Rulename|SIM_FCOMP_L}}|| <math>\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}}</math> || the occurrence of <math>f \fcomp g</math> must appear at the "top level". || M | ||
{{RRRow}}|b||{{Rulename|FIN_SUBSETEQ_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(T) \qquad\textbf{H} \;\;\vdash \;\; S \subseteq T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(S) | {{RRRow}}|b||{{Rulename|FIN_SUBSETEQ_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(T) \qquad\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_BINTER_R}}|| <math>\frac{\textbf{H} \;\;\vdash | {{RRRow}}|*||{{Rulename|FIN_BINTER_R}}|| <math>\frac{\textbf{H} \;\;\vdash | ||
Line 124: | Line 124: | ||
{{RRRow}}|*||{{Rulename|FIN_SETMINUS_R}}|| <math>\frac{\textbf{H} \;\;\vdash | {{RRRow}}|*||{{Rulename|FIN_SETMINUS_R}}|| <math>\frac{\textbf{H} \;\;\vdash | ||
\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T) | \;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)}</math> || || M | ||
{{RRRow}}|b||{{Rulename|FIN_REL_R}}|| <math>\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)}</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}}|b||{{Rulename|FIN_REL_R}}|| <math>\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)}</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_IMG_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(r[s]) | {{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}}|*||{{Rulename|FIN_REL_RAN_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\ran(r)) | {{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}}|*||{{Rulename|FIN_REL_DOM_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(r)) | {{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}}|b||{{Rulename|FIN_FUN1_R}}|| <math>\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) | {{RRRow}}|b||{{Rulename|FIN_FUN1_R}}|| <math>\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)}</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}}|b||{{Rulename|FIN_FUN2_R}}|| <math>\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) | {{RRRow}}|b||{{Rulename|FIN_FUN2_R}}|| <math>\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)}</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}}|b||{{Rulename|FIN_FUN_IMG_R}}|| <math>\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]) | {{RRRow}}|b||{{Rulename|FIN_FUN_IMG_R}}|| <math>\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])}</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}}|b||{{Rulename|FIN_FUN_RAN_R}}|| <math>\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)) | {{RRRow}}|b||{{Rulename|FIN_FUN_RAN_R}}|| <math>\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))}</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}}|b||{{Rulename|FIN_FUN_DOM_R}}|| <math>\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)) | {{RRRow}}|b||{{Rulename|FIN_FUN_DOM_R}}|| <math>\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))}</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|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}}|*||{{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 |
Revision as of 17:40, 11 November 2009
Conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Inference_Rules.
Rules that are marked with a b in the first column are currently broken in Rodin 1.1 (see bug 2895507).
Name | Rule | Side Condition | A/M
| |
---|---|---|---|---|
* | HYP |
A
| ||
* | HYP_OR |
A
| ||
* | CNTR |
A
| ||
* | FALSE_HYP |
A
| ||
* | TRUE_GOAL |
A
| ||
* | FUN_GOAL |
where and denote types and is one of , , , , , , . | A
| |
* | DBL_HYP |
A
| ||
* | AND_L |
A
| ||
* | AND_R |
A
| ||
* | IMP_L1 |
A
| ||
* | IMP_R |
A
| ||
* | IMP_AND_L |
A
| ||
* | IMP_OR_L |
A
| ||
* | AUTO_MH |
A
| ||
* | NEG_IN_L |
A
| ||
* | NEG_IN_R |
A
| ||
* | XST_L |
A
| ||
* | ALL_R |
A
| ||
* | EQL_LR |
is a variable which is not free in | A
| |
* | EQL_RL |
is a variable which is not free in | A
| |
SUBSET_INTER |
the operator must appear at the "top level" | A
| ||
IN_INTER |
the operator must appear at the "top level" | A
| ||
NOTIN_INTER |
the operator must appear at the "top level" | A
| ||
* | FIN_L_LOWER_BOUND_L |
The goal is discharged | A
| |
* | FIN_L_LOWER_BOUND_R |
The goal is discharged | A
| |
* | FIN_L_UPPER_BOUND_L |
The goal is discharged | A
| |
* | FIN_L_UPPER_BOUND_R |
The goal is discharged | A
| |
* | CONTRADICT_L |
M
| ||
* | CONTRADICT_R |
M
| ||
* | CASE |
M
| ||
b | MH |
M
| ||
b | HM |
M
| ||
* | EQV |
M
| ||
* | OV_L |
the operator must appear at the "top level" | M
| |
* | OV_R |
the operator must appear at the "top level" | M
| |
* | OV_L |
the operator must appear at the "top level" | M
| |
* | OV_R |
the operator must appear at the "top level" | M
| |
* | DIS_BINTER_R |
the occurrence of must appear at the "top level". Moreover and denote some type. | M
| |
* | DIS_BINTER_L |
the occurrence of must appear at the "top level". Moreover and denote some type. | M
| |
* | DIS_SETMINUS_R |
the occurrence of must appear at the "top level". Moreover and denote some type. | M
| |
* | DIS_SETMINUS_L |
the occurrence of must appear at the "top level". Moreover and denote some type. | M
| |
* | SIM_REL_IMAGE_R |
the occurrence of must appear at the "top level". | M
| |
* | SIM_REL_IMAGE_L |
the occurrence of must appear at the "top level". | M
| |
* | SIM_FCOMP_R |
the occurrence of must appear at the "top level". | M
| |
* | SIM_FCOMP_L |
the occurrence of must appear at the "top level". | M
| |
b | FIN_SUBSETEQ_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_BINTER_R |
M
| ||
* | FIN_SETMINUS_R |
M
| ||
b | FIN_REL_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_REL_IMG_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_REL_RAN_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_REL_DOM_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | FIN_FUN1_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | FIN_FUN2_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | FIN_FUN_IMG_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | FIN_FUN_RAN_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | FIN_FUN_DOM_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | LOWER_BOUND_L |
must not contain any bound variable | M
| |
* | LOWER_BOUND_R |
must not contain any bound variable | M
| |
* | UPPER_BOUND_L |
must not contain any bound variable | M
| |
* | UPPER_BOUND_R |
must not contain any bound variable | M
| |
* | FIN_LT_0 |
M
| ||
* | FIN_GE_0 |
M
| ||
* | CARD_INTERV |
must appear at "top-level" | M
| |
b | CARD_EMPTY_INTERV |
must appear at "top-level" | M
| |
b | CARD_SUBSETEQ |
and bear the same type | M
| |
* | FORALL_INST |
is instantiated with | M
| |
* | FORALL_INST_MP |
is instantiated with and a Modus Ponens is applied | M
| |
* | CUT |
hypothesis is added | M
| |
* | EXISTS_INST |
is instantiated with | M
| |
* | DISTINCT_CASE |
case distinction on predicate | M
| |
ONE_POINT_L |
The rule can be applied with as well as with | A
| ||
ONE_POINT_R |
The rule can be applied with as well as with | A |