Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/82c023e77a487aea9a02c9571fa400ed]
ty : type.
ty/nat : ty.
ty/arrow : ty -> ty -> ty.
ty/mayraise : ty -> ty.
ty/exn : ty = ty/nat.
eqty : ty -> ty -> type.
eqty/refl : {T:ty} eqty T T.
tm : type.
tm/lam : ty -> (tm -> tm) -> tm.
tm/app : tm -> tm -> tm.
tm/z : tm.
tm/s : tm -> tm.
tm/if : tm -> tm -> (tm -> tm) -> tm.
tm/fix : ty -> (tm -> tm) -> tm.
tm/raise : tm -> tm.
tm/handle : tm -> (tm -> tm) -> tm.
tm/susp : tm -> tm.
tm/unsusp : tm -> tm.
tm/let : tm -> ty -> (tm -> tm) -> tm
   = [e:tm] [t:ty] [f:tm -> tm] tm/app (tm/lam t ([x:tm] f x)) e.
of : tm -> ty -> type.
of* : tm -> ty -> type.
of*/weaken : {E:tm} {T:ty} of E T -> of* E T.
of/lam :
   {T:ty} {E:tm -> tm} {T':ty}
      ({x:tm} of x T -> of (E x) T')
         -> of (tm/lam T ([x:tm] E x)) (ty/arrow T T').
of/app :
   {E1:tm} {T:ty} {T':ty} {E2:tm}
      of E1 (ty/arrow T T') -> of E2 T -> of (tm/app E1 E2) T'.
of/z : of tm/z ty/nat.
of/s : {E:tm} of E ty/nat -> of (tm/s E) ty/nat.
of/if :
   {E:tm} {E1:tm} {T:ty} {E2:tm -> tm}
      of E ty/nat -> of E1 T -> ({x:tm} of x ty/nat -> of (E2 x) T)
         -> of (tm/if E E1 ([x:tm] E2 x)) T.
of/fix :
   {T:ty} {E:tm -> tm}
      ({x:tm} of x T -> of (E x) T) -> of (tm/fix T ([x:tm] E x)) T.
of/handle :
   {E:tm} {T:ty} {E':tm -> tm}
      of* E T -> ({x:tm} of x ty/exn -> of (E' x) T)
         -> of (tm/handle E ([x:tm] E' x)) T.
of/susp : {E:tm} {T:ty} of* E T -> of (tm/susp E) (ty/mayraise T).
of*/app :
   {E1:tm} {T:ty} {T':ty} {E2:tm}
      of* E1 (ty/arrow T T') -> of* E2 T -> of* (tm/app E1 E2) T'.
of*/s : {E:tm} of* E ty/nat -> of* (tm/s E) ty/nat.
of*/if :
   {E:tm} {E1:tm} {T:ty} {E2:tm -> tm}
      of* E ty/nat -> of* E1 T -> ({x:tm} of x ty/nat -> of* (E2 x) T)
         -> of* (tm/if E E1 ([x:tm] E2 x)) T.
of*/raise : {E:tm} {T:ty} of* E ty/exn -> of* (tm/raise E) T.
of*/handle :
   {E:tm} {T:ty} {E':tm -> tm}
      of* E T -> ({x:tm} of x ty/exn -> of* (E' x) T)
         -> of* (tm/handle E ([x:tm] E' x)) T.
of*/unsusp : {E:tm} {T:ty} of* E (ty/mayraise T) -> of* (tm/unsusp E) T.
v : tm -> type.
v/lam : {T:ty} {E:tm -> tm} v (tm/lam T ([x:tm] E x)).
v/z : v tm/z.
v/s : {E:tm} v E -> v (tm/s E).
v/susp : {E:tm} v (tm/susp E).
step : tm -> tm -> type.
step/app1 :
   {E1:tm} {E1':tm} {E2:tm} step E1 E1' -> step (tm/app E1 E2) (tm/app E1' E2).
step/app1x : {E:tm} {X1:tm} v E -> step (tm/app (tm/raise E) X1) (tm/raise E).
step/app2 :
   {E1:tm} {E2:tm} {E2':tm}
      v E1 -> step E2 E2' -> step (tm/app E1 E2) (tm/app E1 E2').
step/app2x :
   {E:tm} {E1:tm} v E -> v E1 -> step (tm/app E1 (tm/raise E)) (tm/raise E).
step/appr :
   {E2:tm} {T:ty} {E:tm -> tm}
      v E2 -> step (tm/app (tm/lam T ([x:tm] E x)) E2) (E E2).
step/s : {E:tm} {E':tm} step E E' -> step (tm/s E) (tm/s E').
step/sx : {E:tm} v E -> step (tm/s (tm/raise E)) (tm/raise E).
step/if :
   {E:tm} {E':tm} {E1:tm} {E2:tm -> tm}
      step E E' -> step (tm/if E E1 ([x:tm] E2 x)) (tm/if E' E1 ([x:tm] E2 x)).
step/ifz : {E1:tm} {E2:tm -> tm} step (tm/if tm/z E1 ([x:tm] E2 x)) E1.
step/ifs :
   {E:tm} {E1:tm} {E2:tm -> tm}
      v E -> step (tm/if (tm/s E) E1 ([x:tm] E2 x)) (E2 E).
step/ifx :
   {E:tm} {E1:tm} {E2:tm -> tm}
      v E -> step (tm/if (tm/raise E) E1 ([x:tm] E2 x)) (tm/raise E).
step/fix :
   {T:ty} {E:tm -> tm} step (tm/fix T ([x:tm] E x)) (E (tm/fix T ([x:tm] E x))).
step/raise : {E:tm} {E':tm} step E E' -> step (tm/raise E) (tm/raise E').
step/raisex : {E:tm} v E -> step (tm/raise (tm/raise E)) (tm/raise E).
step/handle :
   {E1:tm} {E1':tm} {E2:tm -> tm}
      step E1 E1'
         -> step (tm/handle E1 ([x:tm] E2 x)) (tm/handle E1' ([x:tm] E2 x)).
step/handler : {E:tm} {X1:tm -> tm} v E -> step (tm/handle E ([x:tm] X1 x)) E.
step/handlex :
   {E:tm} {E2:tm -> tm}
      v E -> step (tm/handle (tm/raise E) ([x:tm] E2 x)) (E2 E).
step/unsusp : {E:tm} {E':tm} step E E' -> step (tm/unsusp E) (tm/unsusp E').
step/unsuspr : {E:tm} step (tm/unsusp (tm/susp E)) E.
step/unsuspx : {E:tm} v E -> step (tm/unsusp (tm/raise E)) (tm/raise E).
nstuck : tm -> type.
nstuck/step : {E:tm} {E':tm} step E E' -> nstuck E.
nstuck/value : {E:tm} v E -> nstuck E.
nstuck* : tm -> type.
nstuck*/step : {E:tm} {E':tm} step E E' -> nstuck* E.
nstuck*/value : {E:tm} v E -> nstuck* E.
nstuck*/raise : {E:tm} v E -> nstuck* (tm/raise E).
ns-weaken : {E:tm} nstuck E -> nstuck* E -> type.
- : {X1:tm} {X2:tm} {E:step X1 X2} ns-weaken (nstuck/step E) (nstuck*/step E).
- : {X1:tm} {V:v X1} ns-weaken (nstuck/value V) (nstuck*/value V).
%mode +{E:tm} +{A:nstuck E} -{B:nstuck* E} (ns-weaken A B).
%worlds () (ns-weaken _ _).
%total {} (ns-weaken _ _).
mobile : {E:tm} {T:ty} v E -> of* E T -> of E T -> type.
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {F:{x:tm} of x X1 -> of (X2 x) X3}
      mobile v/lam (of*/weaken (of/lam ([x:tm] [x1:of x X1] F x x1)))
         (of/lam ([x:tm] [x1:of x X1] F x x1)).
- : mobile v/z (of*/weaken of/z) of/z.
- :
   {X1:tm} {V:v X1} {S:of X1 ty/nat}
      mobile (v/s V) (of*/weaken (of/s S)) (of/s S).
- :
   {X1:tm} {V:v X1} {S:of* X1 ty/nat} {S':of X1 ty/nat}
      mobile V S S' -> mobile (v/s V) (of*/s S) (of/s S').
- :
   {X1:tm} {X2:ty} {T:of* X1 X2}
      mobile v/susp (of*/weaken (of/susp T)) (of/susp T).
%mode +{E:tm} +{T:ty} +{A:v E} +{B:of* E T} -{C:of E T} (mobile A B C).
%worlds () (mobile _ _ _).
%total T (mobile T _ _).
progress : {E:tm} {T:ty} of E T -> nstuck E -> type.
progress* : {E:tm} {T:ty} of* E T -> nstuck* E -> type.
%mode +{E:tm} +{T:ty} +{A:of E T} -{B:nstuck E} (progress A B).
%mode +{E:tm} +{T:ty} +{A:of* E T} -{B:nstuck* E} (progress* A B).
- :
   {X1:tm} {NS:nstuck X1} {NS*:nstuck* X1} {X2:ty} {T:of X1 X2}
      ns-weaken NS NS* -> progress T NS -> progress* (of*/weaken T) NS*.
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {X4:{x:tm} of x X1 -> of (X2 x) X3}
      progress (of/lam ([x:tm] [x1:of x X1] X4 x x1)) (nstuck/value v/lam).
p0 :
   {E:tm} {T1:ty} {T2:ty} {E':tm}
      of E (ty/arrow T1 T2) -> nstuck E -> nstuck E' -> nstuck (tm/app E E')
         -> type.
- :
   {X1:tm} {X2:ty} {X3:ty} {X4:tm} {X5:of X1 (ty/arrow X2 X3)} {X6:tm}
      {E:step X1 X6} {X7:nstuck X4}
      p0 X5 (nstuck/step E) X7 (nstuck/step (step/app1 E)).
- :
   {X1:tm} {X2:ty} {X3:ty} {X4:tm} {X5:of X1 (ty/arrow X2 X3)} {V:v X1} {X6:tm}
      {E:step X4 X6}
      p0 X5 (nstuck/value V) (nstuck/step E) (nstuck/step (step/app2 V E)).
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {X4:tm} {X5:{x:tm} of x X1 -> of (X2 x) X3}
      {X6:v (tm/lam X1 ([x:tm] X2 x))} {V:v X4}
      p0 (of/lam ([x:tm] [x1:of x X1] X5 x x1)) (nstuck/value X6)
         (nstuck/value V) (nstuck/step (step/appr V)).
%mode +{E:tm} +{T1:ty} +{T2:ty} +{E':tm} +{A:of E (ty/arrow T1 T2)} +{B:nstuck E}
   +{C:nstuck E'} -{D:nstuck (tm/app E E')} (p0 A B C D).
%worlds () (p0 _ _ _ _).
%total {} (p0 _ _ _ _).
- :
   {X1:tm} {X2:ty} {X3:ty} {X4:tm} {T1:of X1 (ty/arrow X2 X3)} {NS1:nstuck X1}
      {NS2:nstuck X4} {NS:nstuck (tm/app X1 X4)} {T2:of X4 X2}
      p0 T1 NS1 NS2 NS -> progress T2 NS2 -> progress T1 NS1
         -> progress (of/app T1 T2) NS.
- : progress of/z (nstuck/value v/z).
p1 : {E:tm} of E ty/nat -> nstuck E -> nstuck (tm/s E) -> type.
- :
   {X1:tm} {X2:of X1 ty/nat} {X3:tm} {E:step X1 X3}
      p1 X2 (nstuck/step E) (nstuck/step (step/s E)).
- :
   {X1:tm} {X2:of X1 ty/nat} {V:v X1}
      p1 X2 (nstuck/value V) (nstuck/value (v/s V)).
%mode +{E:tm} +{A:of E ty/nat} +{B:nstuck E} -{C:nstuck (tm/s E)} (p1 A B C).
%worlds () (p1 _ _ _).
%total {} (p1 _ _ _).
- :
   {X1:tm} {T:of X1 ty/nat} {NS1:nstuck X1} {NS:nstuck (tm/s X1)}
      p1 T NS1 NS -> progress T NS1 -> progress (of/s T) NS.
p2 :
   {E:tm} {E1:tm} {E2:tm -> tm}
      of E ty/nat -> nstuck E -> nstuck (tm/if E E1 ([x:tm] E2 x)) -> type.
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {X4:of X1 ty/nat} {X5:tm} {E:step X1 X5}
      p2 X2 ([x:tm] X3 x) X4 (nstuck/step E) (nstuck/step (step/if E)).
- :
   {X1:tm} {X2:tm -> tm} {X3:of tm/z ty/nat}
      p2 X1 ([x:tm] X2 x) X3 (nstuck/value v/z) (nstuck/step step/ifz).
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {X4:of (tm/s X1) ty/nat} {V:v X1}
      p2 X2 ([x:tm] X3 x) X4 (nstuck/value (v/s V)) (nstuck/step (step/ifs V)).
%mode +{E:tm} +{E1:tm} +{F:tm -> tm} +{A:of E ty/nat} +{B:nstuck E}
   -{C:nstuck (tm/if E E1 ([x:tm] F x))} (p2 E1 F A B C).
%worlds () (p2 _ _ _ _ _).
%total {} (p2 _ _ _ _ _).
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {T:of X1 ty/nat} {NS1:nstuck X1}
      {NS:nstuck (tm/if X1 X2 ([x:tm] X3 x))} {X4:ty} {T1:of X2 X4}
      {T2:{x:tm} of x ty/nat -> of (X3 x) X4}
      p2 X2 ([x:tm] X3 x) T NS1 NS -> progress T NS1
         -> progress (of/if T T1 ([x:tm] [x1:of x ty/nat] T2 x x1)) NS.
- :
   {X1:ty} {X2:tm -> tm} {T:{x:tm} of x X1 -> of (X2 x) X1}
      progress (of/fix ([x:tm] [x1:of x X1] T x x1)) (nstuck/step step/fix).
p3 :
   {E:tm} {T:ty} {E':tm -> tm}
      of* E T -> nstuck* E -> nstuck (tm/handle E ([x:tm] E' x)) -> type.
- :
   {X1:tm} {X2:ty} {X3:tm -> tm} {X4:of* X1 X2} {X5:tm} {E:step X1 X5}
      p3 ([x:tm] X3 x) X4 (nstuck*/step E) (nstuck/step (step/handle E)).
- :
   {X1:tm} {X2:ty} {X3:tm -> tm} {X4:of* X1 X2} {V:v X1}
      p3 ([x:tm] X3 x) X4 (nstuck*/value V) (nstuck/step (step/handler V)).
- :
   {X1:tm} {X2:ty} {X3:tm -> tm} {X4:of* (tm/raise X1) X2} {V:v X1}
      p3 ([x:tm] X3 x) X4 (nstuck*/raise V) (nstuck/step (step/handlex V)).
%mode +{E:tm} +{T:ty} +{A:tm -> tm} +{B:of* E T} +{C:nstuck* E}
   -{D:nstuck (tm/handle E ([x:tm] A x))} (p3 A B C D).
%worlds () (p3 _ _ _ _).
%total {} (p3 _ _ _ _).
- :
   {X1:tm} {X2:ty} {X3:tm -> tm} {T:of* X1 X2} {NS1:nstuck* X1}
      {NS:nstuck (tm/handle X1 ([x:tm] X3 x))}
      {T2:{x:tm} of x ty/exn -> of (X3 x) X2}
      p3 ([x:tm] X3 x) T NS1 NS -> progress* T NS1
         -> progress (of/handle T ([x:tm] [x1:of x ty/exn] T2 x x1)) NS.
- : {X1:tm} {X2:ty} {X3:of* X1 X2} progress (of/susp X3) (nstuck/value v/susp).
p9 :
   {E:tm} {T1:ty} {T2:ty} {E':tm}
      of* E (ty/arrow T1 T2) -> nstuck* E -> nstuck* E' -> nstuck* (tm/app E E')
         -> type.
- :
   {X1:tm} {X2:ty} {X3:ty} {X4:tm} {X5:of* X1 (ty/arrow X2 X3)} {X6:tm}
      {E:step X1 X6} {X7:nstuck* X4}
      p9 X5 (nstuck*/step E) X7 (nstuck*/step (step/app1 E)).
- :
   {X1:tm} {X2:ty} {X3:ty} {X4:tm} {X5:of* (tm/raise X1) (ty/arrow X2 X3)}
      {V:v X1} {X6:nstuck* X4}
      p9 X5 (nstuck*/raise V) X6 (nstuck*/step (step/app1x V)).
- :
   {X1:tm} {X2:ty} {X3:ty} {X4:tm} {X5:of* X1 (ty/arrow X2 X3)} {V:v X1} {X6:tm}
      {E:step X4 X6}
      p9 X5 (nstuck*/value V) (nstuck*/step E) (nstuck*/step (step/app2 V E)).
- :
   {X1:tm} {X2:ty} {X3:ty} {X4:tm} {X5:of* X1 (ty/arrow X2 X3)} {V':v X1}
      {V:v X4}
      p9 X5 (nstuck*/value V') (nstuck*/raise V)
         (nstuck*/step (step/app2x V V')).
- :
   {X1:tm} {X2:tm} {NS:nstuck (tm/app X1 X2)} {NS*:nstuck* (tm/app X1 X2)}
      {X3:ty} {X4:ty} {T:of X1 (ty/arrow X3 X4)} {V1:v X1} {V2:v X2}
      ns-weaken NS NS* -> p0 T (nstuck/value V1) (nstuck/value V2) NS
         -> p9 (of*/weaken T) (nstuck*/value V1) (nstuck*/value V2) NS*.
%mode +{E:tm} +{T1:ty} +{T2:ty} +{E':tm} +{A:of* E (ty/arrow T1 T2)} +{B:nstuck* E}
   +{C:nstuck* E'} -{D:nstuck* (tm/app E E')} (p9 A B C D).
%worlds () (p9 _ _ _ _).
%total {} (p9 _ _ _ _).
- :
   {X1:tm} {X2:ty} {X3:ty} {X4:tm} {T1:of* X1 (ty/arrow X2 X3)} {NS1:nstuck* X1}
      {NS2:nstuck* X4} {NS:nstuck* (tm/app X1 X4)} {T2:of* X4 X2}
      p9 T1 NS1 NS2 NS -> progress* T2 NS2 -> progress* T1 NS1
         -> progress* (of*/app T1 T2) NS.
p5 : {E:tm} of* E ty/nat -> nstuck* E -> nstuck* (tm/s E) -> type.
- :
   {X1:tm} {X2:of* X1 ty/nat} {X3:tm} {E:step X1 X3}
      p5 X2 (nstuck*/step E) (nstuck*/step (step/s E)).
- :
   {X1:tm} {X2:of* X1 ty/nat} {V:v X1}
      p5 X2 (nstuck*/value V) (nstuck*/value (v/s V)).
- :
   {X1:tm} {X2:of* (tm/raise X1) ty/nat} {V:v X1}
      p5 X2 (nstuck*/raise V) (nstuck*/step (step/sx V)).
%mode +{E:tm} +{A:of* E ty/nat} +{B:nstuck* E} -{C:nstuck* (tm/s E)} (p5 A B C).
%worlds () (p5 _ _ _).
%total {} (p5 _ _ _).
- :
   {X1:tm} {T:of* X1 ty/nat} {NS1:nstuck* X1} {NS:nstuck* (tm/s X1)}
      p5 T NS1 NS -> progress* T NS1 -> progress* (of*/s T) NS.
p6 :
   {E:tm} {E1:tm} {E2:tm -> tm}
      of* E ty/nat -> nstuck* E -> nstuck* (tm/if E E1 ([x:tm] E2 x)) -> type.
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {X4:of* X1 ty/nat} {X5:tm} {E:step X1 X5}
      p6 X2 ([x:tm] X3 x) X4 (nstuck*/step E) (nstuck*/step (step/if E)).
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {NS:nstuck (tm/if X1 X2 ([x:tm] X3 x))}
      {NS*:nstuck* (tm/if X1 X2 ([x:tm] X3 x))} {T:of X1 ty/nat} {V:v X1}
      {T*:of* X1 ty/nat}
      ns-weaken NS NS* -> p2 X2 ([x:tm] X3 x) T (nstuck/value V) NS
         -> mobile V T* T -> p6 X2 ([x:tm] X3 x) T* (nstuck*/value V) NS*.
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {X4:of* (tm/raise X1) ty/nat} {V:v X1}
      p6 X2 ([x:tm] X3 x) X4 (nstuck*/raise V) (nstuck*/step (step/ifx V)).
%mode +{E:tm} +{A:tm} +{B:tm -> tm} +{C:of* E ty/nat} +{D:nstuck* E}
   -{E1:nstuck* (tm/if E A ([x:tm] B x))} (p6 A B C D E1).
%worlds () (p6 _ _ _ _ _).
%total {} (p6 _ _ _ _ _).
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {T:of* X1 ty/nat} {NS1:nstuck* X1}
      {NS:nstuck* (tm/if X1 X2 ([x:tm] X3 x))} {X4:ty} {T1:of* X2 X4}
      {T2:{x:tm} of x ty/nat -> of* (X3 x) X4}
      p6 X2 ([x:tm] X3 x) T NS1 NS -> progress* T NS1
         -> progress* (of*/if T T1 ([x:tm] [x1:of x ty/nat] T2 x x1)) NS.
pA : {E:tm} nstuck* E -> nstuck* (tm/raise E) -> type.
- :
   {X1:tm} {X2:tm} {E:step X1 X2}
      pA (nstuck*/step E) (nstuck*/step (step/raise E)).
- : {X1:tm} {V:v X1} pA (nstuck*/value V) (nstuck*/raise V).
- : {X1:tm} {V:v X1} pA (nstuck*/raise V) (nstuck*/step (step/raisex V)).
%mode +{E:tm} +{A:nstuck* E} -{B:nstuck* (tm/raise E)} (pA A B).
%worlds () (pA _ _).
%total {} (pA _ _).
- :
   {X1:tm} {NS1:nstuck* X1} {NS:nstuck* (tm/raise X1)} {T:of* X1 ty/exn} {X2:ty}
      pA NS1 NS -> progress* T NS1 -> progress* (of*/raise T) NS.
- :
   {X1:tm} {X2:tm -> tm} {NS*:nstuck (tm/handle X1 ([x:tm] X2 x))}
      {NS:nstuck* (tm/handle X1 ([x:tm] X2 x))} {X3:ty} {T:of* X1 X3}
      {NS1:nstuck* X1} {T2:{x:tm} of x ty/exn -> of* (X2 x) X3}
      ns-weaken NS* NS -> p3 ([x:tm] X2 x) T NS1 NS* -> progress* T NS1
         -> progress* (of*/handle T ([x:tm] [x1:of x ty/exn] T2 x x1)) NS.
p7 :
   {E:tm} {T:ty} {E':tm}
      v E -> of E (ty/mayraise T) -> step (tm/unsusp E) E' -> type.
- :
   {X1:tm} {X2:ty} {X3:v (tm/susp X1)} {X4:of (tm/susp X1) (ty/mayraise X2)}
      p7 X3 X4 step/unsuspr.
%mode +{E:tm} +{T:ty} -{E':tm} +{A:v E} +{B:of E (ty/mayraise T)}
   -{C:step (tm/unsusp E) E'} (p7 A B C).
%worlds () (p7 _ _ _).
%total {} (p7 _ _ _).
p8 :
   {E:tm} {T:ty}
      of* E (ty/mayraise T) -> nstuck* E -> nstuck* (tm/unsusp E) -> type.
- :
   {X1:tm} {X2:ty} {X3:of* X1 (ty/mayraise X2)} {X4:tm} {E:step X1 X4}
      p8 X3 (nstuck*/step E) (nstuck*/step (step/unsusp E)).
- :
   {X1:tm} {X2:ty} {X3:tm} {V:v X1} {T:of X1 (ty/mayraise X2)}
      {E:step (tm/unsusp X1) X3}
      p7 V T E -> p8 (of*/weaken T) (nstuck*/value V) (nstuck*/step E).
- :
   {X1:tm} {X2:ty} {X3:of* (tm/raise X1) (ty/mayraise X2)} {V:v X1}
      p8 X3 (nstuck*/raise V) (nstuck*/step (step/unsuspx V)).
%mode +{E:tm} +{T:ty} +{A:of* E (ty/mayraise T)} +{B:nstuck* E}
   -{C:nstuck* (tm/unsusp E)} (p8 A B C).
%worlds () (p8 _ _ _).
%total {} (p8 _ _ _).
- :
   {X1:tm} {X2:ty} {T:of* X1 (ty/mayraise X2)} {NS1:nstuck* X1}
      {NS:nstuck* (tm/unsusp X1)}
      p8 T NS1 NS -> progress* T NS1 -> progress* (of*/unsusp T) NS.
%worlds () (progress _ _) (progress* _ _).
%total (T T*) (progress T _) (progress* T* _).
inv-lam :
   {T':ty} {E:tm -> tm} {T:ty} {T'':ty}
      of* (tm/lam T' ([x:tm] E x)) T -> ({x:tm} of x T' -> of (E x) T'')
         -> eqty T (ty/arrow T' T'') -> type.
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {F:{x:tm} of x X1 -> of (X2 x) X3}
      inv-lam (of*/weaken (of/lam ([x:tm] [x1:of x X1] F x x1)))
         ([x:tm] [x1:of x X1] F x x1) eqty/refl.
%mode +{T':ty} +{E:tm -> tm} +{T:ty} -{T'':ty} +{A:of* (tm/lam T' ([x:tm] E x)) T}
   -{B:{x:tm} of x T' -> of (E x) T''} -{C:eqty T (ty/arrow T' T'')}
   (inv-lam A B C).
%worlds () (inv-lam _ _ _).
%total {} (inv-lam _ _ _).
inv-app :
   {E1:tm} {E2:tm} {T:ty} {T':ty}
      of* (tm/app E1 E2) T -> of* E1 (ty/arrow T' T) -> of* E2 T' -> type.
- :
   {X1:tm} {X2:tm} {X3:ty} {X4:ty} {T1:of* X1 (ty/arrow X4 X3)} {T2:of* X2 X4}
      inv-app (of*/app T1 T2) T1 T2.
- :
   {X1:tm} {X2:tm} {X3:ty} {X4:ty} {T1:of X1 (ty/arrow X4 X3)} {T2:of X2 X4}
      inv-app (of*/weaken (of/app T1 T2)) (of*/weaken T1) (of*/weaken T2).
%mode +{E1:tm} +{E2:tm} +{T:ty} -{T':ty} +{A:of* (tm/app E1 E2) T}
   -{B:of* E1 (ty/arrow T' T)} -{C:of* E2 T'} (inv-app A B C).
%worlds () (inv-app _ _ _).
%total {} (inv-app _ _ _).
inv-s : {E:tm} {T:ty} of* (tm/s E) T -> of* E ty/nat -> eqty T ty/nat -> type.
- : {X1:tm} {T:of* X1 ty/nat} inv-s (of*/s T) T eqty/refl.
- :
   {X1:tm} {T:of X1 ty/nat} inv-s (of*/weaken (of/s T)) (of*/weaken T) 
eqty/refl.
%mode +{E:tm} +{T:ty} +{A:of* (tm/s E) T} -{B:of* E ty/nat} -{C:eqty T ty/nat}
   (inv-s A B C).
%worlds () (inv-s _ _ _).
%total {} (inv-s _ _ _).
inv-if :
   {E:tm} {E1:tm} {E2:tm -> tm} {T:ty}
      of* (tm/if E E1 ([x:tm] E2 x)) T -> of* E ty/nat -> of* E1 T
         -> ({x:tm} of x ty/nat -> of* (E2 x) T) -> type.
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {X4:ty} {T:of* X1 ty/nat} {T1:of* X2 X4}
      {T2:{x:tm} of x ty/nat -> of* (X3 x) X4}
      inv-if (of*/if T T1 ([x:tm] [x1:of x ty/nat] T2 x x1)) T T1
         ([x:tm] [x1:of x ty/nat] T2 x x1).
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {X4:ty} {T:of X1 ty/nat} {T1:of X2 X4}
      {T2:{x:tm} of x ty/nat -> of (X3 x) X4}
      inv-if (of*/weaken (of/if T T1 ([x:tm] [x1:of x ty/nat] T2 x x1)))
         (of*/weaken T) (of*/weaken T1)
         ([x:tm] [d:of x ty/nat] of*/weaken (T2 x d)).
%mode +{E:tm} +{E1:tm} +{E2:tm -> tm} +{T:ty} +{A:of* (tm/if E E1 ([x:tm] E2 x)) T}
   -{B:of* E ty/nat} -{C:of* E1 T} -{D:{x:tm} of x ty/nat -> of* (E2 x) T}
   (inv-if A B C D).
%worlds () (inv-if _ _ _ _).
%total {} (inv-if _ _ _ _).
inv-raise : {E:tm} {T:ty} of* (tm/raise E) T -> of* E ty/exn -> type.
- : {X1:tm} {X2:ty} {T:of* X1 ty/exn} inv-raise (of*/raise T) T.
%mode +{E:tm} +{T:ty} +{A:of* (tm/raise E) T} -{B:of* E ty/exn} (inv-raise A B).
%worlds () (inv-raise _ _).
%total {} (inv-raise _ _).
inv-handle :
   {E:tm} {H:tm -> tm} {T:ty}
      of* (tm/handle E ([x:tm] H x)) T -> of* E T
         -> ({x:tm} of x ty/exn -> of* (H x) T) -> type.
- :
   {X1:tm} {X2:tm -> tm} {X3:ty} {T:of* X1 X3}
      {H:{x:tm} of x ty/exn -> of* (X2 x) X3}
      inv-handle (of*/handle T ([x:tm] [x1:of x ty/exn] H x x1)) T
         ([x:tm] [x1:of x ty/exn] H x x1).
- :
   {X1:tm} {X2:tm -> tm} {X3:ty} {T:of* X1 X3}
      {H:{x:tm} of x ty/exn -> of (X2 x) X3}
      inv-handle (of*/weaken (of/handle T ([x:tm] [x1:of x ty/exn] H x x1))) T
         ([x:tm] [d:of x ty/exn] of*/weaken (H x d)).
%mode +{E:tm} +{H:tm -> tm} +{T:ty} +{A:of* (tm/handle E ([x:tm] H x)) T} -{B:of* E T}
   -{C:{x:tm} of x ty/exn -> of* (H x) T} (inv-handle A B C).
%worlds () (inv-handle _ _ _).
%total {} (inv-handle _ _ _).
inv-susp :
   {E:tm} {T:ty} {T':ty}
      of* (tm/susp E) T -> of* E T' -> eqty T (ty/mayraise T') -> type.
- : {X1:tm} {X2:ty} {T:of* X1 X2} inv-susp (of*/weaken (of/susp T)) T eqty/refl.
%mode +{E:tm} +{T:ty} -{T':ty} +{A:of* (tm/susp E) T} -{B:of* E T'}
   -{C:eqty T (ty/mayraise T')} (inv-susp A B C).
%worlds () (inv-susp _ _ _).
%total {} (inv-susp _ _ _).
inv-unsusp : {E:tm} {T:ty} of* (tm/unsusp E) T -> of* E (ty/mayraise T) -> type.
- : {X1:tm} {X2:ty} {T:of* X1 (ty/mayraise X2)} inv-unsusp (of*/unsusp T) T.
%mode +{E:tm} +{T:ty} +{A:of* (tm/unsusp E) T} -{B:of* E (ty/mayraise T)}
   (inv-unsusp A B).
%worlds () (inv-unsusp _ _).
%total {} (inv-unsusp _ _).
preservation : {E:tm} {E':tm} {T:ty} step E E' -> of E T -> of E' T -> type.
preservation* : {E:tm} {E':tm} {T:ty} step E E' -> of* E T -> of* E' T -> type.
%mode +{E:tm} +{E':tm} +{T:ty} +{A:step E E'} +{B:of E T} -{C:of E' T}
   (preservation A B C).
%mode +{E:tm} +{E':tm} +{T:ty} +{A:step E E'} +{B:of* E T} -{C:of* E' T}
   (preservation* A B C).
- :
   {X1:tm} {X2:tm} {X3:ty} {X4:ty} {E:step X1 X2} {T1:of X1 (ty/arrow X3 X4)}
      {T1':of X2 (ty/arrow X3 X4)} {X5:tm} {T2:of X5 X3}
      preservation E T1 T1'
         -> preservation (step/app1 E) (of/app T1 T2) (of/app T1' T2).
- :
   {X1:tm} {X2:tm} {X3:ty} {E:step X1 X2} {T2:of X1 X3} {T2':of X2 X3} {X4:tm}
      {X5:ty} {V:v X4} {T1:of X4 (ty/arrow X3 X5)}
      preservation E T2 T2'
         -> preservation (step/app2 V E) (of/app T1 T2) (of/app T1 T2').
- :
   {T:ty} {X1:tm -> tm} {E:tm} {X2:ty} {V:v E}
      {Tf:{x:tm} of x T -> of (X1 x) X2} {T2:of E T}
      preservation (step/appr V)
         (of/app (of/lam ([x:tm] [x1:of x T] Tf x x1)) T2) (Tf E T2).
- :
   {X1:tm} {X2:tm} {X3:ty} {X4:ty} {E:step X1 X2} {T1:of* X1 (ty/arrow X3 X4)}
      {T1':of* X2 (ty/arrow X3 X4)} {X5:tm} {T:of* (tm/app X1 X5) X4}
      {T2:of* X5 X3}
      preservation* E T1 T1' -> inv-app T T1 T2
         -> preservation* (step/app1 E) T (of*/app T1' T2).
- :
   {X1:tm} {X2:ty} {X3:ty} {T1:of* (tm/raise X1) (ty/arrow X2 X3)}
      {Texn:of* X1 ty/exn} {X4:tm} {T:of* (tm/app (tm/raise X1) X4) X3}
      {T2:of* X4 X2} {V:v X1}
      inv-raise T1 Texn -> inv-app T T1 T2
         -> preservation* (step/app1x V) T (of*/raise Texn).
- :
   {X1:tm} {X2:tm} {X3:ty} {E:step X1 X2} {T2:of* X1 X3} {T2':of* X2 X3} {X4:tm}
      {X5:ty} {T:of* (tm/app X4 X1) X5} {T1:of* X4 (ty/arrow X3 X5)} {V:v X4}
      preservation* E T2 T2' -> inv-app T T1 T2
         -> preservation* (step/app2 V E) T (of*/app T1 T2').
- :
   {X1:tm} {X2:ty} {T2:of* (tm/raise X1) X2} {Texn:of* X1 ty/exn} {X3:tm}
      {X4:ty} {T:of* (tm/app X3 (tm/raise X1)) X4} {T1:of* X3 (ty/arrow X2 X4)}
      {V:v X1} {V':v X3}
      inv-raise T2 Texn -> inv-app T T1 T2
         -> preservation* (step/app2x V V') T (of*/raise Texn).
q2 :
   {T3:ty} {T4:ty} {T1:ty} {T5:ty} {E2:tm -> tm} {E6:tm}
      eqty (ty/arrow T3 T4) (ty/arrow T1 T5) -> ({x:tm} of x T1 -> of (E2 x) T5)
         -> of E6 T3 -> of (E2 E6) T4 -> type.
- :
   {X1:ty} {X2:ty} {X3:tm -> tm} {X4:tm} {F:{x:tm} of x X1 -> of (X3 x) X2}
      {E:of X4 X1} q2 eqty/refl ([x:tm] [x1:of x X1] F x x1) E (F X4 E).
%mode +{T3:ty} +{T4:ty} +{T1:ty} +{T5:ty} +{E2:tm -> tm} +{E6:tm}
   +{A:eqty (ty/arrow T3 T4) (ty/arrow T1 T5)}
   +{B:{x:tm} of x T1 -> of (E2 x) T5} +{C:of E6 T3} -{D:of (E2 E6) T4}
   (q2 A B C D).
%worlds () (q2 _ _ _ _).
%total {} (q2 _ _ _ _).
- :
   {X1:ty} {X2:ty} {X3:ty} {X4:ty} {X5:tm -> tm} {X6:tm}
      {Eq:eqty (ty/arrow X1 X2) (ty/arrow X3 X4)}
      {F:{x:tm} of x X3 -> of (X5 x) X4} {T2:of X6 X1} {Tres:of (X5 X6) X2}
      {T1:of* (tm/lam X3 ([x:tm] X5 x)) (ty/arrow X1 X2)} {V:v X6}
      {T2*:of* X6 X1} {T:of* (tm/app (tm/lam X3 ([x:tm] X5 x)) X6) X2}
      q2 Eq ([x:tm] [x1:of x X3] F x x1) T2 Tres
         -> inv-lam T1 ([x:tm] [x1:of x X3] F x x1) Eq -> mobile V T2* T2
         -> inv-app T T1 T2* -> preservation* (step/appr V) T (of*/weaken Tres).
- :
   {X1:tm} {X2:tm} {E:step X1 X2} {T:of X1 ty/nat} {T':of X2 ty/nat}
      preservation E T T' -> preservation (step/s E) (of/s T) (of/s T').
- :
   {X1:tm} {X2:tm} {E:step X1 X2} {T:of X1 ty/nat} {T':of X2 ty/nat} {X3:tm}
      {X4:tm -> tm} {X5:ty} {T1:of X3 X5}
      {T2:{x:tm} of x ty/nat -> of (X4 x) X5}
      preservation E T T'
         -> preservation (step/if E)
               (of/if T T1 ([x:tm] [x1:of x ty/nat] T2 x x1))
               (of/if T' T1 ([x:tm] [x1:of x ty/nat] T2 x x1)).
- :
   {X1:tm} {X2:tm -> tm} {X3:ty} {T1:of X1 X3}
      {X4:{x:tm} of x ty/nat -> of (X2 x) X3}
      preservation step/ifz (of/if of/z T1 ([x:tm] [x1:of x ty/nat] X4 x x1)) T1.
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {X4:ty} {V:v X1} {T:of X1 ty/nat} {X5:of X2 X4}
      {T2:{x:tm} of x ty/nat -> of (X3 x) X4}
      preservation (step/ifs V)
         (of/if (of/s T) X5 ([x:tm] [x1:of x ty/nat] T2 x x1)) (T2 X1 T).
q1 : {E:tm} {T:ty} of* E ty/nat -> eqty T ty/nat -> of* (tm/s E) T -> type.
- : {X1:tm} {T:of* X1 ty/nat} {X2:eqty ty/nat ty/nat} q1 T X2 (of*/s T).
%mode +{E:tm} +{T:ty} +{A:of* E ty/nat} +{B:eqty T ty/nat} -{C:of* (tm/s E) T}
   (q1 A B C).
%worlds () (q1 _ _ _).
%total {} (q1 _ _ _).
- :
   {X1:tm} {X2:ty} {T':of* X1 ty/nat} {Eq:eqty X2 ty/nat} {Ts':of* (tm/s X1) X2}
      {X3:tm} {E:step X3 X1} {T:of* X3 ty/nat} {Ts:of* (tm/s X3) X2}
      q1 T' Eq Ts' -> preservation* E T T' -> inv-s Ts T Eq
         -> preservation* (step/s E) Ts Ts'.
q3 :
   {E:tm} {TN:ty}
      of* (tm/raise E) ty/nat -> eqty TN ty/nat -> of* (tm/raise E) TN -> type.
- : {X1:tm} {T:of* (tm/raise X1) ty/nat} {X2:eqty ty/nat ty/nat} q3 T X2 T.
%mode +{E:tm} +{TN:ty} +{A:of* (tm/raise E) ty/nat} +{B:eqty TN ty/nat}
   -{C:of* (tm/raise E) TN} (q3 A B C).
%worlds () (q3 _ _ _).
%total {} (q3 _ _ _).
- :
   {E:tm} {TN:ty} {DT:of* (tm/raise E) ty/nat} {Eq:eqty TN ty/nat}
      {DT':of* (tm/raise E) TN} {DTs:of* (tm/s (tm/raise E)) TN} {V:v E}
      q3 DT Eq DT' -> inv-s DTs DT Eq -> preservation* (step/sx V) DTs DT'.
- :
   {X1:tm} {X2:tm} {E:step X1 X2} {T:of* X1 ty/nat} {T':of* X2 ty/nat} {X3:tm}
      {X4:tm -> tm} {X5:ty} {Tif:of* (tm/if X1 X3 ([x:tm] X4 x)) X5}
      {T1:of* X3 X5} {T2:{x:tm} of x ty/nat -> of* (X4 x) X5}
      preservation* E T T' -> inv-if Tif T T1 ([x:tm] [x1:of x ty/nat] T2 x x1)
         -> preservation* (step/if E) Tif
               (of*/if T' T1 ([x:tm] [x1:of x ty/nat] T2 x x1)).
- :
   {E1:tm} {X1:tm -> tm} {T:ty} {Tif:of* (tm/if tm/z E1 ([x:tm] X1 x)) T}
      {DT:of* tm/z ty/nat} {T1:of* E1 T} {X2:{x:tm} of x ty/nat -> of* (X1 x) T}
      inv-if Tif DT T1 ([x:tm] [x1:of x ty/nat] X2 x x1)
         -> preservation* step/ifz Tif T1.
- :
   {N:tm} {V:v N} {Tn*:of* N ty/nat} {Tn:of N ty/nat} {Tsn*:of* (tm/s N) ty/nat}
      {X1:eqty ty/nat ty/nat} {X2:tm} {E2:tm -> tm} {T:ty}
      {DTif:of* (tm/if (tm/s N) X2 ([x:tm] E2 x)) T} {T1:of* X2 T}
      {T2:{x:tm} of x ty/nat -> of* (E2 x) T}
      mobile V Tn* Tn -> inv-s Tsn* Tn* X1
         -> inv-if DTif Tsn* T1 ([x:tm] [x1:of x ty/nat] T2 x x1)
         -> preservation* (step/ifs V) DTif (T2 N Tn).
- :
   {X1:tm} {DT:of* (tm/raise X1) ty/nat} {DTexn:of* X1 ty/exn} {X2:tm}
      {X3:tm -> tm} {X4:ty} {DTif:of* (tm/if (tm/raise X1) X2 ([x:tm] X3 x)) X4}
      {X5:of* X2 X4} {X6:{x:tm} of x ty/nat -> of* (X3 x) X4} {V:v X1}
      inv-raise DT DTexn -> inv-if DTif DT X5 ([x:tm] [x1:of x ty/nat] X6 x x1)
         -> preservation* (step/ifx V) DTif (of*/raise DTexn).
- :
   {X1:ty} {X2:tm -> tm} {F:{x:tm} of x X1 -> of (X2 x) X1}
      preservation step/fix (of/fix ([x:tm] [x1:of x X1] F x x1))
         (F (tm/fix X1 ([x:tm] X2 x)) (of/fix ([x:tm] [x1:of x X1] F x x1))).
- :
   {X1:tm} {X2:tm} {X3:ty} {E:step X1 X2} {T*:of* X1 X3} {T'*:of* X2 X3}
      {X4:tm -> tm} {T:{x:tm} of x ty/exn -> of (X4 x) X3}
      preservation* E T* T'*
         -> preservation (step/handle E)
               (of/handle T* ([x:tm] [x1:of x ty/exn] T x x1))
               (of/handle T'* ([x:tm] [x1:of x ty/exn] T x x1)).
- :
   {X1:tm} {X2:ty} {V:v X1} {T*:of* X1 X2} {T':of X1 X2} {X3:tm -> tm}
      {T:{x:tm} of x ty/exn -> of (X3 x) X2}
      mobile V T* T'
         -> preservation (step/handler V)
               (of/handle T* ([x:tm] [x1:of x ty/exn] T x x1)) T'.
- :
   {X1:tm} {V:v X1} {Texn*:of* X1 ty/exn} {Texn:of X1 ty/exn} {X2:tm -> tm}
      {X3:ty} {T:{x:tm} of x ty/exn -> of (X2 x) X3}
      mobile V Texn* Texn
         -> preservation (step/handlex V)
               (of/handle (of*/raise Texn*) ([x:tm] [x1:of x ty/exn] T x x1))
               (T X1 Texn).
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {T:of (tm/fix X1 ([x:tm] X2 x)) X3}
      {T':of (X2 (tm/fix X1 ([x:tm] X2 x))) X3}
      preservation step/fix T T'
         -> preservation* step/fix (of*/weaken T) (of*/weaken T').
- :
   {X1:tm} {X2:tm} {E:step X1 X2} {T:of* X1 ty/exn} {T':of* X2 ty/exn} {X3:ty}
      preservation* E T T'
         -> preservation* (step/raise E) (of*/raise T) (of*/raise T').
- :
   {X1:tm} {T:of* (tm/raise X1) ty/exn} {Texn:of* X1 ty/exn} {X2:ty} {E:v X1}
      inv-raise T Texn
         -> preservation* (step/raisex E) (of*/raise T) (of*/raise Texn).
- :
   {E:tm} {X1:tm} {T:ty} {DE:step E X1} {DT1:of* E T} {DT1':of* X1 T}
      {H:tm -> tm} {DT:of* (tm/handle E ([x:tm] H x)) T}
      {DT2:{x:tm} of x ty/exn -> of* (H x) T}
      preservation* DE DT1 DT1'
         -> inv-handle DT DT1 ([x:tm] [x1:of x ty/exn] DT2 x x1)
         -> preservation* (step/handle DE) DT
               (of*/handle DT1' ([x:tm] [x1:of x ty/exn] DT2 x x1)).
- :
   {X1:tm} {X2:tm -> tm} {X3:ty} {DT:of* (tm/handle X1 ([x:tm] X2 x)) X3}
      {DT1:of* X1 X3} {DT2:{x:tm} of x ty/exn -> of* (X2 x) X3} {V:v X1}
      inv-handle DT DT1 ([x:tm] [x1:of x ty/exn] DT2 x x1)
         -> preservation* (step/handler V) DT DT1.
- :
   {E:tm} {V:v E} {DTexn:of* E ty/exn} {DTexn':of E ty/exn} {T:ty}
      {DT1:of* (tm/raise E) T} {H:tm -> tm}
      {DT:of* (tm/handle (tm/raise E) ([x:tm] H x)) T}
      {DT2:{x:tm} of x ty/exn -> of* (H x) T}
      mobile V DTexn DTexn' -> inv-raise DT1 DTexn
         -> inv-handle DT DT1 ([x:tm] [x1:of x ty/exn] DT2 x x1)
         -> preservation* (step/handlex V) DT (DT2 E DTexn').
- :
   {E:tm} {E':tm} {T:ty} {DE:step E E'} {DT':of* E (ty/mayraise T)}
      {DT'':of* E' (ty/mayraise T)} {DT:of* (tm/unsusp E) T}
      preservation* DE DT' DT'' -> inv-unsusp DT DT'
         -> preservation* (step/unsusp DE) DT (of*/unsusp DT'').
d4 :
   {T:ty} {T':ty} {E:tm}
      eqty (ty/mayraise T) (ty/mayraise T') -> of* E T' -> of* E T -> type.
- :
   {X1:ty} {X2:tm} {X3:eqty (ty/mayraise X1) (ty/mayraise X1)} {T:of* X2 X1}
      d4 X3 T T.
%mode +{T:ty} +{T':ty} +{E:tm} +{A:eqty (ty/mayraise T) (ty/mayraise T')}
   +{B:of* E T'} -{C:of* E T} (d4 A B C).
%worlds () (d4 _ _ _).
%total {} (d4 _ _ _).
- :
   {T:ty} {T':ty} {E:tm} {Eq:eqty (ty/mayraise T) (ty/mayraise T')}
      {DT'':of* E T'} {DT''':of* E T} {DT':of* (tm/susp E) (ty/mayraise T)}
      {DT:of* (tm/unsusp (tm/susp E)) T}
      d4 Eq DT'' DT''' -> inv-susp DT' DT'' Eq -> inv-unsusp DT DT'
         -> preservation* step/unsuspr DT DT'''.
- :
   {E:tm} {T:ty} {DT':of* (tm/raise E) (ty/mayraise T)} {DTexn:of* E ty/exn}
      {DT:of* (tm/unsusp (tm/raise E)) T} {V:v E}
      inv-raise DT' DTexn -> inv-unsusp DT DT'
         -> preservation* (step/unsuspx V) DT (of*/raise DTexn).
%worlds () (preservation _ _ _) (preservation* _ _ _).
%total (E E*) (preservation E _ _) (preservation* E* _ _).
[Closing file /home/www/twelf/hcode/82c023e77a487aea9a02c9571fa400ed]
%% OK %%