|
(space_3D
(conflict_symm 0
(conflict_symm-1 nil 3471198645
("" (skeep)
((""
(case "FORALL (s,v) : conflict?(s,v) IMPLIES conflict?(-s,-v)")
(("1" (split)
(("1" (flatten)
(("1" (inst -2 "-s" "-v") (("1" (assert) nil nil)) nil)) nil)
("2" (inst? -1) nil nil))
nil)
("2" (hide 2)
(("2" (skolem 1 ("sp" "vp"))
(("2" (flatten)
(("2" (expand "conflict?")
(("2" (skeep -1)
(("2" (inst 1 "nnt")
(("2" (split 1)
(("1" (hide -2) (("1" (grind) nil nil)) nil)
("2" (hide -1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((- const-decl "Vector" vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(conflict? const-decl "bool" space_3D nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(neg_neg formula-decl nil vectors_3D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal 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)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(conflict_ever 0
(conflict_ever-1 nil 3470158403
("" (skeep)
(("" (expand* "conflict?" "conflict_ever?")
(("" (skeep -1) (("" (inst? 1) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((conflict_ever? const-decl "bool" space_3D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(conflict? const-decl "bool" space_3D 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(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)
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil))
(conflict_ever_shift 0
(conflict_ever_shift-1 nil 3470158447
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (expand "conflict_ever?")
(("1" (skolem -1 "tt")
(("1" (inst 1 "tt-t")
(("1" (flatten)
(("1" (split)
(("1" (hide -2)
(("1" (expand* "+" "*") (("1" (assert) nil nil))
nil))
nil)
("2" (hide -1)
(("2" (rewrite "vect2_add")
(("2" (rewrite "vect2_scal")
(("2"
(case-replace
"vect2(s) + tt * vect2(v) = vect2(s) + t * vect2(v) + (tt - t) * vect2(v)")
(("2" (hide-all-but 1)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "conflict_ever?")
(("2" (skolem -1 "tt")
(("2" (inst 1 "tt+t")
(("2" (flatten)
(("2" (split)
(("1" (hide -2)
(("1" (expand* "+" "*") (("1" (assert) nil nil))
nil))
nil)
("2" (hide -1)
(("2"
(case-replace
"vect2(s + t * v) + tt * vect2(v) = vect2(s) + (tt + t) * vect2(v)")
(("2" (hide-all-but 1)
(("2" (rewrite "vect2_add")
(("2" (rewrite "vect2_scal")
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(conflict_ever? const-decl "bool" space_3D nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "Vector" vectors_3D "vectors/")
(+ const-decl "Vector" vectors_3D "vectors/")
(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)
(Vector type-eq-decl nil vectors_3D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(vect2_add formula-decl nil vect_3D_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(vect2_scal formula-decl nil vect_3D_2D "vectors/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(conflict_sum_closed 0
(conflict_sum_closed-2 nil 3467454344
("" (skeep)
(("" (expand "conflict?")
(("" (skosimp*)
(("" (case "nnt!1 = 0 and nnt!2 = 0")
(("1" (flatten)
(("1" (inst + "0")
(("1" (assert)
(("1" (replace -1) (("1" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (name "tt" "nnt!2/(nnt!1 + nnt!2)")
(("1" (label "ttname" -1)
(("1" (case "0<=tt AND tt<=1")
(("1" (flatten)
(("1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)")
(("1" (label "newtname" -1)
(("1"
(case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt")
(("1" (flatten)
(("1" (label "newttt" -1)
(("1" (label "newtomtt" -2)
(("1"
(inst + "newt")
(("1"
(name
"VV"
"vect2(s) + nnt!1 * vect2(v)")
(("1"
(label "vvname" -1)
(("1"
(name
"WW"
"vect2(s) + nnt!2 * vect2(w)")
(("1"
(label "wwname" -1)
(("1"
(name
"VVz"
"s`z + nnt!1 * v`z")
(("1"
(label "vvzname" -1)
(("1"
(name
"WWz"
"s`z + nnt!2 * w`z")
(("1"
(label "wwzname" -1)
(("1"
(name
"VVt"
"s+nnt!1*v")
(("1"
(label
"vvtname"
-1)
(("1"
(name
"WWt"
"s+nnt!2*w")
(("1"
(label
"wwtname"
-1)
(("1"
(replace
"wwzname")
(("1"
(replace
"vvzname")
(("1"
(replace
"wwname")
(("1"
(replace
"vvname")
(("1"
(lemma
"horiz_dist_convex_scaf")
(("1"
(inst
-
"VVt"
"WWt-VVt")
(("1"
(case
"s`z + newt * (v + w)`z = tt*VVz + (1-tt)*WWz AND vect2(s) + newt * vect2(v + w) = tt*VV+(1-tt)*WW")
(("1"
(flatten)
(("1"
(label
"zfin"
-1)
(("1"
(label
"vectfin"
-2)
(("1"
(replace
"zfin")
(("1"
(replace
"vectfin")
(("1"
(case
"convex?(LAMBDA (t): abs(t)-H)")
(("1"
(assert)
(("1"
(lemma
"convex_wtd_av_lt")
(("1"
(inst-cp
-
"0"
"LAMBDA (t): abs(t) - H"
"VVz"
"WWz")
(("1"
(inst
-
"0"
"LAMBDA (t): horiz_dist_scaf(VVt)(t, WWt - VVt)"
"0"
"1")
(("1"
(assert)
(("1"
(expand
"horiz_dist_scaf"
-1
1)
(("1"
(expand
"horiz_dist_scaf"
-1
1)
(("1"
(assert)
(("1"
(case
"vect2(VVt) = VV AND vect2(VVt)+vect2(WWt-VVt) = WW")
(("1"
(flatten)
(("1"
(assert)
(("1"
(inst
-
"tt")
(("1"
(inst
-
"tt")
(("1"
(assert)
(("1"
(expand
"horiz_dist_scaf")
(("1"
(case-replace
"vect2(VVt) + (1 - tt) * vect2(WWt - VVt) = tt * VV + (1 - tt) * WW")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
(-1
-2
1))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
("vvtname"
"vvname"
"wwtname"
"wwname"
1))
(("2"
(replace
"wwtname"
+
rl)
(("2"
(replace
"vvtname"
+
rl)
(("2"
(replace
"vvname"
+
rl)
(("2"
(replace
"wwname"
+
rl)
(("2"
(rewrite
"vect2_add")
(("2"
(rewrite
"vect2_sub")
(("2"
(rewrite
"vect2_add")
(("2"
(rewrite
"vect2_add")
(("2"
(rewrite
"vect2_scal")
(("2"
(rewrite
"vect2_scal")
(("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))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"abs_linear_convex")
(("2"
(inst
-
"H"
"0"
"1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
"vvname"
+
rl)
(("2"
(replace
"wwname"
+
rl)
(("2"
(replace
"vvzname"
+
rl)
(("2"
(replace
"wwzname"
+
rl)
(("2"
(assert)
(("2"
(hide
(2
3
4
5))
(("2"
(split
1)
(("1"
(copy
"newtomtt")
(("1"
(mult-by
-1
"w`z")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(replace
"newttt"
+
rl)
(("1"
(rewrite
"vz_distr_add")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
("newttt"
"newtomtt"
1))
(("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)
("2"
(lemma
"nnreal_div_posreal_is_nnreal")
(("2"
(inst
-
"(nnt!1*nnt!2)"
"nnt!1 + nnt!2")
(("1"
(hide-all-but (-1 "newtname" 1))
(("1" (grind) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace "newtname" + rl)
(("2" (replace "ttname" + rl)
(("2" (hide-all-but (1 2))
(("2"
(ground)
(("2" (field 2) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "nnreal_div_posreal_is_nnreal")
(("2" (inst - "nnt!2" "nnt!1 + nnt!2")
(("1" (replace "ttname" -)
(("1" (assert)
(("1" (replace "ttname" + rl)
(("1" (cross-mult 1) (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(conflict? const-decl "bool" space_3D nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(add_zero_right formula-decl nil vectors_2D "vectors/")
(scal_0 formula-decl nil vectors_2D "vectors/")
(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)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(div_mult_pos_le1 formula-decl nil real_props nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(div_cancel2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nnreal_div_posreal_is_nnreal judgement-tcc nil real_types nil)
(nnt!2 skolem-const-decl "nnreal" space_3D nil)
(nnt!1 skolem-const-decl "nnreal" space_3D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(+ const-decl "Vector" vectors_3D "vectors/")
(* const-decl "Vector" vectors_3D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(horiz_dist_convex_scaf formula-decl nil horizontal_dist_convexity
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)
(D formal-const-decl "posreal" space_3D nil)
(convex? const-decl "bool" convex_functions "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(H formal-const-decl "posreal" space_3D nil)
(convex_wtd_av_lt formula-decl nil convex_functions "reals/")
(horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil)
(scal_1 formula-decl nil vectors_2D "vectors/")
(vect2_sub formula-decl nil vect_3D_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(vect2_scal formula-decl nil vect_3D_2D "vectors/")
(vect2_add formula-decl nil vect_3D_2D "vectors/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_linear_convex formula-decl nil convex_functions "reals/")
(vz_distr_add formula-decl nil vectors_3D "vectors/")
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(- const-decl "Vector" vectors_3D "vectors/")
(newt skolem-const-decl "real" space_3D nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals 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)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil)
(conflict_sum_closed-1 nil 3467382877
("" (skeep)
(("" (expand "conflict?")
(("" (skolem -1 "ntt1")
(("" (skolem -2 "ntt2")
(("" (flatten)
(("" (rewrite "vect2_add") (("" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(conflict_is_an_open_set 0
(conflict_is_an_open_set-1 nil 3566319824
("" (skeep)
(("" (expand "conflict?" -1)
(("" (skosimp*)
(("" (label "underH" -1)
(("" (label "underD" -2)
(("" (case "nnt!1 /= 0")
(("1" (flatten)
(("1" (name "del1" "H - abs(ss`z + nnt!1 * vv`z)")
(("1" (label "del1name" -1)
(("1"
(name "del2"
"D - norm(vect2(ss) + nnt!1 * vect2(vv))")
(("1" (label "del2name" -1)
(("1" (case "del2 > 0")
(("1" (label "del2pos" -1)
(("1" (hide "del2pos")
(("1"
(name "delta" "min(del1,del2)")
(("1"
(label "deltaname" -1)
(("1"
(inst + "delta/(2*nnt!1)")
(("1"
(skeep 2)
(("1"
(case
"norm(ww) >= abs(ww`z) AND norm(ww) >= norm(vect2(ww))")
(("1"
(label "normlem" -1)
(("1"
(hide "normlem")
(("1"
(expand "conflict?")
(("1"
(inst + "nnt!1")
(("1"
(split 2)
(("1"
(lemma "triangle")
(("1"
(rewrite
"vz_distr_add")
(("1"
(assert)
(("1"
(inst
-
"ss`z + vv`z*nnt!1"
"ww`z*nnt!1")
(("1"
(case
"abs(ww`z*nnt!1) < del1")
(("1"
(assert)
nil
nil)
("2"
(hide 2)
(("2"
(rewrite
"abs_mult")
(("2"
(case
"abs(nnt!1) = nnt!1")
(("1"
(replace
-1)
(("1"
(reveal
"normlem")
(("1"
(flatten)
(("1"
(div-by
1
"nnt!1")
(("1"
(case
"del1 / nnt!1 >= delta / (2 * nnt!1)")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(cross-mult
1)
(("2"
(div-by
1
"nnt!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"abs")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"norm(vect2(ss) + nnt!1 * vect2(vv + ww)) < D")
(("1"
(lemma "sq_lt")
(("1"
(inst?)
(("1"
(assert)
(("1"
(lemma
"vectors_2D.sqrt_sqv_norm")
(("1"
(inst?)
(("1"
(replace
-1
:dir
rl)
(("1"
(rewrite
"vect2_add")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite
"vect2_add")
(("2"
(lemma
"vectors_2D.norm_add_le")
(("2"
(inst
-
"vect2(ss) + nnt!1*vect2(vv)"
"nnt!1*vect2(ww)")
(("2"
(assert)
(("2"
(case
"norm(nnt!1 * vect2(ww)) + norm(vect2(ss) + nnt!1 * vect2(vv)) < D")
(("1"
(case
"vect2(ss) + nnt!1 * vect2(vv) + nnt!1 * vect2(ww) = vect2(ss) + nnt!1 * (vect2(vv) + vect2(ww))")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(case
"norm(nnt!1*vect2(ww)) < del2")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(hide
2)
(("2"
(rewrite
"norm_scal")
(("2"
(case
"abs(nnt!1) = nnt!1")
(("1"
(replace
-1)
(("1"
(div-by
1
"nnt!1")
(("1"
(case
"del2 / nnt!1 >= delta/(2*nnt!1)")
(("1"
(reveal
"normlem")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
2)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.89Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
