Index

A

Abs (class in proveit.numbers) abs_elimination() (proveit.numbers.Abs method) Add (class in proveit.numbers) add() (proveit.numbers.Less method) (proveit.numbers.LessEq method) add_left() (proveit.numbers.Less method) (proveit.numbers.LessEq method) add_option() (proveit.StyleOptions method) add_right() (proveit.numbers.Less method) (proveit.numbers.LessEq method) affirm_via_contradiction() (proveit.logic.Equals method) (proveit.logic.Not method) (proveit.logic.NotEquals method) (proveit.logic.Or method) all_assumptions (proveit.Assumption attribute) all_canceled() (proveit.numbers.Add method) all_conditions() (proveit.OperationOverInstances method) all_dependents() (proveit.Axiom method) (proveit.Theorem method) all_domains() (proveit.OperationOverInstances method) all_instance_params() (proveit.OperationOverInstances method) all_instance_vars() (proveit.OperationOverInstances method) all_required_proofs() (proveit.Proof method) all_requirements() (proveit.Theorem method) all_theorems (proveit.Theorem attribute) And (class in proveit.logic) append_sub_theory_name() (proveit.Theory method) apply() (proveit.Lambda method) apply_transitivities() (proveit.TransitiveRelation static method) apply_transitivity() (proveit.logic.Equals method) (proveit.logic.Iff method) (proveit.logic.Implies method) (proveit.logic.ProperSubset method) (proveit.logic.SetEquiv method) (proveit.logic.SubsetEq method) (proveit.numbers.Divides method) (proveit.numbers.Less method) (proveit.numbers.LessEq method) (proveit.TransitiveRelation method)

ArgumentExtractionError as_expression() (in module proveit) as_expressions() (in module proveit) as_impl() (proveit.Judgment method) as_implication() (proveit.Judgment method) as_int() (proveit.numbers.BinarySequence method) (proveit.numbers.DecimalSequence method) (proveit.numbers.Neg method) (proveit.numbers.Numeral method) as_theorem_or_axiom() (proveit.Judgment method) as_variable() (proveit.Literal method) associate() (proveit.logic.And method) (proveit.logic.Or method) associated() (proveit.logic.And method) (proveit.logic.Or method) (proveit.numbers.Add method) (proveit.numbers.Mult method) association() (proveit.logic.And method) (proveit.logic.Or method) (proveit.numbers.Add method) (proveit.numbers.Mult method) Assumption (class in proveit) assumptions() (proveit.Proof method) auto_equality_prover() (in module proveit) auto_prover() (in module proveit) auto_relation_prover() (in module proveit) Axiom (class in proveit)

B

begin_proof() (proveit.Judgment method) Bijections (class in proveit.logic) BinarySequence (class in proveit.numbers) BooleanSet (class in proveit.logic)

bound_via_operand_bound() (proveit.numbers.NumberOperation method) bundle() (in module proveit) (proveit.logic.Forall method) bundle_equality() (proveit.logic.Forall method)

C

cancelation() (proveit.numbers.Add method) (proveit.numbers.Div method) (proveit.numbers.Mult method) cancelations() (proveit.numbers.Add method) (proveit.numbers.Div method) (proveit.numbers.Mult method) canceled() (proveit.numbers.Add method) Card (class in proveit.logic) CartExp (class in proveit.logic) CartProd (class in proveit.logic) Ceil (class in proveit.numbers) check_proven_class_membership() (proveit.logic.InClass static method) choose() (proveit.logic.Exists method) class_paths (proveit.Expression attribute) ClassMembership (class in proveit.logic) ClassNonmembership (class in proveit.logic) clean_active_folder() (proveit.Theory method) combined_exponents() (proveit.numbers.Div method) (proveit.numbers.Mult method) commutation() (proveit.logic.And method) (proveit.logic.Or method) (proveit.numbers.Add method) (proveit.numbers.Mult method) commute() (proveit.logic.And method) (proveit.logic.Or method) commuted() (proveit.logic.And method) (proveit.logic.Or method) (proveit.numbers.Add method) (proveit.numbers.Mult method) complex_polar_coordinates() (in module proveit.numbers) compose() (in module proveit.logic) (proveit.Lambda method) compose_fraction() (in module proveit.numbers) compose_product() (in module proveit.numbers) Composite (class in proveit) composite_expression() (in module proveit) Composition (class in proveit) computation() (proveit.core_expr_types.Len method) computed() (proveit.core_expr_types.Len method) conclude() (proveit.Expression method) (proveit.logic.And method) (proveit.logic.ClassMembership method) (proveit.logic.ClassNonmembership method) (proveit.logic.Equals method) (proveit.logic.Exists method) (proveit.logic.Forall method) (proveit.logic.Iff method) (proveit.logic.Implies method) (proveit.logic.InClass method) (proveit.logic.InSet method) (proveit.logic.Not method) (proveit.logic.NotEquals method) (proveit.logic.NotInClass method) (proveit.logic.NotInSet method) (proveit.logic.NotProperSubset method) (proveit.logic.NotSubsetEq method) (proveit.logic.Or method) (proveit.logic.SetEquiv method) (proveit.logic.SubsetEq method) (proveit.logic.TrueLiteral method) (proveit.numbers.Divides method) (proveit.numbers.Less method) (proveit.TransitiveRelation method)

