see dependencies
import proveit
# Automation is not needed when only building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_theorem_expr # Load the stored theorem expression as 'stored_expr'
# import the special expression
from proveit.physics.quantum.circuits import output_consolidation
# check that the built expression is the same as the stored expression
assert output_consolidation.expr == stored_expr
assert output_consolidation.expr._style_id == stored_expr._style_id
print("Passed sanity check: output_consolidation matches stored_expr")
Passed sanity check: output_consolidation matches stored_expr
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())
\forall_{m \in \mathbb{N}^+}~\left[\begin{array}{l}\forall_{n_{1}, n_{2}, \ldots, n_{m} \in \mathbb{N}^+}~\\ \left[\begin{array}{l}\forall_{\left(A_{1} \in \mathbb{C}^{2^{n_{1}}}\right), \left(A_{2} \in \mathbb{C}^{2^{n_{2}}}\right), \ldots, \left(A_{m} \in \mathbb{C}^{2^{n_{m}}}\right)}~\\ \left[\begin{array}{l}\forall_{N_{0}, N_{1}, \ldots, N_{m} \in \mathbb{N}~|~\left(N_{0} = 0\right)\land \left(N_{1} = \left(N_{1 - 1} + n_{1}\right)\right) \land \left(N_{2} = \left(N_{2 - 1} + n_{2}\right)\right) \land \ldots \land \left(N_{m} = \left(N_{m - 1} + n_{m}\right)\right)}~\\ \left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{ & \qout{A_{1}~\mbox{part}~1~\mbox{on}~\{N_{1 - 1} + 1~\ldotp \ldotp~N_{1}\}} \\ & \qout{A_{1}~\mbox{part}~2~\mbox{on}~\{N_{1 - 1} + 1~\ldotp \ldotp~N_{1}\}} \\ & \qout{\vdots} \\ & \qout{A_{1}~\mbox{part}~n_{1}~\mbox{on}~\{N_{1 - 1} + 1~\ldotp \ldotp~N_{1}\}} \\ & \qout{A_{2}~\mbox{part}~1~\mbox{on}~\{N_{2 - 1} + 1~\ldotp \ldotp~N_{2}\}} \\ & \qout{A_{2}~\mbox{part}~2~\mbox{on}~\{N_{2 - 1} + 1~\ldotp \ldotp~N_{2}\}} \\ & \qout{\vdots} \\ & \qout{A_{2}~\mbox{part}~n_{2}~\mbox{on}~\{N_{2 - 1} + 1~\ldotp \ldotp~N_{2}\}} \\ & \qout{\begin{array}{c}\vdots\\ \vdots\end{array}} \\ & \qout{A_{m}~\mbox{part}~1~\mbox{on}~\{N_{m - 1} + 1~\ldotp \ldotp~N_{m}\}} \\ & \qout{A_{m}~\mbox{part}~2~\mbox{on}~\{N_{m - 1} + 1~\ldotp \ldotp~N_{m}\}} \\ & \qout{\vdots} \\ & \qout{A_{m}~\mbox{part}~n_{m}~\mbox{on}~\{N_{m - 1} + 1~\ldotp \ldotp~N_{m}\}} } \end{array}\right) \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{ & \qout{A_{1} {\otimes} A_{2} {\otimes} \ldots {\otimes} A_{m}~\mbox{part}~N_{1 - 1} + 1~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\ & \qout{A_{1} {\otimes} A_{2} {\otimes} \ldots {\otimes} A_{m}~\mbox{part}~N_{1 - 1} + 2~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\ & \qout{\vdots} \\ & \qout{A_{1} {\otimes} A_{2} {\otimes} \ldots {\otimes} A_{m}~\mbox{part}~N_{1}~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\ & \qout{A_{1} {\otimes} A_{2} {\otimes} \ldots {\otimes} A_{m}~\mbox{part}~N_{2 - 1} + 1~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\ & \qout{A_{1} {\otimes} A_{2} {\otimes} \ldots {\otimes} A_{m}~\mbox{part}~N_{2 - 1} + 2~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\ & \qout{\vdots} \\ & \qout{A_{1} {\otimes} A_{2} {\otimes} \ldots {\otimes} A_{m}~\mbox{part}~N_{2}~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\ & \qout{\begin{array}{c}\vdots\\ \vdots\end{array}} \\ & \qout{A_{1} {\otimes} A_{2} {\otimes} \ldots {\otimes} A_{m}~\mbox{part}~N_{m - 1} + 1~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\ & \qout{A_{1} {\otimes} A_{2} {\otimes} \ldots {\otimes} A_{m}~\mbox{part}~N_{m - 1} + 2~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\ & \qout{\vdots} \\ & \qout{A_{1} {\otimes} A_{2} {\otimes} \ldots {\otimes} A_{m}~\mbox{part}~N_{m}~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} } \end{array}\right)\right)\end{array}\right]\end{array}\right]\end{array}\right]
stored_expr.style_options()
name | description | default | current value | related methods |
---|---|---|---|---|
with_wrapping | If 'True', wrap the Expression after the parameters | None | None/False | ('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()