Quelle infinite_pigeonhole.prf Sprache: Lisp

(infinite_pigeonhole
(Union_inverse_image 0
  (Union_inverse_image-1 nil 3314537897
   ("" (skolem!)
    (("" (decompose-equality)
      (("" (expand* "fullset" "IUnion" "Union")
        (("" (inst + "f!1(x!1)")
          ((""
            (expand* "inverse_image" "inverse_image" "member"
             "singleton")
            nil nil))
          nil))
        nil))
      nil))
    nil)
   ((bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
    (R formal-type-decl nil infinite_pigeonhole nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (D formal-type-decl nil infinite_pigeonhole nil)
    (member const-decl "bool" sets nil)
    (inverse_image const-decl "set[D]" function_image nil))
   shostak))
(infinite_pigeonhole 0
  (infinite_pigeonhole-1 nil 3314538195
   ("" (skolem!)
    (("" (use "Union_inverse_image")
      (("" (rewrite "IUnion_Union")
        (("" (use "Union_finite[D]")
          (("" (replace -2 :dir rl :hide? t)
            (("" (rewrite "finite_full" :dir rl)
              (("" (rewrite "domain_infiniteness")
                (("" (prop)
                  (("1" (hide-all-but 1)
                    (("1" (expand "image")
                      (("1" (rewrite "finite_image")
                        (("1" (rewrite "finite_full" :dir rl)
                          (("1" (forward-chain "range_finiteness") nil
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "every")
                    (("2" (skolem-typepred)
                      (("2" (expand* "image" "image")
                        (("2" (expand "inverse_image" -)
                          (("2" (skolem!)
                            (("2" (replace -1 :hide? t)
                              (("2" (inst?) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Union_inverse_image formula-decl nil infinite_pigeonhole nil)
    (R formal-type-decl nil infinite_pigeonhole nil)
    (D formal-type-decl nil infinite_pigeonhole nil)
    (Union_finite formula-decl nil finite_sets_of_sets nil)
    (fullset const-decl "set" sets nil)
    (image const-decl "set[R]" function_image nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (finite_full formula-decl nil finite_sets nil)
    (range_finiteness formula-decl nil infinite_pigeonhole nil)
    (finite_image judgement-tcc nil function_image_aux nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (image const-decl "set[R]" function_image nil)
    (every const-decl "bool" sets nil)
    (domain_infiniteness formula-decl nil infinite_pigeonhole nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (IUnion_Union formula-decl nil indexed_sets 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.