Lexicographic termination

Published: June 3, 2020, 4 a.m.

b'

Many termination checkers support lexicographic (structural) recursion.\\xa0 The lexicographic combination of orderings on sets A and B is an ordering on A x B where a pair decreases if the A component does (and then the B component can increase unboundedly) or else the A component stays the same and the B component decreases.\\xa0 Connections with nested recursion and ordinals discussed.

'