|
(nth_derivatives
(derivable_n_times?_TCC1 0
(derivable_n_times?_TCC1-1 nil 3445338281
("" (skosimp*)
(("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)) nil)
((deriv_domain formula-decl nil nth_derivatives nil)) nil))
(derivable_n_times?_TCC2 0
(derivable_n_times?_TCC2-1 nil 3445338281
("" (skosimp*)
(("" (lemma "not_one_element") (("" (inst?) nil nil)) nil)) nil)
((not_one_element formula-decl nil nth_derivatives nil)) nil))
(derivable_n_times?_TCC3 0
(derivable_n_times?_TCC3-1 nil 3445338281 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(fullset const-decl "set" sets nil)
(adh const-decl "setof[real]" convergence_functions nil)
(NQ const-decl "real" derivatives_def nil)
(convergence const-decl "bool" convergence_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(derivable? const-decl "bool" derivatives_def nil)
(derivable? const-decl "bool" derivatives nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(derivable_n_times?_TCC4 0
(derivable_n_times?_TCC4-1 nil 3445338281
("" (termination-tcc) nil nil)
((fullset const-decl "set" sets nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(adh const-decl "setof[real]" convergence_functions nil)
(NQ const-decl "real" derivatives_def nil)
(convergence const-decl "bool" convergence_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(derivable? const-decl "bool" derivatives_def nil)
(derivable? const-decl "bool" derivatives nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(derivable_n_times_lem 0
(derivable_n_times_lem-1 nil 3255355367
("" (induct "n")
(("1" (skolem 1 ("f" "m"))
(("1" (lemma "trichotomy" ("x" "m"))
(("1" (split -1)
(("1" (assert) nil nil)
("2" (replace -1) (("2" (flatten) nil nil)) nil)
("3" (assert) nil nil))
nil))
nil))
nil)
("2" (skolem 1 ("j"))
(("2" (flatten)
(("2" (skolem 1 ("f" "m"))
(("2" (flatten)
(("2" (expand "<=" -3)
(("2" (split -3)
(("1" (inst - "f" "m")
(("1" (split -2)
(("1" (propax) nil nil)
("2" (hide -1 2)
(("2"
(case "FORALL (f:[T->real],k: nat): derivable_n_times?(f, k + 1) IMPLIES derivable_n_times?(f, k)")
(("1" (inst - "f" "j") (("1" (assert) nil nil))
nil)
("2" (hide -1 2)
(("2" (induct "k")
(("1" (expand "derivable_n_times?")
(("1" (propax) nil nil)) nil)
("2" (skolem 1 ("k"))
(("2"
(flatten)
(("2"
(skolem 1 ("g"))
(("2"
(flatten)
(("2"
(expand "derivable_n_times?" 1)
(("2"
(expand
"derivable_n_times?"
-2)
(("2"
(flatten -2)
(("2"
(assert)
(("2"
(inst - "deriv(g)")
(("1" (assert) nil nil)
("2"
(lemma
"not_one_element")
(("2"
(expand
"not_one_element?")
(("2"
(propax)
nil
nil))
nil))
nil)
("3"
(lemma "deriv_domain")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil)
("2" (replace -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(not_one_element formula-decl nil nth_derivatives nil)
(deriv_domain formula-decl nil nth_derivatives nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_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)
(trichotomy formula-decl nil real_axioms nil)
(nat_induction formula-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(T formal-subtype-decl nil nth_derivatives nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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))
nil))
(derivable_n_times_def_TCC1 0
(derivable_n_times_def_TCC1-1 nil 3298378055
("" (skosimp*)
(("" (lemma "derivable_n_times_lem")
(("" (inst - "f!1" "1" "n!1+1")
(("" (assert)
(("" (expand "derivable_n_times?") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((derivable_n_times_lem formula-decl nil nth_derivatives nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(T formal-subtype-decl nil nth_derivatives nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
shostak))
(derivable_n_times_def_TCC2 0
(derivable_n_times_def_TCC2-1 nil 3298378055
("" (lemma "deriv_domain") (("" (skosimp*) nil nil)) nil)
((deriv_domain formula-decl nil nth_derivatives nil)) shostak))
(derivable_n_times_def_TCC3 0
(derivable_n_times_def_TCC3-1 nil 3298378055
("" (lemma "not_one_element") (("" (skosimp*) nil nil)) nil)
((not_one_element formula-decl nil nth_derivatives nil)) shostak))
(derivable_n_times_def 0
(derivable_n_times_def-1 nil 3298378047
("" (skosimp*)
(("" (expand "derivable_n_times?" -1) (("" (flatten) nil nil))
nil))
nil)
((derivable_n_times? def-decl "bool" nth_derivatives nil)) shostak))
(nderiv_TCC1 0
(nderiv_TCC1-1 nil 3255355367 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives nil)
(T formal-subtype-decl nil nth_derivatives nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(nderiv_fun type-eq-decl nil nth_derivatives nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(nderiv_TCC2 0
(nderiv_TCC2-1 nil 3255355367
("" (skosimp*)
(("" (typepred "f!1")
(("" (expand "derivable_n_times?") (("" (ground) nil nil)) nil))
nil))
nil)
((nderiv_fun type-eq-decl nil nth_derivatives nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(T formal-subtype-decl nil nth_derivatives nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives 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))
nil))
(nderiv_TCC3 0
(nderiv_TCC3-1 nil 3255355367
("" (skosimp*)
(("" (typepred "f!1")
(("" (expand "derivable_n_times?" -1) (("" (ground) nil nil))
nil))
nil))
nil)
((nderiv_fun type-eq-decl nil nth_derivatives nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(T formal-subtype-decl nil nth_derivatives nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives 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))
nil))
(nderiv_TCC4 0
(nderiv_TCC4-1 nil 3255355367 ("" (termination-tcc) nil nil) nil
nil))
(nderiv_derivable_TCC1 0
(nderiv_derivable_TCC1-1 nil 3255355367
("" (skosimp*)
(("" (lemma "derivable_n_times_lem")
(("" (inst -1 "f!1" "m!1" "1+n!1") (("" (assert) nil nil)) nil))
nil))
nil)
((derivable_n_times_lem formula-decl nil nth_derivatives nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(T formal-subtype-decl nil nth_derivatives nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(nderiv_derivable_TCC2 0
(nderiv_derivable_TCC2-1 nil 3255355367
("" (skosimp*)
(("" (lemma "deriv_domain") (("" (inst?) nil nil)) nil)) nil)
((deriv_domain formula-decl nil nth_derivatives nil)) nil))
(nderiv_derivable_TCC3 0
(nderiv_derivable_TCC3-1 nil 3255355367
("" (skosimp*)
(("" (lemma "not_one_element") (("" (propax) nil nil)) nil)) nil)
((not_one_element formula-decl nil nth_derivatives nil)) nil))
(nderiv_derivable 0
(nderiv_derivable-1 nil 3255355367
("" (induct "m")
(("1" (expand "nderiv")
(("1" (expand "derivable_n_times?")
(("1" (assert) (("1" (skosimp*) nil nil)) nil)) nil))
nil)
("2" (skolem 1 ("j"))
(("2" (flatten)
(("2" (skolem 1 ("f" "n"))
(("2" (flatten 1)
(("2" (expand "<=" -2)
(("2" (split -2)
(("1" (expand "nderiv" 1)
(("1" (expand "derivable_n_times?" -3)
(("1" (flatten -3)
(("1" (inst - "deriv(f)" "n-1")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (lemma "not_one_element")
(("3" (expand "not_one_element?")
(("3" (propax) nil nil)) nil))
nil)
("4" (lemma "deriv_domain")
(("4" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "derivable_n_times?" -3)
(("2" (flatten -3)
(("2" (expand "nderiv" 1)
(("2" (inst - "deriv(f)" "n-1")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (lemma "not_one_element")
(("3" (expand "not_one_element?")
(("3" (propax) nil nil)) nil))
nil)
("4" (lemma "deriv_domain")
(("4" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skolem!)
(("3" (flatten 1)
(("3" (lemma "not_one_element")
(("3" (expand "not_one_element?") (("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("4" (lemma "deriv_domain")
(("4" (skolem! 1) (("4" (flatten 1) nil nil)) nil)) nil)
("5" (lemma "derivable_n_times_lem")
(("5" (hide 2)
(("5" (skosimp*)
(("5" (inst - "f!1" "m!2" "1+n!1") (("5" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((derivable_n_times_lem formula-decl nil nth_derivatives nil)
(deriv_domain formula-decl nil nth_derivatives nil)
(not_one_element formula-decl nil nth_derivatives nil)
(int_plus_int_is_int application-judgement "int" integers 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)
(deriv_fun type-eq-decl nil derivatives nil)
(deriv const-decl "[T -> real]" derivatives nil)
(n skolem-const-decl "nat" nth_derivatives nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(nderiv def-decl "[T -> real]" nth_derivatives nil)
(nderiv_fun type-eq-decl nil nth_derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(pred type-eq-decl nil defined_types nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(deriv_domain? const-decl "bool" deriv_domain_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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives nil)
(T formal-subtype-decl nil nth_derivatives nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(nderiv_derivable_aux_TCC1 0
(nderiv_derivable_aux_TCC1-1 nil 3255545563
("" (skosimp*) (("" (assert) nil nil)) nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
shostak))
(nderiv_derivable_aux_TCC2 0
(nderiv_derivable_aux_TCC2-1 nil 3255545563
("" (skosimp*)
((""
(lemma "derivable_n_times_lem" ("f" "f!1" "n" "n!1+1" "m" "n!1"))
(("" (assert) nil nil)) nil))
nil)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(T formal-subtype-decl nil nth_derivatives nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives 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)
(derivable_n_times_lem formula-decl nil nth_derivatives nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(nderiv_derivable_aux_TCC3 0
(nderiv_derivable_aux_TCC3-1 nil 3255545563
("" (skosimp*)
(("" (lemma "nderiv_derivable" ("m" "n!1" "n" "n!1" "f" "f!1"))
(("" (assert) nil nil)) nil))
nil)
((nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(T formal-subtype-decl nil nth_derivatives nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives 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)
(nderiv_derivable formula-decl nil nth_derivatives nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
shostak))
(nderiv_derivable_aux 0
(nderiv_derivable_aux-1 nil 3255542603
("" (induct "n")
(("1" (expand "nderiv")
(("1" (expand "nderiv") (("1" (propax) nil nil)) nil)) nil)
("2" (skosimp*)
(("2" (expand "nderiv" 1 1)
(("2" (inst-cp - "deriv(f!1)")
(("1" (expand "derivable_n_times?" -3)
(("1" (flatten -3)
(("1" (assert)
(("1" (replace -2 1)
(("1" (expand "nderiv" 1 2) (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element")
(("2" (expand "not_one_element?") (("2" (propax) nil nil))
nil))
nil)
("3" (lemma "deriv_domain") (("3" (propax) nil nil)) nil))
nil))
nil))
nil)
("3" (skolem!)
(("3" (flatten 1)
(("3" (lemma "not_one_element")
(("3" (expand "not_one_element?") (("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("4" (lemma "deriv_domain")
(("4" (skolem!) (("4" (flatten 1) nil nil)) nil)) nil)
("5" (hide 2)
(("5" (skosimp*)
(("5"
(lemma "nderiv_derivable" ("f" "f!1" "n" "n!2" "m" "n!2"))
(("5" (assert) nil nil)) nil))
nil))
nil)
("6" (hide 2)
(("6" (skosimp*)
(("6"
(lemma "derivable_n_times_lem"
("f" "f!1" "n" "1+n!2" "m" "n!2"))
(("6" (assert) nil nil)) nil))
nil))
nil)
("7" (hide 2) (("7" (skosimp*) nil nil)) nil))
nil)
((derivable_n_times_lem formula-decl nil nth_derivatives nil)
(nderiv_derivable formula-decl nil nth_derivatives nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(not_one_element formula-decl nil nth_derivatives nil)
(deriv_domain formula-decl nil nth_derivatives nil)
(nat_induction formula-decl nil naturalnumbers nil)
(deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(derivable? const-decl "bool" derivatives nil)
(nderiv_fun type-eq-decl nil nth_derivatives nil)
(nderiv def-decl "[T -> real]" nth_derivatives 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives nil)
(T formal-subtype-decl nil nth_derivatives nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
shostak))
(nderiv_derivable_eqv_TCC1 0
(nderiv_derivable_eqv_TCC1-1 nil 3255550372
("" (lemma "deriv_domain")
(("" (replace -1) (("" (skosimp*) nil nil)) nil)) nil)
((deriv_domain formula-decl nil nth_derivatives nil)) shostak))
(nderiv_derivable_eqv_TCC2 0
(nderiv_derivable_eqv_TCC2-1 nil 3255550372
("" (lemma "not_one_element")
(("" (replace -1) (("" (skosimp*) nil nil)) nil)) nil)
((not_one_element formula-decl nil nth_derivatives nil)) shostak))
(nderiv_derivable_eqv 0
(nderiv_derivable_eqv-1 nil 3255548066
("" (induct "n")
(("1" (expand "nderiv")
(("1" (expand "derivable_n_times?")
(("1" (expand "derivable_n_times?") (("1" (propax) nil nil))
nil))
nil))
nil)
("2" (skolem 1 ("j"))
(("2" (flatten 1)
(("2" (skolem 1 ("f"))
(("2" (split 1)
(("1" (flatten)
(("1" (split 1)
(("1"
(lemma "derivable_n_times_lem"
("f" "f" "n" "j+2" "m" "j+1"))
(("1" (assert) nil nil)) nil)
("2" (inst - "deriv(f)")
(("1" (expand "derivable_n_times?" -1)
(("1" (flatten -1)
(("1" (assert)
(("1" (flatten -3)
(("1" (expand "nderiv" 1)
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element")
(("2" (expand "not_one_element?")
(("2" (propax) nil nil)) nil))
nil)
("3" (lemma "deriv_domain") (("3" (propax) nil nil))
nil)
("4" (expand "derivable_n_times?" -1)
(("4" (flatten) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (inst - "deriv(f)")
(("1" (flatten -3)
(("1" (expand "derivable_n_times?" 1)
(("1" (expand "derivable_n_times?" -1)
(("1" (flatten -1)
(("1" (replace -2)
(("1" (expand "nderiv" -3)
(("1" (replace -3) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element")
(("2" (expand "not_one_element?")
(("2" (propax) nil nil)) nil))
nil)
("3" (lemma "deriv_domain") (("3" (propax) nil nil))
nil)
("4" (expand "derivable_n_times?" -1)
(("4" (flatten -1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (lemma "not_one_element")
(("3" (skosimp*)
(("3" (expand "not_one_element?") (("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("4" (lemma "deriv_domain")
(("4" (replace -1) (("4" (skosimp*) nil nil)) nil)) nil))
nil)
((f skolem-const-decl "[T -> real]" nth_derivatives nil)
(deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(not_one_element formula-decl nil nth_derivatives nil)
(deriv_domain formula-decl nil nth_derivatives nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(derivable_n_times_lem formula-decl nil nth_derivatives nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(nderiv def-decl "[T -> real]" nth_derivatives nil)
(nderiv_fun type-eq-decl nil nth_derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(not_one_element? const-decl "bool" deriv_domain_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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T_pred const-decl "[real -> boolean]" nth_derivatives nil)
(T formal-subtype-decl nil nth_derivatives nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
shostak)))
¤ Dauer der Verarbeitung: 0.31 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.
|
