Axioms for the theory of proveit.logic.sets.unification

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.logic import Forall, Exists, Or, Equals, InSet, Union
from proveit import m, n, x, Q, R
from proveit.core_expr_types import y_1_to_n, A_1_to_m, Q__y_1_to_n, R__y_1_to_n, S_1_to_n
from proveit.logic.sets import x_in_any_A, general_unionall_Ryn
from proveit.numbers import NaturalPos
%begin axioms
Defining axioms for theory 'proveit.logic.sets.unification'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Membership in the union of sets is the same as having membership in any of the sets being unified:

In [2]:
union_def = Forall(m, Forall((x, A_1_to_m), 
                            Equals(InSet(x, Union(A_1_to_m)), x_in_any_A).with_wrap_after_operator()),
In [3]:
union_all_def = Forall(
    n, Forall((S_1_to_n, Q, R, x), 
              Equals(InSet(x, general_unionall_Ryn),
                     Exists(y_1_to_n, InSet(x, R__y_1_to_n), 
                            domains=[S_1_to_n], conditions=[Q__y_1_to_n]))
In [4]:
%end axioms
These axioms may now be imported from the theory package: proveit.logic.sets.unification