SetNotEquiv

class proveit.logic.SetNotEquiv(a, b, *, styles=None)

Bases: proveit.Operation

Class to capture the LACK of membership equivalence of 2 sets A and B. SetNotEquiv(A, B) is a claim that at least one element of set A does not also appear in set B, and/or vice versa. Like the SetEquiv class, the SetNotEquiv relation uses the (negated) congruence symbol to distinguish the SetNotEquiv claims from the distinctive claim that A ≠ B. The class was initially established using the class NotEquals as an archetype.

Methods Summary

conclude_as_folded(self, \*\*defaults_config)	Conclude (A not_equiv B) from Not(A equiv B).
deduce_in_bool(self, \*\*defaults_config)	Deduce and return that this ‘not equiv’ statement is in the set of BOOLEANS.
definition(self, \*\*defaults_config)	Return (A not_equiv B) = Not(A equiv B) where self represents (A not_equiv B).
derive_contradiction(self, \*\*defaults_config)	From A not_equiv B, and assuming (A equiv B), derive and return FALSE.
derive_reversed(self, \*\*defaults_config)	From A not_equiv B derive B not_equiv A.
side_effects(self, judgment)	Side-effect derivations to attempt automatically for this SetNotEquiv operation.
unfold(self, \*\*defaults_config)	From (A not_equiv B) derive and return Not(A equiv B).

Methods Documentation

conclude_as_folded(self, \*\*defaults_config)

Conclude (A not_equiv B) from Not(A equiv B).

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 equiv’ statement is in the set of BOOLEANS.

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

definition(self, \*\*defaults_config)

Return (A not_equiv B) = Not(A equiv B) where self represents (A not_equiv B).

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

‘defined’ returns the right-hand side of ‘definition’. ‘define’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘definition’ for the inner expression.

derive_contradiction(self, \*\*defaults_config)

From A not_equiv B, and assuming (A equiv B), derive and return FALSE.

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

derive_reversed(self, \*\*defaults_config)

From A not_equiv B derive B not_equiv A. Derived automatically as a side-effect in side_effects() method.

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

side_effects(self, judgment)

Side-effect derivations to attempt automatically for this SetNotEquiv operation.

unfold(self, \*\*defaults_config)

From (A not_equiv B) derive and return Not(A equiv B).

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