Size-based termination of higher-order rewriting. (19th April 2018)