Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: Lisp

Original von: PVS^©

(nn_rational_expt
(nn_rational_expt_TCC1 0
  (nn_rational_expt_TCC1-1 nil 3427140195
   ("" (skosimp)
    (("" (case-replace "q!1=0")
      (("1" (rewrite "numerator_int") (("1" (assert) nil nil)) nil)
       ("2" (lemma "numerator_pos" ("r" "q!1"))
        (("2" (assert) nil nil)) nil))
      nil))
    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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnrat nonempty-type-eq-decl nil rationals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (numerator_int formula-decl nil rational_props_aux nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (numerator_pos formula-decl nil rational_props_aux nil)
    (rat nonempty-type-eq-decl nil rationals nil))
   nil))
(nn_rational_expt_nat_rew_TCC1 0
  (nn_rational_expt_nat_rew_TCC1-1 nil 3427171998
   ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil))
   nil))
(nn_rational_expt_nat_rew 0
  (nn_rational_expt_nat_rew-1 nil 3427172000
   ("" (skosimp)
    (("" (expand "nn_rational_expt")
      (("" (rewrite "denominator_int")
        (("" (rewrite "numerator_int")
          (("" (expand "^") (("" (rewrite "nn_root_x1") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (numerator_int formula-decl nil rational_props_aux nil)
    (expt def-decl "real" exponentiation nil)
    (nnreal type-eq-decl nil real_types nil)
    (nn_root_x1 formula-decl nil nn_root nil)
    (nnreal_expt application-judgement "nnreal" exponentiation nil)
    (^ const-decl "real" exponentiation 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)
    (denominator_int formula-decl nil rational_props_aux nil))
   shostak))
(nn_rational_expt_root_rew 0
  (nn_rational_expt_root_rew-1 nil 3427777673
   ("" (skosimp)
    (("" (expand "nn_rational_expt")
      (("" (expand "numerator")
        (("" (case-replace "denominator(1 / pn!1)=pn!1")
          (("1" (lemma "expt_x1" ("x" "x!1"))
            (("1" (expand "^")
              (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil))
            nil)
           ("2" (hide 2)
            (("2" (expand "denominator")
              (("2" (rewrite "min_def")
                (("1" (expand "minimum?")
                  (("1" (assert)
                    (("1" (rewrite "div_cancel2")
                      (("1" (assert)
                        (("1" (skosimp)
                          (("1"
                            (case "exists (i:int): i = 1 / pn!1 * x!2")
                            (("1" (skosimp)
                              (("1"
                                (typepred "x!2")
                                (("1"
                                  (lemma
                                   "div_mult_pos_le2"
                                   ("py" "pn!1" "x" "1" "z" "x!2"))
                                  (("1"
                                    (replace -1 1 rl)
                                    (("1"
                                      (lemma
                                       "posreal_div_posreal_is_posreal"
                                       ("px" "x!2" "py" "pn!1"))
                                      (("1"
                                        (case-replace "i!1=1")
                                        (("1"
                                          (replace -5 * rl)
                                          (("1" (assert) nil nil))
                                          nil)
                                         ("2"
                                          (case "i!1>=2")
                                          (("1"
                                            (replace -5 * rl)
                                            (("1" (assert) nil nil))
                                            nil)
                                           ("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (inst + "x!2/pn!1")
                              (("1" (assert) nil nil)
                               ("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (expand "nonempty?")
                    (("2" (expand "empty?")
                      (("2" (inst - "pn!1")
                        (("2" (expand "member")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil 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)
    (denominator const-decl "posnat" rational_props_aux nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (^ const-decl "real" exponentiation nil)
    (nnreal type-eq-decl nil real_types nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (minimum? const-decl "bool" min_nat nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (x!2 skolem-const-decl "posnat" nn_rational_expt nil)
    (pn!1 skolem-const-decl "posnat" nn_rational_expt nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (posreal_div_posreal_is_posreal judgement-tcc 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (min_def formula-decl nil min_nat nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numerator const-decl "int" rational_props_aux nil))
   shostak))
(nn_rational_expt_rat_rew 0
  (nn_rational_expt_rat_rew-1 nil 3427791254
   ("" (skosimp)
    (("" (expand "nn_rational_expt")
      (("" (expand "numerator")
        (("" (name "D" "denominator(n!1 / pn!1)")
          (("" (replace -1)
            (("" (typepred "x!1")
              (("" (expand ">=" -1)
                (("" (expand "<=" -1)
                  (("" (split -1)
                    (("1" (lemma "expt_pos" ("px" "x!1" "i" "n!1"))
                      (("1"
                        (lemma "expt_pos"
                         ("px" "x!1" "i" "n!1 / pn!1 * D"))
                        (("1" (expand "^" -1)
                          (("1" (assert)
                            (("1" (case "integer_pred(n!1 / pn!1 * D)")
                              (("1"
                                (lemma
                                 "nn_root_pos"
                                 ("px"
                                  "expt(x!1, n!1 / pn!1 * D)"
                                  "pn"
                                  "D"))
                                (("1"
                                  (lemma
                                   "nn_root_pos"
                                   ("px" "x!1^n!1" "pn" "pn!1"))
                                  (("1"
                                    (lemma
                                     "posreal_times_posreal_is_posreal"
                                     ("px" "pn!1" "py" "D"))
                                    (("1"
                                      (lemma
                                       "both_sides_expt2"
                                       ("px"
                                        "nn_root(expt(x!1, n!1 / pn!1 * D), D)"
                                        "py"
                                        "nn_root(x!1 ^ n!1, pn!1)"
                                        "n0i"
                                        "pn!1*D"))
                                      (("1"
                                        (replace -1 1 rl)
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (lemma
                                             "expt_times"
                                             ("n0x"
                                              "nn_root(x!1 ^ n!1, pn!1)"
                                              "i"
                                              "pn!1"
                                              "j"
                                              "D"))
                                            (("1"
                                              (rewrite
                                               "expt_nn_root"
                                               -1)
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (hide -1)
                                                  (("1"
                                                    (lemma
                                                     "expt_times"
                                                     ("n0x"
                                                      "nn_root(expt(x!1, n!1 / pn!1 * D), D)"
                                                      "i"
                                                      "D"
                                                      "j"
                                                      "pn!1"))
                                                    (("1"
                                                      (rewrite
                                                       "expt_nn_root"
                                                       -1)
                                                      (("1"
                                                        (replace -1)
                                                        (("1"
                                                          (hide -1)
                                                          (("1"
                                                            (lemma
                                                             "expt_times"
                                                             ("n0x"
                                                              "x!1"
                                                              "i"
                                                              "n!1 / pn!1 * D"
                                                              "j"
                                                              "pn!1"))
                                                            (("1"
                                                              (expand
                                                               "^"
                                                               -1
                                                               2)
                                                              (("1"
                                                                (replace
                                                                 -1
                                                                 1
                                                                 rl)
                                                                (("1"
                                                                  (hide
                                                                   -1)
                                                                  (("1"
                                                                    (lemma
                                                                     "div_cancel2"
                                                                     ("x"
                                                                      "n!1*D"
                                                                      "n0z"
                                                                      "pn!1"))
                                                                    (("1"
                                                                      (replace
                                                                       -1
                                                                       1)
                                                                      (("1"
                                                                        (hide
                                                                         -1)
                                                                        (("1"
                                                                          (rewrite
                                                                           "expt_times"
                                                                           1
                                                                           :dir
                                                                           rl)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (assert)
                                                      nil
                                                      nil)
                                                     ("3"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (propax) nil nil)
                                       ("3" (propax) nil nil)
                                       ("4" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2" (propax) nil nil))
                                nil)
                               ("2"
                                (hide -1 2)
                                (("2"
                                  (lemma
                                   "rational_def"
                                   ("r" "n!1/pn!1"))
                                  (("2"
                                    (replace -1 1 rl)
                                    (("2"
                                      (expand "D" 1)
                                      (("2"
                                        (rewrite "div_cancel2" +)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (hide 2)
                            (("2"
                              (lemma "rational_def" ("r" "n!1/pn!1"))
                              (("2"
                                (replace -1 1 rl)
                                (("2"
                                  (hide -1)
                                  (("2"
                                    (expand "D")
                                    (("2"
                                      (rewrite "div_cancel2")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert) nil nil))
                      nil)
                     ("2" (replace -1 * rl)
                      (("2" (expand "^")
                        (("2" (expand "expt")
                          (("2" (case-replace "n!1=0")
                            (("1" (assert)
                              (("1"
                                (rewrite "nn_root_1n")
                                (("1" (rewrite "nn_root_1n") nil nil))
                                nil))
                              nil)
                             ("2" (assert)
                              (("2"
                                (typepred "denominator(n!1 / pn!1)")
                                (("2"
                                  (lemma
                                   "posreal_times_posreal_is_posreal"
                                   ("px" "n!1" "py" "D"))
                                  (("2"
                                    (lemma
                                     "posreal_times_posreal_is_posreal"
                                     ("px" "n!1*D" "py" "pn!1"))
                                    (("1"
                                      (assert)
                                      (("1"
                                        (rewrite "nn_root_0n")
                                        (("1"
                                          (rewrite "nn_root_0n")
                                          nil
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (denominator const-decl "posnat" rational_props_aux 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)
    (rat nonempty-type-eq-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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nnreal type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (nn_root_0n formula-decl nil nn_root nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nn_root_1n formula-decl nil nn_root nil)
    (nat_expt application-judgement "nat" exponentiation nil)
    (expt_pos formula-decl nil exponentiation nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (^ const-decl "real" exponentiation nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (both_sides_expt2 formula-decl nil exponentiation nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (nn_root const-decl "nnreal" nn_root nil)
    (expt_nn_root formula-decl nil nn_root nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (expt_times formula-decl nil exponentiation nil)
    (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
    (expt def-decl "real" exponentiation nil)
    (nn_root_pos formula-decl nil nn_root nil)
    (rational_def formula-decl nil rational_props_aux nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (D skolem-const-decl "posnat" nn_rational_expt nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (nnreal_exp application-judgement "nnreal" exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_expt application-judgement "nnreal" exponentiation nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (numerator const-decl "int" rational_props_aux nil))
   shostak))
(nn_rational_expt_strict_increasing 0
  (nn_rational_expt_strict_increasing-1 nil 3427172121
   ("" (skosimp)
    (("" (expand "nn_rational_expt")
      (("" (typepred "x!1")
        (("" (expand ">=")
          (("" (expand "<=")
            (("" (split -1)
              (("1" (lemma "numerator_pos" ("r" "pq!1"))
                (("1" (assert)
                  (("1"
                    (lemma "both_sides_expt_pos_lt_aux"
                     ("px" "x!1" "py" "y!1" "m" "numerator(pq!1)-1"))
                    (("1" (assert)
                      (("1"
                        (lemma "nn_root_strict_increasing"
                         ("x" "expt(x!1, numerator(pq!1))" "y"
                          "expt(y!1, numerator(pq!1))" "pn"
                          "denominator(pq!1)"))
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (replace -1 * rl)
                (("2" (lemma "numerator_pos" ("r" "pq!1"))
                  (("2" (assert)
                    (("2" (expand "expt" 1 1)
                      (("2" (rewrite "zero_times1")
                        (("2" (rewrite "nn_root_0")
                          (("2"
                            (lemma "expt_pos_aux"
                             ("px" "y!1" "n" "numerator(pq!1)"))
                            (("2"
                              (lemma "nn_root_strict_increasing"
                               ("x"
                                "0"
                                "y"
                                "expt(y!1, numerator(pq!1))"
                                "pn"
                                "denominator(pq!1)"))
                              (("2"
                                (rewrite "nn_root_0")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_expt application-judgement "nnreal" exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (expt def-decl "real" exponentiation nil)
    (denominator const-decl "posnat" rational_props_aux nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (nn_root_strict_increasing formula-decl nil nn_root nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (both_sides_expt_pos_lt_aux formula-decl nil exponentiation nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numerator const-decl "int" rational_props_aux nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (numerator_pos formula-decl nil rational_props_aux nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (nonneg_rat nonempty-type-eq-decl nil rationals nil)
    (> const-decl "bool" reals nil)
    (posrat nonempty-type-eq-decl nil rationals nil)
    (expt_pos_aux formula-decl nil exponentiation nil)
    (zero_times1 formula-decl nil real_props nil)
    (nat_expt application-judgement "nat" exponentiation nil)
    (<= const-decl "bool" reals nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil))
   shostak))
(nn_rational_expt_0q 0
  (nn_rational_expt_0q-1 nil 3427224946
   ("" (skosimp)
    (("" (expand "nn_rational_expt")
      (("" (case-replace "q!1=0")
        (("1" (rewrite "numerator_int")
          (("1" (expand "expt") (("1" (rewrite "nn_root_1n") nil nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (lemma "numerator_pos" ("r" "q!1"))
            (("2" (assert)
              (("2" (expand "expt")
                (("2" (rewrite "zero_times1")
                  (("2" (rewrite "nn_root_0n") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (nat_expt application-judgement "nat" exponentiation 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (zero_times1 formula-decl nil real_props nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numerator const-decl "int" rational_props_aux nil)
    (nn_root_0n formula-decl nil nn_root nil)
    (numerator_pos formula-decl nil rational_props_aux nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (numerator_int formula-decl nil rational_props_aux nil)
    (nn_root_1n formula-decl nil nn_root nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (denominator const-decl "posnat" rational_props_aux nil)
    (expt def-decl "real" exponentiation nil)
    (nnrat nonempty-type-eq-decl nil rationals nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(nn_rational_expt_1q 0
  (nn_rational_expt_1q-1 nil 3427225011
   ("" (skosimp)
    (("" (expand "nn_rational_expt")
      (("" (lemma "expt_1i" ("i" "numerator(q!1)"))
        (("" (expand "^")
          (("" (case-replace "q!1=0")
            (("1" (rewrite "numerator_int")
              (("1" (assert)
                (("1" (replace -2)
                  (("1" (rewrite "nn_root_1n") nil nil)) nil))
                nil))
              nil)
             ("2" (lemma "numerator_pos" ("r" "q!1"))
              (("2" (assert)
                (("2" (replace -2)
                  (("2" (rewrite "nn_root_1n") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (^ const-decl "real" exponentiation nil)
    (numerator_pos formula-decl nil rational_props_aux nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (numerator_int formula-decl nil rational_props_aux nil)
    (nn_root_1n formula-decl nil nn_root nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (denominator const-decl "posnat" rational_props_aux nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (expt_1i formula-decl nil exponentiation 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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (numerator const-decl "int" rational_props_aux nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnrat nonempty-type-eq-decl nil rationals nil))
   shostak))
(nn_rational_expt_x1 0
  (nn_rational_expt_x1-1 nil 3427225202
   ("" (skosimp)
    (("" (rewrite "nn_rational_expt_nat_rew")
      (("" (rewrite "expt_x1") nil nil)) nil))
    nil)
   ((nn_rational_expt_nat_rew formula-decl nil nn_rational_expt 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (nnreal type-eq-decl nil real_types nil)
    (nnreal_exp application-judgement "nnreal" exponentiation nil)
    (expt_x1 formula-decl nil exponentiation nil))
   shostak))
(nn_rational_expt_is_0 0
  (nn_rational_expt_is_0-1 nil 3427225949
   ("" (skosimp)
    (("" (case-replace "x!1=0")
      (("1" (rewrite "nn_rational_expt_0q")
        (("1" (lift-if +) (("1" (assert) nil nil)) nil)) nil)
       ("2" (assert)
        (("2" (case-replace "q!1=0")
          (("1" (rewrite "nn_rational_expt_nat_rew")
            (("1" (rewrite "expt_x0") (("1" (assert) nil nil)) nil))
            nil)
           ("2" (expand "nn_rational_expt")
            (("2" (lemma "numerator_pos" ("r" "q!1"))
              (("2" (assert)
                (("2"
                  (lemma "expt_pos_aux"
                   ("px" "x!1" "n" "numerator(q!1)"))
                  (("2"
                    (lemma "nn_root_pos"
                     ("px" "expt(x!1, numerator(q!1))" "pn"
                      "denominator(q!1)"))
                    (("1" (assert) nil nil) ("2" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (nnrat nonempty-type-eq-decl nil rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (nn_rational_expt_0q formula-decl nil nn_rational_expt nil)
    (expt_x0 formula-decl nil exponentiation nil)
    (nnreal_exp application-judgement "nnreal" exponentiation nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (nn_rational_expt_nat_rew formula-decl nil nn_rational_expt nil)
    (numerator_pos formula-decl nil rational_props_aux nil)
    (rat nonempty-type-eq-decl nil rationals 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)
    (numerator const-decl "int" rational_props_aux nil)
    (expt_pos_aux formula-decl nil exponentiation nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (expt def-decl "real" exponentiation nil)
    (denominator const-decl "posnat" rational_props_aux nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (nn_root_pos formula-decl nil nn_root nil)
    (nnreal_expt application-judgement "nnreal" exponentiation nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nn_rational_expt const-decl "nnreal" nn_rational_expt nil))
   shostak))
(nn_rational_expt_pos 0
  (nn_rational_expt_pos-1 nil 3427226175
   ("" (skosimp)
    (("" (typepred "nn_rational_expt(px!1, q!1)")
      (("" (expand ">=")
        (("" (expand "<=")
          (("" (split)
            (("1" (assert) nil nil)
             ("2"
              (lemma "nn_rational_expt_is_0" ("x" "px!1" "q" "q!1"))
              (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (nnrat nonempty-type-eq-decl nil rationals 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)
    (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)
    (<= const-decl "bool" reals nil)
    (nn_rational_expt_is_0 formula-decl nil nn_rational_expt 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))
   shostak))
(nn_rational_expt_gt1 0
  (nn_rational_expt_gt1-1 nil 3427226319
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (case "x!1<=1")
          (("1" (assert)
            (("1" (hide 1)
              (("1" (expand "<=")
                (("1" (split -1)
                  (("1"
                    (lemma "nn_rational_expt_strict_increasing"
                     ("x" "x!1" "y" "1" "pq" "pq!1"))
                    (("1" (expand "nn_rational_expt" -1 2)
                      (("1" (lemma "expt_1i" ("i" "numerator(pq!1)"))
                        (("1" (expand "^")
                          (("1" (lemma "numerator_pos" ("r" "pq!1"))
                            (("1" (assert)
                              (("1"
                                (replace -2)
                                (("1"
                                  (rewrite "nn_root_1n")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (replace -1)
                    (("2" (hide -1)
                      (("2" (expand "nn_rational_expt")
                        (("2" (rewrite "expt_1n_aux")
                          (("1" (rewrite "nn_root_1n")
                            (("1" (assert) nil nil)) nil)
                           ("2" (lemma "numerator_pos" ("r" "pq!1"))
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil)
       ("2" (flatten)
        (("2"
          (lemma "nn_rational_expt_strict_increasing"
           ("x" "1" "y" "x!1" "pq" "pq!1"))
          (("2" (rewrite "nn_rational_expt_1q")
            (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (^ const-decl "real" exponentiation nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (denominator const-decl "posnat" rational_props_aux nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (nn_root_1n formula-decl nil nn_root nil)
    (numerator_pos formula-decl nil rational_props_aux nil)
    (numerator const-decl "int" rational_props_aux nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (expt_1i formula-decl nil exponentiation nil)
    (nn_rational_expt_strict_increasing formula-decl nil
     nn_rational_expt nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (nonneg_rat nonempty-type-eq-decl nil rationals nil)
    (> const-decl "bool" reals nil)
    (posrat nonempty-type-eq-decl nil rationals nil)
    (expt_1n_aux formula-decl nil exponentiation nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_le_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)
    (nnrat nonempty-type-eq-decl nil rationals nil)
    (nn_rational_expt_1q formula-decl nil nn_rational_expt nil))
   shostak))
(nn_rational_expt_lt1 0
  (nn_rational_expt_lt1-1 nil 3427226471
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (case "x!1>=1")
          (("1" (expand ">=" -1)
            (("1" (expand "<=" -1)
              (("1" (split -1)
                (("1" (hide 1)
                  (("1"
                    (lemma "nn_rational_expt_strict_increasing"
                     ("x" "1" "y" "x!1" "pq" "pq!1"))
                    (("1" (rewrite "nn_rational_expt_1q")
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (replace -1 * rl)
                  (("2" (rewrite "nn_rational_expt_1q") nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil)
       ("2" (flatten)
        (("2"
          (lemma "nn_rational_expt_strict_increasing"
           ("x" "x!1" "y" "1" "pq" "pq!1"))
          (("2" (rewrite "nn_rational_expt_1q")
            (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    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)
    (<= const-decl "bool" reals nil)
    (nnrat nonempty-type-eq-decl nil rationals nil)
    (nn_rational_expt_1q formula-decl nil nn_rational_expt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nn_rational_expt_strict_increasing formula-decl nil
     nn_rational_expt nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (nonneg_rat nonempty-type-eq-decl nil rationals nil)
    (> const-decl "bool" reals nil)
    (posrat nonempty-type-eq-decl nil rationals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(mult_nn_rational_expt 0
  (mult_nn_rational_expt-1 nil 3427226977
   ("" (skosimp)
    (("" (expand "nn_rational_expt")
      ((""
        (case-replace
         "expt(x!1 * y!1, numerator(q!1)) = expt(x!1, numerator(q!1))*expt(y!1, numerator(q!1))")
        (("1" (hide -1)
          (("1" (rewrite "mult_nn_root")
            (("1" (case-replace "q!1=0")
              (("1" (rewrite "numerator_int") (("1" (assert) nil nil))
                nil)
               ("2" (lemma "numerator_pos" ("r" "q!1"))
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (case-replace "q!1=0")
            (("1" (rewrite "numerator_int")
              (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)
             ("2" (lemma "numerator_pos" ("r" "q!1"))
              (("2" (assert) (("2" (rewrite "expt_of_mult") nil nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (hide 2)
          (("3" (case-replace "q!1=0")
            (("1" (rewrite "numerator_int") (("1" (assert) nil nil))
              nil)
             ("2" (lemma "numerator_pos" ("r" "q!1"))
              (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (expt_of_mult formula-decl nil exponentiation nil)
    (numerator_int formula-decl nil rational_props_aux nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (numerator_pos formula-decl nil rational_props_aux nil)
    (mult_nn_root formula-decl nil nn_root nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (denominator const-decl "posnat" rational_props_aux nil)
    (nnrat nonempty-type-eq-decl nil rationals nil)
    (numerator const-decl "int" rational_props_aux nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (nnreal type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (expt def-decl "real" exponentiation 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nnreal_expt application-judgement "nnreal" exponentiation nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(inv_nn_rational_expt_TCC1 0
  (inv_nn_rational_expt_TCC1-1 nil 3427225923
   ("" (skosimp) (("" (rewrite "nn_rational_expt_is_0") nil nil)) nil)
   ((nn_rational_expt_is_0 formula-decl nil nn_rational_expt 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnrat nonempty-type-eq-decl nil rationals nil)
    (nnreal type-eq-decl nil real_types 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))
   nil))
(inv_nn_rational_expt 0
  (inv_nn_rational_expt-1 nil 3427227319
   ("" (skosimp)
    (("" (expand "nn_rational_expt")
      (("" (case-replace "q!1=0")
        (("1" (rewrite "numerator_int")
          (("1" (rewrite "denominator_int")
            (("1" (rewrite "nn_root_x1")
              (("1" (rewrite "nn_root_x1")
                (("1" (rewrite "expt_of_inv") nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (lemma "numerator_pos" ("r" "q!1"))
          (("2" (assert)
            (("2"
              (lemma "expt_of_inv" ("n0x" "px!1" "n" "numerator(q!1)"))
              (("2" (replace -1)
                (("2" (hide -1) (("2" (rewrite "inv_nn_root") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_rational_expt const-decl "nnreal" nn_rational_expt nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (numerator_pos formula-decl nil rational_props_aux nil)
    (numerator const-decl "int" rational_props_aux nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (inv_nn_root formula-decl nil nn_root nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (denominator const-decl "posnat" rational_props_aux 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)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (numerator_int formula-decl nil rational_props_aux nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nzreal_expt application-judgement "nzreal" exponentiation nil)
    (posreal_expt application-judgement "posreal" exponentiation nil)
    (nn_root_x1 formula-decl nil nn_root nil)
    (nnreal type-eq-decl nil real_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (expt def-decl "real" exponentiation nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields 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)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (expt_of_inv formula-decl nil exponentiation nil)
    (denominator_int formula-decl nil rational_props_aux nil)
    (nnrat nonempty-type-eq-decl nil rationals nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(div_nn_rational_expt 0
  (div_nn_rational_expt-1 nil 3427227529
   ("" (skosimp)
    (("" (lemma "inv_nn_rational_expt" ("px" "py!1" "q" "q!1"))
      ((""
        (lemma "mult_nn_rational_expt"
         ("x" "x!1" "y" "1/py!1" "q" "q!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((nnrat nonempty-type-eq-decl nil rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (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)
    (inv_nn_rational_expt formula-decl nil nn_rational_expt nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (mult_nn_rational_expt formula-decl nil nn_rational_expt nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil))
   shostak))
(nn_rational_expt_plus 0
  (nn_rational_expt_plus-1 nil 3427261250
   (""
    (case "FORALL (q, r: nnrat, px: posreal):
        nn_rational_expt(px, q + r) = nn_rational_expt(px, q) * nn_rational_expt(px, r)")
    (("1" (skosimp)
      (("1" (case-replace "x!1=0")
        (("1" (rewrite "nn_rational_expt_0q")
          (("1" (rewrite "nn_rational_expt_0q")
            (("1" (rewrite "nn_rational_expt_0q")
              (("1" (hide -1 -2) (("1" (grind) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (inst - "q!1" "r!1" "x!1") (("2" (assert) nil nil)) nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp)
        (("2" (case-replace "q!1=0")
          (("1" (lemma "nn_rational_expt_nat_rew" ("x" "px!1" "n" "0"))
            (("1" (rewrite "expt_x0") (("1" (assert) nil nil)) nil))
            nil)
           ("2" (case-replace "r!1=0")
            (("1"
              (lemma "nn_rational_expt_nat_rew" ("x" "px!1" "n" "0"))
              (("1" (rewrite "expt_x0") (("1" (assert) nil nil)) nil))
              nil)
             ("2" (case "r!1>0")
              (("1" (case "q!1>0")
                (("1" (hide 1 2)
                  (("1" (lemma "numerator_pos" ("r" "r!1"))
                    (("1" (lemma "numerator_pos" ("r" "q!1"))
                      (("1" (lemma "numerator_pos" ("r" "q!1+r!1"))
                        (("1" (assert)
                          (("1"
                            (case "forall (i:nat,pm,pn:posnat): nn_root(expt(px!1,pm*i), pm*pn)=nn_root(expt(px!1,i), pn)")
                            (("1" (expand "nn_rational_expt")
                              (("1"
                                (inst-cp
                                 -
                                 "numerator(q!1 + r!1)"
                                 "denominator(q!1)*denominator(r!1)"
                                 "denominator(q!1 + r!1)")
                                (("1"
                                  (replace -2 * rl)
                                  (("1"
                                    (inst-cp
                                     -
                                     "numerator(q!1)"
                                     "denominator(r!1) *
                denominator(q!1 + r!1)"
                                     "denominator(q!1)")
                                    (("1"
                                      (replace -2 1 rl)
                                      (("1"
                                        (inst
                                         -
                                         "numerator(r!1)"
                                         "denominator(q!1) *
                denominator(q!1 + r!1)"
                                         "denominator(r!1)")
                                        (("1"
                                          (replace -1 1 rl)
                                          (("1"
                                            (hide -1 -2 -3)
                                            (("1"
                                              (lemma
                                               "posreal_times_posreal_is_posreal"
                                               ("px"
                                                "denominator(q!1)"
                                                "py"
                                                "denominator(r!1)"))
                                              (("1"
                                                (lemma
                                                 "posreal_times_posreal_is_posreal"
                                                 ("px"
                                                  "denominator(q!1)*denominator(r!1)"
                                                  "py"
                                                  "denominator(q!1+r!1)"))
                                                (("1"
                                                  (name-replace
                                                   "PN"
                                                   "denominator(q!1) * denominator(r!1) * denominator(q!1 + r!1)")
                                                  (("1"
                                                    (rewrite
                                                     "mult_nn_root"
                                                     +
                                                     :dir
                                                     rl)
                                                    (("1"
                                                      (rewrite
                                                       "expt_plus_aux"
                                                       +
                                                       :dir
                                                       rl)
                                                      (("1"
                                                        (case-replace
                                                         "denominator(q!1 + r!1) * denominator(q!1) *
                      numerator(r!1)
                      +
                      denominator(q!1 + r!1) * denominator(r!1) *
                       numerator(q!1)=denominator(q!1) * denominator(r!1) *
                     numerator(q!1 + r!1)")
                                                        (("1"
                                                          (hide 2 -1)
                                                          (("1"
                                                            (lemma
                                                             "both_sides_times1"
                                                             ("n0z"
                                                              "denominator(q!1 + r!1)"
                                                              "x"
                                                              "denominator(q!1) * numerator(r!1) +denominator(r!1) * numerator(q!1)"
                                                              "y"
                                                              "denominator(q!1) * denominator(r!1)*(q!1+r!1)"))
                                                            (("1"
                                                              (lemma
                                                               "rational_def"
                                                               ("r"
                                                                "q!1 + r!1"))
                                                              (("1"
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.141 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.