Axioms for the theory of proveit.core_expr_types.expr_arrays

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, ExprArray, VertExprArray
from proveit import a, b, c, d, f, i, j, m, n, fab
from proveit.logic import Forall, Equals, And, NotEquals, InSet
from proveit.core_expr_types import \
    (a_1_to_i, b_1_to_j, c_1_to_i)
from proveit.numbers import zero, one
from proveit.numbers import Natural, NaturalPos, Add, subtract

%begin axioms

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

array_eq_def = Forall(i, Forall((a_1_to_i, b, c_1_to_i, d),
                                Equals(Equals(ExprArray(a_1_to_i, b), 
                                              ExprArray(c_1_to_i, d)),
                                       And(Equals([a_1_to_i], [c_1_to_i]), 
                                           Equals(b, d))) \
                                .with_wrap_after_operator()),
                      domain = Natural)

array_eq_def:

varray_eq_def = Forall(i, Forall((a_1_to_i, b, c_1_to_i, d),
                                 Equals(Equals(VertExprArray(a_1_to_i, b), 
                                               VertExprArray(c_1_to_i, d)),
                                        And(Equals([a_1_to_i], [c_1_to_i]), 
                                            Equals(b, d))) \
                                 .with_wrap_after_operator()),
                      domain = Natural)

varray_eq_def:

array_neq_with_diff_len = Forall(
    (i, j), Forall((a_1_to_i, b_1_to_j),
                   NotEquals(ExprArray(a_1_to_i), ExprArray(b_1_to_j))),
    domain=Natural,
    condition=NotEquals(i, j))

array_neq_with_diff_len:

varray_neq_with_diff_len = Forall(
    (i, j), Forall((a_1_to_i, b_1_to_j),
                   NotEquals(VertExprArray(a_1_to_i), VertExprArray(b_1_to_j))),
    domain=Natural,
    condition=NotEquals(i, j))

varray_neq_with_diff_len:

print(varray_neq_with_diff_len.latex())

\forall_{i, j \in \mathbb{N}~|~i \neq j}~\left[\forall_{a_{1}, a_{2}, \ldots, a_{i}, b_{1}, b_{2}, \ldots, b_{j}}~\left(\left(\begin{array}{cccc} 
 \multirow{1}{*}{$\begin{array}{c} \uparrow \\ a_{1} \\ \downarrow \end{array}$} & \multirow{1}{*}{$\begin{array}{c} \uparrow \\ a_{2} \\ \downarrow \end{array}$} & \multirow{1}{*}{$\begin{array}{c} \uparrow \\ \cdots \\ \downarrow \end{array}$} & \multirow{1}{*}{$\begin{array}{c} \uparrow \\ a_{i} \\ \downarrow \end{array}$} \\
\end{array}
\right) \neq \left(\begin{array}{cccc} 
 \multirow{1}{*}{$\begin{array}{c} \uparrow \\ b_{1} \\ \downarrow \end{array}$} & \multirow{1}{*}{$\begin{array}{c} \uparrow \\ b_{2} \\ \downarrow \end{array}$} & \multirow{1}{*}{$\begin{array}{c} \uparrow \\ \cdots \\ \downarrow \end{array}$} & \multirow{1}{*}{$\begin{array}{c} \uparrow \\ b_{j} \\ \downarrow \end{array}$} \\
\end{array}
\right)\right)\right]

%end axioms

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