conclude_as_folded() (proveit.logic.NotEquals method) (proveit.logic.NotExists method) (proveit.logic.NotInClass method) (proveit.logic.NotInSet method) (proveit.logic.NotProperSubset method) (proveit.logic.NotSubsetEq method) (proveit.logic.SetEquiv method) (proveit.logic.SetNotEquiv method) (proveit.logic.SubsetEq method) conclude_as_redundant() (proveit.logic.And method) conclude_boolean_equality() (proveit.logic.Equals method) conclude_by_cases() (proveit.logic.Forall method) conclude_by_definition() (proveit.logic.Iff method) conclude_negation() (proveit.Expression method) (proveit.logic.And method) (proveit.logic.FalseLiteral method) (proveit.logic.Iff method) (proveit.logic.Implies method) (proveit.logic.Not method) (proveit.logic.Or method) conclude_self_implication() (proveit.logic.Implies method) conclude_via_both() (proveit.logic.Or method) conclude_via_composition() (proveit.logic.And method) conclude_via_demorgans() (proveit.logic.And method) (proveit.logic.Or method) conclude_via_domain_inclusion() (proveit.logic.Exists method) (proveit.logic.Forall method) conclude_via_double_negation() (proveit.logic.Implies method) (proveit.logic.Not method) (proveit.logic.NotEquals method) conclude_via_equality() (proveit.logic.SubsetEq method) (proveit.numbers.LessEq method) conclude_via_equivalence() (proveit.logic.SubsetEq method) conclude_via_example() (proveit.logic.Exists method) (proveit.logic.Or method) conclude_via_factor() (proveit.numbers.Divides method) conclude_via_falsified_negation() (proveit.logic.Not method) conclude_via_implication() (in module proveit.logic) (proveit.Expression method) conclude_via_left() (proveit.logic.Or method) conclude_via_only_left() (proveit.logic.Or method) conclude_via_only_right() (proveit.logic.Or method) conclude_via_permutation() (proveit.logic.Or method) conclude_via_reflexivity() (proveit.logic.Equals method) (proveit.logic.SetEquiv method) (proveit.numbers.Divides method) conclude_via_some() (proveit.logic.Or method) conclude_via_transitivity() (proveit.TransitiveRelation method) conclude_via_zero_factor() (proveit.numbers.Divides method) Conditional (class in proveit) ConditionalSet (class in proveit) Conjugate (class in proveit.numbers) contains_any_expression() (proveit.Theory method) contains_range() (proveit.ExprTuple method) contrapose() (proveit.logic.Implies method) conversion_to_addition() (proveit.numbers.Mult method) conversion_to_multiplication() (proveit.numbers.Add method) copy() (proveit.Expression method) core_info() (proveit.Expression method) cur_sub_expr() (proveit.InnerExpr method)

D

DecimalSequence (class in proveit.numbers) deduce_as_mon_dec_func() (in module proveit.numbers) deduce_bound() (proveit.numbers.Add method) (proveit.numbers.NumberOperation method) (proveit.numbers.Sum method) deduce_difference_in_natural() (proveit.numbers.Add method) deduce_difference_in_natural_pos() (proveit.numbers.Add method) deduce_divided_by() (proveit.numbers.Mult method) deduce_double_negation_equiv() (proveit.logic.Not method) deduce_elem_in_set() (proveit.numbers.Interval method) (proveit.numbers.IntervalCC method) (proveit.numbers.IntervalCO method) (proveit.numbers.IntervalOC method) (proveit.numbers.IntervalOO method) deduce_enum_proper_subset() (proveit.logic.Set method) deduce_enum_subset_eq() (proveit.logic.Set method) deduce_equal_or_not() (in module proveit.logic) deduce_greater_than_equals_zero() (proveit.numbers.Abs method) deduce_in_bool() (proveit.logic.And method) (proveit.logic.ClassMembership method) (proveit.logic.ClassNonmembership method) (proveit.logic.Equals method) (proveit.logic.Exists method) (proveit.logic.FalseLiteral method) (proveit.logic.Forall method) (proveit.logic.Iff method) (proveit.logic.Implies method) (proveit.logic.Not method) (proveit.logic.NotEquals method) (proveit.logic.NotInClass method) (proveit.logic.NotInSet method) (proveit.logic.NotProperSubset method) (proveit.logic.NotSubsetEq method) (proveit.logic.Or method) (proveit.logic.ProperSubset method) (proveit.logic.SetEquiv method) (proveit.logic.SetNotEquiv method) (proveit.logic.SubsetEq method) (proveit.logic.TrueLiteral method) (proveit.numbers.Divides method) (proveit.numbers.Less method) (proveit.numbers.LessEq method) deduce_in_digits() (proveit.numbers.Numeral method) deduce_in_interval() (proveit.numbers.Mod method) deduce_in_natural() (proveit.numbers.DecimalSequence method) (proveit.numbers.Numeral method) deduce_in_natural_pos() (proveit.numbers.DecimalSequence method) (proveit.numbers.Numeral method) deduce_in_number_set() (in module proveit.numbers) (proveit.core_expr_types.Len method) (proveit.numbers.Abs method) (proveit.numbers.Add method) (proveit.numbers.Ceil method) (proveit.numbers.DecimalSequence method) (proveit.numbers.Div method) (proveit.numbers.Exp method) (proveit.numbers.Floor method) (proveit.numbers.Mod method) (proveit.numbers.ModAbs method) (proveit.numbers.Mult method) (proveit.numbers.Neg method) (proveit.numbers.Numeral method) (proveit.numbers.Round method) (proveit.numbers.Sum method) deduce_left_in_bool() (proveit.logic.And method) (proveit.logic.Or method) deduce_left_relaxed_membership() (proveit.numbers.IntervalOO method) deduce_member_in_real() (proveit.numbers.IntervalCC method) (proveit.numbers.IntervalCO method) (proveit.numbers.IntervalOC method) (proveit.numbers.IntervalOO method) deduce_member_lower_bound() (proveit.numbers.IntervalCC method) (proveit.numbers.IntervalCO method) (proveit.numbers.IntervalOC method) (proveit.numbers.IntervalOO method) deduce_member_upper_bound() (proveit.numbers.IntervalCC method) (proveit.numbers.IntervalCO method) (proveit.numbers.IntervalOC method) (proveit.numbers.IntervalOO method) deduce_negated_left_impl() (proveit.logic.Implies method) deduce_negated_reflex() (proveit.logic.Implies method) deduce_negated_right_impl() (proveit.logic.Implies method) deduce_not_equal_numeric_rationals() (in module proveit.numbers) deduce_not_equals() (proveit.logic.Equals method) deduce_not_equiv() (proveit.logic.SetEquiv method) deduce_not_exists() (proveit.logic.Exists method) deduce_not_in() (proveit.logic.InClass method) (proveit.logic.InSet method) deduce_not_left_if_neither() (proveit.logic.Or method) deduce_not_right_if_neither() (proveit.logic.Or method) deduce_not_zero() (proveit.numbers.Exp method) deduce_number_set() (in module proveit.numbers) deduce_operand_in_bool() (proveit.logic.Not method) deduce_part_in_bool() (proveit.logic.And method) (proveit.logic.Or method) deduce_positive() (proveit.numbers.Numeral method) deduce_relatively_prime() (proveit.numbers.GCD method) deduce_relaxed_membership() (proveit.numbers.IntervalCO method) (proveit.numbers.IntervalOC method) deduce_rescaled_membership() (proveit.numbers.IntervalCC method) (proveit.numbers.IntervalCO method) (proveit.numbers.IntervalOC method) (proveit.numbers.IntervalOO method) deduce_right_in_bool() (proveit.logic.And method) (proveit.logic.Or method) deduce_right_relaxed_membership() (proveit.numbers.IntervalOO method) deduce_subset_eq_relation() (proveit.logic.CartExp method) (proveit.numbers.Interval method)

