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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: KLV.vdmpp   Sprache: VDM

Original von: PVS©

(polar
 (argrng_TCC1 0
  (argrng_TCC1-1 nil 3297457117
   ("" (assert) (("" (typepred "pi") (("" (assertnil nil)) nil)) nil)
   ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     "trig/")
    (pi_ub const-decl "posreal" trig_basic "trig/")
    (< const-decl "bool" reals nil)
    (pi_lb const-decl "posreal" trig_basic "trig/")
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
     complex_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   shostak))
 (abs_TCC1 0
  (abs_TCC1-1 nil 3294310508
   ("" (skosimp)
    (("" (lemma "complex_is_Re_Im" ("z" "z!1"))
      (("" (expand "conjugate")
        (("" (name-replace "R" "Re(z!1)")
          (("" (name-replace "II" "Im(z!1)")
            (("" (replace -1)
              (("" (hide -1)
                (("" (assert)
                  (("" (rewrite "sq.sq_rew")
                    (("" (rewrite "sq.sq_rew")
                      (("" (lemma "i_axiom")
                        (("" (rewrite "associative_mult" :dir rl)
                          (("" (expand "sq" -1)
                            (("" (replace -1) (("" (assertnil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((complex nonempty-type-from-decl nil complex_types nil)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     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)
    (complex_is_Re_Im formula-decl nil arithmetic nil)
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (i const-decl "complex" complex_types nil)
    (Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (complex_plus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (associative_mult formula-decl nil number_fields nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (i_axiom formula-decl nil complex_types nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
     complex_types nil)
    (sq_rew formula-decl nil sq "reals/")
    (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil)
    (conjugate const-decl "complex" arithmetic nil)
    (complex_minus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (Re_is_real application-judgement "real" complex_types nil)
    (Im_is_real application-judgement "real" complex_types nil))
   shostak))
 (abs_def 0
  (abs_def-1 nil 3385303712
   ("" (skosimp)
    (("" (expand "abs")
      (("" (lemma "complex_is_Re_Im" ("z" "z!1"))
        (("" (name-replace "DRL100" "conjugate(z!1)")
          ((""
            (name-replace "DRL101"
             "sqrt(sq.sq(Im(z!1)) + sq.sq(Re(z!1)))")
            (("" (replace -1)
              (("" (hide -1)
                (("" (expand "DRL100")
                  (("" (expand "conjugate")
                    (("" (rewrite "associative_mult" 1 :dir rl)
                      (("" (rewrite "associative_mult" 1 :dir rl)
                        (("" (rewrite "associative_mult" 1 :dir rl)
                          (("" (rewrite "i_axiom")
                            (("" (expand "DRL101")
                              ((""
                                (expand "sq")
                                ((""
                                  (rewrite "associative_mult")
                                  (("" (rewrite "minus_add"nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((abs const-decl "nnreal" polar nil)
    (conjugate const-decl "complex" arithmetic nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (DRL100 skolem-const-decl "complex" polar nil)
    (associative_mult formula-decl nil number_fields nil)
    (DRL101 skolem-const-decl
     "{nnz: nnreal | nnz * nnz = sq.sq(Im(z!1)) + sq.sq(Re(z!1))}"
     polar nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_add formula-decl nil number_fields nil)
    (minus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
     complex_types nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (i_axiom formula-decl nil complex_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types nil)
    (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil)
    (i const-decl "complex" complex_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types 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)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (complex_plus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (complex_is_Re_Im formula-decl nil arithmetic 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)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil))
   shostak))
 (abs_real_rew 0
  (abs_real_rew-1 nil 3385304274
   ("" (skosimp)
    (("" (rewrite "abs_def")
      (("" (rewrite "Im_real")
        (("" (rewrite "Re_real")
          (("" (expand "sq" 1 1) (("" (rewrite "sqrt_sq_abs"nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (abs_def formula-decl nil polar 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)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (complex_plus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (Re_real formula-decl nil arithmetic nil)
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (Im_real formula-decl nil arithmetic nil))
   shostak))
 (abs_imag_rew 0
  (abs_imag_rew-1 nil 3596359128
   ("" (skeep)
    (("" (rewrite "abs_def")
      (("" (rewrite "Re_imag")
        (("" (rewrite "Im_imag")
          (("" (case "sq.sq(0) = 0")
            (("1" (replaces -1)
              (("1" (assert)
                (("1" (lemma "sqrt_sq")
                  (("1" (inst - "real_defs.abs(r)")
                    (("1" (assertnil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2) (("2" (grind) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (abs_def formula-decl nil polar 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)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (i const-decl "complex" complex_types nil)
    (complex_plus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (Im_imag formula-decl nil arithmetic nil)
    (sqrt_sq formula-decl nil sqrt "reals/")
    (sq_abs formula-decl nil sq "reals/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Re_imag formula-decl nil arithmetic nil))
   shostak))
 (abs_nzcomplex 0
  (abs_nzcomplex-1 nil 3294771107
   ("" (skosimp)
    (("" (expand "abs")
      (("" (lemma "nz_sq_abs_pos" ("n0z" "n0z!1"))
        (("" (lemma "sqrt_pos" ("px" "n0z!1 * conjugate(n0z!1)"))
          (("1" (propax) nil nil)
           ("2" (expand "conjugate") (("2" (assertnil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((abs const-decl "nnreal" polar nil)
    (conjugate const-decl "complex" arithmetic 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)
    (sqrt_pos judgement-tcc nil sqrt "reals/")
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (complex_minus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (Re_is_real application-judgement "real" complex_types nil)
    (Im_is_real application-judgement "real" complex_types nil)
    (nz_sq_abs_pos formula-decl nil arithmetic 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)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil))
   shostak))
 (abs_nz_iff_nz 0
  (abs_nz_iff_nz-1 nil 3294771228
   ("" (skosimp)
    (("" (prop)
      (("1" (replace -2) (("1" (grind) nil nil)) nil)
       ("2" (lemma "abs_nzcomplex" ("n0z" "z!1"))
        (("1" (propax) nil nil) ("2" (assertnil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (complex_minus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (abs const-decl "nnreal" polar nil)
    (sqrt_0 formula-decl nil sqrt "reals/")
    (conjugate const-decl "complex" arithmetic nil)
    (abs_nzcomplex formula-decl nil polar 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)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil))
   shostak))
 (abs_is_0 0
  (abs_is_0-1 nil 3295007153
   ("" (skosimp)
    (("" (prop)
      (("1" (typepred "abs(z!1)")
        (("1" (expand ">=")
          (("1" (expand "<=")
            (("1" (split)
              (("1" (lemma "abs_nz_iff_nz" ("z" "z!1"))
                (("1" (assertnil nil)) nil)
               ("2" (hide -1)
                (("2" (expand "abs")
                  (("2" (rewrite "sq_abs_def")
                    (("2" (rewrite "sq.sq_rew")
                      (("2" (rewrite "sq.sq_rew")
                        (("2" (rewrite "complex_is_0_Re_Im" 1)
                          (("2" (typepred "sq.sq(Im(z!1))")
                            (("2" (typepred "sq.sq(Re(z!1))")
                              (("2"
                                (lemma
                                 "sqrt_eq"
                                 ("nny"
                                  "sq.sq(Im(z!1)) + sq.sq(Re(z!1))"
                                  "nnz"
                                  "0"))
                                (("2"
                                  (rewrite "sqrt_0")
                                  (("2"
                                    (replace -1 -4)
                                    (("2"
                                      (hide -1)
                                      (("2"
                                        (lemma "sq.sq_nz_pos")
                                        (("2"
                                          (case-replace "Re(z!1) = 0")
                                          (("1"
                                            (inst - "Im(z!1)")
                                            (("1" (assertnil nil)
                                             ("2" (assertnil nil))
                                            nil)
                                           ("2"
                                            (inst - "Re(z!1)")
                                            (("1" (assertnil nil)
                                             ("2" (assertnil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (replace -1)
        (("2" (expand "abs")
          (("2" (rewrite "zero_times1")
            (("2" (rewrite "sqrt_0"nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs_nz_iff_nz formula-decl nil polar nil)
    (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil)
    (i const-decl "complex" complex_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq_rew formula-decl nil sq "reals/")
    (complex_is_0_Re_Im formula-decl nil arithmetic nil)
    (sqrt_0 formula-decl nil sqrt "reals/")
    (sq_0 formula-decl nil sq "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (z!1 skolem-const-decl "complex" polar nil)
    (/= const-decl "boolean" notequal nil)
    (sq_nz_pos judgement-tcc nil sq "reals/")
    (sqrt_eq formula-decl nil sqrt "reals/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types nil)
    (complex_plus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (sq_abs_def formula-decl nil arithmetic nil)
    (<= const-decl "bool" reals nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (abs const-decl "nnreal" polar nil)
    (conjugate const-decl "complex" arithmetic nil)
    (zero_times1 formula-decl nil number_fields_bis nil))
   shostak))
 (abs_neg 0
  (abs_neg-1 nil 3294998991
   ("" (skosimp)
    (("" (expand "abs")
      (("" (rewrite "conjugate_neg")
        (("" (rewrite "neg_times_neg"nil nil)) nil))
      nil))
    nil)
   ((minus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (abs const-decl "nnreal" polar nil)
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (conjugate const-decl "complex" arithmetic nil)
    (neg_times_neg formula-decl nil number_fields_bis nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     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)
    (conjugate_neg formula-decl nil arithmetic nil))
   shostak))
 (abs_mult 0
  (abs_mult-1 nil 3294697248
   ("" (expand "abs")
    (("" (skolem 1 ("a" "b"))
      (("" (lemma "sq_abs_nonneg" ("z" "a"))
        (("" (lemma "sq_abs_nonneg" ("z" "b"))
          (("" (lemma "sq_abs_nonneg" ("z" "a*b"))
            (("" (rewrite "sqrt_times" :dir rl)
              (("1" (assert)
                (("1" (rewrite "conjugate_times"nil nil)) nil)
               ("2" (assert)
                (("2" (expand "conjugate") (("2" (propax) nil nil))
                  nil))
                nil)
               ("3" (expand "conjugate") (("3" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_abs_realpred formula-decl nil arithmetic nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_times formula-decl nil sqrt "reals/")
    (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)
    (conjugate const-decl "complex" arithmetic nil)
    (conjugate_times formula-decl nil arithmetic nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq_abs_nonneg formula-decl nil arithmetic 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)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (abs const-decl "nnreal" polar nil)
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil))
   shostak))
 (abs_inv_TCC1 0
  (abs_inv_TCC1-1 nil 3294998917
   ("" (skosimp) (("" (rewrite "abs_is_0"nil nil)) nil)
   ((abs_is_0 formula-decl nil polar 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)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil))
   shostak))
 (abs_inv 0
  (abs_inv-1 nil 3294999199
   ("" (skosimp)
    (("" (expand "abs")
      (("" (rewrite "conjugate_inv")
        (("" (lemma "conjugate_nz" ("n0z" "n0z!1"))
          (("" (rewrite "div_times")
            (("" (lemma "nz_sq_abs_pos" ("n0z" "n0z!1"))
              (("" (rewrite "sqrt_div")
                (("" (expand "conjugate") (("" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nzcomplex_div_nzcomplex_is_nzcomplex application-judgement
     "nzcomplex" complex_types nil)
    (abs const-decl "nnreal" polar nil)
    (conjugate_nz formula-decl nil arithmetic nil)
    (nz_sq_abs_pos formula-decl nil arithmetic nil)
    (sqrt_div formula-decl nil sqrt "reals/")
    (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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sqrt_1 formula-decl nil sqrt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_abs_realpred formula-decl nil arithmetic nil)
    (nzcomplex_times_nzcomplex_is_nzcomplex application-judgement
     "nzcomplex" complex_types nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (odd_times_odd_is_odd application-judgement "odd_int" integers nil)
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (div_times formula-decl nil number_fields_bis nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (conjugate const-decl "complex" arithmetic nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (/= const-decl "boolean" notequal nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     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)
    (conjugate_inv formula-decl nil arithmetic nil))
   shostak))
 (abs_div 0
  (abs_div-1 nil 3294999065
   ("" (skosimp)
    (("" (lemma "div_def" ("y" "z!1" "n0x" "n0z!1"))
      (("" (lemma "abs_mult" ("z1" "z!1" "z2" "1/n0z!1"))
        (("1" (rewrite "abs_inv" -1) (("1" (assertnil nil)) nil)
         ("2" (lemma "real_is_complex" ("x" "1"))
          (("2" (rewrite "closed_divides"nil nil)) nil))
        nil))
      nil))
    nil)
   ((numfield nonempty-type-eq-decl nil number_fields nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal 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)
    (div_def formula-decl nil number_fields nil)
    (abs_inv formula-decl nil polar nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (complex_div_nzcomplex_is_complex application-judgement "complex"
     complex_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nzcomplex_div_nzcomplex_is_nzcomplex application-judgement
     "nzcomplex" complex_types nil)
    (abs_mult formula-decl nil polar nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil))
   shostak))
 (abs_triangle 0
  (abs_triangle-2 nil 3307889278
   ("" (skolem 1 ("a" "b"))
    (("" (expand "abs")
      (("" (lemma "sq_abs_nonneg" ("z" "a"))
        (("" (lemma "sq_abs_nonneg" ("z" "b"))
          (("" (lemma "sq_abs_nonneg" ("z" "a+b"))
            (("" (case "real_pred(a * conjugate(a))")
              (("1" (case "real_pred(b * conjugate(b))")
                (("1" (case "real_pred((a+b) * conjugate(a+b))")
                  (("1" (name "A2" "a * conjugate(a)")
                    (("1" (replace -1)
                      (("1" (name "B2" "b * conjugate(b)")
                        (("1" (replace -1)
                          (("1" (name "AB2" "(a+b) * conjugate(a+b)")
                            (("1" (replace -1)
                              (("1"
                                (case-replace
                                 "conjugate(a + b) * a + conjugate(a + b) * b = AB2")
                                (("1"
                                  (rewrite "sq_le" 1 :dir rl)
                                  (("1"
                                    (rewrite "sqrt.sq_sqrt")
                                    (("1"
                                      (rewrite "sq.sq_plus")
                                      (("1"
                                        (rewrite "sqrt.sq_sqrt")
                                        (("1"
                                          (rewrite "sqrt.sq_sqrt")
                                          (("1"
                                            (rewrite
                                             "sqrt.sqrt_times"
                                             1
                                             :dir
                                             rl)
                                            (("1"
                                              (rewrite
                                               "conjugate_plus")
                                              (("1"
                                                (rewrite
                                                 "distributive"
                                                 -2)
                                                (("1"
                                                  (lemma
                                                   "commutative_mult")
                                                  (("1"
                                                    (inst-cp
                                                     -
                                                     "a"
                                                     "conjugate(a)")
                                                    (("1"
                                                      (inst-cp
                                                       -
                                                       "b"
                                                       "conjugate(b)")
                                                      (("1"
                                                        (replace
                                                         -2
                                                         *
                                                         rl)
                                                        (("1"
                                                          (replace
                                                           -3
                                                           *
                                                           rl)
                                                          (("1"
                                                            (replace
                                                             -6)
                                                            (("1"
                                                              (replace
                                                               -7)
                                                              (("1"
                                                                (hide
                                                                 -4)
                                                                (("1"
                                                                  (name
                                                                   "DRL"
                                                                   "conjugate(a) * b + conjugate(b) * a")
                                                                  (("1"
                                                                    (case-replace
                                                                     "A2 + conjugate(a) * b + conjugate(b) * a + B2 = A2+B2+DRL")
                                                                    (("1"
                                                                      (case
                                                                       "real_pred(DRL)")
                                                                      (("1"
                                                                        (hide
                                                                         -2)
                                                                        (("1"
                                                                          (replace
                                                                           -6
                                                                           1
                                                                           rl)
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (case
                                                                               "A2*B2>=0")
                                                                              (("1"
                                                                                (lemma
                                                                                 "both_sides_plus_le2"
                                                                                 ("z"
                                                                                  "A2+B2"
                                                                                  "x"
                                                                                  "DRL"
                                                                                  "y"
                                                                                  "2*sqrt(A2 * B2)"))
                                                                                (("1"
                                                                                  (case
                                                                                   "DRL<=2 * sqrt(A2 * B2)")
                                                                                  (("1"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil)
                                                                                   ("2"
                                                                                    (hide
                                                                                     -1
                                                                                     2)
                                                                                    (("2"
                                                                                      (name-replace
                                                                                       "CA"
                                                                                       "conjugate(a)")
                                                                                      (("2"
                                                                                        (name-replace
                                                                                         "CB"
                                                                                         "conjugate(b)")
                                                                                        (("2"
                                                                                          (lemma
                                                                                           "complex_is_Re_Im"
                                                                                           ("z"
                                                                                            "a"))
                                                                                          (("2"
                                                                                            (lemma
                                                                                             "complex_is_Re_Im"
                                                                                             ("z"
                                                                                              "b"))
                                                                                            (("2"
                                                                                              (replace
                                                                                               -1
                                                                                               -5)
                                                                                              (("2"
                                                                                                (replace
                                                                                                 -2
                                                                                                 -5)
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "CA")
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "CB")
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "conjugate")
                                                                                                      (("2"
                                                                                                        (case-replace
                                                                                                         "DRL = 2*(Re(a)*Re(b)+Im(a)*Im(b))")
                                                                                                        (("1"
                                                                                                          (lemma
                                                                                                           "both_sides_times_pos_le1"
                                                                                                           ("pz"
                                                                                                            "2"
                                                                                                            "x"
                                                                                                            "Re(a) * Re(b) + Im(a) * Im(b)"
                                                                                                            "y"
                                                                                                            "sqrt(A2 * B2)"))
                                                                                                          (("1"
                                                                                                            (replace
                                                                                                             -1
                                                                                                             1)
                                                                                                            (("1"
                                                                                                              (hide
                                                                                                               -1)
                                                                                                              (("1"
                                                                                                                (lemma
                                                                                                                 "reals.closed_divides"
                                                                                                                 ("x"
                                                                                                                  "2 * (Re(a) * Re(b) + Im(a) * Im(b))"
                                                                                                                  "n0z"
                                                                                                                  "2"))
                                                                                                                (("1"
                                                                                                                  (rewrite
                                                                                                                   "times_div1"
                                                                                                                   -1
                                                                                                                   :dir
                                                                                                                   rl)
                                                                                                                  (("1"
                                                                                                                    (rewrite
                                                                                                                     "div_cancel1"
                                                                                                                     1)
                                                                                                                    (("1"
                                                                                                                      (case
                                                                                                                       "Im(a) * Im(b) + Re(a) * Re(b) < 0")
                                                                                                                      (("1"
                                                                                                                        (assert)
                                                                                                                        nil
                                                                                                                        nil)
                                                                                                                       ("2"
                                                                                                                        (rewrite
                                                                                                                         "sq_le"
                                                                                                                         2
                                                                                                                         :dir
                                                                                                                         rl)
                                                                                                                        (("2"
                                                                                                                          (rewrite
                                                                                                                           "sq_sqrt")
                                                                                                                          (("2"
                                                                                                                            (expand
                                                                                                                             "B2"
                                                                                                                             2)
                                                                                                                            (("2"
                                                                                                                              (rewrite
                                                                                                                               "sq_abs_def"
                                                                                                                               2)
                                                                                                                              (("2"
                                                                                                                                (name-replace
                                                                                                                                 "DRL_B"
                                                                                                                                 "(Im(b) * Im(b) + Re(b) * Re(b))")
                                                                                                                                (("2"
                                                                                                                                  (expand
                                                                                                                                   "A2")
                                                                                                                                  (("2"
                                                                                                                                    (lemma
                                                                                                                                     "sq_abs_def"
                                                                                                                                     ("z"
                                                                                                                                      "a"))
                                                                                                                                    (("2"
                                                                                                                                      (inst-cp
                                                                                                                                       -9
                                                                                                                                       "conjugate(a)"
                                                                                                                                       "DRL_B")
                                                                                                                                      (("2"
                                                                                                                                        (replace
                                                                                                                                         -10
                                                                                                                                         2)
                                                                                                                                        (("2"
                                                                                                                                          (rewrite
                                                                                                                                           "associative_mult"
                                                                                                                                           2
                                                                                                                                           :dir
                                                                                                                                           rl)
                                                                                                                                          (("2"
                                                                                                                                            (inst-cp
                                                                                                                                             -9
                                                                                                                                             "conjugate(a)"
                                                                                                                                             "a")
                                                                                                                                            (("2"
                                                                                                                                              (replace
                                                                                                                                               -10
                                                                                                                                               2)
                                                                                                                                              (("2"
                                                                                                                                                (replace
                                                                                                                                                 -1
                                                                                                                                                 2)
                                                                                                                                                (("2"
                                                                                                                                                  (expand
                                                                                                                                                   "DRL_B")
                                                                                                                                                  (("2"
                                                                                                                                                    (expand
                                                                                                                                                     "sq")
                                                                                                                                                    (("2"
                                                                                                                                                      (assert)
                                                                                                                                                      (("2"
                                                                                                                                                        (name
                                                                                                                                                         "IA"
                                                                                                                                                         "Im(a)")
                                                                                                                                                        (("2"
                                                                                                                                                          (replace
                                                                                                                                                           -1)
                                                                                                                                                          (("2"
                                                                                                                                                            (name
                                                                                                                                                             "IB"
                                                                                                                                                             "Im(b)")
                                                                                                                                                            (("2"
                                                                                                                                                              (replace
                                                                                                                                                               -1)
                                                                                                                                                              (("2"
                                                                                                                                                                (name
                                                                                                                                                                 "RB"
                                                                                                                                                                 "Re(b)")
                                                                                                                                                                (("2"
                                                                                                                                                                  (replace
                                                                                                                                                                   -1)
                                                                                                                                                                  (("2"
                                                                                                                                                                    (name
                                                                                                                                                                     "RA"
                                                                                                                                                                     "Re(a)")
                                                                                                                                                                    (("2"
                                                                                                                                                                      (replace
                                                                                                                                                                       -1)
                                                                                                                                                                      (("2"
                                                                                                                                                                        (name-replace
                                                                                                                                                                         "DRL10"
                                                                                                                                                                         "IA * IA * IB * IB ")
                                                                                                                                                                        (("2"
                                                                                                                                                                          (name-replace
                                                                                                                                                                           "DRL11"
                                                                                                                                                                           "RA * RA * RB * RB ")
                                                                                                                                                                          (("2"
                                                                                                                                                                            (assert)
                                                                                                                                                                            (("2"
                                                                                                                                                                              (lemma
                                                                                                                                                                               "both_sides_plus_le2"
                                                                                                                                                                               ("z"
                                                                                                                                                                                "DRL10 + DRL11"
                                                                                                                                                                                "x"
                                                                                                                                                                                "2 * (IA * IB * RA * RB)"
                                                                                                                                                                                "y"
                                                                                                                                                                                "IA * IA * RB * RB + IB * IB * RA * RA"))
                                                                                                                                                                              (("2"
                                                                                                                                                                                (replace
                                                                                                                                                                                 -1
                                                                                                                                                                                 2)
                                                                                                                                                                                (("2"
                                                                                                                                                                                  (hide-all-but
                                                                                                                                                                                   (1
                                                                                                                                                                                    2))
                                                                                                                                                                                  (("2"
                                                                                                                                                                                    (case
                                                                                                                                                                                     "IA*IB >= -(RA*RB)")
                                                                                                                                                                                    (("1"
                                                                                                                                                                                      (hide
                                                                                                                                                                                       1)
                                                                                                                                                                                      (("1"
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.72 Sekunden  (vorverarbeitet)  ¤





Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff