Common expressions for the theory of proveit.core_expr_types

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 ExprTuple, IndexedVar, Function, ExprRange, var_range
from proveit import (a, b, c, d, e, f, g, i, j, k, l, m, n, 
                     v, w, x, y, z, A, B, C, D, P, Q, R, S, U, V, W,
                     fa, fx, gx, Pk, alpha, lambda_)
from proveit.numbers import zero, one, two, Add, frac, Neg, subtract
from proveit.logic import Equals, Implies
from proveit.core_expr_types import Len

%begin common

Defining common sub-expressions for theory 'proveit.core_expr_types'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions

a_k = IndexedVar(a, k)

a_k:

a_1_to_i = var_range(a, one, i)

a_1_to_i:

a_1_to_ip1 = var_range(a, one, Add(i, one))

a_1_to_ip1:

a_1_to_j = var_range(a, one, j)

a_1_to_j:

a_1_to_k = var_range(a, one, k)

a_1_to_k:

a_1_to_m = var_range(a, one, m)

a_1_to_m:

a_1_to_n = var_range(a, one, n)

a_1_to_n:

a_i_to_j = var_range(a, i, j)

a_i_to_j:

a_1_to_0 = var_range(a, one, zero)

a_1_to_0:

a_i = IndexedVar(a, i)

a_i:

a_ip1 = IndexedVar(a, Add(i, one))

a_ip1:

alpha_k = IndexedVar(alpha, k)

alpha_k:

bj = IndexedVar(b, j)

bj:

b_i = IndexedVar(b, i)

b_i:

b_1_to_i = var_range(b, one, i)

b_1_to_i:

b_1_to_ip1 = var_range(b, one, Add(i, one))

b_1_to_ip1:

b_1_to_j = var_range(b, one, j)

b_1_to_j:

b_1_to_k = var_range(b, one, k)

b_1_to_k:

b_1_to_m = var_range(b, one, m)

b_1_to_m:

b_1_to_n = var_range(b, one, n)

b_1_to_n:

b_j_to_k = var_range(b, j, k)

b_j_to_k:

b_ip1 = IndexedVar(b, Add(i, one))

b_ip1:

b_kp1 = IndexedVar(b, Add(k, one))

b_kp1:

b_j_to_kp1 = var_range(b, j, Add(k, one))

b_j_to_kp1:

c_i = IndexedVar(c, i)

c_i:

c_1_to_i = var_range(c, one, i)

c_1_to_i:

c_1_to_j = var_range(c, one, j)

c_1_to_j:

c_1_to_k = var_range(c, one, k)

c_1_to_k:

c_1_to_n = var_range(c, one, n)

c_1_to_n:

d_1_to_i = var_range(d, one, i)

d_1_to_i:

d_1_to_j = var_range(d, one, j)

d_1_to_j:

d_1_to_k = var_range(d, one, k)

d_1_to_k:

e_1_to_i = var_range(e, one, i)

e_1_to_i:

e_1_to_j = var_range(e, one, j)

e_1_to_j:

e_1_to_k = var_range(e, one, k)

e_1_to_k:

f_1_to_k = var_range(f, one, k)

f_1_to_k:

f_k = IndexedVar(f, k)

f_k:

i_k = IndexedVar(i, k)

i_k:

j_k = IndexedVar(j, k)

j_k:

n_k = IndexedVar(n, k)

n_k:

i_1_to_m = var_range(i, one, m)

i_1_to_m:

i_1_to_n = var_range(i, one, n)

i_1_to_n:

j_1_to_m = var_range(j, one, m)

j_1_to_m:

j_1_to_n = var_range(j, one, n)

j_1_to_n:

k_1_to_m = var_range(k, one, m)

k_1_to_m:

n_1_to_m = var_range(n, one, m)

n_1_to_m:

v_i = IndexedVar(v, i)

v_i:

v_j = IndexedVar(v, j)

v_j:

w_i = IndexedVar(w, i)

w_i:

w_j = IndexedVar(w, j)

w_j:

