Quelle extra_examples.prf Sprache: Lisp

(extra_examples
(fcb 0
  (fcb-1 nil 3247964601
   ("" (skeep)
    (("" (field)
      (("" (cancel-by 1 "nzz") (("" (postpone) nil nil)) nil)) nil))
    nil)
   nil shostak))
(cf 0
  (cf-1 nil 3248475268
   ("" (skeep) (("" (cancel-formula -1) (("" (postpone) nil nil)) nil))
    nil)
   nil shostak))
(distrib 0
          (distrib-1 nil 3248910299
           ("" (skeep)
            (("" (real-props -1)
              (("" (real-props -2 :distrib? nil)
                (("" (grind-reals :dontdistrib (-3 1))
                  (("" (grind-reals) (("" (postpone) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           nil nil))
(replaces1 0
  (replaces1-1 nil 3248186670
   ("" (skeep)
    (("" (replaces (-1 -2) :in 1 :hide? nil)
      (("" (replaces) (("" (postpone) nil nil)) nil)) nil))
    nil)
   nil nil))
(replaces2 0
  (replaces2-1 nil 3248186702
   ("" (skeep)
    (("" (replaces :from -2 :to -3)
      (("" (replaces -2 :dir rl :in 1)
        (("" (replaces -1) (("" (postpone) nil nil)) nil)) nil))
      nil))
    nil)
   nil nil))
(addformulas 0
  (addformulas-2 nil 3250619622
   ("" (skeep)
    (("" (add-formulas -1 :hide? nil)
      (("" (add-formulas -2 -3 :hide? nil)
        (("" (add-formulas -3 -5 :hide? nil)
          (("" (add-formulas -4 -7 :hide? nil)
            (("" (add-formulas -5 -9 :hide? nil)
              (("" (add-formulas -6 1 :hide? nil)
                (("" (add-formulas -7 2 :hide? nil)
                  (("" (add-formulas -8 3 :hide? nil)
                    (("" (add-formulas -9 4 :hide? nil)
                      (("" (hide (-1 -2 -3 -4 -5 -6 -7 -8 -9))
                        (("" (add-formulas -5 5)
                          (("" (add-formulas 2 -1)
                            (("" (add-formulas 3 -2)
                              ((""
                                (add-formulas 4 -1)
                                ((""
                                  (add-formulas 5 -1)
                                  ((""
                                    (add-formulas 1 2)
                                    ((""
                                      (add-formulas 2 3)
                                      ((""
                                        (add-formulas
                                         1
                                         2
                                         :label
                                         "AddFormula")
                                        (("" (postpone) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil)
  (addformulas-1 nil 3250608376
   ("" (skeep)
    (("" (add-formulas -1 :hide? nil)
      (("" (add-formulas -2 -3 :hide? nil)
        (("" (add-formulas -3 -5 :hide? nil)
          (("" (add-formulas -4 -7 :hide? nil)
            (("" (add-formulas -5 -9 :hide? nil)
              (("" (add-formulas -6 1 :hide? nil)
                (("" (add-formulas -7 2 :hide? nil)
                  (("" (add-formulas -8 3 :hide? nil)
                    (("" (add-formulas -9 4 :hide? nil)
                      (("" (hide (-1 -2 -3 -4 -5 -6 -7 -8 -9))
                        (("" (add-formulas -5 5)
                          (("" (add-formulas 2 -1)
                            (("" (add-formulas 3 -2)
                              ((""
                                (add-formulas 4 -1)
                                ((""
                                  (add-formulas 5 -1)
                                  ((""
                                    (add-formulas 1 2)
                                    ((""
                                      (add-formulas 2 3)
                                      ((""
                                        (add-formulas 1 2)
                                        (("" (postpone) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(subformulas 0
  (subformulas-3 nil 3250619670
   ("" (skeep)
    (("" (sub-formulas -1 -2 :hide? nil)
      (("" (sub-formulas -2 -4 :hide? nil)
        (("" (sub-formulas -3 -6 :hide? nil)
          (("" (sub-formulas -5 -8 :hide? nil)
            (("" (sub-formulas -7 1 :hide? nil)
              (("" (sub-formulas -8 2 :hide? nil)
                (("" (sub-formulas -9 3 :hide? nil)
                  (("" (sub-formulas -10 4 :hide? nil)
                    (("" (hide (-1 -2 -3 -4 -5 -6 -7 -8))
                      (("" (sub-formulas 1 -1)
                        (("" (sub-formulas 2 -2)
                          (("" (sub-formulas 3 -3)
                            (("" (sub-formulas 4 -1)
                              ((""
                                (sub-formulas 1 2)
                                ((""
                                  (sub-formulas 2 3)
                                  ((""
                                    (sub-formulas 1 2)
                                    ((""
                                      (sub-formulas
                                       1
                                       -1
                                       :label
                                       "SubFormula")
                                      (("" (postpone) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil)
  (subformulas-2 nil 3250619641
   ("" (skeep)
    (("" (add-formulas -1 :hide? nil)
      (("" (add-formulas -2 -3 :hide? nil)
        (("" (add-formulas -3 -5 :hide? nil)
          (("" (add-formulas -4 -7 :hide? nil)
            (("" (add-formulas -5 -9 :hide? nil)
              (("" (add-formulas -6 1 :hide? nil)
                (("" (add-formulas -7 2 :hide? nil)
                  (("" (add-formulas -8 3 :hide? nil)
                    (("" (add-formulas -9 4 :hide? nil)
                      (("" (hide (-1 -2 -3 -4 -5 -6 -7 -8 -9))
                        (("" (add-formulas -5 5)
                          (("" (add-formulas 2 -1)
                            (("" (add-formulas 3 -2)
                              ((""
                                (add-formulas 4 -1)
                                ((""
                                  (add-formulas 5 -1)
                                  ((""
                                    (add-formulas 1 2)
                                    ((""
                                      (add-formulas 2 3)
                                      ((""
                                        (add-formulas 1 2)
                                        ((""
                                          (postpone)
                                          nil))))))))))))))))))))))))))))))))))))))
    nil)
   nil nil)
  (subformulas-1 nil 3248220329
   ("" (skeep)
    (("" (sub-formulas -1 -2)
      (("" (sub-formulas 1 2)
        (("" (sub-formulas -1 1 :hide? nil)
          (("" (add-formulas -1 -2)
            (("" (add-formulas 1 2)
              (("" (add-formulas -1 1)
                (("" (add-formulas 1 -1)
                  (("" (add-formulas 1 -3)
                    (("" (sub-formulas 1 -1)
                      (("" (add-formulas 1 -1)
                        (("" (postpone) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
(redlet1 0
  (redlet1-1 nil 3251846195
   ("" (skeep)
    (("" (redlet -1)
      (("" (redlet -1 "a" :nth 2)
        (("" (redlet -1)
          (("" (redlet 1 :nth 2)
            (("" (redlet -1 "b")
              (("" (redlet 1) (("" (postpone) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(redlet2 0
  (redlet2-2 nil 3251846285
   ("" (skeep)
    (("" (redlet 1 "b")
      (("" (redlet 2 :nth 2)
        (("" (redlet 1)
          (("" (redlet* 2 :n 2)
            (("" (redlet 1 "a")
              (("" (redlet 1 "c") (("" (postpone) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil)
  (redlet2-1 nil 3251846267 ("" (postpone) nil nil) nil shostak))
(skolet1 0
  (skolet1-1 nil 3251844997
   ("" (skeep)
    (("" (skoletin 1)
      (("" (skoletin 1 :var "Myb" :hide? t)
        (("" (reveal "Myb:")
          (("" (skoletin -3 "a" :nth 2 :postfix "_2")
            (("" (skoletin -1)
              (("" (skoletin -3 :postfix "_2")
                (("" (skoletin -3 :var "AA") (("" (postpone) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(skolet2 0
  (skolet2-1 nil 3251845057
   ("" (skeep)
    (("" (skoletin 1)
      (("" (skoletin 2 :var "dd")
        (("" (skoletin 2 "e" :hide? t)
          (("" (skoletin* 2)
            (("" (skoletin 2) (("" (postpone) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(redsko 0
  (redsko-2 nil 3251846392
   ("" (skeep)
    (("" (redlet* 1 :n 2)
      (("" (skoletin* -1 :postfix "_2" :hide? t)
        (("" (reveal ("a_2:" "b_2:")) (("" (postpone) nil nil)) nil))
        nil))
      nil))
    nil)
   nil nil)
  (redsko-1 nil 3251846371
   ("" (skolem 1 ("px" "py"))
    (("" (let-red* 1 :n 2)
      (("" (skoletin* 1 :n 2)
        (("" (skoletin* 1 :postfix "_2" :hide? t)
          (("" (reveal ("a_2:" "b_2:")) (("" (postpone) nil))))))))))
    nil)
   nil nil))
(skodef 1
  (skodef-2 "" 3251844853
   ("" (skeep) (("" (skodef -1) (("" (postpone) nil nil)) nil)) nil)
   nil shostak)
  (skodef-1 nil 3251838398
   ("" (skeep)
    (("" (skodef -1 "d")
      (("" (skodef -2 :var "bb")
        (("" (skodef* -3 :hide? t)
          (("" (reveal ("a:" "c:"))
            (("" (skodef* 1 :postfix "_2" :n 2)
              (("" (skodef 1 :postfix "_3") (("" (postpone) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
(splash1 0
  (splash1-1 nil 3251459811
   ("" (skeep)
    (("" (splash 1)
      (("1" (skoletin) (("1" (postpone) nil nil)) nil)
       ("2" (postpone) nil nil))
      nil))
    nil)
   nil shostak))
(splash2 0
  (splash2-1 nil 3251459977
   ("" (skeep)
    (("" (splash -)
      (("1" (skoletin -) (("1" (postpone) nil nil)) nil)
       ("2" (postpone) nil nil))
      nil))
    nil)
   nil shostak))
(bothsidesneg 0
  (bothsidesneg-1 nil 3562352259
   ("" (skeep)
    (("" (both-sides-f -2 "sq")
      (("" (neg-formula -1)
        (("" (neg-formula 1)
          (("" (neg-formula 2) (("" (postpone) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   nil nil)))

quality96%

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