Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 46 kB image not shown  

Quelle  sum_orders.prf   Sprache: Lisp

 
(sum_orders
 (sum_preserves_reflexive 0
  (sum_preserves_reflexive-1 nil 3353304649
   ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T1 formal-type-decl nil sum_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (T2 formal-type-decl nil sum_orders nil)
    (inr? adt-recognizer-decl "[union -> boolean]" union_adt nil)
    (right adt-accessor-decl "[(inr?) -> T2]" union_adt nil)
    (union type-decl nil union_adt nil)
    (inl? adt-recognizer-decl "[union -> boolean]" union_adt nil)
    (left adt-accessor-decl "[(inl?) -> T1]" union_adt nil)
    (+ const-decl "bool" sum_orders nil)
    (reflexive? const-decl "bool" relations nil))
   nil))
 (sum_preserves_transitive 0
  (sum_preserves_transitive-1 nil 3353304649
   ("" (skosimp)
    (("" (typepred "r2!1")
      (("" (typepred "r1!1")
        (("" (expand "transitive?")
          (("" (skosimp)
            (("" (expand "+")
              (("" (assert)
                (("" (flatten)
                  (("" (case-replace "inl?(x!1)")
                    (("1" (assert)
                      (("1" (flatten)
                        (("1" (assert)
                          (("1" (flatten)
                            (("1"
                              (inst -2 "left(x!1)" "left(y!1)"
                               "left(z!1)")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assert)
                      (("2" (flatten)
                        (("2" (assert)
                          (("2" (flatten)
                            (("2"
                              (inst -2 "right(x!1)" "right(y!1)"
                               "right(z!1)")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T2 formal-type-decl nil sum_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (+ const-decl "bool" sum_orders nil)
    (right adt-accessor-decl "[(inr?) -> T2]" union_adt nil)
    (inr? adt-recognizer-decl "[union -> boolean]" union_adt nil)
    (left adt-accessor-decl "[(inl?) -> T1]" union_adt nil)
    (union type-decl nil union_adt nil)
    (inl? adt-recognizer-decl "[union -> boolean]" union_adt nil)
    (T1 formal-type-decl nil sum_orders nil))
   nil))
 (sum_preserves_antisymmetric 0
  (sum_preserves_antisymmetric-1 nil 3353304649
   ("" (skosimp)
    (("" (typepred "r2!1")
      (("" (typepred "r1!1")
        (("" (expand "antisymmetric?")
          (("" (skosimp)
            (("" (expand "+")
              (("" (case-replace "inl?(x!1)")
                (("1" (assert)
                  (("1" (flatten)
                    (("1" (inst -2 "left(x!1)" "left(y!1)")
                      (("1" (assert)
                        (("1" (decompose-equality) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert)
                  (("2" (flatten)
                    (("2" (inst -2 "right(x!1)" "right(y!1)")
                      (("2" (assert)
                        (("2" (case "inr?(x!1)")
                          (("1" (assert)
                            (("1" (grind)
                              (("1"
                                (hide -2 -5)
                                (("1" (decompose-equality 1) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T2 formal-type-decl nil sum_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (+ const-decl "bool" sum_orders nil)
    (right adt-accessor-decl "[(inr?) -> T2]" union_adt nil)
    (inr? adt-recognizer-decl "[union -> boolean]" union_adt nil)
    (union_inr_extensionality formula-decl nil union_adt nil)
    (left adt-accessor-decl "[(inl?) -> T1]" union_adt nil)
    (union_inl_extensionality formula-decl nil union_adt nil)
    (union type-decl nil union_adt nil)
    (inl? adt-recognizer-decl "[union -> boolean]" union_adt nil)
    (T1 formal-type-decl nil sum_orders nil))
   nil))
 (sum_preserves_preorder 0
  (sum_preserves_preorder-1 nil 3353304649 ("" (judgement-tcc) nil nil)
   ((sum_preserves_transitive application-judgement
     "(transitive?[union[T1, T2]])" sum_orders nil)
    (sum_preserves_reflexive application-judgement
     "(reflexive?[union[T1, T2]])" sum_orders nil)
    (preorder? const-decl "bool" orders nil))
   nil))
 (sum_preserves_partial_order 0
  (sum_preserves_partial_order-1 nil 3353304649
   ("" (judgement-tcc) nil nil)
   ((sum_preserves_antisymmetric application-judgement
     "(antisymmetric?[union[T1, T2]])" sum_orders nil)
    (sum_preserves_preorder application-judgement
     "(preorder?[union[T1, T2]])" sum_orders nil)
    (partial_order? const-decl "bool" orders nil))
   nil))
 (sum_preserves_directed_complete 0
  (sum_preserves_directed_complete-1 nil 3353304649
   ("" (skosimp)
    (("" (typepred "r2!1")
      (("" (typepred "r1!1")
        (("" (expand "directed_complete?")
          (("" (skosimp)
            (("" (typepred "D!1")
              (("" (expand "nonempty?")
                (("" (expand "empty?")
                  (("" (skosimp)
                    (("" (expand "member")
                      (("" (case "inl?(x!1)")
                        (("1" (name "LD" "{x:T1 | D!1(inl(x))}")
                          (("1" (hide -7 -8)
                            (("1"
                              (case "D!1=image[T1,union[T1,T2]](inl,LD)")
                              (("1"
                                (inst - "LD")
                                (("1"
                                  (expand "least_bounded_above?")
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (inst + "inl(t!1)")
                                      (("1"
                                        (expand "least_upper_bound?")
                                        (("1"
                                          (expand "upper_bound?")
                                          (("1"
                                            (flatten)
                                            (("1"
                                              (split)
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (expand "+")
                                                  (("1"
                                                    (typepred "r!1")
                                                    (("1"
                                                      (replace -2 -1)
                                                      (("1"
                                                        (expand
                                                         "image")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (inst
                                                               -8
                                                               "x!2")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (case-replace
                                                                     "left[T1,T2](inl(x!2)) =x!2")
                                                                    (("1"
                                                                      (decompose-equality)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (skosimp)
                                                (("2"
                                                  (expand "+")
                                                  (("2"
                                                    (case-replace
                                                     "inl?(r!1)")
                                                    (("1"
                                                      (inst
                                                       -10
                                                       "left(r!1)")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (typepred
                                                             "r!2")
                                                            (("1"
                                                              (expand
                                                               "LD"
                                                               -1)
                                                              (("1"
                                                                (inst
                                                                 -3
                                                                 "inl(r!2)")
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (assert)
                                                      (("2"
                                                        (case-replace
                                                         "inr?(r!1)")
                                                        (("1"
                                                          (inst
                                                           -
                                                           "x!1")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2"
                                    (split)
                                    (("1"
                                      (expand "nonempty?")
                                      (("1"
                                        (expand "empty?")
                                        (("1"
                                          (inst - "left(x!1)")
                                          (("1"
                                            (expand "member")
                                            (("1"
                                              (replace -1 -4)
                                              (("1"
                                                (expand "image")
                                                (("1"
                                                  (skosimp)
                                                  (("1"
                                                    (typepred "x!2")
                                                    (("1"
                                                      (replace -5)
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (expand "directed?")
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (inst
                                           -
                                           "inl(x!2)"
                                           "inl(y!1)")
                                          (("2"
                                            (assert)
                                            (("2"
                                              (expand "LD" (-1 -2))
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (expand "+")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (typepred
                                                         "z!1")
                                                        (("2"
                                                          (replace
                                                           -4
                                                           -1)
                                                          (("2"
                                                            (expand
                                                             "image")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (inst
                                                                 +
                                                                 "x!3")
                                                                (("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (replace
                                                                     -1)
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (apply-extensionality 1 :hide? t)
                                  (("2"
                                    (case-replace "D!1(x!2)")
                                    (("1"
                                      (expand "image")
                                      (("1"
                                        (case "inl?(x!2)")
                                        (("1"
                                          (inst + "left(x!2)")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (hide-all-but 1)
                                              (("1"
                                                (grind)
                                                (("1"
                                                  (decompose-equality)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "LD")
                                            (("2"
                                              (hide-all-but (-1 -2 1))
                                              (("2"
                                                (grind)
                                                (("2"
                                                  (case-replace
                                                   "inl(left[T1, T2](x!2)) = x!2")
                                                  (("2"
                                                    (decompose-equality)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (case "inr?(x!2)")
                                          (("1"
                                            (expand "directed?")
                                            (("1"
                                              (inst - "x!1" "x!2")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (skosimp)
                                                  (("1"
                                                    (expand "+")
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (expand "image")
                                        (("2"
                                          (skosimp)
                                          (("2"
                                            (typepred "x!3")
                                            (("2"
                                              (expand "LD")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (case "inr?(x!1)")
                          (("1" (hide 1 -4 -5)
                            (("1" (name "RD" "{x:T2| D!1(inr(x))}")
                              (("1"
                                (case
                                 "D!1=image[T2, union[T1, T2]](inr,RD)")
                                (("1"
                                  (inst - "RD")
                                  (("1"
                                    (expand "least_bounded_above?")
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (inst + "inr(t!1)")
                                        (("1"
                                          (expand "least_upper_bound?")
                                          (("1"
                                            (flatten)
                                            (("1"
                                              (split)
                                              (("1"
                                                (expand "upper_bound?")
                                                (("1"
                                                  (skosimp)
                                                  (("1"
                                                    (expand "+")
                                                    (("1"
                                                      (typepred "r!1")
                                                      (("1"
                                                        (hide -6 -9)
                                                        (("1"
                                                          (replace
                                                           -2
                                                           -1)
                                                          (("1"
                                                            (expand
                                                             "image")
                                                            (("1"
                                                              (skosimp)
                                                              (("1"
                                                                (typepred
                                                                 "x!2")
                                                                (("1"
                                                                  (inst
                                                                   -8
                                                                   "x!2")
                                                                  (("1"
                                                                    (replace
                                                                     -2)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (skosimp)
                                                (("2"
                                                  (expand "+")
                                                  (("2"
                                                    (expand
                                                     "upper_bound?")
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (case-replace
                                                         "inr?(r!1)")
                                                        (("1"
                                                          (inst
                                                           -10
                                                           "right(r!1)")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (skosimp)
                                                              (("1"
                                                                (typepred
                                                                 "r!2")
                                                                (("1"
                                                                  (expand
                                                                   "RD")
                                                                  (("1"
                                                                    (inst
                                                                     -3
                                                                     "inr(r!2)")
                                                                    (("1"
                                                                      (flatten)
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (assert)
                                                          (("2"
                                                            (case
                                                             "inl?(r!1)")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (inst
                                                                 -2
                                                                 "x!1")
                                                                (("1"
                                                                  (flatten)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (split)
                                      (("1"
                                        (expand "nonempty?")
                                        (("1"
                                          (expand "empty?")
                                          (("1"
                                            (inst - "right(x!1)")
                                            (("1"
                                              (expand "member")
                                              (("1"
                                                (expand "RD")
                                                (("1"
                                                  (case-replace
                                                   "inr(right(x!1))=x!1")
                                                  (("1"
                                                    (decompose-equality)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand "directed?")
                                        (("2"
                                          (skosimp)
                                          (("2"
                                            (expand "RD")
                                            (("2"
                                              (inst
                                               -7
                                               "inr(x!2)"
                                               "inr(y!1)")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (expand "+")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (inst
                                                         +
                                                         "right(z!1)")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil)
                                                         ("2"
                                                          (expand "RD")
                                                          (("2"
                                                            (case-replace
                                                             "inr(right[T1, T2](z!1))=z!1")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil)
                                                             ("2"
                                                              (decompose-equality)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2"
                                    (apply-extensionality 1 :hide? t)
                                    (("2"
                                      (case-replace "D!1(x!2)")
                                      (("1"
                                        (expand "image")
                                        (("1"
                                          (expand "directed?")
                                          (("1"
                                            (inst - "x!1" "x!2")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (expand "+")
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (flatten)
                                                        (("1"
                                                          (inst
                                                           +
                                                           "right(x!2)")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (decompose-equality)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "RD")
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (case-replace
                                                                 "inr(right[T1, T2](x!2))=x!2")
                                                                (("2"
                                                                  (decompose-equality)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (assert)
                                        (("2"
                                          (expand "image")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (replace -1)
                                              (("2"
                                                (typepred "x!3")
                                                (("2"
                                                  (expand "RD")
                                                  (("2"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((directed_complete? const-decl "bool" directed_orders nil)
    (partial_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T2 formal-type-decl nil sum_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (+ const-decl "bool" sum_orders nil)
    (directed? const-decl "bool" directed_orders nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (union type-decl nil union_adt nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (inr adt-constructor-decl "[T2 -> (inr?)]" union_adt nil)
    (x!2 skolem-const-decl "union[T1, T2]" sum_orders nil)
    (RD skolem-const-decl "[T2 -> bool]" sum_orders nil)
    (right adt-accessor-decl "[(inr?) -> T2]" union_adt nil)
    (r!2 skolem-const-decl "(RD)" sum_orders nil)
    (union_inr_extensionality formula-decl nil union_adt nil)
    (z!1 skolem-const-decl "(D!1)" sum_orders nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (inl adt-constructor-decl "[T1 -> (inl?)]" union_adt nil)
    (image const-decl "set[R]" function_image nil)
    (x!1 skolem-const-decl "union[T1, T2]" sum_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (left adt-accessor-decl "[(inl?) -> T1]" union_adt nil)
    (inr? adt-recognizer-decl "[union -> boolean]" union_adt nil)
    (r!2 skolem-const-decl "(LD)" sum_orders nil)
    (D!1 skolem-const-decl "(directed?(r1!1 + r2!1))" sum_orders nil)
    (r2!1 skolem-const-decl "(directed_complete?[T2])" sum_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (r1!1 skolem-const-decl "(directed_complete?[T1])" sum_orders nil)
    (LD skolem-const-decl "[T1 -> bool]" sum_orders nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sum_preserves_partial_order application-judgement
     "(partial_order?[union[T1, T2]])" sum_orders nil)
    (x!2 skolem-const-decl "union[T1, T2]" sum_orders nil)
    (union_inl_extensionality formula-decl nil union_adt nil)
    (inl? adt-recognizer-decl "[union -> boolean]" union_adt nil)
    (T1 formal-type-decl nil sum_orders nil))
   nil))
 (sum_preserves_directed_complete_partial_order 0
  (sum_preserves_directed_complete_partial_order-1 nil 3353304649
   ("" (skosimp)
    (("" (typepred "r2!1")
      (("" (typepred "r1!1")
        (("" (expand "directed_complete_partial_order?")
          (("" (flatten)
            ((""
              (lemma "sum_preserves_directed_complete"
               ("r1" "r1!1" "r2" "r2!1"))
              (("1" (propax) nil nil) ("2" (propax) nil nil)
               ("3" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((directed_complete_partial_order? const-decl "bool" directed_orders
     nil)
    (pred type-eq-decl nil defined_types nil)
    (T2 formal-type-decl nil sum_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (sum_preserves_partial_order application-judgement
     "(partial_order?[union[T1, T2]])" sum_orders nil)
    (directed_complete? const-decl "bool" directed_orders nil)
    (partial_order? const-decl "bool" orders nil)
    (sum_preserves_directed_complete judgement-tcc nil sum_orders nil)
    (T1 formal-type-decl nil sum_orders nil))
   nil)))

100%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




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.