%%% 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*.

%tabled -->*.

id1   :    M -->* M.

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


% Conversion

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

%tabled <->.

refl :    M  <-> M.

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

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


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