beta(app(abs(S),T),subst(S,0,T)).

beta(S,T) -> beta(app(U,S),app(U,T)).

beta(S,T) -> beta(app(S,U),app(T,U)).

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

betas(S,S).

beta(S,T) -> betas(S,T).

(betas(S,T) and beta(T,U)) -> betas(S,U).