InSet

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

Bases: proveit.logic.InClass

Set membership is a special case of class membership, so we’ll derive from InClass for code re-use. The operators are distinct (though the formatting is the same).

Attributes Summary

known_memberships

Methods Summary

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).
negation_side_effects(self, judgment)	Fold Not(x in S) as (x not-in S) as an automatic side-effect.
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.

Attributes Documentation

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

conclude(self, \*\*defaults_config)

Attempt to conclude that the element is in the domain. First see if there is an equivalent known membership to use (same domain). If not, see if there is a membership object that is readily provable and conclude via that object if so. Then check for a membership that is at least as strong with a possibly different domain to use. Finally, defer to InClass.conclude which defers to InRelation.conclude and attempts simplifications.

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.

negation_side_effects(self, judgment)

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

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.