| products/sources/formale sprachen/PVS/vect_analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
||||||
|
(vect_cont_2D
(const_cont_vv 0 (const_cont_vv-1 nil 3445171659 ("" (skosimp*) (("" (expand "continuous_vv") (("" (lemma "cont_vect2_vect2.const_cont_vv_fun") (("" (expand "const_fun") (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((const_cont_vv_fun formula-decl nil cont_vect2_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (const_fun const-decl "[Vect2 -> Vect2]" limit_vect2_vect2 nil)) shostak)) (const_cont_rv 0 (const_cont_rv-1 nil 3445171923 ("" (skeep) (("" (expand "continuous_rv") (("" (lemma "cont_real_vect2[real].const_cont_rv_fun") (("" (inst?) (("" (expand "const_vfun") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) 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) (const_cont_rv_fun formula-decl nil cont_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/")) shostak)) (const_cont_vr 0 (const_cont_vr-2 nil 3473599495 ("" (skeep) (("" (lemma "cont_vect2_real.const_cont_vr_fun") (("" (expand "continuous_vr") (("" (inst?) (("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((const_cont_vr_fun formula-decl nil cont_vect2_real nil) (const_fun const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/") (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) (const_cont_vr-1 nil 3445171947 ("" (skeep) (("" (lemma "cont_vect2_real.const_cont_fun") (("" (expand "continuous_vr") (("" (expand "const_fun") (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((const_fun const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")) shostak)) (pair_cont_rv 0 (pair_cont_rv-4 nil 3445358177 ("" (skeep) (("" (typepred "rr1") (("" (typepred "rr2") (("" (expand "continuous_rv") (("" (expand "continuous?") (("" (expand "continuous_rv?") (("" (skeep) (("" (expand "continuous_rv?") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (expand "continuous?") (("" (inst - "epsilon!1/sqrt(2)") (("" (inst - "epsilon!1/sqrt(2)") (("" (skosimp*) (("" (inst + "min(delta!1,delta!2)") (("" (skosimp*) (("" (inst -1 "x!1") (("" (inst -2 "x!1") (("" (assert) (("" (use-with "sq_lt" 1) (("" (assert) (("" (hide 2) (("" (rewrite "sq_norm") (("" (use-with "sq_lt" -1) (("" (assert) (("" (use-with "sq_lt" -3) (("" (assert) (("" (hide -3 -4) (("" (hide -3) (("" (rewrite "sq_div") (("" (assert) (("" (case "sqv((# x := rr1(x!1), y := rr2(x!1) #) - (# x := rr1(x0), y := rr2(x0) #)) = sq(rr1(x!1) - rr1(x0)) + sq(rr2(x!1) - rr2(x0))") (("1" (assert) nil nil) ("2" (hide - 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_fun nonempty-type-eq-decl nil continuous_functions "analysis/") (continuous? const-decl "bool" continuous_functions "analysis/") (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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (- const-decl "Vector" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (< const-decl "bool" reals nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (sq_lt formula-decl nil sq "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sq_div formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (* const-decl "real" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sq_abs formula-decl nil sq "reals/") (sq_norm formula-decl nil vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (continuous? const-decl "bool" continuous_functions "analysis/") (continuous_rv? const-decl "bool" cont_real_vect2 nil) (real_minus_real_is_real application-judgement "real" reals nil) (continuous_rv? const-decl "bool" cont_real_vect2 nil)) nil) (pair_cont_rv-3 nil 3445358131 ("" (skeep) (("" (typepred "rr1") (("" (typepred "rr2") (("" (expand "continuous_rv") (("" (expand "continuous?") (("" (skeep) (("" (inst?) (("" (inst?) (("" (expand "continuous?") (("" (expand "convergence") (("" (expand "convergence") (("" (flatten) (("" (hide -1 -3) (("" (expand "fullset") (("" (skosimp*) (("" (inst - "sqrt(epsilon!1/2)") (("" (inst - "sqrt(epsilon!1/2)") (("" (skosimp*) (("" (inst + "min(delta!1,delta!2)") (("" (skosimp*) (("" (inst -1 "x!1") (("" (inst -2 "x!1") (("" (assert) (("" (use-with "sq_lt" 1) (("" (assert) (("" (hide 2) (("" (rewrite "sq_norm") (("" (use-with "sq_lt" -1) (("" (assert) (("" (use-with "sq_lt" -3) (("" (assert) (("" (hide -3 -4) (("" (hide -3) (("" (case "sqv((# x := rr1(x!1), y := rr2(x!1) #) - (# x := rr1(x0), y := rr2(x0) #)) = sq(rr1(x!1) - rr1(x0)) + sq(rr2(x!1) - rr2(x0))") (("1" (assert) (("1" (replace -1) (("1" (postpone) nil))))) ("2" (postpone) nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) nil) nil nil) (pair_cont_rv-2 nil 3445358015 (";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (skeep) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (typepred "rr1") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (typepred "rr2") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (expand "continuous_rv") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (expand "continuous?") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (skeep) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (inst?) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (inst?) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (expand "continuous?") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (expand "convergence") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (expand "convergence") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (flatten) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (hide -1 -3) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (expand "fullset") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (skosimp*) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (inst - "sqrt(epsilon!1)/2") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (inst - "sqrt(epsilon!1)/2") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (skosimp*) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (inst + "min(delta!1,delta!2)") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (skosimp*) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (inst -1 "x!1") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (inst -2 "x!1") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (assert) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (use-with "sq_lt" 1) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (assert) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (hide 2) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (rewrite "sq_norm") ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (use-with "sq_lt" -1) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (assert) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (use-with "sq_lt" -3) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (assert) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (hide -3 -4) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (hide -3) ((";;; Proof pair_cont_rv-1 for formula vect_cont_2D.pair_cont_rv" (case "sqv((# x := rr1(x!1), y := rr2(x!1) #) - (# x := rr1(x0), y := rr2(x0) #)) = sq(rr1(x!1) - rr1(x0)) + sq(rr2(x!1) - rr2(x0))") (("1" (assert) (("1" (replace -1) (("1" (postpone) nil))))) ("2" (postpone) nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil) (pair_cont_rv-1 nil 3445357201 ("" (skeep) (("" (typepred "rr1") (("" (typepred "rr2") (("" (expand "continuous_rv") (("" (expand "continuous?") (("" (skeep) (("" (inst?) (("" (inst?) (("" (expand "continuous?") (("" (expand "convergence") (("" (expand "convergence") (("" (flatten) (("" (hide -1 -3) (("" (expand "fullset") (("" (skosimp*) (("" (inst - "sqrt(epsilon!1/2)") (("" (inst - "sqrt(epsilon!1/2)") (("" (skosimp*) (("" (inst + "min(delta!1,delta!2)") (("" (skosimp*) (("" (inst -1 "x!1") (("" (inst -2 "x!1") (("" (assert) (("" (use-with "sq_lt" 1) (("" (assert) (("" (hide 2) (("" (rewrite "sq_norm") (("" (use-with "sq_lt" -1) (("" (assert) (("" (use-with "sq_lt" -3) (("" (assert) (("" (hide -3 -4) (("" (hide -3) (("" (case "sqv((# x := rr1(x!1), y := rr2(x!1) #) - (# x := rr1(x0), y := rr2(x0) #)) = sq(rr1(x!1) - rr1(x0)) + sq(rr2(x!1) - rr2(x0))") (("1" (assert) (("1" (replace -1) (("1" (postpone) nil nil)) nil)) nil) ("2" (postpone) 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 shostak)) (pair_cont_vv 0 (pair_cont_vv-1 nil 3445358259 ("" (skeep) (("" (typepred "vr1") (("" (typepred "vr2") (("" (expand "continuous_vr") (("" (expand "continuous_vv") (("" (expand "continuous_vv?") (("" (expand "continuous_vr?") (("" (skeep) (("" (expand "continuous_vv?") (("" (expand "continuous_vr?") (("" (inst - "x0") (("" (inst -2 "x0") (("" (skosimp*) (("" (inst - "epsilon!1/sqrt(2)") (("" (inst - "epsilon!1/sqrt(2)") (("" (skosimp*) (("" (inst + "min(delta!1,delta!2)") (("" (skosimp*) (("" (inst -1 "x!1") (("" (inst -2 "x!1") (("" (assert) (("" (use-with "sq_lt" 1) (("" (assert) (("" (hide 2) (("" (rewrite "sq_norm") (("" (use-with "sq_lt" -1) (("" (assert) (("" (use-with "sq_lt" -3) (("" (assert) (("" (hide -3 -4) (("" (hide -3) (("" (rewrite "sq_div") (("" (case "sqv((# x := vr1(x!1), y := vr2(x!1) #) - (# x := vr1(x0), y := vr2(x0) #)) = sq(vr1(x!1) - vr1(x0)) + sq(vr2(x!1) - vr2(x0))") (("1" (assert) nil nil) ("2" (hide - 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real nil) (continuous_vr? const-decl "bool" cont_vect2_real 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 nil) (real_minus_real_is_real application-judgement "real" reals nil) (continuous_vr? const-decl "bool" cont_vect2_real nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (- const-decl "Vector" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (< const-decl "bool" reals nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (sq_lt formula-decl nil sq "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sq_div formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "real" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_abs formula-decl nil sq "reals/") (sq_norm formula-decl nil vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 nil)) nil)) (x_cont_vr 0 (x_cont_vr-1 nil 3459094140 ("" (expand "continuous_vr?") (("" (skeep) (("" (expand "continuous_vr?") (("" (skosimp) (("" (inst 1 "epsilon!1") (("" (skosimp) (("" (expand "norm") (("" (case " abs(x(x!1) - x(x0)) <= sqrt(sqv(x!1 - x0))") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (lemma "sq_le") (("2" (inst -1 "abs(x(x!1)-x(x0))" "sqrt(sqv(x!1-x0))") (("2" (assert) (("2" (hide 2) (("2" (rewrite "sqv_sos") (("2" (expand "sos") (("2" (assert) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_le formula-decl nil sq "reals/") (sq_abs formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sqv_sos formula-decl nil vectors_2D "vectors/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sos const-decl "nnreal" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (continuous_vr? const-decl "bool" cont_vect2_real nil) (real_minus_real_is_real application-judgement "real" reals nil) (continuous_vr? const-decl "bool" cont_vect2_real nil)) shostak)) (y_cont_vr 0 (y_cont_vr-1 nil 3459094540 ("" (expand "continuous_vr?") (("" (skeep) (("" (expand "continuous_vr?") (("" (skosimp) (("" (inst 1 "epsilon!1") (("" (skosimp) (("" (expand "norm") (("" (case " abs(y(x!1) - y(x0)) <= sqrt(sqv(x!1 -x0))") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (lemma "sq_le") (("2" (inst -1 "abs(y(x!1)-y(x0))" "sqrt(sqv(x!1-x0))") (("2" (assert) (("2" (hide 2) (("2" (rewrite "sqv_sos") (("2" (expand "sos") (("2" (assert) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_le formula-decl nil sq "reals/") (sq_abs formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sqv_sos formula-decl nil vectors_2D "vectors/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sos const-decl "nnreal" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (continuous_vr? const-decl "bool" cont_vect2_real nil) (real_minus_real_is_real application-judgement "real" reals nil) (continuous_vr? const-decl "bool" cont_vect2_real nil)) nil)) (id_cont_vv 0 (id_cont_vv-1 nil 3445171970 ("" (lemma "cont_vect2_vect2.id_cont_vv_fun") (("" (assert) (("" (expand "continuous_vv") (("" (propax) nil nil)) nil)) nil)) nil) ((id_cont_vv_fun formula-decl nil cont_vect2_vect2 nil)) shostak)) (mult_cont_vr 0 (mult_cont_vr-1 nil 3445173571 ("" (skeep) (("" (typepred "vr1") (("" (typepred "vr2") (("" (lemma "cont_vect2_real.prod_cont_vr_fun") (("" (inst - "vr1" "vr2") (("" (expand "*") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real nil) (continuous_vr? const-decl "bool" cont_vect2_real 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (prod_cont_vr_fun formula-decl nil cont_vect2_real nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")) shostak)) (scal_mult_cont_vr 0 (scal_mult_cont_vr-1 nil 3443885824 ("" (skeep) (("" (lemma "mult_cont_vr") (("" (inst -1 "LAMBDA(v):x" "vr") (("" (rewrite "const_cont_vr") nil nil)) nil)) nil)) nil) ((mult_cont_vr formula-decl nil vect_cont_2D nil) (const_cont_vr formula-decl nil vect_cont_2D nil) (x skolem-const-decl "real" vect_cont_2D nil) (continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real nil) (continuous_vr? const-decl "bool" cont_vect2_real nil) (bool nonempty-type-eq-decl nil booleans 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (div_cont_vr 0 (div_cont_vr-1 nil 3445180419 ("" (skeep) (("" (typepred "vr") (("" (expand "continuous_vr") (("" (lemma "cont_vect2_real.div_cont_vr_fun") (("" (inst - "vr" "vnz") (("" (assert) (("" (expand "/") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real nil) (continuous_vr? const-decl "bool" cont_vect2_real 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals 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 "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (/ const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (div_cont_vr_fun formula-decl nil cont_vect2_real nil)) nil)) (scal_div1_cont_vr 0 (scal_div1_cont_vr-1 nil 3443885918 ("" (skeep) (("" (lemma "div_cont_vr") (("" (inst -1 "vr" "LAMBDA(v):nzx") (("" (assert) (("" (rewrite "const_cont_vr") nil nil)) nil)) nil)) nil)) nil) ((div_cont_vr formula-decl nil vect_cont_2D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (const_cont_vr formula-decl nil vect_cont_2D nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real nil) (continuous_vr? const-decl "bool" cont_vect2_real nil) (bool nonempty-type-eq-decl nil booleans 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (scal_div2_cont_vr 0 (scal_div2_cont_vr-1 nil 3443885989 ("" (skeep) (("" (lemma "div_cont_vr") (("" (inst -1 "LAMBDA(v):x" "vnz") (("1" (assert) nil nil) ("2" (rewrite "const_cont_vr") nil nil)) nil)) nil)) nil) ((div_cont_vr formula-decl nil vect_cont_2D nil) (const_cont_vr formula-decl nil vect_cont_2D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "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) (bool nonempty-type-eq-decl nil booleans nil) (continuous_vr? const-decl "bool" cont_vect2_real nil) (x skolem-const-decl "real" vect_cont_2D nil)) nil)) (add_cont_vv 0 (add_cont_vv-1 nil 3445172614 ("" (skeep) (("" (typepred "vv1") (("" (typepred "vv2") (("" (lemma "sum_cont_vv_fun") (("" (inst - "vv1" "vv2") (("" (expand "+ " -) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vv_fun nonempty-type-eq-decl nil cont_vect2_vect2 nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sum_cont_vv_fun formula-decl nil cont_vect2_vect2 nil) (+ const-decl "[Vect2 -> Vect2]" limit_vect2_vect2 nil)) shostak)) (add_cont_vr 0 (add_cont_vr-2 nil 3473598983 ("" (skeep) (("" (typepred "vr1") (("" (typepred "vr2") (("" (lemma "sum_cont_vr_fun") (("" (inst - "vr1" "vr2") (("" (expand "+ " -1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real nil) (continuous_vr? const-decl "bool" cont_vect2_real 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sum_cont_vr_fun formula-decl nil cont_vect2_real nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")) nil) (add_cont_vr-1 nil 3445172848 ("" (skeep) (("" (typepred "vr1") (("" (typepred "vr2") (("" (expand "continuous_vr") (("" (lemma "cont_vect2_real.sum_cont_fun") (("" (inst - "vr1" "vr2") (("" (assert) (("" (expand "+ ") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vect2 type-eq-decl nil vectors_2D_def "vectors/") (+ const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")) nil)) (add_cont_rv 0 (add_cont_rv-1 nil 3445172935 ("" (skeep) (("" (typepred "rv1") (("" (typepred "rv2") (("" (expand "continuous_rv") (("" (lemma "sum_cont_rv_fun") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_rv_fun nonempty-type-eq-decl nil cont_real_vect2 nil) (continuous_rv? const-decl "bool" cont_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (sum_cont_rv_fun formula-decl nil cont_real_vect2 nil)) nil)) (sub_cont_vv 0 (sub_cont_vv-1 nil 3445172989 ("" (skeep) (("" (typepred "vv1") (("" (typepred "vv2") (("" (expand "continuous_vv") (("" (lemma "diff_cont_vv_fun") (("" (assert) (("" (expand "-") (("" (inst - "vv1" "vv2") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vv_fun nonempty-type-eq-decl nil cont_vect2_vect2 nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (diff_cont_vv_fun formula-decl nil cont_vect2_vect2 nil) (- const-decl "Vector" vectors_2D "vectors/") (- const-decl "[Vect2 -> Vect2]" limit_vect2_vect2 nil)) nil)) (sub_cont_vr 0 (sub_cont_vr-1 nil 3445173027 ("" (skeep) (("" (typepred "vr1") (("" (typepred "vr2") (("" (lemma "diff_cont_vr_fun") (("" (inst - "vr1" "vr2") (("" (expand "-") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real nil) (continuous_vr? const-decl "bool" cont_vect2_real 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (diff_cont_vr_fun formula-decl nil cont_vect2_real nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")) nil)) (sub_cont_rv 0 (sub_cont_rv-2 nil 3473167239 ("" (skeep) (("" (typepred "rv1") (("" (typepred "rv2") (("" (expand "continuous_rv") (("" (lemma "cont_real_vect2.diff_cont_rv_fun") (("" (inst - "rv1" "rv2") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_rv_fun nonempty-type-eq-decl nil cont_real_vect2 nil) (continuous_rv? const-decl "bool" cont_real_vect2 nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (diff_cont_rv_fun formula-decl nil cont_real_vect2 nil)) nil) (sub_cont_rv-1 nil 3445180610 ("" (skeep) (("" (typepred "rv1") (("" (typepred "rv2") (("" (expand "continuous_rv") (("" (lemma "cont_real_vect2.diff_cont_fun") (("" (inst - "rv1" "rv2") (("" (assert) (("" (expand "-") (("" (expand "-") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vect2 type-eq-decl nil vectors_2D_def "vectors/")) nil)) (neg_cont_vr 0 (neg_cont_vr-1 nil 3443886540 ("" (skeep) (("" (lemma "sub_cont_vr") (("" (inst -1 "LAMBDA(v):0" "vr") (("1" (assert) nil nil) ("2" (rewrite "const_cont_vr") nil nil)) nil)) nil)) nil) ((sub_cont_vr formula-decl nil vect_cont_2D nil) (const_cont_vr formula-decl nil vect_cont_2D nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "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) (bool nonempty-type-eq-decl nil booleans nil) (continuous_vr? const-decl "bool" cont_vect2_real nil)) shostak)) (neg_cont_vv 0 (neg_cont_vv-1 nil 3443886609 ("" (skeep) (("" (lemma "sub_cont_vv") (("" (inst -1 "LAMBDA(v):zero" "vv") (("1" (assert) nil nil) ("2" (rewrite "const_cont_vv") nil nil)) nil)) nil)) nil) ((sub_cont_vv formula-decl nil vect_cont_2D nil) (const_cont_vv formula-decl nil vect_cont_2D nil) (sub_zero_left formula-decl nil vectors_2D "vectors/") (continuous_vv_fun nonempty-type-eq-decl nil cont_vect2_vect2 nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 nil) (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/")) shostak)) (neg_cont_rv 0 (neg_cont_rv-1 nil 3443886633 ("" (skeep) (("" (lemma "sub_cont_rv") (("" (inst -1 "LAMBDA(x):zero" "rv") (("1" (assert) nil nil) ("2" (rewrite "const_cont_rv") nil nil)) nil)) nil)) nil) ((sub_cont_rv formula-decl nil vect_cont_2D nil) (const_cont_rv formula-decl nil vect_cont_2D nil) (sub_zero_left formula-decl nil vectors_2D "vectors/") (continuous_rv_fun nonempty-type-eq-decl nil cont_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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (continuous_rv? const-decl "bool" cont_real_vect2 nil) (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/")) shostak)) (scal_scal_cont_vv 0 (scal_scal_cont_vv-1 nil 3443886446 ("" (skeep) (("" (lemma "scal_cont_vv[real]") (("" (inst -1 "LAMBDA(v):y" "vv") (("" (rewrite "const_cont_vr") nil nil)) nil)) nil)) 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) (scal_cont_vv formula-decl nil vect2_cont_dot nil) (const_cont_vr formula-decl nil vect_cont_2D nil) (y skolem-const-decl "real" vect_cont_2D nil) (continuous_vv_fun nonempty-type-eq-decl nil cont_vect2_vect2 nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 nil) (continuous_vr? const-decl "bool" cont_vect2_real nil) (bool nonempty-type-eq-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/")) shostak)) (sqv_cont 0 (sqv_cont-1 nil 3443877907 ("" (expand "sqv") (("" (rewrite "dot_cont_vr[real]") (("" (rewrite "id_cont_vv") nil nil)) nil)) nil) ((dot_cont_vr formula-decl nil vect2_cont_dot nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 nil) (Vector type-eq-decl nil 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) (id_cont_vv formula-decl nil vect_cont_2D nil) (sqv const-decl "nnreal" vectors_2D "vectors/")) nil)) (neg_cont 0 (neg_cont-1 nil 3443886684 ("" (lemma "neg_cont_vv") (("" (inst -1 "id") (("1" (expand "id") (("1" (case-replace "(LAMBDA(v):-v) = vectors_2D.-") (("1" (hide-all-but 1) (("1" (decompose-equality 1) nil nil)) nil)) nil)) nil) ("2" (expand "id") (("2" (rewrite "id_cont_vv") nil nil)) nil)) nil)) nil) ((id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.100 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.Bot Zugriff |
