Expression of type Conditional

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 Conditional, m
from proveit.logic import And, InSet
from proveit.physics.quantum.QPE import _m_domain, _phase_est_circuit, _success_cond

# build up the expression from sub-expressions
expr = Conditional(_phase_est_circuit, And(InSet(m, _m_domain), _success_cond))

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\{\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \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 m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array} \textrm{ if } m \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  \left|\frac{m}{2^{t}} - \varphi\right|_{\textup{mod}\thinspace 1} \leq 2^{-n}\right..

stored_expr.style_options()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

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