|
(circle_optimum_2D
(intersects_circle_fun_scal 0
(intersects_circle_fun_scal-1 nil 3527949260
(""
(case "FORALL (R: posreal, c: Vect2, k: posreal, v: Vect2):
intersects_circle_fun?(v, c, R) IMPLIES
intersects_circle_fun?(k * v, c, R)")
(("1" (skeep)
(("1" (ground)
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (inst - "R" "c" "1/k" "k*v") (("2" (assert) nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skeep)
(("2" (expand "intersects_circle_fun?")
(("2" (flatten)
(("2" (case "v = zero")
(("1" (assert)
(("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)
("2" (case "k*v /= zero")
(("1" (assert)
(("1" (flatten)
(("1" (lemma "Delta_scal[R]")
(("1" (inst - "-c" "k" "v")
(("1" (replace -1)
(("1" (hide -1)
(("1" (mult-by -1 "sq(k)")
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
(("1"
(mult-by -2 "k")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (1 2))
(("2" (flatten)
(("2" (expand "zero")
(("2" (decompose-equality -1)
(("2" (decompose-equality +)
(("1" (mult-by 1 "k")
(("1" (rewrite "vx_scal")
(("1" (assert) nil nil)) nil))
nil)
("2" (mult-by 1 "k")
(("2" (rewrite "vy_scal")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(scal_zero formula-decl nil vectors_2D "vectors/")
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(sqv_neg formula-decl nil vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(vx_scal formula-decl nil vectors_2D "vectors/")
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(vy_scal formula-decl nil vectors_2D "vectors/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(Delta_scal formula-decl nil horizontal nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(sq const-decl "nonneg_real" sq "reals/")
(Delta const-decl "real" horizontal nil)
(* const-decl "real" vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(- const-decl "Vector" vectors_2D "vectors/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
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)
(scal_assoc formula-decl nil vectors_2D "vectors/")
(scal_1 formula-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)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(intersects_circle_fun? const-decl "bool" circle_optimum_2D nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/"))
shostak))
(intersects_circle_fun_def 0
(intersects_circle_fun_def-1 nil 3527524122
("" (skeep)
(("" (case "v = zero")
(("1" (replace -1)
(("1" (expand "intersects_circle_fun?")
(("1" (expand "circle?")
(("1" (expand "segment?")
(("1" (ground)
(("1" (inst + "zero")
(("1" (assert)
(("1" (rewrite "sq_eq" 1 :dir rl)
(("1" (rewrite "sq_norm") nil nil)) nil))
nil))
nil)
("2" (skeep -1)
(("2" (skeep -2)
(("2" (replace -2)
(("2" (assert)
(("2" (rewrite "sqrt_eq" 1 :dir rl)
(("2" (rewrite "sqrt_sqv_norm") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (ground)
(("1" (expand "intersects_circle_fun?")
(("1" (flatten)
(("1" (inst + "Theta_D[R](-c,v,1)*v")
(("1" (split +)
(("1" (expand "circle?")
(("1" (lemma "Theta_D_unique[R]")
(("1" (inst - "v" "-c" "Theta_D[R](-c, v, 1)")
(("1" (assert)
(("1" (rewrite "sqrt_eq" :dir rl)
(("1" (rewrite "sqrt_sqv_norm")
(("1" (hide-all-but (-1 1))
(("1"
(grind :exclude ("norm" "Theta_D"))
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "segment?")
(("2" (inst?)
(("2" (lemma "Theta_D_ge_0[R]")
(("2" (case "NOT sqv(-c) <= sq(R)")
(("1" (assert)
(("1" (inst?)
(("1" (assert)
(("1"
(split -)
(("1"
(lemma "Theta_D_le[R]")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide-all-but (-2 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide -4)
(("2" (hide -2)
(("2"
(lemma
"horizontal_los_inside_Theta[R]")
(("2"
(inst?)
(("2"
(inst - "0")
(("2"
(assert)
(("2"
(lemma "Theta_D_unique[R]")
(("2"
(inst?)
(("2"
(inst - "0")
(("2"
(assert)
(("2"
(lemma "Theta_D_le[R]")
(("2"
(inst?)
(("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)
("2" (skeep -)
(("2" (expand "segment?")
(("2" (skeep -2)
(("2" (replaces -2)
(("2" (expand "intersects_circle_fun?")
(("2" (case "NOT Delta[R](-c, v) >= 0")
(("1" (hide 2)
(("1" (rewrite "Delta_ge_0")
(("1" (inst + "t")
(("1" (expand "circle?")
(("1" (rewrite "sqrt_eq" 1 :dir rl)
(("1"
(rewrite "sqrt_sqv_norm")
(("1" (grind :exclude "norm") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (flatten)
(("2" (case "t = 0")
(("1" (replace -1)
(("1" (expand "circle?")
(("1"
(assert)
(("1"
(rewrite "sqrt_le" 2 :dir rl)
(("1"
(rewrite "sqrt_sqv_norm")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "circle?")
(("2"
(lemma "horizontal_conflict[norm(c)]")
(("1"
(inst - "v" "-c")
(("1"
(flatten)
(("1"
(hide -2)
(("1"
(split -)
(("1"
(flatten)
(("1"
(split -)
(("1"
(hide-all-but -1)
(("1"
(rewrite
"sqrt_lt"
:dir
rl)
(("1"
(assert)
(("1"
(rewrite
"sqrt_sqv_norm")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 2))
(("2" (grind) nil nil))
nil))
nil))
nil)
("2"
(expand "horizontal_conflict?")
(("2"
(inst + "t")
(("2"
(rewrite
"sqrt_lt"
1
:dir
rl)
(("2"
(assert)
(("2"
(rewrite
"sqrt_sqv_norm")
(("2"
(rewrite
"sqrt_le"
4
:dir
rl)
(("2"
(rewrite
"sqrt_sqv_norm")
(("2"
(assert)
(("2"
(hide -1)
(("2"
(grind
:exclude
"norm")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "norm_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(replace -1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(intersects_circle_fun? const-decl "bool" circle_optimum_2D nil)
(segment? const-decl "bool" circle_optimum_2D nil)
(sqrt_eq formula-decl nil sqrt "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(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)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_sqv_norm formula-decl nil vectors_2D "vectors/")
(sq_eq formula-decl nil sq "reals/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(sq_norm formula-decl nil vectors_2D "vectors/")
(norm_neg formula-decl nil vectors_2D "vectors/")
(sub_zero_left formula-decl nil vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(scal_zero formula-decl nil vectors_2D "vectors/")
(circle? const-decl "bool" circle_optimum_2D nil)
(sqrt_le formula-decl nil sqrt "reals/")
(horizontal_conflict formula-decl nil horizontal nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqrt_lt formula-decl nil sqrt "reals/")
(horizontal_conflict? const-decl "bool" horizontal nil)
(dot_zero_left formula-decl nil vectors_2D "vectors/")
(sub_zero_right formula-decl nil vectors_2D "vectors/")
(neg_zero formula-decl nil vectors_2D "vectors/")
(norm_zero formula-decl nil vectors_2D "vectors/")
(norm_eq_0 formula-decl nil vectors_2D "vectors/")
(Delta_ge_0 formula-decl nil horizontal nil)
(v skolem-const-decl "Vect2" circle_optimum_2D nil)
(c skolem-const-decl "Vect2" circle_optimum_2D nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Delta const-decl "real" horizontal nil)
(R skolem-const-decl "posreal" circle_optimum_2D nil)
(* const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(Theta_D const-decl "real" horizontal nil)
(Theta_D_ge_0 formula-decl nil horizontal nil)
(scal_0 formula-decl nil vectors_2D "vectors/")
(add_zero_right formula-decl nil vectors_2D "vectors/")
(horizontal_los_inside_Theta formula-decl nil horizontal nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(* const-decl "real" vectors_2D "vectors/")
(Theta_D_le formula-decl nil horizontal nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(<= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(sqv_neg formula-decl nil vectors_2D "vectors/")
(Theta_D_unique formula-decl nil horizontal nil))
nil))
(intersects_circle_fun_inc 0
(intersects_circle_fun_inc-1 nil 3527947389
(""
(case "FORALL (R: posreal, c: Vect2, u, v: Vect2): sqv(u) = 1 AND sqv(v) = 1 AND
intersects_circle_fun?(v, c, R) AND ^(v) * c <= ^(u) * c IMPLIES
intersects_circle_fun?(u, c, R)")
(("1" (skeep)
(("1" (inst - "R" "c" "^(u)" "^(v)")
(("1" (assert)
(("1" (split -)
(("1" (lemma "intersects_circle_fun_scal")
(("1" (inst - "R" "c" "1/norm(u)" "u")
(("1" (assert)
(("1" (expand "^") (("1" (propax) nil nil)) nil))
nil)
("2" (split +)
(("1" (cross-mult 1)
(("1" (ground)
(("1" (lemma "norm_eq_0")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (cross-mult 1)
(("2" (ground)
(("2" (lemma "norm_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (ground)
(("3" (lemma "norm_eq_0")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (expand "^")
(("2" (rewrite "sqv_scal")
(("2" (rewrite "sq_div")
(("1" (rewrite "sq_norm") (("1" (assert) nil nil))
nil)
("2" (lemma "norm_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("3" (expand "^")
(("3" (rewrite "sqv_scal")
(("3" (rewrite "sq_div")
(("1" (rewrite "sq_norm") (("1" (assert) nil nil))
nil)
("2" (lemma "norm_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("4" (lemma "intersects_circle_fun_scal")
(("4" (inst - "R" "c" "1/norm(v)" "v")
(("1" (assert)
(("1" (expand "^") (("1" (propax) nil nil)) nil))
nil)
("2" (split +)
(("1" (cross-mult 1)
(("1" (ground)
(("1" (lemma "norm_eq_0")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (cross-mult 1)
(("2" (ground)
(("2" (lemma "norm_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (lemma "norm_eq_0")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil)
("5" (case "FORALL (zpt:Nz_vect2): ^(^(zpt)) = ^(zpt)")
(("1" (inst-cp - "u")
(("1" (inst - "v") (("1" (assert) nil nil)) nil)) nil)
("2" (hide-all-but 1)
(("2" (skeep)
(("2" (expand "^" + 1)
(("2" (typepred "^(zpt)")
(("2" (assert)
(("2" (replace -1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skeep)
(("2" (label "sqvuv" (-1 -2))
(("2" (case "^(v) = v AND ^(u) = u")
(("1" (flatten)
(("1" (replaces -1)
(("1" (replaces -1)
(("1" (hide "sqvuv")
(("1" (expand "intersects_circle_fun?")
(("1" (case "NOT (v = zero OR u = zero)")
(("1" (flatten)
(("1" (assert)
(("1" (flatten)
(("1"
(label "uvnz" (1 2))
(("1"
(hide "uvnz")
(("1"
(case
"FORALL (bl1,bl2:bool): (bl1 OR bl2) IFF (bl1 OR (bl2 AND not bl1))")
(("1"
(label "final" 1)
(("1"
(hide "final")
(("1"
(rewrite -1)
(("1"
(hide -1)
(("1"
(reveal "final")
(("1"
(split -)
(("1"
(split +)
(("1"
(expand "Delta")
(("1"
(reveal "sqvuv")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(replace
-1)
(("1"
(hide -1)
(("1"
(case
"sq(u*perpR(c)) <= sq(v*perpR(c))")
(("1"
(hide
-4)
(("1"
(grind)
nil
nil))
nil)
("2"
(hide
(-2
2))
(("2"
(lemma
"orthogonal_basis")
(("2"
(inst
-
"c"
"perpR(c)"
_)
(("2"
(inst-cp
-
"u")
(("2"
(inst
-
"v")
(("2"
(assert)
(("2"
(case
"c /= zero AND perpR(c) /= zero AND orthogonal?(c, perpR(c))")
(("1"
(flatten)
(("1"
(assert)
(("1"
(lemma
"orthogonal_basis_sqv")
(("1"
(inst?)
(("1"
(assert)
(("1"
(label
"ddvc1"
-3)
(("1"
(hide
"ddvc1")
(("1"
(label
"ddvc2"
-1)
(("1"
(hide
"ddvc2")
(("1"
(lemma
"orthogonal_basis_sqv")
(("1"
(inst?)
(("1"
(assert)
(("1"
(reveal
"ddvc1")
(("1"
(reveal
"ddvc2")
(("1"
(delabel
"ddvc1")
(("1"
(delabel
"ddvc2")
(("1"
(case
"sqv(perpR(c)) = sqv(c)")
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(reveal
"sqvuv")
(("1"
(replace
-1)
(("1"
(replace
-2)
(("1"
(case
"sq(u*c) >= sq(v*c)")
(("1"
(rewrite
"sq_div")
(("1"
(rewrite
"sq_div")
(("1"
(rewrite
"sq_div")
(("1"
(rewrite
"sq_div")
(("1"
(mult-by
3
"sqv(c)/sq(sqv(c))")
(("1"
(mult-by
-1
"sqv(c)/sq(sqv(c))")
(("1"
(ground)
nil
nil)
("2"
(real-props)
nil
nil))
nil)
("2"
(split
+)
(("1"
(cross-mult
1)
nil
nil)
("2"
(cross-mult
1)
(("2"
(rewrite
"sq_ge")
(("2"
(lemma
"sqv_eq_0")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"sq_ge")
(("1"
(hide-all-but
(-8
1))
(("1"
(grind)
nil
nil))
nil)
("2"
(hide-all-but
(-8
-9
1))
(("2"
(grind)
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))
nil))
nil))
nil))
nil)
("2"
(split
+)
(("1"
(flatten)
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(flatten)
(("2"
(case
"c = zero")
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
(-1
1))
(("2"
(expand
"zero")
(("2"
(expand
"perpR")
(("2"
(flatten)
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but
1)
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(hide-all-but
(-1 -3 1))
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(lemma
"Delta_ge_0_2[R]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(inst
+
"0")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skeep)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but -1)
(("2" (reveal "sqvuv")
(("2" (split -)
(("1"
(replace -1)
(("1" (assert) nil nil))
nil)
("2"
(replace -1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "norm(u) = 1 and norm(v) = 1")
(("1" (expand "^" 1)
(("1" (flatten)
(("1" (replaces -1)
(("1" (replaces -1) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 -2 1))
(("2" (rewrite "sqrt_eq" -1 :dir rl)
(("2" (rewrite "sqrt_eq" -2 :dir rl)
(("2" (rewrite "sqrt_sqv_norm")
(("2" (rewrite "sqrt_sqv_norm")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.40Angebot
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
|
