Expression of type ExprTuple

from the theory of proveit.core_expr_types.tuples

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import ExprTuple, Lambda, a, b, f, i, j, k, l
from proveit.core_expr_types.tuples import shift_equiv_both
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Add, Integer, Natural, one, subtract

# build up the expression from sub-expressions
expr = ExprTuple(Lambda(f, Forall(instance_param_or_params = [a, b], instance_expr = Forall(instance_param_or_params = [i, j, k, l], instance_expr = shift_equiv_both, conditions = [InSet(subtract(Add(j, one), i), Natural), Equals(Add(i, a), Add(k, b)), Equals(Add(j, a), Add(l, b))]), domain = Integer)))

expr:

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left(f \mapsto \left[\forall_{a, b \in \mathbb{Z}}~\left[\forall_{i, j, k, l~|~\left(\left(j + 1\right) - i\right) \in \mathbb{N}, \left(i + a\right) = \left(k + b\right), \left(j + a\right) = \left(l + b\right)}~\left(\left(f\left(i + a\right), f\left(\left(i + 1\right) + a\right), \ldots, f\left(j + a\right)\right) = \left(f\left(k + b\right), f\left(\left(k + 1\right) + b\right), \ldots, f\left(l + b\right)\right)\right)\right]\right]\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	ExprTuple	1
1	Lambda	parameter: 55 body: 3
2	ExprTuple	55
3	Operation	operator: 10 operand: 5
4	ExprTuple	5
5	Lambda	parameters: 6 body: 7
6	ExprTuple	72, 74
7	Conditional	value: 8 condition: 9
8	Operation	operator: 10 operand: 13
9	Operation	operator: 24 operands: 12
10	Literal
11	ExprTuple	13
12	ExprTuple	14, 15
13	Lambda	parameters: 16 body: 17
14	Operation	operator: 33 operands: 18
15	Operation	operator: 33 operands: 19
16	ExprTuple	71, 69, 59, 60
17	Conditional	value: 20 condition: 21
18	ExprTuple	72, 22
19	ExprTuple	74, 22
20	Operation	operator: 36 operands: 23
21	Operation	operator: 24 operands: 25
22	Literal
23	ExprTuple	26, 27
24	Literal
25	ExprTuple	28, 29, 30
26	ExprTuple	31
27	ExprTuple	32
28	Operation	operator: 33 operands: 34
29	Operation	operator: 36 operands: 35
30	Operation	operator: 36 operands: 37
31	ExprRange	lambda_map: 38 start_index: 71 end_index: 69
32	ExprRange	lambda_map: 39 start_index: 59 end_index: 60
33	Literal
34	ExprTuple	40, 41
35	ExprTuple	42, 43
36	Literal
37	ExprTuple	44, 45
38	Lambda	parameter: 73 body: 46
39	Lambda	parameter: 73 body: 48
40	Operation	operator: 67 operands: 49
41	Literal
42	Operation	operator: 67 operands: 50
43	Operation	operator: 67 operands: 51
44	Operation	operator: 67 operands: 52
45	Operation	operator: 67 operands: 53
46	Operation	operator: 55 operand: 61
47	ExprTuple	73
48	Operation	operator: 55 operand: 62
49	ExprTuple	57, 58
50	ExprTuple	71, 72
51	ExprTuple	59, 74
52	ExprTuple	69, 72
53	ExprTuple	60, 74
54	ExprTuple	61
55	Variable
56	ExprTuple	62
57	Operation	operator: 67 operands: 63
58	Operation	operator: 64 operand: 71
59	Variable
60	Variable
61	Operation	operator: 67 operands: 66
62	Operation	operator: 67 operands: 68
63	ExprTuple	69, 70
64	Literal
65	ExprTuple	71
66	ExprTuple	73, 72
67	Literal
68	ExprTuple	73, 74
69	Variable
70	Literal
71	Variable
72	Variable
73	Variable
74	Variable