use(int).
%use(nat).

K<I -> subst(var(I),K,S)=var(p(I)).
       subst(var(I),I,S)=S.
I<K -> subst(var(I),K,S)=var(I).


subst(app(T,U),K,S)=app(subst(T,K,S),subst(U,K,S)).

subst(abs(T),K,S)=abs(subst(T,s(K),lift(S,0))).


I<K -> lift(var(I),K) = var(I).
K=<I -> lift(var(I),K) = var(s(I)).

lift(app(S,T),K) = app(lift(S,K),lift(T,K)).

lift(abs(S),K) = abs(lift(S,s(K))).


free(var(J),I)<=>(J=I).

free(app(S,T),I)<=>(free(S,I) or free(T,I)).

free(abs(S),I)<=>free(S,s(I)).


precedence([free,subst,lift,abs,app,var,s,p,0]).