V_i = IndexedVar(V, i)

V_i:

V_j = IndexedVar(V, j)

V_j:

v_1_to_m = var_range(v, one, m)

v_1_to_m:

v_1_to_n = var_range(v, one, n)

v_1_to_n:

W_i = IndexedVar(W, i)

W_i:

w_1_to_m = var_range(w, one, m)

w_1_to_m:

w_1_to_n = var_range(w, one, n)

w_1_to_n:

x_i = IndexedVar(x, i)

x_i:

x_j = IndexedVar(x, j)

x_j:

x_k = IndexedVar(x, k)

x_k:

A_k = IndexedVar(A, k)

A_k:

x_1_to_i = var_range(x, one, i)

x_1_to_i:

x_1_to_j = var_range(x, one, j)

x_1_to_j:

x_1_to_k = var_range(x, one, k)

x_1_to_k:

x_1_to_m = var_range(x, one, m)

x_1_to_m:

x_1_to_n = var_range(x, one, n)

x_1_to_n:

x_1_to_np1 = var_range(x, one, Add(n, one))

x_1_to_np1:

y_1_to_j = var_range(y, one, j)

y_1_to_j:

y_1_to_l = var_range(y, one, l)

y_1_to_l:

y_1_to_n = var_range(y, one, n)

y_1_to_n:

y_1_to_m = var_range(y, one, m)

y_1_to_m:

z_1_to_k = var_range(z, one, k)

z_1_to_k:

z_1_to_n = var_range(z, one, n)

z_1_to_n:

range_1_to_i = ExprRange(k, k, one, i)

range_1_to_i:

range_1_to_ip1 = ExprRange(k, k, one, Add(i, one))

range_1_to_ip1:

range_i_to_j = ExprRange(k, k, i, j)

range_i_to_j:

range_i_to_jp1 = ExprRange(k, k, i, Add(j, one))

range_i_to_jp1:

range_1_to_mp1 = ExprRange(k, k, one, Add(m, one))

range_1_to_mp1:

f__a_1_to_i = Function(f, a_1_to_i)

f__a_1_to_i:

g__a_1_to_i = Function(g, a_1_to_i)

g__a_1_to_i:

f__b_1_to_i = Function(f, b_1_to_i)

f__b_1_to_i:

f__b_1_to_j = Function(f, b_1_to_j)

f__b_1_to_j:

g__c_1_to_i = Function(g, c_1_to_i)

g__c_1_to_i:

f__x_1_to_n = Function(f, x_1_to_n)

f__x_1_to_n:

f__y_1_to_n = Function(f, y_1_to_n)

f__y_1_to_n:

g__x_1_to_n = Function(g, x_1_to_n)

g__x_1_to_n:

g__y_1_to_n = Function(g, y_1_to_n)

g__y_1_to_n:

A_i = IndexedVar(A, i)

A_i:

A_1_to_i = var_range(A, one, i)

A_1_to_i:

A_1_to_j = var_range(A, one, j)

A_1_to_j:

A_1_to_l = var_range(A, one, l)

A_1_to_l:

A_i_to_j = var_range(A, i, j)

A_i_to_j:

A_1_to_k = var_range(A, one, k)

A_1_to_k:

A_1_to_l = var_range(A, one, l)

A_1_to_l:

A_1_to_m = var_range(A, one, m)

A_1_to_m:

A_1_to_n = var_range(A, one, n)

A_1_to_n:

B_1_to_i = var_range(B, one, i)

B_1_to_i:

B_1_to_j = var_range(B, one, j)

B_1_to_j:

B_1_to_k = var_range(B, one, k)

B_1_to_k:

B_1_to_m = var_range(B, one, m)

B_1_to_m:

B_1_to_n = var_range(B, one, n)

B_1_to_n:

C_1_to_k = var_range(C, one, k)

C_1_to_k:

C_1_to_l = var_range(C, one, l)

C_1_to_l:

C_1_to_m = var_range(C, one, m)

C_1_to_m:

C_1_to_n = var_range(C, one, n)

