Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: scott.prf Sprache: Lisp

Original von: PVS^©

(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)))

¤ Dauer der Verarbeitung: 0.59 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.