%%% Ordinary reduction for the untyped lambda-calculus
%%% Author: Frank Pfenning

--> : term -> term -> type.  %infix none 10 -->.
			     %name --> R.

beta1 :   (app (lam M1) M2) --> M1 M2.

lm1   :       ({x:term} M x --> M' x)
      ->            (lam M) --> (lam M').

apl1  :              M1 --> M1'
      ->    (app M1 M2) --> (app M1' M2).

apr1  :              M2 --> M2'
      ->    (app M1 M2) --> (app M1 M2').

% Multi-step reduction

-->* : term -> term -> type.  %infix none 10 -->*.
			      %name -->* R*.

id1   :    M -->* M.

% step1 :    M' --> M'' ->  M  -->* M' -> M  -->* M''.
% Bug here:
% Fri Dec 14 18:37:26 2001 -fp !!!
step1 : M --> M' -> M' -->* M'' -> M -->* M''.

% Conversion

<-> : term -> term -> type.  %infix none 10 <->.
			     %name <-> C.

refl :    M  <-> M.

sym  :    M  <-> M'
   <-     M' <-> M.

trans:    M  <-> M''
   <-     M  <-> M'
   <-     M' <-> M''.


red  :    M  <->  M'
   <-     M  -->* M'.