Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/0a35321d3127144d621792f7cdd8c3fc]
tp : type.
tp/unit : tp.
tp/arrow : tp -> tp -> tp.
exp : type.
exp/unit : exp.
exp/lam : tp -> (exp -> exp) -> exp.
exp/app : exp -> exp -> exp.
of : exp -> tp -> type.
of/unit : of exp/unit tp/unit.
of/lam :
   {T1:tp} {E:exp -> exp} {T2:tp}
      ({x:exp} of x T1 -> of (E x) T2)
         -> of (exp/lam T1 ([x:exp] E x)) (tp/arrow T1 T2).
of/app :
   {E1:exp} {T1:tp} {T2:tp} {E2:exp}
      of E1 (tp/arrow T1 T2) -> of E2 T1 -> of (exp/app E1 E2) T2.
val : exp -> type.
val/unit : val exp/unit.
val/lam : {X1:tp} {X2:exp -> exp} val (exp/lam X1 ([x:exp] X2 x)).
step : exp -> exp -> type.
step/app-1 :
   {E1:exp} {E1':exp} {E2:exp}
      step E1 E1' -> step (exp/app E1 E2) (exp/app E1' E2).
step/app-2 :
   {E1:exp} {E2:exp} {E2':exp}
      val E1 -> step E2 E2' -> step (exp/app E1 E2) (exp/app E1 E2').
step/app-beta :
   {E2:exp} {X1:tp} {E:exp -> exp}
      val E2 -> step (exp/app (exp/lam X1 ([x:exp] E x)) E2) (E E2).
