Quelle doubletons.prf Sprache: Lisp

(doubletons
(dbl_comm 0
  (dbl_comm-1 nil 3262699089
   ("" (skosimp*)
    (("" (expand "dbl")
      (("" (apply-extensionality 1 :hide? t)
        (("" (iff) (("" (ground) nil))))))))
    nil)
   ((dbl const-decl "set[T]" doubletons nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil doubletons nil))
   nil))
(doubleton_irreflexive 0
  (doubleton_irreflexive-1 nil 3262699089
   ("" (skosimp*)
    (("" (expand "doubleton?")
      (("" (skosimp*)
        ((""
          (case "(FORALL (z:T): member(z,dbl(x!1, x!1)) = member(z,dbl(x!2, y!1)))")
          (("1" (inst-cp -1 "x!2")
            (("1" (inst -1 "y!1")
              (("1" (expand "member")
                (("1" (expand "dbl")
                  (("1" (hide -3) (("1" (ground) nil)))))))))))
           ("2" (skosimp*)
            (("2" (expand "member")
              (("2" (replace -1) (("2" (propax) nil))))))))))))))
    nil)
   ((doubleton? const-decl "bool" doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil doubletons nil))
   nil))
(doubleton_nonempty 0
  (doubleton_nonempty-1 nil 3262699089
   ("" (auto-rewrite-defs :always? t)
    (("" (assert)
      (("" (skolem-typepred)
        (("" (skolem-typepred)
          (("" (flatten)
            (("" (replace*)
              (("" (assert)
                (("" (inst? :if-match t :polarity? nil)
                  (("" (flatten) (("" (propax) nil))))))))))))))))))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil doubletons nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(doubleton_rest_nonempty 0
  (doubleton_rest_nonempty-1 nil 3262699089
   ("" (skolem-typepred)
    (("" (skosimp*)
      (("" (expand "rest")
        (("" (rewrite "doubleton_nonempty")
          (("" (expand "nonempty?")
            (("" (assert)
              (("" (prop)
                (("" (expand "empty?")
                  (("" (expand "remove")
                    (("" (expand "member")
                      (("" (inst-cp - "x!1")
                        (("" (inst - "y!1")
                          (("" (replace -1)
                            (("" (expand "dbl")
                              ((""
                                (assert)
                                nil))))))))))))))))))))))))))))
    nil)
   ((doubleton_nonempty formula-decl nil doubletons nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (rest const-decl "set" sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil doubletons nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(dbl_choose_TCC1 0
  (dbl_choose_TCC1-1 nil 3262699089 ("" (subtype-tcc) nil nil)
   ((T formal-type-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil))
   nil))
(dbl_choose 0
  (dbl_choose-1 nil 3262699089
   ("" (skosimp*)
    (("" (expand "dbl")
      (("" (assert)
        (("" (lemma "choose_is_epsilon[T]")
          (("" (inst?)
            (("1" (replace -1)
              (("1" (hide -1)
                (("1" (lemma "epsilon_ax[T]")
                  (("1" (inst?)
                    (("1" (assert) (("1" (inst + "x!1") nil nil)) nil))
                    nil)
                   ("2" (assert) (("2" (inst + "x!1") nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (expand "nonempty?")
              (("2" (expand "empty?")
                (("2" (expand "member") (("2" (inst - "x!1") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dbl const-decl "set[T]" doubletons nil)
    (T formal-type-decl nil doubletons nil)
    (choose_is_epsilon formula-decl nil sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (TRUE const-decl "bool" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (x!1 skolem-const-decl "T" doubletons nil)
    (y!1 skolem-const-decl "T" doubletons nil))
   nil))
(dbl_rest_choose_TCC1 0
  (dbl_rest_choose_TCC1-1 nil 3262699089
   ("" (skosimp*)
    (("" (use "doubleton_rest_nonempty")
      (("" (inst?) (("" (assert) nil))))))
    nil)
   ((doubleton_rest_nonempty formula-decl nil doubletons nil)
    (x!1 skolem-const-decl "T" doubletons nil)
    (y!1 skolem-const-decl "T" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil doubletons nil))
   nil))
(dbl_rest_choose 0
  (dbl_rest_choose-1 nil 3262699089
   ("" (skosimp*)
    (("" (expand "rest")
      (("" (lemma "doubleton_nonempty")
        (("" (inst - "dbl(x!1, y!1)")
          (("1" (expand "nonempty?")
            (("1" (assert)
              (("1" (use "dbl_choose")
                (("1" (ground)
                  (("1" (replace -2)
                    (("1" (expand "remove")
                      (("1" (expand "member") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil)
                   ("2" (replace -1)
                    (("2" (expand "remove")
                      (("2" (expand "member")
                        (("2" (assert)
                          (("2" (expand "dbl")
                            (("2" (hide -1 3)
                              (("2"
                                (rewrite "choose_is_epsilon[T]")
                                (("1"
                                  (lemma "epsilon_ax[T]")
                                  (("1"
                                    (inst?)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (inst + "y!1")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (inst + "y!1") nil nil))
                                  nil)
                                 ("2"
                                  (expand "nonempty?")
                                  (("2"
                                    (expand "empty?")
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (inst - "y!1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("3" (replace -2)
                    (("3" (expand "remove")
                      (("3" (expand "member") (("3" (assert) nil nil))
                        nil))
                      nil))
                    nil)
                   ("4" (replace -1)
                    (("4" (expand "remove")
                      (("4" (expand "member")
                        (("4" (expand "dbl")
                          (("4" (assert)
                            (("4" (hide -1)
                              (("4"
                                (hide 3)
                                (("4"
                                  (lemma "epsilon_ax[T]")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (hide 3)
                                        (("1"
                                          (rewrite
                                           "choose_is_epsilon[T]")
                                          (("1"
                                            (lemma "epsilon_ax[T]")
                                            (("1"
                                              (inst?)
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (inst + "x!1")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "nonempty?")
                                            (("2"
                                              (expand "empty?")
                                              (("2"
                                                (expand "member")
                                                (("2"
                                                  (inst - "x!1")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (inst?) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 3) (("2" (inst?) (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rest const-decl "set" sets nil)
    (y!1 skolem-const-decl "T" doubletons nil)
    (x!1 skolem-const-decl "T" doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (remove const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (TRUE const-decl "bool" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (choose_is_epsilon formula-decl nil sets nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (dbl_choose formula-decl nil doubletons nil)
    (nonempty? const-decl "bool" sets nil)
    (doubleton_nonempty formula-decl nil doubletons nil))
   nil))
(dbl_to_pair_TCC1 0
  (dbl_to_pair_TCC1-1 nil 3262699089
   ("" (inst 1 " (LAMBDA D: (choose(D),choose(rest(D))))")
    (("1" (skosimp*)
      (("1" (typepred "D!1")
        (("1" (skosimp*)
          (("1" (replace -1)
            (("1" (lemma "dbl_choose")
              (("1" (inst?)
                (("1" (lemma "dbl_rest_choose")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (flatten)
                        (("1" (assert)
                          (("1" (prop)
                            (("1" (replace*) nil)
                             ("2" (replace*)
                              (("2" (rewrite "dbl_comm") nil)))
                             ("3" (replace*) nil)
                             ("4" (replace*)
                              nil)))))))))))))))))))))))))
     ("2" (lemma "doubleton_rest_nonempty") (("2" (propax) nil)))
     ("3" (lemma "doubleton_nonempty") (("3" (propax) nil))))
    nil)
   ((doubleton_nonempty formula-decl nil doubletons nil)
    (doubleton_rest_nonempty formula-decl nil doubletons nil)
    (dbl_choose formula-decl nil doubletons nil)
    (dbl_rest_choose formula-decl nil doubletons nil)
    (dbl_comm formula-decl nil doubletons nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (rest const-decl "set" sets nil) (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil doubletons nil))
   nil))
(dbl_def 0
  (dbl_def-1 nil 3262699089 ("" (skosimp*) (("" (assert) nil)) nil) nil
   nil))
(dbl_in 0
  (dbl_in-1 nil 3262699089
   ("" (skosimp*)
    (("" (replace -1) (("" (hide -1) (("" (grind) nil)))))) nil)
   ((dbl const-decl "set[T]" doubletons nil)) nil))
(dbl_not_in 0
  (dbl_not_in-1 nil 3262699089
   ("" (skosimp*)
    (("" (replace -1) (("" (hide -1) (("" (grind) nil)))))) nil)
   ((dbl const-decl "set[T]" doubletons nil)) nil))
(dbl_to_pair_lem_TCC1 0
  (dbl_to_pair_lem_TCC1-1 nil 3262699089 ("" (subtype-tcc) nil nil)
   ((T formal-type-decl nil doubletons nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(dbl_to_pair_lem 0
  (dbl_to_pair_lem-1 nil 3262699089
   ("" (skosimp*)
    (("" (typepred "dbl_to_pair(dbl(x!1, y!1))")
      (("1"
        (case "dbl(x!1, y!1)(x!1)
          =
        dbl(PROJ_1(dbl_to_pair(dbl(x!1, y!1))),
            PROJ_2(dbl_to_pair(dbl(x!1, y!1))))(x!1)")
        (("1"
          (case "dbl(x!1, y!1)(y!1)
          =
        dbl(PROJ_1(dbl_to_pair(dbl(x!1, y!1))),
            PROJ_2(dbl_to_pair(dbl(x!1, y!1))))(y!1)")
          (("1" (hide -3)
            (("1" (expand "dbl")
              (("1" (apply-extensionality 2 :hide? t)
                (("1" (apply-extensionality 3 :hide? t)
                  (("1" (expand "dbl")
                    (("1" (inst?) (("1" (assert) nil)))))))
                 ("2" (apply-extensionality 3 :hide? t)
                  (("2" (expand "dbl")
                    (("2" (inst?) (("2" (assert) nil)))))))
                 ("3" (expand "dbl")
                  (("3" (inst?) (("3" (assert) nil)))))))))))
           ("2" (assert) nil)))
         ("2" (assert) nil)))
       ("2" (inst?) (("2" (assert) nil))))))
    nil)
   ((dbl_to_pair const-decl "{x, y | D = dbl(x, y)}" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil doubletons nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (y!1 skolem-const-decl "T" doubletons nil)
    (x!1 skolem-const-decl "T" doubletons nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil))
   nil))
(dbl_to_pair_inverse_l 0
  (dbl_to_pair_inverse_l-1 nil 3262699089
   ("" (skolem-typepred)
    (("" (skosimp*)
      (("" (replace -1)
        (("" (use "dbl_to_pair_lem")
          (("" (assert)
            (("" (ground)
              (("1" (replace -1) (("1" (propax) nil)))
               ("2" (replace -1)
                (("2" (rewrite "dbl_comm") nil))))))))))))))
    nil)
   ((dbl_to_pair_lem formula-decl nil doubletons nil)
    (dbl_comm formula-decl nil doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil doubletons nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(dbl_proj 0
  (dbl_proj-1 nil 3262699089
   ("" (skosimp*)
    (("" (lemma "dbl_to_pair_inverse_l")
      (("" (inst?)
        (("" (expand "dbl")
          (("" (replace -1 + rl) (("" (assert) nil))))))))))
    nil)
   ((dbl_to_pair_inverse_l formula-decl nil doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil doubletons nil))
   nil))
(proj_dbl 0
  (proj_dbl-1 nil 3262699089
   ("" (skosimp*)
    (("" (typepred "D!1")
      (("" (skosimp*)
        (("" (replace -1)
          (("" (hide -1)
            (("" (lemma "dbl_to_pair_lem")
              (("" (inst?)
                (("" (assert) (("" (grind) nil))))))))))))))))
    nil)
   ((doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil doubletons nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (dbl_to_pair_lem formula-decl nil doubletons nil))
   nil))
(dbl_eq 0
  (dbl_eq-1 nil 3262699089
   ("" (skosimp*)
    (("" (case "dbl(x!1, y!1)(x!1) = dbl(v!1, z!1)(x!1)")
      (("1" (case "dbl(x!1, y!1)(y!1) = dbl(v!1, z!1)(y!1)")
        (("1" (case "dbl(x!1, y!1)(z!1) = dbl(v!1, z!1)(z!1)")
          (("1" (case "dbl(x!1, y!1)(v!1) = dbl(v!1, z!1)(v!1)")
            (("1" (expand "dbl") (("1" (ground) nil)))
             ("2" (assert) nil)))
           ("2" (assert) nil)))
         ("2" (assert) nil)))
       ("2" (assert) nil))))
    nil)
   ((dbl const-decl "set[T]" doubletons nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(finite_dbl 0
  (finite_dbl-1 nil 3262699128
   ("" (skosimp*)
    (("" (case-replace "dbl[T](x!1, y!1) = add(x!1,singleton(y!1))")
      (("1" (hide -1) (("1" (rewrite "finite_add") nil nil)) nil)
       ("2" (hide 2)
        (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (nonempty_add_finite application-judgement "non_empty_finite_set"
     finite_sets nil)
    (T formal-type-decl nil doubletons nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (nonempty? const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_add formula-decl nil finite_sets nil)
    (member const-decl "bool" sets nil))
   nil))
(finite_doubleton 0
  (finite_doubleton-1 nil 3262699160
   ("" (skosimp*)
    (("" (typepred "e!1")
      (("" (skosimp*)
        (("" (replace -1)
          (("" (hide -1) (("" (rewrite "finite_dbl") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil doubletons nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (finite_dbl formula-decl nil doubletons nil))
   nil))
(card_dbl_TCC1 0
  (card_dbl_TCC1-1 nil 3262699098
   ("" (skosimp*) (("" (rewrite "finite_dbl") nil nil)) nil)
   ((finite_dbl formula-decl nil doubletons nil)
    (T formal-type-decl nil doubletons nil))
   shostak))
(card_dbl 0
  (card_dbl-1 nil 3262699191
   ("" (skosimp*)
    (("" (case-replace "dbl(x!1, y!1) = add(x!1,singleton(y!1))")
      (("1" (hide -1)
        (("1" (rewrite "card_add")
          (("1" (rewrite "card_singleton")
            (("1" (expand "singleton") (("1" (assert) nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (hide 3)
        (("2" (apply-extensionality 1 :hide? t) (("2" (grind) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (nonempty_add_finite application-judgement "non_empty_finite_set"
     finite_sets nil)
    (T formal-type-decl nil doubletons nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (nonempty? const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (card_add formula-decl nil finite_sets nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (card_singleton formula-decl nil finite_sets nil)
    (member const-decl "bool" sets nil))
   nil))
(dbl_TCC1 0
  (dbl_TCC1-1 nil 3262699098
   ("" (skosimp*) (("" (rewrite "finite_dbl") nil nil)) nil)
   ((finite_dbl formula-decl nil doubletons nil)
    (T formal-type-decl nil doubletons nil))
   shostak))
(rev_TCC1 0
  (rev_TCC1-1 nil 3559558981 ("" (subtype-tcc) nil nil)
   ((int_minus_int_is_int application-judgement "int" integers nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.26 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.