es5

"ri" sta per rightmost-innermost


Axiom
       (\x.M)N -->_ri M[N/x]  se M ed N sono in forma normale

Rules  

         N -->_ri N'           M -->_ri M'  N in normal form
       ---------------       --------------------------------
        MN -->_ri MN'                  MN -->_ri M'N

                         M -->_ri M'
                    -------------------
                     \x.M -->_ri \x.M'