In [1]:

```
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import Conditional
from proveit import a, b, f, g, m, n, A, Q, R
from proveit.core_expr_types import (x_1_to_n, y_1_to_n, f__x_1_to_n, f__y_1_to_n,
g__x_1_to_n, g__y_1_to_n, Q__x_1_to_n, Q__y_1_to_n,
Q_1_to_m, R_1_to_n)
from proveit.logic import TRUE, FALSE, And, Implies, Forall, Equals, Not, NotEquals
from proveit.numbers import Natural, NaturalPos
```

In [2]:

```
%begin theorems
```

In [3]:

```
satisfied_condition_reduction = Forall((a, Q), Equals(Conditional(a, Q), a),
condition=Q)
```

In [4]:

```
dissatisfied_condition_reduction = Forall((a, Q), Equals(Conditional(a, Q), Conditional(a, FALSE)),
condition=Not(Q))
```

In [5]:

```
condition_substitution = \
Forall((a, Q, R), Equals(Conditional(a, Q),
Conditional(a, R)).with_wrap_before_operator(),
conditions=[Equals(Q, R)])
```

In [6]:

```
redundant_condition_reduction = Forall((a, Q), Equals(Conditional(Conditional(a, Q), Q),
Conditional(a, Q)))
```

In [7]:

```
implication_from_conditional = Forall((A, Q), Implies(Q, A),
condition=Conditional(A, Q))
```

Note: to prove the following, we will need to use the fact that a condition of $Q$ is the same as having a condition of $Q=\top$ in order to avoid requiring that $Q$ is boolean.

In [8]:

```
singular_conjunction_condition_reduction = \
Forall((a, Q), Equals(Conditional(a, And(Q)),
Conditional(a, Q)).with_wrap_before_operator())
```

Note: to prove the following, we will need to use the fact that a condition of $Q$ is the same as having a condition of $Q=\top$ in order to avoid requiring that the $Q$ and $R$ variables be booleans.

In [9]:

```
condition_merger_reduction = \
Forall((m, n), Forall((a, Q_1_to_m, R_1_to_n),
Equals(Conditional(a, (And(Q_1_to_m), And(R_1_to_n))),
Conditional(a, (Q_1_to_m, R_1_to_n))).with_wrap_before_operator()),
domain=Natural)
```

In [10]:

```
condition_append_reduction = \
Forall(m, Forall((a, Q_1_to_m, R),
Equals(Conditional(a, (And(Q_1_to_m), R)),
Conditional(a, (Q_1_to_m, R))).with_wrap_before_operator()),
domain=Natural)
```

In [11]:

```
condition_prepend_reduction = \
Forall(n, Forall((a, Q, R_1_to_n),
Equals(Conditional(a, (Q, And(R_1_to_n))),
Conditional(a, (Q, R_1_to_n))).with_wrap_before_operator()),
domain=Natural)
```

In [12]:

```
true_condition_elimination = (
Forall((m, n), Forall((a, Q_1_to_m, R_1_to_n),
Equals(Conditional(a, (And(Q_1_to_m, TRUE, R_1_to_n))),
Conditional(a, (Q_1_to_m, R_1_to_n)))
.with_wrap_before_operator()),
domain=Natural))
```

In [13]:

```
condition_with_true_on_left_reduction = \
Forall(m, Forall((a, Q_1_to_m),
Equals(Conditional(a, (TRUE, And(Q_1_to_m))),
Conditional(a, (Q_1_to_m))).with_wrap_before_operator()),
domain=Natural)
```

In [14]:

```
condition_with_true_on_right_reduction = \
Forall(m, Forall((a, Q_1_to_m),
Equals(Conditional(a, (And(Q_1_to_m), TRUE)),
Conditional(a, (Q_1_to_m))).with_wrap_before_operator()),
domain=Natural)
```

In [15]:

```
%end theorems
```