Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: finite_bags_aux.prf Sprache: Lisp

Original von: PVS^©

(sort_inversions
(finite_inversions 0
  (finite_inversions-1 nil 3262528856
   ("" (skosimp*)
    (("" (expand "is_finite")
      ((""
        (inst + "N*N"
         "LAMBDA (p: {i,j | i < j & NOT A!1(i) <= A!1(j)}): proj_1(p)*N+proj_2(p)")
        (("1" (expand "injective?")
          (("1" (skosimp*)
            (("1" (typepred "PROJ_2(x1!1)")
              (("1" (typepred "PROJ_2(x2!1)")
                (("1" (lemma "unique_division")
                  (("1"
                    (inst - "N" "PROJ_1(x1!1)" "PROJ_1(x2!1)"
                     "PROJ_2(x1!1)" "PROJ_2(x2!1)")
                    (("1" (assert)
                      (("1" (flatten)
                        (("1" (decompose-equality +) nil nil)) nil))
                      nil)
                     ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (typepred "PROJ_1(p!1)")
            (("2" (typepred "PROJ_2(p!1)")
              (("2" (case "(PROJ_1(p!1) - N + 1) * N <= 0")
                (("1" (assert) nil nil)
                 ("2" (rewrite "neg_times_le") (("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_finite const-decl "bool" finite_sets nil)
    (neg_times_le formula-decl nil real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (injective? const-decl "bool" functions nil)
    (unique_division formula-decl nil euclidean_division nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mod nonempty-type-eq-decl nil euclidean_division nil)
    (below type-eq-decl nil nat_types 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)
    (< 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)
    (N formal-const-decl "posnat" sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil sort_inversions nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" sort_inversions nil)
    (A!1 skolem-const-decl "[below(N) -> T]" sort_inversions nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   shostak))
(inversions_TCC1 0
  (inversions_TCC1-1 nil 3262528713
   ("" (skosimp*) (("" (rewrite "finite_inversions") nil nil)) nil)
   ((finite_inversions formula-decl nil sort_inversions 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)
    (< 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)
    (N formal-const-decl "posnat" sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil sort_inversions nil))
   shostak))
(finite_ap 0
  (finite_ap-1 nil 3262601179
   ("" (skosimp*)
    (("" (expand "is_finite")
      (("" (typepred "inv!1")
        (("" (expand "is_finite")
          (("" (skosimp*)
            (("" (typepred "pi!1")
              ((""
                (inst + "N!1"
                 "LAMBDA (p: (LAMBDA (i, j): inv!1(pi!1(i),pi!1(j)))): f!1(pi!1(proj_1(p)),pi!1(proj_2(p)))")
                (("" (expand "injective?" 1)
                  (("" (skosimp*)
                    (("" (expand "injective?")
                      ((""
                        (inst -
                         "(pi!1(PROJ_1(x1!1)), pi!1(PROJ_2(x1!1)))"
                         "(pi!1(PROJ_1(x2!1)), pi!1(PROJ_2(x2!1)))")
                        (("" (assert)
                          (("" (flatten)
                            (("" (expand "bijective?")
                              ((""
                                (flatten)
                                ((""
                                  (expand "injective?")
                                  ((""
                                    (inst-cp
                                     -
                                     "PROJ_1(x1!1)"
                                     "PROJ_1(x2!1)")
                                    ((""
                                      (inst
                                       -
                                       "PROJ_2(x1!1)"
                                       "PROJ_2(x2!1)")
                                      ((""
                                        (decompose-equality 1)
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_finite const-decl "bool" finite_sets nil)
    (bijective? const-decl "bool" functions nil)
    (permutation nonempty-type-eq-decl nil permutation nil)
    (injective? const-decl "bool" functions nil)
    (below type-eq-decl nil nat_types 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)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (N formal-const-decl "posnat" sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (index_pair type-eq-decl nil sort_inversions nil)
    (set type-eq-decl nil sets nil)
    (finite_set type-eq-decl nil finite_sets nil))
   nil))
(ap_TCC1 0
  (ap_TCC1-1 nil 3262539429
   ("" (skosimp*) (("" (rewrite "finite_ap") nil nil)) nil)
   ((finite_ap formula-decl nil sort_inversions 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)
    (< 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)
    (N formal-const-decl "posnat" sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (index_pair type-eq-decl nil sort_inversions nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (bijective? const-decl "bool" functions nil)
    (permutation nonempty-type-eq-decl nil permutation nil))
   shostak))
(card_ap 0
  (card_ap-1 nil 3262608494
   ("" (skosimp*)
    (("" (lemma "card_injective_image[index_pair,index_pair]")
      ((""
        (inst -
         "LAMBDA (p: index_pair): (inverse(pi!1)(proj_1(p)), inverse(pi!1)(proj_2(p)))"
         "inv!1")
        (("1"
          (case-replace "image(LAMBDA (p: index_pair):
                               (inverse(pi!1)(PROJ_1(p)), inverse(pi!1)(PROJ_2(p))),
                             inv!1) = ap(pi!1, inv!1)")
          (("1" (hide-all-but 1)
            (("1" (decompose-equality)
              (("1" (expand "image")
                (("1" (expand "ap")
                  (("1" (iff)
                    (("1" (prop)
                      (("1" (skosimp*)
                        (("1" (typepred "x!3")
                          (("1"
                            (case-replace
                             "x!3 = (pi!1(x!1),pi!1(x!2))")
                            (("1" (hide 2 -1)
                              (("1"
                                (typepred "pi!1")
                                (("1"
                                  (lemma
                                   "bijective_inverse[below(N),below(N)]")
                                  (("1"
                                    (inst-cp
                                     -
                                     "x!1"
                                     "PROJ_1(x!3)"
                                     "pi!1")
                                    (("1"
                                      (inst
                                       -
                                       "x!2"
                                       "PROJ_2(x!3)"
                                       "pi!1")
                                      (("1"
                                        (decompose-equality 1)
                                        nil
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (inst + "0") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (inst + "(pi!1(x!1),pi!1(x!2))")
                        (("2" (hide -1)
                          (("2" (typepred "pi!1")
                            (("2"
                              (lemma
                               "bijective_inverse[below(N),below(N)]")
                              (("1"
                                (inst-cp - "x!1" "pi!1(x!1)" "pi!1")
                                (("1"
                                  (inst - "x!2" "pi!1(x!2)" "pi!1")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2" (inst + "0") nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (skosimp*)
                (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil)
           ("2" (hide-all-but 1)
            (("2" (skosimp*)
              (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (expand "injective?")
            (("2" (skosimp*)
              (("2"
                (case "bijective?(inverse[below(N), below(N)](pi!1))")
                (("1" (expand "bijective?")
                  (("1" (flatten)
                    (("1" (expand "injective?")
                      (("1" (inst-cp - "PROJ_1(x1!1)" "PROJ_1(x2!1)")
                        (("1" (inst - "PROJ_2(x1!1)" "PROJ_2(x2!1)")
                          (("1" (decompose-equality 1) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but 1)
                  (("2" (typepred "pi!1")
                    (("2"
                      (rewrite "bij_inv_is_bij[below(N), below(N)]")
                      nil nil))
                    nil))
                  nil)
                 ("3" (hide-all-but 1)
                  (("3" (inst + "0") (("3" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (hide-all-but 1)
          (("3" (skosimp*)
            (("3" (inst + "0") (("3" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((index_pair type-eq-decl nil sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "posnat" sort_inversions 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)
    (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)
    (card_injective_image formula-decl nil function_image_aux nil)
    (bij_inv_is_bij formula-decl nil function_inverse nil)
    (ap const-decl "finite_set[index_pair]" sort_inversions nil)
    (image const-decl "set[R]" function_image nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_image application-judgement "finite_set[R]"
     function_image_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bijective_inverse formula-decl nil function_inverse nil)
    (bijective_inverse_is_bijective application-judgement
     "(bijective?[R, D])" function_inverse nil)
    (unique_bijective_inverse application-judgement "{x: D | f(x) = y}"
     function_inverse nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (x!2 skolem-const-decl "below(N)" sort_inversions nil)
    (x!1 skolem-const-decl "below(N)" sort_inversions nil)
    (inv!1 skolem-const-decl "finite_set[index_pair]" sort_inversions
     nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (injective? const-decl "bool" functions nil)
    (inverse const-decl "D" function_inverse nil)
    (bijective? const-decl "bool" functions nil)
    (permutation nonempty-type-eq-decl nil permutation nil)
    (pi!1 skolem-const-decl "permutation[N]" sort_inversions nil)
    (TRUE const-decl "bool" booleans nil))
   shostak))
(inversions_transpose_TCC1 0
  (inversions_transpose_TCC1-1 nil 3262619020
   ("" (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (N formal-const-decl "posnat" sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(inversions_transpose 0
  (inversions_transpose-1 nil 3262604054
   ("" (skosimp*)
    (("" (decompose-equality)
      (("" (iff)
        (("" (expand* "inversions" "remove" "member" "ap" "o")
          ((""
            (case "j!1 = transpose(j!1, 1 + j!1)(x!1) & 1 + j!1 = transpose(j!1, 1 + j!1)(x!2)")
            (("1" (flatten)
              (("1" (assert)
                (("1" (expand "transpose")
                  (("1" (lift-if)
                    (("1" (assert)
                      (("1" (prop) (("1" (assert) nil nil)) nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (replace 1)
              (("2"
                (case "A!1(transpose(j!1, 1 + j!1)(x!1)) <= A!1(transpose(j!1, 1 + j!1)(x!2))")
                (("1" (assert) nil nil)
                 ("2" (assert)
                  (("2"
                    (case "j!1+1 = transpose(j!1, 1 + j!1)(x!1) & j!1 = transpose(j!1, 1 + j!1)(x!2)")
                    (("1" (flatten)
                      (("1" (replaces (-2 -1) :dir rl)
                        (("1" (typepred "<=")
                          (("1" (expand "total_order?")
                            (("1" (flatten)
                              (("1"
                                (expand "dichotomous?")
                                (("1"
                                  (inst?)
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 5 2)
                      (("2" (expand "transpose")
                        (("2" (lift-if)
                          (("2" (lift-if)
                            (("2" (assert)
                              (("2"
                                (prop)
                                (("1" (assert) nil nil)
                                 ("2" (assert) nil nil)
                                 ("3" (assert) nil nil)
                                 ("4"
                                  (assert)
                                  (("4"
                                    (lift-if)
                                    (("4" (ground) nil nil))
                                    nil))
                                  nil)
                                 ("5"
                                  (assert)
                                  (("5"
                                    (lift-if)
                                    (("5" (ground) nil nil))
                                    nil))
                                  nil)
                                 ("6"
                                  (assert)
                                  (("6"
                                    (lift-if)
                                    (("6" (ground) nil nil))
                                    nil))
                                  nil)
                                 ("7"
                                  (assert)
                                  (("7"
                                    (lift-if)
                                    (("7" (ground) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (finite_remove application-judgement "finite_set[index_pair]"
     sort_inversions nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (T formal-type-decl nil sort_inversions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (inversions const-decl "finite_set[index_pair]" sort_inversions
     nil)
    (O const-decl "T3" function_props nil)
    (bijective? const-decl "bool" functions nil)
    (permutation nonempty-type-eq-decl nil permutation nil)
    (transpose const-decl "permutation" permutation nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (ap const-decl "finite_set[index_pair]" sort_inversions nil)
    (remove const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (index_pair type-eq-decl nil sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "posnat" sort_inversions 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)
    (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)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (dichotomous? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" sort_inversions nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
(card_inversions_transpose 0
  (card_inversions_transpose-1 nil 3262618943
   ("" (skosimp*)
    (("" (rewrite "inversions_transpose")
      (("" (rewrite "card_ap")
        (("" (rewrite "card_remove[index_pair]")
          (("" (lift-if)
            (("" (assert)
              (("" (prop)
                (("" (expand "inversions") (("" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inversions_transpose formula-decl nil sort_inversions 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)
    (< 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)
    (N formal-const-decl "posnat" sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil sort_inversions nil)
    (finite_remove application-judgement "finite_set[index_pair]"
     sort_inversions nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (card_remove formula-decl nil finite_sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (transpose const-decl "permutation" permutation nil)
    (permutation nonempty-type-eq-decl nil permutation nil)
    (bijective? const-decl "bool" functions nil)
    (inversions const-decl "finite_set[index_pair]" sort_inversions
     nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (remove const-decl "set" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (index_pair type-eq-decl nil sort_inversions nil)
    (card_ap formula-decl nil sort_inversions nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
(sorted_iff_no_inversions 0
  (sorted_iff_no_inversions-1 nil 3262627837
   ("" (skosimp*)
    (("" (expand "empty?")
      (("" (expand "member")
        (("" (expand "inversions")
          (("" (expand "sorted?")
            (("" (prop)
              (("1" (skosimp*)
                (("1" (inst - "x!1`1" "x!1`2") (("1" (assert) nil nil))
                  nil))
                nil)
               ("2" (skosimp*)
                (("2" (inst - "(i!1,j!1)") (("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((empty? const-decl "bool" sets nil)
    (inversions const-decl "finite_set[index_pair]" sort_inversions
     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)
    (< 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)
    (N formal-const-decl "posnat" sort_inversions nil)
    (below type-eq-decl nil nat_types nil)
    (below type-eq-decl nil naturalnumbers nil)
    (index_pair type-eq-decl nil sort_inversions nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sorted? const-decl "bool" sort_array nil)
    (member const-decl "bool" sets nil))
   nil))
(successive_inversion_lem 0
  (successive_inversion_lem-1 nil 3262622508
   ("" (induct "d" :name "NAT_induction")
    (("1" (skosimp*)
      (("1" (case-replace "j!1 = 1")
        (("1" (inst? +) (("1" (assert) nil nil)) nil)
         ("2" (inst - "j!1-1")
          (("1" (assert)
            (("1" (inst?)
              (("1" (replace 3)
                (("1" (case "A!1(i!1+j!1-1) <= A!1(i!1+j!1)")
                  (("1" (hide 4)
                    (("1" (inst + "i!1")
                      (("1" (assert)
                        (("1" (typepred "<=")
                          (("1"
                            (expand* "total_order?" "partial_order?"
                             "preorder?" "transitive?")
                            (("1" (flatten)
                              (("1"
                                (inst
                                 -
                                 "A!1(i!1)"
                                 "A!1(i!1 - 1 + j!1)"
                                 "A!1(i!1 + j!1)")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 3)
                    (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil)
     ("2" (skosimp*) (("2" (assert) nil nil)) nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (j!1 skolem-const-decl "nat" sort_inversions nil)
    (preorder? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (NAT_induction formula-decl nil naturalnumbers 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)
    (< 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)
    (N formal-const-decl "posnat" sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil sort_inversions nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" sort_inversions nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil))
   shostak))
(successive_inversion_exists 0
  (successive_inversion_exists-1 nil 3262621870
   ("" (skosimp*)
    (("" (rewrite "sorted_iff_no_inversions")
      (("" (expand* "empty?" "member" "inversions")
        (("" (skosimp*)
          (("" (lemma "successive_inversion_lem")
            (("" (inst?)
              (("" (inst - "x!1`2 - x!1`1")
                (("1" (replace 2 :hide? t)
                  (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sorted_iff_no_inversions formula-decl nil sort_inversions 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)
    (< 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)
    (N formal-const-decl "posnat" sort_inversions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil sort_inversions nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (x!1 skolem-const-decl "index_pair" sort_inversions nil)
    (index_pair type-eq-decl nil sort_inversions nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (successive_inversion_lem formula-decl nil sort_inversions nil)
    (empty? const-decl "bool" sets nil)
    (inversions const-decl "finite_set[index_pair]" sort_inversions
     nil)
    (member const-decl "bool" sets nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.58 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.