Deduction (class in proveit) deep_eliminated_ones() (proveit.numbers.Div method) (proveit.numbers.Mult method) deep_one_eliminations() (proveit.numbers.Div method) (proveit.numbers.Mult method) default (proveit.Theory attribute) default_domain (proveit.numbers.MonDecFuncs attribute) definition() (proveit.logic.ClassMembership method) (proveit.logic.ClassNonmembership method) (proveit.logic.Exists method) (proveit.logic.Iff method) (proveit.logic.NotEquals method) (proveit.logic.SetNotEquiv method) deny_antecedent() (proveit.logic.Implies method) deny_assumption() (proveit.logic.FalseLiteral method) deny_via_contradiction() (proveit.logic.Equals method) (proveit.logic.Not method) (proveit.logic.NotEquals method) (proveit.logic.Or method) derive_added() (proveit.numbers.NumberOrderingRelation method) derive_any() (proveit.logic.And method) derive_consequent() (proveit.logic.Implies method) derive_contradiction() (proveit.logic.Equals method) (proveit.logic.Not method) (proveit.logic.NotEquals method) (proveit.logic.Or method) (proveit.logic.SetNotEquiv method) derive_equality() (proveit.logic.Iff method) derive_iff() (proveit.logic.Implies method) derive_in_bool() (proveit.logic.And method) (proveit.logic.Not method) (proveit.logic.Or method) derive_is_in_singleton() (proveit.logic.Equals method) derive_left() (proveit.logic.And method) (proveit.logic.Iff method) derive_left_if_not_right() (proveit.logic.Or method) derive_left_implication() (proveit.logic.Iff method) derive_left_via_equality() (proveit.logic.Equals method) derive_negated() (proveit.numbers.LessEq method) derive_negated_forall() (proveit.logic.Exists method) derive_relaxed() (proveit.logic.ProperSubset method) (proveit.numbers.Less method) derive_reversed() (proveit.logic.Equals method) (proveit.logic.Iff method) (proveit.logic.NotEquals method) (proveit.logic.SetEquiv method) (proveit.logic.SetNotEquiv method) derive_right() (proveit.logic.And method) (proveit.logic.Iff method) derive_right_if_not_left() (proveit.logic.Or method) derive_right_implication() (proveit.logic.Iff method) derive_right_via_equality() (proveit.logic.Equals method) derive_shifted() (proveit.numbers.Less method) (proveit.numbers.LessEq method) (proveit.numbers.NumberOrderingRelation method) derive_side_effects() (proveit.Judgment method) derive_some() (proveit.logic.And method) derive_subset_nonmembership() (proveit.logic.SubsetEq method) derive_superset_membership() (proveit.logic.ProperSubset method) (proveit.logic.SubsetEq method) derive_untrue() (proveit.logic.Not method) derive_via_boolean_equality() (proveit.logic.Equals method) derive_via_contradiction() (proveit.logic.Implies method) derive_via_dilemma() (proveit.logic.Or method) derive_via_double_negation() (proveit.logic.Not method) (proveit.logic.NotEquals method) derive_via_multi_dilemma() (proveit.logic.Or method) derive_via_singular_dilemma() (proveit.logic.Or method) Difference (class in proveit.logic) direct_dependents() (proveit.Axiom method) (proveit.Theorem method) disable() (proveit.Proof method) disassociate() (proveit.logic.And method) (proveit.logic.Or method) disassociated() (proveit.logic.And method) (proveit.logic.Or method) (proveit.numbers.Add method) (proveit.numbers.Mult method) disassociation() (proveit.logic.And method) (proveit.logic.Or method) (proveit.numbers.Add method) (proveit.numbers.Mult method) Disjoint (class in proveit.logic) disprove() (proveit.Expression method) disproven() (proveit.Expression method) dist_add() (in module proveit.numbers) dist_subtract() (in module proveit.numbers) Distinct (class in proveit.logic) distinct_subset_existence() (proveit.logic.Card method) distributed() (proveit.numbers.Exp method) (proveit.numbers.Mult method) (proveit.numbers.Neg method) distribution() (proveit.numbers.Div method) (proveit.numbers.Exp method) (proveit.numbers.Mult method) (proveit.numbers.Neg method) Div (class in proveit.numbers) divide_both_sides() (proveit.numbers.Less method) (proveit.numbers.LessEq method) Divides (class in proveit.numbers) DividesProper (class in proveit.numbers) domain_conditions() (proveit.OperationOverInstances method) double_neg_simplification() (proveit.numbers.Neg method) double_neg_simplified() (proveit.numbers.Neg method) double_negation_equivalence() (proveit.logic.Not method) DuplicateLiteralError

