Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/89ec5b6cac17b52fdae6f648f504f136]
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.
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:tp} {X2:exp -> exp} {X3:exp} {X4:tp} {V2:val X3}
      {X5:{x:exp} of x X1 -> of (X2 x) X4}
      progress-exp/app (notstuck/val val/lam) (notstuck/val V2)
         (of/lam ([x:exp] [x1:of x X1] X5 x x1))
         (notstuck/step (step/app-beta V2)).
%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.
%worlds () (progress _ _).
%total D1 (progress D1 _).
[Closing file /home/www/twelfwiki/code/89ec5b6cac17b52fdae6f648f504f136]
%% OK %%