|
(opt_line
(opt_line_eps_TCC1 0
(opt_line_eps_TCC1-1 nil 3441660997
("" (skeep) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(opt_line_eps_TCC2 0
(opt_line_eps_TCC2-1 nil 3441660997 ("" (skosimp*) nil nil) nil nil))
(opt_line_eps_tangent_line 0
(opt_line_eps_tangent_line-3 nil 3445708851
("" (skeep)
(("" (expand "opt_line_eps?")
(("" (flatten)
(("" (expand "opt_line_eps" :assert? none)
(("" (skoletin -1 :postfix "a")
(("" (lift-if)
(("" (split -)
(("1" (flatten)
(("1"
(typepred
"opt_trk_gs_line(tangent_line(sp, eps),vo, vi)")
(("1" (replaces (-4 -5) :dir rl)
(("1" (expand "tangent_line?")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((opt_line_eps? const-decl "bool" opt_line nil)
(opt_line_eps const-decl
"{nvo: Vect2 | nvo /= zero => optimal?(vo, tangent_line(sp, eps))(nvo)}"
opt_line nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ka skolem-const-decl "real" opt_line nil)
(tangent_line? const-decl "bool" tangent_line nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(tangent_line const-decl "Nz_vect2" tangent_line nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(opt_trk_gs_line const-decl
"{k: real, nvo: (optimal?(vo, nzv)) | k * nzv = nvo - vi}"
opt_trk_gs nil)
(D formal-const-decl "posreal" opt_line 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)
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(optimal? const-decl "bool" definitions 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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/")
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil))
nil)
(opt_line_eps_tangent_line-2 nil 3445706887
("" (skeep)
(("" (beta)
(("" (flatten)
((""
(name-replace "opto" "opt_line_eps(sp, vo, vi, eps)" :hide?
nil)
(("" (expand "opt_line_eps" :assert? none)
(("" (skoletin -1 :postfix "a")
(("" (lift-if)
(("" (split -)
(("1" (flatten)
(("1"
(typepred
"opt_trk_gs_line(tangent_line(sp, eps),vo, vi)")
(("1" (replaces (-4 -5) :dir rl)
(("1" (expand "tangent_line?")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(Sp_vect2 type-eq-decl nil horizontal nil)
(Sign type-eq-decl nil sign "reals/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(tangent_line const-decl "Nz_vect2" tangent_line nil)
(opt_trk_gs_line const-decl
"{k: real, nvo: (optimal?(vo, nzv)) | k * nzv = nvo - vi}"
opt_trk_gs nil)
(* const-decl "Vector" vectors_2D "vectors/")
(tangent_line? const-decl "bool" tangent_line nil))
nil)
(opt_line_eps_tangent_line-1 nil 3433323791
("" (skeep)
(("" (beta)
(("" (flatten)
((""
(name-replace "opto" "opt_line_eps(sp, vo, vi, eps)" :hide?
nil)
(("" (expand "opt_line_eps")
(("" (assert) (("" (postpone) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((tangent_line const-decl "Nz_vect2" tangent_line nil)
(Sign type-eq-decl nil sign "reals/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Sp_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(tangent_line? const-decl "bool" tangent_line nil)
(* const-decl "Vector" vectors_2D "vectors/")
(opt_trk_gs_line const-decl
"{k: real, nvo: (optimal?(vo, nzv)) | k * nzv = nvo - vi}"
opt_trk_gs nil))
nil))
(opt_line_is_line_solution 0
(opt_line_is_line_solution-1 nil 3471194384
("" (skeep)
(("" (lemma "opt_line_eps_tangent_line")
(("" (inst?)
(("" (assert)
(("" (lemma "tangent_line_solution")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((opt_line_eps_tangent_line formula-decl nil opt_line nil)
(- const-decl "Vector" vectors_2D "vectors/")
(tangent_line_solution formula-decl nil tangent_line nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" opt_line nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.28Angebot
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
|
