(lebesgue_fundamental
(IMP_fundamental_theorem_TCC1 0
(IMP_fundamental_theorem_TCC1-1
nil 3452514920 (
"" (
assert)
nil nil)
((real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil))
nil))
(IMP_fundamental_theorem_TCC2 0
(IMP_fundamental_theorem_TCC2-1
nil 3452514920
(
"" (
expand "connected?")
((
"" (skosimp*)
((
"" (typepred
"x!1")
((
"" (typepred
"y!1")
((
"" (
expand "closed")
((
"" (
expand "closed_ball") ((
"" (grind)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_plus_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(real nonempty-type-from-decl
nil reals
nil)
(number nonempty-type-decl
nil numbers
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(<= const-decl
"bool" reals
nil) (
set type-eq-decl
nil sets
nil)
(>= const-decl
"bool" reals
nil)
(nnreal type-eq-decl
nil real_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(setof type-eq-decl
nil defined_types
nil)
(setofsets type-eq-decl
nil sets
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(metric_induced_topology const-decl
"setofsets[T]" metric_space_def
"metric_space/")
(closed? const-decl
"bool" topology
"topology/")
(closed nonempty-type-eq-decl
nil topology
"topology/")
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(closed_interval nonempty-type-eq-decl
nil real_topology
"metric_space/")
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(a formal-const-decl
"real" lebesgue_fundamental
nil)
(< const-decl
"bool" reals
nil)
(b formal-const-decl
"{x: real | a < x}" lebesgue_fundamental
nil)
(connected? const-decl
"bool" deriv_domain_def
"analysis/"))
nil))
(IMP_fundamental_theorem_TCC3 0
(IMP_fundamental_theorem_TCC3-1
nil 3452514920
(
"" (
expand "not_one_element?")
((
"" (skosimp)
((
"" (typepred
"x!1")
((
"" (
case "x!1=a")
((
"1" (inst +
"b")
((
"1" (
assert)
nil nil)
(
"2" (hide -2) ((
"2" (grind)
nil nil))
nil))
nil)
(
"2" (inst +
"a")
((
"1" (
assert)
nil nil)
(
"2" (hide -1 2) ((
"2" (grind)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(closed_is_measurable application-judgement
"measurable_set"
lebesgue_def
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(real nonempty-type-from-decl
nil reals
nil)
(number nonempty-type-decl
nil numbers
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(<= const-decl
"bool" reals
nil) (
set type-eq-decl
nil sets
nil)
(>= const-decl
"bool" reals
nil)
(nnreal type-eq-decl
nil real_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(setof type-eq-decl
nil defined_types
nil)
(setofsets type-eq-decl
nil sets
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(metric_induced_topology const-decl
"setofsets[T]" metric_space_def
"metric_space/")
(closed? const-decl
"bool" topology
"topology/")
(closed nonempty-type-eq-decl
nil topology
"topology/")
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(closed_interval nonempty-type-eq-decl
nil real_topology
"metric_space/")
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(a formal-const-decl
"real" lebesgue_fundamental
nil)
(< const-decl
"bool" reals
nil)
(b formal-const-decl
"{x: real | a < x}" lebesgue_fundamental
nil)
(not_one_element? const-decl
"bool" deriv_domain_def
"analysis/"))
nil))
(IMP_fundamental_theorem_TCC4 0
(IMP_fundamental_theorem_TCC4-1
nil 3452518094
(
"" (inst +
"a") ((
"" (grind)
nil nil))
nil)
((real_minus_real_is_real application-judgement
"real" reals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(b formal-const-decl
"{x: real | a < x}" lebesgue_fundamental
nil)
(< const-decl
"bool" reals
nil)
(a formal-const-decl
"real" lebesgue_fundamental
nil)
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(closed_interval nonempty-type-eq-decl
nil real_topology
"metric_space/")
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(closed nonempty-type-eq-decl
nil topology
"topology/")
(closed? const-decl
"bool" topology
"topology/")
(metric_induced_topology const-decl
"setofsets[T]" metric_space_def
"metric_space/")
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(setofsets type-eq-decl
nil sets
nil)
(setof type-eq-decl
nil defined_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(nnreal type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil) (
set type-eq-decl
nil sets
nil)
(<= const-decl
"bool" reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(real nonempty-type-from-decl
nil reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number nonempty-type-decl
nil numbers
nil)
(closed_is_measurable application-judgement
"measurable_set"
lebesgue_def
nil))
nil))
(IMP_restriction_integral_TCC1 0
(IMP_restriction_integral_TCC1-1
nil 3452523885
(
"" (skosimp*)
((
"" (typepred
"x!1")
((
"" (typepred
"y!1") ((
"" (grind)
nil nil))
nil))
nil))
nil)
((b formal-const-decl
"{x: real | a < x}" lebesgue_fundamental
nil)
(< const-decl
"bool" reals
nil)
(a formal-const-decl
"real" lebesgue_fundamental
nil)
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(closed_interval nonempty-type-eq-decl
nil real_topology
"metric_space/")
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(closed nonempty-type-eq-decl
nil topology
"topology/")
(closed? const-decl
"bool" topology
"topology/")
(metric_induced_topology const-decl
"setofsets[T]" metric_space_def
"metric_space/")
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(setofsets type-eq-decl
nil sets
nil)
(setof type-eq-decl
nil defined_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(nnreal type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil) (
set type-eq-decl
nil sets
nil)
(<= const-decl
"bool" reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number nonempty-type-decl
nil numbers
nil)
(real nonempty-type-from-decl
nil reals
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(closed_is_measurable application-judgement
"measurable_set"
lebesgue_def
nil)
(minus_real_is_real application-judgement
"real" reals
nil))
nil))
(IMP_restriction_integral_TCC2 0
(IMP_restriction_integral_TCC2-1
nil 3452523885
(
"" (skosimp) ((
"" (inst +
"x!1+1") ((
"" (
assert)
nil nil))
nil))
nil)
nil nil))
(IMP_restriction_integral_TCC3 0
(IMP_restriction_integral_TCC3-2
nil 3477731956
(
"" (skosimp)
((
"" (typepred
"x!1")
((
"" (
case "x!1=a")
((
"1" (inst +
"b")
((
"1" (
assert)
nil nil)
(
"2" (hide -2) ((
"2" (grind)
nil nil))
nil))
nil)
(
"2" (inst +
"a")
((
"1" (
assert)
nil nil)
(
"2" (hide -1 2) ((
"2" (grind)
nil nil))
nil))
nil))
nil))
nil))
nil)
((b formal-const-decl
"{x: real | a < x}" lebesgue_fundamental
nil)
(< const-decl
"bool" reals
nil)
(a formal-const-decl
"real" lebesgue_fundamental
nil)
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(closed_interval nonempty-type-eq-decl
nil real_topology
"metric_space/")
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(closed nonempty-type-eq-decl
nil topology
"topology/")
(closed? const-decl
"bool" topology
"topology/")
(metric_induced_topology const-decl
"setofsets[T]" metric_space_def
"metric_space/")
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(setofsets type-eq-decl
nil sets
nil)
(setof type-eq-decl
nil defined_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(nnreal type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil) (
set type-eq-decl
nil sets
nil)
(<= const-decl
"bool" reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number nonempty-type-decl
nil numbers
nil)
(real nonempty-type-from-decl
nil reals
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(closed_is_measurable application-judgement
"measurable_set"
lebesgue_def
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(minus_real_is_real application-judgement
"real" reals
nil))
nil)
(IMP_restriction_integral_TCC3-1
nil 3452523885
(
"" (skosimp) ((
"" (inst +
"x!1")
nil nil))
nil)
((
set type-eq-decl
nil sets
nil)
(setofsets type-eq-decl
nil sets
nil)
(metric_induced_topology const-decl
"setofsets[T]" metric_space_def
"metric_space/")
(closed? const-decl
"bool" topology
"topology/")
(closed nonempty-type-eq-decl
nil topology
"topology/")
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(closed_interval nonempty-type-eq-decl
nil real_topology
"metric_space/")
(closed const-decl
"closed_interval" real_topology
"metric_space/"))
nil))
(IMP_restriction_integral_TCC4 0
(IMP_restriction_integral_TCC4-1
nil 3477673281
(
"" (skosimp*) ((
"" (inst +
"x!1+1") ((
"" (
assert)
nil nil))
nil))
nil)
((real_plus_real_is_real application-judgement
"real" reals
nil)
(number nonempty-type-decl
nil numbers
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(real nonempty-type-from-decl
nil reals
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil))
nil))
(IMP_restriction_integral_TCC5 0
(IMP_restriction_integral_TCC5-2
nil 3477731995
(
"" (skosimp*)
((
"" (typepred
"x!1") ((
"" (inst +
"x!1")
nil nil))
nil))
nil)
((b formal-const-decl
"{x: real | a < x}" lebesgue_fundamental
nil)
(< const-decl
"bool" reals
nil)
(a formal-const-decl
"real" lebesgue_fundamental
nil)
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(closed_interval nonempty-type-eq-decl
nil real_topology
"metric_space/")
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(closed nonempty-type-eq-decl
nil topology
"topology/")
(closed? const-decl
"bool" topology
"topology/")
(metric_induced_topology const-decl
"setofsets[T]" metric_space_def
"metric_space/")
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(setofsets type-eq-decl
nil sets
nil)
(setof type-eq-decl
nil defined_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(nnreal type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil) (
set type-eq-decl
nil sets
nil)
(<= const-decl
"bool" reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number nonempty-type-decl
nil numbers
nil)
(real nonempty-type-from-decl
nil reals
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil))
nil)
(IMP_restriction_integral_TCC5-1
nil 3477673281
(
"" (assuming-tcc)
nil nil)
nil nil))
(F_TCC1 0
(F_TCC1-1
nil 3603447121
(
"" (lemma
"deriv_domain") ((
"" (propax)
nil nil))
nil)
((deriv_domain formula-decl
nil fundamental_theorem
"analysis/")
(number nonempty-type-decl
nil numbers
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(real nonempty-type-from-decl
nil reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(<= const-decl
"bool" reals
nil) (
set type-eq-decl
nil sets
nil)
(>= const-decl
"bool" reals
nil)
(nnreal type-eq-decl
nil real_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(setof type-eq-decl
nil defined_types
nil)
(setofsets type-eq-decl
nil sets
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(metric_induced_topology const-decl
"setofsets[T]" metric_space_def
"metric_space/")
(closed? const-decl
"bool" topology
"topology/")
(closed nonempty-type-eq-decl
nil topology
"topology/")
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(closed_interval nonempty-type-eq-decl
nil real_topology
"metric_space/")
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(a formal-const-decl
"real" lebesgue_fundamental
nil)
(< const-decl
"bool" reals
nil)
(b formal-const-decl
"{x: real | a < x}" lebesgue_fundamental
nil))
nil))
(fundamental_lebesgue_TCC1 0
(fundamental_lebesgue_TCC1-1
nil 3452514920
(
"" (skosimp) ((
"" (hide -1 -2) ((
"" (grind)
nil nil))
nil))
nil)
((minus_real_is_real application-judgement
"real" reals
nil)
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(closed_is_measurable application-judgement
"measurable_set"
lebesgue_def
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil))
nil))
(fundamental_lebesgue_TCC2 0
(fundamental_lebesgue_TCC2-1
nil 3452514920
(
"" (skosimp) ((
"" (hide -1 -2) ((
"" (grind)
nil nil))
nil))
nil)
((closed_ball const-decl
"closed" real_topology
"metric_space/")
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(closed_is_measurable application-judgement
"measurable_set"
lebesgue_def
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil))
nil))
(fundamental_lebesgue 0
(fundamental_lebesgue-1
nil 3452515121
(
"" (skosimp*)
((
"" (typepred
"F!1")
((
"" (typepred
"f!1")
((
""
(lemma
"continuous_at_is_ae_continuous"
(
"a" "a" "b" "b" "f" "f!1"))
((
""
(lemma
"bounded_ae_continuous_integrable"
(
"a" "a" "b" "b" "f" "f!1"))
((
""
(lemma
"continuous_at_is_bounded"
(
"a" "a" "b" "b" "f" "f!1"))
((
"" (
assert)
((
"" (
assert)
((
""
(case-replace
"(FORALL x: a <= x AND x <= b => continuous_at?(f!1, x))")
((
"1" (split -4)
((
"1" (
assert)
((
"1" (hide -5)
((
"1"
(lemma
"riemann_integrable_def"
(
"a" "a" "b" "b" "f" "f!1"))
((
"1" (
assert)
((
"1"
(lemma
"fundamental3"
(
"F" "F!1" "f" "f!1" "a" "a" "b" "b"))
((
"1"
(
replace -8)
((
"1"
(
replace -7)
((
"1"
(split -1)
((
"1"
(flatten)
((
"1"
(
assert)
((
"1"
(hide -1 -2)
((
"1"
(
expand "restrict")
((
"1"
(lemma
"riemann_lebesgue_integral"
(
"a"
"a"
"b"
"b"
"f"
"f!1"))
((
"1"
(
assert)
((
"1"
(
replace -1 1 rl)
((
"1"
(case-replace
"(LAMBDA (s_1: real): f!1(s_1)) = f!1")
((
"1"
(lemma
"fundamental3[(closed(a, b))]"
(
"a"
"a"
"b"
"b"
"F"
"F!1"
"f"
"LAMBDA (s_1:(closed(a, b))): f!1(s_1)"))
((
"1"
(
replace -10)
((
"1"
(
replace
-9)
((
"1"
(split)
((
"1"
(flatten)
((
"1"
(lemma
"restrict_Integral")
((
"1"
(inst
-
"a"
"b"
"f!1")
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil)
(
"2"
(hide-all-but
(1
-5))
((
"2"
(
expand
"continuous?")
((
"2"
(skosimp)
((
"2"
(inst
-
"x0!1")
((
"2"
(typepred
"x0!1")
((
"2"
(split)
((
"1"
(
rewrite
"metric_continuous_at_def")
((
"1"
(
expand
"continuous?")
((
"1"
(
expand
"metric_continuous_at?")
((
"1"
(skosimp)
((
"1"
(inst
-
"epsilon!1")
((
"1"
(skosimp)
((
"1"
(inst
+
"delta!1")
((
"1"
(skosimp)
((
"1"
(typepred
"x!1")
((
"1"
(inst
-
"x!1")
((
"1"
(split)
((
"1"
(hide-all-but
(-1
1))
((
"1"
(grind)
nil
nil))
nil)
(
"2"
(hide-all-but
(-3
1))
((
"2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(hide
2)
((
"2"
(grind)
nil
nil))
nil)
(
"3"
(hide
2)
((
"3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(apply-extensionality
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(hide-all-but (-3 1))
((
"2"
(
expand "restrict")
((
"2"
(
assert)
((
"2"
(
expand "continuous?")
((
"2"
(skosimp)
((
"2"
(inst -
"x0!1")
((
"2"
(typepred
"x0!1")
((
"2"
(split -2)
((
"1"
(
rewrite
"metric_continuous_at_def")
((
"1"
(
expand
"continuous?")
((
"1"
(
expand
"metric_continuous_at?")
((
"1"
(skosimp)
((
"1"
(inst
-
"epsilon!1")
((
"1"
(skosimp)
((
"1"
(inst
+
"delta!1")
((
"1"
(skosimp)
((
"1"
(inst
-
"x!1")
((
"1"
(split)
((
"1"
(hide-all-but
(-1
1))
((
"1"
(grind)
nil
nil))
nil)
(
"2"
(hide-all-but
(-2
1))
((
"2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(hide 2)
((
"2"
(grind)
nil
nil))
nil)
(
"3"
(hide 2)
((
"3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (hide-all-but (-1 1))
((
"2" (skosimp)
((
"2" (inst -
"x!1") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2" (hide-all-but (-4 1))
((
"2" (
expand "continuous_on?")
((
"2" (skosimp)
((
"2" (inst -
"x!1")
((
"2" (hide 2) ((
"2" (grind)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_fun type-eq-decl
nil derivatives
"analysis/")
(derivable? const-decl
"bool" derivatives
"analysis/")
(b formal-const-decl
"{x: real | a < x}" lebesgue_fundamental
nil)
(< const-decl
"bool" reals
nil)
(a formal-const-decl
"real" lebesgue_fundamental
nil)
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(closed_interval nonempty-type-eq-decl
nil real_topology
"metric_space/")
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(closed nonempty-type-eq-decl
nil topology
"topology/")
(closed? const-decl
"bool" topology
"topology/")
(metric_induced_topology const-decl
"setofsets[T]" metric_space_def
"metric_space/")
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(setofsets type-eq-decl
nil sets
nil)
(setof type-eq-decl
nil defined_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(nnreal type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil) (
set type-eq-decl
nil sets
nil)
(<= const-decl
"bool" reals
nil)
(real nonempty-type-from-decl
nil reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number nonempty-type-decl
nil numbers
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(continuous_at_is_ae_continuous formula-decl
nil ae_continuous_def
nil)
(continuous_at_is_bounded formula-decl
nil riemann_link
nil)
(x!1 skolem-const-decl
"real" lebesgue_fundamental
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(restrict_Integral formula-decl
nil restriction_integral
nil)
(continuous? const-decl
"bool" continuous_functions
"analysis/")
(continuous? const-decl
"bool" continuous_functions
"analysis/")
(minus_real_is_real application-judgement
"real" reals
nil)
(member const-decl
"bool" sets
nil)
(ball const-decl
"set[T]" metric_space_def
"metric_space/")
(ball_is_metric_open application-judgement
"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]"
convergence_aux
"metric_space/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(> const-decl
"bool" reals
nil)
(posreal nonempty-type-eq-decl
nil real_types
nil)
(metric_continuous_at? const-decl
"bool" metric_continuity
"metric_space/")
(metric_continuous_at_def formula-decl
nil metric_continuity
"metric_space/")
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(riemann_lebesgue_integral formula-decl
nil riemann_link
nil)
(restrict const-decl
"R" restrict
nil)
(fundamental3 formula-decl
nil fundamental_theorem
"analysis/")
(riemann_integrable_def formula-decl
nil riemann_link
nil)
(IMPLIES const-decl
"[bool, bool -> bool]" booleans
nil)
(continuous_at? const-decl
"bool" continuity_def
"topology/")
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(closed_is_measurable application-judgement
"measurable_set"
lebesgue_def
nil)
(bounded_ae_continuous_integrable formula-decl
nil riemann_link
nil)
(continuous_on? const-decl
"bool" continuous_on
nil)
(continuous_on type-eq-decl
nil continuous_on
nil))
shostak))
(integration_by_parts_TCC1 0
(integration_by_parts_TCC1-1
nil 3476038809
(
"" (skosimp) ((
"" (hide-all-but 1) ((
"" (grind)
nil nil))
nil))
nil)
((minus_real_is_real application-judgement
"real" reals
nil)
(closed_ball const-decl
"closed" real_topology
"metric_space/")
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(closed_is_measurable application-judgement
"measurable_set"
lebesgue_def
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil))
nil))
(integration_by_parts_TCC2 0
(integration_by_parts_TCC2-1
nil 3476038809
(
"" (skosimp) ((
"" (hide-all-but 1) ((
"" (grind)
nil nil))
nil))
nil)
((closed_ball const-decl
"closed" real_topology
"metric_space/")
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(closed const-decl
"closed_interval" real_topology
"metric_space/")
(closed_is_measurable application-judgement
"measurable_set"
lebesgue_def
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil))
nil))
(integration_by_parts 0
(integration_by_parts-1
nil 3476040864
(
"" (skosimp)
((
"" (name
"H" "real_fun_ops.*(F!1,G!1)")
((
"1" (lemma
"prod_derivable_fun" (
"f1" "F!1" "f2" "G!1"))
((
"1" (split)
((
"1" (lemma
"deriv_prod_fun" (
"ff1" "F!1" "ff2" "G!1"))
((
"1" (lemma
"fundamental_lebesgue" (
"F" "H"))
((
"1" (
replace -4)
((
"1" (
replace -2)
((
"1" (
replace -5)
((
"1" (
replace -6)
((
"1" (hide -4 -5 -6)
((
"1" (hide -3 -2)
((
"1" (
expand "H" -)
((
"1" (
expand "*" - 3)
((
"1"
(
expand "*" - 4)
((
"1"
(
expand "restrict" -)
((
"1"
(
expand "*" - 1)
((
"1"
(
expand "+" - 1)
((
"1"
(
assert)
((
"1"
(
expand "*" - 1)
((
"1"
(typepred
"f!1")
((
"1"
(typepred
"g!1")
((
"1"
(lemma
"derivable_cont_fun[(closed(a, b))]")
((
"1"
(inst-cp -
"F!1")
((
"1"
(inst -
"G!1")
((
"1"
(
assert)
((
"1"
(name
"CE"
"lambda (f:[real->real]): lambda x: if x)
(("1"
(hide -1)
(("1"
(case
"FORALL (f:[real->real]): (forall x: closed(a,b)(x) => continuous_at?(f,x)) => continuity_def.continuous?(CE(f))")
(("1"
(case
"FORALL (f:[real->real],x): closed(a, b)(x) => CE(f)(x) = f(x)")
(("1"
(name-replace
"FF"
"extend[real, (closed(a, b)), real, 0](F!1)")
(("1"
(name-replace
"GG"
"extend[real, (closed(a, b)), real, 0](G!1)")
(("1"
(inst-cp
-
"f!1")
(("1"
(inst-cp
-
"g!1")
(("1"
(split)
(("1"
(split)
(("1"
(inst-cp
-
"g!1"
"_")
(("1"
(inst-cp
-
"f!1"
"_")
(("1"
(hide
-6)
(("1"
(case
"continuity_def.continuous?(CE(GG)*CE(f!1))")
(("1"
(case
"continuity_def.continuous?(CE(FF)*CE(g!1))")
(("1"
(case
"continuity_def.continuous?((CE(FF)*CE(g!1)) + (CE(GG)*CE(f!1)))")
(("1"
(inst
-13
"(CE(FF) * CE(g!1)) + (CE(GG) * CE(f!1))")
(("1"
(split
-13)
(("1"
(flatten)
(("1"
(lemma
"continuous_is_integrable"
("a"
"a"
"b"
"b"
"f"
"CE(GG) * CE(f!1)"))
(("1"
(lemma
"continuous_is_integrable"
("a"
"a"
"b"
"b"
"f"
"CE(FF) * CE(g!1)"))
(("1"
(assert)
(("1"
(rewrite
"indefinite_add"
-4)
(("1"
(expand
"integral"
(1
-4))
(("1"
(expand
"integrable?"
(1
-1
-2))
(("1"
(expand
"*")
(("1"
(hide-all-but
(-1
-2
-3
-4
1))
(("1"
(expand
"phi")
(("1"
(expand
"member")
(("1"
(case-replace
"(LAMBDA (x_1: real):
IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF *
(CE(FF)(x_1) * CE(g!1)(x_1)))=(LAMBDA (x_1: real):
IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF *
(FF(x_1) * g!1(x_1)))")
(("1"
(replace
-2)
(("1"
(hide
-1)
(("1"
(case-replace
"(LAMBDA (x_1: real):
IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF *
(CE(GG)(x_1) * CE(f!1)(x_1)))=(LAMBDA (x_1: real):
IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF *
(GG(x_1) * f!1(x_1)))")
(("1"
(hide
-1)
(("1"
--> --------------------
--> maximum size reached
--> --------------------
