% These definitions - the "preable" of a .dnt file - are from:
%   http://angg.twu.net/dednat5/preamble.lua.html
%   http://angg.twu.net/dednat5/preamble.lua
%                    (find-dn5 "preamble.lua")
%
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\def\defded#1#2{\expandafter\def\csname ded-#1\endcsname{#2}}
\def\ifdedundefined#1{\expandafter\ifx\csname ded-#1\endcsname\relax}
\def\ded#1{\ifdedundefined{#1}
    \errmessage{UNDEFINED DEDUCTION: #1}
  \else
    \csname ded-#1\endcsname
  \fi
}
\def\defdiag#1#2{\expandafter\def\csname diag-#1\endcsname{\bfig#2\efig}}
\def\defdiagprep#1#2#3{\expandafter\def\csname diag-#1\endcsname{{#2\bfig#3\efig}}}
\def\ifdiagundefined#1{\expandafter\ifx\csname diag-#1\endcsname\relax}
\def\diag#1{\ifdiagundefined{#1}
    \errmessage{UNDEFINED DIAGRAM: #1}
  \else
    \csname diag-#1\endcsname
  \fi
}
% End of the preamble.


  \def\defpgfdiag#1#2{\expandafter\def\csname diag-#1\endcsname
    {\begin{tikzpicture}#2\end{tikzpicture}}}

\defpgfdiag{Kite}{  % no hyperlink yet
    \node (X) at (1,-0) {X};
    \node (U) at (0,-1) {U};
    \node (V) at (2,-1) {V};
    \node (W) at (1,-2) {W};
    \node (O') at (1,-3) {O'};
    \draw [<-] (X) to node {} (U);
    \draw [<-] (X) to node {} (V);
    \draw [<-] (U) to node {} (W);
    \draw [<-] (V) to node {} (W);
    \draw [<-] (W) to node {} (O');
}
\defpgfdiag{PGF-adj-reconstruction-LR}{  % no hyperlink yet
    \node (L0) at (3.5,-0) {L0};
    \node (L1) at (5,-0) {L1};
    \node (L3) at (5,-1.5) {L3};
    \node (L4) at (3.5,-2.4) {L4};
    \node (L5) at (5,-2.4) {L5};
    \node (F0) at (3.5,-3.15) {F0};
    \node (F1) at (5,-3.15) {F1};
    \node (C0) at (0,-4.65) {C0};
    \node (C1) at (1.5,-4.65) {C1};
    \node (F2) at (3.5,-4.65) {F2};
    \node (F3) at (5,-4.65) {F3};
    \node (U0) at (7,-4.65) {U0};
    \node (U1) at (8.5,-4.65) {U1};
    \node (S0) at (5,-5.25) {S0};
    \node (F4) at (3.5,-5.55) {F4};
    \node (C2) at (0,-6.15) {C2};
    \node (C3) at (1.5,-6.15) {C3};
    \node (S1) at (3.5,-6.15) {S1};
    \node (S2) at (5,-6.15) {S2};
    \node (U2) at (7,-6.15) {U2};
    \node (U3) at (8.5,-6.15) {U3};
    \node (S3) at (3.5,-7.65) {S3};
    \node (S4) at (5,-7.65) {S4};
    \node (R0) at (3.5,-8.4) {R0};
    \node (R1) at (5,-8.4) {R1};
    \node (R2) at (3.5,-9.3) {R2};
    \node (R4) at (3.5,-10.8) {R4};
    \node (R5) at (5,-10.8) {R5};
    \node (:35) at (3.75,-3.9) {:35};
    \node (:36) at (4.75,-3.9) {:36};
    \node (:37) at (3.75,-6.9) {:37};
    \node (:38) at (4.75,-6.9) {:38};
    \node (:39) at (0.25,-5.4) {:39};
    \node (:40) at (1.25,-5.4) {:40};
    \node (:41) at (7.25,-5.4) {:41};
    \node (:42) at (8.25,-5.4) {:42};
    \node (:43) at (3.625,-1.2) {:43};
    \node (:44) at (4.625,-1.2) {:44};
    \node (:45) at (3.875,-9.6) {:45};
    \node (:46) at (4.875,-9.6) {:46};
    \draw [<-|] (F0) to node {} (F1);
    \draw [->] (F0) to node {} (F4);
    \draw [->] (F0) to node {} (F2);
    \draw [->] (F1) to node {} (F3);
    \draw [<-|] (:35) to node {} (:36);
    \draw [<-|] (F2) to node {} (F3);
    \draw [->] (F2) to node {} (F4);
    \draw [->] (S0) to node {} (S2);
    \draw [|->] (S1) to node {} (S2);
    \draw [->] (S1) to node {} (S3);
    \draw [->] (S2) to node {} (S4);
    \draw [->] (S0) to node {} (S4);
    \draw [|->] (:37) to node {} (:38);
    \draw [|->] (S3) to node {} (S4);
    \draw [->] (S3) to node {} (S4);
    \draw [<-|] (C0) to node {} (C1);
    \draw [->] (C0) to node {} (C2);
    \draw [->] (C1) to node {} (C3);
    \draw [|->] (C2) to node {} (C3);
    \draw [<-|] (:39) to node {} (:40);
    \draw [<-|] (U0) to node {} (U1);
    \draw [->] (U0) to node {} (U2);
    \draw [->] (U1) to node {} (U3);
    \draw [|->] (U2) to node {} (U3);
    \draw [|->] (:41) to node {} (:42);
    \draw [<-|] (L0) to node {} (L1);
    \draw [->] (L0) to node {} (L4);
    \draw [->] (L1) to node {} (L5);
    \draw [->] (L1) to node {} (L3);
    \draw [->] (L3) to node {} (L5);
    \draw [|->] (L4) to node {} (L5);
    \draw [<-|] (:43) to node {} (:44);
    \draw [<-|] (R0) to node {} (R1);
    \draw [->] (R0) to node {} (R2);
    \draw [->] (R2) to node {} (R4);
    \draw [->] (R0) to node {} (R4);
    \draw [->] (R1) to node {} (R5);
    \draw [|->] (R4) to node {} (R5);
    \draw [|->] (:45) to node {} (:46);
}
\defdiag{adj-reconstruction-LR}{ % no hyperlink yet
  \morphism(1050,-945)/<-|/<450,0>[{LA}`{A};]
  \morphism(1050,-945)|l|/{@{->}@<-16pt>}/<0,-720>[{LA}`{B};{\sm{g^\flat\;:=\\Lg;\eta_B}}]
  \morphism(1050,-945)|l|/->/<0,-450>[{LA}`{LRB};{Lg}]
  \morphism(1500,-945)|r|/->/<0,-450>[{A}`{RB};{g}]
  \morphism(1125,-1170)/<-|/<300,0>[{\phantom{O}}`{\phantom{O}};]
  \morphism(1050,-1395)/<-|/<450,0>[{LRB}`{RB};]
  \morphism(1050,-1395)|l|/->/<0,-270>[{LRB}`{B};{\eta_B}]
  \morphism(1500,-1575)|r|/->/<0,-270>[{A}`{RLA};{\eta_A}]
  \morphism(1050,-1845)/|->/<450,0>[{LA}`{RLA};]
  \morphism(1050,-1845)|l|/->/<0,-450>[{LA}`{B};{f}]
  \morphism(1500,-1845)|r|/->/<0,-450>[{RLA}`{RB};{Rf}]
  \morphism(1500,-1575)|r|/{@{->}@<16pt>}/<0,-720>[{A}`{RB};{\sm{f^\sharp\;:=\\\eta_A;Rf}}]
  \morphism(1125,-2070)/|->/<300,0>[{\phantom{O}}`{\phantom{O}};]
  \morphism(1050,-2295)/|->/<450,0>[{B}`{RB};]
  \morphism(1050,-2295)|l|/->/<450,0>[{B}`{RB};{\eta_B}]
  \morphism(0,-1395)/<-|/<450,0>[{LRB}`{RB};]
  \morphism(0,-1395)|l|/->/<0,-450>[{LRB}`{B};{\sm{\eta_B\;:=\\{\id_{RB}}^\flat}}]
  \morphism(450,-1395)|r|/->/<0,-450>[{RB}`{RB};{\id_{RB}}]
  \morphism(0,-1845)/|->/<450,0>[{B}`{RB};]
  \morphism(75,-1620)/<-|/<300,0>[{\phantom{O}}`{\phantom{O}};]
  \morphism(2100,-1395)/<-|/<450,0>[{LA}`{A};]
  \morphism(2100,-1395)|l|/->/<0,-450>[{LA}`{LA};{\id_{LA}}]
  \morphism(2550,-1395)|r|/->/<0,-450>[{A}`{RLA};{\sm{\eta_A\;:=\\{\id_{LA}}^\sharp}}]
  \morphism(2100,-1845)/|->/<450,0>[{LA}`{RLA};]
  \morphism(2175,-1620)/|->/<300,0>[{\phantom{O}}`{\phantom{O}};]
  \morphism(1050,0)/<-|/<450,0>[{LA'}`{A'};]
  \morphism(1050,0)|l|/->/<0,-720>[{LA'}`{LA};{\sm{L\aa\;:=\\(\aa;\eta_A)^\flat}}]
  \morphism(1500,0)/{@{->}@<-10pt>}/<0,-720>[{A'}`{RLA};]
  \morphism(1500,0)|r|/->/<0,-450>[{A'}`{A};{\aa}]
  \morphism(1500,-450)|r|/->/<0,-270>[{A}`{RLA};{\eta_A}]
  \morphism(1050,-720)/|->/<450,0>[{LA}`{RLA};]
  \morphism(1087,-360)/<-|/<300,0>[{\phantom{O}}`{\phantom{O}};]
  \morphism(1050,-2520)/<-|/<450,0>[{LRB}`{RB};]
  \morphism(1050,-2520)|l|/->/<0,-270>[{LRB}`{B};{\ee_B}]
  \morphism(1050,-2790)|l|/->/<0,-450>[{B}`{B'};{\bb}]
  \morphism(1050,-2520)/{@{->}@<10pt>}/<0,-720>[{LRB}`{B'};]
  \morphism(1500,-2520)|r|/->/<0,-720>[{RB}`{RB'};{\sm{R\bb\;:=\\(\ee_B;\bb)^\sharp}}]
  \morphism(1050,-3240)/|->/<450,0>[{B'}`{RB'};]
  \morphism(1162,-2880)/|->/<300,0>[{\phantom{O}}`{\phantom{O}};]
}