%%
%% This is file `ebproof.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% ebproof.dtx  (with options: `package')
%% 
%% IMPORTANT NOTICE:
%% 
%% For the copyright see the source file.
%% 
%% Any modified versions of this file must be renamed
%% with new filenames distinct from ebproof.sty.
%% 
%% For distribution of the original source see the terms
%% for copying and modification in the file ebproof.dtx.
%% 
%% This generated file may be distributed as long as the
%% original source files, as listed above, are part of the
%% same distribution. (The sources need not necessarily be
%% in the same archive or directory.)
\NeedsTeXFormat{LaTeX2e}
\RequirePackage{expl3}
\RequirePackage{xparse}
\ProvidesExplPackage{ebproof}{2021/01/28}{2.1.1}{EB's proof trees}
\bool_new:N \l__ebproof_updown_bool
\keys_define:nn { ebproof } {
center .bool_set:N = \l__ebproof_center_bool,
proof~style .choice: ,
proof~style / upwards .code:n = \bool_set_false:N \l__ebproof_updown_bool,
proof~style / downwards .code:n = \bool_set_true:N \l__ebproof_updown_bool,
separation .dim_set:N = \l__ebproof_separation_dim,
rule~margin .dim_set:N = \l__ebproof_rule_margin_dim,
rule~thickness .dim_set:N = \l__ebproof_rule_thickness_dim,
rule~separation .dim_set:N = \l__ebproof_rule_separation_dim,
rule~dash~length .dim_set:N = \l__ebproof_rule_dash_length_dim,
rule~dash~space .dim_set:N = \l__ebproof_rule_dash_space_dim,
rule~code .tl_set:N = \l__ebproof_rule_code_tl,
rule~style .choice:,
template .tl_set:N = \l__ebproof_template_tl,
left~template .tl_set:N = \l__ebproof_left_template_tl,
right~template .tl_set:N = \l__ebproof_right_template_tl,
left~label .tl_set:N = \l__ebproof_left_label_tl,
right~label .tl_set:N = \l__ebproof_right_label_tl,
left~label~template .tl_set:N = \l__ebproof_left_label_template_tl,
right~label~template .tl_set:N = \l__ebproof_right_label_template_tl,
label~separation .dim_set:N = \l__ebproof_label_separation_dim,
label~axis .dim_set:N = \l__ebproof_label_axis_dim,
}
\NewDocumentCommand \ebproofnewrulestyle { mm } {
  \keys_define:nn { ebproof } {
    rule~style / #1 .meta:nn = { ebproof } { #2 }
  }
}
\ebproofnewrulestyle { simple } {
  rule~code = { \tex_hrule:D height \l__ebproof_rule_thickness_dim }
}
\ebproofnewrulestyle { no~rule } {
  rule~code =
}
\ebproofnewrulestyle { double } {
  rule~code = {
    \tex_hrule:D height \l__ebproof_rule_thickness_dim
    \skip_vertical:N \l__ebproof_rule_separation_dim
    \tex_hrule:D height \l__ebproof_rule_thickness_dim
  }
}
\ebproofnewrulestyle { dashed } {
  rule~code = {
    \hbox_to_wd:nn { \tex_hsize:D } {
      \dim_set:Nn \l_tmpa_dim { \l__ebproof_rule_dash_space_dim / 2 }
      \skip_horizontal:n { -\l_tmpa_dim }
      \tex_cleaders:D \hbox:n {
        \skip_horizontal:N \l_tmpa_dim
        \tex_vrule:D
          height \l__ebproof_rule_thickness_dim
          width \l__ebproof_rule_dash_length_dim
        \skip_horizontal:N \l_tmpa_dim
      } \tex_hfill:D
      \skip_horizontal:n { -\l_tmpa_dim }
    }
  }
}
\keys_set:nn { ebproof } {
  center = true,
  proof~style = upwards,
  separation = 1.5em,
  rule~margin = .7ex,
  rule~thickness = .4pt,
  rule~separation = 2pt,
  rule~dash~length = .2em,
  rule~dash~space = .3em,
  rule~style = simple,
  template = $\inserttext$,
  left~template = $\inserttext\mathrel{}$,
  right~template = $\mathrel{}\inserttext$,
  left~label = ,
  right~label = ,
  left~label~template = \inserttext,
  right~label~template = \inserttext,
  label~separation = 0.5em,
  label~axis = 0.5ex
}
\NewDocumentCommand \ebproofnewstyle { mm } {
  \keys_define:nn { ebproof } { #1 .meta:n = { #2 } }
}
\int_new:N \g__ebproof_register_int
\cs_new:Nn \__ebproof_box:N {
  \str_item:nn { #1 } { 2 } __ebproof_ \tl_use:N #1 _box
}
\cs_new:Nn \__ebproof_marks:N {
  \str_item:nn { #1 } { 2 } __ebproof_ \tl_use:N #1 _prop
}
\cs_new:Nn \__ebproof_new:N {
  \tl_new:N #1
  \int_gincr:N \g__ebproof_register_int
  \str_if_eq:eeTF { \str_item:nn { #1 } { 2 } } { g }
    { \tl_gset:Nx #1 { \int_to_arabic:n { \g__ebproof_register_int } } }
    { \tl_set:Nx #1 { \int_to_arabic:n { \g__ebproof_register_int } } }
  \box_new:c { \__ebproof_box:N #1 }
  \prop_new:c { \__ebproof_marks:N #1 }
}
\cs_new:Nn \__ebproof_clear:N {
  \hbox_set:cn { \__ebproof_box:N #1 } {}
  \prop_clear:c { \__ebproof_marks:N #1 }
  \__ebproof_set_mark:Nnn #1 { left } { 0pt }
  \__ebproof_set_mark:Nnn #1 { right } { 0pt }
  \__ebproof_set_mark:Nnn #1 { axis } { 0pt }
}
\dim_new:N \l__ebproof_transit_dim
\cs_new:Nn \__ebproof_set_mark:Nnn {
  \dim_set:Nn \l__ebproof_transit_dim { #3 }
  \prop_put:cnV { \__ebproof_marks:N #1 } { #2 }
    \l__ebproof_transit_dim
}
\cs_new:Nn \__ebproof_mark:Nn {
  \prop_item:cn { \__ebproof_marks:N #1 } { #2 }
}
\cs_new:Nn \__ebproof_shift_x:Nn {
  \prop_map_inline:cn { \__ebproof_marks:N #1 } {
    \__ebproof_set_mark:Nnn #1 { ##1 } { ##2 + #2 }
  }
}
\cs_new:Nn \__ebproof_enlarge_conclusion:NN {
  \dim_set:Nn \l_tmpa_dim { \__ebproof_mark:Nn #1 {axis}
    + \__ebproof_mark:Nn #2 {left} - \__ebproof_mark:Nn #2 {axis} }
  \dim_compare:nNnT { \l_tmpa_dim } < { \__ebproof_mark:Nn #1 {left} } {
    \__ebproof_set_mark:Nnn #1 {left} { \l_tmpa_dim } }
  \dim_set:Nn \l_tmpa_dim { \__ebproof_mark:Nn #1 {axis}
    + \__ebproof_mark:Nn #2 {right} - \__ebproof_mark:Nn #2 {axis} }
  \dim_compare:nNnT { \l_tmpa_dim } > { \__ebproof_mark:Nn #1 {right} } {
    \__ebproof_set_mark:Nnn #1 {right} { \l_tmpa_dim } }
}
\cs_new:Nn \__ebproof_make_simple:Nn {
  \hbox_set:cn { \__ebproof_box:N #1 } { #2 }
  \__ebproof_set_mark:Nnn #1 { left } { 0pt }
  \__ebproof_set_mark:Nnn #1 { axis } { \box_wd:c { \__ebproof_box:N #1 } / 2 }
  \__ebproof_set_mark:Nnn #1 { right } { \box_wd:c { \__ebproof_box:N #1 } }
}
\cs_new:Nn \__ebproof_make_split:Nnn {
  \__ebproof_set_mark:Nnn #1 { left } { 0pt }
  \hbox_set:cn { \__ebproof_box:N #1 } { #2 }
  \__ebproof_set_mark:Nnn #1 { axis } { \box_wd:c { \__ebproof_box:N #1 } }
  \hbox_set:cn { \__ebproof_box:N #1 } { \hbox_unpack:c { \__ebproof_box:N #1 } #3 }
  \__ebproof_set_mark:Nnn #1 { right } { \box_wd:c { \__ebproof_box:N #1 } }
}
\cs_new:Nn \__ebproof_make_vertical:Nnnn {
  \__ebproof_set_mark:Nnn #1 { left } { 0pt }
  \__ebproof_set_mark:Nnn #1 { axis } { #2 }
  \__ebproof_set_mark:Nnn #1 { right } { #3 }
  \vbox_set:cn { \__ebproof_box:N #1 } {
    \dim_set:Nn \tex_hsize:D { \__ebproof_mark:Nn #1 {right} }
    #4
  }
  \box_set_wd:cn { \__ebproof_box:N #1 } { \__ebproof_mark:Nn #1 {right} }
}
\cs_new:Nn \__ebproof_extend:Nnnnn {
  \dim_compare:nNnF { #2 } = { 0pt } {
    \hbox_set:cn { \__ebproof_box:N #1 } {
      \skip_horizontal:n { #2 }
      \box_use:c { \__ebproof_box:N #1 }
    }
    \__ebproof_shift_x:Nn #1 { #2 }
  }
  \box_set_ht:Nn #1 { \box_ht:c { \__ebproof_box:N #1 } + #3 }
  \box_set_wd:Nn #1 { \box_wd:c { \__ebproof_box:N #1 } + #4 }
  \box_set_dp:Nn #1 { \box_dp:c { \__ebproof_box:N #1 } + #5 }
}
\cs_new:Nn \__ebproof_append_right:NnN {
  \hbox_set:cn { \__ebproof_box:N #1 } {
    \box_use:c { \__ebproof_box:N #1 }
    \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
    \box_use:c { \__ebproof_box:N #3 }
  }
}
\cs_new:Nn \__ebproof_append_left:NnN {
  \__ebproof_shift_x:Nn #1 { \box_wd:c { \__ebproof_box:N #3 } + #2 }
  \hbox_set:cn { \__ebproof_box:N #1 } {
    \box_use:c { \__ebproof_box:N #3 }
    \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
    \box_use:c { \__ebproof_box:N #1 }
  }
}
\cs_new:Nn \__ebproof_align:NN {
  \dim_set:Nn \l_tmpa_dim
    { \__ebproof_mark:Nn #2 {axis} - \__ebproof_mark:Nn #1 {axis} }
  \dim_compare:nNnTF \l_tmpa_dim < { 0pt } {
    \__ebproof_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt }
  } {
    \__ebproof_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt }
  }
}
\cs_new:Nn \__ebproof_append_above:NN {
  \__ebproof_align:NN #1 #2
  \vbox_set:cn  { \__ebproof_box:N #1 } {
    \box_use:c { \__ebproof_box:N #2 }
    \tex_prevdepth:D -1000pt
    \box_use:c { \__ebproof_box:N #1 }
  }
}
\cs_new:Nn \__ebproof_append_below:NN {
  \__ebproof_align:NN #1 #2
  \vbox_set_top:cn { \__ebproof_box:N #1 } {
    \box_use:c { \__ebproof_box:N #1 }
    \tex_prevdepth:D -1000pt
    \box_use:c { \__ebproof_box:N #2 }
  }
}
\cs_new:Nn \__ebproof_overlay:NN {
  \__ebproof_align:NN #1 #2
  \hbox_set:cn { \__ebproof_box:N #1 } {
    \hbox_overlap_right:n { \box_use:c { \__ebproof_box:N #1 } }
    \box_use:c { \__ebproof_box:N #2 }
    \dim_compare:nNnT
      { \box_wd:c { \__ebproof_box:N #2 } } < { \box_wd:c { \__ebproof_box:N #1 } }
      { \skip_horizontal:n
        { \box_wd:c { \__ebproof_box:N #1 } - \box_wd:c { \__ebproof_box:N #2 } } }
  }
}
\cs_new:Nn \__ebproof_vcenter:N {
  \dim_set:Nn \l_tmpa_dim
    { ( \box_ht:c { \__ebproof_box:N #1 } - \box_dp:c { \__ebproof_box:N #1 } ) / 2 }
  \box_set_eq:Nc \l_tmpa_box { \__ebproof_box:N #1 }
  \hbox_set:cn { \__ebproof_box:N #1 }
    { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_tmpa_box } }
}
\cs_new:Nn \__ebproof_append_vertical:NN {
  \bool_if:NTF \l__ebproof_updown_bool
    { \__ebproof_append_below:NN #1 #2 }
    { \__ebproof_append_above:NN #1 #2 }
}
\cs_new:Nn \__ebproof_make_rule_for:NNN {
  \__ebproof_make_vertical:Nnnn #1
    { \__ebproof_mark:Nn #2 {axis} - \__ebproof_mark:Nn #2 {left} }
    { \__ebproof_mark:Nn #2 {right} - \__ebproof_mark:Nn #2 {left} }
    {
      \skip_vertical:N \l__ebproof_rule_margin_dim
      \tl_if_empty:NF { \l__ebproof_rule_code_tl } {
        \tl_use:N \l__ebproof_rule_code_tl
        \skip_vertical:N \l__ebproof_rule_margin_dim
      }
    }
  \__ebproof_vcenter:N #1
  \tl_if_blank:VF \l__ebproof_left_label_tl {
    \__ebproof_make_simple:Nn #3 {
      \box_move_down:nn { \l__ebproof_label_axis_dim } { \hbox:n {
        \cs_set_eq:NN \inserttext \l__ebproof_left_label_tl
        \tl_use:N \l__ebproof_left_label_template_tl
      } }
    }
    \box_set_ht:cn { \__ebproof_box:N #3 } { 0pt }
    \box_set_dp:cn { \__ebproof_box:N #3 } { 0pt }
    \__ebproof_append_left:NnN
      \l__ebproof_c_box \l__ebproof_label_separation_dim \l__ebproof_d_box
  }
  \tl_if_blank:VF \l__ebproof_right_label_tl {
    \__ebproof_make_simple:Nn #3 {
      \box_move_down:nn { \l__ebproof_label_axis_dim } { \hbox:n {
        \cs_set_eq:NN \inserttext \l__ebproof_right_label_tl
        \tl_use:N \l__ebproof_right_label_template_tl
      } }
    }
    \box_set_ht:cn { \__ebproof_box:N #3 } { 0pt }
    \box_set_dp:cn { \__ebproof_box:N #3 } { 0pt }
    \__ebproof_append_right:NnN
      \l__ebproof_c_box \l__ebproof_label_separation_dim \l__ebproof_d_box
  }
}
\int_new:N \g__ebproof_level_int
\box_new:N \g__ebproof_stack_box
\seq_new:N \g__ebproof_stack_seq
\cs_new:Nn \__ebproof_clear_stack: {
  \int_gset:Nn \g__ebproof_level_int { 0 }
  \hbox_gset:Nn \g__ebproof_stack_box { }
  \seq_gclear:N \g__ebproof_stack_seq
}
\cs_new:Nn \__ebproof_push:N {
  \int_gincr:N \g__ebproof_level_int
  \hbox_gset:Nn \g__ebproof_stack_box
    { \hbox_unpack:N \g__ebproof_stack_box \box_use:c { \__ebproof_box:N #1 } }
  \seq_gput_left:Nv \g__ebproof_stack_seq
    { \__ebproof_marks:N #1 }
}
\cs_new:Nn \__ebproof_pop:N {
  \int_compare:nNnTF { \g__ebproof_level_int } > { 0 } {
    \int_gdecr:N \g__ebproof_level_int
    \hbox_gset:Nn \g__ebproof_stack_box {
      \hbox_unpack:N \g__ebproof_stack_box
      \box_gset_to_last:N \g_tmpa_box
    }
    \box_set_eq_drop:cN { \__ebproof_box:N #1 } \g_tmpa_box
    \seq_gpop_left:NN \g__ebproof_stack_seq \l_tmpa_tl
    \tl_set_eq:cN { \__ebproof_marks:N #1 } \l_tmpa_tl
  } {
    \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{}
    \__ebproof_clear:N #1
  }
}
\__ebproof_new:N \l__ebproof_a_box
\__ebproof_new:N \l__ebproof_b_box
\__ebproof_new:N \l__ebproof_c_box
\__ebproof_new:N \l__ebproof_d_box
\cs_new:Nn \__ebproof_join_horizontal:n {
  \int_case:nnF { #1 } {
  { 0 } {
    \group_begin:
    \__ebproof_clear:N \l__ebproof_a_box
    \__ebproof_push:N \l__ebproof_a_box
    \group_end:
  }
  { 1 } { }
  } {
    \group_begin:
    \__ebproof_pop:N \l__ebproof_a_box
    \prg_replicate:nn { #1 - 1 } {
      \__ebproof_pop:N \l__ebproof_b_box
      \__ebproof_append_left:NnN
        \l__ebproof_a_box \l__ebproof_separation_dim \l__ebproof_b_box
    }
    \__ebproof_set_mark:Nnn \l__ebproof_a_box { left }
      { \__ebproof_mark:Nn \l__ebproof_b_box { left } }
    \__ebproof_set_mark:Nnn \l__ebproof_a_box { axis }
      { ( \__ebproof_mark:Nn \l__ebproof_a_box { left }
        + \__ebproof_mark:Nn \l__ebproof_a_box { right } ) / 2 }
    \__ebproof_push:N \l__ebproof_a_box
    \group_end:
  }
}
\cs_new:Nn \__ebproof_join_vertical: {
  \group_begin:
  \__ebproof_pop:N \l__ebproof_a_box
  \__ebproof_pop:N \l__ebproof_b_box
  \__ebproof_enlarge_conclusion:NN \l__ebproof_b_box \l__ebproof_a_box
  \__ebproof_make_rule_for:NNN \l__ebproof_c_box \l__ebproof_b_box
    \l__ebproof_d_box
  \__ebproof_append_vertical:NN \l__ebproof_a_box \l__ebproof_c_box
  \__ebproof_append_vertical:NN \l__ebproof_a_box \l__ebproof_b_box
  \__ebproof_push:N \l__ebproof_a_box
  \group_end:
}
\cs_new:Npn \__ebproof_statement_parse:w #1 & #2 & #3 \q_stop {
  \tl_if_empty:nTF { #3 } {
    \__ebproof_make_simple:Nn \l__ebproof_a_box
      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l__ebproof_template_tl }
  } {
    \__ebproof_make_split:Nnn \l__ebproof_a_box
      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l__ebproof_left_template_tl }
      { \cs_set:Npn \inserttext { #2 } \tl_use:N \l__ebproof_right_template_tl }
  }
  \__ebproof_push:N \l__ebproof_a_box
}
\cs_new:Nn \__ebproof_push_statement:n {
  \__ebproof_statement_parse:w #1 & & \q_stop
}
\seq_new:N \g__ebproof_statements_seq
\cs_new:Nn \__ebproof_setup_statements: {
  \seq_map_inline:Nn \g__ebproof_statements_seq {
    \cs_set_eq:cc { ebproof_saved_ ##1 } { ##1 }
    \cs_set_eq:cc { ##1 } { ebproof ##1 }
  }
}
\cs_new:Nn \__ebproof_restore_statements: {
  \seq_map_inline:Nn \g__ebproof_statements_seq {
    \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 }
  }
}
\cs_new:Nn \__ebproof_new_statement:nnn {
  \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 }
  \seq_gput_right:Nn \g__ebproof_statements_seq { #1 }
}
\cs_new:Nn \__ebproof_new_deprecated_statement:nnnn {
  \cs_new:cpn { ebproof_#1_warning: } {
    \PackageWarning { ebproof } { \token_to_str:c{#1}~is~deprecated,~#3 }
    \cs_gset:cn { ebproof_#1_warning: } { }
  }
  \__ebproof_new_statement:nnn { #1 } { #2 }
    { \use:c { ebproof_#1_warning: } #4 }
}
\__ebproof_new_statement:nnn { set } { m } {
  \keys_set:nn { ebproof } { #1 }
}
\__ebproof_new_statement:nnn { hypo } { O{} m } {
  \group_begin:
  \__ebproof_restore_statements:
  \keys_set:nn { ebproof } { #1 }
  \__ebproof_push_statement:n { #2 }
  \group_end:
}
\__ebproof_new_statement:nnn { infer } { O{} m O{} m } {
  \group_begin:
  \__ebproof_restore_statements:
  \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl
  \keys_set:nV { ebproof } \l_tmpa_tl
  \tl_set:Nn \l__ebproof_right_label_tl { #3 }
  \__ebproof_join_horizontal:n { #2 }
  \__ebproof_push_statement:n { #4 }
  \__ebproof_join_vertical:
  \group_end:
}
\__ebproof_new_statement:nnn { ellipsis } { m m } {
  \group_begin:
  \__ebproof_restore_statements:
  \tl_clear:N \l__ebproof_rule_code_tl
  \__ebproof_make_split:Nnn \l__ebproof_a_box { } {
    \vbox_set:Nn \l_tmpa_box {
      \skip_vertical:n { 1.2ex }
      \hbox:n { \tex_ignorespaces:D #1 }
      \skip_vertical:n { 1.2ex }
    }
    \vbox_to_ht:nn { \box_ht:N \l_tmpa_box } {
      \tex_xleaders:D \vbox_to_ht:nn { .8ex }
        { \tex_vss:D \hbox:n { . } \tex_vss:D }
      \tex_vfill:D
    }
    \hbox_overlap_right:n { ~ \box_use:N \l_tmpa_box }
  }
  \__ebproof_push:N \l__ebproof_a_box
  \__ebproof_join_vertical:
  \__ebproof_push_statement:n {#2}
  \__ebproof_join_vertical:
  \group_end:
}
\__ebproof_new_statement:nnn { rewrite } { m } {
  \group_begin:
  \__ebproof_restore_statements:
  \__ebproof_pop:N \l__ebproof_a_box
  \box_set_eq:Nc \l_tmpa_box { \__ebproof_box:N \l__ebproof_a_box }
  \hbox_set:Nn \l_tmpb_box {
    \cs_set_eq:NN \treebox \l_tmpa_box
    \cs_set:Npn \treemark { \__ebproof_mark:Nn \l__ebproof_a_box }
    { #1 }
  }
  \box_set_wd:Nn \l_tmpb_box { \box_wd:c { \__ebproof_box:N \l__ebproof_a_box } }
  \box_set_ht:Nn \l_tmpb_box { \box_ht:c { \__ebproof_box:N \l__ebproof_a_box } }
  \box_set_dp:Nn \l_tmpb_box { \box_dp:c { \__ebproof_box:N \l__ebproof_a_box } }
  \box_set_eq:cN { \__ebproof_box:N \l__ebproof_a_box } \l_tmpb_box
  \__ebproof_push:N \l__ebproof_a_box
  \group_end:
}
\__ebproof_new_statement:nnn { delims } { m m } {
  \group_begin:
  \__ebproof_restore_statements:
  \__ebproof_pop:N \l__ebproof_a_box
  \hbox_set:Nn \l_tmpa_box
    { $ \tex_vcenter:D { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } $ }
  \dim_set:Nn \l_tmpa_dim
    { \box_ht:N \l_tmpa_box - \box_ht:c { \__ebproof_box:N \l__ebproof_a_box } }
  \hbox_set:cn { \__ebproof_box:N \l__ebproof_a_box } {
    $ #1 \tex_vrule:D
      height \box_ht:N \l_tmpa_box depth \box_dp:N \l_tmpa_box width 0pt
    \tex_right:D . $
  }
  \__ebproof_shift_x:Nn \l__ebproof_a_box
    { \box_wd:c { \__ebproof_box:N \l__ebproof_a_box } }
  \hbox_set:cn { \__ebproof_box:N \l__ebproof_a_box } {
    \hbox_unpack:c { \__ebproof_box:N \l__ebproof_a_box }
    $ \tex_left:D . \box_use:N \l_tmpa_box #2 $
  }
  \hbox_set:cn { \__ebproof_box:N \l__ebproof_a_box }
    { \box_move_down:nn { \l_tmpa_dim }
        { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } }
  \__ebproof_push:N \l__ebproof_a_box
  \group_end:
}
\__ebproof_new_statement:nnn { overlay } { } {
  \group_begin:
  \__ebproof_pop:N \l__ebproof_a_box
  \__ebproof_pop:N \l__ebproof_b_box
  \__ebproof_overlay:NN \l__ebproof_a_box \l__ebproof_b_box
  \__ebproof_push:N \l__ebproof_a_box
  \group_end:
}
\__ebproof_new_deprecated_statement:nnnn { Alter } { m }
  { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } }
\__ebproof_new_deprecated_statement:nnnn { Delims } { }
  { use~\token_to_str:c{delims}~instead } { \ebproofdelims }
\__ebproof_new_deprecated_statement:nnnn { Ellipsis } { }
  { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis }
\__ebproof_new_deprecated_statement:nnnn { Hypo } { }
  { use~\token_to_str:c{hypo}~instead } { \ebproofhypo }
\__ebproof_new_deprecated_statement:nnnn { Infer } { }
  { use~\token_to_str:c{infer}~instead } { \ebproofinfer }
\__ebproof_clear_stack:
\tl_new:N \l__ebproof_start_level_tl
\NewDocumentEnvironment { prooftree } { s O{} } {
  \group_align_safe_begin:
  \keys_set_known:nnN { ebproof / proof~style } { #2 } \l_tmpa_tl
  \keys_set:nV { ebproof } \l_tmpa_tl
  \tl_set:Nx \l__ebproof_start_level_tl { \int_use:N \g__ebproof_level_int }
  \vbox_set:Nw \l_tmpa_box
  \__ebproof_setup_statements:
} {
  \vbox_set_end:
  \__ebproof_pop:N \l__ebproof_a_box
  \int_compare:nNnF { \g__ebproof_level_int } = { \tl_use:N \l__ebproof_start_level_tl } {
    \PackageError{ebproof}{Malformed~proof~tree}{
      Some~hypotheses~were~declared~but~not~used~in~this~tree.}
  }
  \IfBooleanTF { #1 } {
    \[ \box_use:c { \__ebproof_box:N \l__ebproof_a_box } \]
    \ignorespacesafterend
  } {
    \hbox_unpack:N \c_empty_box
    \bool_if:NTF \l__ebproof_center_bool {
      \hbox:n { $ \tex_vcenter:D { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } $ }
    } {
      \box_use:c { \__ebproof_box:N \l__ebproof_a_box }
    }
  }
  \group_align_safe_end:
}
\cs_new:cpn { prooftree* } { \prooftree* }
\cs_new:cpn { endprooftree* } { \endprooftree }
\endinput
%%
%% End of file `ebproof.sty'.
