Quelle root.prf Sprache: Lisp

(root
(root_0n 0
  (root_0n-1 nil 3427758277
   ("" (skosimp)
    (("" (expand "root")
      (("" (expand "sign")
        (("" (expand "abs") (("" (rewrite "nn_root_0n") nil nil)) nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (nn_root_0n formula-decl nil nn_root nil)
    (sign const-decl "Sign" sign "reals/"))
   shostak))
(root_1n 0
  (root_1n-1 nil 3427758449
   ("" (skosimp)
    (("" (expand "root")
      (("" (expand "sign")
        (("" (expand "abs")
          (("" (assert) (("" (rewrite "nn_root_1n") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nn_root_1n formula-decl nil nn_root 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (sign const-decl "Sign" sign "reals/"))
   shostak))
(root_x1 0
  (root_x1-1 nil 3427758482
   ("" (skosimp)
    (("" (expand "root")
      (("" (expand "sign")
        (("" (expand "abs")
          (("" (case-replace "x!1=0")
            (("1" (assert) (("1" (rewrite "nn_root_0n") nil nil)) nil)
             ("2" (case "x!1<0")
              (("1" (assert)
                (("1" (rewrite "nn_root_x1") (("1" (assert) nil nil))
                  nil))
                nil)
               ("2" (assert) (("2" (rewrite "nn_root_x1") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (< const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (nn_root_x1 formula-decl nil nn_root nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (nn_root_0n formula-decl nil nn_root nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (sign const-decl "Sign" sign "reals/"))
   shostak))
(root_nn_root_rew_TCC1 0
  (root_nn_root_rew_TCC1-1 nil 3427764460 ("" (subtype-tcc) nil nil)
   ((even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (odd? const-decl "bool" integers nil))
   nil))
(root_nn_root_rew 0
  (root_nn_root_rew-1 nil 3427764461
   ("" (skosimp)
    (("" (expand "root")
      (("" (expand "abs")
        (("" (case-replace "nx!1=0")
          (("1" (rewrite "nn_root_0n") (("1" (assert) nil nil)) nil)
           ("2" (expand "sign") (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nnreal type-eq-decl nil real_types nil)
    (sign_nat formula-decl nil sign "reals/")
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (nn_root_0n formula-decl nil nn_root nil)
    (sign const-decl "Sign" sign "reals/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   shostak))
(root_expt_TCC1 0
  (root_expt_TCC1-1 nil 3427758158
   ("" (skosimp) (("" (assert) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(root_expt_TCC2 0
  (root_expt_TCC2-1 nil 3427758158
   ("" (skosimp)
    (("" (typepred "pn!1")
      (("" (split -2)
        (("1" (expand ">=")
          (("1" (expand "<=")
            (("1" (flatten)
              (("1" (split)
                (("1" (lemma "expt_pos" ("px" "x!1" "i" "pn!1"))
                  (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
                 ("2" (replace -1 * rl)
                  (("2" (expand "^")
                    (("2" (expand "expt") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (propax) nil nil))
        nil))
      nil))
    nil)
   ((odd? const-decl "bool" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (> 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)
    (expt def-decl "real" exponentiation nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (nat_expt application-judgement "nat" exponentiation nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (^ const-decl "real" exponentiation nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (expt_pos formula-decl nil exponentiation 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (<= const-decl "bool" reals nil))
   nil))
(root_expt 0
  (root_expt-1 nil 3427759297
   ("" (skosimp)
    (("" (expand "root")
      (("" (rewrite "abs_hat_nat" 1 :dir rl)
        (("" (rewrite "nn_root_expt")
          (("" (expand "sign")
            (("" (expand "abs")
              (("" (case-replace "x!1<0")
                (("1" (typepred "pn!1")
                  (("1" (assert)
                    (("1" (expand "odd?")
                      (("1" (skosimp)
                        (("1" (replace -2)
                          (("1" (rewrite "expt_plus")
                            (("1" (rewrite "expt_x1")
                              (("1"
                                (rewrite "expt_times")
                                (("1"
                                  (rewrite "expt_x2")
                                  (("1"
                                    (lemma
                                     "negreal_times_negreal_is_posreal"
                                     ("nx" "x!1" "ny" "x!1"))
                                    (("1"
                                      (lemma
                                       "expt_pos"
                                       ("px" "x!1*x!1" "i" "j!1"))
                                      (("1"
                                        (lemma
                                         "both_sides_times_pos_lt1"
                                         ("pz"
                                          "(x!1 * x!1) ^ j!1"
                                          "x"
                                          "x!1"
                                          "y"
                                          "0"))
                                        (("1" (assert) nil nil)
                                         ("2" (assert) nil nil))
                                        nil)
                                       ("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (replace 1)
                  (("2" (case-replace "x!1=0")
                    (("1" (assert)
                      (("1" (expand "^")
                        (("1" (expand "expt") (("1" (propax) nil nil))
                          nil))
                        nil))
                      nil)
                     ("2" (lemma "expt_pos" ("px" "x!1" "i" "pn!1"))
                      (("1" (assert) nil nil) ("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (nn_root_expt formula-decl nil nn_root nil)
    (nnreal type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nat_exp application-judgement "nat" exponentiation nil)
    (nat_expt application-judgement "nat" exponentiation nil)
    (expt def-decl "real" exponentiation nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (expt_x2 formula-decl nil exponentiation nil)
    (expt_pos formula-decl nil exponentiation nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (^ const-decl "real" exponentiation nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil)
    (expt_times formula-decl nil exponentiation nil)
    (expt_plus formula-decl nil exponentiation nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (< const-decl "bool" reals nil)
    (sign const-decl "Sign" sign "reals/")
    (nnreal_exp application-judgement "nnreal" exponentiation nil)
    (odd? const-decl "bool" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (abs_hat_nat formula-decl nil exponentiation nil))
   shostak))
(expt_root_TCC1 0
  (expt_root_TCC1-1 nil 3427758158
   ("" (skosimp) (("" (assert) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(expt_root 0
  (expt_root-1 nil 3427759817
   ("" (skosimp)
    (("" (expand "root")
      (("" (case-replace "x!1=0")
        (("1" (expand "sign")
          (("1" (expand "^")
            (("1" (expand "expt")
              (("1" (assert)
                (("1" (expand "abs")
                  (("1" (rewrite "nn_root_0n") (("1" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (case "x!1>0")
          (("1" (expand "abs")
            (("1" (expand "sign")
              (("1" (assert) (("1" (rewrite "expt_nn_root") nil nil))
                nil))
              nil))
            nil)
           ("2" (expand "sign")
            (("2" (expand "abs")
              (("2" (assert)
                (("2" (typepred "pn!1")
                  (("2" (split -2)
                    (("1" (assert) nil nil)
                     ("2" (expand "odd?")
                      (("2" (skosimp)
                        (("2" (replace -1)
                          (("2"
                            (lemma "nn_root_pos"
                             ("px" "-x!1" "pn" "1+2*j!1"))
                            (("1" (rewrite "mult_expt")
                              (("1"
                                (rewrite "expt_nn_root")
                                (("1"
                                  (rewrite "expt_plus")
                                  (("1"
                                    (rewrite "expt_times")
                                    (("1"
                                      (rewrite "expt_x1")
                                      (("1"
                                        (rewrite "expt_x2")
                                        (("1"
                                          (rewrite "expt_1i")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (expt_nn_root formula-decl nil nn_root nil)
    (nnreal type-eq-decl nil real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nn_root const-decl "nnreal" nn_root nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (mult_expt formula-decl nil exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (rat_exp application-judgement "rat" exponentiation nil)
    (nnreal_exp application-judgement "nnreal" exponentiation nil)
    (expt_plus formula-decl nil exponentiation nil)
    (int_exp application-judgement "int" exponentiation nil)
    (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (expt_1i formula-decl nil exponentiation nil)
    (odd_times_odd_is_odd application-judgement "odd_int" integers nil)
    (expt_x2 formula-decl nil exponentiation nil)
    (expt_times formula-decl nil exponentiation nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_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)
    (nn_root_pos formula-decl nil nn_root nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sign const-decl "Sign" sign "reals/")
    (expt def-decl "real" exponentiation nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nat_expt application-judgement "nat" exponentiation nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (odd? const-decl "bool" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (nn_root_0n formula-decl nil nn_root nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (nnreal_expt application-judgement "nnreal" exponentiation nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (^ const-decl "real" exponentiation nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(root_is_0 0
  (root_is_0-1 nil 3427760275
   ("" (skosimp)
    (("" (expand "root")
      (("" (rewrite "zero_times3")
        (("" (rewrite "nn_root_is_0") (("" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (nn_root_is_0 formula-decl nil nn_root nil)
    (minus_even_is_even application-judgement "even_int" integers 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sign const-decl "Sign" sign "reals/")
    (Sign type-eq-decl nil sign "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (odd? const-decl "bool" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nn_root const-decl "nnreal" nn_root nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (zero_times3 formula-decl nil real_props nil))
   shostak))
(root_pos 0
  (root_pos-1 nil 3427760361
   ("" (skosimp)
    (("" (expand "root")
      (("" (typepred "nn_root(abs(x!1), pn!1)")
        (("" (split)
          (("1" (flatten)
            (("1" (expand "sign")
              (("1" (assert)
                (("1" (case-replace "x!1=0")
                  (("1" (assert)
                    (("1" (expand "abs")
                      (("1" (rewrite "nn_root_0n") nil nil)) nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (flatten)
            (("2" (expand "sign")
              (("2" (assert) (("2" (rewrite "nn_root_pos") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (sign const-decl "Sign" sign "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nn_root_0n formula-decl nil nn_root nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nn_root_pos formula-decl nil nn_root 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)
    (nnreal type-eq-decl nil real_types nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nn_root const-decl "nnreal" nn_root nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (odd? const-decl "bool" integers nil))
   shostak))
(root_neg 0
  (root_neg-1 nil 3427760534
   ("" (skosimp)
    (("" (expand "root")
      (("" (lemma "trich_lt" ("x" "x!1" "y" "0"))
        (("" (split -1)
          (("1" (expand "sign")
            (("1" (expand "abs")
              (("1" (assert)
                (("1" (lemma "nn_root_pos" ("px" "-x!1" "pn" "pn!1"))
                  (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (expand "abs")
            (("2" (expand "sign")
              (("2" (assert)
                (("2" (replace -1)
                  (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (expand "sign")
            (("3" (expand "abs")
              (("3" (assert)
                (("3" (typepred "nn_root(x!1, pn!1)")
                  (("3" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (odd? const-decl "bool" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (nn_root_pos formula-decl nil nn_root nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sign const-decl "Sign" sign "reals/")
    (nn_root_0n formula-decl nil nn_root nil)
    (nn_root const-decl "nnreal" nn_root nil)
    (nnreal type-eq-decl nil real_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (trich_lt formula-decl nil real_props 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))
   shostak))
(root_gt1 0
  (root_gt1-1 nil 3427760682
   ("" (skosimp)
    (("" (expand "root")
      (("" (lemma "trich_lt" ("x" "x!1" "y" "0"))
        (("" (split)
          (("1" (expand "sign")
            (("1" (expand "abs")
              (("1" (assert)
                (("1" (typepred "nn_root(-x!1, pn!1)")
                  (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (replace -1)
            (("2" (expand "abs")
              (("2" (expand "sign")
                (("2" (assert)
                  (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (expand "sign")
            (("3" (assert)
              (("3" (rewrite "nn_root_gt1")
                (("3" (expand "abs") (("3" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" root nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (odd? const-decl "bool" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nn_root const-decl "nnreal" nn_root nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sign const-decl "Sign" sign "reals/")
    (nn_root_0n formula-decl nil nn_root nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nn_root_gt1 formula-decl nil nn_root nil)
    (trich_lt formula-decl nil real_props 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))
   shostak))
(root_lt1 0
  (root_lt1-1 nil 3427763570
   ("" (skosimp)
    (("" (typepred "pn!1")
      (("" (case-replace "x!1>=0")
        (("1" (expand "root")
          (("1" (expand ">=")
            (("1" (expand "<=")
              (("1" (split -1)
                (("1" (expand "sign")
                  (("1" (assert)
                    (("1" (rewrite "nn_root_lt1")
                      (("1" (expand "abs") (("1" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "sign")
                  (("2" (expand "abs")
                    (("2" (assert)
                      (("2" (replace -1 * rl)
                        (("2" (rewrite "nn_root_0n")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (replace 1 -2)
          (("2" (expand "root")
            (("2" (expand "sign")
              (("2" (expand "abs")
                (("2" (assert)
                  (("2" (lemma "nn_root_pos" ("px" "-x!1" "pn" "pn!1"))
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((odd? const-decl "bool" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (> 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nn_root_pos formula-decl nil nn_root nil)
    (root const-decl "real" root nil) (<= const-decl "bool" reals nil)
    (nn_root_0n formula-decl nil nn_root nil)
    (sign const-decl "Sign" sign "reals/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (nn_root_lt1 formula-decl nil nn_root 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(neg_root_TCC1 0
  (neg_root_TCC1-1 nil 3427775104 ("" (subtype-tcc) nil 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (odd? const-decl "bool" integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil))
(neg_root_TCC2 0
  (neg_root_TCC2-1 nil 3427775104 ("" (subtype-tcc) nil 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (odd? const-decl "bool" integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil))
(neg_root 0
  (neg_root-1 nil 3427775105
   ("" (skosimp)
    (("" (expand "root")
      (("" (lemma "trich_lt" ("x" "x!1" "y" "0"))
        (("" (expand "abs")
          (("" (expand "sign")
            (("" (split)
              (("1" (assert) nil nil)
               ("2" (assert)
                (("2" (replace -1)
                  (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("3" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (root const-decl "real" root nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (nn_root_0n formula-decl nil nn_root nil)
    (sign const-decl "Sign" sign "reals/")
    (trich_lt formula-decl nil real_props 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))
   shostak))
(mult_root_TCC1 0
  (mult_root_TCC1-1 nil 3427758158
   ("" (skosimp)
    (("" (typepred "pn!1")
      (("" (assert)
        (("" (flatten)
          ((""
            (lemma "le_times_le_pos"
             ("nnx" "0" "y" "x!1" "nnz" "0" "w" "y!1"))
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((odd? const-decl "bool" integers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (> 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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (le_times_le_pos formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(mult_root_TCC2 0
  (mult_root_TCC2-1 nil 3427759296
   ("" (skosimp) (("" (typepred "pn!1") (("" (assert) nil nil)) nil))
    nil)
   ((odd? const-decl "bool" integers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (> 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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(mult_root_TCC3 0
  (mult_root_TCC3-1 nil 3427760995 ("" (subtype-tcc) nil 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (odd? const-decl "bool" integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil))
(mult_root 0
  (mult_root-1 nil 3427762524
   ("" (skosimp)
    (("" (expand "root")
      (("" (expand "sign")
        (("" (expand "abs")
          (("" (lemma "trichotomy" ("x" "x!1"))
            (("" (split -1)
              (("1" (lemma "trichotomy" ("x" "y!1"))
                (("1" (split)
                  (("1"
                    (lemma "posreal_times_posreal_is_posreal"
                     ("px" "x!1" "py" "y!1"))
                    (("1" (assert)
                      (("1" (rewrite "mult_nn_root") nil nil)) nil)
                     ("2" (assert) nil nil) ("3" (assert) nil nil))
                    nil)
                   ("2" (replace -1)
                    (("2" (assert)
                      (("2" (rewrite "nn_root_0n")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil)
                   ("3" (assert)
                    (("3"
                      (lemma "both_sides_times_pos_lt1"
                       ("pz" "x!1" "x" "y!1" "y" "0"))
                      (("3" (assert)
                        (("3"
                          (lemma "mult_nn_root"
                           ("x" "-y!1" "y" "x!1" "pn" "pn!1"))
                          (("3" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (replace -1)
                (("2" (assert)
                  (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("3" (lemma "trichotomy" ("x" "y!1"))
                (("3" (split)
                  (("1"
                    (lemma "both_sides_times_pos_lt1"
                     ("pz" "y!1" "x" "x!1" "y" "0"))
                    (("1" (assert)
                      (("1"
                        (lemma "mult_nn_root"
                         ("x" "-x!1" "y" "y!1" "pn" "pn!1"))
                        (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (assert) nil nil))
                    nil)
                   ("2" (assert)
                    (("2" (replace -1)
                      (("2" (rewrite "nn_root_0n")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil)
                   ("3"
                    (lemma "negreal_times_negreal_is_posreal"
                     ("nx" "x!1" "ny" "y!1"))
                    (("1" (assert)
                      (("1" (rewrite "mult_nn_root" + :dir rl)
                        (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (assert) nil nil) ("3" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (root const-decl "real" root nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types 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)
    (mult_nn_root formula-decl nil nn_root nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (odd? const-decl "bool" integers nil)
    (nnreal type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (nn_root_0n formula-decl nil nn_root nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil)
    (<= const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (trichotomy formula-decl nil real_axioms 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)
    (sign const-decl "Sign" sign "reals/"))
   shostak))
(inv_root_TCC1 0
  (inv_root_TCC1-1 nil 3427758158
   ("" (skosimp)
    (("" (typepred "pn!1")
      (("" (replace 2 -2)
        ((""
          (lemma "posreal_div_posreal_is_posreal"
           ("px" "1" "py" "n0x!1"))
          (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((odd? const-decl "bool" integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (> 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)
    (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil))
   nil))
(inv_root_TCC2 0
  (inv_root_TCC2-1 nil 3427758158
   ("" (skosimp) (("" (rewrite "root_is_0") nil nil)) nil)
   ((root_is_0 formula-decl nil root nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (odd? const-decl "bool" integers nil))
   nil))
(inv_root 0
  (inv_root-1 nil 3427764733
   ("" (skosimp)
    (("" (expand "root")
      (("" (rewrite "abs_div")
        (("" (expand "abs" 1 1)
          (("" (case-replace "sign(1 / n0x!1) =sign(n0x!1)")
            (("1" (rewrite "inv_nn_root")
              (("1" (assert)
                (("1" (hide -1)
                  (("1" (expand "sign")
                    (("1" (case-replace "n0x!1 > 0")
                      (("1" (assert) nil nil) ("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (lemma "trichotomy" ("x" "n0x!1"))
                (("2" (split -1)
                  (("1" (expand "sign")
                    (("1"
                      (lemma "posreal_div_posreal_is_posreal"
                       ("px" "1" "py" "n0x!1"))
                      (("1" (assert) nil nil) ("2" (assert) nil nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil)
                   ("3" (expand "sign")
                    (("3" (rewrite "div_mult_neg_ge1" +)
                      (("3" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (root const-decl "real" root nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (div_mult_neg_ge1 formula-decl nil real_props nil)
    (trichotomy formula-decl nil real_axioms nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (odd? const-decl "bool" integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (inv_nn_root formula-decl nil nn_root nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (sign const-decl "Sign" sign "reals/")
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzint nonempty-type-eq-decl nil integers 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
     real_defs nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
     real_defs nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (abs_div formula-decl nil real_props nil))
   shostak))
(div_root_TCC1 0
  (div_root_TCC1-1 nil 3427758158
   ("" (skosimp)
    (("" (typepred "pn!1")
      (("" (replace 2 -2)
        (("" (flatten)
          ((""
            (lemma "both_sides_div_pos_ge1"
             ("pz" "n0y!1" "x" "x!1" "y" "0"))
            (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((odd? const-decl "bool" integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (> 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_div_nzreal_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (both_sides_div_pos_ge1 formula-decl nil real_props nil))
   nil))
(div_root_TCC2 0
  (div_root_TCC2-1 nil 3427761736 ("" (subtype-tcc) nil 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 "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (odd? const-decl "bool" integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil))
(div_root_TCC3 0
  (div_root_TCC3-1 nil 3427761736 ("" (subtype-tcc) nil 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 "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
--> --------------------

--> maximum size reached

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

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.