Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% 0.tex: some (very basic) tests for dednat6.
% See: http://angg.twu.net/dednat6.html
%      http://angg.twu.net/dednat6/tests/0.tex.html
%      http://angg.twu.net/dednat6/tests/0.tex
%      http://angg.twu.net/dednat6/tests/0.pdf
%
% (defun c () (interactive) (find-sh "lualatex 0.tex"))
% (defun c () (interactive) (find-sh "lualatex --output-format=dvi 0.tex"))
% (defun d () (interactive) (find-xpdfpage "0.pdf"))
% (defun d () (interactive) (find-xdvipage "0.dvi"))

\documentclass[oneside]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}

% See: (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams

\begin{document}

\catcode`\^^J=10
\directlua{dednat6dir = "../"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{texfile(tex.jobname)}
% \directlua{quiet()}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\pu{\directlua{pu()}}
\pu


%D diagram miniadj
%D 2Dx      100   120
%D 2D  100 a^L <= a
%D 2D       -     -
%D 2D       |     |
%D 2D       v     v
%D 2D  120  b => b^R
%D a^L a <=   a^L b |->   a b^R |->   b b^R =>
%D enddiagram
$$\pu \diag{miniadj}$$

%:                   P\&Q
%:                   ----
%:             P\&Q   Q  
%:             ----   :f 
%:  P\&Q        P     R  
%:    :(P\&)f   -------  
%:  P\&R          P\&R   
%:  
%:  ^t1           ^t2
%:  
$$\pu \ded{t1} := \ded{t2}$$

\end{document}

% Local Variables:
% coding: utf-8-unix
% End: