|
(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"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.899 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.
|
