% (find-LATEX "2019douglas.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019douglas.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019douglas.pdf"))
% (defun e () (interactive) (find-LATEX "2019douglas.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019douglas"))
% (find-pdf-page   "~/LATEX/2019douglas.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019douglas.tex /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019douglas.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019douglas.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019douglas.pdf
%               file:///tmp/2019douglas.pdf
%           file:///tmp/pen/2019douglas.pdf
% http://angg.twu.net/LATEX/2019douglas.pdf
% (find-LATEX "2019.mk")

\documentclass[oneside]{book}
\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{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")


%L addabbrevs("->", "\\to ", "=>", "\\Rightarrow ")

%:
%:                                                                 ----(Ax)
%:                                                                 C=>C
%:                              ----(Ax)                           ------(LW)
%:                              A=>A                               A,C=>C
%:    ----(Ax)                ---------(LW)                        -------(R->)
%:    A=>A                    A,B->C=>A                            C=>A->C
%:  ---------(LW)             -----------(RW)     ----------(RW)  ---------(LW)
%:  A,A->B=>A                 A,B->C=>A,C          B=>A->C,B      C,B=>A->C
%:  ------------(RW)          ------------(R->)     -----------------------(L->)
%:  A,A->B=>A,C               B->C=>A->C,A          B,B->C=>A->C  
%:  -------------(R->)        ----------------------------------(L->)
%:  A->B=>A,A->C                 A->B,B->C=>A->C
%:  ------------------(R->)    ----------------------------(L->)
%:  =>(A->B)->(A->C),A         B->C=>(A->B)->(A->B)->(A->C)
%:  -------------------------------------------------------(R->)
%:  A->(B->C)=>(A->B)->(A->C)
%:
%:  ^foo1
%:
\pu
{\footnotesize
$$
  \ded{foo1}
$$
}


\end{document}

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