| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 91 kB |
|
Quelle deriv_real_vect2.prfSprache: Lisp |
|||||||||||||||
|
(deriv_real_vect2 (IMP_derivatives_TCC1 0 (IMP_derivatives_TCC1-1 nil 3460199836 ("" (lemma "deriv_domain") (("" (expand "deriv_domain?") (("" (propax) nil nil)) nil)) nil) ((deriv_domain formula-decl nil deriv_real_vect2 nil)) nil)) (IMP_derivatives_TCC2 0 (IMP_derivatives_TCC2-1 nil 3460199836 ("" (lemma not_one_element) (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil deriv_real_vect2 nil)) nil)) (deriv_rv_TCC1 0 (deriv_rv_TCC1-1 nil 3460199836 ("" (skeep) (("" (typepred "V") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (inst - "r") 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (derivable? const-decl "bool" derivatives "analysis/")) nil)) (deriv_rv_TCC2 0 (deriv_rv_TCC2-2 nil 3465570925 ("" (skeep) (("" (typepred "V") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (inst - "r") (("" (inst - "r") nil 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (derivable? const-decl "bool" derivatives "analysis/")) nil) (deriv_rv_TCC2-1 nil 3460199836 ("" (skeep) (("" (postpone) nil nil)) nil) nil nil)) (sum_derivable_rv 0 (sum_derivable_rv-1 nil 3471880334 ("" (skosimp*) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (lemma "sum_derivable") (("" (split +) (("1" (expand "derivable?" 1) (("1" (skosimp*) (("1" (inst - "(LAMBDA (a): f1!1(a)`x)" "(LAMBDA (a): f2!1(a)`x)" "x!1") (("1" (expand "+ ") (("1" (assert) (("1" (hide 1) (("1" (split +) (("1" (inst -3 "x!1") nil nil) ("2" (inst -1 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "derivable?" 1) (("2" (skosimp*) (("2" (inst - "(LAMBDA (a): f1!1(a)`y)" "(LAMBDA (a): f2!1(a)`y)" "x!1") (("2" (assert) (("2" (expand "+ ") (("2" (assert) (("2" (hide 1) (("2" (split +) (("1" (inst -4 "x!1") nil nil) ("2" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (derivable? const-decl "bool" derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "Vector" vectors_2D "vectors/") (sum_derivable formula-decl nil derivatives_def "analysis/")) nil)) (diff_derivable_rv 0 (diff_derivable_rv-2 nil 3471880451 ("" (skosimp*) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (lemma "diff_derivable") (("" (split +) (("1" (expand "derivable?" 1) (("1" (skosimp*) (("1" (inst - "(LAMBDA (a): f1!1(a)`x)" "(LAMBDA (a): f2!1(a)`x)" "x!1") (("1" (expand "- ") (("1" (assert) (("1" (hide 1) (("1" (split +) (("1" (inst -3 "x!1") nil nil) ("2" (inst -1 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "derivable?" 1) (("2" (skosimp*) (("2" (inst - "(LAMBDA (a): f1!1(a)`y)" "(LAMBDA (a): f2!1(a)`y)" "x!1") (("2" (assert) (("2" (expand "- ") (("2" (assert) (("2" (hide 1) (("2" (split +) (("1" (inst -4 "x!1") nil nil) ("2" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (derivable? const-decl "bool" derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "Vector" vectors_2D "vectors/") (diff_derivable formula-decl nil derivatives_def "analysis/")) nil) (diff_derivable_rv-1 nil 3471880384 (";;; Proof sum_derivable_rv-1 for formula vect_deriv_2D.sum_derivable_rv" (skosimp*) ((";;; Proof sum_derivable_rv-1 for formula vect_deriv_2D.sum_derivable_rv" (typepred "f1!1") ((";;; Proof sum_derivable_rv-1 for formula vect_deriv_2D.sum_derivable_rv" (typepred "f2!1") ((";;; Proof sum_derivable_rv-1 for formula vect_deriv_2D.sum_derivable_rv" (expand "derivable_rv?") ((";;; Proof sum_derivable_rv-1 for formula vect_deriv_2D.sum_derivable_rv" (flatten) ((";;; Proof sum_derivable_rv-1 for formula vect_deriv_2D.sum_derivable_rv" (expand "derivable?" -) ((";;; Proof sum_derivable_rv-1 for formula vect_deriv_2D.sum_derivable_rv" (lemma "sum_derivable") ((";;; Proof sum_derivable_rv-1 for formula vect_deriv_2D.sum_derivable_rv" (split +) (("1" (expand "derivable?" 1) (("1" (skosimp*) (("1" (inst - "(LAMBDA (a): f1!1(a)`x)" "(LAMBDA (a): f2!1(a)`x)" "x!1") (("1" (expand "+ ") (("1" (assert) (("1" (hide 1) (("1" (split +) (("1" (inst -3 "x!1") nil) ("2" (inst -1 "x!1") nil))))))))))))))) ("2" (expand "derivable?" 1) (("2" (skosimp*) (("2" (inst - "(LAMBDA (a): f1!1(a)`y)" "(LAMBDA (a): f2!1(a)`y)" "x!1") (("2" (assert) (("2" (expand "+ ") (("2" (assert) (("2" (hide 1) (("2" (split +) (("1" (inst -4 "x!1") nil) ("2" (inst -2 "x!1") nil)))))))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil)) (neg_derivable_rv 0 (neg_derivable_rv-1 nil 3471880652 ("" (skosimp*) (("" (typepred "f!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (lemma "neg_derivable") (("" (split +) (("1" (expand "derivable?" 1) (("1" (skosimp*) (("1" (inst - "(LAMBDA (a): f!1(a)`x)" "x!1") (("1" (assert) (("1" (expand "-") (("1" (assert) (("1" (inst -1 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "derivable?" 1) (("2" (skosimp*) (("2" (inst - "(LAMBDA (a): f!1(a)`y)" "x!1") (("2" (assert) (("2" (expand "-") (("2" (assert) (("2" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (neg_derivable formula-decl nil derivatives_def "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "Vector" vectors_2D "vectors/") (derivable? const-decl "bool" derivatives "analysis/")) shostak)) (prod_derivable_rv 0 (prod_derivable_rv-3 nil 3472230489 ("" (skosimp*) (("" (typepred "f!1") (("" (typepred "h!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (lemma "prod_derivable") (("" (split +) (("1" (expand "derivable?" 1) (("1" (skosimp*) (("1" (inst - "(LAMBDA (a): h!1(a))" "(LAMBDA (a): f!1(a)`x)" "x!1") (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (hide 1) (("1" (split +) (("1" (inst?) (("1" (assert) (("1" (case-replace "(LAMBDA (a): h!1(a)) = h!1") (("1" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil) ("2" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "derivable?" 1) (("2" (skosimp*) (("2" (inst - "(LAMBDA (a): h!1(a))" "(LAMBDA (a): f!1(a)`y)" "x!1") (("2" (assert) (("2" (expand "*") (("2" (assert) (("2" (hide 1) (("2" (split +) (("1" (inst?) (("1" (case-replace "(LAMBDA (a): h!1(a)) = h!1") (("1" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil) ("2" (inst -3 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "Vector" vectors_2D "vectors/") (* const-decl "[T -> real]" real_fun_ops "reals/") (prod_derivable formula-decl nil derivatives_def "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/")) nil) (prod_derivable_rv-2 nil 3472230462 (";;; Proof prod_derivable_rv-1 for formula vect_deriv_2D.prod_derivable_rv" (skosimp*) ((";;; Proof prod_derivable_rv-1 for formula vect_deriv_2D.prod_derivable_rv" (typepred "f!1") ((";;; Proof prod_derivable_rv-1 for formula vect_deriv_2D.prod_derivable_rv" (typepred "r!1") ((";;; Proof prod_derivable_rv-1 for formula vect_deriv_2D.prod_derivable_rv" (expand "derivable_rv?") ((";;; Proof prod_derivable_rv-1 for formula vect_deriv_2D.prod_derivable_rv" (flatten) ((";;; Proof prod_derivable_rv-1 for formula vect_deriv_2D.prod_derivable_rv" (expand "derivable?" -) ((";;; Proof prod_derivable_rv-1 for formula vect_deriv_2D.prod_derivable_rv" (lemma "prod_derivable") ((";;; Proof prod_derivable_rv-1 for formula vect_deriv_2D.prod_derivable_rv" (split +) (("1" (expand "derivable?" 1) (("1" (skosimp*) (("1" (inst - "(LAMBDA (a): r!1(a))" "(LAMBDA (a): f!1(a)`x)" "x!1") (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (hide 1) (("1" (split +) (("1" (inst?) (("1" (assert) (("1" (case-replace "(LAMBDA (a): r!1(a)) = r!1") (("1" (apply-extensionality 1 :hide? t) nil))))))) ("2" (inst -2 "x!1") nil))))))))))))))))) ("2" (expand "derivable?" 1) (("2" (skosimp*) (("2" (inst - "(LAMBDA (a): r!1(a))" "(LAMBDA (a): f!1(a)`y)" "x!1") (("2" (assert) (("2" (expand "*") (("2" (assert) (("2" (hide 1) (("2" (split +) (("1" (inst?) (("1" (case-replace "(LAMBDA (a): r!1(a)) = r!1") (("1" (apply-extensionality 1 :hide? t) nil))))) ("2" (inst -3 "x!1") nil)))))))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil) (prod_derivable_rv-1 nil 3472229558 ("" (skosimp*) (("" (typepred "f!1") (("" (typepred "r!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (lemma "prod_derivable") (("" (split +) (("1" (expand "derivable?" 1) (("1" (skosimp*) (("1" (inst - "(LAMBDA (a): r!1(a))" "(LAMBDA (a): f!1(a)`x)" "x!1") (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (hide 1) (("1" (split +) (("1" (inst?) (("1" (assert) (("1" (case-replace "(LAMBDA (a): r!1(a)) = r!1") (("1" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil) ("2" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "derivable?" 1) (("2" (skosimp*) (("2" (inst - "(LAMBDA (a): r!1(a))" "(LAMBDA (a): f!1(a)`y)" "x!1") (("2" (assert) (("2" (expand "*") (("2" (assert) (("2" (hide 1) (("2" (split +) (("1" (inst?) (("1" (case-replace "(LAMBDA (a): r!1(a)) = r!1") (("1" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil) ("2" (inst -3 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vect2 type-eq-decl nil vectors_2D_def "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (prod_derivable formula-decl nil derivatives_def "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/")) shostak)) (dot_derivable_rv 0 (dot_derivable_rv-1 nil 3472303865 ("" (skosimp*) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "*") (("" (lemma "sum_derivable_fun") (("" (inst - "(LAMBDA (x: T): f1!1(x)`x * f2!1(x)`x)" "(LAMBDA (x: T): f1!1(x)`y * f2!1(x)`y)") (("" (assert) (("" (expand "+ ") (("" (hide 2) (("" (lemma "prod_derivable_fun") (("" (split +) (("1" (inst - "(LAMBDA (x: T): f1!1(x)`x )" "(LAMBDA (x: T): f2!1(x)`x)") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil) ("2" (inst - "(LAMBDA (x: T): f1!1(x)`y )" "(LAMBDA (x: T): f2!1(x)`y)") (("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "real" vectors_2D "vectors/") (real_times_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/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (sum_derivable_fun formula-decl nil derivatives "analysis/")) nil)) (sqv_derivable_rv 0 (sqv_derivable_rv-1 nil 3476707583 ("" (skosimp*) (("" (expand "sqv") (("" (rewrite "dot_derivable_rv") nil nil)) nil)) nil) ((sqv const-decl "nnreal" vectors_2D "vectors/") (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 deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (dot_derivable_rv formula-decl nil deriv_real_vect2 nil)) shostak)) (const_derivable_rv 0 (const_derivable_rv-1 nil 3472302247 ("" (skosimp*) (("" (expand "derivable_rv?") (("" (lemma "const_derivable_fun") (("" (expand "const_fun") (("" (split +) (("1" (inst?) nil nil) ("2" (inst?) 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/") (const_derivable_fun formula-decl nil derivatives "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) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil)) shostak)) (scal_derivable_rv 0 (scal_derivable_rv-1 nil 3472302300 ("" (skosimp*) (("" (typepred "f!1") (("" (expand "derivable_rv?") (("" (expand "*") (("" (flatten) (("" (lemma "scal_derivable_fun") (("" (split +) (("1" (inst - "c!1" "(LAMBDA (a): f!1(a)`x)") (("1" (assert) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (inst - "c!1" "(LAMBDA (a): f!1(a)`y)") (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (* const-decl "Vector" vectors_2D "vectors/") (scal_derivable_fun formula-decl nil derivatives "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (prod_id_derivable_rv 0 (prod_id_derivable_rv-1 nil 3476023482 ("" (skosimp*) (("" (rewrite "prod_derivable_rv") (("1" (rewrite "id_derivable_fun") nil nil) ("2" (rewrite "const_derivable_rv") nil nil)) nil)) nil) ((prod_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (id_derivable_fun formula-decl nil derivatives "analysis/") (const_derivable_rv formula-decl nil deriv_real_vect2 nil)) shostak)) (deriv_sum_vfun_TCC1 0 (deriv_sum_vfun_TCC1-1 nil 3472229354 ("" (skosimp*) (("" (lemma "sum_derivable_rv") (("" (inst?) nil nil)) nil)) nil) ((sum_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil)) nil)) (deriv_sum_vfun 0 (deriv_sum_vfun-1 nil 3472229360 ("" (skosimp*) (("" (lemma "sum_derivable_rv") (("" (inst - "f1!1" "f2!1") (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (expand "deriv") (("" (expand "deriv_rv") (("" (apply-extensionality 1 :hide? t) (("" (expand "+ ") (("" (prop) (("1" (lemma "deriv_sum") (("1" (inst - "(LAMBDA (a): f1!1(a)`x)" "(LAMBDA (a): f2!1(a)`x)" "x!1") (("1" (split -1) (("1" (expand "+ ") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (inst -3 "x!1") nil nil)) nil) ("3" (hide 2) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "deriv_sum") (("2" (inst - "(LAMBDA (a): f1!1(a)`y)" "(LAMBDA (a): f2!1(a)`y)" "x!1") (("2" (assert) (("2" (split -1) (("1" (assert) (("1" (expand "+ ") (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (inst -4 "x!1") nil nil)) nil) ("3" (hide 2) (("3" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sum_derivable_rv formula-decl nil deriv_real_vect2 nil) (NOT const-decl "[bool -> bool]" booleans nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv_rv const-decl "Vect2" deriv_real_vect2 nil) (real_plus_real_is_real application-judgement "real" reals nil) (deriv_sum formula-decl nil derivatives_def "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (f2!1 skolem-const-decl "(derivable_rv?)" deriv_real_vect2 nil) (f1!1 skolem-const-decl "(derivable_rv?)" deriv_real_vect2 nil) (+ const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (derivable? const-decl "bool" derivatives_def "analysis/") (deriv const-decl "real" derivatives_def "analysis/") (deriv const-decl "[T -> Vect2]" deriv_real_vect2 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 deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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)) (deriv_diff_vfun_TCC1 0 (deriv_diff_vfun_TCC1-1 nil 3472234081 ("" (skosimp*) (("" (lemma "diff_derivable_rv") (("" (inst?) nil nil)) nil)) nil) ((diff_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil)) nil)) (deriv_diff_vfun 0 (deriv_diff_vfun-1 nil 3472234093 ("" (skosimp*) (("" (lemma "diff_derivable_rv") (("" (inst - "f1!1" "f2!1") (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (expand "deriv") (("" (expand "deriv_rv") (("" (apply-extensionality 1 :hide? t) (("" (expand "- ") (("" (prop) (("1" (lemma "deriv_diff") (("1" (inst - "(LAMBDA (a): f1!1(a)`x)" "(LAMBDA (a): f2!1(a)`x)" "x!1") (("1" (split -1) (("1" (expand "- ") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (inst -3 "x!1") nil nil)) nil) ("3" (hide 2) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "deriv_diff") (("2" (inst - "(LAMBDA (a): f1!1(a)`y)" "(LAMBDA (a): f2!1(a)`y)" "x!1") (("2" (assert) (("2" (split -1) (("1" (assert) (("1" (expand "- ") (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (inst -4 "x!1") nil nil)) nil) ("3" (hide 2) (("3" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((diff_derivable_rv formula-decl nil deriv_real_vect2 nil) (NOT const-decl "[bool -> bool]" booleans nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv_rv const-decl "Vect2" deriv_real_vect2 nil) (real_minus_real_is_real application-judgement "real" reals nil) (deriv_diff formula-decl nil derivatives_def "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (f2!1 skolem-const-decl "(derivable_rv?)" deriv_real_vect2 nil) (f1!1 skolem-const-decl "(derivable_rv?)" deriv_real_vect2 nil) (- const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (derivable? const-decl "bool" derivatives_def "analysis/") (deriv const-decl "real" derivatives_def "analysis/") (deriv const-decl "[T -> Vect2]" deriv_real_vect2 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 deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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)) (deriv_neg_vfun_TCC1 0 (deriv_neg_vfun_TCC1-1 nil 3472229396 ("" (skosimp*) (("" (rewrite "neg_derivable_rv") nil nil)) nil) ((neg_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil)) nil)) (deriv_neg_vfun 0 (deriv_neg_vfun-1 nil 3472229400 ("" (skosimp*) (("" (typepred "f!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (expand "deriv") (("" (expand "deriv_rv") (("" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (prop) (("1" (lemma "deriv_neg") (("1" (inst - "(LAMBDA (a): f!1(a)`x)" "x!1") (("1" (split -1) (("1" (expand "-") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (inst -1 "x!1") nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "deriv_neg") (("2" (inst - "(LAMBDA (a): f!1(a)`y)" "x!1") (("2" (split -1) (("1" (expand "-") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "neg_derivable") (("2" (inst - "(LAMBDA (a): f!1(a)`y)" "r!1") (("2" (expand "-") (("2" (assert) (("2" (hide 2) (("2" (inst -2 "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "neg_derivable") (("3" (inst - "(LAMBDA (a): f!1(a)`x)" "r!1") (("3" (assert) (("3" (expand "-") (("3" (assert) (("3" (inst -1 "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (deriv const-decl "[T -> Vect2]" deriv_real_vect2 nil) (deriv const-decl "real" derivatives_def "analysis/") (Vector type-eq-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (f!1 skolem-const-decl "(derivable_rv?)" deriv_real_vect2 nil) (derivable? const-decl "bool" derivatives_def "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (deriv_neg formula-decl nil derivatives_def "analysis/") (neg_derivable formula-decl nil derivatives_def "analysis/") (deriv_rv const-decl "Vect2" deriv_real_vect2 nil) (derivable? const-decl "bool" derivatives "analysis/")) nil)) (deriv_prod_vfun_TCC1 0 (deriv_prod_vfun_TCC1-1 nil 3472229531 ("" (skosimp*) (("" (rewrite "prod_derivable_rv") nil nil)) nil) ((prod_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/")) nil)) (deriv_prod_vfun 0 (deriv_prod_vfun-1 nil 3472230228 ("" (skosimp*) (("" (typepred "h!1") (("" (typepred "f!1") (("" (lemma "prod_derivable_rv") (("" (inst - "f!1" "h!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?" -) (("" (expand "deriv") (("" (expand "deriv_rv") (("" (expand "*") (("" (expand "*") (("" (expand "+ ") (("" (apply-extensionality 1 :hide? t) (("" (prop) (("1" (lemma "deriv_prod") (("1" (inst - "(LAMBDA (a): h!1(a))" "(LAMBDA (a): f!1(a)`x)" "x!1") (("1" (assert) (("1" (split -1) (("1" (expand "*") (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "(LAMBDA (a): h!1(a)) = h!1") (("1" (assert) nil nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst -5 "x!1") (("2" (case-replace "(LAMBDA (a): h!1(a)) = h!1") (("2" (assert) (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (inst -3 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deriv_prod") (("2" (inst - "(LAMBDA (a): h!1(a))" "(LAMBDA (a): f!1(a)`y)" "x!1") (("2" (assert) (("2" (split -1) (("1" (expand "*") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (case-replace "(LAMBDA (a): h!1(a)) = h!1") (("1" (assert) nil nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst -5 "x!1") (("2" (case-replace "(LAMBDA (a): h!1(a)) = h!1") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil) ("3" (inst -4 "x!1") nil nil)) nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (prod_derivable_rv formula-decl nil deriv_real_vect2 nil) (deriv_rv const-decl "Vect2" deriv_real_vect2 nil) (deriv const-decl "real" derivatives_def "analysis/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (f!1 skolem-const-decl "(derivable_rv?)" deriv_real_vect2 nil) (h!1 skolem-const-decl "deriv_fun[T]" deriv_real_vect2 nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (derivable? const-decl "bool" derivatives_def "analysis/") (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (deriv_prod formula-decl nil derivatives_def "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (* const-decl "[T -> Vect2]" vect_fun_ops_rv nil) (deriv const-decl "[T -> Vect2]" deriv_real_vect2 nil) (deriv const-decl "[T -> real]" derivatives "analysis/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (derivable_rv? const-decl "bool" deriv_real_vect2 nil)) shostak)) (deriv_dot_vfun_TCC1 0 (deriv_dot_vfun_TCC1-1 nil 3472303719 ("" (skosimp*) (("" (lemma "dot_derivable_rv") (("" (inst?) nil nil)) nil)) nil) ((dot_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil)) nil)) (deriv_dot_vfun 0 (deriv_dot_vfun-1 nil 3472304379 ("" (skosimp*) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (expand "derivable_rv?") (("" (flatten) (("" (expand "derivable?") (("" (expand "*") (("" (expand "+") (("" (lemma "deriv_sum_fun") (("" (inst - "(LAMBDA (x: T): f1!1(x)`x * f2!1(x)`x)" "(LAMBDA (x: T): f1!1(x)`y * f2!1(x)`y)") (("1" (expand "+") (("1" (replace -1) (("1" (hide -1) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "deriv") (("1" (expand "deriv_rv") (("1" (lemma "deriv_prod") (("1" (inst-cp - "(LAMBDA (x: T): f1!1(x)`x )" "(LAMBDA (x: T): f2!1(x)`x)" "x!1") (("1" (inst - "(LAMBDA (x: T): f1!1(x)`y )" "(LAMBDA (x: T): f2!1(x)`y)" "x!1") (("1" (split -1) (("1" (split -2) (("1" (assert) (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil) ("2" (hide -1 2) (("2" (inst -3 "x!1") nil nil)) nil) ("3" (hide -1 2) (("3" (inst -1 "x!1") nil nil)) nil)) nil) ("2" (hide -1 2) (("2" (inst -4 "x!1") nil nil)) nil) ("3" (hide -1 2) (("3" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "prod_derivable_fun") (("2" (inst - "(LAMBDA (x: T): f1!1(x)`y )" "(LAMBDA (x: T): f2!1(x)`y)") (("2" (assert) (("2" (expand "*") (("2" (hide 2) (("2" (split +) (("1" (expand "derivable?" 1) (("1" (propax) nil nil)) nil) ("2" (expand "derivable?" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "prod_derivable_fun") (("3" (inst - "(LAMBDA (x: T): f1!1(x)`x )" "(LAMBDA (x: T): f2!1(x)`x)") (("3" (assert) (("3" (expand "*") (("3" (hide 2) (("3" (expand "derivable?" 1) (("3" (split +) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "prod_derivable_fun") (("2" (inst - "(LAMBDA (x: T): f1!1(x)`y )" "(LAMBDA (x: T): f2!1(x)`y)") (("2" (expand "*") (("2" (assert) (("2" (hide 2) (("2" (expand "derivable?") (("2" (split +) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "prod_derivable_fun") (("3" (inst - "(LAMBDA (x: T): f1!1(x)`x )" "(LAMBDA (x: T): f2!1(x)`x)") (("3" (expand "*") (("3" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "derivable?" 1) (("2" (propax) nil nil)) nil)) nil) ("3" (hide 2) (("3" (expand "derivable?" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (derivable? const-decl "bool" derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (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) (f1!1 skolem-const-decl "(derivable_rv?)" deriv_real_vect2 nil) (f2!1 skolem-const-decl "(derivable_rv?)" deriv_real_vect2 nil) (deriv_fun type-eq-decl nil derivatives "analysis/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (deriv const-decl "[T -> real]" derivatives "analysis/") (deriv const-decl "[T -> Vect2]" deriv_real_vect2 nil) (real_plus_real_is_real application-judgement "real" reals nil) (deriv_rv const-decl "Vect2" deriv_real_vect2 nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv_prod formula-decl nil derivatives_def "analysis/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (deriv_sum_fun formula-decl nil derivatives "analysis/") (* const-decl "real" vectors_2D "vectors/")) shostak)) (deriv_sqv_vfun_TCC1 0 (deriv_sqv_vfun_TCC1-1 nil 3476707489 ("" (skosimp*) (("" (expand "sqv") (("" (rewrite "dot_derivable_rv") nil nil)) nil)) nil) ((sqv const-decl "nnreal" vectors_2D "vectors/") (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 deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (dot_derivable_rv formula-decl nil deriv_real_vect2 nil)) nil)) (deriv_sqv_vfun 0 (deriv_sqv_vfun-2 nil 3476707542 ("" (skosimp*) (("" (expand "sqv") (("" (lemma "deriv_dot_vfun") (("" (inst?) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (apply-extensionality 1 :hide? t) (("" (expand "+") (("" (assert) (("" (lemma "dot_comm") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sqv const-decl "nnreal" vectors_2D "vectors/") (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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (deriv const-decl "[T -> Vect2]" deriv_real_vect2 nil) (* const-decl "real" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (dot_comm formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (deriv_dot_vfun formula-decl nil deriv_real_vect2 nil)) nil) (deriv_sqv_vfun-1 nil 3476707525 (";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (skosimp*) ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (lemma "deriv_dot_vfun") ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (inst?) ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (assert) ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (replace -1) ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (hide -1) ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (apply-extensionality 1 :hide? t) ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (expand "+") ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (assert) ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (lemma "dot_comm") ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (inst?) ((";;; Proof deriv_dot2_vfun-1 for formula deriv_real_vect2.deriv_dot2_vfun" (assert) nil)))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil)) (deriv_const_vfun_TCC1 0 (deriv_const_vfun_TCC1-1 nil 3472302230 ("" (skosimp*) (("" (lemma "const_derivable_rv") (("" (inst?) nil nil)) nil)) nil) ((const_derivable_rv formula-decl nil deriv_real_vect2 nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/")) nil)) (deriv_const_vfun 0 (deriv_const_vfun-1 nil 3472302687 ("" (skosimp*) (("" (expand "deriv") (("" (lemma "deriv_const") (("" (expand "const_fun") (("" (apply-extensionality 1 :hide? t) (("1" (expand "zero") (("1" (expand "deriv_rv") (("1" (split +) (("1" (inst?) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "const_derivable_rv") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv const-decl "[T -> Vect2]" deriv_real_vect2 nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (const_derivable_rv formula-decl nil deriv_real_vect2 nil) (s!1 skolem-const-decl "Vect2" deriv_real_vect2 nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (bool nonempty-type-eq-decl nil booleans nil) (deriv_rv const-decl "Vect2" deriv_real_vect2 nil) (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (deriv_const formula-decl nil derivatives_def "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) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil)) shostak)) (deriv_scal_vfun_TCC1 0 (deriv_scal_vfun_TCC1-1 nil 3472302838 ("" (skosimp*) (("" (lemma "scal_derivable_rv") (("" (inst?) nil nil)) nil)) nil) ((scal_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil)) nil)) (deriv_scal_vfun 0 (deriv_scal_vfun-1 nil 3472302846 ("" (skosimp*) (("" (typepred "f!1") (("" (lemma "scal_derivable_rv") (("" (inst - "c!1" "f!1") (("" (expand "derivable_rv?" -2) (("" (flatten) (("" (expand "derivable?") (("" (expand "deriv") (("" (expand "deriv_rv") (("" (expand "*") (("" (apply-extensionality 1 :hide? t) (("1" (lemma "deriv_scal") (("1" (split +) (("1" (inst?) (("1" (assert) (("1" (expand "*") (("1" (hide 1) (("1" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (expand "*") (("2" (assert) (("2" (hide 1) (("2" (inst -3 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "derivable_rv?") (("2" (flatten) (("2" (assert) (("2" (expand "derivable?" -2) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "derivable_rv?") (("3" (flatten) (("3" (hide -3 -4) (("3" (expand "derivable?" -) (("3" (inst -1 "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (T formal-subtype-decl nil deriv_real_vect2 nil) (T_pred const-decl "[real -> boolean]" deriv_real_vect2 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) (deriv const-decl "[T -> Vect2]" deriv_real_vect2 nil) (* const-decl "Vector" vectors_2D "vectors/") (deriv_scal formula-decl nil derivatives_def "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (derivable? const-decl "bool" derivatives_def "analysis/") (f!1 skolem-const-decl "(derivable_rv?)" deriv_real_vect2 nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (c!1 skolem-const-decl "real" deriv_real_vect2 nil) (deriv const-decl "real" derivatives_def "analysis/") (deriv_rv const-decl "Vect2" deriv_real_vect2 nil) (derivable? const-decl "bool" derivatives "analysis/") (scal_derivable_rv formula-decl nil deriv_real_vect2 nil)) shostak)) (deriv_prod_id_vfun_TCC1 0 (deriv_prod_id_vfun_TCC1-1 nil 3476023470 ("" (skosimp*) (("" (rewrite "prod_id_derivable_rv") nil nil)) nil) ((prod_id_derivable_rv formula-decl nil deriv_real_vect2 nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/")) nil)) (deriv_prod_id_vfun 0 (deriv_prod_id_vfun-1 nil 3476031530 ("" (skosimp*) (("" (rewrite "deriv_prod_vfun") (("1" (apply-extensionality 1 :hide? t) (("1" (expand "*") (("1" (rewrite "deriv_id_fun") (("1" (assert) (("1" (rewrite "deriv_const_vfun") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "const_derivable_rv") nil nil)) nil) ("3" (skosimp*) (("3" (rewrite "id_derivable_fun") nil nil)) nil)) nil) ("2" (rewrite "id_derivable_fun") nil nil) ("3" (rewrite "const_derivable_rv") nil nil)) nil)) nil) ((deriv_prod_vfun formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (id_derivable_fun formula-decl nil derivatives "analysis/") (const_derivable_rv formula-decl nil deriv_real_vect2 nil) (scal_1 formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (deriv_const_vfun formula-decl nil deriv_real_vect2 nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (v!1 skolem-const-decl "Vect2" deriv_real_vect2 nil) (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "[T -> Vect2]" vect_fun_ops_rv nil) (deriv const-decl "[T -> real]" derivatives "analysis/") (deriv const-decl "[T -> Vect2]" deriv_real_vect2 nil) (Vector type-eq-decl nil vectors_2D "vectors/")) shostak)) (d_sum_vfun 0 (d_sum_vfun-1 nil 3473007766 ("" (skosimp*) (("" (rewrite "deriv_sum_vfun") (("" (rewrite "sum_derivable_rv") nil nil)) nil)) nil) ((deriv_sum_vfun formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (sum_derivable_rv formula-decl nil deriv_real_vect2 nil)) shostak)) (d_diff_vfun 0 (d_diff_vfun-1 nil 3473007893 ("" (skosimp*) (("" (rewrite "diff_derivable_rv") (("" (rewrite "deriv_diff_vfun") nil nil)) nil)) nil) ((diff_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (deriv_diff_vfun formula-decl nil deriv_real_vect2 nil)) shostak)) (d_neg_vfun 0 (d_neg_vfun-1 nil 3473007910 ("" (skosimp*) (("" (rewrite "neg_derivable_rv") (("" (rewrite "deriv_neg_vfun") nil nil)) nil)) nil) ((neg_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (deriv_neg_vfun formula-decl nil deriv_real_vect2 nil)) shostak)) (d_prod_vfun 0 (d_prod_vfun-1 nil 3473007924 ("" (skosimp*) (("" (rewrite "prod_derivable_rv") (("" (rewrite "deriv_prod_vfun") nil nil)) nil)) nil) ((prod_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_prod_vfun formula-decl nil deriv_real_vect2 nil)) shostak)) (d_dot_vfun 0 (d_dot_vfun-1 nil 3473007940 ("" (skosimp*) (("" (rewrite "dot_derivable_rv") (("" (rewrite "deriv_dot_vfun") nil nil)) nil)) nil) ((dot_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (deriv_dot_vfun formula-decl nil deriv_real_vect2 nil)) shostak)) (d_const_vfun 0 (d_const_vfun-1 nil 3473007955 ("" (skosimp*) (("" (rewrite "const_derivable_rv") (("" (rewrite "deriv_const_vfun") nil nil)) nil)) nil) ((const_derivable_rv formula-decl nil deriv_real_vect2 nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (deriv_const_vfun formula-decl nil deriv_real_vect2 nil)) shostak)) (d_scal_vfun 0 (d_scal_vfun-1 nil 3473007985 ("" (skosimp*) (("" (rewrite "scal_derivable_rv") (("" (rewrite "deriv_scal_vfun") nil nil)) nil)) nil) ((scal_derivable_rv formula-decl nil deriv_real_vect2 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]" deriv_real_vect2 nil) (T formal-subtype-decl nil deriv_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (derivable_rv? const-decl "bool" deriv_real_vect2 nil) (deriv_scal_vfun formula-decl nil deriv_real_vect2 nil)) shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.61Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26