for the $\l$-calculus is the $\b$-rule.

    $$(\l x. M \; N) \tr_{\b} M[x:=N]$$

2.  The reduction rules for the $\l\m$-calculus are the $\b$-rule and the $\m$-rule

    $$(\mu \a. M \; N) \tr_{\m}  \mu \a. M[(\a \;
      L) := (\a \; (L \; N))]$$

3.  The reduction rules for the $\l\m^{\f\et\ou}$-calculus are those of the $\l\m$-calculus together with the following rules

    $(\< M_1,M_2 \> \; \pi_i) \tr M_i$

    $(\o_i M\; [x_1. N_1 ,x_2. N_2]) \tr N_i[x_i:=M]$

    $(M \; [x_1.N_1 , x_2.N_2] \; \ep)
    \tr (M \; [x_1.(N_1 \; \ep) , x_2.(N_2 \; \ep)])$

    $(\mu \a. M \; \ep) \tr \mu \a. M[(\a \; N):= (\a \; (N \; \ep))]$

Let ${\cal A}$ be a set of atomic constants.

1.  The set ${\cal T}$ of types is defined by the following grammar

    $${\cal T} ::= \; {\cal A}\cup \{\bot\} \; \mid
    {\cal T} \f {\cal T}$$

2.  The set ${\cal T}'$ of types is defined by the following grammar

    $${\cal T}' ::= \; {\cal A}\cup \{\bot\} \; \mid \;   {\cal T}' \f
    {\cal T}' \; \mid \; {\cal T}' \et {\cal T}' \; \mid \; {\cal T}'
    \ou {\cal T}'$$

As usual $\neg A$ is an abbreviation for $A \f \bot$.

1.  