logo

Expression of type ExprTuple

from the theory of proveit.logic.booleans.disjunction

In [1]:
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 A, ExprRange, ExprTuple, IndexedVar, Variable, m, n
from proveit.core_expr_types import A_1_to_m
from proveit.logic import And, Boolean, Forall, InSet, Or
from proveit.numbers import Add, NaturalPos, one, two
In [2]:
# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = IndexedVar(A, one)
sub_expr3 = IndexedVar(A, sub_expr1)
sub_expr4 = Add(m, one)
sub_expr5 = ExprRange(sub_expr1, sub_expr3, one, n)
expr = ExprTuple(And(Forall(instance_param_or_params = [sub_expr2], instance_expr = InSet(sub_expr2, Boolean), domain = Boolean), Forall(instance_param_or_params = [m], instance_expr = Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr3, one, Add(m, two))], instance_expr = InSet(Or(ExprRange(sub_expr1, sub_expr3, one, sub_expr4)), Boolean), condition = ExprRange(sub_expr1, InSet(sub_expr3, Boolean), one, sub_expr4)), domain = NaturalPos, condition = Forall(instance_param_or_params = [A_1_to_m], instance_expr = InSet(Or(A_1_to_m), Boolean), domain = Boolean))), Forall(instance_param_or_params = [n], instance_expr = Forall(instance_param_or_params = [sub_expr5], instance_expr = InSet(Or(sub_expr5), Boolean), domain = Boolean), domain = NaturalPos))
expr:
In [3]:
# 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
In [4]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())
\left(\left[\forall_{A_{1} \in \mathbb{B}}~\left(A_{1} \in \mathbb{B}\right)\right] \land \left[\forall_{m \in \mathbb{N}^+~|~\forall_{A_{1}, A_{2}, \ldots, A_{m} \in \mathbb{B}}~\left(\left(A_{1} \lor  A_{2} \lor  \ldots \lor  A_{m}\right) \in \mathbb{B}\right)}~\left[\forall_{A_{1}, A_{2}, \ldots, A_{m + 2}~|~\left(A_{1} \in \mathbb{B}\right), \left(A_{2} \in \mathbb{B}\right), \ldots, \left(A_{m + 1} \in \mathbb{B}\right)}~\left(\left(A_{1} \lor  A_{2} \lor  \ldots \lor  A_{m + 1}\right) \in \mathbb{B}\right)\right]\right], \forall_{n \in \mathbb{N}^+}~\left[\forall_{A_{1}, A_{2}, \ldots, A_{n} \in \mathbb{B}}~\left(\left(A_{1} \lor  A_{2} \lor  \ldots \lor  A_{n}\right) \in \mathbb{B}\right)\right]\right)
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
wrap_positionsposition(s) at which wrapping is to occur; 'n' is after the nth comma.()()('with_wrapping_at',)
justificationif any wrap positions are set, justify to the 'left', 'center', or 'right'leftleft('with_justification',)
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0ExprTuple1, 2
1Operationoperator: 65
operands: 3
2Operationoperator: 40
operand: 7
3ExprTuple5, 6
4ExprTuple7
5Operationoperator: 40
operand: 12
6Operationoperator: 40
operand: 13
7Lambdaparameter: 67
body: 11
8ExprTuple12
9ExprTuple13
10ExprTuple67
11Conditionalvalue: 14
condition: 15
12Lambdaparameter: 30
body: 17
13Lambdaparameter: 81
body: 19
14Operationoperator: 40
operand: 25
15Operationoperator: 82
operands: 21
16ExprTuple30
17Conditionalvalue: 22
condition: 22
18ExprTuple81
19Conditionalvalue: 23
condition: 24
20ExprTuple25
21ExprTuple67, 47
22Operationoperator: 82
operands: 26
23Operationoperator: 40
operand: 31
24Operationoperator: 65
operands: 28
25Lambdaparameters: 55
body: 29
26ExprTuple30, 85
27ExprTuple31
28ExprTuple32, 33
29Conditionalvalue: 34
condition: 35
30IndexedVarvariable: 86
index: 80
31Lambdaparameters: 37
body: 38
32Operationoperator: 82
operands: 39
33Operationoperator: 40
operand: 48
34Operationoperator: 82
operands: 42
35Operationoperator: 65
operands: 43
36ExprTuple80
37ExprTuple44
38Conditionalvalue: 45
condition: 46
39ExprTuple81, 47
40Literal
41ExprTuple48
42ExprTuple49, 85
43ExprTuple50
44ExprRangelambda_map: 79
start_index: 80
end_index: 51
45Operationoperator: 82
operands: 52
46Operationoperator: 65
operands: 53
47Literal
48Lambdaparameters: 73
body: 54
49Operationoperator: 72
operands: 55
50ExprRangelambda_map: 74
start_index: 80
end_index: 67
51Operationoperator: 75
operands: 56
52ExprTuple57, 85
53ExprTuple58
54Conditionalvalue: 59
condition: 60
55ExprTuple61
56ExprTuple81, 62
57Operationoperator: 72
operands: 63
58ExprRangelambda_map: 74
start_index: 80
end_index: 71
59Operationoperator: 82
operands: 64
60Operationoperator: 65
operands: 66
61ExprRangelambda_map: 79
start_index: 80
end_index: 67
62Literal
63ExprTuple68
64ExprTuple69, 85
65Literal
66ExprTuple70
67Variable
68ExprRangelambda_map: 79
start_index: 80
end_index: 71
69Operationoperator: 72
operands: 73
70ExprRangelambda_map: 74
start_index: 80
end_index: 81
71Operationoperator: 75
operands: 76
72Literal
73ExprTuple77
74Lambdaparameter: 88
body: 78
75Literal
76ExprTuple81, 80
77ExprRangelambda_map: 79
start_index: 80
end_index: 81
78Operationoperator: 82
operands: 83
79Lambdaparameter: 88
body: 84
80Literal
81Variable
82Literal
83ExprTuple84, 85
84IndexedVarvariable: 86
index: 88
85Literal
86Variable
87ExprTuple88
88Variable