This is the evaluation conversion for numeral addition. It takes a term of the form `m + n`, where "m" and "n" are both natural number numerals, and returns a theorem stating that this equals its numeral value, under no assumptions. `m + n` ------------ |- m + n = z See also: eval_sub_conv, eval_mult_conv, eval_exp_conv.

This is the evaluation conversion for numeral evenness. It takes a term of the form `EVEN n`, where "n" is a natural number numeral, and returns a theorem stating its boolean value, under no assumptions. `EVEN n` --------------- |- EVEN n <=> z See also: eval_odd_conv.

This is the evaluation conversion for numeral exponentiation. It takes a term of the form `m EXP n`, where "m" and "n" are both natural number numerals, and returns a theorem stating that this equals its numeral value, under no assumptions. `m EXP n` -------------- |- m EXP n = z See also: eval_add_conv, eval_sub_conv, eval_mult_conv.

This is the evaluation conversion for numeral greater-than-or-equal comparison. It takes a term of the form `m >= n`, where "m" and "n" are both natural number numerals, and returns a theorem stating that this input equals its boolean value, under no assumptions. `m >= n` --------------- |- m >= n <=> z eval_ge_conv, eval_le_conv, eval_lt_conv, eval_nat_eq_conv.

This is the evaluation conversion for numeral greater-than comparison. It takes a term of the form `m > n`, where "m" and "n" are both natural number numerals, and returns a theorem stating that this input equals its boolean value, under no assumptions. `m > n` -------------- |- m > n <=> z eval_ge_conv, eval_le_conv, eval_lt_conv, eval_nat_eq_conv.

This is the evaluation conversion for numeral less-than-or-equal comparison. It takes a term of the form `m <= n`, where "m" and "n" are both natural number numerals, and returns a theorem stating that this input equals its boolean value, under no assumptions. `m <= n` -------------- |- m <= n <=> z See also: eval_lt_conv, eval_ge_conv, eval_gt_conv, eval_nat_eq_conv.

This is the evaluation conversion for numeral less-than-or-equal comparison. It takes a term of the form `m < n`, where "m" and "n" are both natural number numerals, and returns a theorem stating that this input equals its boolean value, under no assumptions. `m < n` -------------- |- m < n <=> z See also: eval_le_conv, eval_ge_conv, eval_gt_conv, eval_nat_eq_conv.

eval_mult_conv : term -> thm This is the evaluation conversion for numeral multiplication. It takes a term of the form `m * m`, where "m" and "n" are both natural number numerals, and returns a theorem stating that this equals its numeral value, under no assumptions. `m * n` ------------ |- m * n = z See also: eval_add_conv, eval_sub_conv, eval_exp_conv.

This is the evaluation conversion for numeric equality. It takes a term of the form `m = n`, where "m" and "n" are both natural number numerals, and returns a theorem stating that this equals its boolean value, under no assumptions. `m = n` -------------- |- m = n <=> z See also: eval_le_conv, eval_lt_conv, eval_ge_conv, eval_gt_conv.

This is the evaluation conversion for numeral oddness. It takes a term of the form `ODD n`, where "n" is a natural number numeral, and returns a theorem stating its boolean value, under no assumptions. `ODD n` -------------- |- ODD n <=> z See also: eval_even_conv.

eval_pre_conv : term -> thm This is the evaluation conversion for numeral predecessor. It takes a term of the form `PRE n`, where "n" is a natural number numeral, and returns a theorem stating that this equals its numeral value, under no assumptions. `PRE n` ------------ |- PRE n = z See also: eval_suc_conv.

This is the evaluation conversion for numeral subtraction. It takes a term of the form `m - n`, where "m" and "n" are both natural number numerals, and returns a theorem stating that this equals its numeral value, under no assumptions. `m - n` ------------ |- m - n = z See also: eval_add_conv, eval_mult_conv, eval_exp_conv.

This is the evaluation conversion for numeral successor. It takes a term of the form `SUC n`, where "n" is a natural number numeral, and returns a theorem stating that this equals its numeral value, under no assumptions. `SUC n` ------------ |- SUC n = z See also: eval_pre_conv.

Force module evaluation