E

effective_condition() (proveit.OperationOverInstances method) elem_substitution() (proveit.logic.Set method) eliminate() (proveit.Judgment method) (proveit.logic.Exists static method) eliminate_common_exponent() (proveit.numbers.Divides method) eliminate_dividend_exponent() (proveit.numbers.Divides method) eliminated_zero() (proveit.numbers.Add method) eliminated_zeros() (proveit.numbers.Add method) end_indices() (proveit.ExprRange method) enumerated_proof_steps() (proveit.Proof method) equality_prover() (in module proveit) equality_side_effects() (proveit.numbers.Add method) Equals (class in proveit.logic) equate_negated_to_false() (proveit.logic.Not method) EquivalenceClass() (proveit.TransitiveRelation static method) eval_equality() (proveit.logic.FalseLiteral method) (proveit.logic.IrreducibleValue method) (proveit.logic.TrueLiteral method) (proveit.numbers.Numeral method) evaluate_falsehood() (in module proveit.logic) evaluate_truth() (in module proveit.logic) evaluated() (proveit.Expression method) evaluation() (proveit.Expression method) (proveit.Judgment method) (proveit.logic.And method) (proveit.logic.Equals method) (proveit.logic.Iff method) (proveit.logic.Implies method) (proveit.logic.Not method) (proveit.logic.NotEquals method) (proveit.logic.Or method)

evaluation_or_simplification() (in module proveit.logic) EvaluationError Exists (class in proveit.logic) Exp (class in proveit.numbers) exp2pi_i() (in module proveit.numbers) expansion() (proveit.numbers.Exp method) explicit_conditions() (proveit.OperationOverInstances method) explicit_domains() (proveit.OperationOverInstances method) explicit_instance_params() (proveit.OperationOverInstances method) explicit_instance_vars() (proveit.OperationOverInstances method) exponent_combination() (proveit.numbers.Div method) exponentiate_both_sides() (proveit.numbers.Less method) (proveit.numbers.LessEq method) expr_info() (proveit.Expression method) ExprArray (class in proveit) Expression (class in proveit) expression_depth() (in module proveit) expression_notebook() (proveit.Theory static method) ExprRange (class in proveit) ExprTuple (class in proveit) ExprTupleError extract_argument() (proveit.Lambda method) extract_arguments() (proveit.Lambda method) extract_init_arg_value() (proveit.core_expr_types.Len static method) (proveit.Operation class method) extract_markdowntitle_of_notebook() (proveit.Theory static method) extract_my_init_arg_value() (proveit.Operation method) (proveit.OperationOverInstances method) extract_var_tuple_indices() (in module proveit)

F

factorization() (proveit.numbers.Add method) (proveit.numbers.Mult method) (proveit.numbers.Neg method) (proveit.numbers.Sum method) factorized() (proveit.numbers.Add method) (proveit.numbers.Mult method) (proveit.numbers.Neg method) (proveit.numbers.Sum method) FalseLiteral (class in proveit.logic) find_axiom() (proveit.Theory static method) find_judgment() (proveit.Judgment static method) find_theorem() (proveit.Theory static method) first() (proveit.ExprRange method) first_domain() (proveit.OperationOverInstances method) flat() (proveit.ExprArray method)

Floor (class in proveit.numbers) Forall (class in proveit.logic) forall_evaluation() (proveit.logic.BooleanSet method) forget_judgments() (proveit.Judgment static method) formatted() (proveit.ExprArray method) (proveit.Expression method) (proveit.ExprRange method) (proveit.ExprTuple method) (proveit.logic.CartExp method) (proveit.numbers.Exp method) (proveit.numbers.Integrate method) frac() (in module proveit.numbers) free_var_ranges() (in module proveit) free_vars() (in module proveit) Function (class in proveit) Functions (class in proveit.logic)

G

GCD (class in proveit.numbers) Generalization (class in proveit) GeneralizationFailure generalize() (proveit.Judgment method) (proveit.logic.Implies method) generate_all_contained_axioms() (proveit.Theory method) generate_inner_expressions() (in module proveit) generate_local_axioms() (proveit.Theory method) generate_sub_theories() (proveit.Theory method) get_axiom() (proveit.Theory method) get_axiom_names() (proveit.Theory method) get_common_expr() (proveit.Theory method) get_common_expression_names() (proveit.Theory method) get_expression_axiom_and_theorem_names() (proveit.Theory method) get_expression_axiom_or_theorem_kind() (proveit.Theory method) get_format_row_element_positions() (proveit.VertExprArray method) get_latex_formatted_cells() (proveit.VertExprArray method) get_link() (proveit.Axiom method) (proveit.Proof method) (proveit.Theorem method) get_path() (proveit.Theory method) get_presumptions_and_exclusions() (proveit.Theorem method) get_show_proof() (proveit.Theory method)

get_stored_axiom() (proveit.Theory static method) get_stored_expr() (proveit.Theory method) get_stored_judgment_or_proof() (proveit.Theory method) get_stored_stmt() (proveit.Theory static method) get_stored_theorem() (proveit.Theory static method) get_style() (proveit.Expression method) get_styles() (proveit.Expression method) get_sub_theory_names() (proveit.Theory method) get_theorem() (proveit.Theory method) get_theorem_names() (proveit.Theory method) get_theory() (proveit.Theory static method) global_repl() (proveit.Lambda method) greater() (in module proveit.numbers) greater_eq() (in module proveit.numbers) group_commutation() (proveit.logic.And method) (proveit.logic.Or method) (proveit.numbers.Add method) (proveit.numbers.Mult method) group_commute() (proveit.logic.And method) (proveit.logic.Or method) group_commuted() (proveit.logic.And method) (proveit.logic.Or method) (proveit.numbers.Add method) (proveit.numbers.Mult method)

