In [1]:
import proveit
from proveit import n
from proveit.numbers import zero, one, Add
from proveit.numbers.numerals.decimals import one_def
from proveit.numbers.number_sets.natural_numbers import zero_in_nats, successor_in_nats
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving nat1
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
nat1:
(see dependencies)
nat1:
(see dependencies)
In [3]:
one_def
In [4]:
successor_in_nats
In [5]:
zero_plus_one__in__nats = successor_in_nats.instantiate({n:zero})
zero_plus_one__in__nats: ⊢
In [6]:
%qed
Out[6]:
| step type | requirements | statement | ||
|---|---|---|---|---|
| 0 | instantiation | 1, 2, 3* | ⊢ | |
 :  | ||||
| 1 | axiom | ⊢  | ||
| proveit.numbers.number_sets.natural_numbers.successor_in_nats | ||||
| 2 | axiom | ⊢  | ||
| proveit.numbers.number_sets.natural_numbers.zero_in_nats | ||||
| 3 | instantiation | 4, 5 | ⊢  | |
 :  ,  :  | ||||
| 4 | theorem | ⊢  | ||
| proveit.logic.equality.equals_reversal | ||||
| 5 | axiom | ⊢  | ||
| proveit.numbers.numerals.decimals.one_def | ||||
| *equality replacement requirements | ||||