In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import Conditional, ConditionalSet, ExprRange, IndexedVar
from proveit import a, b, c, i, m, n, Q, R
from proveit.core_expr_types import a_1_to_m, c_1_to_n
from proveit.logic import Implies, Iff, Forall, Equals, TRUE, FALSE, Or
from proveit.numbers import one, Natural
```

In [2]:

```
%begin axioms
```

*A Conditional is defined to evaluate to its value when the condition is TRUE:*

In [3]:

```
true_condition_reduction = Forall(a, Equals(Conditional(a, TRUE), a))
```

*A condition may be substituted with a logically equivalent condition. (Since a Conditional is not an Operation, this must be a distinct axiom from Operation substitution axioms).*

In [4]:

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

*The condition is either true or not true but otherwise it doesn't matter if it is a Boolean. Therefore, a condition of $Q$ is the same as a condition of $Q=\top$*

In [5]:

```
condition__as__condition_eq_true = \
Forall((a, Q), Equals(Conditional(a, Q),
Conditional(a, Equals(Q, TRUE))).with_wrap_before_operator())
```

*If two values are equal when the condition is satisfied, one may replace the other within the Conditional.*

In [6]:

```
conditional_substitution = \
Forall((a, b, Q), Equals(Conditional(a, Q),
Conditional(b, Q)).with_wrap_before_operator(),
conditions=[Implies(Q, Equals(a, b))])
```

*If one and only one Conditional in a ConditionalSet is True, equate the ConditionalSet to the Conditional.*

In [7]:

```
# singular_truth_reduction = \
# Forall((m, n),
# Forall((a, b, c),
# Equals(ConditionalSet(var_range(a, one, m), b, var_range(c, one, n)), b),
# conditions=[Equals(Or(var_range(a, one, m)), FALSE), Equals(Or(var_range(c, one, n)), FALSE)]),
# domain=Natural)
```

In [8]:

```
true_case_reduction = \
Forall((m, n),
Forall((a_1_to_m, b, c_1_to_n),
Equals(ConditionalSet(ExprRange(i, Conditional(IndexedVar(a, i), FALSE), one, m), b,
ExprRange(i, Conditional(IndexedVar(c, i), FALSE), one, n)), b)),
domain=Natural)
```

In [9]:

```
%end axioms
```