H

has_domain() (proveit.OperationOverInstances method) has_matching_ranges() (proveit.ExprTuple method)

has_one_domain() (proveit.OperationOverInstances method) has_proof() (proveit.Theorem method) horiz_var_array() (in module proveit)

I

Iff (class in proveit.logic) Image (class in proveit.logic) Implies (class in proveit.logic) ImproperReplacement in_bool() (in module proveit.logic) in_bool_side_effects() (proveit.logic.And method) (proveit.logic.Not method) (proveit.logic.Or method) in_progress_to_conclude (proveit.Expression attribute) in_progress_to_derive_sideeffects (proveit.Judgment attribute) InClass (class in proveit.logic) inclass_expressions (proveit.logic.InClass attribute) index() (proveit.ExprTuple method) (proveit.numbers.Mult method) IndexedVar (class in proveit) initializing (proveit.logic.Equals attribute) (proveit.logic.SetEquiv attribute) Injections (class in proveit.logic) inner_expr() (proveit.Expression method) (proveit.Judgment method) inner_neg_mult_simplification() (proveit.numbers.Neg method) inner_neg_mult_simplified() (proveit.numbers.Neg method) InnerExpr (class in proveit) InnerExprGenerator (class in proveit) innermost_body() (proveit.ExprRange method) insertion_point() (proveit.TransitiveRelation class method) InSet (class in proveit.logic) instance() (proveit.Literal class method) instance_param_lists() (proveit.OperationOverInstances method) instances (proveit.Literal attribute)

instantiate() (proveit.Judgment method) (proveit.logic.Forall method) Instantiation (class in proveit) InstantiationFailure Integrate (class in proveit.numbers) Intersect (class in proveit.logic) IntersectAll (class in proveit.logic) Interval (class in proveit.numbers) IntervalCC (class in proveit.numbers) IntervalCO (class in proveit.numbers) IntervalOC (class in proveit.numbers) IntervalOO (class in proveit.numbers) introduce_common_exponent() (proveit.numbers.Divides method) InvalidAssumptions (class in proveit) inversions (proveit.logic.Equals attribute) invert() (proveit.logic.Equals static method) InvImage (class in proveit.logic) IrreducibleValue (class in proveit.logic) is_conjecture() (proveit.Theorem method) is_double() (proveit.ExprTuple method) is_fully_proven() (proveit.Theorem method) is_irreducible_value() (in module proveit.logic) is_numeric_int() (in module proveit.numbers) is_numeric_natural() (in module proveit.numbers) is_numeric_rational() (in module proveit.numbers) is_proper_class (proveit.numbers.MonDecFuncs attribute) is_root() (proveit.Theory method) is_single() (proveit.ExprTuple method) is_usable() (proveit.Judgment method) (proveit.Proof method) items() (proveit.NamedExprs method)

J

Judgment (class in proveit)

K

keys() (proveit.NamedExprs method) known_equalities (proveit.logic.Equals attribute) known_equivalences (proveit.logic.SetEquiv attribute) known_evaluation_sets (proveit.logic.Equals attribute) known_instance_maps (proveit.logic.Exists attribute) (proveit.logic.Forall attribute) known_left_sides (proveit.logic.Iff attribute) (proveit.logic.Implies attribute) (proveit.logic.ProperSubset attribute) (proveit.logic.SubsetEq attribute) (proveit.numbers.Divides attribute) (proveit.numbers.DividesProper attribute) (proveit.numbers.Less attribute) (proveit.numbers.LessEq attribute) known_memberships (proveit.logic.InClass attribute) (proveit.logic.InSet attribute)

known_mon_dec_funcs_memberships (proveit.numbers.MonDecFuncs attribute) known_relations_from_left() (proveit.logic.Equals static method) (proveit.TransitiveRelation class method) known_relations_from_right() (proveit.logic.Equals static method) (proveit.TransitiveRelation class method) known_right_sides (proveit.logic.Iff attribute) (proveit.logic.Implies attribute) (proveit.logic.ProperSubset attribute) (proveit.logic.SubsetEq attribute) (proveit.numbers.Divides attribute) (proveit.numbers.DividesProper attribute) (proveit.numbers.Less attribute) (proveit.numbers.LessEq attribute) known_simplifications (proveit.logic.Equals attribute) KroneckerDelta (class in proveit.numbers)

L

Label (class in proveit) labeled_to_canonical_meaning_data (proveit.Expression attribute) Lambda (class in proveit) LambdaApplicationError last() (proveit.ExprRange method) latex() (proveit.Conditional method) (proveit.ConditionalSet method) (proveit.core_expr_types.Len method) (proveit.ExprArray method) (proveit.Expression method) (proveit.ExprRange method) (proveit.ExprTuple method) (proveit.Judgment method) (proveit.Label method) (proveit.Lambda method) (proveit.logic.Bijections method) (proveit.logic.Card method) (proveit.logic.CartExp method) (proveit.logic.Functions method) (proveit.logic.Image method) (proveit.logic.Injections method) (proveit.logic.InvImage method) (proveit.logic.Not method) (proveit.logic.Set method) (proveit.logic.Surjections method) (proveit.NamedExprs method) (proveit.numbers.Abs method) (proveit.numbers.Ceil method) (proveit.numbers.Conjugate method) (proveit.numbers.Div method) (proveit.numbers.Exp method) (proveit.numbers.Floor method) (proveit.numbers.Interval method) (proveit.numbers.IntervalCC method) (proveit.numbers.IntervalCO method) (proveit.numbers.IntervalOC method) (proveit.numbers.IntervalOO method) (proveit.numbers.KroneckerDelta method) (proveit.numbers.Log method) (proveit.numbers.ModAbs method) (proveit.numbers.Neg method) (proveit.Operation method) (proveit.OperationOverInstances method) (proveit.VertExprArray method)

