|
(derivatives_alt
(derivative_equivalence1_TCC1 0
(derivative_equivalence1_TCC1-1 nil 3297598424
("" (skosimp*)
(("" (lemma "deriv_domain")
(("" (expand "deriv_domain?") (("" (inst?) nil nil)) nil)) nil))
nil)
((deriv_domain formula-decl nil derivatives_alt nil)) nil))
(derivative_equivalence1_TCC2 0
(derivative_equivalence1_TCC2-1 nil 3297598424
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil derivatives_alt nil)) nil))
(derivative_equivalence1 0
(derivative_equivalence1-1 nil 3297598424
("" (skolem!)
(("" (rewrite "convergence_equiv[(A[T](x!1))]")
(("" (expand "derivable?")
(("" (expand "deriv") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((convergence_equiv formula-decl nil lim_of_functions nil)
(NQ const-decl "real" derivatives_def 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_alt nil)
(T formal-subtype-decl nil derivatives_alt nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(deriv const-decl "real" derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil))
nil))
(derivative_equivalence2 0
(derivative_equivalence2-2 nil 3320060683
(""
(grind :exclude ("abs" "adh") :rewrites
("deriv_TCC[T]" "adherence_fullset[T]") :if-match nil)
(("1"
(inst 1
"LAMBDA y : IF y=x!1 THEN 0 ELSE NQ(f!1, x!1)(y - x!1) - D!1 ENDIF")
(("1" (split)
(("1" (assert)
(("1" (skolem!)
(("1" (inst -3 "epsilon!1")
(("1" (skolem!)
(("1" (inst 1 "delta!1")
(("1" (skosimp)
(("1" (lift-if)
(("1" (ground)
(("1" (inst -4 "x!2 - x!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (delete -)
(("2" (grind)
(("2" (auto-rewrite "times_div2" "div_distributes_minus")
(("2" (assert)
(("2" (use "div_cancel3" ("y" "f!1(y!1) - f!1(x!1)"))
(("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp) (("2" (assert) nil nil)) nil))
nil)
("2" (inst? -5)
(("2" (skolem!)
(("2" (inst 1 "delta!1")
(("2" (skosimp :preds? t)
(("2" (assert)
(("2" (inst -7 "x!1 + x2!1")
(("2" (inst -8 "x!1+x2!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(x!1 skolem-const-decl "T" derivatives_alt nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(div_cancel3 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(div_distributes_minus formula-decl nil real_props nil)
(times_div2 formula-decl nil real_props nil)
(abs_nat formula-decl nil abs_lems "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_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)
(adherence_fullset formula-decl nil lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergence const-decl "bool" convergence_functions nil)
(NQ const-decl "real" derivatives_def nil)
(fullset const-decl "set" sets nil)
(deriv_TCC formula-decl nil derivatives_def 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)
(T_pred const-decl "[real -> boolean]" derivatives_alt nil)
(T formal-subtype-decl nil derivatives_alt nil))
nil)
(derivative_equivalence2-1 nil 3297598424
(""
(grind :exclude ("abs" "adh") :rewrites
("deriv_TCC[T]" "adherence_fullset[T]") :if-match nil)
(("1"
(inst 1
"LAMBDA y : IF y=x!1 THEN 0 ELSE NQ(f!1, x!1)(y - x!1) - D!1 ENDIF")
(("1" (split)
(("1" (assert)
(("1" (skolem!)
(("1" (inst -3 "epsilon!1")
(("1" (skolem!)
(("1" (inst 1 "delta!1")
(("1" (skosimp)
(("1" (lift-if)
(("1" (ground)
(("1" (expand "abs" +) (("1" (assert) nil nil))
nil)
("2" (inst -4 "x!2 - x!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (delete -)
(("2" (grind)
(("2" (auto-rewrite "times_div2" "div_distributes_minus")
(("2" (assert)
(("2" (use "div_cancel3" ("y" "f!1(y!1) - f!1(x!1)"))
(("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp) (("2" (assert) nil nil)) nil))
nil)
("2" (inst? -5)
(("2" (skolem!)
(("2" (inst 1 "delta!1")
(("2" (skosimp :preds? t)
(("2" (assert)
(("2" (inst -7 "x!1 + x!2")
(("2" (inst -8 "x!1+x!2") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((adherence_fullset formula-decl nil lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergence const-decl "bool" convergence_functions nil))
nil))
(derivative_equivalence3 0
(derivative_equivalence3-1 nil 3297611159
("" (skolem 1 ("D" "f" "x"))
(("" (lemma "derivative_equivalence1" ("f" "f" "D" "D" "x" "x"))
(("" (replace -1 1)
(("" (hide -1)
((""
(lemma "derivative_equivalence2" ("f" "f" "D" "D" "x" "x"))
(("" (replace -1 1)
(("" (hide -1)
(("" (split)
(("1" (flatten)
(("1" (skolem!)
(("1" (flatten -1)
(("1" (inst + "LAMBDA (z:T): D+phi!1(z)")
(("1" (split 1)
(("1" (expand "convergence")
(("1"
(expand "fullset")
(("1"
(expand "convergence")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst + "LAMBDA (z:T): psi!1(z) - D")
(("2" (split 1)
(("1" (expand "convergence")
(("1" (expand "convergence")
(("1" (propax) nil nil)) nil))
nil)
("2" (skosimp*)
(("2" (inst - "y!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-subtype-decl nil derivatives_alt nil)
(T_pred const-decl "[real -> boolean]" derivatives_alt 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)
(derivative_equivalence1 formula-decl nil derivatives_alt nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(convergence const-decl "bool" lim_of_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_functions nil)
(fullset const-decl "set" sets nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(derivative_equivalence2 formula-decl nil derivatives_alt nil))
nil))
(epsi_eq_0 0
(epsi_eq_0-1 nil 3297599282
("" (skosimp*)
(("" (prop)
(("1" (inst - "abs(x!1)/2")
(("1" (assert) nil nil)
("2" (assert)
(("2" (mult-by 1 "2")
(("2" (assert)
(("2" (lemma "abs_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (replace -1) (("2" (skosimp*) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types 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)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(T_pred const-decl "[real -> boolean]" derivatives_alt nil)
(T formal-subtype-decl nil derivatives_alt nil)
(x!1 skolem-const-decl "T" derivatives_alt nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil))
shostak))
(derivative_squeeze 0
(derivative_squeeze-2 nil 3297609645
("" (skosimp*)
(("" (case "adh[(A[T](x!1))](fullset[real])(0)")
(("1" (prop)
(("1"
(case "convergence[(A(x!1))](const_fun(fp!1(x!1)),0,fp!1(x!1))")
(("1" (lemma "cv_diff[(A(x!1))]")
(("1" (hide -2)
(("1" (inst?)
(("1" (reveal -2)
(("1" (inst?)
(("1" (assert)
(("1" (hide -1 -3)
(("1" (expand "const_fun")
(("1" (assert)
(("1" (inst?)
(("1"
(assert)
(("1"
(expand "-")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "convergence")
(("2" (rewrite "convergence_const[(A(x!1))]") nil nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (replace -2)
(("2" (hide -2)
(("2" (lemma "cv_sum[(A(x!1))]")
(("2" (inst?)
(("2" (inst - "const_fun(fp!1(x!1))" "fp!1(x!1)")
(("2" (assert)
(("2" (lemma "cv_const[(A(x!1))]")
(("2" (inst?)
(("2" (assert)
(("2" (hide -1 -3)
(("2"
(expand "const_fun")
(("2"
(expand "+")
(("2"
(assert)
(("2"
(case-replace
"(LAMBDA (x_1: ((A(x!1)))): NQ(f!1, x!1)(x_1)) = NQ(f!1, x!1)")
(("2"
(apply-extensionality
1
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (rewrite "adh_A_lem") nil nil))
nil))
nil))
nil)
((fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(adh const-decl "setof[real]" convergence_functions nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_alt nil)
(T_pred const-decl "[real -> boolean]" derivatives_alt nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(setof type-eq-decl nil defined_types 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(cv_const formula-decl nil lim_of_functions nil)
(cv_sum formula-decl nil lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(constant_seq1 application-judgement "(convergent?)"
convergence_ops nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil)
(derivable_const application-judgement "deriv_fun" derivatives nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(NQ const-decl "real" derivatives_def nil)
(cv_diff formula-decl nil lim_of_functions nil)
(convergence_const formula-decl nil convergence_functions nil)
(adh_A_lem formula-decl nil derivatives_def nil))
nil)
(derivative_squeeze-1 nil 3297598473
("" (skosimp*)
(("" (prop)
(("1" (expand "NQ")
(("1" (inst + "const_fun(0)")
(("1" (skosimp*)
(("1" (expand "const_fun")
(("1" (prop)
(("1" (postpone) nil nil)
("2" (lemma "epsi_eq_0")
(("2" (inst?)
(("1" (assert)
(("1" (hide 2)
(("1" (skosimp*)
(("1" (expand "convergence")
(("1" (expand "convergence")
(("1"
(flatten)
(("1"
(inst - "epsi!1")
(("1"
(skosimp*)
(("1"
(inst - "h!1")
(("1"
(assert)
(("1"
(hide 1)
(("1"
(expand "fullset")
(("1"
(typepred "h!1")
(("1"
(expand "A")
(("1"
(expand "adh")
(("1"
(flatten)
(("1"
(postpone)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil) ("3" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil)
nil shostak))
(derivative_squeeze_delta 0
(derivative_squeeze_delta-1 nil 3299421827
("" (skosimp*)
(("" (prop)
(("1" (lemma "derivative_squeeze")
(("1" (inst?)
(("1" (replace -2)
(("1" (flatten)
(("1" (skosimp*)
(("1" (inst + "abs(HH!1)")
(("1" (assert)
(("1" (rewrite "conv_0_0_abs")
(("1" (assert)
(("1" (replace -2)
(("1" (assert)
(("1" (inst + "1")
(("1"
(skosimp*)
(("1"
(expand "abs" 1 2)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lemma "derivative_squeeze")
(("2" (inst?)
(("2" (assert)
(("2"
(inst +
"(LAMBDA (h: (A(x!1))): (NQ(f!1, x!1)(h) - fp!1(x!1)))")
(("2" (hide 2)
(("2" (expand "convergence")
(("2" (expand "convergence")
(("2" (flatten)
(("2" (assert)
(("2" (skosimp*)
(("2" (inst -2 "epsilon!1")
(("2"
(skosimp*)
(("2"
(inst + "min(delta!1,delta!2)")
(("2"
(skosimp*)
(("2"
(inst -5 "x!2")
(("2"
(inst -4 "x!2")
(("2"
(assert)
(("2"
(hide -1 -2 -3)
(("2"
(name-replace
"DD"
"NQ(f!1, x!1)(x!2) - fp!1(x!1)")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(T_pred const-decl "[real -> boolean]" derivatives_alt nil)
(T formal-subtype-decl nil derivatives_alt nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(conv_0_0_abs formula-decl nil lim_of_functions nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(derivative_squeeze formula-decl nil derivatives_alt nil)
(convergence const-decl "bool" convergence_functions nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(convergence const-decl "bool" lim_of_functions nil)
(NQ const-decl "real" derivatives_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(deriv_constant1 0
(deriv_constant1-1 nil 3297598424
("" (skosimp)
(("" (auto-rewrite "deriv_TCC[T]" "A[T]")
(("" (expand "convergence")
((""
(lemma "convergence_locally_constant"
("f" "NQ(f!1, c!1)" "E"
"{x:real| abs(x) < min(c!1 - a!1, b!1 - c!1)}" "b" "0" "a"
"0"))
(("1" (ground)
(("1"
(grind :exclude ("min" "abs" "NQ" "adh") :if-match nil)
(("1" (inst? -4)
(("1" (skolem!)
(("1"
(inst 1 "min(delta!1, min(c!1 - a!1, b!1 - c!1))")
(("1" (skosimp)
(("1" (inst? -4) (("1" (assert) nil nil)) nil))
nil)
("2" (delete -3 -4 -7)
(("2" (expand "min") (("2" (smash) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (delete 2)
(("2" (skosimp :preds? t)
(("2" (assert)
(("2" (inst -5 "c!1 + x!1") (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (delete -3 2)
(("2" (lemma "deriv_TCC[T]" ("x" "c!1"))
(("2" (grind :exclude ("abs" "min") :if-match nil)
(("2" (inst -3 "min(e!1, min(c!1 - a!1, b!1 - c!1))")
(("1" (skosimp)
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (delete 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil derivatives_alt nil)
(T_pred const-decl "[real -> boolean]" derivatives_alt nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(adh const-decl "setof[real]" convergence_functions nil)
(NQ const-decl "real" derivatives_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals 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)
(>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(convergence_locally_constant formula-decl nil
convergence_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(fullset const-decl "set" sets nil)
(deriv_TCC formula-decl nil derivatives_def nil)
(convergence const-decl "bool" convergence_functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(b!1 skolem-const-decl "T" derivatives_alt nil)
(a!1 skolem-const-decl "T" derivatives_alt nil)
(c!1 skolem-const-decl "T" derivatives_alt nil)
(delta!1 skolem-const-decl "posreal" derivatives_alt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(e!1 skolem-const-decl "posreal" derivatives_alt nil)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(deriv_constant2 0
(deriv_constant2-1 nil 3297598424
("" (skosimp)
(("" (rewrite "derivative_equivalence1")
(("" (forward-chain "deriv_constant1") nil nil)) nil))
nil)
((derivative_equivalence1 formula-decl nil derivatives_alt 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)
(T_pred const-decl "[real -> boolean]" derivatives_alt nil)
(T formal-subtype-decl nil derivatives_alt nil)
(deriv_constant1 formula-decl nil derivatives_alt nil))
nil)))
¤ Dauer der Verarbeitung: 0.49 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
