Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: minmax_orders.pvs Sprache: Lisp

Original von: PVS^©

(lifted_orders
(lift_preserves_reflexive 0
  (lift_preserves_reflexive-1 nil 3353157533
   ("" (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)
    (T formal-type-decl nil lifted_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (lift type-decl nil lift_adt nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (lift const-decl "bool" lifted_orders nil)
    (reflexive? const-decl "bool" relations nil))
   nil))
(lift_preserves_transitive 0
  (lift_preserves_transitive-1 nil 3353157533
   ("" (skosimp)
    (("" (typepred "r!1")
      (("" (expand "lift")
        (("" (expand "transitive?")
          (("" (skosimp*)
            (("" (assert)
              (("" (flatten)
                (("" (assert)
                  (("" (flatten)
                    (("" (inst - "down(x!1)" "down(y!1)" "down(z!1)")
                      (("" (assert) 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)
    (T formal-type-decl nil lifted_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (lift type-decl nil lift_adt nil)
    (lift const-decl "bool" lifted_orders nil))
   nil))
(lift_preserves_antisymmetric 0
  (lift_preserves_antisymmetric-1 nil 3353157533
   ("" (skosimp)
    (("" (expand "lift")
      (("" (typepred "r!1")
        (("" (expand "antisymmetric?")
          (("" (skosimp)
            (("" (split -2)
              (("1" (assert)
                (("1" (case-replace "x!1=bottom")
                  (("1" (assert) nil nil)
                   ("2" (case-replace "y!1=bottom")
                    (("1" (assert) nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (flatten)
                (("2" (assert)
                  (("2" (flatten)
                    (("2" (inst - "down(x!1)" "down(y!1)")
                      (("2" (assert)
                        (("2"
                          (lemma "down_equal" ("y1" "x!1" "y2" "y!1"))
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lift const-decl "bool" lifted_orders nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (lift type-decl nil lift_adt nil)
    (down_equal formula-decl nil lift_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil lifted_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil))
   nil))
(lift_preserves_preorder 0
  (lift_preserves_preorder-1 nil 3353157533
   ("" (judgement-tcc) nil nil)
   ((lift_preserves_transitive application-judgement
     "(transitive?[lift[T]])" lifted_orders nil)
    (lift_preserves_reflexive application-judgement
     "(reflexive?[lift[T]])" lifted_orders nil)
    (preorder? const-decl "bool" orders nil))
   nil))
(lift_preserves_partial_order 0
  (lift_preserves_partial_order-1 nil 3353157533
   ("" (judgement-tcc) nil nil)
   ((lift_preserves_antisymmetric application-judgement
     "(antisymmetric?[lift[T]])" lifted_orders nil)
    (lift_preserves_preorder application-judgement
     "(preorder?[lift[T]])" lifted_orders nil)
    (partial_order? const-decl "bool" orders nil))
   nil))
(lift_lub_emptyset_TCC1 0
  (lift_lub_emptyset_TCC1-1 nil 3353299816
   ("" (skosimp)
    (("" (expand "lift")
      (("" (expand "least_bounded_above?")
        (("" (inst + "bottom")
          (("" (expand "least_upper_bound?")
            (("" (expand "upper_bound?")
              (("" (skosimp)
                (("" (typepred "r!1")
                  (("" (expand "emptyset") (("" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lift const-decl "bool" lifted_orders nil)
    (T formal-type-decl nil lifted_orders nil)
    (lift type-decl nil lift_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (emptyset const-decl "set" sets nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil))
   nil))
(lift_lub_emptyset 0
  (lift_lub_emptyset-1 nil 3353299946
   ("" (skosimp)
    (("" (typepred "lub(lift(rel!1))(emptyset[lift[T]])")
      (("" (lemma "lift_lub_emptyset_TCC1")
        (("" (inst - "rel!1")
          ((""
            (name-replace "LUB" "lub(lift(rel!1))(emptyset[lift[T]])")
            (("" (hide -1)
              (("" (expand "least_upper_bound?")
                (("" (flatten)
                  (("" (expand "upper_bound?")
                    (("" (expand "lift")
                      (("" (inst -2 "bottom")
                        (("" (assert)
                          (("" (skosimp)
                            (("" (typepred "r!1")
                              ((""
                                (expand "emptyset")
                                (("" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((emptyset const-decl "set" sets nil)
    (lift const-decl "bool" lifted_orders nil)
    (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
     bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil) (lift type-decl nil lift_adt nil)
    (T formal-type-decl nil lifted_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (finite_emptyset name-judgement "finite_set[T]" lifted_orders nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (lift_lub_emptyset_TCC1 subtype-tcc nil lifted_orders nil))
   shostak))
(lift_lub_bounded_TCC1 0
  (lift_lub_bounded_TCC1-1 nil 3353300373
   ("" (skosimp)
    (("" (typepred "S!1")
      (("" (expand "least_bounded_above?")
        (("" (case "nonempty?(S!1)")
          (("1" (expand "least_upper_bound?")
            (("1" (expand "lift")
              (("1" (expand "upper_bound?")
                (("1" (expand "nonempty_least_bounded_above?")
                  (("1" (assert)
                    (("1" (expand "least_bounded_above?")
                      (("1" (skosimp)
                        (("1" (inst + "up(t!1)")
                          (("1" (expand "least_upper_bound?")
                            (("1" (flatten)
                              (("1"
                                (expand "upper_bound?")
                                (("1"
                                  (split)
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (typepred "r!1")
                                        (("1"
                                          (expand "image")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (inst -4 "x!1")
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (rewrite "down_up")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (skosimp)
                                    (("2"
                                      (case-replace "r!1=bottom")
                                      (("1"
                                        (hide 1 -1)
                                        (("1"
                                          (expand "nonempty?")
                                          (("1"
                                            (expand "empty?")
                                            (("1"
                                              (skosimp)
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (inst - "up(x!1)")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil)
                                                     ("2"
                                                      (expand "image")
                                                      (("2"
                                                        (inst + "x!1")
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (assert)
                                        (("2"
                                          (inst -5 "down(r!1)")
                                          (("2"
                                            (assert)
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (typepred "r!2")
                                                (("2"
                                                  (inst -2 "up(r!2)")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil)
                                                   ("2"
                                                    (expand "image")
                                                    (("2"
                                                      (inst + "r!2")
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "nonempty?")
            (("2" (inst + "bottom")
              (("2" (hide -2)
                (("2" (expand "least_upper_bound?")
                  (("2" (expand "upper_bound?")
                    (("2" (expand "lift")
                      (("2" (skosimp)
                        (("2" (typepred "r!1")
                          (("2" (expand "image")
                            (("2" (skosimp)
                              (("2"
                                (typepred "x!1")
                                (("2"
                                  (expand "empty?")
                                  (("2"
                                    (inst - "x!1")
                                    (("2"
                                      (expand "member")
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              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)
    (nonempty_least_bounded_above? const-decl "bool" bounded_orders
     nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil lifted_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty? const-decl "bool" sets nil)
    (lift const-decl "bool" lifted_orders nil)
    (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (lift type-decl nil lift_adt nil)
    (down_up formula-decl nil lift_props nil)
    (image const-decl "set[R]" function_image nil)
    (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
    (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (x!1 skolem-const-decl "T" lifted_orders nil)
    (S!1 skolem-const-decl "(nonempty_least_bounded_above?[T](rel!1))"
     lifted_orders nil)
    (rel!1 skolem-const-decl "(antisymmetric?[T])" lifted_orders nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (every adt-def-decl "boolean" lift_adt nil)
    (r!2 skolem-const-decl "(S!1)" lifted_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil))
   nil))
(lift_lub_bounded_TCC2 0
  (lift_lub_bounded_TCC2-1 nil 3353301987 ("" (subtype-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)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (nonempty_least_bounded_above? const-decl "bool" bounded_orders
     nil)
    (nonempty? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (T formal-type-decl nil lifted_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil))
   nil))
(lift_lub_bounded 0
  (lift_lub_bounded-1 nil 3353301377
   ("" (skosimp)
    (("" (lemma "lift_lub_bounded_TCC1" ("rel" "rel!1" "S" "S!1"))
      (("" (typepred "lub(lift(rel!1))(image[T, lift[T]](up, S!1))")
        ((""
          (name-replace "LUBL"
           "lub(lift(rel!1))(image[T, lift[T]](up, S!1))")
          (("" (typepred "S!1")
            (("" (typepred "lub(rel!1)(S!1)")
              (("" (name-replace "LUB" "lub(rel!1)(S!1)")
                (("" (hide -2 -4)
                  (("" (expand "least_upper_bound?")
                    (("" (flatten)
                      (("" (inst -4 "up(LUB)")
                        (("" (expand "upper_bound?")
                          (("" (expand "lift")
                            (("" (split -4)
                              (("1"
                                (typepred "S!1")
                                (("1"
                                  (expand
                                   "nonempty_least_bounded_above?")
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (hide-all-but (-1 1 -5))
                                      (("1"
                                        (expand "nonempty?")
                                        (("1"
                                          (expand "empty?")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (expand "member")
                                              (("1"
                                                (inst - "up(x!1)")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (expand "image")
                                                  (("2"
                                                    (inst + "x!1")
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (inst -3 "down(LUBL)")
                                (("2"
                                  (split -3)
                                  (("1"
                                    (typepred "rel!1")
                                    (("1"
                                      (expand "antisymmetric?")
                                      (("1"
                                        (inst - "LUB" "down(LUBL)")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (replace -1)
                                            (("1"
                                              (typepred "S!1")
                                              (("1"
                                                (expand
                                                 "nonempty_least_bounded_above?")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (expand
                                                     "nonempty?")
                                                    (("1"
                                                      (expand "empty?")
                                                      (("1"
                                                        (skosimp)
                                                        (("1"
                                                          (expand
                                                           "member")
                                                          (("1"
                                                            (inst-cp
                                                             -7
                                                             "up(x!1)")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (flatten)
                                                                (("1"
                                                                  (hide
                                                                   -1
                                                                   -2
                                                                   -9)
                                                                  (("1"
                                                                    (lemma
                                                                     "up_down"
                                                                     ("y"
                                                                      "LUBL"))
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "image")
                                                              (("2"
                                                                (inst
                                                                 +
                                                                 "x!1")
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (skosimp)
                                    (("2"
                                      (typepred "r!1")
                                      (("2"
                                        (hide 2 -2 -3)
                                        (("2"
                                          (inst - "up(r!1)")
                                          (("1" (assert) nil nil)
                                           ("2"
                                            (expand "image")
                                            (("2"
                                              (inst + "r!1")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (skosimp)
                                (("3"
                                  (typepred "r!1")
                                  (("3"
                                    (expand "image")
                                    (("3"
                                      (skosimp)
                                      (("3"
                                        (replace -1)
                                        (("3"
                                          (rewrite "down_up")
                                          (("3"
                                            (typepred "x!1")
                                            (("3"
                                              (inst -4 "x!1")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty_least_bounded_above? const-decl "bool" bounded_orders
     nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil lifted_orders nil)
    (lift_lub_bounded_TCC1 subtype-tcc nil lifted_orders nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (x!1 skolem-const-decl "T" lifted_orders nil)
    (S!1 skolem-const-decl "(nonempty_least_bounded_above?(rel!1))"
     lifted_orders nil)
    (rel!1 skolem-const-decl "(antisymmetric?[T])" lifted_orders nil)
    (nonempty? const-decl "bool" sets nil)
    (up_down formula-decl nil lift_props nil)
    (x!1 skolem-const-decl "T" lifted_orders nil)
    (r!1 skolem-const-decl "(S!1)" lifted_orders nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (down_up formula-decl nil lift_props nil)
    (every adt-def-decl "boolean" lift_adt nil)
    (lift_preserves_antisymmetric application-judgement
     "(antisymmetric?[lift[T]])" lifted_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (lift type-decl nil lift_adt nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
     bounded_orders nil)
    (lift const-decl "bool" lifted_orders nil)
    (image const-decl "set[R]" function_image nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (up adt-constructor-decl "[T -> (up?)]" lift_adt nil))
   shostak))
(lift_preserves_directed_complete 0
  (lift_preserves_directed_complete-1 nil 3353157533
   ("" (skosimp)
    (("" (typepred "r!1")
      (("" (expand "lift")
        (("" (expand "directed_complete?")
          (("" (skosimp*)
            (("" (expand "least_bounded_above?")
              (("" (typepred "D!1")
                (("" (name "DD" "{x:T | EXISTS (z:(D!1)): z = up(x)}")
                  (("" (case "nonempty?(DD)")
                    (("1" (inst -6 "DD")
                      (("1" (skosimp)
                        (("1" (inst + "up(t!1)")
                          (("1" (expand "least_upper_bound?")
                            (("1" (flatten)
                              (("1"
                                (split)
                                (("1"
                                  (hide -7)
                                  (("1"
                                    (expand "upper_bound?")
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (typepred "r!2")
                                        (("1"
                                          (inst -8 "down(r!2)")
                                          (("1"
                                            (expand "DD")
                                            (("1"
                                              (inst + "r!2")
                                              (("1"
                                                (lemma
                                                 "up_down"
                                                 ("y" "r!2"))
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skosimp)
                                  (("2"
                                    (case-replace "r!2=bottom")
                                    (("1"
                                      (hide -8 -9 1 -6 -4 -1)
                                      (("1"
                                        (expand "upper_bound?")
                                        (("1"
                                          (expand "nonempty?" -2)
                                          (("1"
                                            (expand "empty?")
                                            (("1"
                                              (skosimp)
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (expand "DD")
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (inst - "z!1")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (inst -8 "down(r!2)")
                                        (("2"
                                          (split -8)
                                          (("1" (propax) nil nil)
                                           ("2"
                                            (expand "upper_bound?")
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (typepred "r!3")
                                                (("2"
                                                  (expand "DD")
                                                  (("2"
                                                    (skosimp)
                                                    (("2"
                                                      (typepred "z!1")
                                                      (("2"
                                                        (inst -3 "z!1")
                                                        (("2"
                                                          (assert)
                                                          (("2"
                                                            (replace
                                                             -2)
                                                            (("2"
                                                              (rewrite
                                                               "down_up")
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert)
                        (("2" (hide 2)
                          (("2" (expand "directed?")
                            (("2" (skosimp)
                              (("2"
                                (expand "DD")
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (inst - "up(x!1)" "up(y!1)")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (inst + "down(z!3)")
                                          (("1" (assert) nil nil)
                                           ("2"
                                            (expand "DD")
                                            (("2"
                                              (inst + "z!3")
                                              (("2"
                                                (lemma
                                                 "up_down"
                                                 ("y" "z!3"))
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "nonempty?" 1)
                      (("2" (expand "empty?")
                        (("2" (expand "member")
                          (("2" (expand "DD" -1)
                            (("2" (inst + "bottom")
                              (("2"
                                (expand "least_upper_bound?")
                                (("2"
                                  (expand "upper_bound?")
                                  (("2"
                                    (skosimp)
                                    (("2"
                                      (typepred "r!2")
                                      (("2"
                                        (lemma "up_down" ("y" "r!2"))
                                        (("2"
                                          (assert)
                                          (("2"
                                            (inst -3 "down(r!2)")
                                            (("2"
                                              (inst + "r!2")
                                              (("2" (assert) 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_complete? const-decl "bool" directed_orders nil)
    (partial_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil lifted_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (DD skolem-const-decl "[T -> boolean]" lifted_orders nil)
    (r!1 skolem-const-decl "(directed_complete?[T])" lifted_orders nil)
    (down_up formula-decl nil lift_props nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
    (D!1 skolem-const-decl "(directed?(LAMBDA (x, y):
             (NOT up?(x)) OR (up?(y) AND r!1(down(x), down(y)))))"
     lifted_orders nil)
    (r!2 skolem-const-decl "(D!1)" lifted_orders nil)
    (up_down formula-decl nil lift_props nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (z!3 skolem-const-decl "(D!1)" lifted_orders nil)
    (lift type-decl nil lift_adt nil) (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (directed? const-decl "bool" directed_orders nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (lift const-decl "bool" lifted_orders nil))
   nil))
(lift_preserves_directed_complete_partial_order 0
  (lift_preserves_directed_complete_partial_order-1 nil 3353157533
   ("" (skosimp)
    (("" (typepred "r!1")
      (("" (expand "pointed_directed_complete_partial_order?")
        (("" (split)
          (("1" (lemma "lift_preserves_directed_complete" ("r" "r!1"))
            (("1" (lemma "lift_preserves_partial_order" ("r" "r!1"))
              (("1" (expand "directed_complete_partial_order?")
                (("1" (propax) nil nil)) nil))
              nil)
             ("2" (expand "directed_complete_partial_order?")
              (("2" (flatten) nil nil)) nil))
            nil)
           ("2" (expand "fullset")
            (("2" (expand "lift")
              (("2" (expand "has_least?")
                (("2" (inst + "bottom")
                  (("2" (expand "least?")
                    (("2" (expand "lower_bound?")
                      (("2" (propax) nil nil)) nil))
                    nil))
                  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)
    (T formal-type-decl nil lifted_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (lift_preserves_partial_order judgement-tcc nil lifted_orders nil)
    (lift_preserves_directed_complete judgement-tcc nil lifted_orders
     nil)
    (partial_order? const-decl "bool" orders nil)
    (directed_complete? const-decl "bool" directed_orders nil)
    (lift const-decl "bool" lifted_orders nil)
    (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
    (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (lift type-decl nil lift_adt nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (fullset const-decl "set" sets nil)
    (pointed_directed_complete_partial_order? const-decl "bool"
     directed_orders nil)
    (lift_preserves_partial_order application-judgement
     "(partial_order?[lift[T]])" lifted_orders nil))
   nil)))

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