NotInSet

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

Bases: proveit.logic.NotInClass

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

Attributes Summary

Methods Summary

conclude(self, \*\*defaults_config)	Attempt to conclude that the element is not in the domain.
conclude_as_folded(self, \*\*defaults_config)	Attempt to conclude x not in S via Not(x in S).
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.
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). For example, NotInSet(a, {b, c, d}).unfold_not_in( assumptions=[NotInSet(a, {b, c, d})]) and NotInSet(a, {b, c, d}).unfold_not_in( assumptions=[NotEquals(a, b), NotEquals(a, c), NotEquals(a, d)]) both return NotInSet(a, {b, c, d}) |- Not (a in {b, c, d}), We include the auto_simplify=False to keep the membership result inside the Not() from being reduced to False.

Attributes Documentation

Methods Documentation

conclude(self, \*\*defaults_config)

Attempt to conclude that the element is not in the domain. First see if the corresponding membership has been disproven. Then see if there is a as-strong known nonmembership to use. If not, use the NotInClass conclude strategies (which uses the Relation conclude strategies that simplify both sides and then uses the domain-specific conclude method of the membership 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 S via Not(x in S).

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.

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). For example, NotInSet(a, {b, c, d}).unfold_not_in(

assumptions=[NotInSet(a, {b, c, d})])

and NotInSet(a, {b, c, d}).unfold_not_in(

assumptions=[NotEquals(a, b), NotEquals(a, c),

NotEquals(a, d)])

both return NotInSet(a, {b, c, d}) |- Not (a in {b, c, d}), We include the auto_simplify=False to keep the membership result inside the Not() from being reduced to False.

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