left_add_both_sides() (proveit.numbers.Less method) (proveit.numbers.LessEq method) left_mult_both_sides() (proveit.numbers.Less method) (proveit.numbers.LessEq method) Len (class in proveit.core_expr_types) Less (class in proveit.numbers) less_eq_numeric_ints() (in module proveit.numbers) less_eq_numeric_rationals() (in module proveit.numbers) less_numeric_ints() (in module proveit.numbers) less_numeric_rationals() (in module proveit.numbers) LessEq (class in proveit.numbers) links() (proveit.Theory method) Literal (class in proveit) literal_int_extent() (proveit.ExprRange method) Log (class in proveit.numbers)

M

make_assumption() (proveit.Assumption static method) make_literal() (proveit.numbers.Numeral static method) MakeNotImplemented mapped_range() (proveit.ExprRange method) Max (class in proveit.numbers) maybe_fenced() (in module proveit) maybe_fenced_latex() (in module proveit) maybe_fenced_string() (in module proveit) membership_object() (proveit.logic.BooleanSet method) (proveit.logic.CartExp method) (proveit.logic.Intersect method) (proveit.logic.Set method) (proveit.logic.Union method) (proveit.numbers.Exp method) (proveit.numbers.MonDecFuncs method) merged() (proveit.ExprTuple method)

merger() (proveit.ExprTuple method) mergesort() (proveit.TransitiveRelation class method) mergesorted_items() (proveit.TransitiveRelation class method) Min (class in proveit.numbers) Mod (class in proveit.numbers) ModAbs (class in proveit.numbers) module proveit proveit.core_expr_types proveit.logic proveit.numbers proveit.physics ModusPonens (class in proveit) ModusPonensFailure MonDecFuncs (class in proveit.numbers) moved() (proveit.logic.Set method) Mult (class in proveit.numbers)

N

NamedExprs (class in proveit) Neg (class in proveit.numbers) neg_simplification() (proveit.numbers.Mult method) neg_simplifications() (proveit.numbers.Mult method) negated() (in module proveit.numbers) (proveit.logic.InClass method) (proveit.logic.NotInClass method) negation_side_effects() (proveit.logic.And method) (proveit.logic.Equals method) (proveit.logic.Exists method) (proveit.logic.Implies method) (proveit.logic.InClass method) (proveit.logic.InSet method) (proveit.logic.Or method) (proveit.logic.SetEquiv method) nested_range_depth() (proveit.ExprRange method) nonmembership_object() (proveit.logic.BooleanSet method) (proveit.logic.Intersect method) (proveit.logic.Set method) (proveit.logic.Union method)

Not (class in proveit.logic) not_equal_numeric_rationals() (in module proveit.numbers) not_proper_superset() (in module proveit.logic) not_superset_eq() (in module proveit.logic) NotEquals (class in proveit.logic) NotExists (class in proveit.logic) NotInClass (class in proveit.logic) notinclass_expressions (proveit.logic.NotInClass attribute) NotInSet (class in proveit.logic) NotProperSubset (class in proveit.logic) NotSubsetEq (class in proveit.logic) num() (in module proveit.numbers) num_elements() (proveit.ExprTuple method) num_entries() (proveit.ExprTuple method) num_steps() (proveit.Proof method) num_sub_expr() (proveit.Expression method) number_ordering() (in module proveit.numbers) NumberOperation (class in proveit.numbers) NumberOrderingRelation (class in proveit.numbers) Numeral (class in proveit.numbers) numeric_rational_ints() (in module proveit.numbers)

O

one_elimination() (proveit.numbers.Mult method) one_eliminations() (proveit.numbers.Mult method) Operation (class in proveit) operation_class_of_operator (proveit.Operation attribute) OperationError

OperationOverInstances (class in proveit) Or (class in proveit.logic) order_of_appearance() (proveit.Expression method) (proveit.Judgment method) other_side() (proveit.logic.Equals method)

P

ParameterCollisionError ParameterMaskingError ParameterRelabelingError parameters() (proveit.ExprRange method) partition() (proveit.ExprRange method) partitioned() (proveit.ExprRange method) permutation() (proveit.logic.Set method) permutation_move() (proveit.logic.Set method) permutation_swap() (proveit.logic.Set method) permuted() (proveit.logic.Set method) PowerSet (class in proveit.logic) presumed_theorems_and_theories (proveit.Judgment attribute) presuming_theorem_and_theory_exclusions (proveit.Judgment attribute) print_dependents() (proveit.Judgment method) print_requirements() (proveit.Judgment method) Prod (class in proveit.numbers) Proof (class in proveit) proof() (proveit.Judgment method)

proof_notebook() (proveit.Theory method) ProofFailure proper_superset() (in module proveit.logic) ProperSubset (class in proveit.logic) prove() (proveit.Expression method) prove_by_cases() (proveit.logic.Set method) proveit module proveit.core_expr_types module proveit.logic module proveit.numbers module proveit.physics module proven() (proveit.Expression method) prover() (in module proveit)

Q

qed_in_progress (proveit.Judgment attribute)

quick_simplified_index() (in module proveit.numbers)

R

raise_unusable_proof() (proveit.Judgment method) RangeInstanceError readily_factorable() (in module proveit.numbers) readily_provable_number_set() (in module proveit.numbers) RealInterval (class in proveit.numbers) reduced() (proveit.logic.Set method) reduction() (proveit.logic.Set method) reference_hyperlinked_objects() (proveit.Theory method) relabeled() (proveit.Lambda method) relation_prover() (in module proveit) remake_arguments() (proveit.Conditional method) (proveit.Expression method) (proveit.ExprRange method) (proveit.ExprTuple method) (proveit.IndexedVar method) (proveit.Label method) (proveit.Lambda method) (proveit.Literal method) (proveit.NamedExprs method) (proveit.numbers.Add method) (proveit.numbers.Exp method) (proveit.numbers.Numeral method) (proveit.Operation method) remake_constructor() (proveit.Expression method) (proveit.logic.NotProperSubset method) (proveit.logic.NotSubsetEq method) (proveit.logic.ProperSubset method) (proveit.logic.SubsetEq method) (proveit.numbers.Add method) (proveit.numbers.Div method) (proveit.numbers.Exp method) (proveit.numbers.Less method) (proveit.numbers.LessEq method) remake_with_style_calls() (proveit.ExprArray method) (proveit.Expression method) (proveit.ExprRange method) (proveit.ExprTuple method) (proveit.logic.And method) (proveit.numbers.Add method) (proveit.Operation method) (proveit.OperationOverInstances method)

