NotInClass

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

Bases: proveit.relation.relation.Relation

NotInClass denotes the logical negation of class membership (see InClass).

Attributes Summary

notinclass_expressions

Methods Summary

conclude(self, \*\*defaults_config)	Attempt to conclude that the the NotInSet object is true — i.e. that the element is not in the domain.
conclude_as_folded(self, \*\*defaults_config)	Attempt to conclude x not in C via Not(x in C).
deduce_in_bool(self, \*\*defaults_config)	Deduce and return that this ‘not in’ statement is in the set of BOOLEANS. For example, NotInSet(x, {1, 2, 3}).deduce_in_bool() returns |- NotInSet(x, {1, 2, 3}) in Bool.
negated(self)	Return the membership expression (double negative), element in domain.
shallow_simplification(self, \*[, must_evaluate])	Attempt to evaluate whether some x ∉ S is TRUE or FALSE using the ‘definition’ method of the domain’s ‘nonmembership_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)	Unfold x not-in S as Not(x in S) as an automatic side-effect.
unfold_not_in(self, \*\*defaults_config)	From (x notin y), derive and return Not(x in y).

Attributes Documentation

notinclass_expressions = {}

Methods Documentation

conclude(self, \*\*defaults_config)

Attempt to conclude that the the NotInSet object is true — i.e. that the element is not in the domain. First see if the corresponding membership has been disproven. Then try the ses the Relation conclude strategies that simplify both sides. Finally use the domain-specific conclude method of the nonmembership object as a last resort.

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

conclude_as_folded(self, \*\*defaults_config)

Attempt to conclude x not in C via Not(x in C).

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

deduce_in_bool(self, \*\*defaults_config)

Deduce and return that this ‘not in’ statement is in the set of BOOLEANS. For example, NotInSet(x, {1, 2, 3}).deduce_in_bool() returns |- NotInSet(x, {1, 2, 3}) in Bool

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

negated(self)

Return the membership expression (double negative), element in domain.

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 ‘nonmembership_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)

Unfold x not-in S as Not(x in S) as an automatic side-effect. If the domain has a ‘nonmembership_object’ method, side effects will also be generated from the ‘side_effects’ object that it generates.

unfold_not_in(self, \*\*defaults_config)

From (x notin y), derive and return Not(x in y).

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