InClass

class proveit.logic.InClass(element, domain, *, operator=None, styles=None)

Bases: proveit.relation.relation.Relation

Class membership denotes a collection of mathmematical objects that satisfy a certain common property. It is distinct from set membership, however. In particular, subsets of sets may be defined via subset comprehension, but there is no such analogue for classes. In this manner, classes can be more inclusive than sets without worrying about Russel’s paradox. A class that is not a set is called a proper class.

Note: Expressions objects that represent proper classes should have an attribute called ‘is_proper_class’ that is True. This will ensure that when such an object is used as a domain, it will automatically make an InClass condition instead of InSet.

Attributes Summary

inclass_expressions
known_memberships

Methods Summary

check_proven_class_membership(membership, …)
conclude(self, \*\*defaults_config)	Attempt to conclude that the element is in the domain.
deduce_not_in(self, \*\*defaults_config)	Deduce x not in C assuming not(A in C), where self = (x in C).
negated(self)	Return the negated membership expression, element not in domain.
negation_side_effects(self, judgment)	Fold Not(x in S) as (x not-in S) as an automatic side-effect.
reversed_operator_str(formatType)	Reversing in gives
shallow_simplification(self, \*[, must_evaluate])	Attempt to evaluate whether some x ∊ S is TRUE or FALSE using the ‘definition’ method of the domain’s ‘membership_object’ if there is one.
shallow_simplified(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘shallow_simplification’.
side_effects(self, judgment)	If the domain has a ‘membership_object’ method, side effects will also be generated from the ‘side_effects’ object that it generates.
yield_known_memberships(element, \*[, …])	Yield the known memberships of the given element applicable under the given assumptions.

Attributes Documentation

inclass_expressions = {(A, BOOLEAN): A in BOOLEAN, (_a, BOOLEAN): _a in BOOLEAN, ([not](FALSE), BOOLEAN): [not](FALSE) in BOOLEAN, ([not](A), BOOLEAN): [not](A) in BOOLEAN, ([not](_a), BOOLEAN): [not](_a) in BOOLEAN, (FALSE, BOOLEAN): FALSE in BOOLEAN, ([not]([not](TRUE)), BOOLEAN): [not]([not](TRUE)) in BOOLEAN, ([not](TRUE), BOOLEAN): [not](TRUE) in BOOLEAN, (TRUE, BOOLEAN): TRUE in BOOLEAN, ([not](TRUE = FALSE), BOOLEAN): [not](TRUE = FALSE) in BOOLEAN, (TRUE = FALSE, BOOLEAN): (TRUE = FALSE) in BOOLEAN, ([not](FALSE = TRUE), BOOLEAN): [not](FALSE = TRUE) in BOOLEAN, (FALSE = TRUE, BOOLEAN): (FALSE = TRUE) in BOOLEAN, (0, Natural): 0 in Natural, (n, Natural): n in Natural, (_a, Natural): _a in Natural, (y, Real): y in Real, (x, Real): x in Real, (_b, Real): _b in Real, (_a, Real): _a in Real, (0, Real): 0 in Real, (0, {0}): 0 in {0}, (0, IntegerNonPos): 0 in IntegerNonPos, (1, Natural): 1 in Natural, (1, Real): 1 in Real, (x, A): x in A, (x, B): x in B, (_a, A): _a in A, (_a, B): _a in B, (_a, _c): _a in _c, (_a, _b): _a in _b, (1, Integer): 1 in Integer, (1, Rational): 1 in Rational, (1, Complex): 1 in Complex, (1, RationalNonNeg): 1 in RationalNonNeg, (q, RationalNonNeg): q in RationalNonNeg, (_a, RationalNonNeg): _a in RationalNonNeg, (1, RealNonNeg): 1 in RealNonNeg, (x, RealNonNeg): x in RealNonNeg, (_a, RealNonNeg): _a in RealNonNeg, (2, Natural): 2 in Natural, (2, Real): 2 in Real, (2, Integer): 2 in Integer, (2, Rational): 2 in Rational, (2, Complex): 2 in Complex, (2, RationalNonNeg): 2 in RationalNonNeg, (2, RealNonNeg): 2 in RealNonNeg, (3, Natural): 3 in Natural, (3, Real): 3 in Real, (3, Integer): 3 in Integer, (3, Rational): 3 in Rational, (3, Complex): 3 in Complex, (3, RationalNonNeg): 3 in RationalNonNeg, (3, RealNonNeg): 3 in RealNonNeg, (4, Natural): 4 in Natural, (4, Real): 4 in Real, (4, Integer): 4 in Integer, (4, Rational): 4 in Rational, (4, Complex): 4 in Complex, (4, RationalNonNeg): 4 in RationalNonNeg, (4, RealNonNeg): 4 in RealNonNeg, (5, Natural): 5 in Natural, (5, Real): 5 in Real, (5, Integer): 5 in Integer, (5, Rational): 5 in Rational, (5, Complex): 5 in Complex, (5, RationalNonNeg): 5 in RationalNonNeg, (5, RealNonNeg): 5 in RealNonNeg, (6, Natural): 6 in Natural, (6, Real): 6 in Real, (6, Integer): 6 in Integer, (6, Rational): 6 in Rational, (6, Complex): 6 in Complex, (6, RationalNonNeg): 6 in RationalNonNeg, (6, RealNonNeg): 6 in RealNonNeg, (7, Natural): 7 in Natural, (7, Real): 7 in Real, (7, Integer): 7 in Integer, (7, Rational): 7 in Rational, (7, Complex): 7 in Complex, (7, RationalNonNeg): 7 in RationalNonNeg, (7, RealNonNeg): 7 in RealNonNeg, (8, Natural): 8 in Natural, (8, Real): 8 in Real, (8, Integer): 8 in Integer, (8, Rational): 8 in Rational, (8, Complex): 8 in Complex, (8, RationalNonNeg): 8 in RationalNonNeg, (8, RealNonNeg): 8 in RealNonNeg, (9, Natural): 9 in Natural, (9, Real): 9 in Real, (9, Integer): 9 in Integer, (9, Rational): 9 in Rational, (9, Complex): 9 in Complex, (9, RationalNonNeg): 9 in RationalNonNeg, (9, RealNonNeg): 9 in RealNonNeg, (a, IntegerNonPos): a in IntegerNonPos, (_a, IntegerNonPos): _a in IntegerNonPos, (0, Integer): 0 in Integer, (0, Rational): 0 in Rational, (0, Complex): 0 in Complex, (0, RationalNonPos): 0 in RationalNonPos, (q, RationalNonPos): q in RationalNonPos, (_a, RationalNonPos): _a in RationalNonPos, (0, RealNonPos): 0 in RealNonPos, (x, RealNonPos): x in RealNonPos, (_a, RealNonPos): _a in RealNonPos, ([not](0 < 0), BOOLEAN): [not](0 < 0) in BOOLEAN, (0 < 0, BOOLEAN): (0 < 0) in BOOLEAN, (0, RationalNonNeg): 0 in RationalNonNeg, (0, RealNonNeg): 0 in RealNonNeg, (b, Real): b in Real, (a, Real): a in Real, ([not](1 = 0), BOOLEAN): [not](1 = 0) in BOOLEAN, (1 = 0, BOOLEAN): (1 = 0) in BOOLEAN, ([not](0 = 1), BOOLEAN): [not](0 = 1) in BOOLEAN, (0 = 1, BOOLEAN): (0 = 1) in BOOLEAN, ([not](1 <= 0), BOOLEAN): [not](1 <= 0) in BOOLEAN, (1 <= 0, BOOLEAN): (1 <= 0) in BOOLEAN, ([not](2 < 1), BOOLEAN): [not](2 < 1) in BOOLEAN, (2 < 1, BOOLEAN): (2 < 1) in BOOLEAN, ([not](2 = 1), BOOLEAN): [not](2 = 1) in BOOLEAN, (2 = 1, BOOLEAN): (2 = 1) in BOOLEAN, ([not](1 = 2), BOOLEAN): [not](1 = 2) in BOOLEAN, (1 = 2, BOOLEAN): (1 = 2) in BOOLEAN, ([not](2 <= 1), BOOLEAN): [not](2 <= 1) in BOOLEAN, (2 <= 1, BOOLEAN): (2 <= 1) in BOOLEAN, ([not](3 < 2), BOOLEAN): [not](3 < 2) in BOOLEAN, (3 < 2, BOOLEAN): (3 < 2) in BOOLEAN, ([not](3 = 2), BOOLEAN): [not](3 = 2) in BOOLEAN, ([not](2 = 3), BOOLEAN): [not](2 = 3) in BOOLEAN, (3 = 2, BOOLEAN): (3 = 2) in BOOLEAN, (2 = 3, BOOLEAN): (2 = 3) in BOOLEAN, ([not](3 <= 2), BOOLEAN): [not](3 <= 2) in BOOLEAN, (3 <= 2, BOOLEAN): (3 <= 2) in BOOLEAN, ([not](4 < 3), BOOLEAN): [not](4 < 3) in BOOLEAN, (4 < 3, BOOLEAN): (4 < 3) in BOOLEAN, ([not](4 = 3), BOOLEAN): [not](4 = 3) in BOOLEAN, ([not](3 = 4), BOOLEAN): [not](3 = 4) in BOOLEAN, (4 = 3, BOOLEAN): (4 = 3) in BOOLEAN, (3 = 4, BOOLEAN): (3 = 4) in BOOLEAN, ([not](4 <= 3), BOOLEAN): [not](4 <= 3) in BOOLEAN, (4 <= 3, BOOLEAN): (4 <= 3) in BOOLEAN, ([not](5 < 4), BOOLEAN): [not](5 < 4) in BOOLEAN, (5 < 4, BOOLEAN): (5 < 4) in BOOLEAN, ([not](5 = 4), BOOLEAN): [not](5 = 4) in BOOLEAN, ([not](4 = 5), BOOLEAN): [not](4 = 5) in BOOLEAN, (5 = 4, BOOLEAN): (5 = 4) in BOOLEAN, (4 = 5, BOOLEAN): (4 = 5) in BOOLEAN, ([not](5 <= 4), BOOLEAN): [not](5 <= 4) in BOOLEAN, (5 <= 4, BOOLEAN): (5 <= 4) in BOOLEAN, ([not](6 < 5), BOOLEAN): [not](6 < 5) in BOOLEAN, (6 < 5, BOOLEAN): (6 < 5) in BOOLEAN, ([not](6 = 5), BOOLEAN): [not](6 = 5) in BOOLEAN, (6 = 5, BOOLEAN): (6 = 5) in BOOLEAN, ([not](5 = 6), BOOLEAN): [not](5 = 6) in BOOLEAN, (5 = 6, BOOLEAN): (5 = 6) in BOOLEAN, ([not](6 <= 5), BOOLEAN): [not](6 <= 5) in BOOLEAN, (6 <= 5, BOOLEAN): (6 <= 5) in BOOLEAN, ([not](7 < 6), BOOLEAN): [not](7 < 6) in BOOLEAN, (7 < 6, BOOLEAN): (7 < 6) in BOOLEAN, ([not](7 = 6), BOOLEAN): [not](7 = 6) in BOOLEAN, (7 = 6, BOOLEAN): (7 = 6) in BOOLEAN, ([not](6 = 7), BOOLEAN): [not](6 = 7) in BOOLEAN, (6 = 7, BOOLEAN): (6 = 7) in BOOLEAN, ([not](7 <= 6), BOOLEAN): [not](7 <= 6) in BOOLEAN, (7 <= 6, BOOLEAN): (7 <= 6) in BOOLEAN, ([not](8 < 7), BOOLEAN): [not](8 < 7) in BOOLEAN, (8 < 7, BOOLEAN): (8 < 7) in BOOLEAN, ([not](8 = 7), BOOLEAN): [not](8 = 7) in BOOLEAN, ([not](7 = 8), BOOLEAN): [not](7 = 8) in BOOLEAN, (8 = 7, BOOLEAN): (8 = 7) in BOOLEAN, (7 = 8, BOOLEAN): (7 = 8) in BOOLEAN, ([not](8 <= 7), BOOLEAN): [not](8 <= 7) in BOOLEAN, (8 <= 7, BOOLEAN): (8 <= 7) in BOOLEAN, ([not](9 < 8), BOOLEAN): [not](9 < 8) in BOOLEAN, (9 < 8, BOOLEAN): (9 < 8) in BOOLEAN, ([not](9 = 8), BOOLEAN): [not](9 = 8) in BOOLEAN, ([not](8 = 9), BOOLEAN): [not](8 = 9) in BOOLEAN, (9 = 8, BOOLEAN): (9 = 8) in BOOLEAN, (8 = 9, BOOLEAN): (8 = 9) in BOOLEAN, ([not](9 <= 8), BOOLEAN): [not](9 <= 8) in BOOLEAN, (9 <= 8, BOOLEAN): (9 <= 8) in BOOLEAN, (1, NaturalPos): 1 in NaturalPos, (n, NaturalPos): n in NaturalPos, (_a, NaturalPos): _a in NaturalPos, ([not](1 < 1), BOOLEAN): [not](1 < 1) in BOOLEAN, (1 < 1, BOOLEAN): (1 < 1) in BOOLEAN, (1, IntegerNonZero): 1 in IntegerNonZero, (a, IntegerNonZero): a in IntegerNonZero, (_a, IntegerNonZero): _a in IntegerNonZero, (1, RationalNonZero): 1 in RationalNonZero, (q, RationalNonZero): q in RationalNonZero, (_a, RationalNonZero): _a in RationalNonZero, (1, RealNonZero): 1 in RealNonZero, (x, RealNonZero): x in RealNonZero, (_a, RealNonZero): _a in RealNonZero, (1, ComplexNonZero): 1 in ComplexNonZero, (x, ComplexNonZero): x in ComplexNonZero, (_a, ComplexNonZero): _a in ComplexNonZero, (1, RationalPos): 1 in RationalPos, (q, RationalPos): q in RationalPos, (_a, RationalPos): _a in RationalPos, (1, RealPos): 1 in RealPos, (x, RealPos): x in RealPos, (_a, RealPos): _a in RealPos, (2, NaturalPos): 2 in NaturalPos, ([not](2 = 0), BOOLEAN): [not](2 = 0) in BOOLEAN, (2 = 0, BOOLEAN): (2 = 0) in BOOLEAN, ([not](0 = 2), BOOLEAN): [not](0 = 2) in BOOLEAN, (0 = 2, BOOLEAN): (0 = 2) in BOOLEAN, ([not](2 <= 0), BOOLEAN): [not](2 <= 0) in BOOLEAN, (2 <= 0, BOOLEAN): (2 <= 0) in BOOLEAN, (2, IntegerNonZero): 2 in IntegerNonZero, (2, RationalNonZero): 2 in RationalNonZero, (2, RealNonZero): 2 in RealNonZero, (2, ComplexNonZero): 2 in ComplexNonZero, (2, RationalPos): 2 in RationalPos, (2, RealPos): 2 in RealPos, (3, NaturalPos): 3 in NaturalPos, ([not](3 < 1), BOOLEAN): [not](3 < 1) in BOOLEAN, (3 < 1, BOOLEAN): (3 < 1) in BOOLEAN, ([not](3 = 0), BOOLEAN): [not](3 = 0) in BOOLEAN, (3 = 0, BOOLEAN): (3 = 0) in BOOLEAN, ([not](0 = 3), BOOLEAN): [not](0 = 3) in BOOLEAN, (0 = 3, BOOLEAN): (0 = 3) in BOOLEAN, ([not](3 <= 0), BOOLEAN): [not](3 <= 0) in BOOLEAN, (3 <= 0, BOOLEAN): (3 <= 0) in BOOLEAN, (3, IntegerNonZero): 3 in IntegerNonZero, (3, RationalNonZero): 3 in RationalNonZero, (3, RealNonZero): 3 in RealNonZero, (3, ComplexNonZero): 3 in ComplexNonZero, (3, RationalPos): 3 in RationalPos, (3, RealPos): 3 in RealPos, (4, NaturalPos): 4 in NaturalPos, ([not](4 < 1), BOOLEAN): [not](4 < 1) in BOOLEAN, (4 < 1, BOOLEAN): (4 < 1) in BOOLEAN, ([not](4 = 0), BOOLEAN): [not](4 = 0) in BOOLEAN, (4 = 0, BOOLEAN): (4 = 0) in BOOLEAN, ([not](0 = 4), BOOLEAN): [not](0 = 4) in BOOLEAN, (0 = 4, BOOLEAN): (0 = 4) in BOOLEAN, ([not](4 <= 0), BOOLEAN): [not](4 <= 0) in BOOLEAN, (4 <= 0, BOOLEAN): (4 <= 0) in BOOLEAN, (4, IntegerNonZero): 4 in IntegerNonZero, (4, RationalNonZero): 4 in RationalNonZero, (4, RealNonZero): 4 in RealNonZero, (4, ComplexNonZero): 4 in ComplexNonZero, (4, RationalPos): 4 in RationalPos, (4, RealPos): 4 in RealPos, (5, NaturalPos): 5 in NaturalPos, ([not](5 < 1), BOOLEAN): [not](5 < 1) in BOOLEAN, (5 < 1, BOOLEAN): (5 < 1) in BOOLEAN, ([not](5 = 0), BOOLEAN): [not](5 = 0) in BOOLEAN, ([not](0 = 5), BOOLEAN): [not](0 = 5) in BOOLEAN, (5 = 0, BOOLEAN): (5 = 0) in BOOLEAN, (0 = 5, BOOLEAN): (0 = 5) in BOOLEAN, ([not](5 <= 0), BOOLEAN): [not](5 <= 0) in BOOLEAN, (5 <= 0, BOOLEAN): (5 <= 0) in BOOLEAN, (5, IntegerNonZero): 5 in IntegerNonZero, (5, RationalNonZero): 5 in RationalNonZero, (5, RealNonZero): 5 in RealNonZero, (5, ComplexNonZero): 5 in ComplexNonZero, (5, RationalPos): 5 in RationalPos, (5, RealPos): 5 in RealPos, (6, NaturalPos): 6 in NaturalPos, ([not](6 < 1), BOOLEAN): [not](6 < 1) in BOOLEAN, (6 < 1, BOOLEAN): (6 < 1) in BOOLEAN, ([not](6 = 0), BOOLEAN): [not](6 = 0) in BOOLEAN, (6 = 0, BOOLEAN): (6 = 0) in BOOLEAN, ([not](0 = 6), BOOLEAN): [not](0 = 6) in BOOLEAN, (0 = 6, BOOLEAN): (0 = 6) in BOOLEAN, ([not](6 <= 0), BOOLEAN): [not](6 <= 0) in BOOLEAN, (6 <= 0, BOOLEAN): (6 <= 0) in BOOLEAN, (6, IntegerNonZero): 6 in IntegerNonZero, (6, RationalNonZero): 6 in RationalNonZero, (6, RealNonZero): 6 in RealNonZero, (6, ComplexNonZero): 6 in ComplexNonZero, (6, RationalPos): 6 in RationalPos, (6, RealPos): 6 in RealPos, (7, NaturalPos): 7 in NaturalPos, ([not](7 < 1), BOOLEAN): [not](7 < 1) in BOOLEAN, (7 < 1, BOOLEAN): (7 < 1) in BOOLEAN, ([not](7 = 0), BOOLEAN): [not](7 = 0) in BOOLEAN, (7 = 0, BOOLEAN): (7 = 0) in BOOLEAN, ([not](0 = 7), BOOLEAN): [not](0 = 7) in BOOLEAN, (0 = 7, BOOLEAN): (0 = 7) in BOOLEAN, ([not](7 <= 0), BOOLEAN): [not](7 <= 0) in BOOLEAN, (7 <= 0, BOOLEAN): (7 <= 0) in BOOLEAN, (7, IntegerNonZero): 7 in IntegerNonZero, (7, RationalNonZero): 7 in RationalNonZero, (7, RealNonZero): 7 in RealNonZero, (7, ComplexNonZero): 7 in ComplexNonZero, (7, RationalPos): 7 in RationalPos, (7, RealPos): 7 in RealPos, (8, NaturalPos): 8 in NaturalPos, ([not](8 < 1), BOOLEAN): [not](8 < 1) in BOOLEAN, (8 < 1, BOOLEAN): (8 < 1) in BOOLEAN, ([not](8 = 0), BOOLEAN): [not](8 = 0) in BOOLEAN, (8 = 0, BOOLEAN): (8 = 0) in BOOLEAN, ([not](0 = 8), BOOLEAN): [not](0 = 8) in BOOLEAN, (0 = 8, BOOLEAN): (0 = 8) in BOOLEAN, ([not](8 <= 0), BOOLEAN): [not](8 <= 0) in BOOLEAN, (8 <= 0, BOOLEAN): (8 <= 0) in BOOLEAN, (8, IntegerNonZero): 8 in IntegerNonZero, (8, RationalNonZero): 8 in RationalNonZero, (8, RealNonZero): 8 in RealNonZero, (8, ComplexNonZero): 8 in ComplexNonZero, (8, RationalPos): 8 in RationalPos, (8, RealPos): 8 in RealPos, (9, NaturalPos): 9 in NaturalPos, ([not](9 < 1), BOOLEAN): [not](9 < 1) in BOOLEAN, (9 < 1, BOOLEAN): (9 < 1) in BOOLEAN, ([not](9 = 0), BOOLEAN): [not](9 = 0) in BOOLEAN, (9 = 0, BOOLEAN): (9 = 0) in BOOLEAN, ([not](0 = 9), BOOLEAN): [not](0 = 9) in BOOLEAN, (0 = 9, BOOLEAN): (0 = 9) in BOOLEAN, ([not](9 <= 0), BOOLEAN): [not](9 <= 0) in BOOLEAN, (9 <= 0, BOOLEAN): (9 <= 0) in BOOLEAN, (9, IntegerNonZero): 9 in IntegerNonZero, (9, RationalNonZero): 9 in RationalNonZero, (9, RealNonZero): 9 in RealNonZero, (9, ComplexNonZero): 9 in ComplexNonZero, (9, RationalPos): 9 in RationalPos, (9, RealPos): 9 in RealPos, (e, RealPos): e in RealPos, (e, Real): e in Real, (e, Complex): e in Complex, (e, RealNonZero): e in RealNonZero, ([not](0 = e), BOOLEAN): [not](0 = e) in BOOLEAN, (0 = e, BOOLEAN): (0 = e) in BOOLEAN, ([not](e = 0), BOOLEAN): [not](e = 0) in BOOLEAN, (e = 0, BOOLEAN): (e = 0) in BOOLEAN, (e, ComplexNonZero): e in ComplexNonZero, (e, RealNonNeg): e in RealNonNeg, ([not](e < 0), BOOLEAN): [not](e < 0) in BOOLEAN, (e < 0, BOOLEAN): (e < 0) in BOOLEAN, ([not](e <= 0), BOOLEAN): [not](e <= 0) in BOOLEAN, (e <= 0, BOOLEAN): (e <= 0) in BOOLEAN, (pi, RealPos): pi in RealPos, (pi, Real): pi in Real, (pi, Complex): pi in Complex, (pi, RealNonZero): pi in RealNonZero, ([not](0 = pi), BOOLEAN): [not](0 = pi) in BOOLEAN, (0 = pi, BOOLEAN): (0 = pi) in BOOLEAN, ([not](pi = 0), BOOLEAN): [not](pi = 0) in BOOLEAN, (pi = 0, BOOLEAN): (pi = 0) in BOOLEAN, (pi, ComplexNonZero): pi in ComplexNonZero, (pi, RealNonNeg): pi in RealNonNeg, ([not](pi < 0), BOOLEAN): [not](pi < 0) in BOOLEAN, (pi < 0, BOOLEAN): (pi < 0) in BOOLEAN, ([not](pi <= 0), BOOLEAN): [not](pi <= 0) in BOOLEAN, (pi <= 0, BOOLEAN): (pi <= 0) in BOOLEAN, (i, Complex): i in Complex, (i, ComplexNonZero): i in ComplexNonZero, ([not](0 = i), BOOLEAN): [not](0 = i) in BOOLEAN, ([not](i = 0), BOOLEAN): [not](i = 0) in BOOLEAN, (0 = i, BOOLEAN): (0 = i) in BOOLEAN, (i = 0, BOOLEAN): (i = 0) in BOOLEAN, (Rational, Fields(+, *)): Rational in_c Fields(+, *), (Real, Fields(+, *)): Real in_c Fields(+, *), (Complex, Fields(+, *)): Complex in_c Fields(+, *)}

known_memberships = {_a: OrderedSet([{_a} |- _a in BOOLEAN, {_a in BOOLEAN} |- _a in BOOLEAN, {(_a = TRUE) or (_a = FALSE)} |- _a in BOOLEAN, {[not](_a) in BOOLEAN} |- _a in BOOLEAN, {_a in Natural} |- _a in Natural, {_a in Real} |- _a in Real, {_a in _c} |- _a in _c, {_c proper_subset _b, _a in _c} |- _a in _b, {_a in RationalNonNeg} |- _a in RationalNonNeg, {_a in RealNonNeg} |- _a in RealNonNeg, {_a in IntegerNonPos} |- _a in IntegerNonPos, {_a in RationalNonPos} |- _a in RationalNonPos, {_a in RealNonPos} |- _a in RealNonPos, {_c subset_eq _b, _a in _c} |- _a in _b, {_a in NaturalPos} |- _a in NaturalPos, {_a in IntegerNonZero} |- _a in IntegerNonZero, {_a in RationalNonZero} |- _a in RationalNonZero, {_a in RealNonZero} |- _a in RealNonZero, {_a in ComplexNonZero} |- _a in ComplexNonZero, {_a in RationalPos} |- _a in RationalPos, {_a in RealPos} |- _a in RealPos]), A: OrderedSet([{A} |- A in BOOLEAN, {A in BOOLEAN} |- A in BOOLEAN, {(A = TRUE) or (A = FALSE)} |- A in BOOLEAN, {[not](A) in BOOLEAN} |- A in BOOLEAN]), [not](FALSE): OrderedSet([|- [not](FALSE) in BOOLEAN]), [not](_a): OrderedSet([{[not](_a) in BOOLEAN} |- [not](_a) in BOOLEAN]), [not](A): OrderedSet([{[not](A) in BOOLEAN} |- [not](A) in BOOLEAN]), FALSE: OrderedSet([|- FALSE in BOOLEAN]), [not]([not](TRUE)): OrderedSet([|- [not]([not](TRUE)) in BOOLEAN]), [not](TRUE): OrderedSet([|- [not](TRUE) in BOOLEAN]), TRUE: OrderedSet([|- TRUE in BOOLEAN]), [not](TRUE = FALSE): OrderedSet([|- [not](TRUE = FALSE) in BOOLEAN]), TRUE = FALSE: OrderedSet([|- (TRUE = FALSE) in BOOLEAN]), [not](FALSE = TRUE): OrderedSet([|- [not](FALSE = TRUE) in BOOLEAN]), FALSE = TRUE: OrderedSet([|- (FALSE = TRUE) in BOOLEAN]), 0: OrderedSet([|- 0 in Natural, |- 0 in IntegerNonPos, |- 0 in Integer, |- 0 in Rational, |- 0 in Real, |- 0 in Complex, |- 0 in RationalNonPos, |- 0 in RealNonPos, |- 0 in RationalNonNeg, |- 0 in RealNonNeg]), n: OrderedSet([{n in Natural} |- n in Natural, {n in NaturalPos} |- n in NaturalPos]), _b: OrderedSet([{_b in Real} |- _b in Real]), x: OrderedSet([{x in Real} |- x in Real, {x in A} |- x in A, {A proper_subset B, x in A} |- x in B, {x in RealNonNeg} |- x in RealNonNeg, {x in RealNonPos} |- x in RealNonPos, {A subset_eq B, x in A} |- x in B, {x in RealNonZero} |- x in RealNonZero, {x in ComplexNonZero} |- x in ComplexNonZero, {x in RealPos} |- x in RealPos]), y: OrderedSet([{y in Real} |- y in Real]), 1: OrderedSet([|- 1 in Natural, |- 1 in Integer, |- 1 in Rational, |- 1 in Real, |- 1 in Complex, |- 1 in RationalNonNeg, |- 1 in RealNonNeg, |- 1 in NaturalPos, |- 1 in IntegerNonZero, |- 1 in RationalNonZero, |- 1 in RealNonZero, |- 1 in ComplexNonZero, |- 1 in RationalPos, |- 1 in RealPos]), q: OrderedSet([{q in RationalNonNeg} |- q in RationalNonNeg, {q in RationalNonPos} |- q in RationalNonPos, {q in RationalNonZero} |- q in RationalNonZero, {q in RationalPos} |- q in RationalPos]), 2: OrderedSet([|- 2 in Natural, |- 2 in Integer, |- 2 in Rational, |- 2 in Real, |- 2 in Complex, |- 2 in RationalNonNeg, |- 2 in RealNonNeg, |- 2 in NaturalPos, |- 2 in IntegerNonZero, |- 2 in RationalNonZero, |- 2 in RealNonZero, |- 2 in ComplexNonZero, |- 2 in RationalPos, |- 2 in RealPos]), 3: OrderedSet([|- 3 in Natural, |- 3 in Integer, |- 3 in Rational, |- 3 in Real, |- 3 in Complex, |- 3 in RationalNonNeg, |- 3 in RealNonNeg, |- 3 in NaturalPos, |- 3 in IntegerNonZero, |- 3 in RationalNonZero, |- 3 in RealNonZero, |- 3 in ComplexNonZero, |- 3 in RationalPos, |- 3 in RealPos]), 4: OrderedSet([|- 4 in Natural, |- 4 in Integer, |- 4 in Rational, |- 4 in Real, |- 4 in Complex, |- 4 in RationalNonNeg, |- 4 in RealNonNeg, |- 4 in NaturalPos, |- 4 in IntegerNonZero, |- 4 in RationalNonZero, |- 4 in RealNonZero, |- 4 in ComplexNonZero, |- 4 in RationalPos, |- 4 in RealPos]), 5: OrderedSet([|- 5 in Natural, |- 5 in Integer, |- 5 in Rational, |- 5 in Real, |- 5 in Complex, |- 5 in RationalNonNeg, |- 5 in RealNonNeg, |- 5 in NaturalPos, |- 5 in IntegerNonZero, |- 5 in RationalNonZero, |- 5 in RealNonZero, |- 5 in ComplexNonZero, |- 5 in RationalPos, |- 5 in RealPos]), 6: OrderedSet([|- 6 in Natural, |- 6 in Integer, |- 6 in Rational, |- 6 in Real, |- 6 in Complex, |- 6 in RationalNonNeg, |- 6 in RealNonNeg, |- 6 in NaturalPos, |- 6 in IntegerNonZero, |- 6 in RationalNonZero, |- 6 in RealNonZero, |- 6 in ComplexNonZero, |- 6 in RationalPos, |- 6 in RealPos]), 7: OrderedSet([|- 7 in Natural, |- 7 in Integer, |- 7 in Rational, |- 7 in Real, |- 7 in Complex, |- 7 in RationalNonNeg, |- 7 in RealNonNeg, |- 7 in NaturalPos, |- 7 in IntegerNonZero, |- 7 in RationalNonZero, |- 7 in RealNonZero, |- 7 in ComplexNonZero, |- 7 in RationalPos, |- 7 in RealPos]), 8: OrderedSet([|- 8 in Natural, |- 8 in Integer, |- 8 in Rational, |- 8 in Real, |- 8 in Complex, |- 8 in RationalNonNeg, |- 8 in RealNonNeg, |- 8 in NaturalPos, |- 8 in IntegerNonZero, |- 8 in RationalNonZero, |- 8 in RealNonZero, |- 8 in ComplexNonZero, |- 8 in RationalPos, |- 8 in RealPos]), 9: OrderedSet([|- 9 in Natural, |- 9 in Integer, |- 9 in Rational, |- 9 in Real, |- 9 in Complex, |- 9 in RationalNonNeg, |- 9 in RealNonNeg, |- 9 in NaturalPos, |- 9 in IntegerNonZero, |- 9 in RationalNonZero, |- 9 in RealNonZero, |- 9 in ComplexNonZero, |- 9 in RationalPos, |- 9 in RealPos]), a: OrderedSet([{a in IntegerNonPos} |- a in IntegerNonPos, {a in Real} |- a in Real, {a in IntegerNonZero} |- a in IntegerNonZero]), [not](0 < 0): OrderedSet([|- [not](0 < 0) in BOOLEAN]), 0 < 0: OrderedSet([|- (0 < 0) in BOOLEAN]), b: OrderedSet([{b in Real} |- b in Real]), [not](1 = 0): OrderedSet([|- [not](1 = 0) in BOOLEAN]), 1 = 0: OrderedSet([|- (1 = 0) in BOOLEAN]), [not](0 = 1): OrderedSet([|- [not](0 = 1) in BOOLEAN]), 0 = 1: OrderedSet([|- (0 = 1) in BOOLEAN]), [not](1 <= 0): OrderedSet([|- [not](1 <= 0) in BOOLEAN]), 1 <= 0: OrderedSet([|- (1 <= 0) in BOOLEAN]), [not](2 < 1): OrderedSet([|- [not](2 < 1) in BOOLEAN]), 2 < 1: OrderedSet([|- (2 < 1) in BOOLEAN]), [not](2 = 1): OrderedSet([|- [not](2 = 1) in BOOLEAN]), 2 = 1: OrderedSet([|- (2 = 1) in BOOLEAN]), [not](1 = 2): OrderedSet([|- [not](1 = 2) in BOOLEAN]), 1 = 2: OrderedSet([|- (1 = 2) in BOOLEAN]), [not](2 <= 1): OrderedSet([|- [not](2 <= 1) in BOOLEAN]), 2 <= 1: OrderedSet([|- (2 <= 1) in BOOLEAN]), [not](3 < 2): OrderedSet([|- [not](3 < 2) in BOOLEAN]), 3 < 2: OrderedSet([|- (3 < 2) in BOOLEAN]), [not](3 = 2): OrderedSet([|- [not](3 = 2) in BOOLEAN]), 3 = 2: OrderedSet([|- (3 = 2) in BOOLEAN]), [not](2 = 3): OrderedSet([|- [not](2 = 3) in BOOLEAN]), 2 = 3: OrderedSet([|- (2 = 3) in BOOLEAN]), [not](3 <= 2): OrderedSet([|- [not](3 <= 2) in BOOLEAN]), 3 <= 2: OrderedSet([|- (3 <= 2) in BOOLEAN]), [not](4 < 3): OrderedSet([|- [not](4 < 3) in BOOLEAN]), 4 < 3: OrderedSet([|- (4 < 3) in BOOLEAN]), [not](4 = 3): OrderedSet([|- [not](4 = 3) in BOOLEAN]), 4 = 3: OrderedSet([|- (4 = 3) in BOOLEAN]), [not](3 = 4): OrderedSet([|- [not](3 = 4) in BOOLEAN]), 3 = 4: OrderedSet([|- (3 = 4) in BOOLEAN]), [not](4 <= 3): OrderedSet([|- [not](4 <= 3) in BOOLEAN]), 4 <= 3: OrderedSet([|- (4 <= 3) in BOOLEAN]), [not](5 < 4): OrderedSet([|- [not](5 < 4) in BOOLEAN]), 5 < 4: OrderedSet([|- (5 < 4) in BOOLEAN]), [not](5 = 4): OrderedSet([|- [not](5 = 4) in BOOLEAN]), 5 = 4: OrderedSet([|- (5 = 4) in BOOLEAN]), [not](4 = 5): OrderedSet([|- [not](4 = 5) in BOOLEAN]), 4 = 5: OrderedSet([|- (4 = 5) in BOOLEAN]), [not](5 <= 4): OrderedSet([|- [not](5 <= 4) in BOOLEAN]), 5 <= 4: OrderedSet([|- (5 <= 4) in BOOLEAN]), [not](6 < 5): OrderedSet([|- [not](6 < 5) in BOOLEAN]), 6 < 5: OrderedSet([|- (6 < 5) in BOOLEAN]), [not](6 = 5): OrderedSet([|- [not](6 = 5) in BOOLEAN]), 6 = 5: OrderedSet([|- (6 = 5) in BOOLEAN]), [not](5 = 6): OrderedSet([|- [not](5 = 6) in BOOLEAN]), 5 = 6: OrderedSet([|- (5 = 6) in BOOLEAN]), [not](6 <= 5): OrderedSet([|- [not](6 <= 5) in BOOLEAN]), 6 <= 5: OrderedSet([|- (6 <= 5) in BOOLEAN]), [not](7 < 6): OrderedSet([|- [not](7 < 6) in BOOLEAN]), 7 < 6: OrderedSet([|- (7 < 6) in BOOLEAN]), [not](7 = 6): OrderedSet([|- [not](7 = 6) in BOOLEAN]), 7 = 6: OrderedSet([|- (7 = 6) in BOOLEAN]), [not](6 = 7): OrderedSet([|- [not](6 = 7) in BOOLEAN]), 6 = 7: OrderedSet([|- (6 = 7) in BOOLEAN]), [not](7 <= 6): OrderedSet([|- [not](7 <= 6) in BOOLEAN]), 7 <= 6: OrderedSet([|- (7 <= 6) in BOOLEAN]), [not](8 < 7): OrderedSet([|- [not](8 < 7) in BOOLEAN]), 8 < 7: OrderedSet([|- (8 < 7) in BOOLEAN]), [not](8 = 7): OrderedSet([|- [not](8 = 7) in BOOLEAN]), 8 = 7: OrderedSet([|- (8 = 7) in BOOLEAN]), [not](7 = 8): OrderedSet([|- [not](7 = 8) in BOOLEAN]), 7 = 8: OrderedSet([|- (7 = 8) in BOOLEAN]), [not](8 <= 7): OrderedSet([|- [not](8 <= 7) in BOOLEAN]), 8 <= 7: OrderedSet([|- (8 <= 7) in BOOLEAN]), [not](9 < 8): OrderedSet([|- [not](9 < 8) in BOOLEAN]), 9 < 8: OrderedSet([|- (9 < 8) in BOOLEAN]), [not](9 = 8): OrderedSet([|- [not](9 = 8) in BOOLEAN]), 9 = 8: OrderedSet([|- (9 = 8) in BOOLEAN]), [not](8 = 9): OrderedSet([|- [not](8 = 9) in BOOLEAN]), 8 = 9: OrderedSet([|- (8 = 9) in BOOLEAN]), [not](9 <= 8): OrderedSet([|- [not](9 <= 8) in BOOLEAN]), 9 <= 8: OrderedSet([|- (9 <= 8) in BOOLEAN]), [not](1 < 1): OrderedSet([|- [not](1 < 1) in BOOLEAN]), 1 < 1: OrderedSet([|- (1 < 1) in BOOLEAN]), [not](2 = 0): OrderedSet([|- [not](2 = 0) in BOOLEAN]), 2 = 0: OrderedSet([|- (2 = 0) in BOOLEAN]), [not](0 = 2): OrderedSet([|- [not](0 = 2) in BOOLEAN]), 0 = 2: OrderedSet([|- (0 = 2) in BOOLEAN]), [not](2 <= 0): OrderedSet([|- [not](2 <= 0) in BOOLEAN]), 2 <= 0: OrderedSet([|- (2 <= 0) in BOOLEAN]), [not](3 < 1): OrderedSet([|- [not](3 < 1) in BOOLEAN]), 3 < 1: OrderedSet([|- (3 < 1) in BOOLEAN]), [not](3 = 0): OrderedSet([|- [not](3 = 0) in BOOLEAN]), 3 = 0: OrderedSet([|- (3 = 0) in BOOLEAN]), [not](0 = 3): OrderedSet([|- [not](0 = 3) in BOOLEAN]), 0 = 3: OrderedSet([|- (0 = 3) in BOOLEAN]), [not](3 <= 0): OrderedSet([|- [not](3 <= 0) in BOOLEAN]), 3 <= 0: OrderedSet([|- (3 <= 0) in BOOLEAN]), [not](4 < 1): OrderedSet([|- [not](4 < 1) in BOOLEAN]), 4 < 1: OrderedSet([|- (4 < 1) in BOOLEAN]), [not](4 = 0): OrderedSet([|- [not](4 = 0) in BOOLEAN]), 4 = 0: OrderedSet([|- (4 = 0) in BOOLEAN]), [not](0 = 4): OrderedSet([|- [not](0 = 4) in BOOLEAN]), 0 = 4: OrderedSet([|- (0 = 4) in BOOLEAN]), [not](4 <= 0): OrderedSet([|- [not](4 <= 0) in BOOLEAN]), 4 <= 0: OrderedSet([|- (4 <= 0) in BOOLEAN]), [not](5 < 1): OrderedSet([|- [not](5 < 1) in BOOLEAN]), 5 < 1: OrderedSet([|- (5 < 1) in BOOLEAN]), [not](5 = 0): OrderedSet([|- [not](5 = 0) in BOOLEAN]), 5 = 0: OrderedSet([|- (5 = 0) in BOOLEAN]), [not](0 = 5): OrderedSet([|- [not](0 = 5) in BOOLEAN]), 0 = 5: OrderedSet([|- (0 = 5) in BOOLEAN]), [not](5 <= 0): OrderedSet([|- [not](5 <= 0) in BOOLEAN]), 5 <= 0: OrderedSet([|- (5 <= 0) in BOOLEAN]), [not](6 < 1): OrderedSet([|- [not](6 < 1) in BOOLEAN]), 6 < 1: OrderedSet([|- (6 < 1) in BOOLEAN]), [not](6 = 0): OrderedSet([|- [not](6 = 0) in BOOLEAN]), 6 = 0: OrderedSet([|- (6 = 0) in BOOLEAN]), [not](0 = 6): OrderedSet([|- [not](0 = 6) in BOOLEAN]), 0 = 6: OrderedSet([|- (0 = 6) in BOOLEAN]), [not](6 <= 0): OrderedSet([|- [not](6 <= 0) in BOOLEAN]), 6 <= 0: OrderedSet([|- (6 <= 0) in BOOLEAN]), [not](7 < 1): OrderedSet([|- [not](7 < 1) in BOOLEAN]), 7 < 1: OrderedSet([|- (7 < 1) in BOOLEAN]), [not](7 = 0): OrderedSet([|- [not](7 = 0) in BOOLEAN]), 7 = 0: OrderedSet([|- (7 = 0) in BOOLEAN]), [not](0 = 7): OrderedSet([|- [not](0 = 7) in BOOLEAN]), 0 = 7: OrderedSet([|- (0 = 7) in BOOLEAN]), [not](7 <= 0): OrderedSet([|- [not](7 <= 0) in BOOLEAN]), 7 <= 0: OrderedSet([|- (7 <= 0) in BOOLEAN]), [not](8 < 1): OrderedSet([|- [not](8 < 1) in BOOLEAN]), 8 < 1: OrderedSet([|- (8 < 1) in BOOLEAN]), [not](8 = 0): OrderedSet([|- [not](8 = 0) in BOOLEAN]), 8 = 0: OrderedSet([|- (8 = 0) in BOOLEAN]), [not](0 = 8): OrderedSet([|- [not](0 = 8) in BOOLEAN]), 0 = 8: OrderedSet([|- (0 = 8) in BOOLEAN]), [not](8 <= 0): OrderedSet([|- [not](8 <= 0) in BOOLEAN]), 8 <= 0: OrderedSet([|- (8 <= 0) in BOOLEAN]), [not](9 < 1): OrderedSet([|- [not](9 < 1) in BOOLEAN]), 9 < 1: OrderedSet([|- (9 < 1) in BOOLEAN]), [not](9 = 0): OrderedSet([|- [not](9 = 0) in BOOLEAN]), 9 = 0: OrderedSet([|- (9 = 0) in BOOLEAN]), [not](0 = 9): OrderedSet([|- [not](0 = 9) in BOOLEAN]), 0 = 9: OrderedSet([|- (0 = 9) in BOOLEAN]), [not](9 <= 0): OrderedSet([|- [not](9 <= 0) in BOOLEAN]), 9 <= 0: OrderedSet([|- (9 <= 0) in BOOLEAN]), e: OrderedSet([|- e in RealPos, |- e in Real, |- e in Complex, |- e in RealNonZero, |- e in ComplexNonZero, |- e in RealNonNeg]), [not](0 = e): OrderedSet([|- [not](0 = e) in BOOLEAN]), 0 = e: OrderedSet([|- (0 = e) in BOOLEAN]), [not](e = 0): OrderedSet([|- [not](e = 0) in BOOLEAN]), e = 0: OrderedSet([|- (e = 0) in BOOLEAN]), [not](e < 0): OrderedSet([|- [not](e < 0) in BOOLEAN]), e < 0: OrderedSet([|- (e < 0) in BOOLEAN]), [not](e <= 0): OrderedSet([|- [not](e <= 0) in BOOLEAN]), e <= 0: OrderedSet([|- (e <= 0) in BOOLEAN]), pi: OrderedSet([|- pi in RealPos, |- pi in Real, |- pi in Complex, |- pi in RealNonZero, |- pi in ComplexNonZero, |- pi in RealNonNeg]), [not](0 = pi): OrderedSet([|- [not](0 = pi) in BOOLEAN]), 0 = pi: OrderedSet([|- (0 = pi) in BOOLEAN]), [not](pi = 0): OrderedSet([|- [not](pi = 0) in BOOLEAN]), pi = 0: OrderedSet([|- (pi = 0) in BOOLEAN]), [not](pi < 0): OrderedSet([|- [not](pi < 0) in BOOLEAN]), pi < 0: OrderedSet([|- (pi < 0) in BOOLEAN]), [not](pi <= 0): OrderedSet([|- [not](pi <= 0) in BOOLEAN]), pi <= 0: OrderedSet([|- (pi <= 0) in BOOLEAN]), i: OrderedSet([|- i in Complex, |- i in ComplexNonZero]), [not](0 = i): OrderedSet([|- [not](0 = i) in BOOLEAN]), 0 = i: OrderedSet([|- (0 = i) in BOOLEAN]), [not](i = 0): OrderedSet([|- [not](i = 0) in BOOLEAN]), i = 0: OrderedSet([|- (i = 0) in BOOLEAN]), Rational: OrderedSet([|- Rational in_c Fields(+, *)]), Real: OrderedSet([|- Real in_c Fields(+, *)]), Complex: OrderedSet([|- Complex in_c Fields(+, *)])}

Methods Documentation

static check_proven_class_membership(membership, element, class_of_class)

conclude(self, \*\*defaults_config)

Attempt to conclude that the element is in the domain. Try standard relation strategies (evaluate or somplify both sides). If that doesn’t work, try using the domain-specific ‘conclude’ method of the membership object.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_not_in(self, \*\*defaults_config)

Deduce x not in C assuming not(A in C), where self = (x in C).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

negated(self)

Return the negated membership expression, element not in domain.

negation_side_effects(self, judgment)

Fold Not(x in S) as (x not-in S) as an automatic side-effect.

static reversed_operator_str(formatType)

Reversing in gives

1. Reversing “in” gives “contains”.

shallow_simplification(self, \*, must_evaluate=False, \*\*defaults_config)

Attempt to evaluate whether some x ∊ S is TRUE or FALSE using the ‘definition’ method of the domain’s ‘membership_object’ if there is one.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘shallow_simplified’ returns the right-hand side of ‘shallow_simplification’. ‘shallow_simplify’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘shallow_simplification’ for the inner expression.

shallow_simplified(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘shallow_simplification’.

side_effects(self, judgment)

If the domain has a ‘membership_object’ method, side effects will also be generated from the ‘side_effects’ object that it generates.

static yield_known_memberships(element, \*, include_canonical_forms=True, assumptions=None)

Yield the known memberships of the given element applicable under the given assumptions. In ‘include_canonical_forms’ is True, then we can treat elements of the same canonical form as the same for this purpose.