InSet¶

class
proveit.logic.
InSet
(element, domain, *, styles=None)[source]¶ Bases:
proveit.relation.relation.Relation
Attributes Summary
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 notin S) as an automatic sideeffect.
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 notin S) as an automatic sideeffect.

static
reversed_operator_str
(formatType)[source]¶ Reversing in gives
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’.
