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

In [1]:
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

In [2]:
%begin axioms

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

In [3]:
one_def = Equals(num(1), Add(zero, one))

one_def:
In [4]:
two_def = Equals(num(2), Add(one, one))

two_def:
In [5]:
three_def = Equals(num(3), Add(num(2), one))

three_def:
In [6]:
four_def = Equals(num(4), Add(num(3), one))

four_def:
In [7]:
five_def = Equals(num(5), Add(num(4), one))

five_def:
In [8]:
six_def = Equals(num(6), Add(num(5), one))

six_def:
In [9]:
seven_def = Equals(num(7), Add(num(6), one))

seven_def:
In [10]:
eight_def = Equals(num(8), Add(num(7), one))

eight_def:
In [11]:
nine_def = Equals(num(9), Add(num(8), one))

nine_def:
In [12]:
#\forall_{n} (n \in N_{\leq 9}) = (n \in N and n \leq 9)

In [13]:
N_leq_9_def = Forall(n, Equals(InSet(n, Digits), And(InSet(n, Natural), LessEq(n, num(9)))))

N_leq_9_def:
In [14]:
single_digit_reduction = Forall(n, Equals(DecimalSequence(n), n), domain=Digits)

single_digit_reduction:
In [15]:
%end axioms

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