0=<I -> pbeta(var(I),var(I)).

pbeta(S,T) -> pbeta(abs(S),abs(T)).

(pbeta(S,T) => (pbeta(U,V) => pbeta(app(S,U),app(T,V)))).

(pbeta(S,T) => (pbeta(U,V) => pbeta(app(abs(S),U),subst(T,0,V)))).

pbeta(S,S).