logo

Expression of type Forall

from the theory of proveit.numbers.numerals.decimals

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 ExprRange, IndexedVar, Variable, a, b, c, d, k, m, n
from proveit.logic import Equals, Forall
from proveit.numbers import DecimalSequence, Digits, Natural, one
In [2]:
# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = ExprRange(sub_expr1, b, one, n)
sub_expr3 = ExprRange(sub_expr1, IndexedVar(a, sub_expr1), one, m)
sub_expr4 = ExprRange(sub_expr1, IndexedVar(c, sub_expr1), one, n)
sub_expr5 = ExprRange(sub_expr1, IndexedVar(d, sub_expr1), one, k)
expr = Forall(instance_param_or_params = [m, n, k], instance_expr = Forall(instance_param_or_params = [sub_expr3, b, sub_expr4, sub_expr5], instance_expr = Equals(DecimalSequence(sub_expr3, sub_expr2, sub_expr5), DecimalSequence(sub_expr3, sub_expr4, sub_expr5)), domain = Digits, condition = Equals([sub_expr2], [sub_expr4])), domain = Natural)
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())
\forall_{m, n, k \in \mathbb{N}}~\left[\forall_{a_{1}, a_{2}, \ldots, a_{m}, b, c_{1}, c_{2}, \ldots, c_{n}, d_{1}, d_{2}, \ldots, d_{k} \in \mathbb{N}^{\leq 9}~|~\left(b, b, ..\left(n - 3\right) \times.., b\right) = \left(c_{1}, c_{2}, \ldots, c_{n}\right)}~\left(\texttt{\#}(a_{1}, a_{2}, \ldots, a_{m} ~ b, b, ..\left(n - 3\right) \times.., b ~ d_{1}, d_{2}, \ldots, d_{k}) = \texttt{\#}(a_{1}, a_{2}, \ldots, a_{m} ~ c_{1}, c_{2}, \ldots, c_{n} ~ d_{1}, d_{2}, \ldots, d_{k})\right)\right]
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
with_wrappingIf 'True', wrap the Expression after the parametersNoneNone/False('with_wrapping',)
condition_wrappingWrap 'before' or 'after' the condition (or None).NoneNone/False('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_paramsIf 'True', wraps every two parameters AND wraps the Expression after the parametersNoneNone/False('with_params',)
justificationjustify to the 'left', 'center', or 'right' in the array cellscentercenter('with_justification',)
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 7
operand: 2
1ExprTuple2
2Lambdaparameters: 3
body: 4
3ExprTuple49, 64, 51
4Conditionalvalue: 5
condition: 6
5Operationoperator: 7
operand: 10
6Operationoperator: 23
operands: 9
7Literal
8ExprTuple10
9ExprTuple11, 12, 13
10Lambdaparameters: 14
body: 15
11Operationoperator: 54
operands: 16
12Operationoperator: 54
operands: 17
13Operationoperator: 54
operands: 18
14ExprTuple41, 67, 57, 42
15Conditionalvalue: 19
condition: 20
16ExprTuple49, 21
17ExprTuple64, 21
18ExprTuple51, 21
19Operationoperator: 39
operands: 22
20Operationoperator: 23
operands: 24
21Literal
22ExprTuple25, 26
23Literal
24ExprTuple27, 28, 29, 30, 31
25Operationoperator: 33
operands: 32
26Operationoperator: 33
operands: 34
27ExprRangelambda_map: 35
start_index: 63
end_index: 49
28Operationoperator: 54
operands: 36
29ExprRangelambda_map: 37
start_index: 63
end_index: 64
30ExprRangelambda_map: 38
start_index: 63
end_index: 51
31Operationoperator: 39
operands: 40
32ExprTuple41, 56, 42
33Literal
34ExprTuple41, 57, 42
35Lambdaparameter: 71
body: 43
36ExprTuple67, 60
37Lambdaparameter: 71
body: 44
38Lambdaparameter: 71
body: 45
39Literal
40ExprTuple46, 47
41ExprRangelambda_map: 48
start_index: 63
end_index: 49
42ExprRangelambda_map: 50
start_index: 63
end_index: 51
43Operationoperator: 54
operands: 52
44Operationoperator: 54
operands: 53
45Operationoperator: 54
operands: 55
46ExprTuple56
47ExprTuple57
48Lambdaparameter: 71
body: 58
49Variable
50Lambdaparameter: 71
body: 59
51Variable
52ExprTuple58, 60
53ExprTuple68, 60
54Literal
55ExprTuple59, 60
56ExprRangelambda_map: 61
start_index: 63
end_index: 64
57ExprRangelambda_map: 62
start_index: 63
end_index: 64
58IndexedVarvariable: 65
index: 71
59IndexedVarvariable: 66
index: 71
60Literal
61Lambdaparameter: 71
body: 67
62Lambdaparameter: 71
body: 68
63Literal
64Variable
65Variable
66Variable
67Variable
68IndexedVarvariable: 69
index: 71
69Variable
70ExprTuple71
71Variable