%                                                       exptrees.sty

% Improvements to be implemented: allow \bpf \epf in \BLIST \ELIST
% Allow both bpt and xmove ymove for ept and epf in all circumstances
% Provide PT with [xoffset,yoffset] parameters

% Define levels of tracing

\typeout{o-o-o exptrees.sty o-o 22 jan 92 o-o-o}
\typeout{o-o-o Dirk Roorda o-o <roorda@fwi.uva.nl> o-o-o}

\catcode`_11            % preventing interaction with latex definitions
\catcode`@11            % to have access to (la)tex definitions

%       SYNONYMS

\let\cs_\csname
\let\es_\endcsname
\let\nx_\noexpand
\let\ea_\expandafter
\let\g_\global
\let\a_\advance
\def\ga_{\global\advance}
\let\d_\divide
\let\m_\multiply
\let\is_\ignorespaces
\let\r_\relax

%       USER INTERFACE: ERROR and DEBUG


\newcount\tr_a\tr_a0

\let\tr_c\tracingcommands
\let\tr_m\tracingmacros

\newif\if_tr_fc\_tr_fcfalse
\newif\if_trac

\def\trac_on{\if_trac\g_\tr_a1\g_\tr_m2\g_\tr_c2\r_\fi}

\def\trac_off{\if_tr_fc\else\g_\tr_c0\g_\tr_m0\r_\fi}

\def\tra{\g_\tr_a1\r_}
\def\notra{\g_\tr_a0\r_}

\def\trace{\g_\tr_a1\g_\tr_m2\g_\tr_c2\r_\_tractrue\is_}
\def\notrace{\g_\tr_a0\g_\tr_m0\g_\tr_c0\r_\_tracfalse\is_}

\def\tracefc{\trace\_tr_fctrue\is_}
\def\notracefc{\_tr_fcfalse\is_}

\newcount\linen_

\def\print_lines{\a_\linen_1\typeout{level \the\INIT_;line \the\linen_}}

{\catcode`\^^M\active % these lines must end with %
  \gdef\numbers{\catcode`\^^M\active \let^^M\print_lines\is_}}

