kdrag.termination.lex_gt

kdrag.termination.lex_gt(es: list[~z3.z3.ExprRef], es1: list[~z3.z3.ExprRef], measure=<function default_measure>) → BoolRef

Lexicographic greater than on lists of expressions.

>>> x, y = smt.Consts("x y", kd.Nat)
>>> _ = kd.prove(smt.Implies(x.is_S, lex_gt([x], [x.pred])))
>>> _ = kd.prove(smt.Implies(y.is_S, lex_gt([x, y], [x, y.pred])))
>>> _ = kd.prove(smt.Implies(y.is_S, smt.Not(lex_gt([x, y.pred], [x, y]))))
>>> _ = kd.prove(smt.Not(lex_gt([x, y], [x, y])))
>>> _ = kd.prove(smt.Implies(x.is_S, lex_gt([x, y], [x.pred, y])))

Parameters:

• es (list[ExprRef])

• es1 (list[ExprRef])

Return type:

BoolRef