23 \newcommand{\rderssimp}[2]{#1 \backslash_{rsimp} #2}

    23 \newcommand{\rderssimp}[2]{#1 \backslash_{rsimp} #2}

    24 \def\derssimp{\textit{ders}\_\textit{simp}}

    24 \def\derssimp{\textit{ders}\_\textit{simp}}

    25 \def\rders{\textit{rders}}

    25 \def\rders{\textit{rders}}

    26 \newcommand{\bders}[2]{#1 \backslash #2}

    26 \newcommand{\bders}[2]{#1 \backslash #2}

    27 \newcommand{\bsimp}[1]{\textit{bsimp}(#1)}

    27 \newcommand{\bsimp}[1]{\textit{bsimp}(#1)}

    28 \newcommand{\rsimp}[1]{\textit{rsimp}\; #1}

    29 \newcommand{\rsimp}[1]{\textit{rsimp}\; #1}

    29 \newcommand{\sflataux}[1]{\llparenthesis #1 \rrparenthesis'}

    30 \newcommand{\sflataux}[1]{\llparenthesis #1 \rrparenthesis'}

    30 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%

    31 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%

    31 \newcommand{\denote}{\stackrel{\mbox{\scriptsize denote}}{=}}%

    32 \newcommand{\denote}{\stackrel{\mbox{\scriptsize denote}}{=}}%

    32 \newcommand{\ZERO}{\mbox{\bf 0}}

    33 \newcommand{\ZERO}{\mbox{\bf 0}}

   117 \def\map{\mathit{map}}

   118 \def\map{\mathit{map}}

   118 \def\distinct{\mathit{distinct}}

   119 \def\distinct{\mathit{distinct}}

   119 \def\blexersimp{\mathit{blexer}\_\mathit{simp}}

   120 \def\blexersimp{\mathit{blexer}\_\mathit{simp}}

   120 \def\blexerStrong{\textit{blexerStrong}}

   121 \def\blexerStrong{\textit{blexerStrong}}

   121 \def\bsimpStrong{\textit{bsimpStrong}}

   122 \def\bsimpStrong{\textit{bsimpStrong}}

   123 \newcommand{\bdersStrong}[2]{#1 \backslash_{bsimpStrongs} #2}

   124 \newcommand{\bdersStrong}[2]{#1 \backslash_{bsimpStrongs} #2}

   124 

   125 

   125 \def\map{\textit{map}}

   126 \def\map{\textit{map}}

   126 \def\rrexp{\textit{rrexp}}

   127 \def\rrexp{\textit{rrexp}}

   127 \newcommand\rnullable[1]{\textit{rnullable} \; #1 }

   128 \newcommand\rnullable[1]{\textit{rnullable} \; #1 }