\def\intro_{o-o-o TREE o-o ERROR o-o MESSAGE o-o-o }
\def\pre_fout#1{\edef\dom_{\nx_\errhelp\nx_{#1\nx_}}\dom_}
\def\_fout#1#2{\pre_fout{#2}\r_
        {{\errorcontextlines0\newlinechar`!\r_
        \errmessage{\intro_!!\space #1.!Type H for more information}}}}

%       USER INTERFACE

%       The if_first_char functions. They skip leading space, check a condition
%       on the first char, (which is always false if the non blank part
%       is empty), and yield (if true) the non blank part in \_arg
%       Sometimes follow parse functions immediately.

\def\fl_#1_{\ifcat#1a\_incharstrue\else\_incharsfalse\fi}

% user name #1 is translated to control sequence N_M#1 to prevent confusion

\def\parse_name#1{\if_u{us_dN_M#1}\ea_\def\cs_ us_dN_M#1\es_{USED}\r_
        \else\r_
\_fout{Name already used}%
{You redefine name _#1_. I leave this to your responsibility. Proceed.}\fi\r_
        \ifnum\tr_a>0\r_
        \wlog{New name _#1_ is \cs_ N_M\r_m\n_me\es_}\fi\r_
        \c_p{N_M#1}{\cs_ N_M\r_m\n_me\es_}\r_
        \ea_\def\cs_ sav_\cs_ N_M\r_m\n_me\es_\es_{s}\is_}

\def\fd_#1_{\let_oc_#1_0123456789.-_}

\def\fr_#1_{\let_oc_#1_<_}

% Scale argument: <dimen> or <<dimen><1-4> for the binary case,
% <dimen> for unary case

\def\parse_dim_t#1_#2{\d_ccc#1\r_}

\def\parse_dim_p#1_#2{}

\def\parse_rdim_Ut<#1_#2{\d_ccc#1\d_\d_ccc10\r_}

\def\parse_rdim_Bt<#1_#2{\r_
\afterassignment\cr_s\d_ccc#1\d_\d_ccc10\r_
        \ifnum\cr_s>0\r_\ifnum\cr_s<5\def\_index{\the\cr_s}\else
\_fout{Wrong index}%
{Node #2: You gave \the\cr_s, but I expect one between 0 and 4.!%
I replace it by 2, you can proceed.}\r_
        \def\_index{2}\fi\else\r_
\_fout{Wrong index}%
{Node #2: You gave \the\cr_s, but I expect one between 0 and 4.!%
I replace it by 2, you can proceed.}\r_
        \def\_index{2}\fi}

\def\parse_rdim_Bp<#1_#2{\r_
\afterassignment\cr_s\d_ccc#1\r_}

\def\parse_rdim_Up<#1_#2{}

% Fork argument: /->f  :->d  '->n for unary case
% Binary case    /->f  :->d  '->n and if there is only one, duplicate
% Gives error messages. Is only called if firstchar in / : '
% moreover, the fully expanded tail is in \_tail. Result in \_arg.

\def\ff_#1_{\let_oc_#1_/_\if_inchars\edef\_head{f}\else\r_
        \let_oc_#1_:_\if_inchars\edef\_head{d}\else\r_
        \let_oc_#1_'_\if_inchars\edef\_head{n}\else\r_
        \fi\fi\fi}

\def\ffc_#1_{\hs_#1_\r_
        \oc_\_head _/_\if_inchars\edef\_head{f}\else\r_
        \oc_\_head _:_\if_inchars\edef\_head{d}\else\r_
        \oc_\_head _'_\if_inchars\edef\_head{n}\else\r_
        \fi\fi\fi}

\def\parse_ff_U#1_#2{\r_
        \edef\_sshead{\_head}\hs_#1_\r_
        \ts_\_tail _\r_
        \if_empty\edef\_arg{\_sshead}\else
\_fout{Wrong unary fork specification}%
{Node #2: Your input is _#1_ After a valid character remains garbage:!%
_\_tail _ I skip it, you can proceed.}\r_
        \edef\_arg{\_sshead}\fi}

\def\parse_ff_Bt#1_#2{\r_
        \edef\_sshead{\_head}\hs_#1_\r_
        \ts_\_tail _\r_
        \if_empty\edef\_argf{\_sshead}\edef\_args{\_sshead}\else
                \ffc_\_tail _\r_
                \if_inchars\edef\_shead{\_head}\ts_\_tail _\r_
                        \if_empty\edef\_argf{\_sshead}\edef\_args{\_shead}\else
\_fout{Wrong binary fork specification}%
{Node #2: Your input is _#1_ After two valid characters remains garbage:!%
_\_tail _ I expected one or two of the characters / : '!%
I skip it, you can proceed.}\r_
                        \edef\_argf{\_sshead}\edef\args{\_shead}\fi\r_
                \else\r_
\_fout{Wrong binary fork specification}%
{Node #2: You specify _\_head _ for the second branch. I expect one!%
of the characters / : ' I replace it by /. You can proceed.}\r_
                \edef\_argf{\_sshead}\edef\_args{f}\fi\r_
        \fi}

\def\parse_ff_Bp#1_#2{\r_
        \edef\_sshead{\_head}\hs_#1_\r_
        \ts_\_tail _\r_
        \if_empty\edef\_arg{\_sshead}\else
                \ffc_\_tail _\r_
                \if_inchars\edef\_shead{\_head}\ts_\_tail _\r_
                        \if_empty\edef\_arg{\_sshead}\else
\_fout{Wrong binary fork specification}%
{Node #2: Your input is _#1_ After two valid characters remains garbage:!%
_\_tail _ I expected one or two of the characters / : '!%
However, the second one will be ignored. I skip it, you can proceed.}\r_
                        \edef\_arg{\_sshead}\fi\r_
                \else\r_
\_fout{Wrong binary fork specification}%
{Node #2: You specify _\_head _ for the second branch. I expect one!%
of the characters / : ' I replace it by /.!%
By the way, the second character will always be ignored. You can proceed.}\r_
                \edef\_arg{\_sshead}\fi\r_
        \fi}


%       USER INTERFACE: GENERAL

\def\_nc#1#2#3{\let\_tempe#1\def\_tempa{#2}\def\_tempb{#3}\r_
        \futurelet\_tempc\_ifnch}

\def\_ncsp#1#2#3{\let\_tempe#1\def\_tempa{#2}\def\_tempb{#3}\r_
        \futur_splet\_tempc\_ifnch}

\def\_ifnch{\ifx\_tempc\_tempe\let\_tempr\_tempa\else\let\_tempr\_tempb\fi\_tempr}

\def\first_split#1#2#3#4{\def\_tmpa{#1}\def\_tmpb{#2}\def\_tmpc{#3}\r_
        \def\_tmpd{#4}\futur_splet\_tmpn\_first}

\def\_first{\r_
        \let_oc_\_tmpn _[_\if_inchars\let\_tmpr\_tmpa\else
        \let_oc_\_tmpn _.$;,:^-!0*&_\if_inchars\let\_tmpr\_tmpb\else
        \let_oc_\_tmpn _"_\if_inchars\let\_tmpr\_tmpc\else
        \let\_tmpr\_tmpd\fi\fi\fi\_tmpr}

\def\second_split#1#2#3{\def\_tmpa{#1}\def\_tmpb{#2}\def\_tmpc{#3}\r_
        \futur_splet\_tmpn\_second}

\def\_second{\r_
        \let_oc_\_tmpn _.$;,:^-!0*&_\if_inchars\let\_tmpr\_tmpa\else
        \let_oc_\_tmpn _"_\if_inchars\let\_tmpr\_tmpb\else
        \let\_tmpr\_tmpc\fi\fi\_tmpr}

\def\third_split#1#2{\def\_tmpa{#1}\def\_tmpb{#2}\r_
        \futur_splet\_tmpn\_third}

\def\_third{\r_
        \let_oc_\_tmpn _"_\if_inchars\let\_tmpr\_tmpa\else
        \let\_tmpr\_tmpb\fi\_tmpr}

\def\parse_opi#1#2#3#4#5#6{\def\_tmpa{#2}\def\_tmpb{#3}\def\_tmpc{#4}\r_
        \def\_tmpd{#5}\def\_tmpe{#6}\hs_#1_\l_t\_tmpn\_head\_opi}

\def\_opi{\r_
        \fl_\_tmpn _\if_inchars\let\_tmpr\_tmpa\else
        \fd_\_tmpn _\if_inchars\let\_tmpr\_tmpb\else
        \fr_\_tmpn _\if_inchars\let\_tmpr\_tmpc\else
        \ff_\_tmpn _\if_inchars\let\_tmpr\_tmpd\else
        \let\_tmpr\_tmpe\fi\fi\fi\fi\_tmpr}

\def\parse_opii#1#2#3#4#5{\def\_tmpa{#2}\def\_tmpb{#3}\def\_tmpc{#4}\r_
        \def\_tmpd{#5}\hs_#1_\l_t\_tmpn\_head\_opii}

\def\_opii{\r_
        \fd_\_tmpn _\if_inchars\let\_tmpr\_tmpa\else
        \fr_\_tmpn _\if_inchars\let\_tmpr\_tmpb\else
        \ff_\_tmpn _\if_inchars\let\_tmpr\_tmpc\else
        \let\_tmpr\_tmpd\fi\fi\fi\_tmpr}

\def\parse_opiii#1#2#3{\def\_tmpa{#2}\def\_tmpb{#3}\r_
        \hs_#1_\l_t\_tmpn\_head\_opiii}

\def\_opiii{\r_
        \ff_\_tmpn _\if_inchars\let\_tmpr\_tmpa\else
        \let\_tmpr\_tmpb\fi\_tmpr}

% xyz means: optional args x y z has been determined, xy: x and y etc.
% u means: still unknown, xu: first arg known, rest not yet etc.
% f means: second argument is just a dimen, r means: <dimen and
% (possibly) index

% Names must begin with a letter, dims begin with .-(0-9), fork spec with /:'
% this enables identification of arguments

%       USER INTERFACE: BINARY for PICTREES

\def\user_Bt{\trac_off\r_
        \new_B\r_
        \first_split{\u_Bt}{\xyzp_f_Bt[1em][ff]}{\xyzp_f_Bt[1em][ff]:}%
{\xyzpl_f_Bt[1em][ff]0"4pt"}}

\def\u_Bt[#1]{\parse_opi{#1}{\parse_name{#1}\x_Bt}%
{\parse_dim_t#1_\_self\xy_f_Bt[\the\d_ccc]}%
{\parse_rdim_Bt#1_\_self\xy_r_Bt<\n_\d_ccc,\_index>}%
{\parse_ff_Bt#1_\_self\xyz_f_Bt[1em][\_argf\_args]}%
{\xyzpl_f_Bt[1em][ff]0 "4pt"\r_
\_fout{Error in options}%
{Binary node \_self: Your first option is neither a name, nor a rigid or!%
flexibel dimen, nor a fork specification. This is serious, but I shall!%
insert a default node (circle 4pt)}}}

\def\x_Bt{\first_split{\xu_Bt}{\xyzp_f_Bt[1em][ff]}{\xyzp_f_Bt[1em][ff]:}%
{\xyzpl_f_Bt[1em][ff]0"4pt"}}

\def\xu_Bt[#1]{\parse_opii{#1}%
{\parse_dim_t#1_\_self\xy_f_Bt[\the\d_ccc]}%
{\parse_rdim_Bt#1_\_self\xy_r_Bt<\n_\d_ccc,\_index>}%
{\parse_ff_Bt#1_\_self\xyz_f_Bt[1em][\_argf\_args]}%
{\xyzpl_f_Bt[1em][ff]0 "4pt"\r_
\_fout{Error in options}%
{Binary node \_self: Your second option is neither a rigid nor!%
flexibel dimen, nor a fork specification. This is serious, but I shall!%
insert a default node (circle 4pt)}}}

\def\xy_f_Bt[#1]{\first_split{\xyu_f_Bt[#1]}{\xyzp_f_Bt[#1][ff]}{\xyzp_f_Bt[#1][ff]:}{\xyzpl_f_Bt[#1][ff]0"4pt"}}

\def\xy_r_Bt<#1,#2>{\first_split{\xyu_r_Bt<#1,#2>}{\xyzp_r_Bt<#1,#2>[ff]}{\xyzp_r_Bt<#1,#2>[ff]:}{\xyzpl_r_Bt<#1,#2>[ff]0"4pt"}}

\def\xyu_f_Bt[#1][#2]{\parse_opiii{#2}%
{\parse_ff_Bt#2_\_self\xyz_f_Bt[#1][\_argf\_args]}%
{\xyzpl_f_Bt[#1][ff]0 "4pt"\r_
\_fout{Error in options}%
{Binary node \_self: Your third option is not a fork specification.!%
This is serious, but I shall insert a default node (circle 4pt)}}}

\def\xyu_r_Bt<#1,#2>[#3]{\parse_opiii{#3}%
{\parse_ff_Bt#3_\_self\xyz_r_Bt<#1,#2>[\_argf\_args]}%
{\xyzpl_r_Bt<#1,#2>[ff]0 "4pt"\r_
\_fout{Error in options}%
{Binary node \_self: Your third option is not a fork specification.!%
This is serious, but I shall insert a default node (circle 4pt)}}}

\def\xyz_f_Bt[#1][#2]{\second_split{\xyzp_f_Bt[#1][#2]}{\xyzp_f_Bt[#1][#2]:}%
{\xyzpl_f_Bt[#1][#2]0"4pt"}}

\def\xyz_r_Bt<#1,#2>[#3]{\second_split{\xyzp_r_Bt<#1,#2>[#3]}{\xyzp_r_Bt<#1,#2>[#3]:}%
{\xyzpl_r_Bt<#1,#2>[#3]0"4pt"}}

\def\xyzp_f_Bt[#1][#2]#3{\third_split{\xyzpl_f_Bt[#1][#2]#3}%
{\if#30\def\_lab{4pt}\else
 \if#3*\def\_lab{4pt}\else
 \if#3&\def\_lab{4pt}\else
 \if#3-\def\_lab{0pt}\else
 \if#3!\def\_lab{4pt}\else
        \def\_lab{LABEL}\fi\fi\fi\fi\fi\r_
 \xyzpl_f_Bt[#1][#2]#3"\_lab"}}

\def\xyzp_r_Bt<#1,#2>[#3]#4{\third_split{\xyzpl_r_Bt<#1,#2>[#3]#4}%
{\if#40\def\_lab{4pt}\else
 \if#4*\def\_lab{4pt}\else
 \if#4&\def\_lab{4pt}\else
 \if#4-\def\_lab{0pt}\else
 \if#4!\def\_lab{0pt}\else
        \def\_lab{LABEL}\fi\fi\fi\fi\fi\r_
 \xyzpl_r_Bt<#1,#2>[#3]#4"\_lab"}}

\def\xyzpl_f_Bt[#1][#2]#3"#4"{\third_split{\xyzplt_f_Bt[#1][#2]#3"#4"}%
{\xyzplt_f_Bt[#1][#2]#3"#4"""}}

\def\xyzplt_f_Bt[#1][#2]#3"#4""#5"{\trac_on\r_
        \comp_rigid_B#3[#1]{#4}:\_left--\_right--\r_
        \_btree\_index#2<\n_\d_ccc>\_self--\_left--\_right--\is_}

\def\xyzpl_r_Bt<#1,#2>[#3]#4"#5"{\third_split{\xyzplt_r_Bt<#1,#2>[#3]#4"#5"}%
{\xyzplt_r_Bt<#1,#2>[#3]#4"#5"""}}

\def\xyzplt_r_Bt<#1,#2>[#3]#4"#5""#6"{\trac_on\r_
        \_node B#4#5--t\r_
        \_btree#2#3<#1>\_self--\_left--\_right--\is_}

%       USER INTERFACE: UNARY for PICTREES

\def\user_Ut{\trac_off\r_
        \new_U\r_
        \first_split{\u_Ut}{\xyzp_f_Ut[3ex][f]}{\xyzp_f_Ut[3ex][f]:}%
{\xyzpl_f_Ut[3ex][f]0"4pt"}}

\def\u_Ut[#1]{\parse_opi{#1}{\parse_name{#1}\x_Ut}%
{\parse_dim_t#1_\_self\xy_f_Ut[\the\d_ccc]}%
{\parse_rdim_Ut#1_\_self\xy_r_Ut<\n_\d_ccc>}%
{\parse_ff_U#1_\_self\xyz_f_Ut[3ex][\_arg]}%
{\xyzpl_f_Ut[3ex][f]0 "4pt"\r_
\_fout{Error in options}%
{Unary node \_self: Your first option is neither a name, nor a rigid or!%
flexibel dimen, nor a fork specification. This is serious, but I shall!%
insert a default node (circle 4pt)}}}

\def\x_Ut{\first_split{\xu_Ut}{\xyzp_f_Ut[3ex][f]}{\xyzp_f_Ut[3ex][f]:}%
{\xyzpl_f_Ut[3ex][f]0"4pt"}}

\def\xu_Ut[#1]{\parse_opii{#1}%
{\parse_dim_t#1_\_self\xy_f_Ut[\the\d_ccc]}%
{\parse_rdim_Ut#1_\_self\xy_r_Ut<\n_\d_ccc>}%
{\parse_ff_U#1_\_self\xyz_f_Ut[3ex][\_arg]}%
{\xyzpl_f_Ut[3ex][f]0 "4pt"\r_
\_fout{Error in options}%
{Unary node \_self: Your second option is neither a rigid nor!%
flexibel dimen, nor a fork specification. This is serious, but I shall!%
insert a default node (circle 4pt)}}}

\def\xy_f_Ut[#1]{\first_split{\xyu_f_Ut[#1]}%
{\xyzp_f_Ut[#1][f]}{\xyzp_f_Ut[#1][f]:}{\xyzpl_f_Ut[#1][f]0"4pt"}}

\def\xy_r_Ut<#1>{\first_split{\xyu_r_Ut<#1>}%
{\xyzp_r_Ut<#1>[f]}{\xyzp_r_Ut<#1>[f]:}{\xyzpl_r_Ut<#1>[f]0"4pt"}}

\def\xyu_f_Ut[#1][#2]{\parse_opiii{#2}%
{\parse_ff_U#2_\_self\xyz_f_Ut[#1][\_arg]}%
{\xyzpl_f_Ut[#1][f]0 "4pt"\r_
\_fout{Error in options}%
{Unary node \_self: Your third option is not a fork specification.!%
This is serious, but I shall insert a default node (circle 4pt)}}}

\def\xyu_r_Ut<#1>[#2]{\parse_opiii{#2}%
{\parse_ff_U#2_\_self\xyz_r_Ut<#1>[\_arg]}%
{\xyzpl_r_Ut<#1>[f]0 "4pt"\r_
\_fout{Error in options}%
{Unary node \_self: Your third option is not a fork specification.!%
This is serious, but I shall insert a default node (circle 4pt)}}}

\def\xyz_f_Ut[#1][#2]{\second_split{\xyzp_f_Ut[#1][#2]}{\xyzp_f_Ut[#1][#2]:}%
{\xyzpl_f_Ut[#1][#2]0"4pt"}}

\def\xyz_r_Ut<#1>[#2]{\second_split{\xyzp_r_Ut<#1>[#2]}{\xyzp_r_Ut<#1>[#2]:}%
{\xyzpl_r_Ut<#1>[#2]0"4pt"}}

\def\xyzp_f_Ut[#1][#2]#3{\third_split{\xyzpl_f_Ut[#1][#2]#3}%
{\if#30\def\_lab{4pt}\else
 \if#3*\def\_lab{4pt}\else
 \if#3&\def\_lab{4pt}\else
 \if#3-\def\_lab{0pt}\else
 \if#3!\def\_lab{4pt}\else
        \def\_lab{LABEL}\fi\fi\fi\fi\fi\r_
 \xyzpl_f_Ut[#1][#2]#3"\_lab"}}

\def\xyzp_r_Ut<#1>[#2]#3{\third_split{\xyzpl_r_Ut<#1>[#2]#3}%
{\if#30\def\_lab{4pt}\else
 \if#3*\def\_lab{4pt}\else
 \if#3&\def\_lab{4pt}\else
 \if#3-\def\_lab{0pt}\else
 \if#3!\def\_lab{4pt}\else
        \def\_lab{LABEL}\fi\fi\fi\fi\fi\r_
 \xyzpl_r_Ut<#1>[#2]#3"\_lab"}}

\def\xyzpl_f_Ut[#1][#2]#3"#4"{\third_split{\xyzplt_f_Ut[#1][#2]#3"#4"}%
{\xyzplt_f_Ut[#1][#2]#3"#4"""}}

\def\xyzplt_f_Ut[#1][#2]#3"#4""#5"{\trac_on\r_
        \comp_rigid_U#3[#1]{#4}:\_above--\r_
        \_utree#2<\n_\d_ccc>\_self--\_above--\is_}

\def\xyzpl_r_Ut<#1>[#2]#3"#4"{\third_split{\xyzplt_r_Ut<#1>[#2]#3"#4"}%
{\xyzplt_r_Ut<#1>[#2]#3"#4"""}}

\def\xyzplt_r_Ut<#1>[#2]#3"#4""#5"{\trac_on\r_
        \_node U#3#4--t\r_
        \_utree#2<#1>\_self--\_above--\is_}

%       USER INTERFACE: AXIOMS for PICTREES

\def\user_At{\trac_off\r_
        \new_A\first_split{\u_At}{\xp_At}{\xp_At:}{\xpl_At0"4pt"}}

\def\u_At[#1]{\parse_opi{#1}{\parse_name{#1}\x_At}%
{\_fout{Error in options}%
{Axiom node \_self: Your first option _#1_ is probably a dimen.!%
Only a name is appropriate here. Names must begin with a letter.!%
I ignore your option and proceed.}\x_At}%
{\_fout{Error in options}%
{Axiom node \_self: Your first option _#1_ is probably a rigid dimen.!%
Only a name is appropriate here. Names must begin with a letter.!%
I ignore your option and proceed.}\x_At}%
{\_fout{Error in options}%
{Axiom node \_self: Your first option _#1_ is probably a fork specification.!%
Only a name is appropriate here. Names must begin with a letter.!%
I ignore your option and proceed.}\x_At}%
{\_fout{Error in options}%
{Axiom node \_self: Your first option _#1_ is not a name.!%
Names must begin with a letter. I ignore your option and proceed.}\x_At}}

\def\x_At{\first_split{\r_
\_fout{Error in options}%
{Axiom node \_self: You specify a second option,!%
where only one is appropriate. I ignore your option and proceed.}\xd_At}%
{\xp_At}{\xp_At:}{\xpl_At0"4pt"}}

\def\xd_At[#1]{\first_split{\r_
\_fout{Error in options}%
{Axiom node \_self: You specify a third option,!%
where only one is appropriate. I ignore your option and proceed.}\xdd_At}%
{\xp_At}{\xp_At:}{\xpl_At0"4pt"}}

\def\xdd_At[#1]{\first_split{\r_
\_fout{Error in options}%
{Axiom node \_self: You specify more than three options, !%
where only one is appropriate. I proceed, but do not ignore your options!%
anymore. Probably you will find garbage in the output.}\xp_At}%
{\xp_At}{\xp_At:}{\xpl_At0"4pt"}}

\def\xp_At#1{\third_split{\xpl_At#1}%
{\if#10\def\_lab{4pt}\else
 \if#1*\def\_lab{4pt}\else
 \if#1&\def\_lab{4pt}\else
 \if#1-\def\_lab{0pt}\else
 \if#1!\def\_lab{4pt}\else
        \def\_lab{LABEL}\fi\fi\fi\fi\fi\r_
 \xpl_At#1"\_lab"}}

\def\xpl_At#1"#2"{\trac_on\r_
        \_node A#1#2--t\_axtree\_self--\is_}

%       USER INTERFACE: BINARY for PROOF TREES

\def\user_Bp{\trac_off\r_
        \new_B\r_
        \first_split{\u_Bp}{\xyzp_Bp[1em][f]}{\xyzp_Bp[1em][f].}%
{\xyzpl_Bp[1em][f]0"4pt"}}

\def\u_Bp[#1]{\parse_opi{#1}{\parse_name{#1}\x_Bp}%
{\parse_dim_t#1_\_self\xy_Bp[\the\d_ccc]}%
{\parse_rdim_Bp#1_\_self\xy_Bp[\the\d_ccc]}%
{\parse_ff_Bp#1_\_self\xyz_Bp[1em][\_arg]}%
{\xyzpl_Bp[1em][f]0 "4pt"\r_
\_fout{Error in options}%
{Binary node \_self: Your first option is neither a name, nor a!%
dimen, nor a fork specification. This is serious, but I shall!%
insert a default node (circle 4pt)}}}

\def\x_Bp{\first_split{\xu_Bp}{\xyzp_Bp[1em][f]}{\xyzp_Bp[1em][f].}%
{\xyzpl_Bp[1em][f]0"4pt"}}

\def\xu_Bp[#1]{\parse_opii{#1}%
{\parse_dim_t#1_\_self\xy_Bp[\the\d_ccc]}%
{\parse_rdim_Bp#1_\_self\xy_Bp[\the\d_ccc]}%
{\parse_ff_Bp#1_\_self\xyz_Bp[1em][\_arg]}%
{\xyzpl_Bp[1em][f]0 "4pt"\r_
\_fout{Error in options}%
{Binary node \_self: Your second option is neither a!%
dimen, nor a fork specification. This is serious, but I shall!%
insert a default node (circle 4pt)}}}

\def\xy_Bp[#1]{\first_split{\xyu_Bp[#1]}%
{\xyzp_Bp[#1][f]}{\xyzp_Bp[#1][f].}{\xyzpl_Bp[#1][f]0"4pt"}}

\def\xyu_Bp[#1][#2]{\parse_opiii{#2}%
{\parse_ff_Bp#2_\_self\xyz_Bp[#1][\_arg]}%
{\xyzpl_Bp[#1][f]0 "4pt"\r_
\_fout{Error in options}%
{Binary node \_self: Your third option is not a fork specification.!%
This is serious, but I shall insert a default node (circle 4pt)}}}

\def\xyz_Bp[#1][#2]{\second_split{\xyzp_Bp[#1][#2]}{\xyzp_Bp[#1][#2].}%
{\xyzpl_Bp[#1][#2]0"4pt"}}

\def\xyzp_Bp[#1][#2]#3{\third_split{\xyzpl_Bp[#1][#2]#3}%
{\if#30\def\_lab{4pt}\else
 \if#3*\def\_lab{4pt}\else
 \if#3&\def\_lab{4pt}\else
 \if#3-\def\_lab{0pt}\else
 \if#3!\def\_lab{4pt}\else
        \def\_lab{LABEL}\fi\fi\fi\fi\fi\r_
 \xyzpl_Bp[#1][#2]#3"\_lab"}}

\def\xyzpl_Bp[#1][#2]#3"#4"{\third_split{\xyzplt_Bp[#1][#2]#3"#4"}%
{\xyzplt_Bp[#1][#2]#3"#4"""}}

\def\xyzplt_Bp[#1][#2]#3"#4""#5"{\trac_on\r_
        \_bproof[#1]#3 {#4} ---(#5) ---\_self--\_left--\_right:#2\is_}

%       USER INTERFACE: UNARY for PROOF TREES

\def\user_Up{\trac_off\r_
        \new_U\r_
        \first_split{\u_Up}{\xyzp_Up[1em][f]}{\xyzp_Up[1em][f].}%
{\xyzpl_Up[1em][f]0"4pt"}}

\def\u_Up[#1]{\parse_opi{#1}{\parse_name{#1}\x_Up}%
{\parse_dim_p#1_\_self\xy_Up[\the\d_ccc]}%
{\parse_rdim_Up#1_\_self\xy_Up[\the\d_ccc]}%
{\parse_ff_U#1_\_self\xyz_Up[1em][\_arg]}%
{\xyzpl_Up[1em][f]0 "4pt"\r_
\_fout{Error in options}%
{Unary node \_self: Your first option is neither a name,!%
nor a fork specification. This is serious, but I shall!%
insert a default node (circle 4pt)}}}

\def\x_Up{\first_split{\xu_Up}{\xyzp_Up[1em][f]}{\xyzp_Up[1em][f].}%
{\xyzpl_Up[1em][f]0"4pt"}}

\def\xu_Up[#1]{\parse_opii{#1}%
{\parse_dim_p#1_\_self\xy_Up[\the\d_ccc]}%
{\parse_rdim_Up#1_\_self\xy_Up[\the\d_ccc]}%
{\parse_ff_U#1_\_self\xyz_Up[1em][\_arg]}%
{\xyzpl_Up[1em][f]0 "4pt"\r_
\_fout{Error in options}%
{Unary node \_self: Your second option is not a fork specification.!%
This is serious, but I shall insert a default node (circle 4pt)}}}

\def\xy_Up[#1]{\first_split{\xyu_Up[#1]}%
{\xyzp_Up[#1][f]}{\xyzp_Up[#1][f].}{\xyzpl_Up[#1][f]0"4pt"}}

\def\xyu_Up[#1][#2]{\parse_opiii{#2}%
{\parse_ff_U#2_\_self\xyz_Up[#1][\_arg]}%
{\xyzpl_Up[#1][f]0 "4pt"\r_
\_fout{Error in options}%
{Unary node \_self: Your third option is not a fork specification.!%
This is serious, but I shall insert a default node (circle 4pt)}}}

\def\xyz_Up[#1][#2]{\second_split{\xyzp_Up[#1][#2]}{\xyzp_Up[#1][#2].}%
{\xyzpl_Up[#1][#2]0"4pt"}}

\def\xyzp_Up[#1][#2]#3{\third_split{\xyzpl_Up[#1][#2]#3}%
{\if#30\def\_lab{4pt}\else
 \if#3*\def\_lab{4pt}\else
 \if#3&\def\_lab{4pt}\else
 \if#3-\def\_lab{0pt}\else
 \if#3!\def\_lab{4pt}\else
        \def\_lab{LABEL}\fi\fi\fi\fi\fi\r_
 \xyzpl_Up[#1][#2]#3"\_lab"}}

\def\xyzpl_Up[#1][#2]#3"#4"{\third_split{\xyzplt_Up[#1][#2]#3"#4"}%
{\xyzplt_Up[#1][#2]#3"#4"""}}

\def\xyzplt_Up[#1][#2]#3"#4""#5"{\trac_on\r_
        \_uproof#3 {#4} ---(#5) ---\_self--\_above:#2\is_}

%       USER INTERFACE: AXIOMS for PROOF TREES

\def\user_Ap{\trac_off\r_
        \new_A\first_split{\u_Ap}{\xp_Ap}{\xp_Ap.}{\xpl_Ap0"4pt"}}

\def\u_Ap[#1]{\parse_opi{#1}{\parse_name{#1}\x_Ap}%
{\_fout{Error in options}%
{Axiom node \_self: Your first option _#1_ is probably a dimen.!%
Only a name is appropriate here. Names must begin with a letter.!%
I ignore your option and proceed.}\x_Ap}%
{\_fout{Error in options}%
{Axiom node \_self: Your first option _#1_ is probably a rigid dimen.!%
Only a name is appropriate here. Names must begin with a letter.!%
I ignore your option and proceed.}\x_Ap}%
{\_fout{Error in options}%
{Axiom node \_self: Your first option _#1_ is probably a fork specification.!%
Only a name is appropriate here. Names must begin with a letter.!%
I ignore your option and proceed.}\x_Ap}%
{\_fout{Error in options}%
{Axiom node \_self: Your first option _#1_ is not a name.!%
Names must begin with a letter. I ignore your option and proceed.}\x_Ap}}

\def\x_Ap{\first_split{\r_
\_fout{Error in options}%
{Axiom node \_self: You specify a second option,!%
where only one is appropriate. I ignore your option and proceed.}\xd_Ap}%
{\xp_Ap}{\xp_Ap.}{\xpl_Ap0"4pt"}}

\def\xd_Ap[#1]{\first_split{\r_
\_fout{Error in options}%
{Axiom node \_self: You specify a third option,!%
where only one is appropriate. I ignore your option and proceed.}\xdd_Ap}%
{\xp_Ap}{\xp_Ap.}{\xpl_Ap0"4pt"}}

\def\xdd_Ap[#1]{\first_split{\r_
\_fout{Error in options}%
{Axiom node \_self: You specify more than three options, !%
where only one is appropriate. I proceed, but do not ignore your options!%
anymore. Probably you will find garbage in the output.}\xp_Ap}%
{\xp_Ap}{\xp_Ap.}{\xpl_Ap0"4pt"}}

\def\xp_Ap#1{\third_split{\xpl_Ap#1}%
{\if#10\def\_lab{4pt}\else
 \if#1*\def\_lab{4pt}\else
 \if#1&\def\_lab{4pt}\else
 \if#1-\def\_lab{0pt}\else
 \if#1!\def\_lab{4pt}\else
        \def\_lab{LABEL}\fi\fi\fi\fi\fi\r_
 \xpl_Ap#1"\_lab"}}

\def\xpl_Ap#1"#2"{\trac_on\r_
        \_axproof#1 {#2} ---\_self:\is_}

%       USER INTERFACE: INSERT

\def\user_I{\_ncsp[{\x_I}{\x_I[\r_m\n_me]}}

\def\x_I[#1]{\r_
        \if_u{us_dN_M#1}\_fout{Name not defined}%
{You use the name _#1_ which I do not know.!%
Instead I use the internal name of the most recently generated tree.}\r_
        \edef\_tmpa{\cs_ N_M\r_m\n_me\es_}\else\edef\_tmpa{N_M#1}\fi\r_
        \new_A\r_
        \c_p{\cs_ N_M\r_m\n_me\es_}{\cs_ \_tmpa\es_}\r_
        \ifnum\tr_a>0\r_
        \wlog{I: use of name _#1_ is \cs_ N_M\r_m\n_me\es_}\fi\is_}

%       USER INTERFACE: CONNECT

\def\conn_split#1#2#3#4{\def\_tmpa{#1}\def\_tmpb{#2}\def\_tmpc{#3}\r_
        \def\_tmpd{#4}\futur_splet\_tmpn\_conn}

\def\_conn{\r_
        \let_oc_\_tmpn _[_\if_inchars\let\_tmpr\_tmpa\else
        \let_oc_\_tmpn _Aabxnlr_\if_inchars\let\_tmpr\_tmpb\else
        \let_oc_\_tmpn _"_\if_inchars\let\_tmpr\_tmpc\else
        \let\_tmpr\_tmpd\fi\fi\fi\_tmpr}

\def\con_split#1#2#3{\def\_tmpa{#1}\def\_tmpb{#2}\def\_tmpc{#3}\r_
        \futur_splet\_tmpn\_con}

\def\_con{\r_
        \let_oc_\_tmpn _Aabxnlrc_\if_inchars\let\_tmpr\_tmpa\else
        \let_oc_\_tmpn _"_\if_inchars\let\_tmpr\_tmpb\else
        \let\_tmpr\_tmpc\fi\fi\_tmpr}

\def\co_split#1#2{\def\_tmpa{#1}\def\_tmpb{#2}\r_
        \futur_splet\_tmpn\_co}

\def\_co{\r_
        \let_oc_\_tmpn _"_\if_inchars\let\_tmpr\_tmpa\else
        \let\_tmpr\_tmpb\fi\_tmpr}

\def\ch_C#1#2{\def\_tmpa{#1}\def\_tmpb{#2}\r_
        \ifnum\INIT_=1001\let\_tmpr\_tmpa\else\let\_tmpr\_tmpb\fi\_tmpr}

\def\wrong_node{\_fout{Forbidden node specification}%
{Since you gave commands that imply that your tree is finished!%
(connect or or put or show coordinates), further node specification is!%
prohibited. I leave all your arguments as garbage in the output.}}

\long\def\wrong_C#1"#2"{\_fout{Connections}%
{In the BLIST ELIST environment the connection commands must!%
appear outside the bpt ept environments. I ignore this connection.}\is_}

\def\good_C{\trac_off\r_
        \let\A\wrong_node\r_
        \let\B\wrong_node\r_
        \let\U\wrong_node\r_
        \let\I\wrong_node\r_
        \conn_split{\u_C}{\u_C[1ex]}{\xy_C[1ex]x}%
{\_fout{Connections}{You specify a connection without telling me!%
what to connect. I expect "name1 name2". I ignore this connection.}}}

\def\user_Ct{\ch_C{\wrong_C}{\good_C}}

\def\u_C[#1]{\con_split{\xy_C[#1]}{\xy_C[#1]x}%
{\_fout{Connections}{You specify a connection without telling me!%
what to connect. I expect "name1 name2". I ignore this connection.}}}

\def\xy_C[#1]#2{\co_split{\trac_on\_C[#1]#2}%
{\_fout{Connections}{You specify a connection without telling me!%
what to connect. I expect "name1 name2". I ignore this connection.}}}

\def\_C[#1]#2"#3 #4"{\trac_off\r_
        \if_u{us_dN_M#3}\_fout{Name not defined}%
{You use the name _#3_ which I do not know.!%
Instead I use the internal name of the most recently generated tree.}\r_
        \edef\_tmpa{\cs_ N_M\r_m\n_me\es_}\else\edef\_tmpa{N_M#3}\fi\r_
        \if_u{us_dN_M#4}\_fout{Name not defined}%
{You use the name _#4_ which I do not know.!%
Instead I use the internal name of the most recently generated tree.}\r_
        \edef\_tmpb{\cs_ N_M\r_m\n_me\es_}\else\edef\_tmpb{N_M#4}\fi\r_
        \ifnum\tr_a>0\r_
        \wlog{C: use of names _\_tmpa _ is \cs_ N_M#3\es_\space
                         and _\_tmpb _ is \cs_ N_M#4\es_}\fi\r_
        \d_fcc#1\r_
\ifnum\INIT_=1000\r_
        \_connect:\cs_ \_tmpa\es_^{\n_\cs_ thi_\cs_ \_tmpa\es_\es_} with
        \cs_ \_tmpb\es_^{\n_\cs_ thi_\cs_ \_tmpb\es_\es_} at {\n_\d_fcc}^{#2}:\r_
\else\r_
        \_root\cs_ N_M\r_m\n_me\es_--\r_
        \THI_\cs_ thi_N_M\r_m\n_me\es_\r_
        \ea_\m_savebox\cs_ b_x\cs_ N_M\r_m\n_me\es_\es_(\n_\d_acc,\n_\d_ecc){\r_
        \_bpic(\n_\d_acc,\n_\d_ecc)(\n_\d_ccc,\n_\d_dcc)\r_
        \_connect:\cs_ \_tmpa\es_^{\n_\cs_ thi_\cs_ \_tmpa\es_\es_} with
        \cs_ \_tmpb\es_^{\n_\cs_ thi_\cs_ \_tmpb\es_\es_} at {\n_\d_fcc}^{#2}:\r_
        \m_put(\n_\d_ccc,\n_\d_dcc){\r_
                \ea_\useb_x\cs_ b_x\cs_ N_M\r_m\n_me\es_\es_}\r_
        \_epic}\r_
\fi\r_
        \trac_on\is_}

%       USER INTERFACE: PUT
        
\def\short_name N_M#1{#1}
\def\sh_nm#1{\edef\d_m{\nx_\short_name\cs_ N_M#1\es_}\d_m}

\def\user_PTt{\_ncsp[{\x_PT}{\x_PT[\r_m\n_me]}}

\def\x_PT[#1]{\third_split{\xo_PT[#1]}%
{\xo_PT[#1]"\m_makebox(0,0){\sh_nm{#1}}"}}

\def\xo_PT{\ch_C{\wrong_x_PT}{\good_x_PT}}

\long\def\wrong_x_PT[#1]"#2"{\_fout{Put command}%
{In the BLIST ELIST environment the put commands must!%
appear outside the bpt ept environments. I ignore this put command.}\is_}

\def\good_x_PT[#1]"#2"{\trac_off\r_
        \ifnum\tr_a>0\r_
        \wlog{PT: use of name _#1_ is \cs_ N_M#1\es_}\fi\r_
        \let\A\wrong_node\r_
        \let\B\wrong_node\r_
        \let\U\wrong_node\r_
        \let\I\wrong_node\r_
        \ifnum\INIT_=1000\r_\else\_root\cs_ N_M\r_m\n_me\es_--\fi\r_
        \cs_ xc_r\cs_ N_M#1\es_\es_\cur_x\r_\d_xcc\r_s\r_
        \cs_ yc_r\cs_ N_M#1\es_\es_\cur_y\r_
\ifnum\INIT_=1000\r_
        \_put(\n_\d_xcc,\n_\r_s){#2}\r_
\else\r_
        \ea_\m_savebox\cs_ b_x\cs_ N_M\r_m\n_me\es_\es_(\n_\d_acc,\n_\d_ecc){\r_
        \_bpic(\n_\d_acc,\n_\d_ecc)(\n_\d_ccc,\n_\d_dcc)\r_
        \_put(\n_\d_xcc,\n_\r_s){#2}\r_
   \m_put(\n_\d_ccc,\n_\d_dcc){\ea_\useb_x\cs_ b_x\cs_ N_M\r_m\n_me\es_\es_}\r_
        \_epic}\r_
\fi\r_
        \trac_on\is_}

%       USER INTERFACE: SHOW
        
\def\user_SHt{\_ncsp[{\x_SH}{\x_SH[\r_m\n_me]}}

\def\x_SH{\ch_C{\wrong_x_SH}{\good_x_SH}}

\long\def\wrong_x_SH[#1]{\_fout{Show coordinates}%
{In the BLIST ELIST environment the show commands must!%
appear outside the bpt ept environments. I ignore this show command.}\is_}

\def\good_x_SH[#1]{\trac_off\r_
        \ifnum\tr_a>0\r_
        \wlog{SH: use of name _#1_ is \cs_ N_M#1\es_}\fi\r_
        \let\A\wrong_node\r_
        \let\B\wrong_node\r_
        \let\U\wrong_node\r_
        \let\I\wrong_node\r_
        \ifnum\INIT_=1000\r_\else\_root\cs_ N_M\r_m\n_me\es_--\fi\r_
        \cs_ xc_r\cs_ N_M#1\es_\es_\cur_x\r_\d_acc\r_s\r_
        \cs_ yc_r\cs_ N_M#1\es_\es_\cur_y\r_
        \typeout{#1: x= \n_\d_acc\space, y= \n_\r_s}\r_
        \trac_on\is_}

%       USER INTERFACE: ENVIRONMENTS for PICTREES

\newcount\INIT_\g_\INIT_0

\newif\if_fst

\newcount\_pall\_pall0
\newcount\_tall\_tall0
\newcount\_ptall\_ptall0

\long\def\in_BLIST#1\ELIST{\_fout{Inner BLIST}%
{BLIST ELIST is only allowed at the outermost level.!%
I skip everything till the next ELIST.!%
Hope you have not a doubly nested BLIST ...}\is_}

\def\ch_BLIST#1#2{\def\_tmpa{#1}\def\_tmpb{#2}\r_
        \ifnum\INIT_>0\let\_tmpr\_tmpa\else\let\_tmpr\_tmpb\fi\_tmpr}

\def\BLIST{\ch_BLIST{\in_BLIST}{\trac_off\g_\INIT_1000\r_\linen_0\r_
        \bgroup\r_
        \let\n_mestack\_mpty\n_me0\r_
        \ball_cinit\all_cinit\r_
        \ball_c{kladb_x}\r_
        \ball_c{tagb_x}\r_
        \all_c{k_h}\r_
        \all_c{k_d}\r_
        \all_c{k_w}\r_
        \all_c{k_o}\r_
        \all_c{k_e}\r_
        \all_c{exc_}\r_
        \all_c{eexc_}\r_
        \all_c{t_sx}\all_c{t_sy}\r_
        \all_c{t_lne}\all_c{t_lnf}\r_
        \all_c{t_msx}\all_c{t_msy}\r_
        \all_c{t_mne}\all_c{t_mnf}\r_
        \all_c{t_dx}\all_c{t_dy}\r_
        \all_c{t_ex}\all_c{t_ey}\r_
        \all_c{t_fx}\all_c{t_fy}\r_
        \all_c{cur_x}\r_
        \all_c{cur_y}\r_
        \all_c{TBR_}\r_
        \all_c{THI_}\r_
        \all_c{LOF_}\r_
        \all_c{TDP_}\r_
        \ball_c{pre_ious}\r_
        \_tall1\r_
        \_ptall1\r_
        \setbox\pre_ious\hbox\bgroup\r_
        \_bpic(0,0)\is_
        \let\C\user_Ct\r_
        \let\SH\user_SHt\r_
        \let\PT\user_PTt\r_
        \_fsttrue\r_
        \cur_x0pt\cur_y0pt\TBR_0pt\THI_0pt\LOF_0pt\TDP_0pt\r_
        \trac_on\is_}}

\def\ELIST{\trac_off\r_
        \g_\d_acc\TBR_\r_
        \g_\d_bcc\THI_\r_
        \g_\d_ccc\LOF_\r_
        \g_\d_dcc\TDP_\r_
        \_epic\egroup\r_
        \d_ecc\d_bcc\a_\d_ecc\d_dcc\a_\d_ecc1ex\r_
        \_bpic(\n_\d_acc,\n_\d_ecc)%(\n_\d_ccc,\n_\d_dcc)\r_
                \m_put(\n_\d_ccc,\n_\d_dcc){\b_x\pre_ious}\r_
        \_epic\r_
        \bdeall_c{kladb_x}\r_
        \bdeall_c{tagb_x}\r_
        \deall_c{k_h}\r_
        \deall_c{k_d}\r_
        \deall_c{k_w}\r_
        \deall_c{k_o}\r_
        \deall_c{k_e}\r_
        \deall_c{exc_}\r_
        \deall_c{eexc_}\r_
        \deall_c{t_sx}\deall_c{t_sy}\r_
        \deall_c{t_lne}\deall_c{t_lnf}\r_
        \deall_c{t_msx}\deall_c{t_msy}\r_
        \deall_c{t_mne}\deall_c{t_mnf}\r_
        \deall_c{t_dx}\deall_c{t_dy}\r_
        \deall_c{t_ex}\deall_c{t_ey}\r_
        \deall_c{t_fx}\deall_c{t_fy}\r_
        \deall_c{cur_x}\r_
        \deall_c{cur_y}\r_
        \deall_c{TBR_}\r_
        \deall_c{THI_}\r_
        \deall_c{LOF_}\r_
        \deall_c{TDP_}\r_
        \bdeall_c{pre_ious}\r_
        \_tall0\r_
        \_ptall0\r_
        \ball_cfinal\all_cfinal\r_
        \egroup\r_
        \g_\INIT_0\r_\trac_on\r_}

\def\bpt{\trac_off\r_\linen_0\r_
        \_lvm\r_
        \ifnum\INIT_=1000\r_\else\r_
        \bgroup\r_
        \let\n_mestack\_mpty\n_me0\r_
        \ball_cinit\all_cinit\r_
        \ifnum\_ptall>0\a_\_ptall1\r_\else\r_
        \ball_c{kladb_x}\r_
        \ball_c{tagb_x}\r_
        \all_c{k_h}\r_
        \all_c{k_d}\r_
        \all_c{k_w}\r_
        \all_c{k_o}\r_
        \all_c{k_e}\r_
        \all_c{exc_}\r_
        \all_c{eexc_}\r_
        \_ptall1\fi\r_
        \ifnum\_tall>0\a_\_tall1\r_\else\r_
        \all_c{t_sx}\all_c{t_sy}\r_
        \all_c{t_lne}\all_c{t_lnf}\r_
        \all_c{t_msx}\all_c{t_msy}\r_
        \all_c{t_mne}\all_c{t_mnf}\r_
        \all_c{t_dx}\all_c{t_dy}\r_
        \all_c{t_ex}\all_c{t_ey}\r_
        \all_c{t_fx}\all_c{t_fy}\r_
        \all_c{cur_x}\r_\cur_x0pt\r_
        \all_c{cur_y}\r_\cur_y0pt\r_
        \all_c{THI_}\r_\THI_0pt\r_
        \_tall1\fi\r_
        \fi\r_
        \ga_\INIT_1\r_
        \let\A\user_At\r_
        \let\U\user_Ut\r_
        \let\B\user_Bt\r_
        \let\I\user_I\r_
        \let\C\user_Ct\r_
        \let\SH\user_SHt\r_
        \let\PT\user_PTt\r_
        \checkn_me\n_me\r_
        \trac_on\is_}
        
\def\ept{\t_p\cr_s\r_\ifnum\checkn_me=\cr_s\r_
        \let\_tmpa\good_ept\else\let\_tmpa\wrong_ept\fi\_tmpa}

\def\wrong_ept{\_fout{Node stack not empty}%
{The tree I have just typeset does not contain all nodes that you!%
specified. Probably you forgot some binary nodes somewhere.!%
This does not matter very much, proceed.}\good_ept}

\def\good_ept{\ga_\INIT_-1\_ncsp[{\x_ept}{\x_ept[b]}}
\def\x_ept[#1]{\trac_off\r_\r_
\ifnum\INIT_=1000\r_
        \if#1b\if_fst\_fstfalse\else\a_\cur_x2em\r_\fi\r_
        \else\if#1<\_fstfalse\_height\r_
        \cur_x0pt\a_\cur_y-\d_ecc\r_\else\r_
        \def\move_x##1,##2:{\a_\cur_x##1\r_}\r_
        \def\move_y##1,##2:{\if##2<\_height\a_\cur_y-\d_ecc\r_\else\r_
                \a_\cur_y##2\r_\fi}\r_
        \move_x#1:\move_y#1:\_fstfalse\r_\fi\fi\r_
        \_place_t\r_
        \m_put(\n_\cur_x,\n_\cur_y){\useb_x\fs_tr}\move_after\r_
\else\r_
        \_place_t\r_
        \fs_dp\dp\fs_tr\fs_ht\ht\fs_tr\r_
        \ifnum\INIT_=0\r_
        \a_\fs_ht1ex\r_
        \edef\_struth{\the\fs_ht}\r_
        \def\_strut{\vrule height\_struth depth1ex width0pt}\r_
        \a_\fs_ht-1ex\r_
        \else\def\_strut{}\fi\r_
        \if#1t\a_\fs_ht-2ex\r_
        \else\if#1c\a_\fs_ht\fs_dp\d_\fs_ht2\r_
              \a_\fs_ht-\fs_dp\a_\fs_ht-1ex\r_
        \else\fs_ht0pt\fi\fi\r_
        \_lvm\lower\fs_ht\hbox{\_strut\b_x\fs_tr}\r_
\fi\r_
        \ifnum\INIT_=1000\r_\else\r_
        \a_\_tall-1\r_\a_\_ptall-1\r_
        \ifnum\_ptall=0\r_
        \bdeall_c{kladb_x}\r_
        \bdeall_c{tagb_x}\r_
        \deall_c{k_h}\r_
        \deall_c{k_d}\r_
        \deall_c{k_w}\r_
        \deall_c{k_o}\r_
        \deall_c{k_e}\r_
        \deall_c{exc_}\r_
        \deall_c{eexc_}\fi\r_
        \ifnum\_tall=0\r_
        \deall_c{t_sx}\deall_c{t_sy}\r_
        \deall_c{t_lne}\deall_c{t_lnf}\r_
        \deall_c{t_msx}\deall_c{t_msy}\r_
        \deall_c{t_mne}\deall_c{t_mnf}\r_
        \deall_c{t_dx}\deall_c{t_dy}\r_
        \deall_c{t_ex}\deall_c{t_ey}\r_
        \deall_c{t_fx}\deall_c{t_fy}\r_
        \deall_c{cur_x}\r_
        \deall_c{cur_y}\r_
        \deall_c{THI_}\fi\r_
        \ball_cfinal\all_cfinal\r_
        \egroup\r_
        \fi\r_
        \trac_on\is_}

%       USER INTERFACE: ENVIRONMENT for PROOF TREES

\def\in_bpf#1\epf{\_fout{bpf in BLIST}%
{bpf epf may not occur in this way in BLIST ELIST; it is only allowed!%
as/in labels of other nodes.!%
I skip everything till the next epf.!%
Possible arguments to epf will occur as garbage in the output.}\is_}

\def\ch_bpf#1#2{\def\_tmpa{#1}\def\_tmpb{#2}\r_
        \ifnum\INIT_=1000\let\_tmpr\_tmpa\else\let\_tmpr\_tmpb\fi\_tmpr}

\def\bpf{\ch_bpf{\in_bpf}{\trac_off\r_\linen_0\r_
        \_lvm\r_
        \bgroup\r_
        \let\n_mestack\_mpty\n_me0\r_
        \ball_cinit\all_cinit\r_
        \ifnum\_ptall>0\a_\_ptall1\r_\else\r_
        \ball_c{kladb_x}\r_
        \ball_c{tagb_x}\r_
        \all_c{k_h}\r_
        \all_c{k_d}\r_
        \all_c{k_w}\r_
        \all_c{k_o}\r_
        \all_c{k_e}\r_
        \all_c{exc_}\r_
        \all_c{eexc_}\r_
        \_ptall1\fi\r_
        \ifnum\_pall>0\a_\_pall1\r_\else\r_
        \all_c{ll_}\r_
        \all_c{chi_}\r_
        \all_c{thi__l}\r_
        \all_c{thi__r}\r_
        \all_c{max_tdp}\r_
        \all_c{tag_}\r_
        \all_c{tgo_}\tgo_.3em\r_
        \_pall1\fi\r_
        \ga_\INIT_1\r_
        \let\A\user_Ap\r_
        \let\U\user_Up\r_
        \let\B\user_Bp\r_
        \let\I\user_I\r_
        \checkn_me\n_me\r_
        \trac_on\is_}}

\def\epf{\t_p\cr_s\r_\ifnum\checkn_me=\cr_s\r_
        \let\_tmpa\good_epf\else\let\_tmpa\wrong_epf\fi\_tmpa}

\def\wrong_epf{\_fout{Node stack not empty}%
{The tree I have just typeset does not contain all nodes that you!%
specified. Probably you forgot some binary nodes somewhere.!%
This does not matter very much, proceed.}\good_epf}

\def\good_epf{\ga_\INIT_-1\_ncsp[{\x_epf}{\x_epf[b]}}
\def\x_epf[#1]{\trac_off\r_
        \_place_p:\cs_ N_M\r_m\n_me\es_:\r_
        \fs_dp\dp\fs_tr\fs_ht\ht\fs_tr\r_
        \ifnum\INIT_=0\r_
        \a_\fs_ht1ex\r_
        \edef\_struth{\the\fs_ht}\r_
        \def\_strut{\vrule height\_struth depth1ex width0pt}\r_
        \a_\fs_ht-1ex\r_
        \else\_depth\def\_strut{\vrule height0pt depth\d_dcc width0pt}\fi\r_
        \if#1t\a_\fs_ht-2ex\r_
        \else\if#1c\a_\fs_ht\fs_dp\d_\fs_ht2\r_
              \a_\fs_ht-\fs_dp\a_\fs_ht-1ex\r_
        \else\fs_ht0pt\fi\fi
        \_lvm\lower\fs_ht\hbox{\_strut\b_x\fs_tr}\r_
        \ifnum\INIT_=1000\else\r_
        \a_\_ptall-1\r_\a_\_pall-1\r_
        \ifnum\_ptall=0\r_
        \bdeall_c{kladb_x}\r_
        \bdeall_c{tagb_x}\r_
        \deall_c{k_h}\r_
        \deall_c{k_d}\r_
        \deall_c{k_w}\r_
        \deall_c{k_o}\r_
        \deall_c{k_e}\r_
        \deall_c{exc_}\r_
        \deall_c{eexc_}\fi\r_
        \ifnum\_pall=0\r_
        \deall_c{ll_}\r_
        \deall_c{chi_}\r_
        \deall_c{thi__l}\r_
        \deall_c{thi__r}\r_
        \deall_c{max_tdp}\r_
        \deall_c{tag_}\r_
        \deall_c{tgo_}\fi\r_
        \ball_cfinal\all_cfinal\r_
        \egroup\r_
        \fi\r_
        \trac_on\is_}

%       MACHINE INTERFACE: STARTING a NEW NODE (GENERAL)

\def\new_B{\p_p\pprevn_me{\cs_ N_M\r_m\n_me\es_}\prevn_me\n_me\inc_\n_me\r_
        \def\_self{\cs_ N_M\r_m\n_me\es_}\r_
        \def\_left{\cs_ N_M\r_m\pprevn_me\es_}\r_
        \def\_right{\cs_ N_M\r_m\prevn_me\es_}}

\def\new_U{\prevn_me\n_me\inc_\n_me\r_
        \def\_self{\cs_ N_M\r_m\n_me\es_}\r_
        \def\_above{\cs_ N_M\r_m\prevn_me\es_}}

\def\new_A{\p_sh\n_me\inc_\n_me\r_
        \def\_self{\cs_ N_M\r_m\n_me\es_}\r_}

%       MACHINE INTERFACE: PACKING THE LABEL INTO A BOX (GENERAL)

\newdimen\shrink\shrink.2em

\def\_nodebox#1{\r_
        \d_acc\shrink\r_
        \a_\k_h2\d_acc\a_\k_d\d_acc\a_\k_o\d_acc\r_
        \m_savebox\kladb_x(\n_\k_w,\n_\k_h){\r_
        \_bpic(\n_\k_w,\n_\k_h)(\n_\k_e,\n_\k_d)\r_
                \m_put(0,\n_\k_o){\b_x#1}\r_
        \_epic}}

\def\_emptybox#1{\r_
        \m_savebox\kladb_x(\n_\k_w,\n_\k_h){\r_
        \if#1t\_bpic(\n_\k_w,\n_\k_h)(\n_\k_e,\n_\k_d)\r_
         \else\_bpic(\n_\k_w,\n_\k_h)\r_\fi
                \m_put(\n_\k_e,\n_\k_o){}\r_
        \_epic}}

\def\_circlebox#1#2{\r_
        \m_savebox\kladb_x(\n_\k_w,\n_\k_h){\r_
        \if#2t\_bpic(\n_\k_w,\n_\k_h)(\n_\k_e,\n_\k_o)\r_
         \else\_bpic(\n_\k_w,\n_\k_h)\r_\fi
                \m_put(\n_\k_e,\n_\k_o){\circle#1{\n_\k_w}}\r_
        \_epic}}

% \_node#1#2#3--#4: #1 is type: A U B. #2 is position .$;,:^-!0*&
%       #3 is contents #4 is p (proof) or t (tree)
% output k_h = total height and depth
%        k_d = depth after positioning
%        k_o = depth before positioning
%        k_e = left offset after positioning
%        k_w = total width after positioning

\def\text_node#1--{\r_
        \setbox\kladb_x\hbox{#1}\r_
        \k_h\ht\kladb_x\r_
        \k_d\dp\kladb_x\r_
        \k_w\wd\kladb_x\r_
        \a_\k_h\k_d\r_
        \k_o\k_d\r_}

\def\_node#1#2#3--#4{\trac_off\r_
        \if#4t\position_t#1#2#3--\else\position_p#1#2#3--\fi}

\def\position_t#1#2#3--{\r_
        \if#2.\text_node#3--\k_e0pt\r_\_nodebox\kladb_x\r_\else 
        \if#2;\text_node#3--\k_e.5\k_w\r_\_nodebox\kladb_x\r_\else
        \if#2$\text_node$#3$--\k_e.5\k_w\r_\_nodebox\kladb_x\r_\else
        \if#2,\text_node#3--\k_e.5\k_w\r_\k_d0pt\_nodebox\kladb_x\r_\else
        \if#2:\text_node#3--\k_e.5\k_w\r_\k_d.5\k_h\_nodebox\kladb_x\r_\else
        \if#2^\text_node#3--\k_e.5\k_w\r_\k_d\k_h\_nodebox\kladb_x\r_\else
        \if#2-\k_w#3\r_\k_h\k_w\r_\k_e\k_w\d_\k_e2\r_\k_d\k_e\r_
                \k_o\k_d\r_
                \_emptybox t\else
        \if#2!\k_w#3\r_\k_e\k_w\d_\k_e2\r_\k_h0pt\k_d0pt\r_
                \k_o\k_e\r_
                \_emptybox t\else
        \if#20\k_w#3\r_\k_h\k_w\r_\k_e\k_w\d_\k_e2\r_\k_d\k_e\r_
                \k_o\k_e\r_
                \_circlebox{}t\else
        \if#2*\k_w#3\r_\k_e\k_w\d_\k_e2\r_\k_h0pt\k_d0pt\r_
                \k_o\k_e\r_
                \if#1A\k_h\k_e\fi\r_
                \_circlebox*t\else
        \if#2&\k_w#3\r_\k_e\k_w\d_\k_e2\r_\r_
                \k_o\k_e\r_
                \k_h\k_e\r_\k_d\k_h\r_
                \_circlebox*t\r_
        \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi}

% Closed circles are internally regarded as empty nodes. So the lines
% go into them. But the total height and depth are not quite correct.
% For big circles a problem. But: for axioms the height is adapted,
% and for the root you must specify not * but & .

\def\position_p#1#2#3--{\r_
        \if#2.\text_node#3--\k_e0pt\r_\_nodebox\kladb_x\r_\else 
        \if#2$\text_node$#3$--\k_e0pt\r_\_nodebox\kladb_x\r_\else       
        \if#2;\text_node#3--\k_e0pt\r_\_nodebox\kladb_x\r_\else 
        \if#2,\text_node#3--\k_e0pt\r_\k_d0pt\_nodebox\kladb_x\r_\else
        \if#2:\text_node#3--\k_e0pt\r_\k_d.5\k_h\_nodebox\kladb_x\r_\else
        \if#2^\text_node#3--\k_e0pt\r_\k_d\k_h\_nodebox\kladb_x\r_\else
        \if#2-\k_w#3\r_\k_h\k_w\r_\k_e\k_w\d_\k_e2\r_\k_d0pt\r_
                \k_o\k_e\r_
                \_emptybox p\else
        \if#2!\k_w#3\r_\k_h\k_w\r_\k_e\k_w\d_\k_e2\r_\k_d0pt\r_
                \k_o\k_e\r_
                \_emptybox p\else
        \if#20\k_w#3\r_\k_h\k_w\r_\k_e\k_w\d_\k_e2\r_\k_d0pt\r_
                \k_o\k_e\r_
                \_circlebox{}p\else
        \if#2*\k_w#3\r_\k_h\k_w\r_\k_e\k_w\d_\k_e2\r_\k_d0pt\r_
                \k_o\k_e\r_
                \_circlebox{*}p\else
        \if#2&\k_w#3\r_\k_h\k_w\r_\k_e\k_w\d_\k_e2\r_\k_d0pt\r_
                \k_o\k_e\r_
                \_circlebox{*}p\else
        \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi}

%       MACHINE INTERFACE: COMPUTE SCALE for PICTREES

% Index to \_index, scale to \d_ccc

\def\comp_rigid_U#1[#2]#3:#4--{\trac_off\r_     % #2 is a length
% LABEL
        \_node U#1#3--t\r_
% height plus depths plus 10.25pt
        \d_acc\cs_ tdp_#4\es_\r_\r_
        \a_\d_acc\k_h\a_\d_acc-\k_d\r_
        \a_\d_acc10.25pt\r_ % \d_acc is minimal height
        \d_ccc#2\r_
        \ifdim\d_ccc<\d_acc\d_ccc\d_acc\fi\r_
        \mn_tt<1>\ni_\t_sy\d_\d_ccc\cr_s\r_
        \trac_on\r_}

\def\comp_rigid_B#1[#2]#3:#4--#5--{\trac_off\r_% #2 is sep betw prems (length)
% LABEL
        \_node B#1#3--t\r_
% minimal forkwidth
        \d_dcc\cs_ tbr_#4\es_\a_\d_dcc-\cs_ lof_#4\es_\r_
        \a_\d_dcc\cs_ lof_#5\es_\r_
        \a_\d_dcc#2\r_ % \d_dcc is minimal fork wd
% height plus depths plus 10.25pt
        \d_acc\cs_ tdp_#4\es_\r_\d_bcc\cs_ tdp_#5\es_\r_
        \ifdim\d_acc<\d_bcc\d_acc\d_bcc\fi\r_
        \a_\d_acc\k_h\a_\d_acc-\k_d\r_
        \a_\d_acc10.25pt\r_ % \d_acc is minimal height
% t_acc is also minimal fork width
        \ifdim\d_dcc<\d_acc\d_dcc\d_acc\fi\r_
% determine first index
        \ifdim\d_dcc<48.4pt\def\_index{1}\else\r_
        \ifdim\d_dcc<74.0pt\def\_index{2}\else\r_
        \ifdim\d_dcc<116.6pt\def\_index{3}\else\r_
        \def\_index{4}\fi\fi\fi\r_
% compute scale 
        \b_tt<1>\_index\ni_\t_sx\a_\cr_s\cr_s\d_\d_dcc\cr_s\r_\d_ccc\d_dcc\r_
        \trac_on\r_}

%       MACHINE INTERFACE: COMPUTATION and TYPESET for PICTREES

% \def_cor helps to define the coordinate functions for the nodes

\def\def_cor#1#2#3#4{\ea_\edef\cs_#1\es_##1{\r_
                \nx_\cs_\nx_#2\nx_\es_\nx_##1\r_
                \nx_\a_\nx_\r_s#4 \the#3}\is_}

%       COMPUTATION and TYPESET DUMMY (GENERAL)

\def\_dum_tp{\r_
        \trac_off\r_
        \all_c{cbr_N_M}\r_
        \all_c{tbr_N_M}\r_
        \all_c{thi_N_M}\r_
        \all_c{tdp_N_M}\r_
        \all_c{lof_N_M}\r_
% TBR and THI and TDP and LOF
        \k_w1em\r_\k_e.5em\r_
        \cs_ tbr_N_M\es_\k_w\r_
        \cs_ cbr_N_M\es_\k_w\r_
        \cs_ lof_N_M\es_\k_e\r_
        \k_h2ex\r_\k_d.5ex\r_\cs_ thi_N_M\es_1.5ex\r_
        \cs_ tdp_N_M\es_\k_d\r_
% TYPESET
        \ball_c{b_xN_M}\r_
\ea_\m_savebox\cs_ b_xN_M\es_(\n_\k_w,\n_\k_h)%
{\_bpic(\n_\k_w,\n_\k_h)(\n_\k_e,\n_\k_d)\r_
        \m_put(\n_\k_e,\n_\k_d){\m_makebox(0,0){?}}\r_
\_epic}\r_
        \trac_on\is_}

%       COMPUTATION and TYPESET BINARY (PICTREES)

\def\_btree#1<#2>#3--#4--#5--{\r_  % #2 is scalingratio
        \edef\_index{\f_th#1.}\r_
        \edef\form_l{\s_th#1.}\r_
        \edef\form_r{\t_th#1.}\r_
        \trac_off\r_
        \all_c{tbr_#3}\r_
        \all_c{thi_#3}\r_
        \all_c{tdp_#3}\r_
        \all_c{lof_#3}\r_
        \b_tt<#2>\_index\r_
% COORDINATE FUNCTIONS
        \def_cor{xc_r#4}{xc_r#3}{\t_sx}{-}\r_
        \def_cor{yc_r#4}{yc_r#3}{\t_sy}{}\r_
        \def_cor{xc_r#5}{xc_r#3}{\t_sx}{}\r_
        \def_cor{yc_r#5}{yc_r#3}{\t_sy}{}\r_
% EXCES
        \d_acc\cs_ lof_#5\es_\a_\d_acc-\t_sx\r_
        \d_bcc\cs_ lof_#4\es_\a_\d_bcc\t_sx\r_
        \ifdim\d_acc>\d_bcc\exc_\d_acc\a_\exc_-\d_bcc\r_
        \else\exc_0pt\fi
        \d_acc\cs_ tbr_#4\es_\a_\d_acc-\t_sx\r_
        \a_\d_acc-\cs_ lof_#4\es_\r_
        \d_bcc\cs_ tbr_#5\es_\a_\d_bcc\t_sx\r_
        \a_\d_bcc-\cs_ lof_#5\es_\r_
        \ifdim\d_acc>\d_bcc\eexc_\d_acc\a_\eexc_-\d_bcc\r_
        \else\eexc_0pt\fi
% TBR without label
   \d_acc\cs_ lof_#4\es_\a_\d_acc\cs_ tbr_#5\es_\a_\d_acc-\cs_ lof_#5\es_\r_
        \a_\d_acc2\t_sx\a_\d_acc\exc_\a_\d_acc\eexc_\r_
        \cs_ tbr_#3\es_\d_acc\r_
% LOF without label
        \d_acc\cs_ lof_#4\es_\a_\d_acc\t_sx\a_\d_acc\exc_\r_
        \cs_ lof_#3\es_\d_acc\r_
% TBR and LOF with label
        \d_acc\cs_ lof_#3\es_\r_
        \ifdim\d_acc<\k_e\exc_\k_e\a_\exc_-\d_acc\a_\cs_ tbr_#3\es_\exc_\r_
                \cs_ lof_#3\es_\k_e\fi
        \d_acc\cs_ tbr_#3\es_\r_
        \ifdim\d_acc<\k_w\exc_\k_w\a_\exc_-\d_acc\a_\cs_ tbr_#3\es_\exc_\fi
% THI 
        \d_acc\cs_ thi_#4\es_\d_bcc\cs_ thi_#5\es_\r_
        \ifdim\d_acc>\d_bcc\d_dcc\d_acc\else\d_dcc\d_bcc\fi
        \a_\d_dcc\t_sy\r_
        \d_ecc\k_h\a_\d_ecc-\k_d\r_
        \ifdim\d_dcc<\d_ecc\d_dcc\d_ecc\fi
        \cs_ thi_#3\es_\d_dcc\r_
% TDP 
        \d_acc\cs_ tdp_#4\es_\d_bcc\cs_ tdp_#5\es_\r_
        \a_\d_acc-\t_sy\a_\d_bcc-\t_sy\r_
        \ifdim\d_acc>\k_d\r_
                \ifdim\d_bcc>\k_d\r_
                        \ifdim\d_acc>\d_bcc\d_dcc\d_acc\r_
                        \else\d_dcc\d_bcc\fi
                \else\d_dcc\d_acc\fi
        \else\ifdim\d_bcc>\k_d\d_dcc\d_bcc\r_
                \else\d_dcc\k_d\fi\fi
        \cs_ tdp_#3\es_\d_dcc\r_
% TYPESET
        \ball_c{b_x#3}\r_
        \d_acc\cs_ tbr_#3\es_\d_bcc\cs_ thi_#3\es_\a_\d_bcc\cs_ tdp_#3\es_\r_
        \exc_\cs_ lof_#3\es_\eexc_\cs_ tdp_#3\es_\r_
        \a_\k_h-\k_d\r_
        \k_e\cs_ tdp_#4\es_\r_
        \k_w\cs_ tdp_#5\es_\r_
\ea_\m_savebox\cs_ b_x#3\es_(\n_\d_acc,\n_\d_bcc)%
{\_bpic(\n_\d_acc,\n_\d_bcc)(\n_\exc_,\n_\eexc_)\r_
        \s_tt<#2>\_index\form_l{\form_r} D{\n_\k_h} E{\n_\k_e} F{\n_\k_w}:\r_
        \m_put(\n_\exc_,\n_\eexc_){\f_rk\form_l\form_r}\r_
        \m_put(\n_\exc_,\n_\eexc_){\useb_x\kladb_x}\r_
        \d_acc\exc_\a_\exc_-\t_sx\a_\eexc_\t_sy\r_
        \m_put(\n_\exc_,\n_\eexc_){\ea_\useb_x\cs_ b_x#4\es_}\r_
        \a_\d_acc\t_sx\r_
        \m_put(\n_\d_acc,\n_\eexc_){\ea_\useb_x\cs_ b_x#5\es_}\r_
\_epic}\r_
        \if_u{sav_\cs_#4\es_}\r_
        \deall_c{thi_#4}\r_
        \deall_c{tbr_#4}\r_
        \deall_c{tdp_#4}\r_
        \deall_c{lof_#4}\r_
        \bdeall_c{b_x#4}\fi\r_
        \if_u{sav_\cs_#5\es_}\r_
        \deall_c{thi_#5}\r_
        \deall_c{tbr_#5}\r_
        \deall_c{tdp_#5}\r_
        \deall_c{lof_#5}\r_
        \bdeall_c{b_x#5}\fi\r_
        \trac_on\is_}

%       COMPUTATION and TYPESET UNARY (PICTREES)

\def\_utree#1<#2>#3--#4--{\r_   % #2 is the scaling ratio
        \trac_off\r_
        \all_c{tbr_#3}\r_
        \all_c{thi_#3}\r_
        \all_c{tdp_#3}\r_
        \all_c{lof_#3}\r_
        \mn_tt<#2>\r_
% COORDINATE FUNCTIONS
        \def_cor{xc_r#4}{xc_r#3}{\t_sx}{}\r_
        \def_cor{yc_r#4}{yc_r#3}{\t_sy}{}\r_
% TBR without label
        \cs_ tbr_#3\es_\cs_ tbr_#4\es_\r_
% LOF without label
        \d_acc\cs_ lof_#4\es_\a_\d_acc\t_sx\a_\d_acc\exc_\r_
        \cs_ lof_#3\es_\cs_ lof_#4\es_\r_
% TBR and LOF with label
        \d_acc\cs_ lof_#3\es_\r_
        \ifdim\d_acc<\k_e\exc_\k_e\a_\exc_-\d_acc\a_\cs_ tbr_#3\es_\exc_\r_
                \cs_ lof_#3\es_\k_e\fi
        \d_acc\cs_ tbr_#3\es_\r_
        \ifdim\d_acc<\k_w\exc_\k_w\a_\exc_-\d_acc\a_\cs_ tbr_#3\es_\exc_\r_\fi
% THI 
        \d_acc\cs_ thi_#4\es_\r_
        \a_\d_acc\t_sy\r_
        \d_ecc\k_h\a_\d_ecc-\k_d\r_
        \ifdim\d_acc<\d_ecc\d_acc\d_ecc\fi
        \cs_ thi_#3\es_\d_acc\r_
% TDP 
        \d_acc\cs_ tdp_#4\es_\r_
        \a_\d_acc-\t_sy\r_
        \ifdim\d_acc>\k_d\else\d_acc\k_d\fi
        \cs_ tdp_#3\es_\d_acc\r_
% TYPESET
        \ball_c{b_x#3}\r_
        \d_acc\cs_ tbr_#3\es_\d_bcc\cs_ thi_#3\es_\a_\d_bcc\cs_ tdp_#3\es_\r_
        \exc_\cs_ lof_#3\es_\eexc_\cs_ tdp_#3\es_\r_
        \a_\k_h-\k_d\r_
        \k_e\cs_ tdp_#4\es_\r_
\ea_\m_savebox\cs_ b_x#3\es_(\n_\d_acc,\n_\d_bcc)%
{\_bpic(\n_\d_acc,\n_\d_bcc)(\n_\exc_,\n_\eexc_)\r_
        \s_tt<#2>1#1 D{\n_\k_h} E{\n_\k_e} F0:\r_
        \m_put(\n_\exc_,\n_\eexc_){\m_rk#1}\r_
        \m_put(\n_\exc_,\n_\eexc_){\useb_x\kladb_x}\r_
        \a_\exc_\t_sx\a_\eexc_\t_sy\r_
        \m_put(\n_\exc_,\n_\eexc_){\ea_\useb_x\cs_ b_x#4\es_}\r_
\_epic}\r_
        \if_u{sav_\cs_#4\es_}\r_
        \deall_c{thi_#4}\r_
        \deall_c{tbr_#4}\r_
        \deall_c{tdp_#4}\r_
        \deall_c{lof_#4}\r_
        \bdeall_c{b_x#4}\fi\r_
        \trac_on\is_}

%       COMPUTATION and TYPESET AXIOMS (PICTREES)

\def\_dum{\r_
        \trac_off\r_
        \all_c{tbr_N_M}\r_
        \all_c{thi_N_M}\r_
        \all_c{tdp_N_M}\r_
        \all_c{lof_N_M}\r_
% TBR and THI and TDP and LOF
        \k_w1em\r_\k_e.5em\r_\cs_ tbr_N_M\es_\k_w\r_
        \cs_ lof_N_M\es_\k_e\r_
        \k_h2ex\r_\k_d.5ex\r_\cs_ thi_N_M\es_1.5ex\r_
        \cs_ tdp_N_M\es_\k_d\r_
% TYPESET
        \ball_c{b_xN_M}\r_
\ea_\m_savebox\cs_ b_xN_M\es_(\n_\k_w,\n_\k_h)%
{\_bpic(\n_\k_w,\n_\k_h)(\n_\k_e,\n_\k_d)\r_
        \m_put(\n_\k_e,\n_\k_d){\m_makebox(0,0){?}}\r_
\_epic}\r_
        \trac_on\is_}

\def\_axtree#1--{\r_
        \trac_off\r_
        \all_c{tbr_#1}\r_
        \all_c{thi_#1}\r_
        \all_c{tdp_#1}\r_
        \all_c{lof_#1}\r_
% TBR and THI and TDP and LOF
        \cs_ tbr_#1\es_\k_w\r_
        \cs_ thi_#1\es_\k_h\a_\cs_ thi_#1\es_-\k_d\r_
        \cs_ tdp_#1\es_\k_d\r_
        \cs_ lof_#1\es_\k_e\r_
% TYPESET
        \ball_c{b_x#1}\r_
\ea_\m_savebox\cs_ b_x#1\es_(\n_\k_w,\n_\k_h)%
{\_bpic(\n_\k_w,\n_\k_h)(\n_\k_e,\n_\k_d)\r_
        \m_put(\n_\k_e,\n_\k_d){\useb_x\kladb_x}\r_
\_epic}\r_
        \trac_on\is_}

%       COMPUTATION and TYPESET BINARY (PROOF TREES)

\def\_bproof[#1]#2 #3 ---(#4) ---#5--#6--#7:#8{\r_
        \ea_\def\cs_ sav_#5\es_{n}\r_
        \trac_off\r_
        \all_c{cbr_#5}\r_
        \all_c{tdp_#5}\r_
        \all_c{tbr_#5}\r_
        \all_c{thi_#5}\r_
        \all_c{lof_#5}\r_
        \trac_on\r_
        \ea_\let\cs_ blw_#5\es_\r_
% CBR CDP TAG and a preliminary CHI
        \_node B#2#3--p\r_
        \cs_ cbr_#5\es_\k_w\r_
        \cs_ tdp_#5\es_\k_d\r_
        \chi_\k_h\a_\chi_-\k_d\r_
        \setbox\tagb_x\hbox{#4}\r_
        \tag_\wd\tagb_x\r_
        \ifdim\tag_=0pt\else\a_\tag_\tgo_\fi
% TBR preliminary
        \cs_ tbr_#5\es_\ea_\the\cs_ tbr_#6\es_\r_
        \a_\cs_ tbr_#5\es_\ea_\the\cs_ tbr_#7\es_\r_
        \a_\cs_ tbr_#5\es_#1\r_
% LL preliminary
        \ll_\ea_\the\cs_ tbr_#6\es_\r_
        \a_\ll_-\ea_\the\cs_ lof_#6\es_\r_
        \a_\ll_#1\r_
        \a_\ll_\ea_\the\cs_ lof_#7\es_\r_
        \a_\ll_\ea_\the\cs_ cbr_#7\es_\r_
% if the conclusion is wider than the two premises
    \ifdim\cs_ tbr_#5\es_<\cs_ cbr_#5\es_\r_
%       EXC
        \exc_\cs_ cbr_#5\es_\r_
        \a_\exc_-\ea_\the\cs_ tbr_#5\es_\r_
%       TBR definitief
        \cs_ tbr_#5\es_\cs_ cbr_#5\es_\r_
        \a_\cs_ tbr_#5\es_\the\tag_\r_
%       LL nog steeds preliminary
        \a_\ll_\ea_\the\exc_\r_
%       LOF = 0
        \cs_ lof_#5\es_0pt\r_
%       BLW = true
        \ea_\def\cs_ blw_#5\es_{TRUE}\r_
% otherwise the conclusion fits below the premises
    \else\exc_0pt\r_
%       LOF
        \d_acc\ll_\d_\d_acc2\r_
        \cs_ lof_#5\es_\the\d_acc\r_
        \a_\cs_ lof_#5\es_\ea_\the\cs_ lof_#6\es_\r_
        \d_acc-\cs_ cbr_#5\es_\d_\d_acc2\r_
        \a_\cs_ lof_#5\es_\the\d_acc\r_
    \fi
% if the conclusion is wider than the preliminary line
% LL definitive, BLW true
    \ifdim\ll_<\cs_ cbr_#5\es_\ll_\cs_ cbr_#5\es_\r_
        \ea_\def\cs_ blw_#5\es_{TRUE}\fi
% TBR definitive
        \if_u{blw_#5}\d_bcc\cs_ lof_#6\es_\else\d_bcc\cs_ lof_#5\es_\fi
        \a_\d_bcc\the\ll_\r_
        \a_\d_bcc\the\tag_\r_
        \ifdim\d_bcc>\cs_ tbr_#5\es_\cs_ tbr_#5\es_\d_bcc\fi
% CHI almost definitive
        \a_\chi_1ex\r_
% THI
    \ifdim\cs_ tdp_#6\es_>\cs_ tdp_#7\es_\max_tdp\cs_ tdp_#6\es_\r_
        \thi__l0pt\thi__r\cs_ tdp_#6\es_\a_\thi__r-\ea_\the\cs_ tdp_#7\es_\r_
    \else\max_tdp\cs_ tdp_#7\es_\r_
        \thi__r0pt\thi__l\cs_ tdp_#7\es_\a_\thi__l-\ea_\the\cs_ tdp_#6\es_\r_
    \fi
    \a_\thi__l\ea_\the\cs_ thi_#6\es_\r_
    \a_\thi__r\ea_\the\cs_ thi_#7\es_\r_
    \ifdim\thi__l>\thi__r\d_acc\thi__l\else
                \d_acc\thi__r\fi
        \cs_ thi_#5\es_\d_acc\r_
        \a_\cs_ thi_#5\es_\the\chi_\r_
        \a_\cs_ thi_#5\es_\ea_\the\cs_ tdp_#5\es_\r_
% TYPESET
%
        \trac_off\r_
\ball_c{b_x#5}\r_
\ea_\m_savebox\cs_ b_x#5\es_(\n_\cs_ tbr_#5\es_,\n_\cs_ thi_#5\es_)%
{\_bpic(\n_\cs_ tbr_#5\es_,\n_\cs_ thi_#5\es_)\r_
                \linethickness{.4pt}\r_
                \d_bcc\the\chi_\r_
                \a_\d_bcc\the\max_tdp\r_
        \m_put(0,\n_\d_bcc){\ea_\useb_x\cs_ b_x#6\es_}\r_
                \d_acc\ea_\the\cs_ tbr_#6\es_\r_
                \a_\d_acc#1\r_
                \a_\d_acc\ea_\the\exc_\r_
        \m_put(\n_\d_acc,\n_\d_bcc){\ea_\useb_x\cs_ b_x#7\es_}\r_
                \d_acc\the\chi_\r_
                \a_\d_acc-.5ex\r_
           \if_u{blw_#5}\d_bcc\cs_ lof_#6\es_\else\d_bcc\cs_ lof_#5\es_\fi
                \l_ne#8\r_
                \a_\d_bcc\the\ll_\r_
                \a_\d_bcc.3em\r_
                \a_\d_acc-.5ex\r_
        \m_put(\n_\d_bcc,\n_\d_acc){\useb_x\tagb_x}\r_
        \m_put(\n_\cs_ lof_#5\es_,0){\useb_x\kladb_x}\r_
\_epic}\r_
        \if_u{sav_\cs_#6\es_}\r_
        \deall_c{cbr_#6}\r_
        \deall_c{tdp_#6}\r_
        \deall_c{tbr_#6}\r_
        \deall_c{thi_#6}\r_
        \deall_c{lof_#6}\r_
        \bdeall_c{b_x#6}\r_
        \dinc_{#6}\r_
        \fi\r_
        \if_u{sav_\cs_#7\es_}\r_
        \deall_c{cbr_#7}\r_
        \deall_c{tdp_#7}\r_
        \deall_c{tbr_#7}\r_
        \deall_c{thi_#7}\r_
        \deall_c{lof_#7}\r_
        \bdeall_c{b_x#7}\r_
        \dinc_{#7}\fi\r_
        \trac_on\is_}

%       COMPUTATION and TYPESET UNARY (PROOF TREES)

\def\_uproof#1 #2 ---(#3) ---#4--#5:#6{\r_
        \ea_\def\cs_ sav_#4\es_{n}\r_
        \trac_off\r_
        \all_c{cbr_#4}\r_
        \all_c{tdp_#4}\r_
        \all_c{tbr_#4}\r_
        \all_c{thi_#4}\r_
        \all_c{lof_#4}\r_
        \trac_on\r_
        \ea_\let\cs_ blw_#4\es_\r_
% CBR CDP and preliminary CHI
        \_node U#1#2--p\r_
        \cs_ cbr_#4\es_\k_w\r_
        \cs_ tdp_#4\es_\k_d\r_
        \chi_\k_h\a_\chi_-\k_d\r_
        \setbox\tagb_x\hbox{#3}\r_
        \tag_\wd\tagb_x\r_
        \ifdim\tag_=0pt\else\a_\tag_\tgo_\fi
% TBR preliminary
        \cs_ tbr_#4\es_\ea_\the\cs_ tbr_#5\es_\r_
% if the conclusion is wider than the premiss
    \ifdim\cs_ tbr_#4\es_<\cs_ cbr_#4\es_\r_
%       EXC
        \exc_\cs_ cbr_#4\es_\r_
        \a_\exc_-\ea_\the\cs_ tbr_#4\es_\r_\d_\exc_2\r_
%       TBR definitief, BLW true
        \cs_ tbr_#4\es_\cs_ cbr_#4\es_\r_
        \ea_\def\cs_ blw_#4\es_{TRUE}\else\exc_0pt\fi
% LL preliminary
        \ll_\ea_\the\cs_ cbr_#5\es_\r_
% LOF
        \d_acc\ll_\d_\d_acc2\r_
        \cs_ lof_#4\es_\the\d_acc\r_
        \a_\cs_ lof_#4\es_\ea_\the\cs_ lof_#5\es_\r_
        \d_acc-\cs_ cbr_#4\es_\d_\d_acc2\r_
        \a_\cs_ lof_#4\es_\the\d_acc\r_
% if LOF negative, then becomes 0, BLW true
    \ifdim\cs_ lof_#4\es_<0pt\cs_ lof_#4\es_0pt\r_
        \ea_\def\cs_ blw_#4\es_{TRUE}\fi
% if LL less than conclusion width, then becomes equal, BLW true
    \ifdim\ll_<\cs_ cbr_#4\es_\ll_\cs_ cbr_#4\es_\r_
        \ea_\def\cs_ blw_#4\es_{TRUE}\fi
% TBR definitive
        \if_u{blw_#4}\d_bcc\cs_ lof_#5\es_\else\d_bcc\cs_ lof_#4\es_\fi
        \a_\d_bcc\the\ll_\r_
        \a_\d_bcc\the\tag_\r_
        \ifdim\d_bcc>\cs_ tbr_#4\es_\r_\cs_ tbr_#4\es_\d_bcc\fi
% CHI almost definitive
        \a_\chi_1ex\r_
% THI
        \cs_ thi_#4\es_\cs_ thi_#5\es_\r_
        \a_\cs_ thi_#4\es_\ea_\the\cs_ tdp_#4\es_\r_
        \a_\cs_ thi_#4\es_\the\chi_\r_
% TYPESET
%
        \trac_off\r_
\ball_c{b_x#4}\r_
\ea_\m_savebox\cs_ b_x#4\es_(\n_\cs_ tbr_#4\es_,\n_\cs_ thi_#4\es_)%
{\_bpic(\n_\cs_ tbr_#4\es_,\n_\cs_ thi_#4\es_)\r_
                \linethickness{.4pt}\r_
                \d_acc\the\chi_\r_
                \a_\d_acc\ea_\the\cs_ tdp_#5\es_\r_
        \m_put(\n_\exc_,\n_\d_acc){\ea_\useb_x\cs_ b_x#5\es_}\r_
                \d_acc\the\chi_\r_
                \a_\d_acc-.5ex\r_
           \if_u{blw_#4}\d_bcc\cs_ lof_#5\es_\else\d_bcc\cs_ lof_#4\es_\fi
                \l_ne#6\r_
                \a_\d_bcc\the\ll_\r_
                \a_\d_bcc.3em\r_
                \a_\d_acc-.5ex\r_
        \m_put(\n_\d_bcc,\n_\d_acc){\useb_x\tagb_x}\r_
        \m_put(\n_\cs_ lof_#4\es_,0){\useb_x\kladb_x}\r_
\_epic}\r_
        \if_u{sav_\cs_#5\es_}\r_
        \deall_c{cbr_#5}\r_
        \deall_c{tdp_#5}\r_
        \deall_c{tbr_#5}\r_
        \deall_c{thi_#5}\r_
        \deall_c{lof_#5}\r_
        \dinc_{#5}\r_
        \bdeall_c{b_x#5}\fi\r_
        \trac_on\is_}

%       COMPUTATION and TYPESET AXIOMS (PROOF TREES)

\def\_axproof#1 #2 ---#3:{\r_
        \ea_\def\cs_ sav_#3\es_{n}\r_
        \trac_off\r_
        \all_c{cbr_#3}\r_
        \all_c{tdp_#3}\r_
        \all_c{tbr_#3}\r_
        \all_c{thi_#3}\r_
        \all_c{lof_#3}\r_
        \trac_on\r_
        \ea_\let\cs_ blw_#3\es_\r_
% CDP CBR CHI
        \_node A#1#2--p\r_
        \cs_ cbr_#3\es_\k_w\r_
        \cs_ tdp_#3\es_\k_d\r_
        \chi_\k_h\a_\chi_-\k_d\r_
        \a_\chi_1ex\r_
% THI
        \cs_ thi_#3\es_\chi_\r_
        \a_\cs_ thi_#3\es_\ea_\the\cs_ tdp_#3\es_\r_
% TBR
        \cs_ tbr_#3\es_\ea_\the\cs_ cbr_#3\es_\r_
% LOF
        \cs_ lof_#3\es_0pt\r_
% TYPESET
%
        \trac_off\r_
\ball_c{b_x#3}\r_
\ea_\m_savebox\cs_ b_x#3\es_(\n_\cs_ tbr_#3\es_,\n_\cs_ thi_#3\es_)%
{\_bpic(\n_\cs_ tbr_#3\es_,\n_\cs_ thi_#3\es_)\r_
                \linethickness{.4pt}\r_
                \m_put(0,0){\useb_x\kladb_x}\r_
\_epic}\r_
        \trac_on\r_
        \is_}

%       COMPUTATION and TYPESET: PLACING TREES

\def\_newsize{\r_
% X-EXCES
        \exc_\cur_x\a_\exc_\d_acc\a_\exc_-\TBR_\a_\exc_\LOF_\r_
        \ifdim\exc_<0pt\exc_0pt\fi\r_
        \eexc_-\cur_x\a_\eexc_-\LOF_\r_
        \ifdim\eexc_<0pt\eexc_0pt\fi\r_
% TBR and LOF
        \a_\TBR_\exc_\a_\TBR_\eexc_\r_
        \a_\LOF_\eexc_\r_
% Y-EXCES
        \exc_\cur_y\a_\exc_\d_ecc\a_\exc_-\THI_\r_
        \ifdim\exc_<0pt\exc_0pt\fi\r_
        \eexc_-\cur_y\a_\eexc_-\TDP_\r_
        \ifdim\eexc_<0pt\eexc_0pt\fi\r_
% THI and TDP
        \a_\THI_\exc_\r_
        \a_\TDP_\eexc_\r_}

\def\_root#1--{\r_
        \d_acc\cs_ tbr_#1\es_\r_
        \d_bcc\cs_ thi_#1\es_\r_
        \d_ccc\cs_ lof_#1\es_\r_
        \d_dcc\cs_ tdp_#1\es_\r_
        \d_ecc\d_bcc\r_\a_\d_ecc\d_dcc\r_
   \ea_\edef\cs_ xc_r#1\es_##1{\nx_\r_s\the\d_ccc\nx_\a_\nx_\r_s\the\cur_x}\r_
   \ea_\edef\cs_ yc_r#1\es_##1{\nx_\r_s\the\d_dcc\nx_\a_\nx_\r_s\the\cur_y}\r_
        \is_}

\def\_tree#1--{\r_
        \_root#1--\r_
        \m_savebox\fs_tr{\_bpic(\n_\d_acc,\n_\d_ecc)\r_
                \m_put(\n_\d_ccc,\n_\d_dcc){\ea_\useb_x\cs_ b_x#1\es_}\r_
        \_epic}\r_
        \ifnum\INIT_=1000\r_\_newsize\r_
        \xdef\move_after{\nx_\a_\nx_\cur_x\the\d_acc\nx_\r_}\fi\is_}

\def\_place_t{\_tree\cs_ N_M\r_m\n_me\es_--}

\def\_place_p:#1:{\setbox\fs_tr\hbox{\ea_\b_x\cs_ b_x#1\es_}\is_}

\def\_height{\d_bcc\cs_ thi_\cs_ N_M\r_m\n_me\es_\es_\r_
        \d_dcc\cs_ tdp_\cs_ N_M\r_m\n_me\es_\es_\r_
        \d_ecc\d_bcc\r_\a_\d_ecc\d_dcc\r_}

\def\_depth{\d_dcc\cs_ tdp_\cs_ N_M\r_m\n_me\es_\es_}

%       COMPUTATION and TYPESET: CONNECTIONS 

\newcount\dir_AB

\def\_connect:#1^#2 with #3^#4 at #5^#6:{\r_
        \trac_off\r_
\all_c{A_x}\all_c{A_y}\r_
\all_c{B_x}\all_c{B_y}\r_
\all_c{A_line}\all_c{B_line}\r_
\all_c{Between_line}\all_c{H_ight}\r_
        \cs_ xc_r#1\es_\z@\r_\A_x\r_s\r_\cs_ yc_r#1\es_\z@\A_y\r_s\r_
        \cs_ xc_r#3\es_\z@\r_\B_x\r_s\r_\cs_ yc_r#3\es_\z@\B_y\r_s\r_
        \a_\A_y#2pt\r_
        \a_\B_y#4pt\r_
        \ifdim\A_x>\B_x\r_
                \def\Re_y{\A_y}\def\Li_y{\B_y}\r_
           \else\def\Re_y{\B_y}\def\Li_y{\A_y}\r_
        \fi\r_
        \ifdim\A_y>\B_y\r_
                \def\Max_y{\A_y}\def\Min_y{\B_y}\r_
           \else\def\Max_y{\B_y}\def\Min_y{\A_y}\r_
        \fi\r_
        \ea_\ifdim\A_x<\B_x\dir_AB1\else\dir_AB-1\fi
\if#6A\H_ight=#5pt\a_\H_ight\cur_y\r_\else
\if#6a\H_ight=\A_y\a_\H_ight#5pt\r_\else
\if#6b\H_ight=\B_y\a_\H_ight#5pt\r_\else
\if#6x\H_ight=\Max_y\a_\H_ight#5pt\r_\else
\if#6y\H_ight=\Min_y\a_\H_ight#5pt\r_\else
\if#6l\H_ight=\Li_y\a_\H_ight#5pt\r_\else
\if#6r\H_ight=\Re_y\a_\H_ight#5pt\r_\fi\fi\fi\fi\fi\fi\fi\r_
\ifdim\H_ight>\THI_\r_\g_\THI_\H_ight\fi\r_
\ifnum\INIT_=1000\r_\else\g_\cs_ thi_\cs_ N_M\r_m\n_me\es_\es_\THI_\fi\r_
        \ifdim\A_y>\H_ight\r_
\_fout{Impossible connection}%
{You want to connect _#1_ with _#3_.!%
Your height specification leads to \n_\H_ight,!%
wich is below or in node #1. I mark this in the output.  Proceed.}\r_
        \_put(\n_\A_x,\n_\A_y){\#}\r_
                \def\d_sh{TRUE}\r_
   \else\A_line\H_ight\a_\A_line-\A_y\r_
                \_put(\n_\A_x,\n_\A_y){\line(0,1){\n_\A_line}}\r_\fi
        \ifdim\B_y>\H_ight\r_
\_fout{Impossible connection}%
{You want to connect _#1_ with _#3_.!%
Your height specification leads to \n_\H_ight,!%
wich is below or in node #3. I mark this in the output.  Proceed.}\r_
        \_put(\n_\B_x,\n_\B_y){\#}\r_
                \def\d_sh{TRUE}\r_
   \else\B_line\H_ight\a_\B_line-\B_y\r_
                \_put(\n_\B_x,\n_\B_y){\line(0,1){\n_\B_line}}\r_\fi
        \Between_line\B_x\a_\Between_line-\A_x\r_
        \m_\Between_line\dir_AB\r_
 \if_u{d_sh}\_put(\n_\A_x,\n_\H_ight){\line(\dir_AB,0){\n_\Between_line}}\r_
       \else\d_\Between_line2\ea_\gt_m\the\Between_line\r_
            \_multiput(\n_\A_x,\n_\H_ight)(2,0){\cr_s}{\c_t}\fi\r_
\deall_c{A_x}\deall_c{A_y}\r_
\deall_c{B_x}\deall_c{B_y}\r_
\deall_c{A_line}\deall_c{B_line}\r_
\deall_c{Between_line}\deall_c{H_ight}\r_
        \trac_on\r_}


%       BASICS: COMPACT FORMAT

\newcount\n_me
\newcount\checkn_me
\newcount\prevn_me
\newcount\pprevn_me

\def\N_M{N_M}

\def\p_sh#1{\ifnum#1>0\r_\ea_\lap_it\the#1\to\n_mestack\fi}

\def\p_p#1#2{\ifx\n_mestack\_mpty\r_
\_fout{Missing child above #2}%
{Binary node _#2_ misses a child. I put in a dummy somewhere,!%
The output may look weird. Proceed.}\r_
             \_dum_tp\r_#10\r_
             \else\lop_it\n_mestack\to\tmp_rary#1\tmp_rary\fi}

\def\t_p#1{\ifx\n_mestack\_mpty\r_#10\r_
             \else\top_it\n_mestack\to\tmp_rary#1\tmp_rary\fi}

\newif\ifgu_rd

\def\inc_#1{#1=1\loop\if_u{us_dN_M\r_m#1}\r_
        \ea_\edef\cs_ N_M\r_m#1\es_{N_M\r_m#1}\r_
        \ea_\def\cs_ us_d\cs_ N_M\r_m#1\es_\es_{USED}\gu_rdfalse\r_
        \else\a_#11\gu_rdtrue\r_
        \fi\ifgu_rd\repeat}

\def\dinc_#1{\ea_\let\cs_ us_d#1\es_\r_}

%       BASICS: LISTS
%
% see TeX book pag 378
%
%       \_mpty          : empty list
%       \lap_it#1\to#2  : adds element #1 to list #2
%       \lop_it#1\to#2  : removes element from #1 and put it into #2
%       \top_it#1\to#2  : first element of #1 is put into #2
%
\toksdef\t_a0\toksdef\t_b2

\def\_mpty{\r_}

\def\lap_it#1\to#2{\t_a{\.{#1}}\t_b\ea_{#2}\edef#2{\the\t_a\the\t_b}}

\def\lop_it#1\to#2{\ea_\lop_ff#1\lop_ff#1#2}
\def\lop_ff\.#1#2\lop_ff#3#4{\def#4{#1}\def#3{#2}}

\def\top_it#1\to#2{\ea_\top_ff#1\top_ff#1#2}
\def\top_ff\.#1#2\top_ff#3#4{\def#4{#1}\def#3{#1#2}}

%       BASICS: DIMEN BOX ALLOCATION

% Memory management. Free space from dimen_min (\count11) 
% and box_min (\count14) to \insc@unt. If there is no more room, a TeX
% error message is invoked.
% For every cell i there is a flag full_i.
% Allocation: a cel is assigned to a name, the cel number comes in \alno_name.
% This enables deallocation.

% A new cel is found as follows. \all_cno is a pointer to cells. First its
% value is stored. Then it is cyclically stepped until a free cel is found,
% or the start position is encountered. The latter case means overflow. 

% Another solution is: take the first free cel from dimen-min. But this involves
% much lengthier iteratations.

% Undefined control sequences are equal to \relax. It is important that
% different allocation sessions are separated by grouping.

%       BASICS: DIMEN ALLOCATION

\newcount\dimen_cmin
\newcount\dimen_cmax
\newcount\dimen_clast

\newcount\all_cno

\let\f_ll\noexpand      % the value "full"; "empty" is \relax

\def\all_cinit{\r_ 
        \dimen_cmin\count11\a_\dimen_cmin3\r_
        \dimen_cmax\insc@unt\a_\dimen_cmax-2\r_
        \ifnum\tr_a>0\r_
        \wlog{page \thepage: dimens allocatable from \the\dimen_cmin to \the\dimen_cmax}\r_\fi
        \all_cno\dimen_cmin\r_}

\def\all_cfinal{\r_
        \count11\dimen_cmin\r_
        \a_\count11-3\r_
        \ifnum\tr_a>0\r_
        \wlog{page \thepage: end of dimen allocation}\r_\fi}

\newif\if_cd

\def\id_{\r_
        \ifnum\all_cno=\dimen_cmax\r_\all_cno\dimen_cmin\r_
                        \else\a_\all_cno1\fi\r_
        \ea_\ifx\cs_ f_ll\the\all_cno\es_\f_ll\r_
                \ifnum\all_cno=\dimen_clast\r_\ch@ck1{\count11}\dimen\r_
                \else\_cdtrue\fi
        \else\_cdfalse\fi}

\def\all_c#1{\dimen_clast\all_cno\r_
        \loop\id_\if_cd\repeat
        \ea_\dimendef\cs_ #1\es_\all_cno\r_
        \ea_\edef\cs_ alno_#1\es_{\the\all_cno}\r_
        \ea_\let\cs_ f_ll\the\all_cno\es_\f_ll\r_
        \ifnum\tr_a>0\r_
        \wlog{#1 = dimen\the\all_cno\space---\space occupied}\r_\fi}

\def\deall_c#1{\all_cno\cs_ alno_#1\es_\r_
        \ea_\let\cs_ f_ll\the\all_cno\es_\r_
        \ifnum\tr_a>0\r_
        \wlog{#1 = dimen\the\all_cno\space---\space freed}\r_\fi}

%       BASICS: BOX ALLOCATION

\newcount\box_cmin
\newcount\box_cmax
\newcount\box_clast

\newcount\ball_cno

\let\bf_ll\noexpand     % the value "full"; "empty" is \relax

\def\ball_cinit{\r_
        \box_cmin\count14\r_
        \a_\box_cmin3\r_
        \box_cmax\insc@unt\a_\box_cmax-2\r_
        \ifnum\tr_a>0\r_
\wlog{page \thepage: boxes allocatable from \the\box_cmin to \the\box_cmax}\r_\fi
        \ball_cno\box_cmin\r_}

\def\ball_cfinal{\r_
        \count14\box_cmin\r_
        \a_\count14-3\r_
        \ifnum\tr_a>0\r_
        \wlog{page \thepage: end of box allocation}\r_\fi}

\newif\if_cb

\def\ib_{\r_
        \ifnum\ball_cno=\box_cmax\r_\ball_cno\box_cmin\r_
                        \else\a_\ball_cno1\fi\r_
        \ea_\ifx\cs_ bf_ll\the\ball_cno\es_\bf_ll\r_
                \ifnum\ball_cno=\box_clast\r_\ch@ck4{\count14}\box\r_
                \else\_cbtrue\fi
        \else\_cbfalse\fi}

\def\ball_c#1{\box_clast\ball_cno\r_
        \loop\ib_\if_cb\repeat
        \ea_\chardef\cs_ #1\es_\ball_cno\r_
        \ea_\edef\cs_ balno_#1\es_{\the\ball_cno}\r_
        \ea_\let\cs_ bf_ll\the\ball_cno\es_\bf_ll\r_
        \ifnum\tr_a>0\r_
        \wlog{#1 = box\the\ball_cno\space---\space occupied}\r_\fi}

\def\bdeall_c#1{\ball_cno\cs_ balno_#1\es_\r_
        \ea_\let\cs_ bf_ll\the\ball_cno\es_\r_
        \ea_\m_savebox\cs_ #1\es_{}\r_
        \ifnum\tr_a>0\r_
        \wlog{#1 = box\the\ball_cno\space---\space freed}\r_\fi}

\def\useb_x#1{\leavevmode\unhcopy#1}

\let\b_x\unhbox

%       BASICS: MACRO TECHNICS

%       MODIFIED PICTURE COMMANDS

% I do not want to use unitlength, to prevent confusion

\let\un_t\unitlength

\def\m_put{\un_t1pt\r_\put}
\def\m_multiput{\un_t1pt\r_\multiput}
\def\m_savebox{\un_t1pt\r_\savebox}
\def\m_makebox{\un_t1pt\r_\makebox}
\def\_bpic{\trac_off\r_\un_t1pt\begin{picture}}
\def\_epic{\end{picture}\is_}

% in PT and C there will be \put and \multiput outside picture
% \_put and \_multiput differ in that they do not an initial
% \@killglue

\def\_put(#1,#2)#3{\un_t1pt\r_
        \raise #2\un_t \hbox to \z@ {\kern #1\un_t#3\hss}\is_}

\def\_multiput(#1,#2)(#3,#4)#5#6{\un_t1pt\r_\@multicnt =#5\relax \@xdim =
#1\un_t \@ydim =#2\un_t \@whilenum \@multicnt > 0\do {\raise
 \@ydim \hbox to \z@ {\kern \@xdim #6\hss }\advance \@multicnt \m@ne \ad
vance \@xdim #3\un_t \advance \@ydim #4\un_t }\is_}

\def\_lvm{\leavevmode}

%       VARIABLES

\newbox\fs_tr
\newdimen\fs_ht
\newdimen\fs_dp

\newcount\c_acc

\newdimen\d_acc
\newdimen\d_bcc
\newdimen\d_ccc
\newdimen\d_dcc
\newdimen\d_ecc
\newdimen\d_fcc
\newdimen\d_xcc
\newdimen\d_ycc

\newdimen\r_s           % function result
\newcount\cr_s          % function result

%       DISSECTION

\def\i_#1{#1}           % argument is undelimited: strips leading spaces!

\def\h_#1#2_{#1}
\def\t_#1#2_{#2}

\def\f_th#1#2#3.{#1}
\def\s_th#1#2#3.{#2}
\def\t_th#1#2#3.{#3}

\def\f_t#1#2#3#4.{#1}
\def\s_t#1#2#3#4.{#2}
\def\t_t#1#2#3#4.{#3}
\def\q_t#1#2#3#4.{#4}

% head and tail. Does macro expansion first

\def\hs_#1#2_{\edef\_head{\nx_\h_\i_#1#2_}\r_
                \edef\_tail{\nx_\t_\i_#1#2_}\r_
                \edef\_arg{\_head\_tail}}

% \ts_ tests whether argument is empty. Expands macros, skips blanks

\def\ts_#1_{\def\_arg{}\if _\i_#1_\_emptytrue\else\r_
        \edef\_arg{\i_#1}\ifx\_arg\sp_\_emptytrue\def\_arg{}\else\r_
        \if _\_arg _\_emptytrue\else\_emptyfalse\fi\fi\fi}

\def\l_t#1#2{\edef\_dummy{\nx_\let\nx_#1#2}\_dummy}

\def\c_p#1#2{\ea_\edef\cs_#1\es_{#2}}

\def\if_u#1{\ea_\ifx\cs_ #1\es_\r_}     % IFUNDEFINED{control sequence}

%       LOOK AHEAD

\def\sp_{ }

\def\futur_splet#1{\g_\def\_cs{#1}%
        \afterassignment\step_one\let\n_xtt_k= }
{\def\\{\global\let\_sp= } \\ }%
\def\step_one{\ea_\futurelet\_cs\step_two}
\def\step_two{\ea_\ifx\_cs\_sp\let\n_xt=\step_three
        \else\let\n_xt=\n_xtt_k\fi \n_xt}
\def\step_three{\afterassignment\step_one\let\n_xt= }

%       DECISIONS

\newif\if_empty
\newif\if_inchars
 
\newtoks\_list

\def\oc_#1_#2_{\edef\do_{\nx_\prim_oc_#1_\nx_#2_}\do_}
\def\prim_oc_#1_#2_{\edef\dud_{\g_\_list{#2}}\dud_\r_
        \edef\atst##1{\nx_\ea_\nx_\a\nx_\the\nx_##1#1\nx_\atst\nx_\a}\r_
        \def\a##1#1##2##3\a{\ifx\atst##2\_incharsfalse\else\_incharstrue\fi}\r_
        \atst\_list}

\def\let_oc_#1_#2_{\edef\do_{\nx_\_list\nx_{#2\nx_}}\do_\r_
        \if _#2_\_incharsfalse\else\r_
        \edef\_iii{\nx_\h_\the\_list\nx_ _}\r_
        \edef\_jjj{\nx_\t_\the\_list\nx_ _}\r_
        \edef\_ii{\nx_\let\nx_\_i\_iii}\_ii\r_
        \edef\_jj{\nx_\_list\nx_{\_jjj\nx_}}\_jj\r_
        \ifx\_i#1\_incharstrue\else\let_oc_#1_\the\_list _\fi\fi}

%       ARITHMETIC

{\catcode`p12\catcode`t12
\gdef\vv_vv#1pt{#1}                     % removes pt from a string

% \rr_rr removes digits behind decimal point, rounds off
% \dd_dd removes digits behind decimal point, rounds off down

\gdef\rr_rr#1.#2pt{\cr_s#1\ifnum\h_#2_>4\a_\cr_s1\fi}
\gdef\dd_dd#1.#2pt{\cr_s#1}}

\let\gt_r\vv_vv
\let\gt_n\rr_rr
\let\gt_m\dd_dd

\def\n_#1{\ea_\gt_r\the#1}      % gives rat value of a dimen
\def\ni_#1{\ea_\gt_n\the#1}     % gives int value of a dimen

\def\r_m#1{\romannumeral\the#1} % gives roman representation of a count

%       DATA: FORKS (PICTREES)

\newcount\t_slx         \newcount\t_sly

% Several dimens get temporal values just before set up of forks

% \t_sx \t_sy half width and  total height of fork
% \t_slx \t_sly slopes of firm   lines
% \t_msx \t_msy slopes of dotted lines
% \t_lne \t_lnf length of firm   lines
% \t_mne \t_mnf length of dotted lines
% \t_dx  \t_dy  lower  endpoint of lines
% \t_ex  \t_ey  upper  endpoint of left line
% \t_fx  \t_fy  upper  endpoint of right line

% \mn_tt sets sizes for unary forks dependent of scale

\def\mn_tt<#1>{\r_
        \t_sx0pt\t_sy10pt\r_
        \t_sx#1\t_sx\r_
        \t_sy#1\t_sy\r_}

% \b_tt sets sizes for binary forks dependent of scale

\def\b_tt<#1>#2{\r_
        \ifnum#2=1\r_\t_sx5pt\t_sy10pt\r_
   \else\ifnum#2=2\r_\t_sx8pt\t_sy10pt\r_
   \else\ifnum#2=3\r_\t_sx10pt\t_sy10pt\r_
   \else\ifnum#2=4\r_\t_sx15pt\t_sy10pt\r_
        \fi\fi\fi\fi
        \t_sx#1\t_sx\r_
        \t_sy#1\t_sy\r_}

% \xy_def computes x-cos of endpoints from y-cos

\def\xy_def#1#2#3{\r_
        \t_dx#1pt\d_\t_dx\t_sly\m_\t_dx\t_slx\r_
        \t_ex#2pt\d_\t_ex\t_sly\m_\t_ex\t_slx\r_
        \t_fx#3pt\d_\t_fx\t_sly\m_\t_fx\t_slx\r_}

% \s_tt sets all parameters.
% The third parameter selects branches: firm, dotted, no. It consists
% of one letter F,N,D in the unary case, and any pair of letters from
% f,n,d in the binary case.

\def\s_tt<#1>#2#3 D#4 E#5 F#6:{\r_
        \hs_#3_\ts_\_tail _\r_
        \if_empty\r_
                \if\_head f\def\f_l{F}\r_
                \else\if\_head d\def\f_l{D}\r_
                \else\if\_head n\def\f_l{N}\fi\fi\fi\r_
                \edef\f_r{\f_l}\r_
                \edef\_arg{\_head}\r_
        \else\edef\f_l{\_head}\edef\f_r{\_tail}\fi\r_
        \t_dy#4pt\t_ey#5pt\t_ey#6pt\r_
        \if\f_l f\b_tt<#1>#2\fi
        \if\f_l d\b_tt<#1>#2\fi
        \if\f_r f\b_tt<#1>#2\fi
        \if\f_r d\b_tt<#1>#2\fi
        \if\f_l F\mn_tt<#1>\fi
        \if\f_l D\mn_tt<#1>\fi
             \ifnum#2=1\r_\t_slx1\t_sly2\r_
        \else\ifnum#2=2\r_\t_slx4\t_sly5\r_
        \else\ifnum#2=3\r_\t_slx1\t_sly1\r_
        \else\ifnum#2=4\r_\t_slx3\t_sly2\r_
                \fi\fi\fi\fi
        \if\f_l F\r_
                \t_slx0\t_sly1\t_lne10pt\r_
                \t_lne#1\t_lne\r_
                \a_\t_lne-#4pt\r_
                \a_\t_lne-#5pt\r_
        \else\if\f_l D\r_
                \t_mne2.5pt\t_msx0pt\t_msy4pt\r_
                \a_\t_dy2pt\r_
                \t_mne#1\t_mne\r_
                \d_acc#4pt\a_\d_acc#5pt\r_
                \d_\d_acc4\r_
                \a_\t_mne-\d_acc\r_
                %\a_\t_mne1pt\r_
        \else\if\f_l f\set_f{#1}#2{#4}{#5}{#6}\fi\r_
             \if\f_l d\set_d{#1}#2{#4}{#5}{#6}\fi\r_
             \if\f_r f\set_f{#1}#2{#4}{#5}{#6}\fi\r_
             \if\f_r d\set_d{#1}#2{#4}{#5}{#6}\fi\r_
        \fi\fi}

\def\set_f#1#2#3#4#5{\r_
             \ifnum#2=1\r_\t_lne5pt\r_
        \else\ifnum#2=2\r_\t_lne8pt\r_
        \else\ifnum#2=3\r_\t_lne10pt\r_
        \else\ifnum#2=4\r_\t_lne15pt\r_
                \fi\fi\fi\fi
                \xy_def{#3}{#4}{#5}\r_
                \t_lne#1\t_lne\r_
                \a_\t_lne-\t_dx\r_
                \t_lnf\t_lne\r_
                \a_\t_lne-\t_ex\r_
                \a_\t_lnf-\t_fx\r_}

\def\set_d#1#2#3#4#5{\r_
                \ifnum#2=1\r_\t_mne2.5pt\t_mnf2.5pt\t_msx2pt\t_msy4pt\r_
                \xy_def{#3}{#4}{#5}\r_
                \d_xcc\t_dx\r_\d_ycc\t_dy\r_
                \a_\d_xcc.5\t_msx\r_\a_\d_ycc.5\t_msy\r_
                \d_acc\d_xcc\a_\d_acc\t_ex\r_
                \d_\d_acc2\r_
                \t_mne#1\t_mne\r_
                \a_\t_mne-\d_acc\r_
                %\a_\t_mne1pt\r_
                \d_acc\d_xcc\a_\d_acc\t_fx\r_
                \d_\d_acc2\r_
                \t_mnf#1\t_mnf\r_
                \a_\t_mnf-\d_acc\r_
                %\a_\t_mnf1pt\r_
\else\ifnum#2=2\r_\t_mne2.66667pt\t_mnf2.66667pt\t_msx3pt\t_msy3.6pt\r_
                \xy_def{#3}{#4}{#5}\r_
                \d_xcc\t_dx\r_\d_ycc\t_dy\r_
                \a_\d_xcc.5\t_msx\r_\a_\d_ycc.5\t_msy\r_
                \d_acc\d_xcc\a_\d_acc\t_ex\r_
                \d_\d_acc3\r_
                \t_mne#1\t_mne\r_
                \a_\t_mne-\d_acc\r_
                \a_\t_mne1pt\r_
                \d_acc\d_xcc\a_\d_acc\t_fx\r_
                \d_\d_acc3\r_
                \t_mnf#1\t_mnf\r_
                \a_\t_mnf-\d_acc\r_
                \a_\t_mnf1pt\r_
\else\ifnum#2=3\r_\t_mne2.5pt\t_mnf2.5pt\t_msx4pt\t_msy4pt\r_
                \xy_def{#3}{#4}{#5}\r_
                \d_xcc\t_dx\r_\d_ycc\t_dy\r_
                \a_\d_xcc.5\t_msx\r_\a_\d_ycc.5\t_msy\r_
                \d_acc\d_xcc\a_\d_acc\t_ex\r_
                \d_\d_acc4\r_
                \t_mne#1\t_mne\r_
                \a_\t_mne-\d_acc\r_
                %\a_\t_mne1pt\r_
                \d_acc\d_xcc\a_\d_acc\t_fx\r_
                \d_\d_acc4\r_
                \t_mnf#1\t_mnf\r_
                \a_\t_mnf-\d_acc\r_
                %\a_\t_mnf1pt\r_
\else\ifnum#2=4\r_\t_mne3.33333pt\t_mnf3.33333pt\t_msx4.5pt\t_msy3pt\r_
                \xy_def{#3}{#4}{#5}\r_
                \d_xcc\t_dx\r_\d_ycc\t_dy\r_
                \a_\d_xcc.5\t_msx\r_\a_\d_ycc.5\t_msy\r_
                \d_acc\d_xcc\a_\d_acc\t_ex\r_
                \d_\d_acc9\m_\d_acc2\r_
                \t_mne#1\t_mne\r_
                \a_\t_mne-\d_acc\r_
                \a_\t_mne1pt\r_
                \d_acc\d_xcc\a_\d_acc\t_fx\r_
                \d_\d_acc9\m_\d_acc2\r_
                \t_mnf#1\t_mnf\r_
                \a_\t_mnf-\d_acc\r_
                \a_\t_mnf1pt\r_
                \fi\fi\fi\fi}

\def\c_t{\circle{0}}

% Selective typesetting of unary fork

\def\m_rk#1{\d_acc\t_sx\m_\d_acc2\r_
        \_bpic(\n_\d_acc,\n_\t_sy)\r_
        \if#1f\m_put(0,\n_\t_dy){\line(-\t_slx,\t_sly){\n_\t_lne}}\fi
        \if#1d\ea_\gt_m\the\t_mne\r_
        \m_multiput(0,\n_\d_ycc)(-\n_\t_msx,\n_\t_msy){\cr_s}{\c_t}\fi
        \_epic}

% Selective typesetting of unary fork

\def\f_rk#1#2{\r_\d_acc\t_sx\m_\d_acc2\r_
        \_bpic(\n_\d_acc,\n_\t_sy)\r_
        \if#1f\m_put(-\n_\t_dx,\n_\t_dy){\line(-\t_slx,\t_sly){\n_\t_lne}}\fi
        \if#2f\m_put(\n_\t_dx,\n_\t_dy){\line(\t_slx,\t_sly){\n_\t_lnf}}\fi
        \if#1d \ea_\gt_m\the\t_mne\r_
        \m_multiput(-\n_\d_xcc,\n_\d_ycc)(-\n_\t_msx,\n_\t_msy){\cr_s}{\c_t}\fi
        \if#2d\ea_\gt_m\the\t_mnf\r_
        \m_multiput(\n_\d_xcc,\n_\d_ycc)(\n_\t_msx,\n_\t_msy){\cr_s}{\c_t}\fi
        \_epic}

% The line that separates conclusion from premises in PROOF TREES

\def\l_ne#1{\r_
        \if#1f\m_put(\n_\d_bcc,\n_\d_acc){\line(1,0){\n_\ll_}}\r_
   \else\if#1d\d_ccc\ll_\a_\d_ccc-4pt\d_\d_ccc8\r_\ni_\d_ccc\r_\c_acc\cr_s\r_ 
% number of dashes is now in the count \c_acc
        \d_ccc8pt\m_\d_ccc\c_acc\r_
        \exc_\ll_\a_\exc_-4pt\a_\exc_-\d_ccc\r_ 
% exces width of total line over the dashed line
        \d_\exc_\c_acc\r_\a_\exc_8pt\r_
% exces divided over the dashes
        \m_multiput(\n_\d_bcc,\n_\d_acc)(\n_\exc_,0){\c_acc}{\line(1,0){4}}\r_
        \d_ccc\d_bcc\r_\a_\d_ccc\ll_\r_
        \m_put(\n_\d_ccc,\n_\d_acc){\line(-1,0){4}}\r_
        \fi\fi}


\catcode`_8             % preventing interaction with latex definitions