import proveit
# Prepare this notebook for defining the common expressions of a theory:
%common_expressions_notebook # Keep this at the top following 'import proveit'.
from proveit import Function, ExprRange, IndexedVar, ExprTuple
from proveit.logic import Equals, InSet
from proveit import a, b, f, k, i, j, k, l, m, n, x
from proveit.core_expr_types import (
f_k, i_k, j_k, f_1_to_n, f_i_to_j, f_i_to_j_dec, i_1_to_n, j_1_to_n)
from proveit.numbers import Natural, one, Add, Neg
%begin common
fk_ik_to_jk = ExprRange(x, Function(f_k, x), i_k, j_k)
f_ik_to_jk__1_to_n = ExprRange(k, fk_ik_to_jk, one, n)
fk_i_to_j = ExprRange(x, Function(f_k, x), i, j)
f_i_to_j__1_to_n = ExprRange(k, fk_i_to_j, one, n)
fk_1_to_i = ExprRange(x, Function(f_k, x), one, i)
f_1_to_i__1_to_n = ExprRange(k, fk_1_to_i, one, n)
f_i_to_j__m_to_n = ExprRange(k, fk_i_to_j, m, n)
general_range_of_ranges = ExprTuple(ExprRange(k, ExprRange(l, Function(f, (k, l)),
Function(i, k), Function(j, k)), m, n))
range_len_conditions = ExprRange(k, InSet(Add(j_k, Neg(i_k), one), Natural), one, n)
range_len_sum = Add(ExprRange(k, Add(j_k, Neg(i_k), one), one, n))
shift_equiv = Equals([f_i_to_j],
[ExprRange(i, Function(f, Add(i, a)), k, l)])
f_i_to_j_dec.first()
f_i_to_j_dec.start_index
f_i_to_j_dec.get_styles()
f_i_to_j_dec
neg_shift_equiv = Equals([f_i_to_j_dec],
[ExprRange(i, Function(f, Add(i, a)), k, l, order='decreasing')])
shift_equiv_both = Equals([ExprRange(k, Function(f, Add(k, a)), i, j)],
[ExprRange(i, Function(f, Add(i, b)), k, l)])
neg_shift_equiv_both = Equals([ExprRange(k, Function(f, Add(k, a)), i, j, order='decreasing')],
[ExprRange(i, Function(f, Add(i, b)), k, l, order='decreasing')])
%end common