Lines Matching defs:neg
128 \neg \Var{P} & \equiv & \Var{P}\imp\bot \\
135 of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$. For
136 example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
156 \[ \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}} \qquad
157 \infer[({\neg}E)]{Q}{\neg P & P} \]
159 $$ (P\Imp\bot) \Imp \neg P \eqno(\neg I) $$
160 $$ \List{\neg P; P} \Imp Q. \eqno(\neg E) $$
163 \subsection{Deriving the $\neg$ introduction rule}
164 To derive $(\neg I)$, we may call \texttt{Goal} with the appropriate formula.
223 \subsection{Deriving the $\neg$ elimination rule}
224 Let us derive the rule $(\neg E)$. The proof follows that of~\texttt{conjE}
727 and~$\neg$, we take advantage of the meta-logic;\footnote
729 and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work