Automatically proving termination and innermost normalisation of term rewriting systems door T.H.J.J. Arts