products/Sources/formale Sprachen/Coq/dev/ci/nix/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: fun_below_props.prf   Sprache: Unknown

(fun_below_props
 (cartesian_bijection 0
  (cartesian_bijection-1 nil 3308405027
   ("" (skolem!)
    (("" (case "m!1 = 0")
      (("1" (inst + "LAMBDA (x: [below[n!1], below[m!1]]): 0")
        (("1" (grind :if-match nil)
          (("1" (typepred "x1!1`2") (("1" (assert) nil nil)) nil)) nil)
         ("2" (skolem!)
          (("2" (typepred "x!1`2") (("2" (assert) nil nil)) nil)) nil))
        nil)
       ("2"
        (inst +
         "LAMBDA (x: [below[n!1], below[m!1]]): m!1 * x`1 + x`2")
        (("1" (grind :if-match nil)
          (("1" (inst + "(ndiv(y!1, m!1), rem(m!1)(y!1))")
            (("1" (assert) nil nil)
             ("2" (assert)
              (("2" (typepred "ndiv(y!1, m!1)")
                (("2" (case "ndiv(y!1, m!1) <= y!1 / m!1")
                  (("1" (hide -2 -3)
                    (("1"
                      (lemma "both_sides_div_pos_lt1"
                       ("pz" "m!1" "x" "y!1" "y" "n!1 * m!1"))
                      (("1" (assert) nil nil)) nil))
                    nil)
                   ("2" (use "ndiv_lt") nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (forward-chain "unique_division")
            (("2" (apply-extensionality 2) nil nil)) nil))
          nil)
         ("2" (skolem!)
          (("2" (assert)
            (("2"
              (lemma "both_sides_times_pos_le1"
               ("x" "x!1`1" "y" "n!1 - 1" "pz" "m!1"))
              (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (bijective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (n!1 skolem-const-decl "nat" fun_below_props nil)
    (below type-eq-decl nil nat_types nil)
    (m!1 skolem-const-decl "nat" fun_below_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (both_sides_div_pos_lt1 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ndiv_lt formula-decl nil modulo_arithmetic nil)
    (<= const-decl "bool" reals nil)
    (y!1 skolem-const-decl "below[n!1 * m!1]" fun_below_props nil)
    (ndiv const-decl "{q: int | x = b * q + rem(b)(x)}"
     modulo_arithmetic nil)
    (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}"
         modulo_arithmetic nil)
    (mod nonempty-type-eq-decl nil euclidean_division nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (nil application-judgement "upto(n)" modulo_arithmetic nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (unique_division formula-decl nil euclidean_division nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil))
   shostak))
 (empty_domain1 0
  (empty_domain1-1 nil 3308405352
   ("" (skolem!)
    (("" (inst + "LAMBDA (x: below[0]): 0")
      (("" (skolem-typepred) nil nil)) nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (FALSE const-decl "bool" booleans nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (m!1 skolem-const-decl "nat" fun_below_props nil))
   shostak))
 (empty_domain2 0
  (empty_domain2-1 nil 3308405370
   ("" (skolem!) (("" (apply-extensionality) nil nil)) nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (FALSE const-decl "bool" booleans nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil))
   shostak))
 (empty_range 0
  (empty_range-1 nil 3308405383
   ("" (skosimp*)
    (("" (typepred "f!1(0)") (("" (assert) nil nil)) nil)) nil)
   ((below type-eq-decl nil nat_types 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)
    (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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (funset_bijection_TCC1 0
  (funset_bijection_TCC1-1 nil 3308404994 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (funset_bijection 0
  (funset_bijection-1 nil 3308405401
   ("" (induct "n")
    (("1" (skolem!)
      (("1" (inst + "LAMBDA (x: [below[0] -> below[m!1]]): 0")
        (("1" (grind)
          (("1" (rewrite "empty_domain1") nil nil)
           ("2" (rewrite "empty_domain2") nil nil))
          nil)
         ("2" (grind) nil nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (case "m!1 = 0")
        (("1" (delete -2)
          (("1" (assert)
            (("1" (lemma "empty_range" ("m" "m!1" "p" "1 + j!1"))
              (("1" (assert)
                (("1"
                  (inst +
                   "LAMBDA (h: [below[1 + j!1] -> below[m!1]]): 0")
                  (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (inst - "m!1")
            (("2" (skolem!)
              (("2"
                (inst +
                 "LAMBDA (h: [below[1 + j!1] -> below[m!1]]): m!1 * f!1(LAMBDA (x: below[j!1]): h(x)) + h(j!1)")
                (("1" (expand "bijective?")
                  (("1" (prop)
                    (("1" (delete -2)
                      (("1" (expand "injective?")
                        (("1" (skosimp)
                          (("1"
                            (name-replace "h1"
                             "LAMBDA (x: below[j!1]): x1!1(x)" :hide?
                             nil)
                            (("1"
                              (name-replace "h2"
                               "LAMBDA (x: below[j!1]): x2!1(x)" :hide?
                               nil)
                              (("1"
                                (lemma
                                 "unique_division"
                                 ("b"
                                  "m!1"
                                  "q1"
                                  "f!1(h1)"
                                  "q2"
                                  "f!1(h2)"
                                  "r1"
                                  "x1!1(j!1)"
                                  "r2"
                                  "x2!1(j!1)"))
                                (("1"
                                  (smash)
                                  (("1"
                                    (inst - "h1" "h2")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (apply-extensionality :hide? t)
                                        (("1"
                                          (case "h1(x!1) = h2(x!1)")
                                          (("1"
                                            (replace -4 -1 rl)
                                            (("1"
                                              (replace -5 -1 rl)
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil)
                                           ("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (delete -1)
                      (("2" (expand "surjective?")
                        (("2" (skolem!)
                          (("2" (inst - "ndiv(y!1, m!1)")
                            (("1" (skolem!)
                              (("1"
                                (inst
                                 +
                                 "LAMBDA (x: below[1 + j!1]): IF x = j!1 THEN rem(m!1)(y!1) ELSE x!1(x) ENDIF")
                                (("1"
                                  (assert)
                                  (("1"
                                    (replace-eta "x!1")
                                    (("1"
                                      (typepred "ndiv(y!1, m!1)")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skosimp)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2)
                              (("2"
                                (typepred "y!1")
                                (("2"
                                  (expand "^")
                                  (("2"
                                    (expand "expt" -)
                                    (("2"
                                      (use "ndiv_lt")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (lemma
                                           "both_sides_div_pos_lt1"
                                           ("pz"
                                            "m!1"
                                            "x"
                                            "y!1"
                                            "y"
                                            "m!1 * expt(m!1, j!1)"))
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skolem!)
                  (("2" (assert)
                    (("2"
                      (name-replace "u"
                       "f!1(LAMBDA (x: below[j!1]): h!1(x))")
                      (("2" (typepred "u")
                        (("2" (auto-rewrite "expt_plus" "expt_x1")
                          (("2" (assert)
                            (("2" (name-replace "v" "m!1 ^ j!1")
                              (("2"
                                (lemma
                                 "both_sides_times_pos_le2"
                                 ("x" "u" "y" "v - 1" "pz" "m!1"))
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (both_sides_times_pos_le2 formula-decl nil real_props nil)
    (expt_plus formula-decl nil exponentiation nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (ndiv_lt formula-decl nil modulo_arithmetic nil)
    (both_sides_div_pos_lt1 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)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (<= const-decl "bool" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (y!1 skolem-const-decl "below[m!1 ^ (1 + j!1)]" fun_below_props
     nil)
    (ndiv const-decl "{q: int | x = b * q + rem(b)(x)}"
     modulo_arithmetic nil)
    (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}"
         modulo_arithmetic nil)
    (nil application-judgement "upto(n)" modulo_arithmetic nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mod nonempty-type-eq-decl nil euclidean_division nil)
    (unique_division formula-decl nil euclidean_division nil)
    (f!1 skolem-const-decl
     "[[below[j!1] -> below[m!1]] -> below[m!1 ^ j!1]]" fun_below_props
     nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (empty_range formula-decl nil fun_below_props nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (j!1 skolem-const-decl "nat" fun_below_props nil)
    (m!1 skolem-const-decl "nat" fun_below_props 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (expt def-decl "real" exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nat_expt application-judgement "nat" exponentiation nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (empty_domain1 formula-decl nil fun_below_props nil)
    (empty_domain2 formula-decl nil fun_below_props nil)
    (m!1 skolem-const-decl "nat" fun_below_props nil)
    (FALSE const-decl "bool" booleans nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (bijective? const-decl "bool" functions nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (pred type-eq-decl nil defined_types 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)
    (nat_exp application-judgement "nat" exponentiation nil))
   shostak)))

[ Dauer der Verarbeitung: 0.5 Sekunden  (vorverarbeitet)  ]