Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/0e7be47e4f6ca72d05e97efbe0f2bd38]
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.
assm : exp -> tp -> type.
of : exp -> tp -> type.
of/var : {E:exp} {T:tp} assm E T -> of E T.
of/unit : of exp/unit tp/unit.
of/lam :
   {T:tp} {E:exp -> exp} {T':tp}
      ({x:exp} assm x T -> of (E x) T')
         -> of (exp/lam T ([x:exp] E x)) (tp/arrow T T').
of/app :
   {E1:exp} {T:tp} {T':tp} {E2:exp}
      of E1 (tp/arrow T T') -> of E2 T -> of (exp/app E1 E2) T'.
subst :
   {E1:exp} {T:tp} {E2:exp -> exp} {T':tp}
      of E1 T -> ({x:exp} assm x T -> of (E2 x) T') -> of (E2 E1) T' -> type.
%mode +{E1:exp} +{T:tp} +{E2:exp -> exp} +{T':tp} +{D1:of E1 T}
   +{D2:{x:exp} assm x T -> of (E2 x) T'} -{D3:of (E2 E1) T'} (subst D1 D2 D3).
- :
   {X1:exp} {X2:tp} {D1:of X1 X2} subst D1 ([x:exp] [dx:assm x X2] of/var dx) D1.
- :
   {X1:exp} {X2:tp} {X3:exp} {X4:tp} {D1:of X1 X2} {D2:of X3 X4}
      subst D1 ([x:exp] [dx:assm x X2] D2) D2.
- :
   {X1:tp} {X2:exp} {X3:tp} {X4:exp -> exp -> exp} {X5:tp} {D1:of X2 X3}
      {D2:{x:exp} assm x X3 -> ({x1:exp} assm x1 X1 -> of (X4 x x1) X5)}
      {D2':{x:exp} assm x X1 -> of (X4 X2 x) X5}
      ({y:exp} {dy:assm y X1}
          subst D1 ([x:exp] [dx:assm x X3] D2 x dx y dy) (D2' y dy))
         -> subst D1
               ([x:exp] [dx:assm x X3]
                   of/lam ([y:exp] [dy:assm y X1] D2 x dx y dy))
               (of/lam ([x:exp] [x1:assm x X1] D2' x x1)).
- :
   {X1:exp} {X2:tp} {X3:exp -> exp} {X4:tp} {D1:of X1 X2}
      {D3:{x:exp} assm x X2 -> of (X3 x) X4} {D3':of (X3 X1) X4} {X5:exp -> exp}
      {X6:tp} {D2:{x:exp} assm x X2 -> of (X5 x) (tp/arrow X4 X6)}
      {D2':of (X5 X1) (tp/arrow X4 X6)}
      subst D1 ([x:exp] [dx:assm x X2] D3 x dx) D3'
         -> subst D1 ([x:exp] [dx:assm x X2] D2 x dx) D2'
         -> subst D1 ([x:exp] [dx:assm x X2] of/app (D2 x dx) (D3 x dx))
               (of/app D2' D3').
%block assm-block : some {T:tp} block {x:exp} {dx:assm x T}.
%worlds (assm-block) (subst _ _ _).
%total D1 (subst _ D1 _).
[Closing file /home/www/twelfwiki/code/0e7be47e4f6ca72d05e97efbe0f2bd38]
%% OK %%