Expression of type Lambda

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 Lambda, a, b
from proveit.core_expr_types import U_1_to_m
from proveit.logic import Implies
from proveit.physics.quantum.circuits import QcircuitEquiv, circuit_aU, circuit_aUb, circuit_b

# build up the expression from sub-expressions
expr = Lambda([a, b, U_1_to_m], Implies(circuit_aUb, QcircuitEquiv(circuit_aU, circuit_b)))

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(a, b, U_{1}, U_{2}, \ldots, U_{m}\right) \mapsto \left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{a} & \gate{\begin{array}{c} \uparrow \\U_{1} \\ \downarrow\end{array}} & \gate{\begin{array}{c} \uparrow \\U_{2} \\ \downarrow\end{array}} & \gate{\begin{array}{c} \uparrow \\\cdots \\ \downarrow\end{array}} & \gate{\begin{array}{c} \uparrow \\U_{m} \\ \downarrow\end{array}} & \qout{b}
} \end{array}\right) \Rightarrow \left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{a} & \gate{\begin{array}{c} \uparrow \\U_{1} \\ \downarrow\end{array}} & \gate{\begin{array}{c} \uparrow \\U_{2} \\ \downarrow\end{array}} & \gate{\begin{array}{c} \uparrow \\\cdots \\ \downarrow\end{array}} & \gate{\begin{array}{c} \uparrow \\U_{m} \\ \downarrow\end{array}} & { /^{k} } \qw
} \end{array}\right) \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{b} & { /^{k} } \qw
} \end{array}\right)\right)\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	Lambda	parameters: 1 body: 2
1	ExprTuple	47, 48, 19
2	Operation	operator: 3 operands: 4
3	Literal
4	ExprTuple	5, 6
5	Operation	operator: 15 operands: 7
6	Operation	operator: 8 operands: 9
7	ExprTuple	18, 19, 10
8	Literal
9	ExprTuple	11, 12
10	ExprTuple	13
11	Operation	operator: 15 operands: 14
12	Operation	operator: 15 operand: 20
13	ExprRange	lambda_map: 17 start_index: 50 end_index: 51
14	ExprTuple	18, 19
15	Literal
16	ExprTuple	20
17	Lambda	parameter: 49 body: 21
18	ExprTuple	22
19	ExprRange	lambda_map: 23 start_index: 50 end_index: 24
20	ExprTuple	25
21	Operation	operator: 37 operands: 26
22	ExprRange	lambda_map: 27 start_index: 50 end_index: 51
23	Lambda	parameter: 49 body: 28
24	Variable
25	ExprRange	lambda_map: 29 start_index: 50 end_index: 51
26	NamedExprs	element: 30 targets: 41
27	Lambda	parameter: 49 body: 31
28	IndexedVar	variable: 32 index: 49
29	Lambda	parameter: 49 body: 34
30	Operation	operator: 35 operands: 44
31	Operation	operator: 37 operands: 36
32	Variable
33	ExprTuple	49
34	Operation	operator: 37 operands: 38
35	Literal
36	NamedExprs	element: 39 targets: 41
37	Literal
38	NamedExprs	element: 40 targets: 41
39	Operation	operator: 43 operands: 42
40	Operation	operator: 43 operands: 44
41	Operation	operator: 45 operands: 46
42	NamedExprs	state: 47 part: 49
43	Literal
44	NamedExprs	state: 48 part: 49
45	Literal
46	ExprTuple	50, 51
47	Variable
48	Variable
49	Variable
50	Literal
51	Variable