In [1]:
import proveit
from proveit import a, b, i
from proveit.core_expr_types.tuples import tuple_len_incr
from proveit.numbers.numerals.decimals import tuple_len_1, add_1_1
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving tuple_len_2
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
tuple_len_2:
(see dependencies)
tuple_len_2:
(see dependencies)
In [3]:
one_spec = tuple_len_1.instantiate({a:a}, auto_simplify=False)
one_spec: ⊢ 
In [4]:
tuple_spec = tuple_len_incr.instantiate(
{i: one_spec.rhs, a: [one_spec.lhs.operands[0]], b: b})
tuple_spec: ⊢ 
