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 ExprRange, ExprTuple, IndexedVar
from proveit import k, m, x, y, A, B, S
from proveit.core_expr_types import x_1_to_m
from proveit.logic import (in_bool, And, Forall, Equals,
InSet, ProperSubset, SubsetEq, CartExp, CartProd)
from proveit.numbers import NaturalPos, one
%begin theorems
cart_exp_abstract_membership_def = Forall(
m, Forall((x, S),
Equals(InSet(x, CartExp(S, m)),
InSet(x, CartProd(ExprRange(k, S, one, m))))),
domain=NaturalPos)
cart_exp_explicit_membership_def = Forall(
m, Forall((x_1_to_m, S),
Equals(InSet(ExprTuple(x_1_to_m), CartExp(S, m)),
And(ExprRange(k, InSet(IndexedVar(x, k), S),
one, m)))),
domain=NaturalPos)
cart_exp_unfold_abstract = Forall(
m, Forall((x, S),
InSet(x, CartProd(ExprRange(k, S, one, m))),
condition=InSet(x, CartExp(S, m))),
domain=NaturalPos)
cart_exp_unfold_explicit = Forall(
m, Forall((x_1_to_m, S),
And(ExprRange(k, InSet(IndexedVar(x, k), S), one, m)),
condition=InSet(ExprTuple(x_1_to_m), CartExp(S, m))),
domain=NaturalPos)
cart_exp_fold_abstract = Forall(
m, Forall((x, S),
InSet(x, CartExp(S, m)),
condition=InSet(x, CartProd(ExprRange(k, S, one, m)))),
domain=NaturalPos)
cart_exp_fold_explicit = Forall(
m, Forall((x_1_to_m, S),
InSet(ExprTuple(x_1_to_m), CartExp(S, m)),
conditions=ExprRange(k, InSet(IndexedVar(x, k), S), one, m)),
domain=NaturalPos)
in_cart_exp_is_bool = Forall(
m, Forall((x, S),
in_bool(InSet(x, CartExp(S, m))),
condition=Forall(y, in_bool(InSet(y, S)))),
domain=NaturalPos)
cart_exp_proper_subset = Forall(
m, Forall((A, B), ProperSubset(CartExp(A, m), CartExp(B, m)),
condition=ProperSubset(A, B)),
domain=NaturalPos)
cart_exp_subset_eq = Forall(
m, Forall((A, B), SubsetEq(CartExp(A, m), CartExp(B, m)),
condition=SubsetEq(A, B)),
domain=NaturalPos)
%end theorems