And

class proveit.logic.And(*operands, styles=None)

Bases: proveit.Operation

Methods Summary

associate(self, start_idx, length, …)	From self, derive and return a form in which operands in the range [start_idx, start_idx+length) are grouped together.
associated(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘association’.
association(self, start_idx, length, …)	Given Boolean operands, deduce that this expression is equal to a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example, (A and B and … and Y and Z) = (A and B … and (L and … and M) and … and Y and Z).
commutation(self[, init_idx, final_idx])	Given Boolean operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx.
commute(self[, init_idx, final_idx])	From self, derive and return a form in which the operand at index init_idx has been moved to final_idx.
commuted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘commutation’.
conclude(self, \*\*defaults_config)	Try to automatically conclude this conjunction via composing the constituents.
conclude_as_redundant(self, \*\*defaults_config)	Conclude an expression of the form A and ..n repeats.
conclude_negation(self, \*\*defaults_config)	Prove the negation of this conjunction (by disproving any operand).
conclude_via_composition(self, …)	Prove and return some (A and B .
conclude_via_demorgans(self, \*\*defaults_config)	# created by JML 6/28/19 From A and B and C conclude Not(Not(A) or Not(B) or Not(C))
deduce_in_bool(self, \*\*defaults_config)	Attempt to deduce, then return, that this ‘and’ expression is in the BOOLEAN set.
deduce_left_in_bool(self, \*\*defaults_config)	Deduce A in Boolean from (A and B) in Boolean.
deduce_part_in_bool(self, index_or_expr, …)	Deduce X in Boolean from (A and B and .
deduce_right_in_bool(self, \*\*defaults_config)	Deduce B in Boolean from (A and B) in Boolean.
derive_any(self, index_or_expr, …)	From (A and .
derive_in_bool(self, \*\*defaults_config)	If the expression can be proven, it must be TRUE and therefore Boolean.
derive_left(self, \*\*defaults_config)	From A and B derive A.
derive_right(self, \*\*defaults_config)	From A and B derive B.
derive_some(self, start_idx[, end_idx])	From (A and .
disassociate(self, idx, \*\*defaults_config)	From self, derive and return a form in which the operand at the given index is ungrouped.
disassociated(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘disassociation’.
disassociation(self, idx, \*\*defaults_config)	Given Boolean operands, deduce that this expression is equal to a form in which the operand at index idx is no longer grouped together. For example, (A and B … and (L and … and M) and … and Y and Z) = (A and B and … and Y and Z).
evaluation(self, \*\*defaults_config)	If possible, return a Judgment of this expression equal to an irreducible value.
group_commutation(self, init_idx, final_idx, …)	Given Boolean operands, deduce that this expression is equal to a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx.
group_commute(self, init_idx, final_idx, length)	Given self, deduce and return a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx.
group_commuted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘group_commutation’.
in_bool_side_effects(self, judgment)	From (A and B and .
negation_side_effects(self, judgment)	Side-effect derivations to attempt automatically for Not(A and B and .
remake_with_style_calls(self)	In order to reconstruct this Expression to have the same styles, what “with…” method calls are most appropriate? Return a tuple of strings with the calls to make.
side_effects(self, judgment)	Side-effect derivations to attempt automatically.
style_options(self)	Return the StyleOptions object for this And expression.
unary_reduction(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
with_total_ordering_style(self)	Use the total ordering style.

Methods Documentation

associate(self, start_idx, length, \*\*defaults_config)

From self, derive and return a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example, from (A and B and … and Y and Z) derive (A and B … and (L and … and M) and … and Y and Z).

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

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

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

association(self, start_idx, length, \*\*defaults_config)

Given Boolean operands, deduce that this expression is equal to a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example,

(A and B and … and Y and Z) = (A and B … and (L and … and M) and … and Y and Z)

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

‘associated’ returns the right-hand side of ‘association’. ‘associate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘association’ for the inner expression.

commutation(self, init_idx=None, final_idx=None, \*\*defaults_config)

Given Boolean operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx. For example, (A and B and … and Y and Z) = (A and … and Y and B and Z) via init_idx = 1 and final_idx = -2.

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

‘commuted’ returns the right-hand side of ‘commutation’. ‘commute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘commutation’ for the inner expression.

commute(self, init_idx=None, final_idx=None, \*\*defaults_config)

From self, derive and return a form in which the operand at index init_idx has been moved to final_idx. For example, given (A and B and … and Y and Z) derive (A and … and Y and B and Z) via init_idx = 1 and final_idx = -2.

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

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

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

conclude(self, \*\*defaults_config)

Try to automatically conclude this conjunction via composing the constituents. That is, conclude some A and B and … and Z via A, B, …, Z individually.

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

conclude_as_redundant(self, \*\*defaults_config)

Conclude an expression of the form A and ..n repeats.. and A given n in Natural and A is TRUE.

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

conclude_negation(self, \*\*defaults_config)

Prove the negation of this conjunction (by disproving any operand).

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

conclude_via_composition(self, \*\*defaults_config)

Prove and return some (A and B … and … Z) via A, B, …, Z each proven individually. See also the compose method to do this constructively.

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

conclude_via_demorgans(self, \*\*defaults_config)

# created by JML 6/28/19 From A and B and C conclude Not(Not(A) or Not(B) or Not(C))

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

deduce_in_bool(self, \*\*defaults_config)

Attempt to deduce, then return, that this ‘and’ expression is in the BOOLEAN set.

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

deduce_left_in_bool(self, \*\*defaults_config)

Deduce A in Boolean from (A and B) in Boolean.

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

deduce_part_in_bool(self, index_or_expr, \*\*defaults_config)

Deduce X in Boolean from (A and B and .. and X and .. and Z) in Boolean provided X by expression or index number.

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

deduce_right_in_bool(self, \*\*defaults_config)

Deduce B in Boolean from (A and B) in Boolean.

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

derive_any(self, index_or_expr, \*\*defaults_config)

From (A and … and X and … and Z) derive X. index_or_expr specifies X, either by index or the expression. If X is an ExprRange, derive the universally quantified form of And(X).

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

derive_in_bool(self, \*\*defaults_config)

If the expression can be proven, it must be TRUE and therefore Boolean.

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

derive_left(self, \*\*defaults_config)

From A and B derive A.

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

derive_right(self, \*\*defaults_config)

From A and B derive B.

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

derive_some(self, start_idx, end_idx=None, \*\*defaults_config)

From (A and … and B and … Z) derive a range of the conjunction, such as (C and … and F). Specify the range by providing the start and end indices (inclusive) w.r.t. operand entries. If end_idx is not provided, it defaults to start_idx for a single entry which should be an ExprRange.

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

disassociate(self, idx, \*\*defaults_config)

From self, derive and return a form in which the operand at the given index is ungrouped. For example, from (A and B … and (L and … and M) and … and Y and Z) derive (A and B and … and Y and Z).

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

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

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

disassociation(self, idx, \*\*defaults_config)

Given Boolean operands, deduce that this expression is equal to a form in which the operand at index idx is no longer grouped together. For example,

(A and B … and (L and … and M) and … and Y and Z) = (A and B and … and Y and Z)

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

‘disassociated’ returns the right-hand side of ‘disassociation’. ‘disassociate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘disassociation’ for the inner expression.

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.

group_commutation(self, init_idx, final_idx, length, disassociate=True, \*\*defaults_config)

Given Boolean operands, deduce that this expression is equal to a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx. final_idx+length). It will do this by performing association first. If disassociate is True, it will be disassociated afterwards.

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

‘group_commuted’ returns the right-hand side of ‘group_commutation’. ‘group_commute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘group_commutation’ for the inner expression.

group_commute(self, init_idx, final_idx, length, disassociate=True, \*\*defaults_config)

Given self, deduce and return a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx. final_idx+length). It will do this by performing association first. If disassocate is True, it will be disassociated afterwards.

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

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

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

in_bool_side_effects(self, judgment)

From (A and B and .. and Z) in Boolean deduce (A in Boolean), (B in Boolean), … (Z in Boolean).

negation_side_effects(self, judgment)

Side-effect derivations to attempt automatically for Not(A and B and .. and .. Z).

remake_with_style_calls(self)

In order to reconstruct this Expression to have the same styles, what “with…” method calls are most appropriate? Return a tuple of strings with the calls to make. The default for the Operation class is to include appropriate ‘with_wrapping_at’ and ‘with_justification’ calls.

side_effects(self, judgment)

Side-effect derivations to attempt automatically.

style_options(self)

Return the StyleOptions object for this And expression.

unary_reduction(self, \*\*defaults_config)

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

‘unary_reduced’ returns the right-hand side of ‘unary_reduction’. ‘unary_reduce’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘unary_reduction’ for the inner expression.

with_total_ordering_style(self)

Use the total ordering style.