Expression of type ExprTuple

from the theory of proveit.physics.quantum.circuits

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 Conditional, ExprRange, ExprTuple, IndexedVar, Lambda, U, Variable, m, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import And, Equals, Forall, InSet
from proveit.numbers import Exp, Mult, NaturalPos, e, i, one, pi, two
from proveit.physics.quantum import m_ket_domain, normalized_var_ket_u, var_ket_u, varphi
from proveit.physics.quantum.circuits import phase_kickback_on_register_circuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = IndexedVar(U, sub_expr1)
sub_expr3 = IndexedVar(varphi, sub_expr1)
expr = ExprTuple(Lambda([m, t], Conditional(Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr2, one, t)], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr3, one, t)], instance_expr = Equals(Prob(phase_kickback_on_register_circuit), one), condition = ExprRange(sub_expr1, Equals(MatrixMult(sub_expr2, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, sub_expr3)), var_ket_u)), one, t)).with_wrapping(), domain = m_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = Unitary(Exp(two, m))).with_wrapping(), And(InSet(m, NaturalPos), InSet(t, 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())

\left(\left(m, t\right) \mapsto \left\{\begin{array}{l}\forall_{U_{1}, U_{2}, \ldots, U_{t} \in \textrm{U}\left(2^{m}\right)}~\\
\left[\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{m}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi_{1}, \varphi_{2}, \ldots, \varphi_{t}~|~\left(\left(U_{1} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert u \rangle\right)\right), \left(\left(U_{2} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert u \rangle\right)\right), \ldots, \left(\left(U_{t} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{t}} \cdot \lvert u \rangle\right)\right)}~\\
\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{t}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U_{1}} & \gate{U_{2}} & \gate{\cdots} & \gate{U_{t}} & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right)\end{array}\right]\end{array}\right]\end{array} \textrm{ if } m \in \mathbb{N}^+ ,  t \in \mathbb{N}^+\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	ExprTuple	1
1	Lambda	parameters: 2 body: 3
2	ExprTuple	158, 174
3	Conditional	value: 4 condition: 5
4	Operation	operator: 29 operand: 8
5	Operation	operator: 51 operands: 7
6	ExprTuple	8
7	ExprTuple	9, 10
8	Lambda	parameters: 11 body: 12
9	Operation	operator: 39 operands: 13
10	Operation	operator: 39 operands: 14
11	ExprTuple	15
12	Conditional	value: 16 condition: 17
13	ExprTuple	158, 18
14	ExprTuple	174, 18
15	ExprRange	lambda_map: 19 start_index: 175 end_index: 174
16	Operation	operator: 29 operand: 22
17	Operation	operator: 51 operands: 21
18	Literal
19	Lambda	parameter: 184 body: 88
20	ExprTuple	22
21	ExprTuple	23
22	Lambda	parameter: 122 body: 24
23	ExprRange	lambda_map: 25 start_index: 175 end_index: 174
24	Conditional	value: 26 condition: 27
25	Lambda	parameter: 184 body: 28
26	Operation	operator: 29 operand: 33
27	Operation	operator: 51 operands: 31
28	Operation	operator: 39 operands: 32
29	Literal
30	ExprTuple	33
31	ExprTuple	34, 35
32	ExprTuple	88, 36
33	Lambda	parameters: 37 body: 38
34	Operation	operator: 39 operands: 40
35	Operation	operator: 135 operands: 41
36	Operation	operator: 42 operand: 60
37	ExprTuple	44
38	Conditional	value: 45 condition: 46
39	Literal
40	ExprTuple	122, 47
41	ExprTuple	48, 175
42	Literal
43	ExprTuple	60
44	ExprRange	lambda_map: 49 start_index: 175 end_index: 174
45	Operation	operator: 135 operands: 50
46	Operation	operator: 51 operands: 52
47	Operation	operator: 53 operands: 54
48	Operation	operator: 55 operand: 122
49	Lambda	parameter: 184 body: 181
50	ExprTuple	57, 175
51	Literal
52	ExprTuple	58
53	Literal
54	ExprTuple	59, 60
55	Literal
56	ExprTuple	122
57	Operation	operator: 61 operand: 65
58	ExprRange	lambda_map: 63 start_index: 175 end_index: 174
59	Literal
60	Operation	operator: 166 operands: 64
61	Literal
62	ExprTuple	65
63	Lambda	parameter: 184 body: 66
64	ExprTuple	178, 158
65	Operation	operator: 67 operands: 68
66	Operation	operator: 135 operands: 69
67	Literal
68	ExprTuple	70, 71, 72
69	ExprTuple	73, 74
70	ExprTuple	75, 76
71	ExprRange	lambda_map: 77 start_index: 175 end_index: 174
72	ExprTuple	78, 79
73	Operation	operator: 80 operands: 81
74	Operation	operator: 153 operands: 82
75	ExprRange	lambda_map: 83 start_index: 175 end_index: 174
76	ExprRange	lambda_map: 84 start_index: 175 end_index: 158
77	Lambda	parameter: 157 body: 85
78	ExprRange	lambda_map: 86 start_index: 175 end_index: 174
79	ExprRange	lambda_map: 87 start_index: 175 end_index: 158
80	Literal
81	ExprTuple	88, 122
82	ExprTuple	161, 122
83	Lambda	parameter: 184 body: 89
84	Lambda	parameter: 184 body: 90
85	ExprTuple	91, 92
86	Lambda	parameter: 184 body: 93
87	Lambda	parameter: 184 body: 94
88	IndexedVar	variable: 148 index: 184
89	Operation	operator: 108 operands: 95
90	Operation	operator: 133 operands: 96
91	ExprRange	lambda_map: 97 start_index: 175 end_index: 174
92	ExprRange	lambda_map: 98 start_index: 175 end_index: 158
93	Operation	operator: 113 operands: 99
94	Operation	operator: 133 operands: 100
95	NamedExprs	state: 101
96	NamedExprs	element: 102 targets: 119
97	Lambda	parameter: 184 body: 103
98	Lambda	parameter: 184 body: 104
99	NamedExprs	state: 105
100	NamedExprs	element: 106 targets: 119
101	Operation	operator: 168 operand: 115
102	Operation	operator: 108 operands: 114
103	Operation	operator: 109 operands: 110
104	Operation	operator: 133 operands: 111
105	Operation	operator: 153 operands: 112
106	Operation	operator: 113 operands: 114
107	ExprTuple	115
108	Literal
109	Literal
110	ExprTuple	116, 117
111	NamedExprs	element: 118 targets: 119
112	ExprTuple	120, 121
113	Literal
114	NamedExprs	state: 122 part: 184
115	Literal
116	Conditional	value: 123 condition: 124
117	Conditional	value: 125 condition: 126
118	Operation	operator: 136 operands: 127
119	Operation	operator: 128 operands: 129
120	Operation	operator: 164 operands: 130
121	Operation	operator: 131 operands: 132
122	Variable
123	Operation	operator: 133 operands: 134
124	Operation	operator: 135 operands: 139
125	Operation	operator: 136 operands: 137
126	Operation	operator: 138 operands: 139
127	NamedExprs	operation: 140 part: 184
128	Literal
129	ExprTuple	163, 141
130	ExprTuple	175, 142
131	Literal
132	ExprTuple	143, 144
133	Literal
134	NamedExprs	element: 145 targets: 146
135	Literal
136	Literal
137	NamedExprs	operation: 147
138	Literal
139	ExprTuple	157, 184
140	IndexedVar	variable: 148 index: 157
141	Operation	operator: 170 operands: 150
142	Operation	operator: 166 operands: 151
143	Operation	operator: 168 operand: 160
144	Operation	operator: 153 operands: 154
145	Literal
146	Operation	operator: 155 operand: 163
147	Literal
148	Variable
149	ExprTuple	157
150	ExprTuple	174, 158
151	ExprTuple	178, 159
152	ExprTuple	160
153	Literal
154	ExprTuple	161, 162
155	Literal
156	ExprTuple	163
157	Variable
158	Variable
159	Operation	operator: 164 operands: 165
160	Literal
161	Operation	operator: 166 operands: 167
162	Operation	operator: 168 operand: 175
163	Operation	operator: 170 operands: 171
164	Literal
165	ExprTuple	175, 178
166	Literal
167	ExprTuple	172, 173
168	Literal
169	ExprTuple	175
170	Literal
171	ExprTuple	174, 175
172	Literal
173	Operation	operator: 176 operands: 177
174	Variable
175	Literal
176	Literal
177	ExprTuple	178, 179, 180, 181
178	Literal
179	Literal
180	Literal
181	IndexedVar	variable: 182 index: 184
182	Variable
183	ExprTuple	184
184	Variable