Termination of rewriting and its certification by