Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: poly_system_strategy.prf Sprache: Lisp

Original von: PVS^©

(complex_fun_ops
(Re_fun_rew 0
  (Re_fun_rew-1 nil 3509263489
   ("" (skosimp) (("" (expand "Re" 1 1) (("" (propax) nil nil)) nil))
    nil)
   ((Re const-decl "[T -> real]" complex_fun_ops nil)) shostak))
(Im_fun_rew 0
  (Im_fun_rew-1 nil 3509263506
   ("" (skosimp) (("" (expand "Im" 1 1) (("" (propax) nil nil)) nil))
    nil)
   ((Im const-decl "[T -> real]" complex_fun_ops nil)) shostak))
(diff_function 0
  (diff_function-1 nil 3456290470
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (- const-decl "[T -> complex]" complex_fun_ops nil)
    (+ const-decl "[T -> complex]" complex_fun_ops nil)
    (- const-decl "[T -> complex]" complex_fun_ops nil)
    (eq_rew formula-decl nil complex_types nil)
    (Re const-decl "real" complex_types nil)
    (Im const-decl "real" complex_types nil)
    (- const-decl "complex" complex_types nil)
    (- const-decl "complex" complex_types nil)
    (+ const-decl "complex" complex_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
(div_function 0
  (div_function-1 nil 3456290487
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (* const-decl "[T -> complex]" complex_fun_ops nil)
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types 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)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (eq_rew formula-decl nil complex_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_abs const-decl "nnreal" complex_types nil)
    (/ const-decl "complex" complex_types nil)
    (/ const-decl "complex" complex_types nil)
    (* const-decl "complex" complex_types nil)
    (div_nzcomplex2 application-judgement "nzcomplex" complex_types
     nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nz_sq_abs_pos application-judgement "posreal" complex_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   shostak))
(scal_function 0
  (scal_function-1 nil 3456290495
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (const_fun const-decl "[S -> T]" const_fun_def "structures/")
    (* const-decl "[T -> complex]" complex_fun_ops nil)
    (* const-decl "[T -> complex]" complex_fun_ops nil)
    (eq_rew formula-decl nil complex_types nil)
    (Re const-decl "real" complex_types nil)
    (Im const-decl "real" complex_types nil)
    (* const-decl "complex" complex_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
(scaldiv_function 0
  (scaldiv_function-1 nil 3456290504
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (const_fun const-decl "[S -> T]" const_fun_def "structures/")
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types 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)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (eq_rew formula-decl nil complex_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_abs const-decl "nnreal" complex_types nil)
    (/ const-decl "complex" complex_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nz_sq_abs_pos application-judgement "posreal" complex_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   shostak))
(negneg_function 0
  (negneg_function-1 nil 3456290512
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "-")
        (("" (assert)
          (("" (expand "-")
            (("" (assert)
              (("" (decompose-equality)
                (("1" (expand "Re") (("1" (assert) nil nil)) nil)
                 ("2" (expand "Im") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (- const-decl "[T -> complex]" complex_fun_ops nil)
    (eq_rew formula-decl nil complex_types nil)
    (Re_neg1 formula-decl nil complex_types nil)
    (Im_neg1 formula-decl nil complex_types nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(prod_def 0
  (prod_def-1 nil 3456290621
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (+ const-decl "[T -> complex]" complex_fun_ops nil)
    (sq const-decl "[T -> complex]" complex_fun_ops nil)
    (- const-decl "[T -> complex]" complex_fun_ops nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[T -> complex]" complex_fun_ops 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)
    (* const-decl "[T -> complex]" complex_fun_ops nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (eq_rew formula-decl nil complex_types nil)
    (Re const-decl "real" complex_types nil)
    (Im const-decl "real" complex_types nil)
    (* const-decl "complex" complex_types nil)
    (+ const-decl "complex" complex_types nil)
    (sq const-decl "complex" complex_types nil)
    (- const-decl "complex" complex_types nil)
    (* const-decl "complex" complex_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
(Re_fun_conjugate 0
  (Re_fun_conjugate-1 nil 3509263537
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "conjugate")
        (("" (expand "conjugate") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (conjugate const-decl "[T -> complex]" complex_fun_ops nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (conjugate const-decl "complex" complex_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (Re_rew formula-decl nil complex_types nil))
   shostak))
(Im_fun_conjugate 0
  (Im_fun_conjugate-1 nil 3509263568
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "-")
        (("" (assert)
          (("" (expand "conjugate")
            (("" (expand "conjugate") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (conjugate const-decl "[T -> complex]" complex_fun_ops nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (conjugate const-decl "complex" complex_types nil)
    (Im_rew formula-decl nil complex_types nil))
   shostak))
(sq_abs_TCC1 0
  (sq_abs_TCC1-1 nil 3509263212 ("" (subtype-tcc) nil nil)
   ((Re const-decl "real" complex_types nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (T formal-type-decl nil complex_fun_ops nil)
    (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (Im const-decl "real" complex_types nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(nz_fun_sq_abs_pos 0
  (nz_fun_sq_abs_pos-1 nil 3509263212
   ("" (skolem + ("f!1" "x!1"))
    (("" (expand "sq_abs")
      (("" (expand "+ ")
        (("" (expand "sq")
          (("" (assert)
            (("" (typepred "f!1(x!1)")
              (("" (expand "/=")
                (("" (split)
                  (("1" (lemma "sq_nz_pos" ("nz" "Re(f!1(x!1))"))
                    (("1" (assert) nil nil) ("2" (assert) nil nil))
                    nil)
                   ("2" (lemma "sq_nz_pos" ("nz" "Im(f!1(x!1))"))
                    (("1" (assert) nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_abs const-decl "[T -> nnreal]" complex_fun_ops nil)
    (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (T formal-type-decl nil complex_fun_ops nil)
    (Re const-decl "real" complex_types 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)
    (complex type-decl nil complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (sq_nz_pos judgement-tcc nil sq "reals/")
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/"))
   nil))
(complex_abs_nzfunction_pos 0
  (complex_abs_nzfunction_pos-1 nil 3509263212
   ("" (skolem + ("f!1" "x!1"))
    (("" (expand "abs")
      (("" (expand "abs")
        (("" (lemma "nz_fun_sq_abs_pos")
          (("" (inst - "f!1" "x!1") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((abs const-decl "[T -> nonneg_real]" complex_fun_ops nil)
    (nz_fun_sq_abs_pos judgement-tcc nil complex_fun_ops nil)
    (nz_sq_abs_pos application-judgement "posreal" complex_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (nz_fun_sq_abs_pos application-judgement "[T -> posreal]"
     complex_fun_ops nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types 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)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (complex type-decl nil complex_types nil)
    (T formal-type-decl nil complex_fun_ops nil)
    (abs const-decl "nnreal" polar nil))
   nil))
(complex_abs_neg 0
  (complex_abs_neg-1 nil 3509263892
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "abs")
        (("" (expand "-") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (- const-decl "[T -> complex]" complex_fun_ops nil)
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (abs_neg formula-decl nil polar nil))
   shostak))
(complex_abs_mul 0
  (complex_abs_mul-1 nil 3509263918
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("1" (expand "*")
        (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)
       ("2" (skosimp)
        (("2" (expand "*")
          (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (* const-decl "[T -> complex]" complex_fun_ops nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (complex type-decl nil complex_types nil)
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops nil)
    (f1!1 skolem-const-decl "[T -> complex]" complex_fun_ops nil)
    (f2!1 skolem-const-decl "[T -> complex]" complex_fun_ops nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (abs_mult formula-decl nil polar nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(Re_fun_add1 0
  (Re_fun_add1-1 nil 3509263965
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "+ ") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> complex]" complex_fun_ops nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (Re_add1 formula-decl nil complex_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
(Re_fun_neg1 0
  (Re_fun_neg1-1 nil 3509263983
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "-") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> complex]" complex_fun_ops nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (Re_neg1 formula-decl nil complex_types nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(Re_fun_sub1 0
  (Re_fun_sub1-1 nil 3509263996
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "-") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> complex]" complex_fun_ops nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (Re_sub1 formula-decl nil complex_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
(Re_fun_mul1 0
  (Re_fun_mul1-1 nil 3509264010
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "*") (("" (expand "-") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> complex]" complex_fun_ops nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (Re_mul1 formula-decl nil complex_types nil))
   shostak))
(Re_fun_mul2 0
  (Re_fun_mul2-1 nil 3509264034
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "*") (("" (expand "-") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> complex]" complex_fun_ops nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (Re_mul1 formula-decl nil complex_types nil))
   shostak))
(Re_fun_div1 0
  (Re_fun_div1-1 nil 3509264053
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "/")
        (("" (expand "+ ")
          (("" (expand "*")
            (("" (assert)
              (("" (assert)
                (("" (expand "sq_abs")
                  (("" (expand "sq" 1 3)
                    (("" (expand "sq" 1 4)
                      (("" (expand "+" 1 4) (("" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (sq_abs const-decl "[T -> nnreal]" complex_fun_ops nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (nz_fun_sq_abs_pos application-judgement "[T -> posreal]"
     complex_fun_ops nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (nz_sq_abs_pos application-judgement "posreal" complex_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (Re_div1 formula-decl nil complex_types nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (sq_abs const-decl "nnreal" complex_types nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/"))
   shostak))
(Re_fun_div2 0
  (Re_fun_div2-1 nil 3509264266
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "/")
        (("" (expand "sq_abs")
          (("" (expand "sq")
            (("" (expand "+ ")
              (("" (expand "*")
                (("" (assert)
                  (("" (expand "sq_abs") (("" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (sq_abs const-decl "[T -> nnreal]" complex_fun_ops nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (nz_fun_sq_abs_pos application-judgement "[T -> posreal]"
     complex_fun_ops nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nz_sq_abs_pos application-judgement "posreal" complex_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (Re_div1 formula-decl nil complex_types nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (sq_abs const-decl "nnreal" complex_types nil)
    (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/"))
   shostak))
(Re_fun_div3 0
  (Re_fun_div3-1 nil 3509264357
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      ((""
        (expand "+
")
        (("" (expand "*")
          (("" (assert)
            (("" (assert)
              (("" (expand "/") (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (sq_abs const-decl "nnreal" complex_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (nz_sq_abs_pos application-judgement "posreal" complex_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (Re_div1 formula-decl nil complex_types nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(Im_fun_add1 0
  (Im_fun_add1-1 nil 3509264435
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "+ ") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> complex]" complex_fun_ops nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (Im_add1 formula-decl nil complex_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
(Im_fun_neg1 0
  (Im_fun_neg1-1 nil 3509264449
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "-") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> complex]" complex_fun_ops nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (Im_neg1 formula-decl nil complex_types nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(Im_fun_sub1 0
  (Im_fun_sub1-1 nil 3509264474
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "-") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> complex]" complex_fun_ops nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (Im_sub1 formula-decl nil complex_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
(Im_fun_mul1 0
  (Im_fun_mul1-1 nil 3509264606
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "+ ")
        (("" (expand "*") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> complex]" complex_fun_ops nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (Im_mul1 formula-decl nil complex_types nil))
   shostak))
(Im_fun_mul2 0
  (Im_fun_mul2-1 nil 3509264632
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "*")
        ((""
          (expand "+
")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Re const-decl "real" complex_types nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (Im const-decl "real" complex_types nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> complex]" complex_fun_ops nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (Im_mul1 formula-decl nil complex_types nil))
   shostak))
(Im_fun_div1 0
  (Im_fun_div1-1 nil 3509264650
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "/")
        (("" (expand "-")
          (("" (expand "*")
            (("" (assert)
              (("" (expand "sq_abs")
                (("" (assert)
                  (("" (expand "+" 1 2)
                    (("" (expand "sq" 1 3)
                      (("" (expand "sq" 1 3) (("" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (sq_abs const-decl "[T -> nnreal]" complex_fun_ops nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (nz_fun_sq_abs_pos application-judgement "[T -> posreal]"
     complex_fun_ops nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (nz_sq_abs_pos application-judgement "posreal" complex_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (Im_div1 formula-decl nil complex_types nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (sq_abs const-decl "nnreal" complex_types nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(Im_fun_div2 0
  (Im_fun_div2-1 nil 3509264770
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "/")
        (("" (expand "sq_abs")
          (("" (expand "+ ")
            (("" (expand "sq")
              (("" (expand "-")
                (("" (expand "*")
                  (("" (assert)
                    (("" (expand "sq_abs") (("" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (sq_abs const-decl "[T -> nnreal]" complex_fun_ops nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (nz_fun_sq_abs_pos application-judgement "[T -> posreal]"
     complex_fun_ops nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (sq_abs const-decl "nnreal" complex_types nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (Im_div1 formula-decl nil complex_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nz_sq_abs_pos application-judgement "posreal" complex_types nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/"))
   shostak))
(Im_fun_div3 0
  (Im_fun_div3-1 nil 3509264846
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "/")
        (("" (expand "-")
          (("" (expand "*") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil complex_fun_ops nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Re const-decl "[T -> real]" complex_fun_ops nil)
    (sq_abs const-decl "nnreal" complex_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (/ const-decl "[T -> complex]" complex_fun_ops nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (Im const-decl "real" complex_types nil)
    (Re const-decl "real" complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Im const-decl "[T -> real]" complex_fun_ops nil)
    (complex type-decl nil complex_types nil)
    (nz_sq_abs_pos application-judgement "posreal" complex_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (Im_fun_rew formula-decl nil complex_fun_ops nil)
    (Im_div1 formula-decl nil complex_types nil)
    (Re_fun_rew formula-decl nil complex_fun_ops nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(c_fun_eq1 0
  (c_fun_eq1-1 nil 3509264900
   ("" (skosimp) (("" (expand "=" 1 1) (("" (propax) nil nil)) nil))
    nil)
   ((= const-decl "bool" complex_fun_ops nil)) shostak))
(c_fun_ne1 0
  (c_fun_ne1-1 nil 3509264963
   ("" (skosimp) (("" (expand "/=") (("" (propax) nil nil)) nil)) nil)
   ((/= const-decl "bool" complex_fun_ops nil)) shostak)))

¤ Dauer der Verarbeitung: 0.87 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.