Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Termsby Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand12 Nov