These are archival webpages, generated on 2023-03-20 by Prove-It Beta Version 0.3, licensed under the GNU Public Licence by Sandia Corporation. See pyproveit.org for the lastest version.
logo

Common expressions for the theory of proveit

These are generic common expressions based upon single-symbol Variable names.

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 Variable, Function
#%begin common
In [2]:
%begin common
Defining common sub-expressions for theory 'proveit'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions
In [3]:
a = Variable('a')
a:
In [4]:
b = Variable('b')
b:
In [5]:
c = Variable('c')
c:
In [6]:
d = Variable('d')
d:
In [7]:
e = Variable('e')
e:
In [8]:
f = Variable('f')
f:
In [9]:
g = Variable('g')
g:
In [10]:
h = Variable('h')
h:
In [11]:
i = Variable('i')
i:
In [12]:
j = Variable('j')
j:
In [13]:
k = Variable('k')
k:
In [14]:
l = Variable('l')
l:
In [15]:
m = Variable('m')
m:
In [16]:
n = Variable('n')
n:
In [17]:
o = Variable('o')
o:
In [18]:
p = Variable('p')
p:
In [19]:
q = Variable('q')
q:
In [20]:
r = Variable('r')
r:
In [21]:
s = Variable('s')
s:
In [22]:
t = Variable('t')
t:
In [23]:
u = Variable('u')
u:
In [24]:
v = Variable('v')
v:
In [25]:
w = Variable('w')
w:
In [26]:
x = Variable('x')
x:
In [27]:
y = Variable('y')
y:
In [28]:
z = Variable('z')
z:
In [29]:
A = Variable('A')
A:
In [30]:
B = Variable('B')
B:
In [31]:
C = Variable('C')
C:
In [32]:
D = Variable('D')
D:
In [33]:
E = Variable('E')
E:
In [34]:
F = Variable('F')
F:
In [35]:
G = Variable('G')
G:
In [36]:
H = Variable('H')
H:
In [37]:
I = Variable('I')
I:
In [38]:
J = Variable('J')
J:
In [39]:
K = Variable('K')
K:
In [40]:
L = Variable('L')
L:
In [41]:
M = Variable('M')
M:
In [42]:
N = Variable('N')
N:
In [43]:
O = Variable('O')
O:
In [44]:
P = Variable('P')
P:
In [45]:
Q = Variable('Q')
Q:
In [46]:
R = Variable('R')
R:
In [47]:
S = Variable('S')
S:
In [48]:
T = Variable('T')
T:
In [49]:
U = Variable('U')
U:
In [50]:
V = Variable('V')
V:
In [51]:
W = Variable('W')
W:
In [52]:
X = Variable('X')
X:
In [53]:
Y = Variable('Y')
Y:
In [54]:
Z = Variable('Z')
Z:
In [55]:
a_star = Variable('a_star', "a^*", fence_when_forced=True)
a_star:
In [56]:
b_star = Variable('b_star', "b^*", fence_when_forced=True)
b_star:
In [57]:
c_star = Variable('c_star', "c^*", fence_when_forced=True)
c_star:
In [58]:
d_star = Variable('d_star', "d^*", fence_when_forced=True)
d_star:
In [59]:
Am = Function(A,m)
Am:
In [60]:
b_of_j = Function(b, j)
b_of_j:
In [61]:
b_of_k = Function(b, k)
b_of_k:
In [62]:
Bm = Function(B,m)
Bm:
In [63]:
Cn = Function(C,n)
Cn:
In [64]:
PofA = Function(P, A)
PofA:
In [65]:
PofB = Function(P, B)
PofB:
In [66]:
Pk = Function(P, k)
Pk:
In [67]:
Px = Function(P, x)
Px:
In [68]:
Py = Function(P, y)
Py:
In [69]:
Pxy = Function(P, (x, y))
Pxy:
In [70]:
Pxyz = Function(P, (x, y, z))
Pxyz:
In [71]:
Pq = Function(P, q)
Pq:
In [72]:
QofA = Function(Q, A)
QofA:
In [73]:
Qx = Function(Q, x)
Qx:
In [74]:
Qy = Function(Q, y)
Qy:
In [75]:
Qz = Function(Q, z)
Qz:
In [76]:
Rx = Function(R, x)
Rx:
In [77]:
Ry = Function(R, y)
Ry:
In [78]:
Rz = Function(R, z)
Rz:
In [79]:
fa = Function(f, a)
fa:
In [80]:
fb = Function(f, b)
fb:
In [81]:
fab = Function(f, (a, b))
fab:
In [82]:
fi = Function(f, i)
fi:
In [83]:
fj = Function(f, j)
fj:
In [84]:
fij = Function(f, (i,j))
fij:
In [85]:
fx = Function(f, x)
fx:
In [86]:
fy = Function(f, y)
fy:
In [87]:
fz = Function(f, z)
fz:
In [88]:
fxy = Function(f, (x, y))
fxy:
In [89]:
gj = Function(g, j)
gj:
In [90]:
gx = Function(g, x)
gx:
In [91]:
gy = Function(g, y)
gy:
In [92]:
gz = Function(g, z)
gz:
In [93]:
pi = Function(p, i)
pi:
In [94]:
pj = Function(p, j)
pj:
In [95]:
pk = Function(p, k)
pk:
In [96]:
va = Function(v, a)
va:
In [97]:
vb = Function(v, b)
vb:
In [98]:
vi = Function(v, i)
vi:
In [99]:
vk = Function(v, k)
vk:
In [100]:
alpha = Variable('alpha', r'\alpha')
alpha:
In [101]:
beta = Variable('beta', r'\beta')
beta:
In [102]:
gamma = Variable('gamma', r'\gamma')
gamma:
In [103]:
delta = Variable('delta', r'\delta')
delta:
In [104]:
lambda_ = Variable('lambda', r'\lambda')
lambda_:
In [105]:
theta = Variable('theta', r'\theta')
theta:
In [106]:
eps = Variable('eps', r'\epsilon')
eps:
In [107]:
vareps = Variable('vareps', r'\varepsilon')
vareps:
In [108]:
rho = Variable('rho', r'\rho')
rho:
In [109]:
Psi = Variable('Psi', r'\Psi')
Psi:
In [110]:
Upsilon = Variable('Upsilon', r'\Upsilon')
Upsilon:
In [111]:
Omega = Variable('Omega', r'\Omega')
Omega:
In [112]:
a_prime = Variable("a'", fence_when_forced=True)
a_prime:
In [113]:
b_prime = Variable("b'", fence_when_forced=True)
b_prime:
In [114]:
%end common
These common expressions may now be imported from the theory package: proveit