Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/6a50f3536ed15e3e596f58c09ed7b919]
trm : type.
lam : (trm -> trm) -> trm.
app : trm -> trm -> trm.
=> : trm -> trm -> type.
%infix none 10 =>.
=>/beta :
   {N:trm} {N':trm} {M:trm -> trm} {M':trm -> trm}
      N => N' -> ({x:trm} x => x -> M x => M' x)
         -> app (lam ([x:trm] M x)) N => M' N'.
=>/app :
   {M:trm} {M':trm} {N:trm} {N':trm} M => M' -> N => N' -> app M N => app M' N'.
=>/lam :
   {M:trm -> trm} {M':trm -> trm}
      ({x:trm} x => x -> M x => M' x) -> lam ([x:trm] M x) => lam ([x:trm] M' x).
%block =>b : block {x:trm} {=>/x:x => x}.
%worlds (=>b) (=> _ _).
=> : trm -> trm -> type.
%infix none 10 =>.
=>/refl : {M:trm} M => M.
=>/beta :
   {N:trm} {N':trm} {M:trm -> trm} {M':trm -> trm}
      N => N' -> ({x:trm} M x => M' x) -> app (lam ([x:trm] M x)) N => M' N'.
=>/app :
   {M:trm} {M':trm} {N:trm} {N':trm} M => M' -> N => N' -> app M N => app M' N'.
=>/lam :
   {M:trm -> trm} {M':trm -> trm}
      ({x:trm} M x => M' x) -> lam ([x:trm] M x) => lam ([x:trm] M' x).
%block trmb : block {x:trm}.
%worlds (trmb) (=> _ _).
notlam : trm -> type.
notlam/app : {X1:trm} {X2:trm} notlam (app X1 X2).
%block nlb : block {x:trm} {nlx:notlam x}.
%worlds (nlb) (notlam _).
==> : trm -> trm -> type.
%infix none 10 ==>.
==>/beta :
   {N:trm} {N':trm} {M:trm -> trm} {M':trm -> trm}
      N ==> N' -> ({x:trm} notlam x -> x ==> x -> M x ==> M' x)
         -> app (lam ([x:trm] M x)) N ==> M' N'.
==>/app :
   {M:trm} {M':trm} {N:trm} {N':trm}
      notlam M -> M ==> M' -> N ==> N' -> app M N ==> app M' N'.
==>/lam :
   {M:trm -> trm} {M':trm -> trm}
      ({x:trm} notlam x -> x ==> x -> M x ==> M' x)
         -> lam ([x:trm] M x) ==> lam ([x:trm] M' x).
%block ==>b : block {x:trm} {nlx:notlam x} {==>/x:x ==> x}.
%worlds (==>b) (==> _ _).
[Closing file /home/www/twelf/hcode/6a50f3536ed15e3e596f58c09ed7b919]
%% OK %%