|
(law_cosines
(distance_refl 0
(distance_refl-1 nil 3269434431
("" (grind) (("" (rewrite "sqrt_0") nil nil)) nil)
((sq const-decl "nonneg_real" sq "reals/")
(sq_dist const-decl "nonneg_real" law_cosines nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(dist const-decl "nonneg_real" law_cosines nil))
nil))
(distance_symm 0
(distance_symm-1 nil 3269434431
("" (skolem 1 ("x0" "y0" "x1" "y1"))
(("" (expand "dist")
(("" (expand "sq_dist") (("" (grind) nil nil)) nil)) nil))
nil)
((dist const-decl "nonneg_real" law_cosines nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_dist const-decl "nonneg_real" law_cosines nil))
nil))
(distance_trans 0
(distance_trans-1 nil 3269668543
("" (skosimp*)
(("" (expand "dist")
(("" (expand "sq_dist") (("" (propax) nil nil)) nil)) nil))
nil)
((dist const-decl "nonneg_real" law_cosines nil)
(sq_dist const-decl "nonneg_real" law_cosines nil))
shostak))
(distance_scale 0
(distance_scale-1 nil 3269668008
("" (skosimp*)
(("" (expand "dist")
(("" (expand "sq_dist")
(("" (lemma "sq_times")
(("" (inst-cp - "pz!1" "x0!1-x1!1")
(("" (inst - "pz!1" "y0!1-y1!1")
(("" (lemma "sqrt_times")
((""
(inst - "sq(pz!1)"
"sq(x0!1 - x1!1) + sq(y0!1 - y1!1)")
(("" (rewrite "sqrt_sq") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((dist const-decl "nonneg_real" law_cosines nil)
(sq_times formula-decl nil sq "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_times formula-decl nil sqrt "reals/")
(- const-decl "[numfield, numfield -> numfield]" 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)
(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)
(real_minus_real_is_real application-judgement "real" reals nil)
(sq_dist const-decl "nonneg_real" law_cosines nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(distance_rot 0
(distance_rot-1 nil 3269668867
("" (skosimp*)
(("" (expand "dist")
(("" (expand "sq_dist")
(("" (name "KX" "x0!1 - x1!1")
(("" (name "KY" "y0!1 - y1!1")
((""
(case "(cos(ac!1) * x0!1 + sin(ac!1) * y1!1 - cos(ac!1) * x1!1 -
sin(ac!1) * y0!1) = cos(ac!1)*KX - sin(ac!1)*KY")
(("1" (replace -1)
(("1"
(case "(cos(ac!1) * y0!1 + sin(ac!1) * x0!1 - cos(ac!1) * y1!1 -
sin(ac!1) * x1!1) = sin(ac!1)*KX +cos(ac!1)*KY")
(("1" (replace -1)
(("1" (replace -3)
(("1" (replace -4)
(("1" (hide-all-but 1)
(("1" (lemma "sin2_cos2" ("a" "ac!1"))
(("1" (name-replace "SIN" "sin(ac!1)")
(("1"
(name-replace "COS" "cos(ac!1)")
(("1"
(expand "sq")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2 -1)
(("2" (expand "KX")
(("2" (expand "KY") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "KY")
(("2" (expand "KX") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sin_range application-judgement "trig_range" trig_basic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(dist const-decl "nonneg_real" law_cosines 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(cos const-decl "real" trig_basic nil)
(sin const-decl "real" trig_basic nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(trig_range type-eq-decl nil trig_basic nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(sq const-decl "nonneg_real" sq "reals/")
(sin2_cos2 formula-decl nil trig_basic nil)
(KX skolem-const-decl "real" law_cosines nil)
(KY skolem-const-decl "real" law_cosines nil)
(sq_dist const-decl "nonneg_real" law_cosines nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(Law_Cosines 0
(Law_Cosines-1 nil 3269434431
("" (expand "dist")
(("" (expand "sq_dist")
(("" (ground)
(("" (expand "sq")
(("" (ground) (("" (skosimp*) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sq_dist const-decl "nonneg_real" law_cosines nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(dist const-decl "nonneg_real" law_cosines nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(triangle 0
(triangle-1 nil 3269434431
(""
(case "FORALL (x,y:real): dist(0,0,0,1) <= dist(x,y,0,1) + dist(x,y,0,0)")
(("1"
(case "FORALL (x,y:real,pz:posreal): dist(0, 0, 0, pz) <= dist(x, y, 0, pz) + dist(x, y, 0, 0)")
(("1" (hide -2)
(("1"
(case "FORALL (x,y,a,b:real): dist(0, 0, a,b) <= dist(x, y, a,b) + dist(x, y, 0, 0)")
(("1" (hide -2)
(("1" (skosimp*)
(("1"
(lemma "distance_trans" ("x2" "-x0!1" "y2" "-y0!1"))
(("1" (inst-cp - "x0!1" "x1!1" "y0!1" "y1!1")
(("1" (inst-cp - "x2!1" "x1!1" "y2!1" "y1!1")
(("1" (inst - "x2!1" "x0!1" "y2!1" "y0!1")
(("1"
(inst - "x2!1-x0!1" "y2!1-y0!1" "x1!1-x0!1"
"y1!1-y0!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (case "a!1=0")
(("1" (replace -1)
(("1" (lemma "trichotomy" ("x" "b!1"))
(("1" (split -1)
(("1" (inst - "x!1" "y!1" "b!1")
(("1" (assert) nil nil)) nil)
("2" (replace -1)
(("2" (expand "dist")
(("2" (expand "sq_dist")
(("2" (rewrite "sq_0")
(("2"
(rewrite "sqrt_0")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (inst - "x!1" "-y!1" "-b!1")
(("1" (expand "dist")
(("1" (expand "sq_dist")
(("1" (rewrite "sq_neg")
(("1"
(lemma "sq_neg" ("a" "y!1-b!1"))
(("1"
(replace -1)
(("1"
(assert)
(("1"
(lemma "sq_neg" ("a" "-1*b!1"))
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (name "theta" "atan2(b!1,a!1)")
(("1" (lemma "distance_rot" ("ac" "theta"))
(("1" (lemma "sin_atan2" ("x" "b!1" "y" "a!1"))
(("1" (lemma "cos_atan2" ("x" "b!1" "y" "a!1"))
(("1" (assert)
(("1" (replace -4)
(("1" (inst-cp - "0" "a!1" "0" "b!1")
(("1"
(simplify -4)
(("1"
(case
"cos(theta) * a!1 - sin(theta) * b!1 = 0")
(("1"
(case
"cos(theta) * b!1 + sin(theta) * a!1 = sqrt(sq(a!1)+sq(b!1))")
(("1"
(inst-cp - "x!1" "0" "y!1" "0")
(("1"
(inst
-
"x!1"
"a!1"
"y!1"
"b!1")
(("1"
(replace -1)
(("1"
(replace -2)
(("1"
(replace -5)
(("1"
(replace -6)
(("1"
(replace -7)
(("1"
(simplify 2)
(("1"
(inst
-
"cos(theta) * x!1 - sin(theta) * y!1"
"cos(theta) * y!1 + sin(theta) * x!1"
"sqrt(sq(a!1) + sq(b!1))")
(("1"
(hide
-3
-4
-5
-6
-7
-8
3)
(("1"
(lemma
"sqrt_pos"
("px"
"sq(a!1) + sq(b!1)"))
(("1"
(propax)
nil
nil)
("2"
(hide
-1
-2
2)
(("2"
(lemma
"sq_nz_pos"
("nz"
"a!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 -4 -5 -6 -7 3)
(("2"
(case "b!1=0")
(("1"
(replace -1)
(("1"
(rewrite "sq_0")
(("1"
(simplify 1)
(("1"
(case "a!1>0")
(("1"
(rewrite "sqrt_sq")
(("1"
(assert)
nil
nil))
nil)
("2"
(lemma
"sq_neg"
("a" "a!1"))
(("2"
(replace -1 2 rl)
(("2"
(rewrite
"sqrt_sq")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case
"1 + sq(a!1 / b!1) = (sq(a!1)+sq(b!1))/sq(b!1)")
(("1"
(replace -1)
(("1"
(rewrite "sqrt_div")
(("1"
(case "b!1>0")
(("1"
(assert)
(("1"
(rewrite
"sqrt_sq")
(("1"
(rewrite
"div_div1")
(("1"
(rewrite
"div_div1")
(("1"
(lemma
"div_cancel2"
("x"
"a!1"
"n0z"
"b!1"))
(("1"
(replace
-1
-5)
(("1"
(replace
-4)
(("1"
(replace
-5)
(("1"
(lemma
"div_cancel3"
("x"
"b!1*b!1+a!1*a!1"
"n0z"
"sqrt(sq(a!1) + sq(b!1))"
"y"
"sqrt(sq(a!1) + sq(b!1))"))
(("1"
(replace
-1
2)
(("1"
(rewrite
"sq_rew"
2)
(("1"
(rewrite
"sq_rew"
2)
(("1"
(rewrite
"sq_rew"
2)
(("1"
(rewrite
"sq_sqrt")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(rewrite
"div_div1")
(("2"
(rewrite
"div_div1")
(("2"
(lemma
"sq_neg"
("a" "b!1"))
(("2"
(replace
-1
*
rl)
(("2"
(rewrite
"sqrt_sq")
(("2"
(case
"-((a!1 / b!1 * -b!1) / sqrt((sq(a!1) + sq(-b!1)))) = a!1/ sqrt((sq(a!1) + sq(-b!1)))")
(("1"
(replace
-1)
(("1"
(case
"-1*-b!1=b!1")
(("1"
(replace
-1)
(("1"
(hide
-1
-2
-4)
(("1"
(replace
-2)
(("1"
(replace
-3)
(("1"
(replace
-1)
(("1"
(hide
(-1
-2
-3))
(("1"
(lemma
"div_cancel3")
(("1"
(inst
-
"sqrt(sq(a!1) + sq(b!1))"
"b!1*b!1+a!1*a!1"
"sqrt(sq(a!1) + sq(b!1))")
(("1"
(replace
-1
3)
(("1"
(rewrite
"sq_rew")
(("1"
(rewrite
"sq_rew")
(("1"
(rewrite
"sq_rew")
(("1"
(rewrite
"sq_sqrt")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
4
-3
-4)
(("2"
(assert)
nil
nil))
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"sq_nz_pos"
("nz" "b!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(rewrite "sq_div")
(("2" (assert) nil nil))
nil)
("3"
(lemma
"sq_nz_pos"
("nz" "b!1"))
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -3 -4 -5 -6 3)
(("2"
(case "b!1=0")
(("1" (assert) nil nil)
("2"
(case "b!1>0")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "b!1=0")
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (lemma "distance_scale" ("pz" "pz!1"))
(("2" (inst-cp - "0" "0" "0" "1")
(("2" (inst-cp - "x!1/pz!1" "0" "y!1/pz!1" "1")
(("2" (inst - "x!1/pz!1" "0" "y!1/pz!1" "0")
(("2" (inst - "x!1/pz!1" "y!1/pz!1")
(("2"
(lemma "both_sides_times_pos_le1"
("x" "dist(0, 0, 0, 1)" "y"
"dist(x!1/pz!1, y!1/pz!1, 0, 1) + dist(x!1/pz!1, y!1/pz!1, 0, 0)"
"pz" "pz!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (expand "dist")
(("2" (expand "sq_dist")
(("2" (rewrite "sq_neg")
(("2" (rewrite "sq_0")
(("2" (rewrite "sq_1")
(("2" (rewrite "sqrt_1")
(("2" (name-replace "K1" "sq(x!1)")
(("2" (rewrite "sq_le" :dir rl)
(("2" (rewrite "sq_1")
(("2" (rewrite "sq_plus")
(("2" (rewrite "sq_sqrt")
(("2"
(rewrite "sq_sqrt")
(("2"
(rewrite "sq_minus")
(("2"
(rewrite "sq_1")
(("2"
(lemma "trichotomy" ("x" "y!1"))
(("2"
(split -1)
(("1"
(case
"sq(y!1) - 2 * y!1 + K1 + (sq(y!1) + K1) >=0")
(("1" (assert) nil nil)
("2"
(case
"y!1-sq(y!1)-K1 <= (sqrt(1 + sq(y!1) - 2 * y!1 + K1) * sqrt(sq(y!1) + K1))")
(("1" (assert) nil nil)
("2"
(hide 3)
(("2"
(rewrite
"sqrt_times"
:dir
rl)
(("2"
(rewrite
"sq_le"
:dir
rl)
(("2"
(rewrite "sq_sqrt")
(("2"
(expand "sq" 1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil)
("2"
(replace -1)
(("2"
(rewrite "sq_0")
(("2" (assert) nil nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq_1 formula-decl nil sq "reals/")
(sq_minus formula-decl nil sq "reals/")
(sqrt_times formula-decl nil sqrt "reals/")
(sq_plus formula-decl nil sq "reals/")
(sq_le formula-decl nil sq "reals/")
(sqrt_1 formula-decl nil sqrt "reals/")
(cos const-decl "real" trig_basic nil)
(sin const-decl "real" trig_basic nil)
(sq_div formula-decl nil sq "reals/")
(sq_sqrt formula-decl nil sqrt "reals/")
(sq_rew formula-decl nil sq "reals/")
(sqrt_div formula-decl nil sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_pos judgement-tcc nil sqrt "reals/")
(sq_nz_pos judgement-tcc nil sq "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(sq_0 formula-decl nil sq "reals/")
(sqrt_0 formula-decl nil sqrt "reals/")
(sq_neg formula-decl nil sq "reals/"))
nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.48Angebot
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
|
