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