Expression of type Equals

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.logic import Equals
from proveit.numbers import one
from proveit.physics.quantum.circuits import phase_kickback_on_register_circuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
expr = Equals(Prob(phase_kickback_on_register_circuit), one)

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

\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

stored_expr.style_options()

name	description	default	current value	related methods
operation	'infix' or 'function' style formatting	infix	infix
wrap_positions	position(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.	()	()	('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	center	center	('with_justification',)
direction	Direction of the relation (normal or reversed)	normal	normal	('with_direction_reversed', 'is_reversed')

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	Operation	operator: 67 operands: 1
1	ExprTuple	2, 107
2	Operation	operator: 3 operand: 5
3	Literal
4	ExprTuple	5
5	Operation	operator: 6 operands: 7
6	Literal
7	ExprTuple	8, 9, 10
8	ExprTuple	11, 12
9	ExprRange	lambda_map: 13 start_index: 107 end_index: 106
10	ExprTuple	14, 15
11	ExprRange	lambda_map: 16 start_index: 107 end_index: 106
12	ExprRange	lambda_map: 17 start_index: 107 end_index: 90
13	Lambda	parameter: 89 body: 18
14	ExprRange	lambda_map: 19 start_index: 107 end_index: 106
15	ExprRange	lambda_map: 20 start_index: 107 end_index: 90
16	Lambda	parameter: 116 body: 21
17	Lambda	parameter: 116 body: 22
18	ExprTuple	23, 24
19	Lambda	parameter: 116 body: 25
20	Lambda	parameter: 116 body: 26
21	Operation	operator: 40 operands: 27
22	Operation	operator: 65 operands: 28
23	ExprRange	lambda_map: 29 start_index: 107 end_index: 106
24	ExprRange	lambda_map: 30 start_index: 107 end_index: 90
25	Operation	operator: 45 operands: 31
26	Operation	operator: 65 operands: 32
27	NamedExprs	state: 33
28	NamedExprs	element: 34 targets: 51
29	Lambda	parameter: 116 body: 35
30	Lambda	parameter: 116 body: 36
31	NamedExprs	state: 37
32	NamedExprs	element: 38 targets: 51
33	Operation	operator: 100 operand: 47
34	Operation	operator: 40 operands: 46
35	Operation	operator: 41 operands: 42
36	Operation	operator: 65 operands: 43
37	Operation	operator: 85 operands: 44
38	Operation	operator: 45 operands: 46
39	ExprTuple	47
40	Literal
41	Literal
42	ExprTuple	48, 49
43	NamedExprs	element: 50 targets: 51
44	ExprTuple	52, 53
45	Literal
46	NamedExprs	state: 54 part: 116
47	Literal
48	Conditional	value: 55 condition: 56
49	Conditional	value: 57 condition: 58
50	Operation	operator: 68 operands: 59
51	Operation	operator: 60 operands: 61
52	Operation	operator: 96 operands: 62
53	Operation	operator: 63 operands: 64
54	Variable
55	Operation	operator: 65 operands: 66
56	Operation	operator: 67 operands: 71
57	Operation	operator: 68 operands: 69
58	Operation	operator: 70 operands: 71
59	NamedExprs	operation: 72 part: 116
60	Literal
61	ExprTuple	95, 73
62	ExprTuple	107, 74
63	Literal
64	ExprTuple	75, 76
65	Literal
66	NamedExprs	element: 77 targets: 78
67	Literal
68	Literal
69	NamedExprs	operation: 79
70	Literal
71	ExprTuple	89, 116
72	IndexedVar	variable: 80 index: 89
73	Operation	operator: 102 operands: 82
74	Operation	operator: 98 operands: 83
75	Operation	operator: 100 operand: 92
76	Operation	operator: 85 operands: 86
77	Literal
78	Operation	operator: 87 operand: 95
79	Literal
80	Variable
81	ExprTuple	89
82	ExprTuple	106, 90
83	ExprTuple	110, 91
84	ExprTuple	92
85	Literal
86	ExprTuple	93, 94
87	Literal
88	ExprTuple	95
89	Variable
90	Variable
91	Operation	operator: 96 operands: 97
92	Literal
93	Operation	operator: 98 operands: 99
94	Operation	operator: 100 operand: 107
95	Operation	operator: 102 operands: 103
96	Literal
97	ExprTuple	107, 110
98	Literal
99	ExprTuple	104, 105
100	Literal
101	ExprTuple	107
102	Literal
103	ExprTuple	106, 107
104	Literal
105	Operation	operator: 108 operands: 109
106	Variable
107	Literal
108	Literal
109	ExprTuple	110, 111, 112, 113
110	Literal
111	Literal
112	Literal
113	IndexedVar	variable: 114 index: 116
114	Variable
115	ExprTuple	116
116	Variable