products/sources/formale Sprachen/PVS/ACCoRD/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Lisp

Untersuchung PVS©
(repulsive
 (tca_TCC1 0
  (tca_TCC1-1 nil 3481393354 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (repulsive_simple 0
  (repulsive_simple-1 nil 3581756359
   ("" (skeep)
    (("" (case "s*v<0")
      (("1" (hide 2)
        (("1" (assert)
          (("1" (case "tca(s,v) > 0")
            (("1" (assert)
              (("1" (skeep)
                (("1" (expand "repulsive?")
                  (("1" (split -)
                    (("1" (case "s*nv>=0")
                      (("1"
                        (lemma
                         "closest_approach_2D.dot_nneg_divergent")
                        (("1" (inst - "s" "zero" "nv" "zero")
                          (("1" (assert)
                            (("1" (case "norm(s)>=norm(s+tca(s,v)*v)")
                              (("1"
                                (assert)
                                (("1"
                                  (split -)
                                  (("1"
                                    (expand "divergent?")
                                    (("1"
                                      (case "t = 0")
                                      (("1"
                                        (replaces -1)
                                        (("1" (assert) nil nil))
                                        nil)
                                       ("2"
                                        (inst - "t")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (rewrite "dist_norm")
                                            (("1"
                                              (rewrite "dist_norm")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (flatten)
                                    (("2"
                                      (replaces -1)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (lemma "horizontal_tca_min")
                                  (("2"
                                    (inst - "v" "s" "0")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (rewrite
                                         "horizontal_sq_dtca_eq")
                                        (("1"
                                          (rewrite
                                           "sqrt_le"
                                           -1
                                           :dir
                                           rl)
                                          (("1"
                                            (rewrite "sqrt_sqv_norm")
                                            (("1"
                                              (rewrite "sqrt_sqv_norm")
                                              (("1"
                                                (expand "tca" +)
                                                (("1"
                                                  (lift-if)
                                                  (("1"
                                                    (split +)
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (flatten)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (flatten)
                                      (("2"
                                        (replaces -1)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (expand "tca" -1)
                        (("2" (lift-if)
                          (("2" (split -)
                            (("1" (flatten)
                              (("1"
                                (replaces -1)
                                (("1" (assert) nil nil))
                                nil))
                              nil)
                             ("2" (flatten)
                              (("2"
                                (expand "horizontal_tca" -1)
                                (("2"
                                  (cross-mult -1)
                                  (("2"
                                    (ground)
                                    (("2"
                                      (lemma "sqv_eq_0")
                                      (("2"
                                        (inst?)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (case "nv = zero OR v = zero")
                      (("1" (split -)
                        (("1" (replaces -1) (("1" (assert) nil nil))
                          nil)
                         ("2" (replaces -1) (("2" (assert) nil nil))
                          nil))
                        nil)
                       ("2" (flatten)
                        (("2" (expand "tca")
                          (("2" (assert)
                            (("2" (lemma "horizontal_tca_min")
                              (("2"
                                (inst - "nv" "s" "t")
                                (("2"
                                  (rewrite "horizontal_sq_dtca_eq")
                                  (("2"
                                    (rewrite "sqrt_le" -1 :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))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (expand "tca" 1)
                (("2" (lift-if)
                  (("2" (ground)
                    (("1" (replaces -1) (("1" (assert) nil nil)) nil)
                     ("2" (expand "horizontal_tca")
                      (("2" (cross-mult 2)
                        (("2" (ground)
                          (("2" (lemma "sqv_eq_0")
                            (("2" (inst?) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert)
        (("2" (hide 2)
          (("2" (skeep 2)
            (("2" (expand "repulsive?")
              (("2" (flatten)
                (("2" (case "NOT s*nv>=0")
                  (("1" (assert) nil nil)
                   ("2" (hide (-2 -3))
                    (("2"
                      (lemma "closest_approach_2D.dot_nneg_divergent")
                      (("2" (inst - "s" "zero" "nv" "zero")
                        (("2" (assert)
                          (("2" (case "nv = zero")
                            (("1" (replaces -1)
                              (("1" (assert) nil nil)) nil)
                             ("2" (assert)
                              (("2"
                                (expand "divergent?")
                                (("2"
                                  (inst - "t")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (rewrite "dist_norm")
                                      (("1"
                                        (rewrite "dist_norm")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (assert)
                                    (("2"
                                      (case "t = 0")
                                      (("1"
                                        (replaces -1)
                                        (("1" (assert) nil nil))
                                        nil)
                                       ("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (< 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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (div_mult_pos_neg_gt1 formula-decl nil extra_real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (repulsive? const-decl "bool" repulsive nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (>= const-decl "bool" reals nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (+ const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (scal_0 formula-decl nil vectors_2D "vectors/")
    (add_zero_right formula-decl nil vectors_2D "vectors/")
    (scal_zero formula-decl nil vectors_2D "vectors/")
    (add_zero_left formula-decl nil vectors_2D "vectors/")
    (dist_norm formula-decl nil distance_2D "vectors/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (t skolem-const-decl "nnreal" repulsive nil)
    (divergent? const-decl "bool" closest_approach_2D "vectors/")
    (dot_zero_right formula-decl nil vectors_2D "vectors/")
    (horizontal_tca_min formula-decl nil definitions nil)
    (horizontal_tca const-decl "real" definitions nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sqrt_le formula-decl nil sqrt "reals/")
    (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/")
    (horizontal_sq_dtca_eq formula-decl nil definitions nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (v skolem-const-decl "Vect2" repulsive nil)
    (/= const-decl "boolean" notequal nil)
    (sub_zero_right 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)
    (dot_nneg_divergent formula-decl nil closest_approach_2D
     "vectors/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (tca const-decl "real" repulsive nil)
    (> const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (t skolem-const-decl "nnreal" repulsive nil))
   shostak))
 (repulsive_transitive 0
  (repulsive_transitive-1 nil 3549787475
   ("" (skeep)
    (("" (expand "repulsive?")
      (("" (flatten)
        (("" (assert)
          (("" (case "v = zero")
            (("1" (assert)
              (("1" (replace -1)
                (("1" (assert) (("1" (grind) nil nil)) nil)) nil))
              nil)
             ("2" (assert)
              (("2" (case "s*v < 0")
                (("1" (assert)
                  (("1" (flatten)
                    (("1" (hide 4)
                      (("1" (ground)
                        (("1" (expand "tca" -3)
                          (("1" (assert)
                            (("1" (lift-if)
                              (("1"
                                (ground)
                                (("1"
                                  (replaces -1)
                                  (("1" (assert) nil nil))
                                  nil)
                                 ("2"
                                  (expand "horizontal_tca")
                                  (("2"
                                    (cross-mult -1)
                                    (("2"
                                      (ground)
                                      (("2"
                                        (lemma "sqv_eq_0")
                                        (("2"
                                          (inst?)
                                          (("2" (ground) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "tca" 2)
                          (("2" (assert)
                            (("2" (lift-if)
                              (("2"
                                (ground)
                                (("2"
                                  (expand "horizontal_tca")
                                  (("2"
                                    (cross-mult 2)
                                    (("2"
                                      (ground)
                                      (("2"
                                        (lemma "sqv_eq_0")
                                        (("2"
                                          (inst?)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("3" (expand "tca")
                          (("3" (expand "horizontal_tca")
                            (("3" (cross-mult 2)
                              (("3"
                                (ground)
                                (("3"
                                  (lemma "sqv_eq_0")
                                  (("3"
                                    (inst?)
                                    (("3" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("4" (expand "tca")
                          (("4" (lift-if 3)
                            (("4" (ground)
                              (("4"
                                (expand "horizontal_tca")
                                (("4"
                                  (cross-mult 2)
                                  (("4"
                                    (ground)
                                    (("4"
                                      (lemma "sqv_eq_0")
                                      (("4"
                                        (inst?)
                                        (("4" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("5" (expand "tca" 2)
                          (("5" (lift-if)
                            (("5" (ground)
                              (("5"
                                (expand "horizontal_tca")
                                (("5"
                                  (cross-mult 2)
                                  (("5"
                                    (ground)
                                    (("5"
                                      (lemma "sqv_eq_0")
                                      (("5"
                                        (inst?)
                                        (("5" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("6" (expand "tca" 2)
                          (("6" (assert)
                            (("6" (expand "horizontal_tca")
                              (("6"
                                (ground)
                                (("6"
                                  (cross-mult 2)
                                  (("6"
                                    (ground)
                                    (("6"
                                      (lemma "sqv_eq_0")
                                      (("6"
                                        (inst?)
                                        (("6" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("7" (expand "tca" 3)
                          (("7" (assert)
                            (("7" (lift-if)
                              (("7"
                                (ground)
                                (("7"
                                  (expand "horizontal_tca")
                                  (("7"
                                    (ground)
                                    (("7"
                                      (cross-mult 2)
                                      (("7"
                                        (ground)
                                        (("7"
                                          (lemma "sqv_eq_0")
                                          (("7"
                                            (inst?)
                                            (("7" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert)
                  (("2" (hide 3) (("2" (grind) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((repulsive? const-decl "bool" repulsive nil)
    (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (comp_zero_y formula-decl nil vectors_2D "vectors/")
    (comp_zero_x formula-decl nil vectors_2D "vectors/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (tca const-decl "real" repulsive nil)
    (horizontal_tca const-decl "real" definitions nil)
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/")
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (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)
    (dot_zero_right formula-decl nil vectors_2D "vectors/")
    (scal_zero formula-decl nil vectors_2D "vectors/")
    (add_zero_right formula-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (* const-decl "real" vectors_2D "vectors/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/"))
   shostak))
 (not_repulsive_sum_closed 0
  (not_repulsive_sum_closed-1 nil 3481443204
   ("" (expand "sum_closed_2D?")
    (("" (skosimp*)
      (("" (ground)
        (("" (expand "repulsive?")
          (("" (case "tca(s!1,nv!1)>=0 AND tca(s!1,nw!1)>=0")
            (("1" (flatten)
              (("1" (assert)
                (("1" (split -)
                  (("1" (hide-all-but (-1 1 3))
                    (("1" (expand "tca")
                      (("1" (lift-if)
                        (("1" (ground)
                          (("1" (case "nv!1 = -nw!1")
                            (("1" (replace -1)
                              (("1"
                                (expand "horizontal_tca")
                                (("1"
                                  (rewrite "sqv_neg")
                                  (("1"
                                    (case "sqv(nw!1)>0")
                                    (("1"
                                      (cross-mult 2)
                                      (("1"
                                        (cross-mult 4)
                                        (("1"
                                          (hide-all-but (2 4))
                                          (("1" (grind) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (lemma "sqv_eq_0")
                                      (("2"
                                        (inst - "nw!1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but (-1 1))
                              (("2"
                                (expand "zero")
                                (("2"
                                  (decompose-equality)
                                  (("1" (grind) nil nil)
                                   ("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2"
                            (case "sqv(nv!1+nw!1)>0 AND sqv(nv!1)>0 AND sqv(nw!1)>0")
                            (("1" (flatten)
                              (("1"
                                (expand "horizontal_tca")
                                (("1"
                                  (cross-mult -4)
                                  (("1"
                                    (cross-mult 2)
                                    (("1"
                                      (cross-mult 4)
                                      (("1"
                                        (hide-all-but (-4 2 4))
                                        (("1" (grind) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (lemma "sqv_eq_0")
                              (("2"
                                (inst-cp - "nv!1+nw!1")
                                (("2"
                                  (inst-cp - "nv!1")
                                  (("2"
                                    (inst - "nw!1")
                                    (("2" (ground) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2"
                    (case "FORALL (epsilon: posreal): norm(s!1 + tca(s!1, nv!1 + nw!1) * (nv!1 + nw!1)) <=norm(s!1 + tca(s!1, v!1) * v!1) + epsilon")
                    (("1"
                      (case "FORALL (epsilon: posreal): norm(s!1 + tca(s!1, nv!1 + nw!1) * (nv!1 + nw!1)) <
                                            norm(s!1 + tca(s!1, v!1) * v!1) + epsilon")
                      (("1"
                        (inst -
                         "norm(s!1 + tca(s!1, nv!1 + nw!1) * (nv!1 + nw!1)) - norm(s!1 + tca(s!1, v!1) * v!1)")
                        (("1" (assert) nil nil) ("2" (assert) nil nil))
                        nil)
                       ("2" (hide-all-but (-1 1))
                        (("2" (skosimp*)
                          (("2" (inst - "epsilon!1/2")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide -1)
                      (("2" (skosimp*)
                        (("2"
                          (name "A"
                                "norm(s!1 + tca(s!1, v!1) * v!1) + epsilon!1")
                          (("2" (replace -1)
                            (("2"
                              (case "NOT (norm(s!1 + tca(s!1, v!1) * v!1) + epsilon!1 > norm(s!1 + tca(s!1, nw!1) * nw!1) AND norm(s!1 + tca(s!1, v!1) * v!1) + epsilon!1 > norm(s!1 + tca(s!1, nv!1) * nv!1))")
                              (("1" (ground) nil nil)
                               ("2"
                                (flatten)
                                (("2"
                                  (label "Aname" -3)
                                  (("2"
                                    (hide "Aname")
                                    (("2"
                                      (lemma
                                       "horizontal_conflict_sum_closed[A]")
                                      (("2"
                                        (inst - "s!1" "nv!1" "nw!1")
                                        (("2"
                                          (split -)
                                          (("1"
                                            (expand
                                             "horizontal_conflict?")
                                            (("1"
                                              (skosimp*)
                                              (("1"
                                                (lemma
                                                 "horizontal_tca_los[A]")
                                                (("1"
                                                  (inst
                                                   -
                                                   "nv!1 + nw!1"
                                                   "s!1")
                                                  (("1"
                                                    (split -)
                                                    (("1"
                                                      (rewrite
                                                       "sqrt_sqv_norm"
                                                       :dir
                                                       rl)
                                                      (("1"
                                                        (rewrite
                                                         "sqrt_sqv_norm"
                                                         :dir
                                                         rl)
                                                        (("1"
                                                          (lemma
                                                           "sq_le")
                                                          (("1"
                                                            (inst?)
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (expand
                                                                 "tca"
                                                                 1)
                                                                (("1"
                                                                  (lift-if)
                                                                  (("1"
                                                                    (ground)
                                                                    (("1"
                                                                      (case
                                                                       "nv!1=-nw!1")
                                                                      (("1"
                                                                        (replace
                                                                         -1)
                                                                        (("1"
                                                                          (hide-all-but
                                                                           (3
                                                                            5))
                                                                          (("1"
                                                                            (expand
                                                                             "tca")
                                                                            (("1"
                                                                              (lift-if)
                                                                              (("1"
                                                                                (ground)
                                                                                (("1"
                                                                                  (expand
                                                                                   "horizontal_tca")
                                                                                  (("1"
                                                                                    (rewrite
                                                                                     "sqv_neg")
                                                                                    (("1"
                                                                                      (case
                                                                                       "sqv(nw!1)>0")
                                                                                      (("1"
                                                                                        (cross-mult
                                                                                         2)
                                                                                        (("1"
                                                                                          (cross-mult
                                                                                           3)
                                                                                          (("1"
                                                                                            (grind)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (lemma
                                                                                         "sqv_eq_0")
                                                                                        (("2"
                                                                                          (inst?)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         (-1
                                                                          1))
                                                                        (("2"
                                                                          (expand
                                                                           "zero")
                                                                          (("2"
                                                                            (decompose-equality)
                                                                            (("1"
                                                                              (grind)
                                                                              nil
                                                                              nil)
                                                                             ("2"
                                                                              (grind)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (case
                                                                       "FORALL (vvk: Vect2): sq(norm(vvk)) = sqv(vvk)")
                                                                      (("1"
                                                                        (inst
                                                                         -
                                                                         "s!1 + horizontal_tca(s!1, nv!1 + nw!1) * (nv!1 + nw!1)")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (skeep)
                                                                          (("2"
                                                                            (lemma
                                                                             "sqrt_eq")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (assert)
                                                                                (("2"
                                                                                  (rewrite
                                                                                   "sqrt_sqv_norm")
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (lemma
                                                       "Delta_gt_0[A]")
                                                      (("2"
                                                        (inst
                                                         -
                                                         "s!1"
                                                         "nv!1+nw!1")
                                                        (("2"
                                                          (assert)
                                                          (("2"
                                                            (case
                                                             "nv!1+nw!1 = zero")
                                                            (("1"
                                                              (hide-all-but
                                                               (-1
                                                                4
                                                                6))
                                                              (("1"
                                                                (case
                                                                 "nv!1=-nw!1")
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (expand
                                                                     "tca")
                                                                    (("1"
                                                                      (lift-if)
                                                                      (("1"
                                                                        (ground)
                                                                        (("1"
                                                                          (expand
                                                                           "horizontal_tca")
                                                                          (("1"
                                                                            (rewrite
                                                                             "sqv_neg")
                                                                            (("1"
                                                                              (case
                                                                               "sqv(nw!1)>0")
                                                                              (("1"
                                                                                (cross-mult
                                                                                 2)
                                                                                (("1"
                                                                                  (cross-mult
                                                                                   4)
                                                                                  (("1"
                                                                                    (grind)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (lemma
                                                                                 "sqv_eq_0")
                                                                                (("2"
                                                                                  (inst?)
                                                                                  (("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide-all-but
                                                                   (-1
                                                                    1))
                                                                  (("2"
                                                                    (expand
                                                                     "zero")
                                                                    (("2"
                                                                      (decompose-equality)
                                                                      (("1"
                                                                        (grind)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (grind)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (assert)
                                                              (("2"
                                                                (expand
                                                                 "horizontal_conflict_ever?")
                                                                (("2"
                                                                  (inst
                                                                   +
                                                                   "nnt!1")
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (flatten)
                                                    (("2"
                                                      (hide-all-but
                                                       (-1 2 4))
                                                      (("2"
                                                        (case
                                                         "nv!1=-nw!1")
                                                        (("1"
                                                          (replace -1)
                                                          (("1"
                                                            (case
                                                             "sqv(nw!1)>0")
                                                            (("1"
                                                              (expand
                                                               "tca")
                                                              (("1"
                                                                (lift-if)
                                                                (("1"
                                                                  (ground)
                                                                  (("1"
                                                                    (expand
                                                                     "horizontal_tca")
                                                                    (("1"
                                                                      (cross-mult
                                                                       2)
                                                                      (("1"
                                                                        (cross-mult
                                                                         4)
                                                                        (("1"
                                                                          (grind)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (lemma
                                                               "sqv_eq_0")
                                                              (("2"
                                                                (inst?)
                                                                (("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (expand
                                                                     "tca")
                                                                    (("2"
                                                                      (lift-if)
                                                                      (("2"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide-all-but
                                                           (-1 1))
                                                          (("2"
                                                            (expand
                                                             "zero")
                                                            (("2"
                                                              (decompose-equality)
                                                              (("1"
                                                                (grind)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (grind)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand
                                             "horizontal_conflict?")
                                            (("2"
                                              (inst + "tca(s!1,nv!1)")
                                              (("2"
                                                (case
                                                 "norm(s!1 + tca(s!1, nv!1) * nv!1) < A")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (lemma "sqrt_lt")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "sqv(s!1 + tca(s!1, nv!1) * nv!1)"
                                                       "sq(A)")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (rewrite
                                                           "sqrt_sqv_norm")
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (reveal "Aname")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("3"
                                            (assert)
                                            (("3"
                                              (expand
                                               "horizontal_conflict?")
                                              (("3"
                                                (inst
                                                 +
                                                 "tca(s!1,nw!1)")
                                                (("3"
                                                  (case
                                                   "norm(s!1 + tca(s!1, nw!1) * nw!1) < A")
                                                  (("1"
                                                    (lemma "sqrt_lt")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "sqv(s!1 + tca(s!1, nw!1) * nw!1)"
                                                       "sq(A)")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (rewrite
                                                           "sqrt_sqv_norm")
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (reveal "Aname")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (flatten) (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((repulsive? const-decl "bool" repulsive nil)
    (+ const-decl "Vector" vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (sqv_neg formula-decl nil vectors_2D "vectors/")
    (minus_real_is_real application-judgement "real" reals nil)
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/")
    (neg_add_left formula-decl nil vectors_2D "vectors/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "real" vectors_2D "vectors/")
    (nw!1 skolem-const-decl "Vect2" repulsive nil)
    (real_gt_is_strict_total_order name-judgement
--> --------------------

--> maximum size reached

--> --------------------

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.101Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Kontakt
Drucken
Kontakt
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff