Expression of type Forall¶

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.
# import Expression classes needed to build the expression
from proveit import a, b, i, v, vb, vi
from proveit.logic import Equals, Forall
from proveit.numbers import Integer, Interval, Less, one, subtract

In [2]:
# build up the expression from sub-expressions
sub_expr1 = [i]
expr = Forall(instance_param_or_params = [v], instance_expr = Forall(instance_param_or_params = [a, b], instance_expr = Equals(VecSum(index_or_indices = sub_expr1, summand = vi, domain = Interval(a, b)), VecAdd(VecSum(index_or_indices = sub_expr1, summand = vi, domain = Interval(a, subtract(b, one))), vb)), domain = Integer, condition = Less(a, b)))

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_{v}~\left[\forall_{a, b \in \mathbb{Z}~|~a < b}~\left(\left(\sum_{i=a}^{b} v\left(i\right)\right) = \left(\left(\sum_{i=a}^{b - 1} v\left(i\right)\right) + v\left(b\right)\right)\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: 5
operand: 2
1ExprTuple2
2Lambdaparameter: 42
body: 4
3ExprTuple42
4Operationoperator: 5
operand: 7
5Literal
6ExprTuple7
7Lambdaparameters: 41
body: 8
8Conditionalvalue: 9
condition: 10
9Operationoperator: 11
operands: 12
10Operationoperator: 13
operands: 14
11Literal
12ExprTuple15, 16
13Literal
14ExprTuple17, 18, 19
15Operationoperator: 31
operand: 26
16Operationoperator: 21
operands: 22
17Operationoperator: 44
operands: 23
18Operationoperator: 44
operands: 24
19Operationoperator: 25
operands: 41
20ExprTuple26
21Literal
22ExprTuple27, 28
23ExprTuple50, 29
24ExprTuple54, 29
25Literal
26Lambdaparameter: 46
body: 30
27Operationoperator: 31
operand: 35
28Operationoperator: 42
operand: 54
29Literal
30Conditionalvalue: 39
condition: 34
31Literal
32ExprTuple35
33ExprTuple54
34Operationoperator: 44
operands: 36
35Lambdaparameter: 46
body: 37
36ExprTuple46, 38
37Conditionalvalue: 39
condition: 40
38Operationoperator: 48
operands: 41
39Operationoperator: 42
operand: 46
40Operationoperator: 44
operands: 45
41ExprTuple50, 54
42Variable
43ExprTuple46
44Literal
45ExprTuple46, 47
46Variable
47Operationoperator: 48
operands: 49
48Literal
49ExprTuple50, 51
50Variable
51Operationoperator: 52
operands: 53
52Literal
53ExprTuple54, 55
54Variable
55Operationoperator: 56
operand: 58
56Literal
57ExprTuple58
58Literal