products/Sources/formale Sprachen/JAVA/openjdk-20-36_src/src/hotspot/share/jfr/recorder/service/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: cc.v   Sprache: SML

Original von: PVS©
(ln_exp_ineq
 (noa_posreal 0
  (noa_posreal-1 nil 3477843693
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst + "x!1 + 1") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((+ 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)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
   shostak))
 (conn_posreal 0
  (conn_posreal-1 nil 3477843707
   ("" (expand "connected?")
    (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/"))
   shostak))
 (ln_ineq1_TCC1 0
  (ln_ineq1_TCC1-1 nil 3254127856 ("" (grind) nil nil) nil shostak))
 (ln_ineq1_TCC2 0
  (ln_ineq1_TCC2-1 nil 3254127856 ("" (grind) nil nil) nil shostak))
 (ln_ineq1 0
  (ln_ineq1-1 nil 3253817629
   ("" (skolem + "x")
    (("" (name "z" "1+x")
      (("" (name "foo" "z-1")
        (("" (typepred "x")
          (("" (replace -4)
            (("" (replace -4 -3 rl)
              (("" (replace -3 (1 -1 -2))
                (("" (replace -4)
                  (("" (replace -3 (-1 -2 1) rl)
                    (("" (hide -3 -4)
                      (("" (simplify -2)
                        (("" (assert)
                          ((""
                            (lemma "both_sides_plus_gt1"
                             ("z" "1" "x" "z-1" "y" "-1"))
                            (("" (replace -1 -3 rl)
                              ((""
                                (simplify -3)
                                ((""
                                  (hide -1)
                                  ((""
                                    (name
                                     "F"
                                     "LAMBDA (x:posreal): x - 1 - ln(x)")
                                    ((""
                                      (name
                                       "G"
                                       "LAMBDA (x:posreal): ln(x) - (x-1)/x")
                                      ((""
                                        (case
                                         "FORALL (x, y: posreal), (z: real): x <= z AND z <= y IMPLIES z >= 0 AND z > 0")
                                        (("1"
                                          (case
                                           "FORALL (x: posreal): EXISTS (y: posreal): x /= y")
                                          (("1"
                                            (lemma "ln_derivable")
                                            (("1"
                                              (flatten -1)
                                              (("1"
                                                (lemma
                                                 "const_derivable_fun[posreal]"
                                                 ("b" "1"))
                                                (("1"
                                                  (lemma
                                                   "identity_derivable_fun[posreal]")
                                                  (("1"
                                                    (lemma
                                                     "diff_derivable_fun[posreal]")
                                                    (("1"
                                                      (inst-cp
                                                       -1
                                                       "I[posreal]"
                                                       "const_fun(1)")
                                                      (("1"
                                                        (inst-cp
                                                         -
                                                         "I[posreal] - const_fun(1)"
                                                         "ln")
                                                        (("1"
                                                          (lemma
                                                           "div_derivable_fun[posreal]"
                                                           ("f"
                                                            "I[posreal]-const_fun(1)"
                                                            "g"
                                                            "I[posreal]"))
                                                          (("1"
                                                            (inst
                                                             -
                                                             "ln"
                                                             "(I[posreal]-const_fun(1))/I[posreal]")
                                                            (("1"
                                                              (lemma
                                                               "deriv_const_fun[posreal]"
                                                               ("b"
                                                                "1"))
                                                              (("1"
                                                                (expand
                                                                 "I")
                                                                (("1"
                                                                  (expand
                                                                   "const_fun")
                                                                  (("1"
                                                                    (lemma
                                                                     "deriv_id_fun[posreal]")
                                                                    (("1"
                                                                      (lemma
                                                                       "deriv_diff_fun[posreal]")
                                                                      (("1"
                                                                        (replace
                                                                         -10)
                                                                        (("1"
                                                                          (replace
                                                                           -8)
                                                                          (("1"
                                                                            (expand
                                                                             "-"
                                                                             (-4
                                                                              -5
                                                                              -6
                                                                              -7))
                                                                            (("1"
                                                                              (expand
                                                                               "/"
                                                                               (-4
                                                                                -5))
                                                                              (("1"
                                                                                (inst-cp
                                                                                 -
                                                                                 "LAMBDA (x: posreal): x"
                                                                                 "LAMBDA (x: posreal): 1")
                                                                                (("1"
                                                                                  (inst-cp
                                                                                   -
                                                                                   "LAMBDA (x:posreal): x - 1"
                                                                                   "ln")
                                                                                  (("1"
                                                                                    (lemma
                                                                                     "deriv_div_fun[posreal]"
                                                                                     ("ff"
                                                                                      "LAMBDA (x:posreal): x-1"
                                                                                      "gg"
                                                                                      "LAMBDA (x:posreal): x"))
                                                                                    (("1"
                                                                                      (inst
                                                                                       -
                                                                                       "ln"
                                                                                       "LAMBDA (x:posreal): (x-1)/x")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "-"
                                                                                         (-1
                                                                                          -2
                                                                                          -3
                                                                                          -4))
                                                                                        (("1"
                                                                                          (expand
                                                                                           "/")
                                                                                          (("1"
                                                                                            (expand
                                                                                             "*")
                                                                                            (("1"
                                                                                              (replace
                                                                                               -14)
                                                                                              (("1"
                                                                                                (replace
                                                                                                 -6)
                                                                                                (("1"
                                                                                                  (replace
                                                                                                   -5)
                                                                                                  (("1"
                                                                                                    (simplify)
                                                                                                    (("1"
                                                                                                      (replace
                                                                                                       -4)
                                                                                                      (("1"
                                                                                                        (simplify
                                                                                                         -1)
                                                                                                        (("1"
                                                                                                          (replace
                                                                                                           -1)
                                                                                                          (("1"
                                                                                                            (simplify
                                                                                                             -2)
                                                                                                            (("1"
                                                                                                              (simplify
                                                                                                               -3)
                                                                                                              (("1"
                                                                                                                (replace
                                                                                                                 -18)
                                                                                                                (("1"
                                                                                                                  (replace
                                                                                                                   -17)
                                                                                                                  (("1"
                                                                                                                    (hide-all-but
                                                                                                                     (-2
                                                                                                                      -3
                                                                                                                      -8
                                                                                                                      -9
                                                                                                                      -15
                                                                                                                      -16
                                                                                                                      -17
                                                                                                                      -18
                                                                                                                      -19
                                                                                                                      -20
                                                                                                                      1))
                                                                                                                    (("1"
                                                                                                                      (assert)
                                                                                                                      (("1"
                                                                                                                        (lemma
                                                                                                                         "minimum_derivative[posreal]")
                                                                                                                        (("1"
                                                                                                                          (inst
                                                                                                                           -
                                                                                                                           "F"
                                                                                                                           "1"
                                                                                                                           "z")
                                                                                                                          (("1"
                                                                                                                            (lemma
                                                                                                                             "minimum_derivative[posreal]")
                                                                                                                            (("1"
                                                                                                                              (inst
                                                                                                                               -
                                                                                                                               "G"
                                                                                                                               "1"
                                                                                                                               "z")
                                                                                                                              (("1"
                                                                                                                                (replace
                                                                                                                                 -3)
                                                                                                                                (("1"
                                                                                                                                  (replace
                                                                                                                                   -4)
                                                                                                                                  (("1"
                                                                                                                                    (simplify
                                                                                                                                     -1)
                                                                                                                                    (("1"
                                                                                                                                      (simplify
                                                                                                                                       -2)
                                                                                                                                      (("1"
                                                                                                                                        (replace
                                                                                                                                         -9
                                                                                                                                         -1
                                                                                                                                         rl)
                                                                                                                                        (("1"
                                                                                                                                          (replace
                                                                                                                                           -10
                                                                                                                                           -2
                                                                                                                                           rl)
                                                                                                                                          (("1"
                                                                                                                                            (simplify
                                                                                                                                             -1)
                                                                                                                                            (("1"
                                                                                                                                              (simplify
                                                                                                                                               -2)
                                                                                                                                              (("1"
                                                                                                                                                (rewrite
                                                                                                                                                 "ln_1")
                                                                                                                                                (("1"
                                                                                                                                                  (simplify
                                                                                                                                                   -2)
                                                                                                                                                  (("1"
                                                                                                                                                    (split
                                                                                                                                                     -1)
                                                                                                                                                    (("1"
                                                                                                                                                      (split
                                                                                                                                                       -2)
                                                                                                                                                      (("1"
                                                                                                                                                        (assert)
                                                                                                                                                        nil
                                                                                                                                                        nil)
                                                                                                                                                       ("2"
                                                                                                                                                        (hide-all-but
                                                                                                                                                         1)
                                                                                                                                                        (("2"
                                                                                                                                                          (skosimp)
                                                                                                                                                          (("2"
                                                                                                                                                            (rewrite
                                                                                                                                                             "div_cancel1")
                                                                                                                                                            (("2"
                                                                                                                                                              (lemma
                                                                                                                                                               "trich_lt"
                                                                                                                                                               ("x"
                                                                                                                                                                "y!1"
                                                                                                                                                                "y"
                                                                                                                                                                "1"))
                                                                                                                                                              (("2"
                                                                                                                                                                (split
                                                                                                                                                                 -1)
                                                                                                                                                                (("1"
                                                                                                                                                                  (lemma
                                                                                                                                                                   "negreal_times_negreal_is_posreal"
                                                                                                                                                                   ("nx"
                                                                                                                                                                    "y!1-1"
                                                                                                                                                                    "ny"
                                                                                                                                                                    "y!1-1"))
                                                                                                                                                                  (("1"
                                                                                                                                                                    (lemma
                                                                                                                                                                     "both_sides_div_pos_gt1"
                                                                                                                                                                     ("x"
                                                                                                                                                                      "(y!1-1)*(y!1-1)"
                                                                                                                                                                      "y"
                                                                                                                                                                      "0"
                                                                                                                                                                      "pz"
                                                                                                                                                                      "y!1"))
                                                                                                                                                                    (("1"
                                                                                                                                                                      (assert)
                                                                                                                                                                      nil
                                                                                                                                                                      nil))
                                                                                                                                                                    nil)
                                                                                                                                                                   ("2"
                                                                                                                                                                    (assert)
                                                                                                                                                                    nil
                                                                                                                                                                    nil))
                                                                                                                                                                  nil)
                                                                                                                                                                 ("2"
                                                                                                                                                                  (propax)
                                                                                                                                                                  nil
                                                                                                                                                                  nil)
                                                                                                                                                                 ("3"
                                                                                                                                                                  (lemma
                                                                                                                                                                   "posreal_times_posreal_is_posreal"
                                                                                                                                                                   ("px"
                                                                                                                                                                    "y!1-1"
                                                                                                                                                                    "py"
                                                                                                                                                                    "y!1-1"))
                                                                                                                                                                  (("1"
                                                                                                                                                                    (lemma
                                                                                                                                                                     "both_sides_div_pos_gt1"
                                                                                                                                                                     ("x"
                                                                                                                                                                      "(y!1-1)*(y!1-1)"
                                                                                                                                                                      "y"
                                                                                                                                                                      "0"
                                                                                                                                                                      "pz"
                                                                                                                                                                      "y!1"))
                                                                                                                                                                    (("1"
                                                                                                                                                                      (assert)
                                                                                                                                                                      nil
                                                                                                                                                                      nil))
                                                                                                                                                                    nil)
                                                                                                                                                                   ("2"
                                                                                                                                                                    (assert)
                                                                                                                                                                    nil
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil)
                                                                                                                                                     ("2"
                                                                                                                                                      (hide-all-but
                                                                                                                                                       1)
                                                                                                                                                      (("2"
                                                                                                                                                        (skosimp*)
                                                                                                                                                        (("2"
                                                                                                                                                          (rewrite
                                                                                                                                                           "div_cancel1")
                                                                                                                                                          (("2"
                                                                                                                                                            (lemma
                                                                                                                                                             "div_times"
                                                                                                                                                             ("x"
                                                                                                                                                              "y!1"
                                                                                                                                                              "n0x"
                                                                                                                                                              "1"
                                                                                                                                                              "y"
                                                                                                                                                              "1"
                                                                                                                                                              "n0y"
                                                                                                                                                              "y!1*y!1"))
                                                                                                                                                            (("2"
                                                                                                                                                              (replace
                                                                                                                                                               -1
                                                                                                                                                               2)
                                                                                                                                                              (("2"
                                                                                                                                                                (simplify
                                                                                                                                                                 2)
                                                                                                                                                                (("2"
                                                                                                                                                                  (simplify
                                                                                                                                                                   2)
                                                                                                                                                                  (("2"
                                                                                                                                                                    (lemma
                                                                                                                                                                     "div_cancel1"
                                                                                                                                                                     ("x"
                                                                                                                                                                      "1/y!1"
                                                                                                                                                                      "n0z"
                                                                                                                                                                      "y!1"))
                                                                                                                                                                    (("2"
                                                                                                                                                                      (rewrite
                                                                                                                                                                       "div_div2"
                                                                                                                                                                       -1)
                                                                                                                                                                      (("2"
                                                                                                                                                                        (replace
                                                                                                                                                                         -1)
                                                                                                                                                                        (("2"
                                                                                                                                                                          (hide
                                                                                                                                                                           -1)
                                                                                                                                                                          (("2"
                                                                                                                                                                            (lemma
                                                                                                                                                                             "trich_lt"
                                                                                                                                                                             ("x"
                                                                                                                                                                              "y!1"
                                                                                                                                                                              "y"
                                                                                                                                                                              "1"))
                                                                                                                                                                            (("2"
                                                                                                                                                                              (split
                                                                                                                                                                               -1)
                                                                                                                                                                              (("1"
                                                                                                                                                                                (lemma
                                                                                                                                                                                 "negreal_times_negreal_is_posreal"
                                                                                                                                                                                 ("nx"
                                                                                                                                                                                  "y!1-1"
                                                                                                                                                                                  "ny"
                                                                                                                                                                                  "y!1-1"))
                                                                                                                                                                                (("1"
                                                                                                                                                                                  (lemma
                                                                                                                                                                                   "both_sides_div_pos_gt1"
                                                                                                                                                                                   ("pz"
                                                                                                                                                                                    "y!1*y!1"
                                                                                                                                                                                    "x"
                                                                                                                                                                                    "(y!1-1)*(y!1-1)"
                                                                                                                                                                                    "y"
                                                                                                                                                                                    "0"))
                                                                                                                                                                                  (("1"
                                                                                                                                                                                    (assert)
                                                                                                                                                                                    nil
                                                                                                                                                                                    nil))
                                                                                                                                                                                  nil)
                                                                                                                                                                                 ("2"
                                                                                                                                                                                  (assert)
                                                                                                                                                                                  nil
                                                                                                                                                                                  nil))
                                                                                                                                                                                nil)
                                                                                                                                                                               ("2"
                                                                                                                                                                                (propax)
                                                                                                                                                                                nil
                                                                                                                                                                                nil)
                                                                                                                                                                               ("3"
                                                                                                                                                                                (lemma
                                                                                                                                                                                 "posreal_times_posreal_is_posreal"
                                                                                                                                                                                 ("px"
                                                                                                                                                                                  "y!1-1"
                                                                                                                                                                                  "py"
                                                                                                                                                                                  "y!1-1"))
                                                                                                                                                                                (("1"
                                                                                                                                                                                  (lemma
                                                                                                                                                                                   "both_sides_div_pos_gt1"
                                                                                                                                                                                   ("pz"
                                                                                                                                                                                    "y!1*y!1"
                                                                                                                                                                                    "x"
                                                                                                                                                                                    "(y!1-1)*(y!1-1)"
                                                                                                                                                                                    "y"
                                                                                                                                                                                    "0"))
                                                                                                                                                                                  (("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))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil)
                                                                                                                         ("2"
                                                                                                                          (propax)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
--> --------------------

--> maximum size reached

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

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



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff