Equals

class proveit.logic.Equals(a, b, *, styles=None)[source]

Bases: proveit.TransitiveRelation

Attributes Summary

initializing

inversions

known_equalities

known_evaluation_sets

known_simplifications

Methods Summary

StrongRelationClass()

WeakRelationClass()

affirm_via_contradiction(self, conclusion, …)

From (A=FALSE), derive the conclusion provided that the negated conclusion implies both (A=FALSE) as well as A, and the conclusion is a Boolean.

apply_transitivity(self, other, …)

From x = y (self) and y = z (other) derive and return x = z.

conclude(self, \*\*defaults_config)

Attempt to conclude the equality various ways: simple reflexivity (x=x), via an evaluation (if one side is an irreducible).

conclude_boolean_equality(self, …)

Prove and return self of the form

conclude_via_reflexivity(self, …)

Prove and return self of the form x = x.

deduce_in_bool(self, \*\*defaults_config)

Deduce and return that this equality statement is in the Boolean set.

deduce_not_equals(self, \*\*defaults_config)

Deduce x != y assuming not(x = y), where self is x=y.

deny_via_contradiction(self, conclusion, …)

From (A=FALSE), derive the negated conclusion provided that the conclusion implies both (A=FALSE) as well as A, and the conclusion is a Boolean.

derive_contradiction(self, \*\*defaults_config)

From A=FALSE, and assuming A, derive FALSE.

derive_is_in_singleton(self, \*\*defaults_config)

From (x = y), derive (x in {y}).

derive_left_via_equality(self, …)

From A = B, derive A (the Right-Hand-Side) assuming B.

derive_reversed(self, \*\*defaults_config)

From x = y derive y = x.

derive_right_via_equality(self, …)

From A = B, derive B (the Right-Hand-Side) assuming A.

derive_via_boolean_equality(self, …)

From A = TRUE derive A, or from A = FALSE derive Not(A).

evaluation(self, \*\*defaults_config)

If possible, return a Judgment of this expression equal to an irreducible value.

invert(lambda_map, rhs[, assumptions])

Given some x -> f(x) map and a right-hand-side, find the x for which f(x) = rhs amongst known equalities under the given assumptions.

known_relations_from_left(expr, assumptions_set)

For each Judgment that is an Equals involving the given expression on the left hand side, yield the Judgment and the right hand side.

known_relations_from_right(expr, assumptions_set)

For each Judgment that is an Equals involving the given expression on the right hand side, yield the Judgment and the left hand side.

negation_side_effects(self, judgment)

Side-effect derivations to attempt automatically for a negated equation.

other_side(self, expr)

Returns the ‘other’ side of the of the equation if the given expr is on one side.

reversed(self)

Return an Equals expression with the right side and left side reversed from this one.

side_effects(self, judgment)

Record the judgment in Equals.known_equalities, associated from the left hand side and the right hand side.

sub_left_side_into(self, lambda_map, …)

From x = y, and given P(y), derive P(x) assuming P(y).

sub_right_side_into(self, lambda_map, …)

From x = y, and given P(x), derive P(y) assuming P(x).

substitution(self, lambda_map, …)

From x = y, and given f(x), derive f(x)=f(y).

Attributes Documentation

