products/sources/formale Sprachen/Java/openjdk-20-36_src/.jcheck/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: restriction_cont_fun.pvs   Sprache: Unknown

(hyperbolicx
 (sinh_lemma 0
  (sinh_lemma-1 nil 3394197876
   ("" (skosimp)
    (("" (expand "sinh")
      (("" (expand "cauchy_sinh")
        (("" (lemma "exp_lemma" ("x" "x!1" "cx" "cx!1"))
          (("" (lemma "neg_lemma" ("x" "x!1" "cx" "cx!1"))
            (("" (assert)
              ((""
                (lemma "exp_lemma"
                 ("x" "-x!1" "cx" "cauchy_neg(cx!1)"))
                (("" (assert)
                  ((""
                    (lemma "sub_lemma"
                     ("x" "exp(x!1)" "cx" "cauchy_exp(cx!1)" "y"
                      "exp(-x!1)" "cy" "cauchy_exp(cauchy_neg(cx!1))"))
                    (("" (assert)
                      ((""
                        (lemma "lemma_div2n"
                         ("x" "exp(x!1) - exp(-x!1)" "cx"
                          "cauchy_sub(cauchy_exp(cx!1),cauchy_exp(cauchy_neg(cx!1)))"
                          "n" "1"))
                        (("" (assert)
                          (("" (expand "div2n")
                            (("" (rewrite "expt_x1") nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sinh const-decl "real" hyperbolic "lnexp_fnd/")
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (exp_lemma formula-decl nil exp nil)
    (cauchy_exp_is_posreal application-judgement "cauchy_posreal" exp
     nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (div2n const-decl "real" shift nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (cauchy_sub const-decl "cauchy_real" sub nil)
    (lemma_div2n formula-decl nil shift nil)
    (sub_lemma formula-decl nil sub nil)
    (cauchy_exp const-decl "[nat -> int]" exp nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (ln const-decl "real" ln_exp "lnexp_fnd/")
    (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cauchy_neg const-decl "cauchy_real" neg nil)
    (neg_lemma formula-decl nil neg nil)
    (cauchy_sinh const-decl "[nat -> int]" hyperbolicx nil))
   shostak))
 (cosh_lemma 0
  (cosh_lemma-1 nil 3394198044
   ("" (skosimp)
    (("" (expand "cauchy_cosh")
      (("" (expand "cosh")
        (("" (lemma "neg_lemma" ("x" "x!1" "cx" "cx!1"))
          (("" (assert)
            (("" (lemma "exp_lemma" ("x" "x!1" "cx" "cx!1"))
              ((""
                (lemma "exp_lemma"
                 ("x" "-x!1" "cx" "cauchy_neg(cx!1)"))
                (("" (assert)
                  ((""
                    (lemma "add_lemma"
                     ("x" "exp(x!1)" "cx" "cauchy_exp(cx!1)" "y"
                      "exp(-x!1)" "cy" "cauchy_exp(cauchy_neg(cx!1))"))
                    (("" (assert)
                      ((""
                        (lemma "lemma_div2n"
                         ("x" "exp(-x!1) + exp(x!1)" "cx"
                          "cauchy_add(cauchy_exp(cx!1),cauchy_exp(cauchy_neg(cx!1)))"
                          "n" "1"))
                        (("" (assert)
                          (("" (expand "div2n")
                            (("" (rewrite "expt_x1") nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_cosh const-decl "[nat -> int]" hyperbolicx nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (neg_lemma formula-decl nil neg nil)
    (exp_lemma formula-decl nil exp nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (div2n const-decl "real" shift nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (cauchy_add const-decl "cauchy_real" add nil)
    (lemma_div2n formula-decl nil shift nil)
    (add_lemma formula-decl nil add nil)
    (cauchy_exp const-decl "[nat -> int]" exp nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (ln const-decl "real" ln_exp "lnexp_fnd/")
    (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cauchy_neg const-decl "cauchy_real" neg nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (cauchy_exp_is_posreal application-judgement "cauchy_posreal" exp
     nil)
    (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/"))
   shostak))
 (cauchy_sinh_type 0
  (cauchy_sinh_type-1 nil 3394196253
   ("" (skosimp)
    (("" (typepred "cx!1")
      (("" (expand "cauchy_real?")
        (("" (skosimp)
          (("" (lemma "sinh_lemma" ("x" "x!1" "cx" "cx!1"))
            (("" (inst + "sinh(x!1)") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sinh const-decl "real" hyperbolic "lnexp_fnd/")
    (sinh_lemma formula-decl nil hyperbolicx nil))
   nil))
 (cauchy_cosh_type 0
  (cauchy_cosh_type-1 nil 3394196253
   ("" (skosimp)
    (("" (typepred "cx!1")
      (("" (expand "cauchy_real?")
        (("" (skosimp)
          (("" (lemma "cosh_lemma" ("x" "x!1" "cx" "cx!1"))
            (("" (expand "cauchy_posreal?")
              (("" (inst + "cosh(x!1)")
                (("1" (assert) nil nil)
                 ("2" (typepred "cosh(x!1)") (("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (cauchy_posreal? const-decl "bool" cauchy nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (x!1 skolem-const-decl "real" hyperbolicx nil)
    (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/")
    (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")
    (AND const-decl "[bool, bool -> bool]" 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)
    (cosh_lemma formula-decl nil hyperbolicx nil))
   nil))
 (cauchy_coth_TCC1 0
  (cauchy_coth_TCC1-1 nil 3394195229
   ("" (skosimp)
    (("" (typepred "cnzx!1")
      (("" (expand "cauchy_nzreal?")
        (("" (skosimp)
          (("" (lemma "sinh_lemma" ("x" "x!1" "cx" "cnzx!1"))
            (("" (assert)
              (("" (inst + "sinh(x!1)")
                (("" (hide -1 -2)
                  (("" (typepred "x!1")
                    (("" (lemma "sinh_strict_increasing")
                      (("" (expand "strict_increasing?")
                        (("" (lemma "trichotomy" ("x" "x!1"))
                          (("" (split -1)
                            (("1" (inst - "0" "x!1")
                              (("1"
                                (rewrite "sinh_0")
                                (("1" (assert) nil nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil)
                             ("3" (inst - "x!1" "0")
                              (("3"
                                (rewrite "sinh_0")
                                (("3" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sinh_strict_increasing formula-decl nil hyperbolic "lnexp_fnd/")
    (trichotomy formula-decl nil real_axioms nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sinh_0 formula-decl nil hyperbolic "lnexp_fnd/")
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (x!1 skolem-const-decl "nzreal" hyperbolicx nil)
    (sinh const-decl "real" hyperbolic "lnexp_fnd/")
    (sinh_lemma formula-decl nil hyperbolicx nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil))
   nil))
 (tanh_lemma 0
  (tanh_lemma-1 nil 3394198250
   ("" (skosimp)
    (("" (expand "tanh")
      (("" (expand "cauchy_tanh")
        (("" (lemma "sinh_lemma" ("x" "x!1" "cx" "cx!1"))
          (("" (lemma "cosh_lemma" ("x" "x!1" "cx" "cx!1"))
            (("" (assert)
              ((""
                (lemma "div_lemma"
                 ("x" "sinh(x!1)" "cx" "cauchy_sinh(cx!1)" "nzy"
                  "cosh(x!1)" "nzcy" "cauchy_cosh(cx!1)"))
                (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tanh const-decl "real_abs_lt1" hyperbolic "lnexp_fnd/")
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sinh_lemma formula-decl nil hyperbolicx nil)
    (cauchy_cosh_type application-judgement "cauchy_posreal"
     hyperbolicx nil)
    (cauchy_sinh_type application-judgement "cauchy_real" hyperbolicx
     nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_lemma formula-decl nil div nil)
    (cauchy_sinh const-decl "[nat -> int]" hyperbolicx nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_cosh const-decl "[nat -> int]" hyperbolicx nil)
    (/= const-decl "boolean" notequal nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")
    (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/")
    (sinh const-decl "real" hyperbolic "lnexp_fnd/")
    (cosh_lemma formula-decl nil hyperbolicx nil)
    (cauchy_tanh const-decl "[nat -> int]" hyperbolicx nil))
   shostak))
 (sech_lemma 0
  (sech_lemma-1 nil 3394198358
   ("" (skosimp)
    (("" (expand "sech")
      (("" (expand "cauchy_sech")
        (("" (lemma "cosh_lemma" ("x" "x!1" "cx" "cx!1"))
          (("" (assert)
            ((""
              (lemma "inv_lemma"
               ("nzx" "cosh(x!1)" "nzcx" "cauchy_cosh(cx!1)"))
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sech const-decl "posreal_le1" hyperbolic "lnexp_fnd/")
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (cosh_lemma formula-decl nil hyperbolicx nil)
    (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/")
    (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (cauchy_cosh const-decl "[nat -> int]" hyperbolicx nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (inv_lemma formula-decl nil inv nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (cauchy_cosh_type application-judgement "cauchy_posreal"
     hyperbolicx nil)
    (cauchy_sech const-decl "[nat -> int]" hyperbolicx nil))
   shostak))
 (coth_lemma 0
  (coth_lemma-1 nil 3394198526
   ("" (skosimp)
    (("" (expand "cauchy_coth")
      (("" (expand "coth")
        (("" (lemma "sinh_lemma" ("x" "nzx!1" "cx" "cnzx!1"))
          (("" (lemma "cosh_lemma" ("x" "nzx!1" "cx" "cnzx!1"))
            (("" (assert)
              (("" (expand "tanh")
                (("" (rewrite "div_div1")
                  (("1" (assert)
                    (("1"
                      (lemma "div_lemma"
                       ("x" "cosh(nzx!1)" "cx" "cauchy_cosh(cnzx!1)"
                        "nzy" "sinh(nzx!1)" "nzcy"
                        "cauchy_sinh(cnzx!1)"))
                      (("1" (assert) nil nil)) nil))
                    nil)
                   ("2" (hide-all-but 1)
                    (("2" (lemma "sinh_0")
                      (("2" (lemma "sinh_strict_increasing")
                        (("2" (expand "strict_increasing?")
                          (("2" (lemma "trichotomy" ("x" "nzx!1"))
                            (("2" (split -1)
                              (("1"
                                (inst - "0" "nzx!1")
                                (("1" (assert) nil nil))
                                nil)
                               ("2" (assert) nil nil)
                               ("3"
                                (inst - "nzx!1" "0")
                                (("3" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_coth const-decl "[nat -> int]" hyperbolicx nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sinh_lemma formula-decl nil hyperbolicx nil)
    (cauchy_sinh_type application-judgement "cauchy_real" hyperbolicx
     nil)
    (cauchy_cosh_type application-judgement "cauchy_posreal"
     hyperbolicx nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/")
    (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")
    (sinh const-decl "real" hyperbolic "lnexp_fnd/")
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_div1 formula-decl nil real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (div_lemma formula-decl nil div nil)
    (cauchy_cosh const-decl "[nat -> int]" hyperbolicx nil)
    (cauchy_sinh const-decl "[nat -> int]" hyperbolicx nil)
    (sinh_0 formula-decl nil hyperbolic "lnexp_fnd/")
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (trichotomy formula-decl nil real_axioms nil)
    (sinh_strict_increasing formula-decl nil hyperbolic "lnexp_fnd/")
    (tanh const-decl "real_abs_lt1" hyperbolic "lnexp_fnd/")
    (cosh_lemma formula-decl nil hyperbolicx nil)
    (coth const-decl "real_abs_gt1" hyperbolic "lnexp_fnd/"))
   shostak))
 (csch_lemma 0
  (csch_lemma-1 nil 3394198422
   ("" (skosimp)
    (("" (lemma "sinh_lemma" ("x" "nzx!1" "cx" "cnzx!1"))
      (("" (assert)
        (("" (expand "cauchy_csch")
          (("" (expand "csch")
            ((""
              (lemma "inv_lemma"
               ("nzx" "sinh(nzx!1)" "nzcx" "cauchy_sinh(cnzx!1)"))
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sinh_lemma formula-decl nil hyperbolicx nil)
    (cauchy_csch const-decl "[nat -> int]" hyperbolicx nil)
    (cauchy_sinh_type application-judgement "cauchy_real" hyperbolicx
     nil)
    (inv_lemma formula-decl nil inv nil)
    (cauchy_sinh const-decl "[nat -> int]" hyperbolicx nil)
    (sinh const-decl "real" hyperbolic "lnexp_fnd/")
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (csch const-decl "real" hyperbolic "lnexp_fnd/"))
   shostak))
 (cauchy_tanh_type 0
  (cauchy_tanh_type-1 nil 3394196253
   ("" (skosimp)
    (("" (typepred "cx!1")
      (("" (expand "cauchy_real?")
        (("" (skosimp)
          (("" (lemma "tanh_lemma" ("x" "x!1" "cx" "cx!1"))
            (("" (assert)
              (("" (typepred "tanh(x!1)")
                (("" (expand "cauchy_smallreal?")
                  (("" (inst + "tanh(x!1)") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (cauchy_smallreal? const-decl "bool" cauchy nil)
    (smallreal nonempty-type-eq-decl nil prelude_aux nil)
    (tanh const-decl "real_abs_lt1" hyperbolic "lnexp_fnd/")
    (real_abs_lt1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (tanh_lemma formula-decl nil hyperbolicx nil))
   nil))
 (cauchy_coth_type 0
  (cauchy_coth_type-1 nil 3394196253
   ("" (skosimp)
    (("" (typepred "cnzx!1")
      (("" (expand "cauchy_nzreal?")
        (("" (skosimp)
          (("" (lemma "coth_lemma" ("nzx" "x!1" "cnzx" "cnzx!1"))
            (("" (assert)
              (("" (typepred "coth(x!1)")
                (("" (inst + "coth(x!1)")
                  (("" (split -1)
                    (("1" (assert) nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (x!1 skolem-const-decl "nzreal" hyperbolicx nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (coth const-decl "real_abs_gt1" hyperbolic "lnexp_fnd/")
    (real_abs_gt1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (coth_lemma formula-decl nil hyperbolicx nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil))
   nil))
 (cauchy_csch_type 0
  (cauchy_csch_type-1 nil 3394196253
   ("" (skosimp)
    (("" (typepred "cnzx!1")
      (("" (expand "cauchy_nzreal?")
        (("" (skosimp)
          (("" (lemma "csch_lemma" ("nzx" "x!1" "cnzx" "cnzx!1"))
            (("" (assert)
              (("" (inst + "csch(x!1)")
                (("" (hide -1 -2)
                  (("" (expand "csch")
                    (("" (lemma "sinh_strict_increasing")
                      (("" (expand "strict_increasing?")
                        (("" (lemma "trichotomy" ("x" "x!1"))
                          (("" (split -1)
                            (("1" (inst - "0" "x!1")
                              (("1"
                                (rewrite "sinh_0")
                                (("1" (assert) nil nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil)
                             ("3" (inst - "x!1" "0")
                              (("3"
                                (rewrite "sinh_0")
                                (("3" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sinh_strict_increasing formula-decl nil hyperbolic "lnexp_fnd/")
    (trichotomy formula-decl nil real_axioms nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sinh_0 formula-decl nil hyperbolic "lnexp_fnd/")
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (x!1 skolem-const-decl "nzreal" hyperbolicx nil)
    (csch const-decl "real" hyperbolic "lnexp_fnd/")
    (csch_lemma formula-decl nil hyperbolicx nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil))
   nil))
 (cauchy_sech_type 0
  (cauchy_sech_type-1 nil 3394196253
   ("" (skosimp)
    (("" (typepred "cx!1")
      (("" (expand "cauchy_real?")
        (("" (skosimp)
          (("" (lemma "sech_lemma" ("x" "x!1" "cx" "cx!1"))
            (("" (assert)
              (("" (expand "cauchy_posreal?")
                (("" (inst + "sech(x!1)") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sech const-decl "posreal_le1" hyperbolic "lnexp_fnd/")
    (posreal_le1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")
    (<= const-decl "bool" reals 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)
    (cauchy_posreal? const-decl "bool" cauchy nil)
    (sech_lemma formula-decl nil hyperbolicx nil))
   nil))
 (cauchy_ge1_TCC1 0
  (cauchy_ge1_TCC1-1 nil 3394200357
   ("" (expand "cauchy_ge1?")
    (("" (inst + "1") (("" (rewrite "int_lemma") nil nil)) nil)) 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)
    (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (int_lemma formula-decl nil int nil)
    (cauchy_ge1? const-decl "bool" hyperbolicx nil))
   nil))
 (subtype_TCC1 0
  (subtype_TCC1-1 nil 3394200357
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "cauchy_ge1?")
        (("" (skosimp)
          (("" (expand "cauchy_posreal?") (("" (inst + "x!2") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_ge1 nonempty-type-eq-decl nil hyperbolicx nil)
    (cauchy_ge1? const-decl "bool" hyperbolicx nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (cauchy_posreal? const-decl "bool" cauchy nil))
   nil))
 (cauchy_asinh_TCC1 0
  (cauchy_asinh_TCC1-1 nil 3394199209
   ("" (skosimp)
    (("" (typepred "cx!1")
      (("" (expand "cauchy_real?")
        (("" (skosimp)
          (("" (expand "cauchy_nnreal?")
            ((""
              (lemma "mul_lemma"
               ("x" "x!1" "y" "x!1" "cx" "cx!1" "cy" "cx!1"))
              (("" (assert)
                (("" (rewrite "sq_rew")
                  ((""
                    (lemma "add_lemma"
                     ("x" "sq(x!1)" "y" "1" "cx"
                      "cauchy_mul(cx!1, cx!1)" "cy" "cauchy_int(1)"))
                    (("" (rewrite "int_lemma")
                      (("" (assert) (("" (inst + "1+sq(x!1)") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (mul_lemma formula-decl nil mul nil)
    (sq_rew formula-decl nil sq "reals/")
    (int_lemma formula-decl nil int nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (+ 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)
    (add_lemma formula-decl nil add nil)
    (cauchy_mul const-decl "cauchy_real" mul nil)
    (cauchy_int const-decl "cauchy_real" int nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (cauchy_nnreal? const-decl "bool" cauchy nil))
   nil))
 (cauchy_asinh_TCC2 0
  (cauchy_asinh_TCC2-1 nil 3508998299
   ("" (skosimp)
    (("" (typepred "cx!1")
      (("" (expand "cauchy_posreal?")
        (("" (expand "cauchy_real?")
          (("" (skosimp)
            ((""
              (lemma "mul_lemma"
               ("x" "x!1" "y" "x!1" "cx" "cx!1" "cy" "cx!1"))
              (("" (rewrite "sq_rew")
                (("" (assert)
                  ((""
                    (lemma "add_lemma"
                     ("x" "sq(x!1)" "y" "1" "cx"
                      "cauchy_mul(cx!1, cx!1)" "cy" "cauchy_int(1)"))
                    (("" (rewrite "int_lemma")
                      (("" (assert)
                        (("" (case "1+sq(x!1)>=1")
                          (("1"
                            (lemma "sqrt_lemma"
                             ("nnx" "1 + sq(x!1)" "nncx"
                              "cauchy_add(cauchy_mul(cx!1, cx!1), cauchy_int(1))"))
                            (("1" (assert)
                              (("1"
                                (lemma
                                 "add_lemma"
                                 ("x"
                                  "x!1"
                                  "y"
                                  "sqrt(1 + sq(x!1))"
                                  "cx"
                                  "cx!1"
                                  "cy"
                                  "cauchy_sqrt(cauchy_add(cauchy_mul(cx!1, cx!1),
                                         cauchy_int(1)))"))
                                (("1"
                                  (assert)
                                  (("1"
                                    (inst + "sqrt(1 + sq(x!1)) + x!1")
                                    (("1"
                                      (hide-all-but (-3 1))
                                      (("1"
                                        (lemma
                                         "sq_lt"
                                         ("nna"
                                          "abs(x!1)"
                                          "nnb"
                                          "sqrt(1 + sq(x!1))"))
                                        (("1"
                                          (rewrite "sq_abs")
                                          (("1"
                                            (rewrite "sq_sqrt")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "cauchy_nnreal?")
                              (("2" (inst + "1+sq(x!1)") nil nil))
                              nil))
                            nil)
                           ("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (mul_lemma formula-decl nil mul nil)
    (int_lemma formula-decl nil int nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     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)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sq_abs formula-decl nil sq "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (sq_lt formula-decl nil sq "reals/")
    (x!1 skolem-const-decl "real" hyperbolicx nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (cauchy_sqrt const-decl "cauchy_nnreal" sqrtx nil)
    (nnreal type-eq-decl nil real_types nil)
    (cauchy_add const-decl "cauchy_real" add nil)
    (cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nnreal? const-decl "bool" cauchy nil)
    (sqrt_lemma formula-decl nil sqrtx nil)
    (add_lemma formula-decl nil add nil)
    (cauchy_mul const-decl "cauchy_real" mul nil)
    (cauchy_int const-decl "cauchy_real" int nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_rew formula-decl nil sq "reals/")
    (cauchy_posreal? const-decl "bool" cauchy nil))
   nil))
 (cauchy_acosh_TCC1 0
  (cauchy_acosh_TCC1-2 nil 3508599835
   ("" (skosimp)
    (("" (typepred "cge1x!1")
      (("" (expand "cauchy_ge1?")
        (("" (skosimp)
          (("" (typepred "x!1")
            ((""
              (lemma "sub_lemma"
               ("x" "sq(x!1)" "y" "1" "cx"
                "cauchy_mul(cge1x!1, cge1x!1)" "cy" "cauchy_int(1)"))
              (("" (rewrite "int_lemma")
                (("" (expand "sq" -1 1)
                  (("" (rewrite "mul_lemma")
                    (("" (expand "cauchy_nnreal?")
                      (("" (inst + "sq(x!1)-1")
                        (("" (lemma "sq_le" ("nna" "1" "nnb" "x!1"))
                          (("" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_ge1 nonempty-type-eq-decl nil hyperbolicx nil)
    (cauchy_ge1? const-decl "bool" hyperbolicx nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (cauchy_int const-decl "cauchy_real" int nil)
    (cauchy_mul const-decl "cauchy_real" mul nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (sub_lemma formula-decl nil sub nil)
    (cauchy_nnreal? const-decl "bool" cauchy nil)
    (sq_le formula-decl nil sq "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sq_1 formula-decl nil sq "reals/")
    (x!1 skolem-const-decl "posreal_ge1" hyperbolicx nil)
    (nnreal 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_minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (mul_lemma formula-decl nil mul nil)
    (int_lemma formula-decl nil int nil)
    (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/"))
   nil)
  (cauchy_acosh_TCC1-1 nil 3394200357
   ("" (skosimp)
    (("" (typepred "cge1x!1")
      (("" (expand "cauchy_ge1?")
        (("" (skosimp)
          ((""
            (lemma "mul_lemma"
             ("x" "x!1" "cx" "cge1x!1" "y" "x!1" "cy" "cge1x!1"))
            (("" (rewrite "sq_rew")
              (("" (assert)
                ((""
                  (lemma "sub_lemma"
                   ("x" "sq(x!1)" "cx" "cauchy_mul(cge1x!1, cge1x!1)"
                    "y" "1" "cy" "cauchy_int(1)"))
                  (("" (rewrite "int_lemma")
                    (("" (assert)
                      (("" (expand "cauchy_nnreal?")
                        (("" (inst + "sq(x!1)-1")
                          (("" (hide-all-but 1)
                            (("" (typepred "x!1")
                              ((""
                                (lemma "sq_le" ("nna" "1" "nnb" "x!1"))
                                ((""
                                  (rewrite "sq_1")
                                  (("" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_rew formula-decl nil sq "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (cauchy_int const-decl "cauchy_real" int nil)
    (cauchy_mul const-decl "cauchy_real" mul nil)
    (sub_lemma formula-decl nil sub nil)
    (sq_1 formula-decl nil sq "reals/")
    (sq_le formula-decl nil sq "reals/")
    (cauchy_nnreal? const-decl "bool" cauchy nil)
    (int_lemma formula-decl nil int nil)
    (mul_lemma formula-decl nil mul nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/"))
   nil))
 (cauchy_acosh_TCC2 0
  (cauchy_acosh_TCC2-1 nil 3508998299
   ("" (skosimp)
    (("" (typepred "cge1x!1")
      (("" (expand "cauchy_ge1?")
        (("" (skosimp)
          (("" (typepred "x!1")
            ((""
              (lemma "sub_lemma"
               ("x" "sq(x!1)" "y" "1" "cx"
                "cauchy_mul(cge1x!1, cge1x!1)" "cy" "cauchy_int(1)"))
              (("" (rewrite "int_lemma")
                (("" (expand "sq" -1 1)
                  (("" (rewrite "mul_lemma")
                    (("" (case "sq(x!1)-1>=0")
                      (("1"
                        (lemma "sqrt_lemma"
                         ("nnx" "sq(x!1)-1" "nncx"
                          "cauchy_sub(cauchy_mul(cge1x!1, cge1x!1), cauchy_int(1))"))
                        (("1" (assert)
                          (("1"
                            (lemma "add_lemma"
                             ("x" "x!1" "cx" "cge1x!1" "y"
                              "sqrt(sq(x!1) - 1)" "cy"
                              "cauchy_sqrt(cauchy_sub(cauchy_mul(cge1x!1, cge1x!1),
                                         cauchy_int(1)))"))
                            (("1" (assert)
                              (("1"
                                (expand "cauchy_posreal?")
                                (("1"
                                  (inst + "sqrt(sq(x!1) - 1) + x!1")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (propax) nil nil))
                        nil)
                       ("2" (lemma "sq_le" ("nna" "1" "nnb" "x!1"))
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_ge1 nonempty-type-eq-decl nil hyperbolicx nil)
    (cauchy_ge1? const-decl "bool" hyperbolicx nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (cauchy_int const-decl "cauchy_real" int nil)
    (cauchy_mul const-decl "cauchy_real" mul nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (sub_lemma formula-decl nil sub nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (cauchy_posreal? const-decl "bool" cauchy nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (cauchy_sqrt const-decl "cauchy_nnreal" sqrtx nil)
    (add_lemma formula-decl nil add nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_lemma formula-decl nil sqrtx nil)
    (cauchy_nnreal? const-decl "bool" cauchy nil)
    (cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_sub const-decl "cauchy_real" sub nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq_1 formula-decl nil sq "reals/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_le formula-decl nil sq "reals/")
    (mul_lemma formula-decl nil mul nil)
    (int_lemma formula-decl nil int nil)
    (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/"))
   nil))
 (cauchy_atanh_TCC1 0
  (cauchy_atanh_TCC1-1 nil 3394199209
   ("" (skosimp)
    (("" (typepred "csx!1")
      (("" (expand "cauchy_smallreal?")
        (("" (skosimp)
          (("" (typepred "sx!1")
            ((""
              (lemma "sub_lemma"
               ("x" "1" "cx" "cauchy_int(1)" "y" "sx!1" "cy" "csx!1"))
              (("" (rewrite "int_lemma")
                (("" (assert)
                  (("" (expand "cauchy_nzreal?")
                    (("" (inst + "1-sx!1") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_smallreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_smallreal? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (cauchy_int const-decl "cauchy_real" int nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (sub_lemma formula-decl nil sub nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_lemma formula-decl nil int nil)
    (smallreal nonempty-type-eq-decl nil prelude_aux nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil))
   nil))
 (cauchy_atanh_TCC2 0
  (cauchy_atanh_TCC2-1 nil 3394199209
   ("" (skosimp)
    (("" (typepred "csx!1")
      (("" (expand "cauchy_smallreal?")
        (("" (skosimp)
          (("" (typepred "sx!1")
            ((""
              (lemma "add_lemma"
               ("x" "1" "cx" "cauchy_int(1)" "y" "sx!1" "cy" "csx!1"))
              ((""
                (lemma "sub_lemma"
                 ("x" "1" "cx" "cauchy_int(1)" "y" "sx!1" "cy"
                  "csx!1"))
                (("" (rewrite "int_lemma")
                  (("" (assert)
                    ((""
                      (lemma "div_lemma"
                       ("x" "1+sx!1" "cx"
                        "cauchy_add(cauchy_int(1), csx!1)" "nzy"
                        "1 - sx!1" "nzcy"
                        "cauchy_sub(cauchy_int(1), csx!1)"))
                      (("" (assert)
                        (("" (expand "cauchy_posreal?")
                          (("" (inst + "(1 + sx!1) / (1 - sx!1)")
                            (("" (assert)
                              ((""
                                (lemma
                                 "posreal_div_posreal_is_posreal"
                                 ("px" "1 + sx!1" "py" "1 - sx!1"))
                                (("" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_smallreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_smallreal? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (cauchy_int const-decl "cauchy_real" int nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (add_lemma formula-decl nil add nil)
    (int_lemma formula-decl nil int nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (cauchy_sub const-decl "cauchy_real" sub nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (cauchy_add const-decl "cauchy_real" add nil)
    (div_lemma formula-decl nil div nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cauchy_posreal? const-decl "bool" cauchy nil)
    (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
    (sx!1 skolem-const-decl "smallreal" hyperbolicx nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_div_nzreal_is_real application-judgement "real" reals 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)
    (sub_lemma formula-decl nil sub nil)
    (smallreal nonempty-type-eq-decl nil prelude_aux nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil))
   nil))
 (asinh_lemma 0
  (asinh_lemma-1 nil 3394201044
   ("" (skosimp)
    (("" (expand "cauchy_asinh")
      (("" (expand "asinh")
        ((""
          (lemma "mul_lemma"
           ("x" "x!1" "cx" "cx!1" "y" "x!1" "cy" "cx!1"))
          (("" (assert)
            (("" (rewrite "sq_rew")
              ((""
                (lemma "add_lemma"
                 ("x" "sq(x!1)" "cx" "cauchy_mul(cx!1, cx!1)" "y" "1"
                  "cy" "cauchy_int(1)"))
                (("" (rewrite "int_lemma")
                  (("" (assert)
                    ((""
                      (lemma "sqrt_lemma"
                       ("nnx" "1 + sq(x!1)" "nncx"
                        "cauchy_add(cauchy_mul(cx!1, cx!1), cauchy_int(1))"))
                      (("1" (assert)
                        (("1"
                          (lemma "add_lemma"
                           ("x" "x!1" "cx" "cx!1" "y"
                            "sqrt(1 + sq(x!1))" "cy"
                            "cauchy_sqrt(cauchy_add(cauchy_mul(cx!1, cx!1),
                                         cauchy_int(1)))"))
                          (("1" (assert)
                            (("1"
                              (lemma "ln_lemma"
                               ("px"
                                "sqrt(1 + sq(x!1)) + x!1"
                                "pcx"
                                "cauchy_add(cx!1,
                             cauchy_sqrt(cauchy_add
                                         (cauchy_mul(cx!1, cx!1),
                                          cauchy_int(1))))"))
                              (("1" (assert) nil nil)
                               ("2"
                                (hide-all-but 1)
                                (("2"
                                  (lemma
                                   "sqrt_lt"
                                   ("nny" "sq(x!1)" "nnz" "1+sq(x!1)"))
                                  (("2"
                                    (case "x!1>=0")
                                    (("1"
                                      (rewrite "sqrt_sq")
                                      (("1" (assert) nil nil))
                                      nil)
                                     ("2"
                                      (rewrite "sqrt_sq_neg")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (expand "cauchy_nnreal?")
                        (("2" (inst + "1+sq(x!1)") nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_asinh const-decl "[nat -> int]" hyperbolicx nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
--> --------------------

--> maximum size reached

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

[ zur Elbe Produktseite wechseln0.75Quellennavigators  Analyse erneut starten  ]