notstuck : exp -> type.
notstuck/val : {E:exp} val E -> notstuck E.
notstuck/step : {E:exp} {E':exp} step E E' -> notstuck E.
tp-sub : tp -> tp -> type.
tp-sub/unit : tp-sub tp/unit tp/unit.
tp-sub/arrow :
   {T3:tp} {T1:tp} {T2:tp} {T4:tp}
      tp-sub T3 T1 -> tp-sub T2 T4 -> tp-sub (tp/arrow T1 T2) (tp/arrow T3 T4).
of/sub : {E1:exp} {T1:tp} {T2:tp} of E1 T1 -> tp-sub T1 T2 -> of E1 T2.
seq-exp : exp -> exp -> type.
seq-exp/i : {E:exp} seq-exp E E.
cfl-tp/arrow :
   {E1:exp} {X1:tp} {X2:tp} {T:tp} {E:exp -> exp}
      val E1 -> of E1 (tp/arrow X1 X2) -> seq-exp E1 (exp/lam T ([x:exp] E x))
         -> type.
%mode +{E1:exp} +{X1:tp} +{X2:tp} -{T:tp} -{E:exp -> exp} +{D1:val E1}
   +{D2:of E1 (tp/arrow X1 X2)} -{D3:seq-exp E1 (exp/lam T ([x:exp] E x))}
   (cfl-tp/arrow D1 D2 D3).
- :
   {X1:tp} {X2:exp -> exp} {X3:tp} {X4:{x:exp} of x X1 -> of (X2 x) X3}
      cfl-tp/arrow val/lam (of/lam ([x:exp] [x1:of x X1] X4 x x1)) seq-exp/i.
- :
   {X1:exp} {X2:tp} {X3:tp} {X4:tp} {X5:exp -> exp} {V:val X1}
      {D1:of X1 (tp/arrow X2 X3)} {DQ:seq-exp X1 (exp/lam X4 ([x:exp] X5 x))}
      {X6:tp} {X7:tp} {X8:tp-sub X6 X2} {X9:tp-sub X3 X7}
      cfl-tp/arrow V D1 DQ -> cfl-tp/arrow V (of/sub D1 (tp-sub/arrow X8 X9)) DQ.
%worlds () (cfl-tp/arrow _ _ _).
%total D1 (cfl-tp/arrow _ D1 _).
progress-exp/app-beta :
   {E1:exp} {T:tp} {E:exp -> exp} {E2:exp}
      seq-exp E1 (exp/lam T ([x:exp] E x)) -> val E2 -> notstuck (exp/app E1 E2)
         -> type.
%mode +{E1:exp} +{T:tp} +{E:exp -> exp} +{E2:exp}
   +{D1:seq-exp E1 (exp/lam T ([x:exp] E x))} +{D2:val E2}
   -{D3:notstuck (exp/app E1 E2)} (progress-exp/app-beta D1 D2 D3).
- :
   {X1:tp} {X2:exp -> exp} {X3:exp} {V:val X3}
      progress-exp/app-beta seq-exp/i V (notstuck/step (step/app-beta V)).
%worlds () (progress-exp/app-beta _ _ _).
%total {} (progress-exp/app-beta _ _ _).
progress-exp/app :
   {E1:exp} {E2:exp} {X1:tp} {X2:tp}
      notstuck E1 -> notstuck E2 -> of E1 (tp/arrow X1 X2)
         -> notstuck (exp/app E1 E2) -> type.
%mode +{E1:exp} +{E2:exp} +{X1:tp} +{X2:tp} +{D1:notstuck E1} +{D2:notstuck E2}
   +{D3:of E1 (tp/arrow X1 X2)} -{D4:notstuck (exp/app E1 E2)}
   (progress-exp/app D1 D2 D3 D4).
- :
   {X1:exp} {X2:exp} {X3:tp} {X4:tp} {X5:exp} {S:step X1 X5} {X6:notstuck X2}
      {X7:of X1 (tp/arrow X3 X4)}
      progress-exp/app (notstuck/step S) X6 X7 (notstuck/step (step/app-1 S)).
- :
   {X1:exp} {X2:exp} {X3:tp} {X4:tp} {V:val X1} {X5:exp} {S:step X2 X5}
      {X6:of X1 (tp/arrow X3 X4)}
      progress-exp/app (notstuck/val V) (notstuck/step S) X6
         (notstuck/step (step/app-2 V S)).
- :
   {X1:exp} {X2:tp} {X3:exp -> exp} {X4:exp}
      {DQ:seq-exp X1 (exp/lam X2 ([x:exp] X3 x))} {V2:val X4}
      {NS:notstuck (exp/app X1 X4)} {X5:tp} {X6:tp} {V:val X1}
      {D1:of X1 (tp/arrow X5 X6)}
      progress-exp/app-beta DQ V2 NS -> cfl-tp/arrow V D1 DQ
         -> progress-exp/app (notstuck/val V) (notstuck/val V2) D1 NS.
%worlds () (progress-exp/app _ _ _ _).
%total {} (progress-exp/app _ _ _ _).
progress : {E:exp} {T:tp} of E T -> notstuck E -> type.
%mode +{E:exp} +{T:tp} +{D1:of E T} -{D2:notstuck E} (progress D1 D2).
- : progress of/unit (notstuck/val val/unit).
- :
   {X1:tp} {X2:exp -> exp} {X3:tp} {X4:{x:exp} of x X1 -> of (X2 x) X3}
      progress (of/lam ([x:exp] [x1:of x X1] X4 x x1)) (notstuck/val val/lam).
- :
   {X1:exp} {X2:exp} {X3:tp} {X4:tp} {NS1:notstuck X1} {NS2:notstuck X2}
      {D1:of X1 (tp/arrow X3 X4)} {NS:notstuck (exp/app X1 X2)} {D2:of X2 X3}
      progress-exp/app NS1 NS2 D1 NS -> progress D2 NS2 -> progress D1 NS1
         -> progress (of/app D1 D2) NS.
- :
   {X1:exp} {X2:tp} {D1:of X1 X2} {NS:notstuck X1} {X3:tp} {X4:tp-sub X2 X3}
      progress D1 NS -> progress (of/sub D1 X4) NS.
%worlds () (progress _ _).
%total D1 (progress D1 _).
[Closing file /home/www/twelf/hcode/0a35321d3127144d621792f7cdd8c3fc]
%% OK %%