Theorems (or conjectures) for the theory of proveit.core_expr_types.operations

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 f, g, n
from proveit import ExprTuple
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
from proveit.logic import Forall, Equals
from proveit.numbers import Natural

%begin theorems

Defining theorems for theory 'proveit.core_expr_types.operations'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

operands_substitution_via_tuple = Forall(
    n, Forall((f, x_1_to_n, y_1_to_n),
              Equals(f__x_1_to_n, f__y_1_to_n).with_wrap_after_operator(),
              condition=Equals(ExprTuple(x_1_to_n), ExprTuple(y_1_to_n))),
    domain=Natural)

operands_substitution_via_tuple (conjecture without proof):

We can derive operator_substitution as a special case of proveit.logic.equality.substitution.

operator_substitution = Forall(n, Forall((f, g, x_1_to_n),
                                         Equals(f__x_1_to_n, g__x_1_to_n),
                                         conditions = [Equals(f, g)]),
                               domain=Natural)

operator_substitution (established theorem):

%end theorems

These theorems may now be imported from the theory package: proveit.core_expr_types.operations