jon-ebproof.sty

\RequirePackage{expl3}
\RequirePackage{xparse}
\RequirePackage{ebproof}

%% This package is an extension and modification of code by Emmanuel Beffara

\ExplSyntaxOn

\cs_new_protected:Npn \__formulas_split: {
  $\hskip 1em plus 1fil$\displaystyle
}

\cs_new_protected:Npn \__formulas_break: {
  $\penalty-10000$\displaystyle
}

\NewDocumentEnvironment{formulas}{}{
  \center
  \cs_set_eq:NN \split \__formulas_split:
  \cs_set_eq:NN \break \__formulas_break:
  \lineskip=2ex\relax
  $\displaystyle
}{$
  \endcenter
}

\seq_new:N \l_matrix_rows
\seq_new:N \l_matrix_cells
\cs_new_protected:Npn \jms_count_columns:Nn #1 #2{
  \int_set:Nn #1 {1}
  \seq_set_split:Nnn \l_matrix_rows {\\} {#2}
  \seq_map_inline:Nn \l_matrix_rows {
    \seq_set_split:Nnn \l_matrix_cells {&} {##1}
    \int_set:Nn #1 {
      \int_max:nn {\seq_count:N \l_matrix_cells} {#1}
    }
  }
}

\int_new:N \l_matrix_num_cols
\cs_new_protected:Npn \jms_auto_array:n #1 {
  \jms_count_columns:Nn \l_matrix_num_cols {#1}
  \begin{array}{*{\l_matrix_num_cols}{l}}
    #1
  \end{array}
}

\NewDocumentCommand\inferrule{omm}{
  \vbox{
    \IfValueT{#1}{\hbox{\textsc{#1}}\vspace{-.5em}}
    \hbox{
      \begin{prooftree}[center=false]
        \matrix{#2}
        \infer1{#3}
      \end{prooftree}
    }
  }
}

\ebproof_new_statement:nnn { matrix } { O{} m } {
  \group_begin:
  \ebproof_restore_statements:
  \keys_set:nn { ebproof } { #1 }
  \ebproof_push_statement:n {
    {\jms_auto_array:n { #2 }}
  }
  \group_end:
}


\ExplSyntaxOff