logo

Common expressions for the theory of proveit.core_expr_types.expr_arrays

In [1]:
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 IndexedVar, var_range, var_array, vert_var_array
from proveit import A, B, C, D, E, P, Q, R, S, T, U, V, g, h, i, j, k, l, m, n 
from proveit.numbers import one
In [2]:
%begin common

Defining common sub-expressions for theory 'proveit.core_expr_types.expr_arrays'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions
In [3]:
Aij = IndexedVar(A, [i, j])
Aij:
In [4]:
Bij = IndexedVar(B,(i,j))
Bij:
In [5]:
Cij = IndexedVar(C,(i,j))
Cij:
In [6]:
Dij = IndexedVar(D,(i,j))
Dij:
In [7]:
Eij = IndexedVar(E,(i,j))
Eij:
In [8]:
Pij = IndexedVar(P,(i,j))
Pij:
In [9]:
Qij = IndexedVar(Q,(i,j))
Qij:
In [10]:
Rij = IndexedVar(R,(i,j))
Rij:
In [11]:
Sij = IndexedVar(S,(i,j))
Sij:
In [12]:
Tij = IndexedVar(T,(i,j))
Tij:
In [13]:
Uij = IndexedVar(U,(i,j))
Uij:
In [14]:
Vij = IndexedVar(V,(i,j))
Vij:
In [15]:
A11_to_Akm = var_range(A, [one, one], [k, m])
A11_to_Akm:
In [16]:
A11_to_Akl = var_range(A, [one, one], [k, l])
A11_to_Akl:
In [17]:
A11_to_Akl_array = var_array(A, [one, one], [k, l])
A11_to_Akl_array:
In [18]:
A11_to_Akl_varray = vert_var_array(A, [one, one], [k, l])
A11_to_Akl_varray:
In [19]:
A11_to_Amn = var_range(A, [one, one], [m, n])
A11_to_Amn:
In [20]:
B11_to_Bkl  = var_range(B, [one, one], [k, l])
B11_to_Bkl:
In [21]:
B11_to_Bkm = var_range(B, [one, one], [k, m])
B11_to_Bkm:
In [22]:
B11_to_Bkn = var_range(B, [one, one], [k, n])
B11_to_Bkn:
In [23]:
B11_to_Bmn = var_range(B, [one, one], [m, n])
B11_to_Bmn:
In [24]:
B11_to_Bkl_array = var_array(B, [one, one], [k, l])
B11_to_Bkl_array:
In [25]:
B11_to_Bkl_varray = vert_var_array(B, [one, one], [k, l])
B11_to_Bkl_varray:
In [26]:
C11_to_Ckn = var_range(C, [one, one], [k, n])
C11_to_Ckn:
In [27]:
C11_to_Cmn = var_range(C, [one, one], [m, n])
C11_to_Cmn:
In [28]:
C11_to_Clm = var_range(C, [one, one], [l, m])
C11_to_Clm:
In [29]:
C11_to_Ckm = var_range(C, [one, one], [k, m])
C11_to_Ckm:
In [30]:
D11_to_Dkm = var_range(D, [one, one], [k, m])
D11_to_Dkm:
In [31]:
D11_to_Dkn = var_range(D, [one, one], [k, n])
D11_to_Dkn:
In [32]:
D11_to_Dmn = var_range(D, [one, one], [m, n])
D11_to_Dmn:
In [33]:
R11_to_Rkm = var_range(R, [one, one], [k, m])
R11_to_Rkm:
In [34]:
S11_to_Skm = var_range(S, [one, one], [k, m])
S11_to_Skm:
In [35]:
S11_to_Skn = var_range(S, [one, one], [k, n])
S11_to_Skn:
In [36]:
S11_to_Smn = var_range(S, [one, one], [m, n])
S11_to_Smn:
In [37]:
T11_to_Tkm = var_range(T, [one, one], [k, m])
T11_to_Tkm:
In [38]:
T11_to_Tlm = var_range(T, [one, one], [l, m])
T11_to_Tlm:
In [39]:
U11_to_Ukm = var_range(U, [one, one], [k, m])
U11_to_Ukm:
In [40]:
U11_to_Ukn = var_range(U, [one, one], [k, n])
U11_to_Ukn:
In [41]:
V11_to_Vkm = var_range(V, [one, one], [k, m])
V11_to_Vkm:
In [42]:
%end common

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