Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/3eb2da870ee2a7fda66d9018b3d353e0]
tp : type.
unit : tp.
arrow : tp -> tp -> tp.
tm : type.
empty : tm.
app : tm -> tm -> tm.
lam : tp -> (tm -> tm) -> tm.
of : tm -> tp -> type.
of-empty : of empty unit.
of-lam :
   {T2:tp} {E:tm -> tm} {T:tp}
      ({x:tm} of x T2 -> of (E x) T) -> of (lam T2 ([x:tm] E x)) (arrow T2 T).
of-app :
   {E2:tm} {T2:tp} {E1:tm} {T:tp}
      of E2 T2 -> of E1 (arrow T2 T) -> of (app E1 E2) T.
value : tm -> type.
value-empty : value empty.
value-lam : {T:tp} {E:tm -> tm} value (lam T ([x:tm] E x)).
step : tm -> tm -> type.
step-app-1 :
   {E1:tm} {E1':tm} {E2:tm} step E1 E1' -> step (app E1 E2) (app E1' E2).
step-app-2 :
   {E2:tm} {E2':tm} {E1:tm}
      step E2 E2' -> value E1 -> step (app E1 E2) (app E1 E2').
step-app-beta :
   {E2:tm} {T2:tp} {E:tm -> tm}
      value E2 -> step (app (lam T2 ([x:tm] E x)) E2) (E E2).
preserv : {E:tm} {E':tm} {T:tp} step E E' -> of E T -> of E' T -> type.
%mode +{E:tm} +{E':tm} +{T:tp} +{Dstep:step E E'} +{Dof:of E T} -{Dof':of E' T}
   (preserv Dstep Dof Dof').
preserv-app-1 :
   {E1:tm} {E1':tm} {T2:tp} {T:tp} {DstepE1:step E1 E1'}
      {DofE1:of E1 (arrow T2 T)} {DofE1':of E1' (arrow T2 T)} {E2:tm}
      {DofE2:of E2 T2}
      preserv DstepE1 DofE1 DofE1'
         -> preserv (step-app-1 DstepE1) (of-app DofE2 DofE1)
               (of-app DofE2 DofE1').
preserv-app-2 :
   {E2:tm} {E2':tm} {T2:tp} {DstepE2:step E2 E2'} {DofE2:of E2 T2}
      {DofE2':of E2' T2} {E1:tm} {T:tp} {DvalE1:value E1}
      {DofE1:of E1 (arrow T2 T)}
      preserv DstepE2 DofE2 DofE2'
         -> preserv (step-app-2 DstepE2 DvalE1) (of-app DofE2 DofE1)
               (of-app DofE2' DofE1).
preserv-app-beta :
   {T2:tp} {E:tm -> tm} {E2:tm} {T:tp} {Dval:value E2} {DofE2:of E2 T2}
      {DofE:{x:tm} of x T2 -> of (E x) T}
      preserv (step-app-beta Dval)
         (of-app DofE2 (of-lam ([x:tm] [dx:of x T2] DofE x dx))) (DofE E2 DofE2).
%worlds () (preserv _ _ _).
%total D (preserv D _ _).
[Closing file /home/www/twelfwiki/code/3eb2da870ee2a7fda66d9018b3d353e0]
%% OK %%