products/sources/formale Sprachen/Coq/test-suite/output/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: complex_fun_ops.prf   Sprache: Coq

(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.16 Sekunden  (vorverarbeitet)  ]