# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(_t, one)
sub_expr3 = Add(_t, _s)
sub_expr4 = Interval(one, _t)
sub_expr5 = Interval(sub_expr2, sub_expr3)
sub_expr6 = [ExprRange(sub_expr1, Measure(basis = Z), one, _t), _s_wire]
sub_expr7 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr3))
sub_expr8 = ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)
sub_expr9 = [ExprRange(sub_expr1, Input(state = ket_plus), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)]
sub_expr10 = [ExprRange(sub_expr1, sub_expr7, one, _t), ExprRange(sub_expr1, sub_expr7, sub_expr2, sub_expr3)]
expr = And(InSet(Lambda(m, _phase_est_circuit), Functions(_m_domain, _Omega)), Forall(instance_param_or_params = [a, b], instance_expr = NotEquals(Qcircuit(vert_expr_array = VertExprArray(sub_expr9, sub_expr10, sub_expr6, [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(a, _t), part = sub_expr1), targets = sub_expr4), one, _t), sub_expr8])), Qcircuit(vert_expr_array = VertExprArray(sub_expr9, sub_expr10, sub_expr6, [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(b, _t), part = sub_expr1), targets = sub_expr4), one, _t), sub_expr8]))), domain = _m_domain, condition = NotEquals(a, b)))