Axioms for the theory of proveit.core_expr_types.operations

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 ExprTuple, ExprRange, IndexedVar
from proveit import f, g, k, n, x, y
from proveit.logic import Forall, Equals
from proveit.core_expr_types import Len
from proveit.core_expr_types import (x_1_to_n, y_1_to_n, f__x_1_to_n, f__y_1_to_n, x_eq_y__1_to_n)
from proveit.numbers import Natural, one

%begin axioms

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

When there are multiple operands of an operation, they are internally represented as an ExprTuple. However, this axiom is need to replace one ExprTuple of operands with another ExprTuple of operands. The alternative would be to invent some notation to make a unary map expand a single ExprTuple argument into the operands of an operation (something like $x \mapsto f(*x)$ where $*$ acts in the sense of the unpacking operator in Python). We can attain this affect from the following axiom using explicit and standard notation.

operands_substitution = 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(),
                                         conditions = [x_eq_y__1_to_n]),
                               domain=Natural)

operands_substitution:

%end axioms

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