initializing = {}
inversions = {}
known_equalities = {[not](FALSE): {|- TRUE = [not](FALSE), |- [not](FALSE) = TRUE}, TRUE: {|- TRUE = TRUE, |- TRUE = [not](FALSE), |- [not](FALSE) = TRUE}, BOOLEAN: {|- BOOLEAN = {TRUE, FALSE}, |- BOOLEAN = BOOLEAN, |- {TRUE, FALSE} = BOOLEAN}, TRUE = FALSE: {|- (TRUE = FALSE) = FALSE, |- FALSE = (TRUE = FALSE)}, FALSE: {|- (3 <= 2) = FALSE, |- (TRUE = (7 <= 0)) = FALSE, |- FALSE = (TRUE = (pi < 0)), |- (TRUE = (5 <= 0)) = FALSE, |- FALSE = (0 = 5), |- (9 = 0) = FALSE, |- (TRUE = (9 <= 8)) = FALSE, |- FALSE = (TRUE = (e < 0)), |- (TRUE = (6 < 0)) = FALSE, |- FALSE = ((5 < 0) = TRUE), |- (TRUE = (9 <= 0)) = FALSE, |- FALSE = (1 = 2), |- (1 <= 0) = FALSE, |- FALSE = ((6 <= 5) = TRUE), |- FALSE = ((5 <= 4) = TRUE), |- (TRUE = (5 < 0)) = FALSE, |- (2 < 0) = FALSE, |- ((2 < 1) = TRUE) = FALSE, |- (TRUE = FALSE) = FALSE, |- FALSE = (pi = 0), |- (TRUE = (pi < 0)) = FALSE, |- ((3 < 2) = TRUE) = FALSE, |- (0 < 0) = FALSE, |- FALSE = (1 = 0), |- FALSE = (TRUE = (4 <= 0)), |- FALSE = (6 <= 0), |- FALSE = ((1 <= 0) = TRUE), |- FALSE = ((7 < 6) = TRUE), |- ((2 <= 0) = TRUE) = FALSE, |- FALSE = (7 <= 0), |- FALSE = (3 = 4), |- (7 <= 6) = FALSE, |- (4 < 0) = FALSE, |- (pi < 0) = FALSE, |- FALSE = ((6 < 5) = TRUE), |- FALSE = (TRUE = (2 <= 1)), |- FALSE = (6 = 7), |- FALSE = (7 < 1), |- (5 < 4) = FALSE, |- ((3 <= 2) = TRUE) = FALSE, |- (TRUE = (2 < 1)) = FALSE, |- FALSE = ((8 < 0) = TRUE), |- (3 < 2) = FALSE, |- (TRUE = (9 < 8)) = FALSE, |- ((6 < 1) = TRUE) = FALSE, |- FALSE = (0 = 6), |- (3 <= 0) = FALSE, |- (7 <= 0) = FALSE, |- (TRUE = (6 <= 0)) = FALSE, |- FALSE = (e <= 0), |- FALSE = (TRUE = (3 < 0)), |- (0 = 5) = FALSE, |- FALSE = (TRUE = (1 <= 0)), |- FALSE = ((2 <= 1) = TRUE), |- FALSE = (TRUE = FALSE), |- FALSE = (TRUE = (9 <= 0)), |- FALSE = ((4 < 3) = TRUE), |- FALSE = (6 < 5), |- FALSE = (3 < 0), |- (4 < 3) = FALSE, |- FALSE = (4 < 1), |- (TRUE = (9 < 0)) = FALSE, |- (5 = 4) = FALSE, |- FALSE = ((6 < 1) = TRUE), |- FALSE = (TRUE = (5 <= 4)), |- FALSE = (7 = 6), |- FALSE = ((5 < 1) = TRUE), |- FALSE = (7 = 0), |- (4 < 1) = FALSE, |- FALSE = (TRUE = (8 < 0)), |- FALSE = (TRUE = (4 < 0)), |- (TRUE = (8 < 0)) = FALSE, |- FALSE = ((7 < 0) = TRUE), |- FALSE = (8 = 7), |- FALSE = (2 <= 0), |- (3 < 0) = FALSE, |- (2 < 1) = FALSE, |- FALSE = (TRUE = (8 <= 7)), |- FALSE = (0 = 8), |- (8 < 1) = FALSE, |- (5 <= 0) = FALSE, |- FALSE = (TRUE = (5 < 0)), |- ((6 <= 0) = TRUE) = FALSE, |- FALSE = ((7 <= 0) = TRUE), |- FALSE = (3 <= 2), |- FALSE = ((6 <= 0) = TRUE), |- FALSE = (5 = 0), |- FALSE = (8 < 7), |- (2 = 0) = FALSE, |- FALSE = (TRUE = (7 <= 0)), |- FALSE = (TRUE = (6 <= 0)), |- ((4 <= 3) = TRUE) = FALSE, |- FALSE = (6 < 1), |- FALSE = (0 = 1), |- (4 = 5) = FALSE, |- (TRUE = (2 < 0)) = FALSE, |- FALSE = ((4 < 1) = TRUE), |- FALSE = (4 = 3), |- FALSE = (TRUE = (9 < 0)), |- FALSE = (TRUE = (e <= 0)), |- ((7 <= 0) = TRUE) = FALSE, |- (i = 0) = FALSE, |- FALSE = (TRUE = (6 <= 5)), |- (4 = 3) = FALSE, |- FALSE = (8 = 9), |- (TRUE = (5 < 4)) = FALSE, |- FALSE = ((1 < 0) = TRUE), |- FALSE = (6 = 5), |- ((8 < 7) = TRUE) = FALSE, |- FALSE = (TRUE = (7 < 0)), |- FALSE = ((7 < 1) = TRUE), |- FALSE = (7 <= 6), |- FALSE = ((5 < 4) = TRUE), |- FALSE = ((0 < 0) = TRUE), |- FALSE = (2 = 3), |- (5 = 6) = FALSE, |- ((pi < 0) = TRUE) = FALSE, |- FALSE = ((pi < 0) = TRUE), |- (8 < 7) = FALSE, |- (0 = pi) = FALSE, |- (TRUE = (4 <= 0)) = FALSE, |- ((4 < 1) = TRUE) = FALSE, |- (6 = 5) = FALSE, |- (TRUE = (e < 0)) = FALSE, |- (9 <= 0) = FALSE, |- ((0 < 0) = TRUE) = FALSE, |- (TRUE = (8 < 7)) = FALSE, |- FALSE = (TRUE = (3 <= 0)), |- FALSE = (2 <= 1), |- ((e < 0) = TRUE) = FALSE, |- (e < 0) = FALSE, |- (0 = 2) = FALSE, |- (pi = 0) = FALSE, |- FALSE = (8 = 0), |- FALSE = (2 < 1), |- FALSE = (TRUE = (1 < 0)), |- (7 = 0) = FALSE, |- (1 = 2) = FALSE, |- (5 < 0) = FALSE, |- (TRUE = (4 < 0)) = FALSE, |- (TRUE = (2 <= 0)) = FALSE, |- (2 <= 0) = FALSE, |- FALSE = (TRUE = (4 < 1)), |- FALSE = (TRUE = (3 <= 2)), |- (6 = 7) = FALSE, |- ((9 < 0) = TRUE) = FALSE, |- ((8 < 1) = TRUE) = FALSE, |- (4 <= 0) = FALSE, |- ((4 < 0) = TRUE) = FALSE, |- ((9 < 8) = TRUE) = FALSE, |- (TRUE = (e <= 0)) = FALSE, |- FALSE = (3 < 1), |- FALSE = (TRUE = (2 < 0)), |- (3 = 4) = FALSE, |- FALSE = (TRUE = (7 < 1)), |- FALSE = (5 <= 0), |- FALSE = (9 < 0), |- FALSE = (TRUE = (9 < 1)), |- FALSE = (8 < 0), |- FALSE = ([not](TRUE) = TRUE), |- FALSE = (e = 0), |- FALSE = ((pi <= 0) = TRUE), |- FALSE = (4 <= 0), |- FALSE = ((2 < 1) = TRUE), |- FALSE = ((e < 0) = TRUE), |- FALSE = ((8 <= 7) = TRUE), |- ((7 <= 6) = TRUE) = FALSE, |- FALSE = (9 <= 8), |- ((5 < 4) = TRUE) = FALSE, |- (TRUE = (7 < 1)) = FALSE, |- (8 = 0) = FALSE, |- FALSE = (0 = e), |- (6 <= 5) = FALSE, |- ((5 < 1) = TRUE) = FALSE, |- (5 < 1) = FALSE, |- FALSE = ((8 <= 0) = TRUE), |- FALSE = (TRUE = (7 <= 6)), |- (2 <= 1) = FALSE, |- FALSE = ((4 <= 3) = TRUE), |- ((6 <= 5) = TRUE) = FALSE, |- FALSE = (TRUE = [not](TRUE)), |- (TRUE = (3 < 2)) = FALSE, |- FALSE = (TRUE = (6 < 5)), |- (5 = 0) = FALSE, |- FALSE = (5 <= 4), |- FALSE = (7 < 6), |- (8 = 7) = FALSE, |- FALSE = (0 < 0), |- (TRUE = (5 <= 4)) = FALSE, |- FALSE = (5 < 1), |- FALSE = (TRUE = (2 <= 0)), |- (3 < 1) = FALSE, |- (7 < 6) = FALSE, |- FALSE = (TRUE = (8 <= 0)), |- FALSE = FALSE, |- (TRUE = (8 <= 0)) = FALSE, |- ((8 <= 0) = TRUE) = FALSE, |- (TRUE = (5 < 1)) = FALSE, |- ((pi <= 0) = TRUE) = FALSE, |- (TRUE = (1 <= 0)) = FALSE, |- FALSE = ((4 < 0) = TRUE), |- (TRUE = (3 <= 0)) = FALSE, |- FALSE = ((9 <= 0) = TRUE), |- (TRUE = [not](TRUE)) = FALSE, |- (1 < 0) = FALSE, |- (TRUE = (7 < 6)) = FALSE, |- FALSE = (TRUE = (4 < 3)), |- FALSE = ((3 < 2) = TRUE), |- FALSE = (5 = 6), |- ((e <= 0) = TRUE) = FALSE, |- FALSE = ((9 < 0) = TRUE), |- FALSE = ((3 < 1) = TRUE), |- (9 < 0) = FALSE, |- FALSE = (3 = 0), |- (6 < 1) = FALSE, |- ((3 < 1) = TRUE) = FALSE, |- FALSE = ((8 < 7) = TRUE), |- FALSE = (TRUE = (0 < 0)), |- (0 = 6) = FALSE, |- FALSE = (9 < 1), |- FALSE = (0 = 4), |- FALSE = (TRUE = (4 <= 3)), |- ((5 <= 4) = TRUE) = FALSE, |- (FALSE = TRUE) = FALSE, |- FALSE = ((3 <= 0) = TRUE), |- (TRUE = (6 < 5)) = FALSE, |- FALSE = (TRUE = (3 < 2)), |- ((9 <= 0) = TRUE) = FALSE, |- (8 <= 7) = FALSE, |- (9 < 8) = FALSE, |- FALSE = (0 = 7), |- FALSE = (5 = 4), |- (0 = i) = FALSE, |- (6 <= 0) = FALSE, |- FALSE = ((9 <= 8) = TRUE), |- FALSE = ((2 < 0) = TRUE), |- FALSE = (4 <= 3), |- FALSE = (TRUE = (9 <= 8)), |- ((5 < 0) = TRUE) = FALSE, |- (TRUE = (3 < 1)) = FALSE, |- (TRUE = (pi <= 0)) = FALSE, |- (6 = 0) = FALSE, |- (6 < 0) = FALSE, |- FALSE = (0 = 2), |- (TRUE = (0 < 0)) = FALSE, |- FALSE = (9 = 0), |- FALSE = (9 = 8), |- FALSE = ((3 < 0) = TRUE), |- (2 = 1) = FALSE, |- (TRUE = (6 <= 5)) = FALSE, |- (TRUE = (8 <= 7)) = FALSE, |- (TRUE = (4 <= 3)) = FALSE, |- FALSE = (8 <= 7), |- FALSE = (4 = 0), |- FALSE = (5 < 4), |- FALSE = (pi <= 0), |- FALSE = (1 <= 0), |- (e <= 0) = FALSE, |- (TRUE = (7 <= 6)) = FALSE, |- FALSE = (9 <= 0), |- FALSE = ((9 < 1) = TRUE), |- FALSE = (3 < 2), |- FALSE = (5 < 0), |- FALSE = (TRUE = (5 < 4)), |- FALSE = (0 = 3), |- (4 <= 3) = FALSE, |- FALSE = (pi < 0), |- (9 < 1) = FALSE, |- FALSE = (8 < 1), |- FALSE = (TRUE = (8 < 1)), |- FALSE = (7 < 0), |- (0 = 9) = FALSE, |- ((3 < 0) = TRUE) = FALSE, |- (0 = 1) = FALSE, |- FALSE = (6 < 0), |- ((6 < 5) = TRUE) = FALSE, |- (TRUE = (8 < 1)) = FALSE, |- (3 = 0) = FALSE, |- (TRUE = (1 < 0)) = FALSE, |- (7 = 8) = FALSE, |- FALSE = ((2 <= 0) = TRUE), |- FALSE = (2 < 0), |- FALSE = ((8 < 1) = TRUE), |- ((7 < 6) = TRUE) = FALSE, |- (7 = 6) = FALSE, |- (2 = 3) = FALSE, |- FALSE = (FALSE = TRUE), |- (7 < 1) = FALSE, |- FALSE = (0 = 9), |- (TRUE = (9 < 1)) = FALSE, |- [not](TRUE) = FALSE, |- FALSE = ((9 < 8) = TRUE), |- (8 < 0) = FALSE, |- FALSE = (TRUE = (3 < 1)), |- (5 <= 4) = FALSE, |- (6 < 5) = FALSE, |- FALSE = (6 = 0), |- (TRUE = (4 < 3)) = FALSE, |- (TRUE = (7 < 0)) = FALSE, |- FALSE = (8 <= 0), |- ((7 < 1) = TRUE) = FALSE, |- ((1 < 0) = TRUE) = FALSE, |- (0 = 8) = FALSE, |- (0 = 4) = FALSE, |- FALSE = (i = 0), |- (9 <= 8) = FALSE, |- ((8 <= 7) = TRUE) = FALSE, |- FALSE = (6 <= 5), |- FALSE = ((3 <= 2) = TRUE), |- FALSE = (TRUE = (9 < 8)), |- FALSE = (TRUE = (pi <= 0)), |- (pi <= 0) = FALSE, |- FALSE = (4 = 5), |- ((6 < 0) = TRUE) = FALSE, |- (7 < 0) = FALSE, |- FALSE = (3 = 2), |- FALSE = ((5 <= 0) = TRUE), |- ((8 < 0) = TRUE) = FALSE, |- ((2 <= 1) = TRUE) = FALSE, |- FALSE = ((7 <= 6) = TRUE), |- ((1 <= 0) = TRUE) = FALSE, |- FALSE = (9 < 8), |- FALSE = ((4 <= 0) = TRUE), |- ((4 < 3) = TRUE) = FALSE, |- ((4 <= 0) = TRUE) = FALSE, |- FALSE = ((6 < 0) = TRUE), |- FALSE = (TRUE = (7 < 6)), |- FALSE = (7 = 8), |- FALSE = (0 = pi), |- FALSE = ((e <= 0) = TRUE), |- FALSE = (TRUE = (6 < 0)), |- FALSE = (TRUE = (2 < 1)), |- (TRUE = (4 < 1)) = FALSE, |- (0 = 7) = FALSE, |- ((5 <= 0) = TRUE) = FALSE, |- FALSE = (e < 0), |- (9 = 8) = FALSE, |- FALSE = (1 < 0), |- ((7 < 0) = TRUE) = FALSE, |- (TRUE = (3 <= 2)) = FALSE, |- (TRUE = (6 < 1)) = FALSE, |- (0 = e) = FALSE, |- (0 = 3) = FALSE, |- ([not](TRUE) = TRUE) = FALSE, |- FALSE = (3 <= 0), |- FALSE = (4 < 3), |- ((3 <= 0) = TRUE) = FALSE, |- ((9 < 1) = TRUE) = FALSE, |- FALSE = (4 < 0), |- FALSE = (TRUE = (5 <= 0)), |- FALSE = (2 = 0), |- ((9 <= 8) = TRUE) = FALSE, |- (8 <= 0) = FALSE, |- FALSE = (TRUE = (6 < 1)), |- FALSE = (0 = i), |- (e = 0) = FALSE, |- FALSE = (TRUE = (8 < 7)), |- ((2 < 0) = TRUE) = FALSE, |- (8 = 9) = FALSE, |- (TRUE = (2 <= 1)) = FALSE, |- (3 = 2) = FALSE, |- FALSE = [not](TRUE), |- (4 = 0) = FALSE, |- (TRUE = (3 < 0)) = FALSE, |- FALSE = (2 = 1), |- FALSE = (TRUE = (5 < 1)), |- (1 = 0) = FALSE}, FALSE = TRUE: {|- (FALSE = TRUE) = FALSE, |- FALSE = (FALSE = TRUE)}, [not](TRUE): {|- FALSE = [not](TRUE), |- [not](TRUE) = FALSE}, TRUE = [not](TRUE): {|- (TRUE = [not](TRUE)) = FALSE, |- FALSE = (TRUE = [not](TRUE))}, [not](TRUE) = TRUE: {|- FALSE = ([not](TRUE) = TRUE), |- ([not](TRUE) = TRUE) = FALSE}, {TRUE, FALSE}: {|- BOOLEAN = {TRUE, FALSE}, |- {TRUE, FALSE} = BOOLEAN}, 0 < 0: {|- (0 < 0) = FALSE, |- FALSE = (0 < 0)}, TRUE = (0 < 0): {|- FALSE = (TRUE = (0 < 0)), |- (TRUE = (0 < 0)) = FALSE}, (0 < 0) = TRUE: {|- ((0 < 0) = TRUE) = FALSE, |- FALSE = ((0 < 0) = TRUE)}, 1: {|- 1 = 1}, Real: {|- Real = Real}, 0 = 1: {|- FALSE = (0 = 1), |- (0 = 1) = FALSE}, 1 = 0: {|- (1 = 0) = FALSE, |- FALSE = (1 = 0)}, 2 < 1: {|- (2 < 1) = FALSE, |- FALSE = (2 < 1)}, TRUE = (2 < 1): {|- (TRUE = (2 < 1)) = FALSE, |- FALSE = (TRUE = (2 < 1))}, (2 < 1) = TRUE: {|- FALSE = ((2 < 1) = TRUE), |- ((2 < 1) = TRUE) = FALSE}, 2 < 0: {|- (2 < 0) = FALSE, |- FALSE = (2 < 0)}, TRUE = (2 < 0): {|- (TRUE = (2 < 0)) = FALSE, |- FALSE = (TRUE = (2 < 0))}, (2 < 0) = TRUE: {|- ((2 < 0) = TRUE) = FALSE, |- FALSE = ((2 < 0) = TRUE)}, 0 = 2: {|- (0 = 2) = FALSE, |- FALSE = (0 = 2)}, 2 = 0: {|- (2 = 0) = FALSE, |- FALSE = (2 = 0)}, 2 <= 0: {|- FALSE = (2 <= 0), |- (2 <= 0) = FALSE}, TRUE = (2 <= 0): {|- FALSE = (TRUE = (2 <= 0)), |- (TRUE = (2 <= 0)) = FALSE}, (2 <= 0) = TRUE: {|- ((2 <= 0) = TRUE) = FALSE, |- FALSE = ((2 <= 0) = TRUE)}, 3 < 1: {|- FALSE = (3 < 1), |- (3 < 1) = FALSE}, TRUE = (3 < 1): {|- (TRUE = (3 < 1)) = FALSE, |- FALSE = (TRUE = (3 < 1))}, (3 < 1) = TRUE: {|- FALSE = ((3 < 1) = TRUE), |- ((3 < 1) = TRUE) = FALSE}, 3 < 0: {|- (3 < 0) = FALSE, |- FALSE = (3 < 0)}, TRUE = (3 < 0): {|- (TRUE = (3 < 0)) = FALSE, |- FALSE = (TRUE = (3 < 0))}, (3 < 0) = TRUE: {|- FALSE = ((3 < 0) = TRUE), |- ((3 < 0) = TRUE) = FALSE}, 0 = 3: {|- FALSE = (0 = 3), |- (0 = 3) = FALSE}, 3 = 0: {|- FALSE = (3 = 0), |- (3 = 0) = FALSE}, 3 <= 0: {|- FALSE = (3 <= 0), |- (3 <= 0) = FALSE}, TRUE = (3 <= 0): {|- FALSE = (TRUE = (3 <= 0)), |- (TRUE = (3 <= 0)) = FALSE}, (3 <= 0) = TRUE: {|- FALSE = ((3 <= 0) = TRUE), |- ((3 <= 0) = TRUE) = FALSE}, 4 < 1: {|- (4 < 1) = FALSE, |- FALSE = (4 < 1)}, TRUE = (4 < 1): {|- (TRUE = (4 < 1)) = FALSE, |- FALSE = (TRUE = (4 < 1))}, (4 < 1) = TRUE: {|- ((4 < 1) = TRUE) = FALSE, |- FALSE = ((4 < 1) = TRUE)}, 4 < 0: {|- (4 < 0) = FALSE, |- FALSE = (4 < 0)}, TRUE = (4 < 0): {|- (TRUE = (4 < 0)) = FALSE, |- FALSE = (TRUE = (4 < 0))}, (4 < 0) = TRUE: {|- ((4 < 0) = TRUE) = FALSE, |- FALSE = ((4 < 0) = TRUE)}, 0 = 4: {|- (0 = 4) = FALSE, |- FALSE = (0 = 4)}, 4 = 0: {|- FALSE = (4 = 0), |- (4 = 0) = FALSE}, 4 <= 0: {|- FALSE = (4 <= 0), |- (4 <= 0) = FALSE}, TRUE = (4 <= 0): {|- FALSE = (TRUE = (4 <= 0)), |- (TRUE = (4 <= 0)) = FALSE}, (4 <= 0) = TRUE: {|- ((4 <= 0) = TRUE) = FALSE, |- FALSE = ((4 <= 0) = TRUE)}, 5 < 1: {|- (5 < 1) = FALSE, |- FALSE = (5 < 1)}, TRUE = (5 < 1): {|- FALSE = (TRUE = (5 < 1)), |- (TRUE = (5 < 1)) = FALSE}, (5 < 1) = TRUE: {|- ((5 < 1) = TRUE) = FALSE, |- FALSE = ((5 < 1) = TRUE)}, 5 < 0: {|- FALSE = (5 < 0), |- (5 < 0) = FALSE}, TRUE = (5 < 0): {|- FALSE = (TRUE = (5 < 0)), |- (TRUE = (5 < 0)) = FALSE}, (5 < 0) = TRUE: {|- FALSE = ((5 < 0) = TRUE), |- ((5 < 0) = TRUE) = FALSE}, 0 = 5: {|- FALSE = (0 = 5), |- (0 = 5) = FALSE}, 5 = 0: {|- FALSE = (5 = 0), |- (5 = 0) = FALSE}, 5 <= 0: {|- (5 <= 0) = FALSE, |- FALSE = (5 <= 0)}, TRUE = (5 <= 0): {|- FALSE = (TRUE = (5 <= 0)), |- (TRUE = (5 <= 0)) = FALSE}, (5 <= 0) = TRUE: {|- FALSE = ((5 <= 0) = TRUE), |- ((5 <= 0) = TRUE) = FALSE}, 6 < 1: {|- (6 < 1) = FALSE, |- FALSE = (6 < 1)}, TRUE = (6 < 1): {|- FALSE = (TRUE = (6 < 1)), |- (TRUE = (6 < 1)) = FALSE}, (6 < 1) = TRUE: {|- ((6 < 1) = TRUE) = FALSE, |- FALSE = ((6 < 1) = TRUE)}, 6 < 0: {|- FALSE = (6 < 0), |- (6 < 0) = FALSE}, TRUE = (6 < 0): {|- (TRUE = (6 < 0)) = FALSE, |- FALSE = (TRUE = (6 < 0))}, (6 < 0) = TRUE: {|- FALSE = ((6 < 0) = TRUE), |- ((6 < 0) = TRUE) = FALSE}, 0 = 6: {|- FALSE = (0 = 6), |- (0 = 6) = FALSE}, 6 = 0: {|- (6 = 0) = FALSE, |- FALSE = (6 = 0)}, 6 <= 0: {|- (6 <= 0) = FALSE, |- FALSE = (6 <= 0)}, TRUE = (6 <= 0): {|- (TRUE = (6 <= 0)) = FALSE, |- FALSE = (TRUE = (6 <= 0))}, (6 <= 0) = TRUE: {|- FALSE = ((6 <= 0) = TRUE), |- ((6 <= 0) = TRUE) = FALSE}, 7 < 1: {|- (7 < 1) = FALSE, |- FALSE = (7 < 1)}, TRUE = (7 < 1): {|- FALSE = (TRUE = (7 < 1)), |- (TRUE = (7 < 1)) = FALSE}, (7 < 1) = TRUE: {|- FALSE = ((7 < 1) = TRUE), |- ((7 < 1) = TRUE) = FALSE}, 7 < 0: {|- FALSE = (7 < 0), |- (7 < 0) = FALSE}, TRUE = (7 < 0): {|- (TRUE = (7 < 0)) = FALSE, |- FALSE = (TRUE = (7 < 0))}, (7 < 0) = TRUE: {|- ((7 < 0) = TRUE) = FALSE, |- FALSE = ((7 < 0) = TRUE)}, 0 = 7: {|- FALSE = (0 = 7), |- (0 = 7) = FALSE}, 7 = 0: {|- FALSE = (7 = 0), |- (7 = 0) = FALSE}, 7 <= 0: {|- (7 <= 0) = FALSE, |- FALSE = (7 <= 0)}, TRUE = (7 <= 0): {|- FALSE = (TRUE = (7 <= 0)), |- (TRUE = (7 <= 0)) = FALSE}, (7 <= 0) = TRUE: {|- FALSE = ((7 <= 0) = TRUE), |- ((7 <= 0) = TRUE) = FALSE}, 8 < 1: {|- (8 < 1) = FALSE, |- FALSE = (8 < 1)}, TRUE = (8 < 1): {|- FALSE = (TRUE = (8 < 1)), |- (TRUE = (8 < 1)) = FALSE}, (8 < 1) = TRUE: {|- FALSE = ((8 < 1) = TRUE), |- ((8 < 1) = TRUE) = FALSE}, 8 < 0: {|- (8 < 0) = FALSE, |- FALSE = (8 < 0)}, TRUE = (8 < 0): {|- FALSE = (TRUE = (8 < 0)), |- (TRUE = (8 < 0)) = FALSE}, (8 < 0) = TRUE: {|- ((8 < 0) = TRUE) = FALSE, |- FALSE = ((8 < 0) = TRUE)}, 0 = 8: {|- FALSE = (0 = 8), |- (0 = 8) = FALSE}, 8 = 0: {|- FALSE = (8 = 0), |- (8 = 0) = FALSE}, 8 <= 0: {|- (8 <= 0) = FALSE, |- FALSE = (8 <= 0)}, TRUE = (8 <= 0): {|- (TRUE = (8 <= 0)) = FALSE, |- FALSE = (TRUE = (8 <= 0))}, (8 <= 0) = TRUE: {|- ((8 <= 0) = TRUE) = FALSE, |- FALSE = ((8 <= 0) = TRUE)}, 9 < 1: {|- FALSE = (9 < 1), |- (9 < 1) = FALSE}, TRUE = (9 < 1): {|- FALSE = (TRUE = (9 < 1)), |- (TRUE = (9 < 1)) = FALSE}, (9 < 1) = TRUE: {|- ((9 < 1) = TRUE) = FALSE, |- FALSE = ((9 < 1) = TRUE)}, 9 < 0: {|- FALSE = (9 < 0), |- (9 < 0) = FALSE}, TRUE = (9 < 0): {|- FALSE = (TRUE = (9 < 0)), |- (TRUE = (9 < 0)) = FALSE}, (9 < 0) = TRUE: {|- ((9 < 0) = TRUE) = FALSE, |- FALSE = ((9 < 0) = TRUE)}, 0 = 9: {|- (0 = 9) = FALSE, |- FALSE = (0 = 9)}, 9 = 0: {|- (9 = 0) = FALSE, |- FALSE = (9 = 0)}, 9 <= 0: {|- FALSE = (9 <= 0), |- (9 <= 0) = FALSE}, TRUE = (9 <= 0): {|- (TRUE = (9 <= 0)) = FALSE, |- FALSE = (TRUE = (9 <= 0))}, (9 <= 0) = TRUE: {|- ((9 <= 0) = TRUE) = FALSE, |- FALSE = ((9 <= 0) = TRUE)}, 1 < 0: {|- FALSE = (1 < 0), |- (1 < 0) = FALSE}, TRUE = (1 < 0): {|- FALSE = (TRUE = (1 < 0)), |- (TRUE = (1 < 0)) = FALSE}, (1 < 0) = TRUE: {|- FALSE = ((1 < 0) = TRUE), |- ((1 < 0) = TRUE) = FALSE}, 1 <= 0: {|- (1 <= 0) = FALSE, |- FALSE = (1 <= 0)}, TRUE = (1 <= 0): {|- FALSE = (TRUE = (1 <= 0)), |- (TRUE = (1 <= 0)) = FALSE}, (1 <= 0) = TRUE: {|- ((1 <= 0) = TRUE) = FALSE, |- FALSE = ((1 <= 0) = TRUE)}, 2 = 1: {|- FALSE = (2 = 1), |- (2 = 1) = FALSE}, 1 = 2: {|- FALSE = (1 = 2), |- (1 = 2) = FALSE}, 2 <= 1: {|- FALSE = (2 <= 1), |- (2 <= 1) = FALSE}, TRUE = (2 <= 1): {|- (TRUE = (2 <= 1)) = FALSE, |- FALSE = (TRUE = (2 <= 1))}, (2 <= 1) = TRUE: {|- ((2 <= 1) = TRUE) = FALSE, |- FALSE = ((2 <= 1) = TRUE)}, 3 < 2: {|- FALSE = (3 < 2), |- (3 < 2) = FALSE}, TRUE = (3 < 2): {|- FALSE = (TRUE = (3 < 2)), |- (TRUE = (3 < 2)) = FALSE}, (3 < 2) = TRUE: {|- ((3 < 2) = TRUE) = FALSE, |- FALSE = ((3 < 2) = TRUE)}, 3 = 2: {|- FALSE = (3 = 2), |- (3 = 2) = FALSE}, 2 = 3: {|- FALSE = (2 = 3), |- (2 = 3) = FALSE}, 3 <= 2: {|- (3 <= 2) = FALSE, |- FALSE = (3 <= 2)}, TRUE = (3 <= 2): {|- (TRUE = (3 <= 2)) = FALSE, |- FALSE = (TRUE = (3 <= 2))}, (3 <= 2) = TRUE: {|- ((3 <= 2) = TRUE) = FALSE, |- FALSE = ((3 <= 2) = TRUE)}, 4 < 3: {|- FALSE = (4 < 3), |- (4 < 3) = FALSE}, TRUE = (4 < 3): {|- (TRUE = (4 < 3)) = FALSE, |- FALSE = (TRUE = (4 < 3))}, (4 < 3) = TRUE: {|- ((4 < 3) = TRUE) = FALSE, |- FALSE = ((4 < 3) = TRUE)}, 4 = 3: {|- (4 = 3) = FALSE, |- FALSE = (4 = 3)}, 3 = 4: {|- (3 = 4) = FALSE, |- FALSE = (3 = 4)}, 4 <= 3: {|- FALSE = (4 <= 3), |- (4 <= 3) = FALSE}, TRUE = (4 <= 3): {|- FALSE = (TRUE = (4 <= 3)), |- (TRUE = (4 <= 3)) = FALSE}, (4 <= 3) = TRUE: {|- ((4 <= 3) = TRUE) = FALSE, |- FALSE = ((4 <= 3) = TRUE)}, 5 < 4: {|- FALSE = (5 < 4), |- (5 < 4) = FALSE}, TRUE = (5 < 4): {|- (TRUE = (5 < 4)) = FALSE, |- FALSE = (TRUE = (5 < 4))}, (5 < 4) = TRUE: {|- FALSE = ((5 < 4) = TRUE), |- ((5 < 4) = TRUE) = FALSE}, 5 = 4: {|- FALSE = (5 = 4), |- (5 = 4) = FALSE}, 4 = 5: {|- FALSE = (4 = 5), |- (4 = 5) = FALSE}, 5 <= 4: {|- FALSE = (5 <= 4), |- (5 <= 4) = FALSE}, TRUE = (5 <= 4): {|- (TRUE = (5 <= 4)) = FALSE, |- FALSE = (TRUE = (5 <= 4))}, (5 <= 4) = TRUE: {|- ((5 <= 4) = TRUE) = FALSE, |- FALSE = ((5 <= 4) = TRUE)}, 6 < 5: {|- FALSE = (6 < 5), |- (6 < 5) = FALSE}, TRUE = (6 < 5): {|- (TRUE = (6 < 5)) = FALSE, |- FALSE = (TRUE = (6 < 5))}, (6 < 5) = TRUE: {|- FALSE = ((6 < 5) = TRUE), |- ((6 < 5) = TRUE) = FALSE}, 6 = 5: {|- FALSE = (6 = 5), |- (6 = 5) = FALSE}, 5 = 6: {|- FALSE = (5 = 6), |- (5 = 6) = FALSE}, 6 <= 5: {|- FALSE = (6 <= 5), |- (6 <= 5) = FALSE}, TRUE = (6 <= 5): {|- FALSE = (TRUE = (6 <= 5)), |- (TRUE = (6 <= 5)) = FALSE}, (6 <= 5) = TRUE: {|- FALSE = ((6 <= 5) = TRUE), |- ((6 <= 5) = TRUE) = FALSE}, 7 < 6: {|- (7 < 6) = FALSE, |- FALSE = (7 < 6)}, TRUE = (7 < 6): {|- (TRUE = (7 < 6)) = FALSE, |- FALSE = (TRUE = (7 < 6))}, (7 < 6) = TRUE: {|- ((7 < 6) = TRUE) = FALSE, |- FALSE = ((7 < 6) = TRUE)}, 7 = 6: {|- FALSE = (7 = 6), |- (7 = 6) = FALSE}, 6 = 7: {|- FALSE = (6 = 7), |- (6 = 7) = FALSE}, 7 <= 6: {|- (7 <= 6) = FALSE, |- FALSE = (7 <= 6)}, TRUE = (7 <= 6): {|- FALSE = (TRUE = (7 <= 6)), |- (TRUE = (7 <= 6)) = FALSE}, (7 <= 6) = TRUE: {|- ((7 <= 6) = TRUE) = FALSE, |- FALSE = ((7 <= 6) = TRUE)}, 8 < 7: {|- FALSE = (8 < 7), |- (8 < 7) = FALSE}, TRUE = (8 < 7): {|- (TRUE = (8 < 7)) = FALSE, |- FALSE = (TRUE = (8 < 7))}, (8 < 7) = TRUE: {|- ((8 < 7) = TRUE) = FALSE, |- FALSE = ((8 < 7) = TRUE)}, 8 = 7: {|- (8 = 7) = FALSE, |- FALSE = (8 = 7)}, 7 = 8: {|- FALSE = (7 = 8), |- (7 = 8) = FALSE}, 8 <= 7: {|- (8 <= 7) = FALSE, |- FALSE = (8 <= 7)}, TRUE = (8 <= 7): {|- (TRUE = (8 <= 7)) = FALSE, |- FALSE = (TRUE = (8 <= 7))}, (8 <= 7) = TRUE: {|- FALSE = ((8 <= 7) = TRUE), |- ((8 <= 7) = TRUE) = FALSE}, 9 < 8: {|- (9 < 8) = FALSE, |- FALSE = (9 < 8)}, TRUE = (9 < 8): {|- FALSE = (TRUE = (9 < 8)), |- (TRUE = (9 < 8)) = FALSE}, (9 < 8) = TRUE: {|- FALSE = ((9 < 8) = TRUE), |- ((9 < 8) = TRUE) = FALSE}, 9 = 8: {|- FALSE = (9 = 8), |- (9 = 8) = FALSE}, 8 = 9: {|- FALSE = (8 = 9), |- (8 = 9) = FALSE}, 9 <= 8: {|- (9 <= 8) = FALSE, |- FALSE = (9 <= 8)}, TRUE = (9 <= 8): {|- FALSE = (TRUE = (9 <= 8)), |- (TRUE = (9 <= 8)) = FALSE}, (9 <= 8) = TRUE: {|- FALSE = ((9 <= 8) = TRUE), |- ((9 <= 8) = TRUE) = FALSE}, -0: {|- (-0) = 0, |- 0 = (-0)}, 0: {|- (-0) = 0, |- 0 = (-0)}, 0 = e: {|- (0 = e) = FALSE, |- FALSE = (0 = e)}, e = 0: {|- (e = 0) = FALSE, |- FALSE = (e = 0)}, e < 0: {|- (e < 0) = FALSE, |- FALSE = (e < 0)}, TRUE = (e < 0): {|- (TRUE = (e < 0)) = FALSE, |- FALSE = (TRUE = (e < 0))}, (e < 0) = TRUE: {|- ((e < 0) = TRUE) = FALSE, |- FALSE = ((e < 0) = TRUE)}, e <= 0: {|- FALSE = (e <= 0), |- (e <= 0) = FALSE}, TRUE = (e <= 0): {|- (TRUE = (e <= 0)) = FALSE, |- FALSE = (TRUE = (e <= 0))}, (e <= 0) = TRUE: {|- ((e <= 0) = TRUE) = FALSE, |- FALSE = ((e <= 0) = TRUE)}, 0 = pi: {|- (0 = pi) = FALSE, |- FALSE = (0 = pi)}, pi = 0: {|- FALSE = (pi = 0), |- (pi = 0) = FALSE}, pi < 0: {|- (pi < 0) = FALSE, |- FALSE = (pi < 0)}, TRUE = (pi < 0): {|- FALSE = (TRUE = (pi < 0)), |- (TRUE = (pi < 0)) = FALSE}, (pi < 0) = TRUE: {|- ((pi < 0) = TRUE) = FALSE, |- FALSE = ((pi < 0) = TRUE)}, pi <= 0: {|- FALSE = (pi <= 0), |- (pi <= 0) = FALSE}, TRUE = (pi <= 0): {|- FALSE = (TRUE = (pi <= 0)), |- (TRUE = (pi <= 0)) = FALSE}, (pi <= 0) = TRUE: {|- FALSE = ((pi <= 0) = TRUE), |- ((pi <= 0) = TRUE) = FALSE}, 0 = i: {|- (0 = i) = FALSE, |- FALSE = (0 = i)}, i = 0: {|- (i = 0) = FALSE, |- FALSE = (i = 0)}}
known_evaluation_sets = {[not](FALSE): {|- [not](FALSE) = TRUE}, TRUE: {|- TRUE = TRUE}, TRUE = FALSE: {|- (TRUE = FALSE) = FALSE}, FALSE = TRUE: {|- (FALSE = TRUE) = FALSE}, [not](TRUE): {|- [not](TRUE) = FALSE}, TRUE = [not](TRUE): {|- (TRUE = [not](TRUE)) = FALSE}, [not](TRUE) = TRUE: {|- ([not](TRUE) = TRUE) = FALSE}, FALSE: {|- FALSE = FALSE}, 0 < 0: {|- (0 < 0) = FALSE}, TRUE = (0 < 0): {|- (TRUE = (0 < 0)) = FALSE}, (0 < 0) = TRUE: {|- ((0 < 0) = TRUE) = FALSE}, 1: {|- 1 = 1}, 0 = 1: {|- (0 = 1) = FALSE}, 1 = 0: {|- (1 = 0) = FALSE}, 2 < 1: {|- (2 < 1) = FALSE}, TRUE = (2 < 1): {|- (TRUE = (2 < 1)) = FALSE}, (2 < 1) = TRUE: {|- ((2 < 1) = TRUE) = FALSE}, 2 < 0: {|- (2 < 0) = FALSE}, TRUE = (2 < 0): {|- (TRUE = (2 < 0)) = FALSE}, (2 < 0) = TRUE: {|- ((2 < 0) = TRUE) = FALSE}, 0 = 2: {|- (0 = 2) = FALSE}, 2 = 0: {|- (2 = 0) = FALSE}, 2 <= 0: {|- (2 <= 0) = FALSE}, TRUE = (2 <= 0): {|- (TRUE = (2 <= 0)) = FALSE}, (2 <= 0) = TRUE: {|- ((2 <= 0) = TRUE) = FALSE}, 3 < 1: {|- (3 < 1) = FALSE}, TRUE = (3 < 1): {|- (TRUE = (3 < 1)) = FALSE}, (3 < 1) = TRUE: {|- ((3 < 1) = TRUE) = FALSE}, 3 < 0: {|- (3 < 0) = FALSE}, TRUE = (3 < 0): {|- (TRUE = (3 < 0)) = FALSE}, (3 < 0) = TRUE: {|- ((3 < 0) = TRUE) = FALSE}, 0 = 3: {|- (0 = 3) = FALSE}, 3 = 0: {|- (3 = 0) = FALSE}, 3 <= 0: {|- (3 <= 0) = FALSE}, TRUE = (3 <= 0): {|- (TRUE = (3 <= 0)) = FALSE}, (3 <= 0) = TRUE: {|- ((3 <= 0) = TRUE) = FALSE}, 4 < 1: {|- (4 < 1) = FALSE}, TRUE = (4 < 1): {|- (TRUE = (4 < 1)) = FALSE}, (4 < 1) = TRUE: {|- ((4 < 1) = TRUE) = FALSE}, 4 < 0: {|- (4 < 0) = FALSE}, TRUE = (4 < 0): {|- (TRUE = (4 < 0)) = FALSE}, (4 < 0) = TRUE: {|- ((4 < 0) = TRUE) = FALSE}, 0 = 4: {|- (0 = 4) = FALSE}, 4 = 0: {|- (4 = 0) = FALSE}, 4 <= 0: {|- (4 <= 0) = FALSE}, TRUE = (4 <= 0): {|- (TRUE = (4 <= 0)) = FALSE}, (4 <= 0) = TRUE: {|- ((4 <= 0) = TRUE) = FALSE}, 5 < 1: {|- (5 < 1) = FALSE}, TRUE = (5 < 1): {|- (TRUE = (5 < 1)) = FALSE}, (5 < 1) = TRUE: {|- ((5 < 1) = TRUE) = FALSE}, 5 < 0: {|- (5 < 0) = FALSE}, TRUE = (5 < 0): {|- (TRUE = (5 < 0)) = FALSE}, (5 < 0) = TRUE: {|- ((5 < 0) = TRUE) = FALSE}, 0 = 5: {|- (0 = 5) = FALSE}, 5 = 0: {|- (5 = 0) = FALSE}, 5 <= 0: {|- (5 <= 0) = FALSE}, TRUE = (5 <= 0): {|- (TRUE = (5 <= 0)) = FALSE}, (5 <= 0) = TRUE: {|- ((5 <= 0) = TRUE) = FALSE}, 6 < 1: {|- (6 < 1) = FALSE}, TRUE = (6 < 1): {|- (TRUE = (6 < 1)) = FALSE}, (6 < 1) = TRUE: {|- ((6 < 1) = TRUE) = FALSE}, 6 < 0: {|- (6 < 0) = FALSE}, TRUE = (6 < 0): {|- (TRUE = (6 < 0)) = FALSE}, (6 < 0) = TRUE: {|- ((6 < 0) = TRUE) = FALSE}, 0 = 6: {|- (0 = 6) = FALSE}, 6 = 0: {|- (6 = 0) = FALSE}, 6 <= 0: {|- (6 <= 0) = FALSE}, TRUE = (6 <= 0): {|- (TRUE = (6 <= 0)) = FALSE}, (6 <= 0) = TRUE: {|- ((6 <= 0) = TRUE) = FALSE}, 7 < 1: {|- (7 < 1) = FALSE}, TRUE = (7 < 1): {|- (TRUE = (7 < 1)) = FALSE}, (7 < 1) = TRUE: {|- ((7 < 1) = TRUE) = FALSE}, 7 < 0: {|- (7 < 0) = FALSE}, TRUE = (7 < 0): {|- (TRUE = (7 < 0)) = FALSE}, (7 < 0) = TRUE: {|- ((7 < 0) = TRUE) = FALSE}, 0 = 7: {|- (0 = 7) = FALSE}, 7 = 0: {|- (7 = 0) = FALSE}, 7 <= 0: {|- (7 <= 0) = FALSE}, TRUE = (7 <= 0): {|- (TRUE = (7 <= 0)) = FALSE}, (7 <= 0) = TRUE: {|- ((7 <= 0) = TRUE) = FALSE}, 8 < 1: {|- (8 < 1) = FALSE}, TRUE = (8 < 1): {|- (TRUE = (8 < 1)) = FALSE}, (8 < 1) = TRUE: {|- ((8 < 1) = TRUE) = FALSE}, 8 < 0: {|- (8 < 0) = FALSE}, TRUE = (8 < 0): {|- (TRUE = (8 < 0)) = FALSE}, (8 < 0) = TRUE: {|- ((8 < 0) = TRUE) = FALSE}, 0 = 8: {|- (0 = 8) = FALSE}, 8 = 0: {|- (8 = 0) = FALSE}, 8 <= 0: {|- (8 <= 0) = FALSE}, TRUE = (8 <= 0): {|- (TRUE = (8 <= 0)) = FALSE}, (8 <= 0) = TRUE: {|- ((8 <= 0) = TRUE) = FALSE}, 9 < 1: {|- (9 < 1) = FALSE}, TRUE = (9 < 1): {|- (TRUE = (9 < 1)) = FALSE}, (9 < 1) = TRUE: {|- ((9 < 1) = TRUE) = FALSE}, 9 < 0: {|- (9 < 0) = FALSE}, TRUE = (9 < 0): {|- (TRUE = (9 < 0)) = FALSE}, (9 < 0) = TRUE: {|- ((9 < 0) = TRUE) = FALSE}, 0 = 9: {|- (0 = 9) = FALSE}, 9 = 0: {|- (9 = 0) = FALSE}, 9 <= 0: {|- (9 <= 0) = FALSE}, TRUE = (9 <= 0): {|- (TRUE = (9 <= 0)) = FALSE}, (9 <= 0) = TRUE: {|- ((9 <= 0) = TRUE) = FALSE}, 1 < 0: {|- (1 < 0) = FALSE}, TRUE = (1 < 0): {|- (TRUE = (1 < 0)) = FALSE}, (1 < 0) = TRUE: {|- ((1 < 0) = TRUE) = FALSE}, 1 <= 0: {|- (1 <= 0) = FALSE}, TRUE = (1 <= 0): {|- (TRUE = (1 <= 0)) = FALSE}, (1 <= 0) = TRUE: {|- ((1 <= 0) = TRUE) = FALSE}, 2 = 1: {|- (2 = 1) = FALSE}, 1 = 2: {|- (1 = 2) = FALSE}, 2 <= 1: {|- (2 <= 1) = FALSE}, TRUE = (2 <= 1): {|- (TRUE = (2 <= 1)) = FALSE}, (2 <= 1) = TRUE: {|- ((2 <= 1) = TRUE) = FALSE}, 3 < 2: {|- (3 < 2) = FALSE}, TRUE = (3 < 2): {|- (TRUE = (3 < 2)) = FALSE}, (3 < 2) = TRUE: {|- ((3 < 2) = TRUE) = FALSE}, 3 = 2: {|- (3 = 2) = FALSE}, 2 = 3: {|- (2 = 3) = FALSE}, 3 <= 2: {|- (3 <= 2) = FALSE}, TRUE = (3 <= 2): {|- (TRUE = (3 <= 2)) = FALSE}, (3 <= 2) = TRUE: {|- ((3 <= 2) = TRUE) = FALSE}, 4 < 3: {|- (4 < 3) = FALSE}, TRUE = (4 < 3): {|- (TRUE = (4 < 3)) = FALSE}, (4 < 3) = TRUE: {|- ((4 < 3) = TRUE) = FALSE}, 4 = 3: {|- (4 = 3) = FALSE}, 3 = 4: {|- (3 = 4) = FALSE}, 4 <= 3: {|- (4 <= 3) = FALSE}, TRUE = (4 <= 3): {|- (TRUE = (4 <= 3)) = FALSE}, (4 <= 3) = TRUE: {|- ((4 <= 3) = TRUE) = FALSE}, 5 < 4: {|- (5 < 4) = FALSE}, TRUE = (5 < 4): {|- (TRUE = (5 < 4)) = FALSE}, (5 < 4) = TRUE: {|- ((5 < 4) = TRUE) = FALSE}, 5 = 4: {|- (5 = 4) = FALSE}, 4 = 5: {|- (4 = 5) = FALSE}, 5 <= 4: {|- (5 <= 4) = FALSE}, TRUE = (5 <= 4): {|- (TRUE = (5 <= 4)) = FALSE}, (5 <= 4) = TRUE: {|- ((5 <= 4) = TRUE) = FALSE}, 6 < 5: {|- (6 < 5) = FALSE}, TRUE = (6 < 5): {|- (TRUE = (6 < 5)) = FALSE}, (6 < 5) = TRUE: {|- ((6 < 5) = TRUE) = FALSE}, 6 = 5: {|- (6 = 5) = FALSE}, 5 = 6: {|- (5 = 6) = FALSE}, 6 <= 5: {|- (6 <= 5) = FALSE}, TRUE = (6 <= 5): {|- (TRUE = (6 <= 5)) = FALSE}, (6 <= 5) = TRUE: {|- ((6 <= 5) = TRUE) = FALSE}, 7 < 6: {|- (7 < 6) = FALSE}, TRUE = (7 < 6): {|- (TRUE = (7 < 6)) = FALSE}, (7 < 6) = TRUE: {|- ((7 < 6) = TRUE) = FALSE}, 7 = 6: {|- (7 = 6) = FALSE}, 6 = 7: {|- (6 = 7) = FALSE}, 7 <= 6: {|- (7 <= 6) = FALSE}, TRUE = (7 <= 6): {|- (TRUE = (7 <= 6)) = FALSE}, (7 <= 6) = TRUE: {|- ((7 <= 6) = TRUE) = FALSE}, 8 < 7: {|- (8 < 7) = FALSE}, TRUE = (8 < 7): {|- (TRUE = (8 < 7)) = FALSE}, (8 < 7) = TRUE: {|- ((8 < 7) = TRUE) = FALSE}, 8 = 7: {|- (8 = 7) = FALSE}, 7 = 8: {|- (7 = 8) = FALSE}, 8 <= 7: {|- (8 <= 7) = FALSE}, TRUE = (8 <= 7): {|- (TRUE = (8 <= 7)) = FALSE}, (8 <= 7) = TRUE: {|- ((8 <= 7) = TRUE) = FALSE}, 9 < 8: {|- (9 < 8) = FALSE}, TRUE = (9 < 8): {|- (TRUE = (9 < 8)) = FALSE}, (9 < 8) = TRUE: {|- ((9 < 8) = TRUE) = FALSE}, 9 = 8: {|- (9 = 8) = FALSE}, 8 = 9: {|- (8 = 9) = FALSE}, 9 <= 8: {|- (9 <= 8) = FALSE}, TRUE = (9 <= 8): {|- (TRUE = (9 <= 8)) = FALSE}, (9 <= 8) = TRUE: {|- ((9 <= 8) = TRUE) = FALSE}, -0: {|- (-0) = 0}, 0 = e: {|- (0 = e) = FALSE}, e = 0: {|- (e = 0) = FALSE}, e < 0: {|- (e < 0) = FALSE}, TRUE = (e < 0): {|- (TRUE = (e < 0)) = FALSE}, (e < 0) = TRUE: {|- ((e < 0) = TRUE) = FALSE}, e <= 0: {|- (e <= 0) = FALSE}, TRUE = (e <= 0): {|- (TRUE = (e <= 0)) = FALSE}, (e <= 0) = TRUE: {|- ((e <= 0) = TRUE) = FALSE}, 0 = pi: {|- (0 = pi) = FALSE}, pi = 0: {|- (pi = 0) = FALSE}, pi < 0: {|- (pi < 0) = FALSE}, TRUE = (pi < 0): {|- (TRUE = (pi < 0)) = FALSE}, (pi < 0) = TRUE: {|- ((pi < 0) = TRUE) = FALSE}, pi <= 0: {|- (pi <= 0) = FALSE}, TRUE = (pi <= 0): {|- (TRUE = (pi <= 0)) = FALSE}, (pi <= 0) = TRUE: {|- ((pi <= 0) = TRUE) = FALSE}, 0 = i: {|- (0 = i) = FALSE}, i = 0: {|- (i = 0) = FALSE}}
known_simplifications = {}

