Skip to content
Snippets Groups Projects
Commit a80976cc authored by Haniel Barbosa's avatar Haniel Barbosa
Browse files

[Calculus] Fix conclusion of not_ite2

parent 77b4700a
No related branches found
No related tags found
No related merge requests found
Pipeline #4479 passed
......@@ -915,7 +915,7 @@ with $1 \leq k \leq n$.
\begin{plContainer}
\begin{plList}
\proofsep& i.& \neg(\operatorname{ite}\varphi_1\;\varphi_2\;\varphi_3) &(\dots)\\
\proofsep& j.& \neg\varphi_2 , \neg\varphi_2 &(\currule; i)\\
\proofsep& j.& \neg\varphi_1 , \neg\varphi_2 &(\currule; i)\\
\end{plList}
\end{plContainer}
\end{proof-rule}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment