Expression of type Conditional ¶

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 Conditional, a, b, i, j, k, l
from proveit.core_expr_types.tuples import neg_shift_equiv_both
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Add, Integer, Natural, one, subtract

# build up the expression from sub-expressions
expr = Conditional(Forall(instance_param_or_params = [i, j, k, l], instance_expr = neg_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))]), And(InSet(a, Integer), InSet(b, Integer)))

# 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\{\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) \textrm{ if } a \in \mathbb{Z} ,  b \in \mathbb{Z}\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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

Expression of type Conditional¶

from the theory of proveit.core_expr_types.tuples¶

Expression of type Conditional ¶

from the theory of proveit.core_expr_types.tuples ¶