remove_common_factors() (in module proveit.numbers) remove_proof() (proveit.Theorem method) repl_lambda() (proveit.InnerExpr method) reset() (in module proveit) reversed() (proveit.logic.Equals method) (proveit.logic.NotEquals method) reversed_operator_str() (proveit.logic.InClass static method) (proveit.logic.NotProperSubset static method) (proveit.logic.NotSubsetEq static method) (proveit.logic.ProperSubset static method) (proveit.logic.SubsetEq static method) (proveit.numbers.Less static method) (proveit.numbers.LessEq static method) right_add_both_sides() (proveit.numbers.Less method) (proveit.numbers.LessEq method) right_mult_both_sides() (proveit.numbers.Less method) (proveit.numbers.LessEq method) Round (class in proveit.numbers) rounding_eliminated() (proveit.numbers.Ceil method) (proveit.numbers.Floor method) (proveit.numbers.Round method) rounding_elimination() (proveit.numbers.Ceil method) (proveit.numbers.Floor method) (proveit.numbers.Round method) rounding_extracted() (proveit.numbers.Ceil method) (proveit.numbers.Floor method) (proveit.numbers.Round method) rounding_extraction() (proveit.numbers.Ceil method) (proveit.numbers.Floor method) (proveit.numbers.Round method)

S

safe_default_or_dummy_var() (in module proveit) safe_dummy_var() (in module proveit) (proveit.Expression method) safe_dummy_vars() (in module proveit) (proveit.Expression method) Set (class in proveit.logic) set_active_folder() (proveit.Theory method) set_sub_theory_names() (proveit.Theory method) SetEquiv (class in proveit.logic) SetMembership (class in proveit.logic) SetNonmembership (class in proveit.logic) SetNotEquiv (class in proveit.logic) SetOfAll (class in proveit.logic) shallow_simplification() (proveit.logic.InClass method) (proveit.logic.NotInClass method) (proveit.numbers.BinarySequence method) shallow_simplified() (proveit.logic.InClass method) (proveit.logic.NotInClass method) (proveit.numbers.BinarySequence method) shift_equivalence() (proveit.ExprRange method) side_effects() (proveit.Expression method) (proveit.logic.And method) (proveit.logic.ClassMembership method) (proveit.logic.ClassNonmembership method) (proveit.logic.Equals method) (proveit.logic.Exists method) (proveit.logic.Forall method) (proveit.logic.Iff method) (proveit.logic.Implies method) (proveit.logic.InClass method) (proveit.logic.InSet method) (proveit.logic.Not method) (proveit.logic.NotEquals method) (proveit.logic.NotExists method) (proveit.logic.NotInClass method) (proveit.logic.NotInSet method) (proveit.logic.NotProperSubset method) (proveit.logic.NotSubsetEq method) (proveit.logic.Or method) (proveit.logic.SetEquiv method) (proveit.logic.SetNotEquiv method) (proveit.numbers.NumberOrderingRelation method) (proveit.TransitiveRelation method) simplification() (proveit.core_expr_types.Len method) (proveit.Expression method) SimplificationDirectives (class in proveit) SimplificationError simplified() (proveit.Expression method) (proveit.numbers.Sum method) simplified_index() (in module proveit) simplified_indices() (in module proveit) simplified_numeric_rational() (in module proveit.numbers) single_bit_reduced() (proveit.numbers.BinarySequence method) single_bit_reduction() (proveit.numbers.BinarySequence method) single_elem_substitution() (proveit.logic.Set method) single_or_composite_expression() (in module proveit) skip_over_branch() (proveit.InnerExprGenerator method) skolem_consts_to_existential (proveit.logic.Exists attribute) sort() (proveit.TransitiveRelation class method) sorted_items() (proveit.TransitiveRelation class method) special_expr_kind_to_module_name (proveit.Theory attribute) sqrd() (in module proveit.numbers) sqrt() (in module proveit.numbers) square_both_sides() (proveit.numbers.NumberOrderingRelation method) square_root_both_sides() (proveit.numbers.NumberOrderingRelation method) standard_number_set() (in module proveit.numbers) standardized_styles() (proveit.StyleOptions method) start_indices() (proveit.ExprRange method) stash_extraneous_thm_proof_notebooks() (proveit.Theory method) step_type() (proveit.Assumption method) (proveit.Axiom method) (proveit.Deduction method) (proveit.Generalization method) (proveit.Instantiation method) (proveit.ModusPonens method) (proveit.Theorem method)

