products/sources/formale sprachen/PVS/scott/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Ereignis.dat   Sprache: Lisp

Original von: PVS©
(scott_continuity
 (lub_set_image 0
  (lub_set_image-1 nil 3330742497
   ("" (skosimp)
    (("" (typepred "D!1")
      (("" (typepred "g!1")
        (("" (expand "lub_set?")
          (("" (typepred "le2")
            (("" (expand "directed_complete_partial_order?")
              (("" (flatten)
                (("" (expand "directed_complete?")
                  (("" (inst - "image(g!1,D!1)")
                    (("" (hide 2)
                      (("" (split)
                        (("1" (expand "nonempty?")
                          (("1" (expand "empty?")
                            (("1" (skosimp)
                              (("1"
                                (inst - "g!1(x!1)")
                                (("1"
                                  (expand "member")
                                  (("1"
                                    (expand "image")
                                    (("1" (inst + "x!1") nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "directed?")
                          (("2" (skosimp*)
                            (("2" (expand "image")
                              (("2"
                                (skosimp*)
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (replace -2)
                                    (("2"
                                      (expand "directed?")
                                      (("2"
                                        (inst - "x!2" "x!3")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (inst + "g!1(z!1)")
                                              (("1"
                                                (expand "increasing?")
                                                (("1"
                                                  (inst-cp
                                                   -
                                                   "x!2"
                                                   "z!1")
                                                  (("1"
                                                    (inst
                                                     -
                                                     "x!3"
                                                     "z!1")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (expand "image")
                                                (("2"
                                                  (inst + "z!1")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (le1 formal-const-decl "(directed_complete_partial_order?[T1])"
     scott_continuity nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     "orders/")
    (pred type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T1 formal-type-decl nil scott_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (lub_set? const-decl "bool" bounded_order_props "orders/")
    (directed_complete? const-decl "bool" directed_orders "orders/")
    (z!1 skolem-const-decl "(D!1)" scott_continuity nil)
    (member const-decl "bool" sets nil)
    (x!1 skolem-const-decl "T1" scott_continuity nil)
    (empty? const-decl "bool" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (g!1 skolem-const-decl "(increasing?)" scott_continuity nil)
    (D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
    (image const-decl "set[R]" function_image nil)
    (directed? const-decl "bool" directed_orders "orders/")
    (partial_order? const-decl "bool" orders nil)
    (increasing? const-decl "bool" fun_preds_partial nil)
    (le2 formal-const-decl "(directed_complete_partial_order?[T2])"
     scott_continuity nil)
    (T2 formal-type-decl nil scott_continuity nil))
   shostak))
 (directed_image_TCC1 0
  (directed_image_TCC1-1 nil 3352749145
   ("" (skosimp)
    (("" (typepred "D!1")
      (("" (expand "nonempty?")
        (("" (expand "empty?")
          (("" (skosimp)
            (("" (expand "member")
              (("" (inst - "g!1(x!1)")
                (("" (expand "image") (("" (inst + "x!1") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (le1 formal-const-decl "(directed_complete_partial_order?[T1])"
     scott_continuity nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     "orders/")
    (pred type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T1 formal-type-decl nil scott_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (image const-decl "set[R]" function_image nil)
    (x!1 skolem-const-decl "T1" scott_continuity nil)
    (D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
    (T2 formal-type-decl nil scott_continuity nil)
    (le2 formal-const-decl "(directed_complete_partial_order?[T2])"
     scott_continuity nil)
    (increasing? const-decl "bool" fun_preds_partial nil))
   nil))
 (directed_image 0
  (directed_image-1 nil 3352750482
   ("" (skosimp)
    (("" (typepred "D!1")
      (("" (typepred "g!1")
        (("" (expand "directed?")
          (("" (expand "directed?")
            (("" (skosimp*)
              (("" (expand "image")
                (("" (skosimp*)
                  (("" (replace -4)
                    (("" (replace -5)
                      (("" (hide -4 -5 -2)
                        (("" (inst - "x!2" "x!3")
                          (("" (assert)
                            (("" (skosimp)
                              ((""
                                (inst + "g!1(z!1)")
                                (("1"
                                  (expand "increasing?")
                                  (("1"
                                    (inst-cp - "x!2" "z!1")
                                    (("1"
                                      (inst - "x!3" "z!1")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "image")
                                  (("2" (inst + "z!1") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (le1 formal-const-decl "(directed_complete_partial_order?[T1])"
     scott_continuity nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     "orders/")
    (pred type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T1 formal-type-decl nil scott_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (g!1 skolem-const-decl "(increasing?)" scott_continuity nil)
    (D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
    (z!1 skolem-const-decl "(D!1)" scott_continuity nil)
    (image const-decl "set[R]" function_image nil)
    (directed? const-decl "bool" directed_orders "orders/")
    (increasing? const-decl "bool" fun_preds_partial nil)
    (le2 formal-const-decl "(directed_complete_partial_order?[T2])"
     scott_continuity nil)
    (T2 formal-type-decl nil scott_continuity nil))
   shostak))
 (lub_image_TCC1 0
  (lub_image_TCC1-1 nil 3352749145
   ("" (skosimp)
    (("" (lemma "lub_set_image" ("g" "g!1" "D" "D!1"))
      (("" (propax) nil nil)) nil))
    nil)
   ((increasing? const-decl "bool" fun_preds_partial nil)
    (le2 formal-const-decl "(directed_complete_partial_order?[T2])"
     scott_continuity nil)
    (T2 formal-type-decl nil scott_continuity nil)
    (directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (le1 formal-const-decl "(directed_complete_partial_order?[T1])"
     scott_continuity nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     "orders/")
    (pred type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil scott_continuity nil)
    (lub_set_image formula-decl nil scott_continuity nil))
   nil))
 (lub_image 0
  (lub_image-1 nil 3352750819
   ("" (skosimp)
    (("" (typepred "D!1")
      (("" (lemma "directed_image" ("g" "g!1" "D" "D!1"))
        (("" (typepred "lub(image(g!1, D!1))")
          (("1" (expand "least_upper_bound?")
            (("1" (flatten)
              (("1" (inst - "g!1(lub(D!1))")
                (("1" (split -2)
                  (("1" (propax) nil nil)
                   ("2" (hide 2)
                    (("2" (expand "upper_bound?" 1)
                      (("2" (skosimp)
                        (("2" (typepred "r!1")
                          (("2" (expand "image")
                            (("2" (skosimp)
                              (("2"
                                (replace -1)
                                (("2"
                                  (hide -1 -2 -3)
                                  (("2"
                                    (typepred "g!1")
                                    (("2"
                                      (typepred "lub(D!1)")
                                      (("1"
                                        (expand "least_upper_bound?")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (hide -2)
                                            (("1"
                                              (expand "upper_bound?")
                                              (("1"
                                                (inst - "x!1")
                                                (("1"
                                                  (expand
                                                   "increasing?")
                                                  (("1"
                                                    (inst
                                                     -
                                                     "x!1"
                                                     "lub(D!1)")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil)
                                                     ("2"
                                                      (typepred "le1")
                                                      (("2"
                                                        (expand
                                                         "directed_complete_partial_order?")
                                                        (("2"
                                                          (flatten)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (typepred "le1")
                                        (("2"
                                          (expand
                                           "directed_complete_partial_order?")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (typepred "le1")
                  (("2" (expand "directed_complete_partial_order?")
                    (("2" (flatten) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (typepred "le2")
            (("2" (expand "directed_complete_partial_order?")
              (("2" (flatten) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (le1 formal-const-decl "(directed_complete_partial_order?[T1])"
     scott_continuity nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     "orders/")
    (pred type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T1 formal-type-decl nil scott_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (image const-decl "set[R]" function_image nil)
    (lub const-decl
     "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
     bounded_order_props "orders/")
    (lub_set? const-decl "bool" bounded_order_props "orders/")
    (least_upper_bound? const-decl "bool" bounded_orders "orders/")
    (upper_bound? const-decl "bool" bounded_orders "orders/")
    (directed_image formula-decl nil scott_continuity nil)
    (T2 formal-type-decl nil scott_continuity nil)
    (le2 formal-const-decl "(directed_complete_partial_order?[T2])"
     scott_continuity nil)
    (increasing? const-decl "bool" fun_preds_partial nil))
   shostak))
 (lub_image_increasing_TCC1 0
  (lub_image_increasing_TCC1-1 nil 3353382632
   ("" (skosimp)
    (("" (typepred "D!1")
      (("" (expand "nonempty?")
        (("" (expand "empty?")
          (("" (skosimp)
            (("" (inst - "f!1(x!1)")
              (("" (expand "member")
                (("" (expand "image") (("" (inst + "x!1") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (le1 formal-const-decl "(directed_complete_partial_order?[T1])"
     scott_continuity nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     "orders/")
    (pred type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T1 formal-type-decl nil scott_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (empty? const-decl "bool" sets nil)
    (T2 formal-type-decl nil scott_continuity nil)
    (image const-decl "set[R]" function_image nil)
    (x!1 skolem-const-decl "T1" scott_continuity nil)
    (D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
    (member const-decl "bool" sets nil))
   nil))
 (lub_image_increasing_TCC2 0
  (lub_image_increasing_TCC2-1 nil 3353382632
   ("" (skosimp)
    (("" (typepred "D!1")
      (("" (expand "lub_set?")
        (("" (typepred "le2")
          (("" (expand "directed_complete_partial_order?")
            (("" (flatten)
              (("" (expand "directed_complete?")
                (("" (inst - "image[T1,T2](f!1,D!1)")
                  (("" (expand "directed?" -4) (("" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (le1 formal-const-decl "(directed_complete_partial_order?[T1])"
     scott_continuity nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     "orders/")
    (pred type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T1 formal-type-decl nil scott_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil scott_continuity nil)
    (le2 formal-const-decl "(directed_complete_partial_order?[T2])"
     scott_continuity nil)
    (partial_order? const-decl "bool" orders nil)
    (directed? const-decl "bool" directed_orders "orders/")
    (image const-decl "set[R]" function_image nil)
    (D!1 skolem-const-decl "directed[T1, le1]" scott_continuity nil)
    (f!1 skolem-const-decl "[T1 -> T2]" scott_continuity nil)
    (directed_complete? const-decl "bool" directed_orders "orders/")
    (lub_set? const-decl "bool" bounded_order_props "orders/"))
   nil))
 (lub_image_increasing 0
  (lub_image_increasing-1 nil 3353382128
   ("" (skolem + ("f"))
    (("" (expand "increasing?")
      (("" (flatten)
        (("" (skolem + ("x" "y"))
          (("" (flatten)
            (("" (name "X" "lambda (z:T1): z=x OR z=y")
              (("" (case "lub_set?(X)")
                (("1" (case "lub[T1,le1](X)=y")
                  (("1" (inst - "X")
                    (("1" (replace -1)
                      (("1" (case-replace "f(x)=f(y)")
                        (("1" (typepred "le2")
                          (("1"
                            (expand "directed_complete_partial_order?")
                            (("1" (expand "partial_order?")
                              (("1"
                                (expand "preorder?")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (expand "reflexive?")
                                    (("1" (inst - "f(y)") nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2"
                          (case-replace
                           "image(f,X) = LAMBDA (z:T2): z = f(x) OR z = f(y)")
                          (("1"
                            (name-replace "Y"
                             "LAMBDA (z: T2): z = f(x) OR z = f(y)")
                            (("1" (flatten)
                              (("1"
                                (case "lub_set?(Y)")
                                (("1"
                                  (case
                                   "lub[T2,le2](Y)=f(x) OR lub[T2,le2](Y)=f(y)")
                                  (("1"
                                    (split -1)
                                    (("1" (assert) nil nil)
                                     ("2"
                                      (typepred "lub[T2, le2](Y)")
                                      (("2"
                                        (expand "least_upper_bound?")
                                        (("2"
                                          (flatten)
                                          (("2"
                                            (expand "upper_bound?")
                                            (("2"
                                              (inst - "f(x)")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (expand "Y")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (flatten)
                                    (("2"
                                      (typepred "lub[T2, le2](Y)")
                                      (("2"
                                        (expand "least_upper_bound?")
                                        (("2"
                                          (flatten)
                                          (("2"
                                            (expand "upper_bound?")
                                            (("2"
                                              (inst - "f(y)")
                                              (("1"
                                                (typepred "le2")
                                                (("1"
                                                  (expand
                                                   "directed_complete_partial_order?")
                                                  (("1"
                                                    (expand
                                                     "partial_order?")
                                                    (("1"
                                                      (expand
                                                       "antisymmetric?")
                                                      (("1"
                                                        (flatten)
                                                        (("1"
                                                          (inst
                                                           -
                                                           "lub[T2, le2](Y)"
                                                           "f(y)")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (expand "Y")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (assert)
                                    (("3"
                                      (typepred "le2")
                                      (("3"
                                        (expand
                                         "directed_complete_partial_order?")
                                        (("3" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "lub_set?")
                                  (("2"
                                    (typepred "le2")
                                    (("2"
                                      (expand
                                       "directed_complete_partial_order?")
                                      (("2"
                                        (expand "directed_complete?")
                                        (("2"
                                          (flatten)
                                          (("2"
                                            (inst - "Y")
                                            (("2"
                                              (expand "directed?")
                                              (("2"
                                                (skosimp)
                                                (("2"
                                                  (expand "directed?")
                                                  (("2"
                                                    (inst
                                                     -8
                                                     "x!1"
                                                     "y!1")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (typepred "le2")
                                  (("3"
                                    (expand
                                     "directed_complete_partial_order?")
                                    (("3" (flatten) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (apply-extensionality 1 :hide? t)
                            (("2" (expand "image")
                              (("2"
                                (hide-all-but 1)
                                (("2"
                                  (case-replace
                                   "EXISTS (x: (X)): x!1 = f(x)")
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (typepred "x!2")
                                      (("1"
                                        (expand "X")
                                        (("1"
                                          (split -1)
                                          (("1" (assert) nil nil)
                                           ("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (replace 1 2)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (split -1)
                                        (("1"
                                          (inst + "x")
                                          (("1"
                                            (expand "X")
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (inst + "y")
                                          (("2"
                                            (expand "X")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2 -3)
                      (("2" (split)
                        (("1" (expand "nonempty?")
                          (("1" (expand "empty?")
                            (("1" (inst - "x")
                              (("1"
                                (expand "member")
                                (("1"
                                  (expand "X")
                                  (("1" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "directed?")
                          (("2" (expand "directed?")
                            (("2" (skosimp)
                              (("2"
                                (typepred "lub[T1, le1](X)")
                                (("2"
                                  (replace -4)
                                  (("2"
                                    (expand "least_upper_bound?")
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (expand "upper_bound?")
                                        (("2"
                                          (inst + "y")
                                          (("1"
                                            (inst-cp - "x!1")
                                            (("1"
                                              (inst - "y!1")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "X")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -3 2)
                    (("2" (typepred "lub[T1, le1](X)")
                      (("2" (expand "least_upper_bound?")
                        (("2" (flatten)
                          (("2" (expand "upper_bound?")
                            (("2" (inst -2 "y")
                              (("2"
                                (inst -1 "y")
                                (("1"
                                  (split -2)
                                  (("1"
                                    (typepred "le1")
                                    (("1"
                                      (expand
                                       "directed_complete_partial_order?")
                                      (("1"
                                        (expand "partial_order?")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (expand "antisymmetric?")
                                            (("1"
                                              (inst
                                               -
                                               "lub[T1, le1](X)"
                                               "y")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (skosimp)
                                    (("2"
                                      (typepred "r!1")
                                      (("2"
                                        (expand "X")
                                        (("2"
                                          (split -1)
                                          (("1" (assert) nil nil)
                                           ("2"
                                            (typepred "le1")
                                            (("2"
                                              (expand
                                               "directed_complete_partial_order?")
                                              (("2"
                                                (expand
                                                 "partial_order?")
                                                (("2"
                                                  (expand "preorder?")
                                                  (("2"
                                                    (flatten)
                                                    (("2"
                                                      (expand
                                                       "reflexive?")
                                                      (("2"
                                                        (inst - "y")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "X")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("3" (propax) nil nil))
                  nil)
                 ("2" (hide 2 -2 -1)
                  (("2" (expand "lub_set?")
                    (("2" (expand "least_bounded_above?")
                      (("2" (inst + "y")
                        (("2" (expand "least_upper_bound?")
                          (("2" (expand "upper_bound?")
                            (("2" (split)
                              (("1"
                                (skosimp)
                                (("1"
                                  (typepred "r!1")
                                  (("1"
                                    (expand "X")
                                    (("1"
                                      (split -1)
                                      (("1" (assert) nil nil)
                                       ("2"
                                        (typepred "le1")
                                        (("2"
                                          (expand
                                           "directed_complete_partial_order?")
                                          (("2"
                                            (expand "partial_order?")
                                            (("2"
                                              (expand "preorder?")
                                              (("2"
                                                (flatten)
                                                (("2"
                                                  (expand "reflexive?")
                                                  (("2"
                                                    (inst - "y")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (skosimp*)
                                (("2"
                                  (inst - "y")
                                  (("2"
                                    (expand "X")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (typepred "le1")
                  (("3" (expand "directed_complete_partial_order?")
                    (("3" (flatten) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((increasing? const-decl "bool" fun_preds_partial nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil scott_continuity nil)
    (least_bounded_above? const-decl "bool" bounded_orders "orders/")
    (lub const-decl
     "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
     bounded_order_props "orders/")
    (least_upper_bound? const-decl "bool" bounded_orders "orders/")
    (y!1 skolem-const-decl "T1" scott_continuity nil)
    (x!1 skolem-const-decl "T1" scott_continuity nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (image const-decl "set[R]" function_image nil)
    (directed? const-decl "bool" directed_orders "orders/")
    (directed_complete? const-decl "bool" directed_orders "orders/")
    (Y skolem-const-decl "[T2 -> boolean]" scott_continuity nil)
    (f skolem-const-decl "[T1 -> T2]" scott_continuity nil)
    (x skolem-const-decl "T1" scott_continuity nil)
    (upper_bound? const-decl "bool" bounded_orders "orders/")
    (y skolem-const-decl "T1" scott_continuity nil)
    (antisymmetric? const-decl "bool" relations nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (le2 formal-const-decl "(directed_complete_partial_order?[T2])"
     scott_continuity nil)
    (partial_order? const-decl "bool" orders nil)
    (reflexive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (T2 formal-type-decl nil scott_continuity nil)
    (directed type-eq-decl nil directed_order_props "orders/")
    (directed? const-decl "bool" directed_order_props "orders/")
    (X skolem-const-decl "[T1 -> boolean]" scott_continuity nil)
    (nonempty? const-decl "bool" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (partial_order_antisymmetric formula-decl nil partial_order_props
     "orders/")
    (partial_order_reflexive formula-decl nil partial_order_props
     "orders/")
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (directed_complete_partial_order? const-decl "bool" directed_orders
     "orders/")
    (le1 formal-const-decl "(directed_complete_partial_order?[T1])"
     scott_continuity nil)
    (lub_set? const-decl "bool" bounded_order_props "orders/"))
   shostak))
 (scott_continuous_def 0
  (scott_continuous_def-1 nil 3330155115
   ("" (skosimp)
    (("" (expand "scott_continuous?")
      (("" (split)
        (("1" (flatten)
          (("1" (case-replace "increasing?(f!1)")
            (("1" (expand "lub_preserving?")
              (("1" (skosimp)
                (("1" (typepred "D!1")
                  (("1" (lemma "directed_image" ("g" "f!1" "D" "D!1"))
                    (("1"
                      (case "nonempty?[T2](image[T1, T2](f!1,D!1))")
                      (("1"
                        (lemma "closure_is_down"
                         ("x" "lub[T2, le2](image(f!1, D!1))"))
                        (("1" (name "FD" "image(f!1, D!1)")
                          (("1" (replace -1)
                            (("1" (name "JFD" "lub[T2, le2](FD)")
                              (("1"
                                (replace -1)
                                (("1"
                                  (lemma
                                   "down_is_closed[T2,le2]"
                                   ("x" "JFD"))
                                  (("1"
                                    (expand "member")
                                    (("1"
                                      (rewrite
                                       "continuous_closed_sets")
                                      (("1"
                                        (inst - "down(JFD)")
                                        (("1"
                                          (expand "closed?")
                                          (("1"
                                            (expand "scott_open_sets")
                                            (("1"
                                              (expand "Complement")
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (split -10)
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (typepred "b!1")
                                                      (("1"
                                                        (rewrite
                                                         "complement_equal")
                                                        (("1"
                                                          (case
                                                           "subset?(D!1,b!1)")
                                                          (("1"
                                                            (expand
                                                             "scott_closed_sets")
                                                            (("1"
                                                              (expand
                                                               "extend")
                                                              (("1"
                                                                (prop)
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "D!1")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (typepred
                                                                       "lub[T2,le2](FD)")
                                                                      (("1"
                                                                        (replace
                                                                         -7)
                                                                        (("1"
                                                                          (typepred
                                                                           "lub(D!1)")
                                                                          (("1"
                                                                            (name
                                                                             "JD"
                                                                             "lub(D!1)")
                                                                            (("1"
                                                                              (replace
                                                                               -1)
                                                                              (("1"
                                                                                (expand
                                                                                 "least_upper_bound?")
                                                                                (("1"
                                                                                  (flatten)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "increasing?")
                                                                                    (("1"
                                                                                      (inst
                                                                                       -5
                                                                                       "f!1(JD)")
                                                                                      (("1"
                                                                                        (split
                                                                                         -5)
                                                                                        (("1"
                                                                                          (expand
                                                                                           "inverse_image")
                                                                                          (("1"
                                                                                            (expand
                                                                                             "member")
                                                                                            (("1"
                                                                                              (replace
                                                                                               -9
                                                                                               -7
                                                                                               rl)
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "down")
                                                                                                  (("1"
                                                                                                    (lemma
                                                                                                     "partial_order_antisymmetric"
                                                                                                     ("x"
                                                                                                      "f!1(JD)"
                                                                                                      "y"
                                                                                                      "JFD"))
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (expand
                                                                                           "upper_bound?")
                                                                                          (("2"
                                                                                            (skosimp)
                                                                                            (("2"
                                                                                              (typepred
                                                                                               "r!1")
                                                                                              (("2"
                                                                                                (replace
                                                                                                 -12
                                                                                                 -1
                                                                                                 rl)
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "image")
                                                                                                  (("2"
                                                                                                    (skosimp)
                                                                                                    (("2"
                                                                                                      (replace
                                                                                                       -1)
                                                                                                      (("2"
                                                                                                        (inst
                                                                                                         -18
                                                                                                         "x!1"
                                                                                                         "JD")
                                                                                                        (("2"
                                                                                                          (inst
                                                                                                           -3
                                                                                                           "x!1")
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (typepred
                                                                             "le1")
                                                                            (("2"
                                                                              (expand
                                                                               "directed_complete_partial_order?")
                                                                              (("2"
                                                                                (flatten)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "subset?")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (expand
                                                                 "member")
                                                                (("2"
                                                                  (replace
                                                                   -3
                                                                   1
                                                                   rl)
                                                                  (("2"
                                                                    (expand
                                                                     "inverse_image")
                                                                    (("2"
                                                                      (expand
                                                                       "member")
                                                                      (("2"
                                                                        (expand
                                                                         "down")
                                                                        (("2"
                                                                          (expand
                                                                           "JFD")
                                                                          (("2"
                                                                            (typepred
                                                                             "lub[T2, le2](FD)")
                                                                            (("2"
                                                                              (expand
                                                                               "least_upper_bound?")
                                                                              (("2"
                                                                                (flatten)
                                                                                (("2"
                                                                                  (expand
                                                                                   "upper_bound?")
                                                                                  (("2"
                                                                                    (inst
                                                                                     -
                                                                                     "f!1(x!1)")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "FD")
                                                                                      (("2"
                                                                                        (expand
                                                                                         "image")
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.74 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
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.


Bot Zugriff