decreases clauses added; default includes lex ordering only on non-function-typed arguments; revised tests to use this style