Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/e02e08ddc5111ccb18bc7aeb65ef0eaa]
loc : type.
loc/z : loc.
loc/s : loc -> loc.
tm : type.
tm/loc : loc -> tm.
tm/lam : (tm -> tm) -> tm.
tm/app : tm -> tm -> tm.
st : type.
st/nil : st.
st/cons : loc -> tm -> st -> st.
st-lookup : st -> loc -> tm -> type.
st-lookup/1 : {L:loc} {T:tm} {_S1:st} st-lookup (st/cons L T _S1) L T.
st-lookup/2 :
   {S:st} {L':loc} {T':tm} {L:loc} {T:tm}
      st-lookup S L' T' -> st-lookup (st/cons L T S) L' T'.
tm-wf : tm -> st -> type.
tm-var : tm -> type.
tm-wf/var : {V:tm} {S:st} tm-var V -> tm-wf V S.
tm-wf/loc :
   {T:tm} {S:st} {L:loc} tm-wf T S -> st-lookup S L T -> tm-wf (tm/loc L) S.
tm-wf/lam :
   {T:tm -> tm} {S:st}
      ({v:tm} tm-var v -> tm-wf (T v) S) -> tm-wf (tm/lam ([x:tm] T x)) S.
tm-wf/app :
   {T2:tm} {S:st} {T1:tm} tm-wf T2 S -> tm-wf T1 S -> tm-wf (tm/app T1 T2) S.
eval : tm -> tm -> type.
eval/loc : {L:loc} eval (tm/loc L) (tm/loc L).
eval/lam : {T:tm -> tm} eval (tm/lam ([x:tm] T x)) (tm/lam ([x:tm] T x)).
eval/app :
   {T1':tm -> tm} {T2:tm} {T':tm} {T1:tm}
      eval (T1' T2) T' -> eval T1 (tm/lam ([x:tm] T1' x))
         -> eval (tm/app T1 T2) T'.
eval-pres-wf :
   {T:tm} {T':tm} {S:st} eval T T' -> tm-wf T S -> tm-wf T' S -> type.
%mode +{T:tm} +{T':tm} +{S:st} +{X1:eval T T'} +{X2:tm-wf T S} -{X3:tm-wf T' S}
   (eval-pres-wf X1 X2 X3).
-/loc : {_L1:loc} {_S1:st} {D:tm-wf (tm/loc _L1) _S1} eval-pres-wf eval/loc D D.
-/lam :
   {_T1:tm -> tm} {_S1:st} {D:tm-wf (tm/lam ([x:tm] _T1 x)) _S1}
      eval-pres-wf eval/lam D D.
/home/www/twelfwiki/code/e02e08ddc5111ccb18bc7aeb65ef0eaa:58.8-58.19 Error: 
Undeclared identifier tm-wf-subst
/home/www/twelfwiki/code/e02e08ddc5111ccb18bc7aeb65ef0eaa:58.8-58.19 Error: 
Ambiguous reconstruction
Inferred: [_dwf:{_t:tm} {x:tm-var _t} tm-wf (_T1 _t) _S1]
             [_dwf1:tm-wf (_T2 _dwf) (_S2 _dwf)]
             [_dwf2:tm-wf (_T3 _dwf _dwf1) (_S3 _dwf _dwf1)] `%A1%
Omitted type is ambiguous
[Closing file /home/www/twelfwiki/code/e02e08ddc5111ccb18bc7aeb65ef0eaa]
/home/www/twelfwiki/code/e02e08ddc5111ccb18bc7aeb65ef0eaa:56.1-59.39 Error: 
 2 errors found
%% ABORT %%