NotEquals

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

Bases: proveit.relation.relation.Relation

Methods Summary

affirm_via_contradiction(self, conclusion, …)	From x != y, derive the conclusion provided that the negated conclusion implies x != y and x = y, and the conclusion is a Boolean.
conclude(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
conclude_as_folded(self, \*\*defaults_config)	Conclude (x != y) from Not(x = y).
conclude_via_double_negation(self, …)	Prove and return self of the form A != FALSE or FALSE != A assuming A or A != TRUE or TRUE != A assuming not A.
deduce_in_bool(self, \*\*defaults_config)	Deduce and return that this ‘not equals’ statement is in the set of BOOLEANS.
definition(self, \*\*defaults_config)	Return (x != y) = Not(x=y) where self represents (x != y).
deny_via_contradiction(self, conclusion, …)	From x != y, derive the negated conclusion provided that the conclusion implies x != y and x = y, and the conclusion is a Boolean.
derive_contradiction(self, \*\*defaults_config)	From x != y, and assuming x = y, derive and return FALSE.
derive_reversed(self, \*\*defaults_config)	From x != y derive y != x.
derive_via_double_negation(self, …)	From A != FALSE, derive and return A assuming in_bool(A).
evaluation(self, \*\*defaults_config)	If possible, return a Judgment of this expression equal to an irreducible value.
reversed(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘symmetrization’.
side_effects(self, judgment)	Side-effect derivations to attempt automatically for this NotEquals operation.
unfold(self, \*\*defaults_config)	From (x != y), derive and return Not(x=y).

Methods Documentation

affirm_via_contradiction(self, conclusion, \*\*defaults_config)

From x != y, derive the conclusion provided that the negated conclusion implies x != y and x = y, and the conclusion is a Boolean.

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

conclude(self, \*\*defaults_config)

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

conclude_as_folded(self, \*\*defaults_config)

Conclude (x != y) from Not(x = y).

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

conclude_via_double_negation(self, \*\*defaults_config)

Prove and return self of the form A != FALSE or FALSE != A assuming A or A != TRUE or TRUE != A assuming not A. Also see version in Not class.

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 equals’ 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 (x != y) = Not(x=y) where self represents (x != y).

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.

deny_via_contradiction(self, conclusion, \*\*defaults_config)

From x != y, derive the negated conclusion provided that the conclusion implies x != y and x = y, and the conclusion is a Boolean.

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

derive_contradiction(self, \*\*defaults_config)

From x != y, and assuming x = y, derive and return FALSE.

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

derive_reversed(self, \*\*defaults_config)

From x != y derive y != x.

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

derive_via_double_negation(self, \*\*defaults_config)

From A != FALSE, derive and return A assuming in_bool(A). Also see version in Not class.

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

evaluation(self, \*\*defaults_config)

If possible, return a Judgment of this expression equal to an irreducible value. This Operation.evaluation version simplifies the operands and then calls shallow_simplification with must_evaluat=True.

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

‘evaluated’ returns the right-hand side of ‘evaluation’. ‘evaluate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘evaluation’ for the inner expression.

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

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

side_effects(self, judgment)

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

unfold(self, \*\*defaults_config)

From (x != y), derive and return Not(x=y).

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