SSL set_antisymmetric.prf Sprache: Lisp

(set_antisymmetric
(inj_inj_bij 0
  (inj_inj_bij-1 nil 3315050511
   ("" (skosimp*)
    ((""
      (inst +
       "LAMBDA (d: D): IF in_closure(f!1, f!2, d) THEN f!1(d) ELSE inverse_alt(f!2)(d) ENDIF")
      (("1" (expand "bijective?")
        (("1" (split)
          (("1" (expand "injective?")
            (("1" (skosimp)
              (("1" (lift-if)
                (("1" (lift-if)
                  (("1" (lift-if)
                    (("1" (prop)
                      (("1" (inst - "x1!1" "x2!1")
                        (("1" (assert) nil nil)) nil)
                       ("2" (expand "in_closure" +)
                        (("2" (flatten)
                          (("2" (inst + "x1!1")
                            (("2" (assert)
                              (("2"
                                (expand*
                                 "image"
                                 "complement"
                                 "difference"
                                 "member")
                                (("2"
                                  (skolem!)
                                  (("2"
                                    (replace -1)
                                    (("2"
                                      (typepred
                                       "inverse_alt[R, D](f!2)")
                                      (("1"
                                        (expand "inverse?")
                                        (("1"
                                          (inst - "x2!1")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (inst + "x!1")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (flatten)
                                        (("2" (inst?) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("3" (expand "in_closure" +)
                        (("3" (flatten)
                          (("3" (inst + "x2!1")
                            (("3" (assert)
                              (("3"
                                (expand*
                                 "image"
                                 "complement"
                                 "difference"
                                 "member")
                                (("3"
                                  (skosimp*)
                                  (("3"
                                    (replace -3)
                                    (("3"
                                      (replace -2 :dir rl)
                                      (("3"
                                        (typepred
                                         "inverse_alt[R, D](f!2)")
                                        (("1"
                                          (expand "inverse?")
                                          (("1"
                                            (inst - "f!2(x!1)")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (inst + "x!1")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (flatten)
                                          (("2" (inst?) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("4"
                        (expand* "in_closure" "image" "complement"
                         "difference" "member")
                        (("4" (skosimp*)
                          (("4" (replace -1)
                            (("4" (replace -3)
                              (("4"
                                (typepred "inverse_alt[R, D](f!2)")
                                (("1"
                                  (expand "inverse?")
                                  (("1"
                                    (inst-cp - "f!2(x!2)")
                                    (("1"
                                      (inst - "f!2(x!1)")
                                      (("1"
                                        (ground)
                                        (("1" (inst + "x!2") nil nil)
                                         ("2" (inst + "x!1") nil nil)
                                         ("3" (inst + "x!2") nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (flatten)
                                  (("2" (inst?) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "surjective?")
            (("2" (skolem!)
              (("2" (case "in_closure(f!1, f!2, f!2(y!1))")
                (("1" (expand "in_closure" -)
                  (("1" (split)
                    (("1"
                      (expand* "fullset" "image" "complement"
                       "difference" "member")
                      (("1" (inst + "y!1") nil nil)) nil)
                     ("2" (skosimp)
                      (("2" (inst + "e!1")
                        (("2" (assert)
                          (("2" (expand "injective?")
                            (("2" (inst -4 "f!1(e!1)" "y!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (inst + "f!2(y!1)")
                  (("2" (assert)
                    (("2" (typepred "inverse_alt[R, D](f!2)")
                      (("1" (expand "inverse?")
                        (("1" (inst - "f!2(y!1)")
                          (("1" (split)
                            (("1" (expand "injective?")
                              (("1"
                                (inst
                                 -3
                                 "inverse_alt(f!2)(f!2(y!1))"
                                 "y!1")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (flatten)
                                  (("2" (inst?) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (inst + "y!1") nil nil))
                            nil))
                          nil))
                        nil)
                       ("2" (flatten) (("2" (inst?) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp) (("2" (inst + "f!1(d!1)") nil nil)) nil))
      nil))
    nil)
   ((FALSE const-decl "bool" booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (f!2 skolem-const-decl "[R -> D]" set_antisymmetric nil)
    (f!1 skolem-const-decl "[D -> R]" set_antisymmetric nil)
    (in_closure inductive-decl "bool" set_antisymmetric nil)
    (R formal-type-decl nil set_antisymmetric nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (D formal-type-decl nil set_antisymmetric nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (inverses nonempty-type-eq-decl nil function_inverse_alt nil)
    (inverse_alt const-decl "inverses(f)" function_inverse_alt nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (image const-decl "set[R]" function_image nil)
    (member const-decl "bool" sets nil)
    (complement const-decl "set" sets nil)
    (injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions nil))
   shostak))
(surj_surj_bij 0
  (surj_surj_bij-1 nil 3315051063
   ("" (skosimp*)
    (("" (lemma "inj_inj_bij")
      (("" (prop)
        (("1" (use "surjective_inverse_exists[R, D]")
          (("1" (skolem!)
            (("1" (use "inj_inv_alt[R, D]") (("1" (inst?) nil nil))
              nil))
            nil))
          nil)
         ("2" (use "surjective_inverse_exists[D, R]")
          (("2" (skolem!)
            (("2" (use "inj_inv_alt[D, R]") (("2" (inst?) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inj_inj_bij formula-decl nil set_antisymmetric nil)
    (f!1 skolem-const-decl "[D -> R]" set_antisymmetric nil)
    (g!1 skolem-const-decl "[R -> D]" set_antisymmetric nil)
    (surjective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (R formal-type-decl nil set_antisymmetric nil)
    (D formal-type-decl nil set_antisymmetric nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (surjective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[R -> D]" set_antisymmetric nil)
    (inj_inv_alt formula-decl nil function_inverse_def nil)
    (g!1 skolem-const-decl "[D -> R]" set_antisymmetric nil)
    (inverse? const-decl "bool" function_inverse_def nil))
   shostak))
(inj_surj_bij 0
  (inj_surj_bij-1 nil 3315051117
   ("" (skosimp*)
    (("" (lemma "inj_inj_bij")
      (("" (prop)
        (("1" (inst?) nil nil)
         ("2" (assert)
          (("2" (lemma "surjective_inverse_exists[D, R]" ("f" "f!2"))
            (("2" (skolem!)
              (("2" (use "inj_inv_alt[D, R]") (("2" (inst?) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inj_inj_bij formula-decl nil set_antisymmetric nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (g!1 skolem-const-decl "[R -> D]" set_antisymmetric nil)
    (f!2 skolem-const-decl "[D -> R]" set_antisymmetric nil)
    (inj_inv_alt formula-decl nil function_inverse_def nil)
    (surjective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (surjective? const-decl "bool" functions nil)
    (R formal-type-decl nil set_antisymmetric nil)
    (D formal-type-decl nil set_antisymmetric nil))
   shostak)))

quality100%

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