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, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Add, Exp, Interval, IntervalCO, Mult, NaturalPos, Real, e, i, one, pi, subtract, two, zero
from proveit.physics.quantum import I, NumKet, Z, ket_plus, normalized_var_ket_u, var_ket_u
from proveit.physics.quantum.QPE import QPE, phase, s_ket_domain, two_pow_s, two_pow_t
from proveit.physics.quantum.circuits import Gate, Input, Measure, 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 = Mult(two_pow_t, phase)
sub_expr6 = MultiQubitElem(element = Gate(operation = QPE(U, t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = Forall(instance_param_or_params = [s, t], instance_expr = Forall(instance_param_or_params = [U], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [phase], 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 = var_ket_u, part = sub_expr1), targets = sub_expr4), one, s)], [ExprRange(sub_expr1, sub_expr6, one, t), ExprRange(sub_expr1, sub_expr6, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, t), ExprRange(sub_expr1, Gate(operation = I).with_implicit_representation(), one, s)], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(sub_expr5, t), part = sub_expr1), targets = Interval(one, t)), one, t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = var_ket_u, part = sub_expr1), targets = sub_expr4), one, s)]))), one), domain = Real, conditions = [InSet(sub_expr5, Interval(zero, subtract(two_pow_t, one))), Equals(MatrixMult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, phase)), var_ket_u)), InSet(phase, IntervalCO(zero, one))]), domain = s_ket_domain, condition = normalized_var_ket_u), domain = Unitary(two_pow_s)), 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_{s, t \in \mathbb{N}^+}~\left[\forall_{U \in \textrm{U}\left(2^{s}\right)}~\left[\forall_{\lvert u \rangle \in \mathbb{C}^{2^{s}}~|~\left \|\lvert u \rangle\right \| = 1}~\left[\forall_{\varphi \in \mathbb{R}~|~\left(2^{t} \cdot \varphi\right) \in \{0~\ldotp \ldotp~2^{t} - 1\}, \left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right), \varphi \in \left[0,1\right)}~\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}\left(U, t\right)} & \measure{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert 2^{t} \cdot \varphi \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right)\right]\right]\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: 28 operand: 2
1	ExprTuple	2
2	Lambda	parameters: 3 body: 4
3	ExprTuple	168, 176
4	Conditional	value: 5 condition: 6
5	Operation	operator: 28 operand: 9
6	Operation	operator: 43 operands: 8
7	ExprTuple	9
8	ExprTuple	10, 11
9	Lambda	parameter: 165 body: 13
10	Operation	operator: 62 operands: 14
11	Operation	operator: 62 operands: 15
12	ExprTuple	165
13	Conditional	value: 16 condition: 17
14	ExprTuple	168, 18
15	ExprTuple	176, 18
16	Operation	operator: 28 operand: 21
17	Operation	operator: 62 operands: 20
18	Literal
19	ExprTuple	21
20	ExprTuple	165, 22
21	Lambda	parameter: 154 body: 23
22	Operation	operator: 24 operand: 55
23	Conditional	value: 26 condition: 27
24	Literal
25	ExprTuple	55
26	Operation	operator: 28 operand: 31
27	Operation	operator: 43 operands: 30
28	Literal
29	ExprTuple	31
30	ExprTuple	32, 33
31	Lambda	parameter: 172 body: 35
32	Operation	operator: 62 operands: 36
33	Operation	operator: 60 operands: 37
34	ExprTuple	172
35	Conditional	value: 38 condition: 39
36	ExprTuple	154, 40
37	ExprTuple	41, 167
38	Operation	operator: 60 operands: 42
39	Operation	operator: 43 operands: 44
40	Operation	operator: 45 operands: 46
41	Operation	operator: 47 operand: 154
42	ExprTuple	49, 167
43	Literal
44	ExprTuple	50, 51, 52, 53
45	Literal
46	ExprTuple	54, 55
47	Literal
48	ExprTuple	154
49	Operation	operator: 56 operand: 65
50	Operation	operator: 62 operands: 58
51	Operation	operator: 62 operands: 59
52	Operation	operator: 60 operands: 61
53	Operation	operator: 62 operands: 63
54	Literal
55	Operation	operator: 173 operands: 64
56	Literal
57	ExprTuple	65
58	ExprTuple	172, 66
59	ExprTuple	166, 67
60	Literal
61	ExprTuple	68, 69
62	Literal
63	ExprTuple	172, 70
64	ExprTuple	175, 168
65	Operation	operator: 71 operands: 72
66	Literal
67	Operation	operator: 149 operands: 73
68	Operation	operator: 74 operands: 75
69	Operation	operator: 76 operands: 77
70	Operation	operator: 78 operands: 79
71	Literal
72	ExprTuple	80, 81, 82, 83
73	ExprTuple	86, 84
74	Literal
75	ExprTuple	165, 154
76	Literal
77	ExprTuple	85, 154
78	Literal
79	ExprTuple	86, 167
80	ExprTuple	87, 88
81	ExprTuple	89, 90
82	ExprTuple	91, 92
83	ExprTuple	93, 94
84	Operation	operator: 163 operands: 95
85	Operation	operator: 173 operands: 96
86	Literal
87	ExprRange	lambda_map: 97 start_index: 167 end_index: 176
88	ExprRange	lambda_map: 98 start_index: 167 end_index: 168
89	ExprRange	lambda_map: 99 start_index: 167 end_index: 176
90	ExprRange	lambda_map: 99 start_index: 156 end_index: 157
91	ExprRange	lambda_map: 100 start_index: 167 end_index: 176
92	ExprRange	lambda_map: 101 start_index: 167 end_index: 168
93	ExprRange	lambda_map: 102 start_index: 167 end_index: 176
94	ExprRange	lambda_map: 103 start_index: 167 end_index: 168
95	ExprTuple	171, 104
96	ExprTuple	105, 106
97	Lambda	parameter: 155 body: 107
98	Lambda	parameter: 155 body: 108
99	Lambda	parameter: 155 body: 109
100	Lambda	parameter: 155 body: 110
101	Lambda	parameter: 155 body: 111
102	Lambda	parameter: 155 body: 112
103	Lambda	parameter: 155 body: 114
104	Operation	operator: 115 operand: 167
105	Literal
106	Operation	operator: 169 operands: 117
107	Operation	operator: 141 operands: 118
108	Operation	operator: 125 operands: 119
109	Operation	operator: 125 operands: 120
110	Operation	operator: 121 operands: 122
111	Operation	operator: 142 operands: 123
112	Operation	operator: 125 operands: 124
113	ExprTuple	155
114	Operation	operator: 125 operands: 126
115	Literal
116	ExprTuple	167
117	ExprTuple	175, 127, 128, 172
118	NamedExprs	state: 129
119	NamedExprs	element: 130 targets: 138
120	NamedExprs	element: 131 targets: 132
121	Literal
122	NamedExprs	basis: 133
123	NamedExprs	operation: 134
124	NamedExprs	element: 135 targets: 136
125	Literal
126	NamedExprs	element: 137 targets: 138
127	Literal
128	Literal
129	Operation	operator: 139 operand: 151
130	Operation	operator: 141 operands: 148
131	Operation	operator: 142 operands: 143
132	Operation	operator: 149 operands: 144
133	Literal
134	Literal
135	Operation	operator: 147 operands: 145
136	Operation	operator: 149 operands: 146
137	Operation	operator: 147 operands: 148
138	Operation	operator: 149 operands: 150
139	Literal
140	ExprTuple	151
141	Literal
142	Literal
143	NamedExprs	operation: 152 part: 155
144	ExprTuple	167, 157
145	NamedExprs	state: 153 part: 155
146	ExprTuple	167, 176
147	Literal
148	NamedExprs	state: 154 part: 155
149	Literal
150	ExprTuple	156, 157
151	Literal
152	Operation	operator: 158 operands: 159
153	Operation	operator: 160 operands: 161
154	Variable
155	Variable
156	Operation	operator: 163 operands: 162
157	Operation	operator: 163 operands: 164
158	Literal
159	ExprTuple	165, 176
160	Literal
161	ExprTuple	166, 176
162	ExprTuple	176, 167
163	Literal
164	ExprTuple	176, 168
165	Variable
166	Operation	operator: 169 operands: 170
167	Literal
168	Variable
169	Literal
170	ExprTuple	171, 172
171	Operation	operator: 173 operands: 174
172	Variable
173	Literal
174	ExprTuple	175, 176
175	Literal
176	Variable