Methods Documentation

static StrongRelationClass()[source]
static WeakRelationClass()[source]
affirm_via_contradiction(self, conclusion, \*\*defaults_config)[source]

From (A=FALSE), derive the conclusion provided that the negated conclusion implies both (A=FALSE) as well as A, and the conclusion is a Boolean.

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

apply_transitivity(self, other, \*\*defaults_config)[source]

From x = y (self) and y = z (other) derive and return x = z. Also works more generally as long as there is a common side to the equations. If “other” is not an equality, reverse roles and call ‘apply_transitivity’ from the “other” side.

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

conclude(self, \*\*defaults_config)[source]

Attempt to conclude the equality various ways: simple reflexivity (x=x), via an evaluation (if one side is an irreducible). Use conclude_via_transitivity for transitivity cases.

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

conclude_boolean_equality(self, \*\*defaults_config)[source]
Prove and return self of the form

A=TRUE given A, A=FALSE given Not(A), or [Not(A)=FALSE] given A.

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

conclude_via_reflexivity(self, \*\*defaults_config)[source]

Prove and return self of the form x = x.

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

deduce_in_bool(self, \*\*defaults_config)[source]

Deduce and return that this equality statement is in the Boolean set.

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

deduce_not_equals(self, \*\*defaults_config)[source]

