# Can I typeset a certain proof tree in ConTeXt?

Now, I know that the below picture can be done in LaTeX. Can it be done in ConTeXt? Because I have yet to learn any TeX system, I'm not asking how to do it in ConTeXt, but I am primarily interested in whether it's possible or not. Or, should I ask if ConTeXt can do everything that LaTeX can do?

• Since you can always write some new macros, I assume the answer is technically yes. However, some things will be much easier in LaTeX and others will be much easier in ConTeXt because you will not have to write the macros to do the job yourself. That is, the wheel may already be invented for one and not the other, and it is easier not to have to reinvent the wheel even though reinventing the wheel is always an option. There are several packages for creating these kinds of proofs. At least some require LaTeX. There are likely to be fewer, if any, which require ConTeXt. – cfr Nov 26 '15 at 14:24
• It is probably not coincidence that we have LaTeX for Logicians and not, as far as I know, ConTeXt for Logicians. – cfr Nov 26 '15 at 21:19

I adapted egreg’s answer and ported it to ConTeXt. This is feasible in this case, because bussproofs was written to be also compatible to plain TeX, which makes it way easier. Unfortunately, the developer of bussproofs thought it was a good idea to define his own \newcount, which results in this ugly hack in the first lines of the example.

If the slash in the \cancel macro is too unseeable, replace / in the \cancel macro with \backslash.

\catcode\@=11
% Ugly hackery to make the own definition of \newcount in bussproofs work
\countdef\insc@unt=20
\countdef\allocationnumber=21
\allocationnumber=\count1#1%
\global#3#5=\allocationnumber
\wlog{\string#5=\string#2\the\allocationnumber}}
\catcode\@=12

\input bussproofs.sty

\def\lto{\mathbin{\to}}
\catcode\@=11
\def\cancel#1{\mathpalette\cancel@{#1}}
\def\cancel@#1#2{{\ooalign{%
$#1#2$\cr
\hidewidth$#1/$\hidewidth\cr}%
}}
\def\circled#1{\mathpalette\circled@{#1}}
\def\circled@#1#2{{\ooalign{%
$#1\bigcirc$\cr
\hidewidth\lower.125ex\hbox{$#1#2$}\hidewidth\cr}%
}}
\catcode\@=12

\starttext

\def\defaultHypSeparation{\hskip 4em}
\AxiomC{${\cancel{\psi}}^{\circled{1}}$}
\AxiomC{$(\phi\land\psi)$}
\RightLabel{($\land\rm{E}$)}
\UnaryInfC{$\phi$}
\RightLabel{($\land\rm{I}$)}
\BinaryInfC{$(\psi\land\phi)$}
\LeftLabel{$\circled{1}$}
\RightLabel{($\lto\rm{I}$)}
\UnaryInfC{$(\psi\lto(\psi\land\phi))$}
\DisplayProof

\stoptext


• The slash is inconspicuous. – crocket Nov 27 '15 at 1:59
• @crocket You can either use \backslash instead of /, or you can use MetaFun. – Henri Menke Nov 27 '15 at 7:31