C_1_to_n:

D_1_to_m = var_range(D, one, m)

D_1_to_m:

D_1_to_n = var_range(D, one, n)

D_1_to_n:

Q_1_to_m = var_range(Q, one, m)

Q_1_to_m:

R_1_to_n = var_range(R, one, n)

R_1_to_n:

S_1_to_n = var_range(S, one, n)

S_1_to_n:

U_1_to_i = var_range(U, one, i)

U_1_to_i:

U_1_to_m = var_range(U, one, m)

U_1_to_m:

V_1_to_i = var_range(V, one, i)

V_1_to_i:

V_1_to_j = var_range(V, one, j)

V_1_to_j:

V_1_to_n = var_range(V, one, n)

V_1_to_n:

W_1_to_k = var_range(W, one, k)

W_1_to_k:

W_1_to_n = var_range(W, one, n)

W_1_to_n:

lambda_i = IndexedVar(lambda_, i)

lambda_i:

P__x_1_to_n = Function(P, x_1_to_n)

P__x_1_to_n:

P__y_1_to_n = Function(P, y_1_to_n)

P__y_1_to_n:

P__x_1_to_m_y_1_to_n = Function(P, [x_1_to_m, y_1_to_n])

P__x_1_to_m_y_1_to_n:

P__x_1_to_np1 = Function(P, x_1_to_np1)

P__x_1_to_np1:

Q__x_1_to_n = Function(Q, x_1_to_n)

Q__x_1_to_n:

Q__x_1_to_m = Function(Q, x_1_to_m)

Q__x_1_to_m:

Q__y_1_to_n = Function(Q, y_1_to_n)

Q__y_1_to_n:

Q__z_1_to_n = Function(Q, z_1_to_n)

Q__z_1_to_n:

Q__a_1_to_i = Function(Q, a_1_to_i)

Q__a_1_to_i:

Q__b_1_to_i = Function(Q, b_1_to_i)

Q__b_1_to_i:

Q__c_1_to_i = Function(Q, c_1_to_i)

Q__c_1_to_i:

R__x_1_to_n = Function(R, x_1_to_n)

R__x_1_to_n:

R__y_1_to_n = Function(R, y_1_to_n)

R__y_1_to_n:

R__y_1_to_m = Function(R, y_1_to_m)

R__y_1_to_m:

R__x_1_to_m_y_1_to_n = Function(R, [x_1_to_m, y_1_to_n])

R__x_1_to_m_y_1_to_n:

R__z_1_to_n = Function(R, z_1_to_n)

R__z_1_to_n:

fi = Function(f, i)

fi:

fj = Function(f, j)

fj:

fk = Function(f, k)

fk:

f_jp1 = Function(f, Add(j, one))

f_jp1:

f_1_to_n = var_range(f, one, n)

f_1_to_n:

f_m_to_n = var_range(f, m, n)

f_m_to_n:

f_1_to_i = ExprRange(a, fa, one, i)

f_1_to_i:

f_1_to_j = ExprRange(a, fa, one, j)

f_1_to_j:

f_i_to_j = ExprRange(a, fa, i, j)

f_i_to_j:

f_i_to_j_dec = ExprRange(a, fa, i, j, order='decreasing')

f_i_to_j_dec:

f_i_to_jp1 = ExprRange(a, fa, i, Add(j, one))

f_i_to_jp1:

f_i_to_jm1 = ExprRange(a, fa, i, subtract(j, one))

f_i_to_jm1:

f_i_to_k = ExprRange(a, fa, i, k)

f_i_to_k:

f_i_to_l = ExprRange(a, fa, i, l)

f_i_to_l:

f_j_to_k = ExprRange(a, fa, j, k)

f_j_to_k:

f_k_to_l = ExprRange(a, fa, k, l)

f_k_to_l:

f_ip1_to_j = ExprRange(a, fa, Add(i, one), j)

f_ip1_to_j:

f_jp1_to_k = ExprRange(a, fa, Add(j, one), k)

f_jp1_to_k:

gi = Function(g, i)

