|
(vect_deriv_2D
(IMP_deriv_real_vect2_TCC1 0
(IMP_deriv_real_vect2_TCC1-1 nil 3474291163
("" (lemma deriv_domain) (("" (propax) nil nil)) nil)
((deriv_domain formula-decl nil vect_deriv_2D nil)) nil))
(IMP_deriv_real_vect2_TCC2 0
(IMP_deriv_real_vect2_TCC2-1 nil 3474291163
("" (lemma not_one_element) (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil vect_deriv_2D nil)) nil))
(detsv_diff 0
(detsv_diff-1 nil 3460284090
("" (skeep)
(("" (expand "detsv")
(("" (expand "det")
(("" (lemma "derivable_diff")
((""
(inst - "(lambda (r): s`x * V(r)`y)"
"(lambda (r): s`y * V(r)`x)")
(("1" (expand "-[T]" -) (("1" (propax) nil nil)) nil)
("2" (lemma "derivable_scal")
(("2" (inst - "s`y" "(LAMBDA (r): V(r)`x)")
(("1" (expand "*" -) (("1" (propax) nil nil)) nil)
("2" (typepred "V")
(("2" (expand "derivable_rv?")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("3" (lemma "derivable_scal")
(("3" (inst - "s`x" "(LAMBDA (r): V(r)`y)")
(("1" (expand "*" -) (("1" (propax) nil nil)) nil)
("2" (typepred "V")
(("2" (expand "derivable_rv?")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((detsv const-decl "real" vect_deriv_2D nil)
(T formal-subtype-decl nil vect_deriv_2D nil)
(T_pred const-decl "[real -> boolean]" vect_deriv_2D 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_diff judgement-tcc nil derivatives "analysis/")
(derivable_scal judgement-tcc nil derivatives "analysis/")
(NOT const-decl "[bool -> bool]" booleans nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives "analysis/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(s skolem-const-decl "Vect2" vect_deriv_2D nil)
(derivable_rv? const-decl "bool" deriv_real_vect2 nil)
(V skolem-const-decl "(derivable_rv?)" vect_deriv_2D nil)
(det const-decl "real" det_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(detsvp_deriv_TCC1 0
(detsvp_deriv_TCC1-1 nil 3460199836
("" (skeep)
(("" (lemma "detsv_diff") (("" (inst - "V" "s") nil nil)) nil))
nil)
((detsv_diff formula-decl nil vect_deriv_2D nil)
(derivable_rv? const-decl "bool" deriv_real_vect2 nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil vect_deriv_2D nil)
(T_pred const-decl "[real -> boolean]" vect_deriv_2D 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))
(detsvp_deriv 0
(detsvp_deriv-1 nil 3460284097
("" (skeep)
(("" (expand "detsv")
(("" (expand "det")
(("" (expand "deriv_rv")
(("" (expand "deriv" 1 1)
((""
(case "derivable?(lambda(a): V(a)`y) AND derivable?(lambda(a): V(a)`x)")
(("1"
(case "derivable?(LAMBDA (r): s`x * V(r)`y) AND derivable?(LAMBDA (r): s`y * V(r)`x)")
(("1"
(case "derivable?(LAMBDA (r): s`x * V(r)`y - s`y * V(r)`x)")
(("1" (label "diffderiv" -1)
(("1" (hide -1)
(("1" (label "constderiv" -1)
(("1" (hide -1)
(("1" (flatten)
(("1" (label "yderiv" -1)
(("1"
(label "xderiv" -2)
(("1"
(case
"deriv(LAMBDA (r): s`x * V(r)`y - s`y * V(r)`x) =
s`x * deriv(LAMBDA (a): V(a)`y) -
s`y * deriv(LAMBDA (a): V(a)`x)")
(("1"
(assert)
(("1"
(decompose-equality)
(("1"
(inst - "r")
(("1"
(expand "deriv" -)
(("1"
(expand "*" -)
(("1"
(expand "-" -)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(hide (-1 -2 2))
(("2"
(reveal -4)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide (-1 -2 2))
(("2"
(lemma "deriv_diff_fun")
(("2"
(inst
-
"LAMBDA (r): s`x * V(r)`y"
"LAMBDA (r): s`y * V(r)`x")
(("1"
(lemma "deriv_scal_fun")
(("1"
(inst
-
"s`x"
"lambda (r): V(r)`y")
(("1"
(expand "*" -1 1)
(("1"
(lemma
"deriv_scal_fun")
(("1"
(inst
-
"s`y"
"lambda (r): V(r)`x")
(("1"
(expand "*" -1 1)
(("1"
(expand "-" -3 1)
(("1"
(replace -3)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(reveal "xderiv")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(reveal "yderiv")
(("2" (propax) nil nil))
nil))
nil))
nil)
("2"
(reveal "constderiv")
(("2" (assert) nil nil))
nil)
("3"
(reveal "constderiv")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil)
("4" (propax) nil nil)
("5"
(reveal "diffderiv")
(("5" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "derivable_diff")
(("2"
(inst - "LAMBDA (r): s`x * V(r)`y"
"LAMBDA (r): s`y * V(r)`x")
(("1" (expand "-" -1) (("1" (propax) nil nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil)
("2" (lemma "derivable_scal")
(("2" (ground)
(("1" (inst - "s`x" "LAMBDA (r): V(r)`y")
(("1" (expand "*" -1) (("1" (propax) nil nil))
nil))
nil)
("2" (inst - "s`y" "LAMBDA (r): V(r)`x")
(("2" (expand "*" -1) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "V")
(("2" (expand "derivable_rv?") (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((detsv const-decl "real" vect_deriv_2D nil)
(deriv_rv const-decl "Vect2" deriv_real_vect2 nil)
(derivable_rv? const-decl "bool" deriv_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(derivable? const-decl "bool" derivatives "analysis/")
(T formal-subtype-decl nil vect_deriv_2D nil)
(T_pred const-decl "[real -> boolean]" vect_deriv_2D 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(derivable_scal judgement-tcc nil derivatives "analysis/")
(derivable_scal application-judgement "deriv_fun[T]" vect_deriv_2D
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(deriv_diff_fun formula-decl nil derivatives "analysis/")
(deriv_scal_fun formula-decl nil derivatives "analysis/")
(V skolem-const-decl "(derivable_rv?)" vect_deriv_2D nil)
(s skolem-const-decl "Vect2" vect_deriv_2D nil)
(derivable_diff judgement-tcc nil derivatives "analysis/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(deriv const-decl "[T -> real]" derivatives "analysis/")
(det const-decl "real" det_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(sqvdot_diff 0
(sqvdot_diff-1 nil 3460284107
("" (skeep)
(("" (expand "sqv")
(("" (expand "*")
((""
(case "derivable?((LAMBDA (r): V(r)`x)) AND derivable?((LAMBDA (r): V(r)`y))")
(("1" (flatten)
(("1" (lemma "derivable_sum")
(("1"
(inst - "LAMBDA (r): V(r)`x * V(r)`x"
"LAMBDA (r): V(r)`y * V(r)`y")
(("1" (expand "+" -1) (("1" (propax) nil nil)) nil)
("2" (lemma "derivable_prod")
(("2"
(inst - "LAMBDA (r): V(r)`y" "LAMBDA (r): V(r)`y")
(("2" (expand "*" -1) (("2" (propax) nil nil))
nil))
nil))
nil)
("3" (lemma "derivable_prod")
(("3"
(inst - "LAMBDA (r): V(r)`x" "LAMBDA (r): V(r)`x")
(("3" (expand "*" -1) (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "V")
(("2" (expand "derivable_rv?") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqv const-decl "nnreal" vectors_2D "vectors/")
(derivable_rv? const-decl "bool" deriv_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(derivable? const-decl "bool" derivatives "analysis/")
(T formal-subtype-decl nil vect_deriv_2D nil)
(T_pred const-decl "[real -> boolean]" vect_deriv_2D 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(derivable_sum judgement-tcc nil derivatives "analysis/")
(derivable_prod judgement-tcc nil derivatives "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(V skolem-const-decl "(derivable_rv?)" vect_deriv_2D nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(* const-decl "real" vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(sqvdot_deriv_TCC1 0
(sqvdot_deriv_TCC1-1 nil 3460199836
("" (skeep)
(("" (lemma "sqvdot_diff") (("" (inst - "V") nil nil)) nil)) nil)
((sqvdot_diff formula-decl nil vect_deriv_2D nil)
(derivable_rv? const-decl "bool" deriv_real_vect2 nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil vect_deriv_2D nil)
(T_pred const-decl "[real -> boolean]" vect_deriv_2D 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))
(sqvdot_deriv 0
(sqvdot_deriv-1 nil 3460284113
("" (skeep)
((""
(case "derivable?(lambda(a): V(a)`y) AND derivable?(lambda(a): V(a)`x)")
(("1"
(case "derivable?(LAMBDA (a): V(a)`y*V(a)`y) AND derivable?(LAMBDA (a): V(a)`x*V(a)`x)")
(("1"
(case "derivable?(LAMBDA (a): V(a)`x * V(a)`x + V(a)`y * V(a)`y)")
(("1" (flatten)
(("1" (label "totderiv" -1)
(("1" (label "ypderiv" -2)
(("1" (label "xpderiv" -3)
(("1" (label "yderiv" -4)
(("1" (label "xderiv" -5)
(("1" (expand "sqv")
(("1" (expand "*")
(("1" (expand "deriv_rv")
(("1" (lemma "deriv_sum")
(("1"
(inst
-
"LAMBDA (r): V(r)`x * V(r)`x"
"LAMBDA (r): V(r)`y * V(r)`y"
"r1")
(("1"
(copy "ypderiv")
(("1"
(copy "xpderiv")
(("1"
(expand "derivable?" -1)
(("1"
(expand "derivable?" -2)
(("1"
(inst - "r1")
(("1"
(inst - "r1")
(("1"
(assert)
(("1"
(hide -1)
(("1"
(hide -1)
(("1"
(expand
"deriv"
+
1)
(("1"
(expand "+" -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma
"deriv_prod")
(("1"
(inst-cp
-
"LAMBDA (r): V(r)`x"
"LAMBDA (r): V(r)`x"
"r1")
(("1"
(expand
"*"
-2)
(("1"
(inst
-
"LAMBDA (r): V(r)`y"
"LAMBDA (r): V(r)`y"
"r1")
(("1"
(assert)
(("1"
(copy
"yderiv")
(("1"
(copy
"xderiv")
(("1"
(expand
"derivable?"
-1)
(("1"
(expand
"derivable?"
-2)
(("1"
(inst
-
"r1")
(("1"
(inst
-
"r1")
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(hide
-1)
(("1"
(expand
"*"
-)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "derivable_sum")
(("2"
(inst - "LAMBDA (a): V(a)`x * V(a)`x"
"LAMBDA (a): V(a)`y * V(a)`y")
(("1" (expand "+" -1) (("1" (propax) nil nil)) nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil)
("2" (lemma "derivable_prod")
(("2" (inst-cp -1 "LAMBDA (a): V(a)`y" "LAMBDA (a): V(a)`y")
(("1" (inst - "LAMBDA (a): V(a)`x" "LAMBDA (a): V(a)`x")
(("1" (expand "*" -) (("1" (assert) nil nil)) nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (typepred "V")
(("2" (expand "derivable_rv?")
(("2" (flatten) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((derivable_rv? const-decl "bool" deriv_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(derivable? const-decl "bool" derivatives "analysis/")
(T formal-subtype-decl nil vect_deriv_2D nil)
(T_pred const-decl "[real -> boolean]" vect_deriv_2D 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(derivable_prod judgement-tcc nil derivatives "analysis/")
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "Vector" vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(deriv_sum formula-decl nil derivatives_def "analysis/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_prod formula-decl nil derivatives_def "analysis/")
(deriv const-decl "[T -> real]" derivatives "analysis/")
(deriv_rv const-decl "Vect2" deriv_real_vect2 nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(V skolem-const-decl "(derivable_rv?)" vect_deriv_2D nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(derivable_sum judgement-tcc nil derivatives "analysis/")
(real_times_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(NOT const-decl "[bool -> bool]" booleans 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.
|