storages (proveit.Theory attribute) stored_common_expr_dependencies() (proveit.Theory method) StrictSubset (in module proveit.logic) string() (proveit.Conditional method) (proveit.ConditionalSet method) (proveit.core_expr_types.Len method) (proveit.ExprArray method) (proveit.Expression method) (proveit.ExprRange method) (proveit.ExprTuple method) (proveit.Judgment method) (proveit.Label method) (proveit.Lambda method) (proveit.logic.Card method) (proveit.logic.CartExp method) (proveit.logic.Functions method) (proveit.logic.Image method) (proveit.logic.InvImage method) (proveit.logic.Set method) (proveit.NamedExprs method) (proveit.numbers.Abs method) (proveit.numbers.Conjugate method) (proveit.numbers.Exp method) (proveit.numbers.Interval method) (proveit.numbers.IntervalCC method) (proveit.numbers.IntervalCO method) (proveit.numbers.IntervalOC method) (proveit.numbers.IntervalOO method) (proveit.numbers.KroneckerDelta method) (proveit.numbers.Log method) (proveit.numbers.ModAbs method) (proveit.numbers.Neg method) (proveit.Operation method) (proveit.OperationOverInstances method) StrongRelationClass() (proveit.logic.Equals class method) (proveit.logic.Implies static method) (proveit.numbers.NumberOrderingRelation static method) (proveit.TransitiveRelation static method) style_names() (proveit.Expression method) style_options() (proveit.Conditional method) (proveit.ExprArray method) (proveit.Expression method) (proveit.ExprRange method) (proveit.ExprTuple method) (proveit.Function method) (proveit.Label method) (proveit.logic.And method) (proveit.numbers.Add method) (proveit.numbers.Div method) (proveit.numbers.Exp method) (proveit.Operation method) (proveit.OperationOverInstances method) StyleOptions (class in proveit) sub_expr() (proveit.Expression method) sub_expr_iter() (proveit.Expression method) sub_left_side_into() (proveit.logic.Equals method) (proveit.logic.SetEquiv method) sub_right_side_into() (proveit.logic.Equals method) (proveit.logic.SetEquiv method) SubsetEq (class in proveit.logic) SubsetProper (in module proveit.logic) substitute() (proveit.InnerExpr method) substitute_domain() (proveit.logic.Exists method) substitute_falsehood() (proveit.logic.Not method) substitute_in_false() (proveit.logic.Not method) substitute_instances() (proveit.logic.Exists method) substitution() (proveit.InnerExpr method) (proveit.logic.Equals method) subtract() (in module proveit.numbers) subtraction_folding() (proveit.numbers.Add method) Sum (class in proveit.numbers) superset_eq() (in module proveit.logic) Surjections (class in proveit.logic) swapped() (proveit.logic.Set method)

T

temporary() (proveit.SimplificationDirectives method) Theorem (class in proveit) theorem_being_proven (proveit.Judgment attribute) theorem_name_and_containing_theories() (proveit.Theorem method) Theory (class in proveit) TheoryException TheoryPackage (class in proveit) thm_proof_notebook() (proveit.Theory method)

total_ordering() (in module proveit) TransitiveRelation (class in proveit) TransitivityException TransRelUpdater (class in proveit) traverse_inner_expressions() (in module proveit) trivial_disjunctions (proveit.logic.Or attribute) TrueLiteral (class in proveit.logic) typical_eq() (proveit.core_expr_types.Len method)

U

unary_reduction() (proveit.logic.And method) (proveit.logic.Or method) unbundle() (in module proveit) (proveit.logic.Forall method) unbundle_equality() (proveit.logic.Forall method) unfold() (proveit.logic.Exists method) (proveit.logic.Forall method) (proveit.logic.NotEquals method) (proveit.logic.NotExists method) (proveit.logic.NotProperSubset method) (proveit.logic.NotSubsetEq method) (proveit.logic.ProperSubset method) (proveit.logic.SetEquiv method) (proveit.logic.SetNotEquiv method) (proveit.logic.SubsetEq method) (proveit.numbers.LessEq method) unfold_forall() (proveit.logic.BooleanSet method) unfold_not_in() (proveit.logic.NotInClass method) (proveit.logic.NotInSet method)

Union (class in proveit.logic) union_number_set() (in module proveit.numbers) UnionAll (class in proveit.logic) UniqueExists (class in proveit.logic) unit_length_complex_polar_angle() (in module proveit.numbers) UnsatisfiedPrerequisites UnusableProof update() (proveit.TransRelUpdater method) update_proving_name_if_needed() (proveit.Theory static method) update_title_if_needed() (proveit.Theory static method) update_usability() (proveit.Theorem static method) used_axioms() (proveit.Axiom method) (proveit.Proof method) used_literals() (in module proveit) used_theorems() (proveit.Proof method) (proveit.Theorem method) used_vars() (in module proveit)

V

values() (proveit.NamedExprs method) var_array() (in module proveit) var_range() (in module proveit)

Variable (class in proveit) vert_var_array() (in module proveit) VertExprArray (class in proveit)

W

WeakRelationClass() (proveit.logic.Equals class method) (proveit.logic.Implies static method) (proveit.numbers.NumberOrderingRelation static method) (proveit.TransitiveRelation static method) with_comma_delimiter() (proveit.Conditional method) with_conjunction_delimiter() (proveit.Conditional method) with_default_parameterization_style() (proveit.ExprRange method) with_default_style() (proveit.Expression method) with_explicit_parameterization() (proveit.ExprRange method) with_fraction_style() (proveit.numbers.Div method) with_implicit_parameterization() (proveit.ExprRange method) with_inline_style() (proveit.numbers.Div method) with_justification() (proveit.ExprArray method) (proveit.ExprTuple method) (proveit.Operation method) (proveit.OperationOverInstances method)

with_matching_style() (proveit.Expression method) with_matching_styles() (proveit.Judgment method) with_mimicked_style() (proveit.Expression method) with_radical() (proveit.numbers.Exp method) with_styles() (proveit.Expression method) with_total_ordering_style() (proveit.logic.And method) with_wrap_after_operator() (proveit.Operation method) with_wrap_before_operator() (proveit.Operation method) with_wrapping() (proveit.OperationOverInstances method) with_wrapping_at() (proveit.ExprTuple method) (proveit.Operation method) without_radical() (proveit.numbers.Exp method) wrap_params() (proveit.OperationOverInstances method) wrap_positions() (proveit.ExprTuple method) (proveit.Operation method)

Y

yield_known_memberships() (proveit.logic.InClass static method)

Z

zero_elimination() (proveit.numbers.Add method)

zero_eliminations() (proveit.numbers.Add method)