\section{Applications}


Consider the following program:
\[
\begin{array}{lll}
betarx & : & isredx(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ F )\\
etarx & : & isredx(lam(\lamb{x^u}{exp} app\ M\ x^u))
\end{array}\]

We can compute
$\mmnot\{(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F),lam(\lamb{x^u}{exp} app\ M\ x^u)\}
$ by intersecting $\mmnot(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F)$ and $ \mmnot(lam(\lamb{x^{u}}{exp} app\ (M\ x^{0}) \x^{1} ))$ \ie 

$
%\mmnot(app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)= 
\{ lam\ (\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H_{3}\}$
$\mbc $
\{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H,
\{ lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ H_4\ H_5)), \\
lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u)),
app\ H_1\ H_2,
 lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ y^u) )\}
\\
=
 \{ 
 lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'\ x^{u}),  
  lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ H_4\ x^{u} H_5\ x^{u})),
lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u))\\
  lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ y^u) ),
  app\ ( app\ H_1\ H_2) H_{3}\}$

Yielding the program: 

\[
\begin{array}{lll}
nb1 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'\ x^{u}))\\
nb2 & : & non\_isredx( lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ H_4\ x^{u} H_5\ x^{u}))\\
nb3 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u)))\\
nb4 & : & non\_isredx(lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ 
y^u) ))\\
nb5 & : & non\_isredx( app\ (app\ H_{1}\ H_{2})\ H_{3}\  )
\end{array}\]