The simply typed rewriting calculus