Common expressions for the theory of proveit

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

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

%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

a = Variable('a')

a:

b = Variable('b')

b:

c = Variable('c')

c:

d = Variable('d')

d:

e = Variable('e')

e:

f = Variable('f')

f:

g = Variable('g')

g:

h = Variable('h')

h:

i = Variable('i')

i:

j = Variable('j')

j:

k = Variable('k')

k:

l = Variable('l')

l:

m = Variable('m')

m:

n = Variable('n')

n:

o = Variable('o')

o:

p = Variable('p')

p:

q = Variable('q')

q:

r = Variable('r')

r:

s = Variable('s')

s:

t = Variable('t')

t:

u = Variable('u')

u:

v = Variable('v')

v:

w = Variable('w')

w:

x = Variable('x')

x:

y = Variable('y')

y:

z = Variable('z')

z:

A = Variable('A')

A:

B = Variable('B')

B:

C = Variable('C')

C:

D = Variable('D')

D:

E = Variable('E')

E:

F = Variable('F')

F:

G = Variable('G')

G:

H = Variable('H')

H:

I = Variable('I')

I:

J = Variable('J')

J:

K = Variable('K')

K:

L = Variable('L')

L:

M = Variable('M')

M:

N = Variable('N')

N:

O = Variable('O')

O:

P = Variable('P')

P:

Q = Variable('Q')

Q:

R = Variable('R')

R:

S = Variable('S')

S:

T = Variable('T')

T:

U = Variable('U')

U:

V = Variable('V')

V:

W = Variable('W')

W:

X = Variable('X')

X:

Y = Variable('Y')

Y:

Z = Variable('Z')

Z:

a_star = Variable('a_star', "a^*", fence_when_forced=True)

a_star:

b_star = Variable('b_star', "b^*", fence_when_forced=True)

b_star:

c_star = Variable('c_star', "c^*", fence_when_forced=True)

c_star:

d_star = Variable('d_star', "d^*", fence_when_forced=True)

d_star:

Am = Function(A,m)

Am:

b_of_j = Function(b, j)

b_of_j:

b_of_k = Function(b, k)

b_of_k:

Bm = Function(B,m)

Bm:

Cn = Function(C,n)

Cn:

PofA = Function(P, A)

PofA:

PofB = Function(P, B)

PofB:

Pk = Function(P, k)

Pk:

Px = Function(P, x)

Px:

Py = Function(P, y)

Py:

Pxy = Function(P, (x, y))

Pxy:

Pxyz = Function(P, (x, y, z))

Pxyz:

Pq = Function(P, q)

Pq:

QofA = Function(Q, A)

QofA:

Qx = Function(Q, x)

Qx:

Qy = Function(Q, y)

Qy:

Qz = Function(Q, z)

Qz:

Rx = Function(R, x)

Rx:

Ry = Function(R, y)

Ry:

Rz = Function(R, z)

Rz:

fa = Function(f, a)

fa:

fb = Function(f, b)

fb:

fab = Function(f, (a, b))

fab:

fi = Function(f, i)

fi:

fj = Function(f, j)

fj:

fij = Function(f, (i,j))

fij:

fx = Function(f, x)

fx:

fy = Function(f, y)

fy:

fz = Function(f, z)

fz:

fxy = Function(f, (x, y))

fxy:

gj = Function(g, j)

gj:

gx = Function(g, x)

gx:

gy = Function(g, y)

gy:

gz = Function(g, z)

gz:

pi = Function(p, i)

pi:

pj = Function(p, j)

pj:

pk = Function(p, k)

pk:

va = Function(v, a)

va:

vb = Function(v, b)

vb:

vi = Function(v, i)

vi:

vk = Function(v, k)

vk:

alpha = Variable('alpha', r'\alpha')

alpha:

beta = Variable('beta', r'\beta')

beta:

gamma = Variable('gamma', r'\gamma')

gamma:

delta = Variable('delta', r'\delta')

delta:

lambda_ = Variable('lambda', r'\lambda')

lambda_:

theta = Variable('theta', r'\theta')

theta:

eps = Variable('eps', r'\epsilon')

eps:

vareps = Variable('vareps', r'\varepsilon')

vareps:

rho = Variable('rho', r'\rho')

rho:

Psi = Variable('Psi', r'\Psi')

Psi:

Upsilon = Variable('Upsilon', r'\Upsilon')

Upsilon:

Omega = Variable('Omega', r'\Omega')

Omega:

a_prime = Variable("a'", fence_when_forced=True)

a_prime:

b_prime = Variable("b'", fence_when_forced=True)

Expression notebook is being updated for b'

b_prime:

%end common

gj expression notebook is being updated
Omega expression notebook is being updated
These common expressions may now be imported from the theory package: proveit