Quelle similarity_props.prf Sprache: Lisp

(similarity_props
(similarity_greatest 0
  (similarity_greatest-1 nil 3324312693
   ("" (skosimp :preds? t)
    ((""
      (expand* "similarity?" "preserves" "greatest?" "fullset"
       "upper_bound?" "bijective?" "surjective?")
      (("" (skosimp)
        (("" (inst - "r!1")
          (("" (skolem!)
            (("" (inst - "x!1" "d!1")
              (("" (inst - "x!1") (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((preserves const-decl "bool" functions nil)
    (fullset const-decl "set" sets nil)
    (surjective? const-decl "bool" functions nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (greatest? const-decl "bool" minmax_orders nil)
    (similarity? const-decl "bool" similarity nil)
    (TRUE const-decl "bool" booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil similarity_props nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (R formal-type-decl nil similarity_props nil)
    (bijective? const-decl "bool" functions nil))
   shostak))
(similar_has_greatest 0
  (similar_has_greatest-1 nil 3324312737
   ("" (expand* "similar?" "has_greatest?")
    (("" (skosimp*)
      (("" (inst + "f!1(t!1)")
        (("" (forward-chain "similarity_greatest") nil nil)) nil))
      nil))
    nil)
   ((similarity_greatest formula-decl nil similarity_props nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (D formal-type-decl nil similarity_props nil)
    (R formal-type-decl nil similarity_props nil)
    (similar? const-decl "bool" similarity nil)
    (has_greatest? const-decl "bool" minmax_orders nil))
   shostak))
(similarity_least 0
  (similarity_least-1 nil 3324312766
   ("" (skosimp :preds? t)
    ((""
      (expand* "similarity?" "preserves" "least?" "fullset"
       "lower_bound?" "bijective?" "surjective?")
      (("" (skosimp)
        (("" (inst - "r!1")
          (("" (skolem!)
            (("" (inst - "d!1" "x!1")
              (("" (inst - "x!1") (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((preserves const-decl "bool" functions nil)
    (fullset const-decl "set" sets nil)
    (surjective? const-decl "bool" functions nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (similarity? const-decl "bool" similarity nil)
    (TRUE const-decl "bool" booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil similarity_props nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (R formal-type-decl nil similarity_props nil)
    (bijective? const-decl "bool" functions nil))
   shostak))
(similar_has_least 0
  (similar_has_least-1 nil 3324312811
   ("" (expand* "similar?" "has_least?")
    (("" (skosimp*)
      (("" (inst + "f!1(t!1)")
        (("" (forward-chain "similarity_least") nil nil)) nil))
      nil))
    nil)
   ((similarity_least formula-decl nil similarity_props nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (D formal-type-decl nil similarity_props nil)
    (R formal-type-decl nil similarity_props nil)
    (similar? const-decl "bool" similarity nil)
    (has_least? const-decl "bool" minmax_orders nil))
   shostak))
(similar_finite_TCC1 0
  (similar_finite_TCC1-1 nil 3324312664
   ("" (flatten) (("" (rewrite "finite_full[D]") nil nil)) nil)
   ((finite_full formula-decl nil finite_sets nil)
    (D formal-type-decl nil similarity_props nil))
   nil))
(similar_finite_TCC2 0
  (similar_finite_TCC2-1 nil 3324312664
   ("" (flatten) (("" (rewrite "finite_full[R]") nil nil)) nil)
   ((finite_full formula-decl nil finite_sets nil)
    (R formal-type-decl nil similarity_props nil))
   nil))
(similar_finite 0
  (similar_finite-1 nil 3324312842
   ("" (flatten)
    (("" (skolem-typepred)
      (("" (expand* "similar?" "similarity?" "preserves")
        (("" (rewrite "finite_full[D]")
          (("" (rewrite "finite_full[R]")
            ((""
              (inst +
               "nth(fullset[R], irreflexive_kernel(Rord!1)) o index(fullset[D], irreflexive_kernel(Dord!1))")
              (("1" (skosimp)
                (("1" (expand "o")
                  (("1" (use "index_monotonic[D]")
                    (("1" (expand* "restrict" "preserves")
                      (("1" (inst - "x1!1" "x2!1")
                        (("1" (split)
                          (("1" (use "nth_monotonic[R]")
                            (("1" (expand* "restrict" "preserves")
                              (("1"
                                (inst
                                 -
                                 "index(fullset[D], irreflexive_kernel(Dord!1))(x1!1)"
                                 "index(fullset[D], irreflexive_kernel(Dord!1))(x2!1)")
                                (("1"
                                  (assert)
                                  (("1"
                                    (expand "irreflexive_kernel" -1 1)
                                    (("1"
                                      (expand* "difference" "member")
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "irreflexive_kernel" 1)
                            (("2" (expand* "difference" "member")
                              (("2"
                                (assert)
                                (("2"
                                  (expand "total_order?" -3)
                                  (("2"
                                    (expand*
                                     "partial_order?"
                                     "preorder?"
                                     "reflexive?")
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (inst?)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "fullset" 1 1)
                (("2"
                  (use "composition_bijective[D, below[card(fullset[R])], R]")
                  (("1" (hide -2 -3 -4 -5 -6) (("1" (grind) nil nil))
                    nil)
                   ("2" (use "nth_bijective[R]")
                    (("2" (hide -2 -3 -4 -5 -6 2)
                      (("2" (grind) nil nil)) nil))
                    nil)
                   ("3" (expand "fullset" 1 1)
                    (("3" (split)
                      (("1" (skolem!) (("1" (assert) nil nil)) nil)
                       ("2" (use "index_bijective[D]")
                        (("2" (hide -2 -3 2)
                          (("2"
                            (expand* "bijective?" "injective?"
                             "surjective?")
                            (("2" (prop)
                              (("1"
                                (skosimp)
                                (("1"
                                  (inst - "x1!1" "x2!1")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2"
                                (skolem-typepred)
                                (("2"
                                  (inst - "y!1")
                                  (("1"
                                    (skolem!)
                                    (("1" (inst?) nil nil))
                                    nil)
                                   ("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (skolem!) (("3" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil similarity_props nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (R formal-type-decl nil similarity_props nil)
    (finite_full formula-decl nil finite_sets nil)
    (index_bijective application-judgement
     "(bijective?[(S), below[card(S)]])" similarity_props nil)
    (nth_bijective application-judgement
     "(bijective?[below[card(S)], (S)])" similarity_props nil)
    (linear_order_to_strict_total_order application-judgement
     "(strict_total_order?)" similarity_props nil)
    (linear_order_to_strict_total_order application-judgement
     "(strict_total_order?)" similarity_props nil)
    (Dord!1 skolem-const-decl "(total_order?[D])" similarity_props nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (irreflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (index def-decl "below[card(S)]" finite_below nil)
    (below type-eq-decl nil nat_types nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (strict_total_order? const-decl "bool" orders nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets 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)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (Rord!1 skolem-const-decl "(total_order?[R])" similarity_props nil)
    (nth def-decl "(S)" finite_below nil)
    (O const-decl "T3" function_props nil)
    (bijective? const-decl "bool" functions nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (restrict const-decl "R" restrict nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (difference const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (nth_monotonic formula-decl nil finite_below nil)
    (partial_order? const-decl "bool" orders nil)
    (reflexive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (index_monotonic formula-decl nil finite_below nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (least? const-decl "bool" minmax_orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (union const-decl "set" sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (nth_bijective judgement-tcc nil finite_below nil)
    (y!1 skolem-const-decl "below[card(fullset[R])]" similarity_props
     nil)
    (index_bijective judgement-tcc nil finite_below nil)
    (similar? const-decl "bool" similarity nil)
    (preserves const-decl "bool" functions nil)
    (similarity? const-decl "bool" similarity nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.