| products/Sources/formale Sprachen/PVS/vect_analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: AbstractTask.vdmrt Sprache: LispOriginal von: PVS© |
|
||||||
|
(vect_vect_2D_continuity
(div_vvr_TCC1 0 (div_vvr_TCC1-1 nil 3515487776 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (nzero_vvr? const-decl "bool" vect_vect_2D_continuity nil) (/= const-decl "boolean" notequal nil)) nil)) (sum_vvv_cont 0 (sum_vvv_cont-1 nil 3515488189 ("" (skeep) (("" (expand "continuous_vvv?") (("" (skeep) (("" (typepred "ffvc") (("" (typepred "ggvc") (("" (expand "continuous_vvv?") (("" (inst - "epsil/2" "s" "nzv") (("" (inst - "epsil/2" "s" "nzv") (("" (skosimp*) (("" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)") (("" (skeep) (("" (inst - "sp" "nzvp") (("" (inst - "sp" "nzvp") (("" (assert) (("" (expand "sum_vvv") (("" (lemma "norm_add_le") (("" (inst - "ffvc(s,nzv) - ffvc(sp,nzvp)" "ggvc(s,nzv) - ggvc(sp,nzvp)") (("" (grind :exclude ("norm" "min")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vvv? const-decl "bool" vect_vect_2D_continuity nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (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) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (norm_add_le formula-decl nil vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "Vector" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (sum_vvv const-decl "Vect2" vect_vect_2D_continuity nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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) (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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sum_vvr_cont 0 (sum_vvr_cont-1 nil 3515494507 ("" (skeep) (("" (expand "continuous_vvr?") (("" (skeep) (("" (typepred "ffrc") (("" (typepred "ggrc") (("" (expand "continuous_vvr?") (("" (inst - "epsil/2" "s" "nzv") (("" (inst - "epsil/2" "s" "nzv") (("" (skosimp*) (("" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)") (("" (skeep) (("" (inst - "sp" "nzvp") (("" (inst - "sp" "nzvp") (("" (assert) (("" (expand "sum_vvr") (("" (lemma "triangle") (("" (inst - "ffrc(s,nzv) - ffrc(sp,nzvp)" "ggrc(s,nzv) - ggrc(sp,nzvp)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (continuous_vvr? const-decl "bool" vect_vect_2D_continuity 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) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (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) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (triangle formula-decl nil real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sum_vvr const-decl "real" vect_vect_2D_continuity nil) (real_plus_real_is_real application-judgement "real" reals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (diff_vvv_cont 0 (diff_vvv_cont-2 nil 3515488435 ("" (skeep) (("" (expand "continuous_vvv?") (("" (skeep) (("" (typepred "ffvc") (("" (typepred "ggvc") (("" (expand "continuous_vvv?") (("" (inst - "epsil/2" "s" "nzv") (("" (inst - "epsil/2" "s" "nzv") (("" (skosimp*) (("" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)") (("" (skeep) (("" (inst - "sp" "nzvp") (("" (inst - "sp" "nzvp") (("" (assert) (("" (expand "diff_vvv") (("" (lemma "norm_add_le") (("" (inst - "ffvc(s,nzv) - ffvc(sp,nzvp)" "ggvc(sp,nzvp) - ggvc(s,nzv)") (("" (lemma "norm_neg") (("" (inst - "ggvc(sp, nzvp) - ggvc(s, nzv)") (("" (grind :exclude ("norm" "min")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vvv? const-decl "bool" vect_vect_2D_continuity nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (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) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (norm_add_le formula-decl nil vectors_2D "vectors/") (norm_neg formula-decl nil vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "Vector" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (diff_vvv const-decl "Vect2" vect_vect_2D_continuity nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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) (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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil) (diff_vvv_cont-1 nil 3515488366 ("" (skeep) (("" (expand "continuous_vvv?") (("" (skeep) (("" (typepred "ffvc") (("" (typepred "ggvc") (("" (expand "continuous_vvv?") (("" (inst - "epsil/2" "s" "nzv") (("" (inst - "epsil/2" "s" "nzv") (("" (skosimp*) (("" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)") (("" (skeep) (("" (inst - "sp" "nzvp") (("" (inst - "sp" "nzvp") (("" (assert) (("" (expand "sum_vvv") (("" (lemma "norm_add_le") (("" (inst - "ffvc(s,nzv) - ffvc(sp,nzvp)" "ggvc(s,nzv) - ggvc(sp,nzvp)") (("" (grind :exclude ("norm" "min")) nil)))))))))))))))))))))))))))))))))) nil) nil nil)) (scal_vvv_cont 0 (scal_vvv_cont-1 nil 3515833806 ("" (skeep) (("" (typepred "ffvc") (("" (expand "continuous_vvv?") (("" (skosimp*) (("" (inst - "epsil!1/(abs(c)+1)" "s!1" "nzv!1") (("" (skosimp*) (("" (inst + "ds!1" "dv!1") (("" (skosimp*) (("" (inst - "sp!1" "nzvp!1") (("" (assert) (("" (expand "scal_vvv") (("" (lemma "norm_scal") (("" (inst - "c" "ffvc(s!1, nzv!1) - ffvc(sp!1, nzvp!1)") (("" (assert) (("" (case "c * (ffvc(s!1, nzv!1) - ffvc(sp!1, nzvp!1))=c * ffvc(s!1, nzv!1) - c * ffvc(sp! (("1" (replace -1) (("1" (hide -1) (("1" (case "abs(c) * norm(ffvc(s!1, nzv!1) - ffvc(sp!1, nzvp!1)) < epsil!1") (("1" (assert) nil nil) ("2" (hide (-1 2)) (("2" (cross-mult -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_vvv? const-decl "bool" vect_vect_2D_continuity nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (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) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (norm_scal formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (< const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_2D "vectors/") (div_mult_pos_lt2 formula-decl nil real_props nil) (* const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "Vector" vectors_2D "vectors/") (scal_vvv const-decl "Vect2" vect_vect_2D_continuity nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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) (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) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (dot_vvv_cont 0 (dot_vvv_cont-2 nil 3515489053 ("" (skeep) (("" (expand "continuous_vvr?") (("" (skosimp*) (("" (typepred "ffvc") (("" (typepred "ggvc") (("" (expand "continuous_vvv?") (("" (label "fcont" -2) (("" (label "gcont" -1) (("" (name "ep1" "epsil!1/(8*norm(ggvc(s!1,nzv!1))+1)") (("" (name "ep2" "epsil!1/(8*(norm(ffvc(s!1,nzv!1)) + ep1))") (("" (label "ep1name" -2) (("" (label "ep2name" -1) (("" (inst - "ep2" "s!1" "nzv!1") (("" (inst - "ep1" "s!1" "nzv!1") (("" (skosimp*) (("" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)") (("" (skosimp*) (("" (inst - "sp!1" "nzvp!1") (("" (inst - "sp!1" "nzvp!1") (("" (assert) (("" (expand "dot_vvv") (("" (lemma "triangle") (("" (inst - "ffvc(s!1,nzv!1) * ggvc(s!1,nzv!1) - ffvc(sp!1,nzvp!1) * ggvc(s!1,nzv!1)" " ffvc(sp!1,nzvp!1) * ggvc(s!1,nzv!1) - ffvc(sp!1,nzvp!1) * ggvc(sp!1,nzvp!1)") (("" (assert) (("" (lemma "schwarz") (("" (inst - "ffvc(s!1,nzv!1)-ffvc(sp!1,nzvp!1)" "ggvc(s!1,nzv!1)") (("" (assert) (("" (lemma "schwarz") (("" (inst - "ffvc(sp!1,nzvp!1)" "ggvc(s!1,nzv!1) - ggvc(sp!1,nzvp!1)") (("" (assert) (("" (rewrite "dot_sub_right") (("" (rewrite "dot_sub_left") (("" (case "norm(ffvc(s!1, nzv!1) - ffvc(sp!1, nzvp!1)) * norm(ggvc(s!1, nzv!1)) + norm(ffv norm(ggvc(s!1, nzv!1) - ggvc(sp!1, nzvp!1))<epsil!1") (("1" (assert) nil nil) ("2" (hide (-1 -2 -3 2)) (("2" (case "norm(ffvc(sp!1,nzvp!1)) <= norm(ffvc(s!1,nzv!1)) + ep1") (("1" (replace "ep1name" - rl) (("1" (hide "ep1name") (("1" (replace "ep2name" - rl) (("1" (hide "ep2name") (("1" (name "A" "ffvc(s!1,nzv!1)") (("1" (name "B" "ffvc(sp!1,nzvp!1)") (("1" (name "X" "ggvc(s!1,nzv!1)") (("1" (name "Y" "ggvc(sp!1,nzvp!1)") (("1" (label "yname" -1) (("1" (label "xname" -2) (("1" (label "bname" -3) (("1" (label "aname" -4) (("1" (replace "aname") (("1" (replace "bname") (("1" (replace "xname") (("1" (replace "yname") (("1" (hide "aname") (("1" (hide "bname") (("1" (hide "xname") (("1" (hide "yname") (("1" (copy "gcont") (("1" (reveal "ep1name") (("1" (reveal "xname") (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (name "myvar" "norm(A) + epsil!1 / (1+8 * norm(X))") (("1" (label "namemyvar" -1) (("1" (case "norm(A - B) * norm(X) < epsil!1/2 AND norm(B) * norm(X - Y) <= epsil!1/2") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (case "ep1*norm(X) < epsil!1/2") (("1" (copy "fcont") (("1" (mult-by -1 "norm(X)") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (replace "ep1name" + :dir rl) (("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (copy -4) (("2" (mult-by -1 "norm(X-Y)") (("2" (copy -4) (("2" (cross-mult -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but ("fcont" 1)) (("2" (lemma "norm_add_le") (("2" (inst - "ffvc(s!1, nzv!1)-ffvc(sp!1, nzvp!1)" "-ffvc(s!1, nzv!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (continuous_vvr? const-decl "bool" vect_vect_2D_continuity nil) (continuous_vvv? const-decl "bool" vect_vect_2D_continuity nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (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) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (triangle formula-decl nil real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "Vector" vectors_2D "vectors/") (dot_sub_left formula-decl nil vectors_2D "vectors/") (norm_add_le formula-decl nil vectors_2D "vectors/") (sub_cancel formula-decl nil vectors_2D "vectors/") (add_neg_sub formula-decl nil vectors_2D "vectors/") (norm_neg formula-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div2 formula-decl nil real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (X skolem-const-decl "Vect2" vect_vect_2D_continuity nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (< const-decl "bool" reals nil) (dot_sub_right formula-decl nil vectors_2D "vectors/") (schwarz formula-decl nil vectors_2D "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (dot_vvv const-decl "real" vect_vect_2D_continuity nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (>= 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_2D "vectors/")) nil) (dot_vvv_cont-1 nil 3515488825 ("" (postpone) nil nil) nil shostak)) (prod_vvr_cont 0 (prod_vvr_cont-1 nil 3515496006 ("" (skeep) (("" (name "fffv" "LAMBDA (s,nzv): (# x:= ffrc(s,nzv), y:= 0 #)") (("" (name "gggv" "LAMBDA (s,nzv): (# x:= ggrc(s,nzv), y:= 0 #)") (("" (lemma "dot_vvv_cont") (("" (inst - "fffv" "gggv") (("1" (hide -2 -3) (("1" (expand "dot_vvv") (("1" (expand "prod_vvr") (("1" (expand "gggv") (("1" (expand "fffv") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "continuous_vvv?") (("2" (typepred "ggrc") (("2" (expand "continuous_vvr?") (("2" (skosimp*) (("2" (inst - "epsil!1" "s!1" "nzv!1") (("2" (skosimp*) (("2" (inst + "ds!1" "dv!1") (("2" (skosimp*) (("2" (inst - "sp!1" "nzvp!1") (("2" (assert) (("2" (rewrite "sqrt_sqv_norm" 1 :dir rl) (("2" (case "FORALL (vvww:Vect2): sqv(vvww) = sq(vvww`x) + sq(vvww`y)") (("1" (rewrite -1) (("1" (expand "gggv" +) (("1" (expand "-" +) (("1" (rewrite "sq_0") (("1" (assert) (("1" (case "FORALL (aaa:real): sqrt(sq(aaa)) = abs(aaa)") (("1" (rewrite -1 1) nil nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (case "aaa>=0") (("1" (grind) nil nil) ("2" (lemma "sqrt_sq") (("2" (inst - "-aaa") (("2" (rewrite "sq_neg") (("2" (split -) (("1" (replace -1) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "continuous_vvv?") (("3" (typepred "ffrc") (("3" (expand "continuous_vvr?") (("3" (skosimp*) (("3" (inst - "epsil!1" "s!1" "nzv!1") (("3" (skosimp*) (("3" (inst + "ds!1" "dv!1") (("3" (skosimp*) (("3" (inst - "sp!1" "nzvp!1") (("3" (assert) (("3" (rewrite "sqrt_sqv_norm" 1 :dir rl) (("3" (case "FORALL (vvww:Vect2): sqv(vvww) = sq(vvww`x) + sq(vvww`y)") (("1" (rewrite -1) (("1" (expand "fffv" +) (("1" (expand "-" +) (("1" (rewrite "sq_0") (("1" (assert) (("1" (case "FORALL (aaa:real): sqrt(sq(aaa)) = abs(aaa)") (("1" (rewrite -1 1) nil nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (case "aaa>=0") (("1" (grind) nil nil) ("2" (lemma "sqrt_sq") --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.97Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Entwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
