Expression of type Forall

from the theory of proveit.physics.quantum.QPE

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, Variable, VertExprArray, t
from proveit.logic import Equals, Forall
from proveit.numbers import Add, Interval, NaturalPos, one
from proveit.physics.quantum import ket_plus
from proveit.physics.quantum.QPE import QPE1, _U, _ket_u, _psi_t_ket, _s
from proveit.physics.quantum.circuits import Gate, Input, MultiQubitElem, Output, Qcircuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(t, one)
sub_expr3 = Add(t, _s)
sub_expr4 = Interval(sub_expr2, sub_expr3)
sub_expr5 = MultiQubitElem(element = Gate(operation = QPE1(_U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Forall(instance_param_or_params = [t], instance_expr = Equals(Prob(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr4), one, _s)], [ExprRange(sub_expr1, sub_expr5, one, t), ExprRange(sub_expr1, sub_expr5, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _psi_t_ket, part = sub_expr1), targets = Interval(one, t)), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr4), one, _s)]))), one), domain = NaturalPos)

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())

\forall_{t \in \mathbb{N}^+}~\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}_1\left(U, t\right)} & \multiqout{3}{\lvert \psi_{t} \rangle} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \ghostqout{\lvert \psi_{t} \rangle} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \ghostqout{\lvert \psi_{t} \rangle} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \ghostqout{\lvert \psi_{t} \rangle} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right)

stored_expr.style_options()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	None/False	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

# display the expression information
stored_expr.expr_info()

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