Deduce x != y assuming not(x = y), where self is x=y.

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

deny_via_contradiction(self, conclusion, \*\*defaults_config)[source]

From (A=FALSE), derive the negated conclusion provided that the conclusion implies both (A=FALSE) as well as A, 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)[source]

From A=FALSE, and assuming A, derive FALSE.

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

derive_is_in_singleton(self, \*\*defaults_config)[source]

From (x = y), derive (x in {y}).

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

derive_left_via_equality(self, \*\*defaults_config)[source]

From A = B, derive A (the Right-Hand-Side) assuming B.

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

derive_reversed(self, \*\*defaults_config)[source]

From x = y derive y = x. This derivation is an automatic side-effect.

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

derive_right_via_equality(self, \*\*defaults_config)[source]

From A = B, derive B (the Right-Hand-Side) assuming A.

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

derive_via_boolean_equality(self, \*\*defaults_config)[source]

From A = TRUE derive A, or from A = FALSE derive Not(A). This derivation is an automatic side-effect. Note, see derive_stmt_eq_true or Not.equate_negated_to_false for the reverse process.

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.

static invert(lambda_map, rhs, assumptions=None)[source]

Given some x -> f(x) map and a right-hand-side, find the x for which f(x) = rhs amongst known equalities under the given assumptions. Return this x if one is found; return None otherwise.

