InSet

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

Bases: proveit.relation.relation.Relation

Attributes Summary

inset_expressions

known_memberships

Methods Summary

conclude(self, \*\*defaults_config)

Attempt to conclude that the element is in the domain. First,

deduce_not_in(self, \*\*defaults_config)

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

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

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

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

side_effects(self, judgment)

Store the proven membership in known_memberships.

yield_known_memberships(element[, assumptions])

Yield the known memberships of the given element applicable under the given assumptions.

Attributes Documentation

inset_expressions = {(A, BOOLEAN): A in BOOLEAN, (_a, BOOLEAN): _a in BOOLEAN, (TRUE, BOOLEAN): TRUE in BOOLEAN, (not(TRUE = FALSE), BOOLEAN): not(TRUE = FALSE) in BOOLEAN, ([not](A), BOOLEAN): [not](A) in BOOLEAN, ([not](_a), BOOLEAN): [not](_a) 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, ([not](FALSE), BOOLEAN): [not](FALSE) in BOOLEAN, (FALSE, BOOLEAN): FALSE in BOOLEAN, (not(TRUE = [not](TRUE)), BOOLEAN): not(TRUE = [not](TRUE)) in BOOLEAN, (TRUE = [not](TRUE), BOOLEAN): (TRUE = [not](TRUE)) in BOOLEAN, (not([not](TRUE) = TRUE), BOOLEAN): not([not](TRUE) = TRUE) in BOOLEAN, ([not](TRUE) = TRUE, BOOLEAN): ([not](TRUE) = TRUE) in BOOLEAN, (not([not](TRUE)), BOOLEAN): not([not](TRUE)) in BOOLEAN, ([not](TRUE), BOOLEAN): [not](TRUE) in BOOLEAN, (0, Rational): 0 in Rational, (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, (0, Real): 0 in Real, (0, Complex): 0 in Complex, (0, Natural): 0 in Natural, (n, Natural): n in Natural, (_a, Natural): _a in Natural, (0, Integer): 0 in Integer, (0, RationalNonNeg): 0 in RationalNonNeg, (q, RationalNonNeg): q in RationalNonNeg, (_a, RationalNonNeg): _a in RationalNonNeg, (0, RealNonNeg): 0 in RealNonNeg, (x, RealNonNeg): x in RealNonNeg, (_a, RealNonNeg): _a in RealNonNeg, (b, Real): b in Real, (a, Real): a in Real, (_b, Real): _b in Real, (_a, Real): _a in Real, (1, Real): 1 in Real, (1, NaturalPos): 1 in NaturalPos, (n, NaturalPos): n in NaturalPos, (_a, NaturalPos): _a in NaturalPos, (1, Natural): 1 in Natural, (1, Integer): 1 in Integer, (1, Rational): 1 in Rational, (1, Complex): 1 in Complex, (1, RationalNonNeg): 1 in RationalNonNeg, (1, RealNonNeg): 1 in RealNonNeg, (1, IntegerNonZero): 1 in IntegerNonZero, (a, IntegerNonZero): a in IntegerNonZero, (_a, IntegerNonZero): _a in IntegerNonZero, (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, (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, (2, Natural): 2 in Natural, (2, Integer): 2 in Integer, (2, Rational): 2 in Rational, (2, Real): 2 in Real, (2, Complex): 2 in Complex, (2, RationalNonNeg): 2 in RationalNonNeg, (2, RealNonNeg): 2 in RealNonNeg, (2, IntegerNonZero): 2 in IntegerNonZero, (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, 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, (3, Natural): 3 in Natural, (3, Integer): 3 in Integer, (3, Rational): 3 in Rational, (3, Real): 3 in Real, (3, Complex): 3 in Complex, (3, RationalNonNeg): 3 in RationalNonNeg, (3, RealNonNeg): 3 in RealNonNeg, (3, IntegerNonZero): 3 in IntegerNonZero, (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, 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, (4, Natural): 4 in Natural, (4, Integer): 4 in Integer, (4, Rational): 4 in Rational, (4, Real): 4 in Real, (4, Complex): 4 in Complex, (4, RationalNonNeg): 4 in RationalNonNeg, (4, RealNonNeg): 4 in RealNonNeg, (4, IntegerNonZero): 4 in IntegerNonZero, (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, 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, (5, Natural): 5 in Natural, (5, Integer): 5 in Integer, (5, Rational): 5 in Rational, (5, Real): 5 in Real, (5, Complex): 5 in Complex, (5, RationalNonNeg): 5 in RationalNonNeg, (5, RealNonNeg): 5 in RealNonNeg, (5, IntegerNonZero): 5 in IntegerNonZero, (not(0 = 5), BOOLEAN): not(0 = 5) 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, 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, (6, Natural): 6 in Natural, (6, Integer): 6 in Integer, (6, Rational): 6 in Rational, (6, Real): 6 in Real, (6, Complex): 6 in Complex, (6, RationalNonNeg): 6 in RationalNonNeg, (6, RealNonNeg): 6 in RealNonNeg, (6, IntegerNonZero): 6 in IntegerNonZero, (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, 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, (7, Natural): 7 in Natural, (7, Integer): 7 in Integer, (7, Rational): 7 in Rational, (7, Real): 7 in Real, (7, Complex): 7 in Complex, (7, RationalNonNeg): 7 in RationalNonNeg, (7, RealNonNeg): 7 in RealNonNeg, (7, IntegerNonZero): 7 in IntegerNonZero, (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, 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, (8, Natural): 8 in Natural, (8, Integer): 8 in Integer, (8, Rational): 8 in Rational, (8, Real): 8 in Real, (8, Complex): 8 in Complex, (8, RationalNonNeg): 8 in RationalNonNeg, (8, RealNonNeg): 8 in RealNonNeg, (8, IntegerNonZero): 8 in IntegerNonZero, (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, 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, (9, Natural): 9 in Natural, (9, Integer): 9 in Integer, (9, Rational): 9 in Rational, (9, Real): 9 in Real, (9, Complex): 9 in Complex, (9, RationalNonNeg): 9 in RationalNonNeg, (9, RealNonNeg): 9 in RealNonNeg, (9, IntegerNonZero): 9 in IntegerNonZero, (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, RationalNonZero): 9 in RationalNonZero, (9, RealNonZero): 9 in RealNonZero, (9, ComplexNonZero): 9 in ComplexNonZero, (9, RationalPos): 9 in RationalPos, (9, RealPos): 9 in RealPos, (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(3 = 2), BOOLEAN): not(3 = 2) in BOOLEAN, (3 = 2, BOOLEAN): (3 = 2) in BOOLEAN, (not(2 = 3), BOOLEAN): not(2 = 3) in BOOLEAN, (2 = 3, BOOLEAN): (2 = 3) in BOOLEAN, (not(4 = 3), BOOLEAN): not(4 = 3) in BOOLEAN, (4 = 3, BOOLEAN): (4 = 3) in BOOLEAN, (not(3 = 4), BOOLEAN): not(3 = 4) in BOOLEAN, (3 = 4, BOOLEAN): (3 = 4) in BOOLEAN, (not(5 = 4), BOOLEAN): not(5 = 4) in BOOLEAN, (5 = 4, BOOLEAN): (5 = 4) in BOOLEAN, (not(4 = 5), BOOLEAN): not(4 = 5) in BOOLEAN, (4 = 5, BOOLEAN): (4 = 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(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(8 = 7), BOOLEAN): not(8 = 7) in BOOLEAN, (8 = 7, BOOLEAN): (8 = 7) in BOOLEAN, (not(7 = 8), BOOLEAN): not(7 = 8) in BOOLEAN, (7 = 8, BOOLEAN): (7 = 8) in BOOLEAN, (not(9 = 8), BOOLEAN): not(9 = 8) in BOOLEAN, (9 = 8, BOOLEAN): (9 = 8) in BOOLEAN, (not(8 = 9), BOOLEAN): not(8 = 9) in BOOLEAN, (8 = 9, BOOLEAN): (8 = 9) in BOOLEAN, (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, (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, (i, Complex): i in Complex, (i, ComplexNonZero): i in ComplexNonZero, (not(0 = i), BOOLEAN): not(0 = i) in BOOLEAN, (0 = i, BOOLEAN): (0 = i) in BOOLEAN, (not(i = 0), BOOLEAN): not(i = 0) in BOOLEAN, (i = 0, BOOLEAN): (i = 0) in BOOLEAN}
known_memberships = {TRUE: {|- TRUE in BOOLEAN}, not(TRUE = FALSE): {|- not(TRUE = FALSE) in BOOLEAN}, TRUE = FALSE: {|- (TRUE = FALSE) in BOOLEAN}, not(FALSE = TRUE): {|- not(FALSE = TRUE) in BOOLEAN}, FALSE = TRUE: {|- (FALSE = TRUE) in BOOLEAN}, [not](FALSE): {|- [not](FALSE) in BOOLEAN}, FALSE: {|- FALSE in BOOLEAN}, not(TRUE = [not](TRUE)): {|- not(TRUE = [not](TRUE)) in BOOLEAN}, TRUE = [not](TRUE): {|- (TRUE = [not](TRUE)) in BOOLEAN}, not([not](TRUE) = TRUE): {|- not([not](TRUE) = TRUE) in BOOLEAN}, [not](TRUE) = TRUE: {|- ([not](TRUE) = TRUE) in BOOLEAN}, not([not](TRUE)): {|- not([not](TRUE)) in BOOLEAN}, [not](TRUE): {|- [not](TRUE) in BOOLEAN}, 0: {|- 0 in Real, |- 0 in Complex, |- 0 in Integer, |- 0 in Natural, |- 0 in RealNonNeg, |- 0 in RationalNonNeg, |- 0 in Rational}, 1: {|- 1 in Real, |- 1 in IntegerNonZero, |- 1 in Complex, |- 1 in Rational, |- 1 in RealNonNeg, |- 1 in RationalPos, |- 1 in RationalNonZero, |- 1 in ComplexNonZero, |- 1 in RealPos, |- 1 in RationalNonNeg, |- 1 in Natural, |- 1 in Integer, |- 1 in NaturalPos, |- 1 in RealNonZero}, not(0 = 1): {|- not(0 = 1) in BOOLEAN}, 0 = 1: {|- (0 = 1) in BOOLEAN}, not(1 = 0): {|- not(1 = 0) in BOOLEAN}, 1 = 0: {|- (1 = 0) in BOOLEAN}, 2: {|- 2 in RationalNonNeg, |- 2 in ComplexNonZero, |- 2 in Integer, |- 2 in Rational, |- 2 in Real, |- 2 in NaturalPos, |- 2 in IntegerNonZero, |- 2 in Natural, |- 2 in RealNonZero, |- 2 in RationalPos, |- 2 in Complex, |- 2 in RationalNonZero, |- 2 in RealNonNeg, |- 2 in RealPos}, not(0 = 2): {|- not(0 = 2) in BOOLEAN}, 0 = 2: {|- (0 = 2) in BOOLEAN}, not(2 = 0): {|- not(2 = 0) in BOOLEAN}, 2 = 0: {|- (2 = 0) in BOOLEAN}, 3: {|- 3 in ComplexNonZero, |- 3 in RealNonZero, |- 3 in Complex, |- 3 in Real, |- 3 in Integer, |- 3 in RationalNonNeg, |- 3 in RealNonNeg, |- 3 in RationalPos, |- 3 in RationalNonZero, |- 3 in RealPos, |- 3 in IntegerNonZero, |- 3 in Rational, |- 3 in NaturalPos, |- 3 in Natural}, not(0 = 3): {|- not(0 = 3) in BOOLEAN}, 0 = 3: {|- (0 = 3) in BOOLEAN}, not(3 = 0): {|- not(3 = 0) in BOOLEAN}, 3 = 0: {|- (3 = 0) in BOOLEAN}, 4: {|- 4 in Real, |- 4 in Integer, |- 4 in RealNonNeg, |- 4 in RationalPos, |- 4 in ComplexNonZero, |- 4 in NaturalPos, |- 4 in IntegerNonZero, |- 4 in RationalNonZero, |- 4 in Complex, |- 4 in Natural, |- 4 in RealNonZero, |- 4 in Rational, |- 4 in RealPos, |- 4 in RationalNonNeg}, not(0 = 4): {|- not(0 = 4) in BOOLEAN}, 0 = 4: {|- (0 = 4) in BOOLEAN}, not(4 = 0): {|- not(4 = 0) in BOOLEAN}, 4 = 0: {|- (4 = 0) in BOOLEAN}, 5: {|- 5 in RealNonZero, |- 5 in Rational, |- 5 in RealNonNeg, |- 5 in IntegerNonZero, |- 5 in Natural, |- 5 in Real, |- 5 in NaturalPos, |- 5 in ComplexNonZero, |- 5 in RationalNonNeg, |- 5 in RealPos, |- 5 in Complex, |- 5 in RationalPos, |- 5 in RationalNonZero, |- 5 in Integer}, not(0 = 5): {|- not(0 = 5) in BOOLEAN}, 0 = 5: {|- (0 = 5) in BOOLEAN}, not(5 = 0): {|- not(5 = 0) in BOOLEAN}, 5 = 0: {|- (5 = 0) in BOOLEAN}, 6: {|- 6 in NaturalPos, |- 6 in RealNonNeg, |- 6 in RationalNonNeg, |- 6 in IntegerNonZero, |- 6 in Complex, |- 6 in RealNonZero, |- 6 in RealPos, |- 6 in Integer, |- 6 in RationalPos, |- 6 in ComplexNonZero, |- 6 in Natural, |- 6 in RationalNonZero, |- 6 in Rational, |- 6 in Real}, not(0 = 6): {|- not(0 = 6) in BOOLEAN}, 0 = 6: {|- (0 = 6) in BOOLEAN}, not(6 = 0): {|- not(6 = 0) in BOOLEAN}, 6 = 0: {|- (6 = 0) in BOOLEAN}, 7: {|- 7 in RealPos, |- 7 in RealNonNeg, |- 7 in Complex, |- 7 in Rational, |- 7 in Integer, |- 7 in RationalPos, |- 7 in Real, |- 7 in NaturalPos, |- 7 in RealNonZero, |- 7 in ComplexNonZero, |- 7 in RationalNonNeg, |- 7 in RationalNonZero, |- 7 in IntegerNonZero, |- 7 in Natural}, not(0 = 7): {|- not(0 = 7) in BOOLEAN}, 0 = 7: {|- (0 = 7) in BOOLEAN}, not(7 = 0): {|- not(7 = 0) in BOOLEAN}, 7 = 0: {|- (7 = 0) in BOOLEAN}, 8: {|- 8 in Natural, |- 8 in ComplexNonZero, |- 8 in RealPos, |- 8 in RationalNonNeg, |- 8 in Integer, |- 8 in RationalNonZero, |- 8 in Rational, |- 8 in RationalPos, |- 8 in RealNonZero, |- 8 in Real, |- 8 in RealNonNeg, |- 8 in Complex, |- 8 in IntegerNonZero, |- 8 in NaturalPos}, not(0 = 8): {|- not(0 = 8) in BOOLEAN}, 0 = 8: {|- (0 = 8) in BOOLEAN}, not(8 = 0): {|- not(8 = 0) in BOOLEAN}, 8 = 0: {|- (8 = 0) in BOOLEAN}, 9: {|- 9 in Rational, |- 9 in RationalNonZero, |- 9 in RationalPos, |- 9 in Real, |- 9 in RealPos, |- 9 in NaturalPos, |- 9 in Integer, |- 9 in IntegerNonZero, |- 9 in ComplexNonZero, |- 9 in RationalNonNeg, |- 9 in Natural, |- 9 in RealNonNeg, |- 9 in Complex, |- 9 in RealNonZero}, not(0 = 9): {|- not(0 = 9) in BOOLEAN}, 0 = 9: {|- (0 = 9) in BOOLEAN}, not(9 = 0): {|- not(9 = 0) in BOOLEAN}, 9 = 0: {|- (9 = 0) in BOOLEAN}, not(2 = 1): {|- not(2 = 1) in BOOLEAN}, 2 = 1: {|- (2 = 1) in BOOLEAN}, not(1 = 2): {|- not(1 = 2) in BOOLEAN}, 1 = 2: {|- (1 = 2) in BOOLEAN}, not(3 = 2): {|- not(3 = 2) in BOOLEAN}, 3 = 2: {|- (3 = 2) in BOOLEAN}, not(2 = 3): {|- not(2 = 3) in BOOLEAN}, 2 = 3: {|- (2 = 3) in BOOLEAN}, not(4 = 3): {|- not(4 = 3) in BOOLEAN}, 4 = 3: {|- (4 = 3) in BOOLEAN}, not(3 = 4): {|- not(3 = 4) in BOOLEAN}, 3 = 4: {|- (3 = 4) in BOOLEAN}, not(5 = 4): {|- not(5 = 4) in BOOLEAN}, 5 = 4: {|- (5 = 4) in BOOLEAN}, not(4 = 5): {|- not(4 = 5) in BOOLEAN}, 4 = 5: {|- (4 = 5) in BOOLEAN}, not(6 = 5): {|- not(6 = 5) in BOOLEAN}, 6 = 5: {|- (6 = 5) in BOOLEAN}, not(5 = 6): {|- not(5 = 6) in BOOLEAN}, 5 = 6: {|- (5 = 6) in BOOLEAN}, not(7 = 6): {|- not(7 = 6) in BOOLEAN}, 7 = 6: {|- (7 = 6) in BOOLEAN}, not(6 = 7): {|- not(6 = 7) in BOOLEAN}, 6 = 7: {|- (6 = 7) in BOOLEAN}, not(8 = 7): {|- not(8 = 7) in BOOLEAN}, 8 = 7: {|- (8 = 7) in BOOLEAN}, not(7 = 8): {|- not(7 = 8) in BOOLEAN}, 7 = 8: {|- (7 = 8) in BOOLEAN}, not(9 = 8): {|- not(9 = 8) in BOOLEAN}, 9 = 8: {|- (9 = 8) in BOOLEAN}, not(8 = 9): {|- not(8 = 9) in BOOLEAN}, 8 = 9: {|- (8 = 9) in BOOLEAN}, e: {|- e in RealPos, |- e in Complex, |- e in Real, |- e in RealNonZero, |- e in RealNonNeg, |- e in ComplexNonZero}, not(0 = e): {|- not(0 = e) in BOOLEAN}, 0 = e: {|- (0 = e) in BOOLEAN}, not(e = 0): {|- not(e = 0) in BOOLEAN}, e = 0: {|- (e = 0) in BOOLEAN}, pi: {|- pi in RealNonZero, |- pi in Complex, |- pi in RealPos, |- pi in ComplexNonZero, |- pi in RealNonNeg, |- pi in Real}, not(0 = pi): {|- not(0 = pi) in BOOLEAN}, 0 = pi: {|- (0 = pi) in BOOLEAN}, not(pi = 0): {|- not(pi = 0) in BOOLEAN}, pi = 0: {|- (pi = 0) in BOOLEAN}, i: {|- i in ComplexNonZero, |- i in Complex}, not(0 = i): {|- not(0 = i) in BOOLEAN}, 0 = i: {|- (0 = i) in BOOLEAN}, not(i = 0): {|- not(i = 0) in BOOLEAN}, i = 0: {|- (i = 0) in BOOLEAN}}

Methods Documentation

conclude(self, \*\*defaults_config)[source]

Attempt to conclude that the element is in the domain. First, see if it is known to be contained in a known subset of the domain. Next, check if the element has a known simplification; if so, try to derive membership via this simplification. If there isn’t a known simplification, next try to call the ‘self.domain.membership_object.conclude(..)’ method to prove the membership. If that fails, try simplifying the element again, this time using automation to push the simplification through if possible.

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

deduce_not_in(self, \*\*defaults_config)[source]

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

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

negation_side_effects(self, judgment)[source]

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

static reversed_operator_str(formatType)[source]

Reversing in gives

  1. Reversing “in” gives “contains”.

shallow_simplification(self, \*, must_evaluate=False, \*\*defaults_config)[source]

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(expr, \*args, \*\*kwargs)

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

side_effects(self, judgment)[source]

Store the proven membership in known_memberships. 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, assumptions=None)[source]

Yield the known memberships of the given element applicable under the given assumptions.