1:- module(bussproofs, []).    2:- reexport(library(mathml)).    3
    4:- multifile mlx/3. 
    5
    6% Render in MathML
    7%
    8%      <mpadded height="+.5em" width="+.5em" voffset="-.15em" semantics="bspr_prooflabel:right">
    9%        <mstyle displaystyle="false" scriptlevel="0">
   10%          <mrow data-mjx-texclass="ORD">
   11%            <mstyle mathsize="0.7em">
   12%              <mrow data-mjx-texclass="ORD">
   13%                <mi>R</mi>
   14%                <mo accent="false" stretchy="false">&#x2192;</mo>
   15%              </mrow>
   16%            </mstyle>
   17%          </mrow>
   18%        </mstyle>
   19%      </mpadded>
   20%
   21% math_hook(rcond(A, B), [frac(B, A), '%->%'('R', xx)]).
   22
   23% Render in MathML
   24mathml:mlx(proof(Denominator, Numerator), M, Flags) :-
   25    X1 =.. ['###1', '##'(Numerator)],
   26    X =.. ['###2', '##'(X1), '##1'(Denominator)],
   27    mathml:ml(proof_tree(X), M, Flags).
   28
   29mathml:mlx(proof(Denominator, Numerator1, Numerator2), M, Flags) :-
   30    X1 =.. ['###1', '##'(Numerator1, '', Numerator2)],
   31    X =.. ['###2', '##'(X1), '##1'(Denominator)],
   32    mathml:ml(proof_tree(X), M, Flags).
   33
   34mathml:mlx(format_operator(Op), R, Flags) :-
   35    mathml:ml(Op, R1, Flags),
   36    mathml:ml(size(R1, '0.7em'), R2, Flags),
   37    mathml:ml(mstyle_right(R2), R3, Flags),
   38    mathml:ml(mpadded_right(R3), R, Flags).
   39
   40mathml:mlx(size(A, Size), M, _Flags) :-
   41    M = mrow([mstyle([mathsize(Size)], A)]).
   42
   43mathml:mlx(mstyle_right(A), M, _Flags) :-
   44    M = mstyle([displaystyle('false'), scriptlevel('0')], A).
   45
   46mathml:mlx(mpadded_right(A), M, _Flags) :-
   47    M = mpadded([height('.5em'), width('.5em'), voffset('.9em'), semantics('bspr_prooflabel:right')], A).
   48
   49mathml:mlx(rbicond(A, B), M, Flags) :-
   50    mathml:ml(proof(A, B), F, Flags),
   51    mathml:ml(format_operator('%<->%'('R', '')), R, Flags),
   52    M = mrow([F, R]).  
   53
   54mathml:mlx(rbicond(A, B, C), M, Flags) :-
   55    mathml:ml(proof(A, B, C), F, Flags),
   56    mathml:ml(format_operator('%<->%'('R', '')), R, Flags),
   57    M = mrow([F, R]).  
   58
   59mathml:mlx(rcond(A, B), M, Flags) :-
   60    mathml:ml(proof(A, B), F, Flags),
   61    mathml:ml(format_operator('%->%'('R', '')), R, Flags),
   62    M = mrow([F, R]).  
   63
   64mathml:mlx(rcond(A, B, C), M, Flags) :-
   65    mathml:ml(proof(A, B, C), F, Flags),
   66    mathml:ml(format_operator('%->%'('R', '')), R, Flags),
   67    M = mrow([F, R]).  
   68
   69mathml:mlx(rand(A, B), M, Flags) :-
   70    mathml:ml(proof(A, B), F, Flags),
   71    mathml:ml(format_operator(and('R', '')), R, Flags),
   72    M = mrow([F, R]). 
   73
   74mathml:mlx(rand(A, B, C), M, Flags) :-
   75    mathml:ml(proof(A, B, C), F, Flags),
   76    mathml:ml(format_operator(and('R', '')), R, Flags),
   77    M = mrow([F, R]). 
   78    
   79mathml:mlx(ror(A, B), M, Flags) :-
   80    mathml:ml(proof(A, B), F, Flags),
   81    mathml:ml(format_operator(or('R', '')), R, Flags),
   82    M = mrow([F, R]). 
   83
   84mathml:mlx(ror(A, B, C), M, Flags) :-
   85    mathml:ml(proof(A, B, C), F, Flags),
   86    mathml:ml(format_operator(or('R', '')), R, Flags),
   87    M = mrow([F, R]). 
   88
   89mathml:mlx(rneg(A, B), M, Flags) :-
   90    mathml:ml(proof(A, B), F, Flags),
   91    mathml:ml(format_operator(!('R','')), R, Flags),
   92    M = mrow([F, R]). 
   93
   94mathml:mlx(rneg(A, B, C), M, Flags) :-
   95    mathml:ml(proof(A, B, C), F, Flags),
   96    mathml:ml(format_operator(!('R','')), R, Flags),
   97    M = mrow([F, R]). 
   98
   99mathml:mlx(lbicond(A, B), M, Flags) :-
  100    mathml:ml(proof(A, B), F, Flags),
  101    mathml:ml(format_operator('%<->%'('L', '')), R, Flags),
  102    M = mrow([F, R]). 
  103
  104mathml:mlx(lbicond(A, B, C), M, Flags) :-
  105    mathml:ml(proof(A, B, C), F, Flags),
  106    mathml:ml(format_operator('%<->%'('L', '')), R, Flags),
  107    M = mrow([F, R]).  
  108
  109mathml:mlx(lcond(A, B), M, Flags) :-
  110    mathml:ml(proof(A, B), F, Flags),
  111    mathml:ml(format_operator('%->%'('L', '')), R, Flags),
  112    M = mrow([F, R]).  
  113
  114mathml:mlx(lcond(A, B, C), M, Flags) :-
  115    mathml:ml(proof(A, B, C), F, Flags),
  116    mathml:ml(format_operator('%->%'('L', '')), R, Flags),
  117    M = mrow([F, R]).  
  118
  119mathml:mlx(land(A, B), M, Flags) :-
  120    mathml:ml(proof(A, B), F, Flags),
  121    mathml:ml(format_operator('&'('L', '')), R, Flags),
  122    M = mrow([F, R]).  
  123
  124mathml:mlx(land(A, B, C), M, Flags) :-
  125    mathml:ml(proof(A, B, C), F, Flags),
  126    mathml:ml(format_operator('&'('L', '')), R, Flags),
  127    M = mrow([F, R]).  
  128
  129mathml:mlx(lor(A, B), M, Flags) :-
  130    mathml:ml(proof(A, B), F, Flags),
  131    mathml:ml(format_operator(or('L', '')), R, Flags),
  132    M = mrow([F, R]). 
  133
  134mathml:mlx(lor(A, B, C), M, Flags) :-
  135    mathml:ml(proof(A, B, C), F, Flags),
  136    mathml:ml(format_operator(or('L', '')), R, Flags),
  137    M = mrow([F, R]). 
  138
  139mathml:mlx(lneg(A, B), M, Flags) :-
  140    mathml:ml(proof(A, B), F, Flags),
  141    mathml:ml(format_operator(!('L', '')), R, Flags),
  142    M = mrow([F, R]). 
  143
  144mathml:mlx(lneg(A, B, C), M, Flags) :-
  145    mathml:ml(proof(A, B, C), F, Flags),
  146    mathml:ml(format_operator(!('L', '')), R, Flags),
  147    M = mrow([F, R]). 
  148
  149mathml:mlx(ax(A, B), M, Flags) :-
  150    mathml:ml(proof(A, B), F, Flags),
  151    mathml:ml(format_operator(ident('Ax.')), R, [mathvariant(italic)]),
  152    M = mrow([F, R]).
  153
  154mathml:mlx(asq(A, B), M, Flags) :-
  155    mathml:ml(proof(A, B), F, Flags),
  156    mathml:ml(format_operator(ident('Asq.')), R, [mathvariant(italic)]),
  157    M = mrow([mathcolor(red)], [F, R])