static known_relations_from_left(expr, assumptions_set)[source]

For each Judgment that is an Equals involving the given expression on the left hand side, yield the Judgment and the right hand side.

static known_relations_from_right(expr, assumptions_set)[source]

For each Judgment that is an Equals involving the given expression on the right hand side, yield the Judgment and the left hand side.

negation_side_effects(self, judgment)[source]

Side-effect derivations to attempt automatically for a negated equation.

other_side(self, expr)[source]

Returns the ‘other’ side of the of the equation if the given expr is on one side.

reversed(self)[source]

Return an Equals expression with the right side and left side reversed from this one. This is not a derivation: see derive_reversed().

side_effects(self, judgment)[source]

Record the judgment in Equals.known_equalities, associated from the left hand side and the right hand side. This information may be useful for concluding new equations via transitivity. If the right hand side is an “irreducible value” (see is_irreducible_value), also record it in Equals.known_evaluation_sets for use when the evaluation method is called. Some side-effects derivations are also attempted depending upon the form of this equality. If the rhs is an “irreducible value” (see is_irreducible_value), also record the judgment in the Equals.known_evaluation_sets dictionary, for use when the simplification or evaluation method is called. Some side-effects derivations are also attempted depending upon the form of this equality.

sub_left_side_into(self, lambda_map, \*\*defaults_config)[source]

From x = y, and given P(y), derive P(x) assuming P(y). P(x) is provided via lambda_map as a Lambda expression or an object that returns a Lambda expression when calling lambda_map() (see proveit.lambda_map, proveit.lambda_map.SubExprRepl in particular), or, if neither of those, an expression to upon which to perform a global replacement of self.rhs.

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

sub_right_side_into(self, lambda_map, \*\*defaults_config)[source]

From x = y, and given P(x), derive P(y) assuming P(x). P(x) is provided via lambda_map as a Lambda expression or an object that returns a Lambda expression when calling lambda_map() (see proveit.lambda_map, proveit.lambda_map.SubExprRepl in particular), or, if neither of those, an expression to upon which to perform a global replacement of self.lhs.

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

substitution(self, lambda_map, \*\*defaults_config)[source]

From x = y, and given f(x), derive f(x)=f(y). f(x) is provided via lambda_map as a Lambda expression or an object that returns a Lambda expression when calling lambda_map() (see proveit.lambda_map, proveit.lambda_map.SubExprRepl in particular), or, if neither of those, an expression upon which to perform a global replacement of self.lhs.

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