gi:

gk = Function(g, k)

gk:

gj = Function(g, j)

gj:

g_i_to_j = ExprRange(x, gx, i, j)

g_i_to_j:

g_k_to_l = ExprRange(x, gx, k, l)

g_k_to_l:

Q__b_1_to_j = Function(Q, b_1_to_j)

Q__b_1_to_j:

Pk_1_to_n = ExprRange(k, Pk, one, n)

Pk_1_to_n:

Pk_a1_to_an = ExprRange(k, Function(P, IndexedVar(a, k)), one, n)

Pk_a1_to_an:

Qk_a1_to_an = ExprRange(k, Function(Q, IndexedVar(a, k)), one, n)

Qk_a1_to_an:

Qk_implies_Pk_a1_to_an = ExprRange(k, Implies( Function(Q, IndexedVar(a, k)), Function(P, IndexedVar(a, k))), one, n)

Qk_implies_Pk_a1_to_an:

xk_over_y_1_to_n = ExprRange(k, frac(IndexedVar(x, k), y), one, n)

xk_over_y_1_to_n:

i_to_j_len = Add(j, Neg(i), one)

i_to_j_len:

j_to_k_len = Add(k, Neg(j), one)

j_to_k_len:

k_to_l_len = Add(l, Neg(k), one)

k_to_l_len:

tuple_len_incr_equiv = Equals(Len([a_1_to_i, b]),
                             Add(Len([a_1_to_i]), one)) \
    .with_wrap_after_operator()

tuple_len_incr_equiv:

concat_len_equiv = Equals(Len([a_1_to_i, f_j_to_k]),
                          Add(i, k, Neg(j), one)) \
    .with_wrap_after_operator()

concat_len_equiv:

concat_len_simple_equiv = Equals(Len([a_1_to_i, f_1_to_j]),
                                 Add(i, j)) \
    .with_wrap_after_operator()

concat_len_simple_equiv:

iter_ext_equiv = Equals(ExprTuple(f_i_to_jp1),
                        ExprTuple(f_i_to_j, f_jp1))\
    .with_wrap_after_operator()

iter_ext_equiv:

partition_equiv = Equals(ExprTuple(f_i_to_k),
                         ExprTuple(f_i_to_j, f_jp1_to_k))\
    .with_wrap_after_operator()

partition_equiv:

merge_equiv = Equals(ExprTuple(f_i_to_j, f_k_to_l),
                     ExprTuple(f_i_to_l))\
    .with_wrap_after_operator()

merge_equiv:

partition_front_equiv = Equals(ExprTuple(f_i_to_j),
                               ExprTuple(fi, f_ip1_to_j))\
    .with_wrap_after_operator()

partition_front_equiv:

merge_front_equiv = Equals(ExprTuple(fi, f_j_to_k),
                           ExprTuple(f_i_to_k))\
    .with_wrap_after_operator()

merge_front_equiv:

partition_back_equiv = Equals(ExprTuple(f_i_to_j),
                              ExprTuple(f_i_to_jm1, fj))\
    .with_wrap_after_operator()

partition_back_equiv:

merge_back_equiv = Equals(ExprTuple(f_i_to_j, fk),
                          ExprTuple(f_i_to_k))\
    .with_wrap_after_operator()

merge_back_equiv:

x_0_to_jmi = ExprRange(i, IndexedVar(x, i), zero, subtract(j, i))

x_0_to_jmi:

merge_series_conditions = \
    ExprRange(k, Equals(IndexedVar(x, k), Function(f, Add(i, k))),
              zero, subtract(j, i))

merge_series_conditions:

merge_series_equiv = Equals(ExprTuple(x_0_to_jmi),
                            ExprTuple(f_i_to_j))\
    .with_wrap_after_operator()

merge_series_equiv:

x_eq_y__1_to_n = ExprRange(k, Equals(IndexedVar(x, k), IndexedVar(y, k)), one, n)

x_eq_y__1_to_n:

%end common

These common expressions may now be imported from the theory package: proveit.core_expr_types