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