Axioms for the theory of proveit.numbers.numerals.decimals

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import Literal
from proveit import n, x
from proveit.logic import Equals, Forall, And, InSet
from proveit.numbers import num, zero, one, Add, LessEq, Natural
from proveit.numbers.numerals.decimals import DecimalSequence, Digits

%begin axioms

Defining axioms for theory 'proveit.numbers.numerals.decimals'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

one_def = Equals(num(1), Add(zero, one))

one_def:

two_def = Equals(num(2), Add(one, one))

two_def:

three_def = Equals(num(3), Add(num(2), one))

three_def:

four_def = Equals(num(4), Add(num(3), one))

four_def:

five_def = Equals(num(5), Add(num(4), one))

five_def:

six_def = Equals(num(6), Add(num(5), one))

six_def:

seven_def = Equals(num(7), Add(num(6), one))

seven_def:

eight_def = Equals(num(8), Add(num(7), one))

eight_def:

nine_def = Equals(num(9), Add(num(8), one))

nine_def:

#\forall_{n} (n \in N_{\leq 9}) = (n \in N and n \leq 9)

N_leq_9_def = Forall(n, Equals(InSet(n, Digits), And(InSet(n, Natural), LessEq(n, num(9)))))

N_leq_9_def:

single_digit_reduction = Forall(n, Equals(DecimalSequence(n), n), domain=Digits)

single_digit_reduction:

%end axioms

These axioms may now be imported from the theory package: proveit.numbers.numerals.decimals