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 e
from proveit.logic import Equals, Forall
from proveit.physics.quantum.QPE import Psuccess, _e_domain, _success_prob_e

# build up the expression from sub-expressions
expr = Forall(instance_param_or_params = [e], instance_expr = Equals(Psuccess(e), _success_prob_e), domain = _e_domain).with_wrapping()

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

\begin{array}{l}\forall_{e \in \{1~\ldotp \ldotp~2^{t - 1} - 2\}}~\\
\left(\left[P_{\rm success}\right]\left(e\right) = \left[\begin{array}{l}\textrm{Prob}_{m \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~\left|m - b_{\textit{f}}\right|_{\textup{mod}\thinspace 2^{t}} \leq e}~\\
\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}\right)\end{array}\right]\right)\end{array}

stored_expr.style_options()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	True	('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: 1 operand: 3
1	Literal
2	ExprTuple	3
3	Lambda	parameter: 62 body: 4
4	Conditional	value: 5 condition: 6
5	Operation	operator: 7 operands: 8
6	Operation	operator: 48 operands: 9
7	Literal
8	ExprTuple	10, 11
9	ExprTuple	62, 12
10	Operation	operator: 13 operand: 62
11	Operation	operator: 15 operand: 18
12	Operation	operator: 108 operands: 17
13	Literal
14	ExprTuple	62
15	Literal
16	ExprTuple	18
17	ExprTuple	136, 19
18	Lambda	parameter: 135 body: 21
19	Operation	operator: 130 operands: 22
20	ExprTuple	135
21	Conditional	value: 23 condition: 24
22	ExprTuple	25, 26
23	Operation	operator: 27 operands: 28
24	Operation	operator: 29 operands: 30
25	Operation	operator: 120 operands: 31
26	Operation	operator: 123 operand: 132
27	Literal
28	ExprTuple	33, 34, 35, 36
29	Literal
30	ExprTuple	37, 38
31	ExprTuple	132, 39
32	ExprTuple	132
33	ExprTuple	40, 41
34	ExprTuple	42, 43
35	ExprTuple	44, 45
36	ExprTuple	46, 47
37	Operation	operator: 48 operands: 49
38	Operation	operator: 50 operands: 51
39	Operation	operator: 130 operands: 52
40	ExprRange	lambda_map: 53 start_index: 136 end_index: 137
41	ExprRange	lambda_map: 54 start_index: 136 end_index: 138
42	ExprRange	lambda_map: 55 start_index: 136 end_index: 137
43	ExprRange	lambda_map: 55 start_index: 118 end_index: 119
44	ExprRange	lambda_map: 56 start_index: 136 end_index: 137
45	ExprRange	lambda_map: 57 start_index: 136 end_index: 138
46	ExprRange	lambda_map: 58 start_index: 136 end_index: 137
47	ExprRange	lambda_map: 59 start_index: 136 end_index: 138
48	Literal
49	ExprTuple	135, 60
50	Literal
51	ExprTuple	61, 62
52	ExprTuple	137, 111
53	Lambda	parameter: 117 body: 63
54	Lambda	parameter: 117 body: 64
55	Lambda	parameter: 117 body: 65
56	Lambda	parameter: 117 body: 66
57	Lambda	parameter: 117 body: 67
58	Lambda	parameter: 117 body: 68
59	Lambda	parameter: 117 body: 70
60	Operation	operator: 108 operands: 71
61	Operation	operator: 72 operands: 73
62	Variable
63	Operation	operator: 100 operands: 74
64	Operation	operator: 81 operands: 75
65	Operation	operator: 81 operands: 76
66	Operation	operator: 77 operands: 78
67	Operation	operator: 101 operands: 79
68	Operation	operator: 81 operands: 80
69	ExprTuple	117
70	Operation	operator: 81 operands: 82
71	ExprTuple	83, 84
72	Literal
73	ExprTuple	85, 110
74	NamedExprs	state: 86
75	NamedExprs	element: 87 targets: 95
76	NamedExprs	element: 88 targets: 89
77	Literal
78	NamedExprs	basis: 90
79	NamedExprs	operation: 91
80	NamedExprs	element: 92 targets: 93
81	Literal
82	NamedExprs	element: 94 targets: 95
83	Literal
84	Operation	operator: 130 operands: 96
85	Operation	operator: 130 operands: 97
86	Operation	operator: 98 operand: 113
87	Operation	operator: 100 operands: 107
88	Operation	operator: 101 operands: 102
89	Operation	operator: 108 operands: 103
90	Literal
91	Literal
92	Operation	operator: 106 operands: 104
93	Operation	operator: 108 operands: 105
94	Operation	operator: 106 operands: 107
95	Operation	operator: 108 operands: 109
96	ExprTuple	110, 111
97	ExprTuple	135, 112
98	Literal
99	ExprTuple	113
100	Literal
101	Literal
102	NamedExprs	operation: 114 part: 117
103	ExprTuple	136, 119
104	NamedExprs	state: 115 part: 117
105	ExprTuple	136, 137
106	Literal
107	NamedExprs	state: 116 part: 117
108	Literal
109	ExprTuple	118, 119
110	Operation	operator: 120 operands: 121
111	Operation	operator: 123 operand: 136
112	Operation	operator: 123 operand: 133
113	Literal
114	Operation	operator: 125 operands: 126
115	Operation	operator: 127 operands: 128
116	Literal
117	Variable
118	Operation	operator: 130 operands: 129
119	Operation	operator: 130 operands: 131
120	Literal
121	ExprTuple	132, 137
122	ExprTuple	136
123	Literal
124	ExprTuple	133
125	Literal
126	ExprTuple	134, 137
127	Literal
128	ExprTuple	135, 137
129	ExprTuple	137, 136
130	Literal
131	ExprTuple	137, 138
132	Literal
133	Literal
134	Literal
135	Variable
136	Literal
137	Literal
138	Literal