products/sources/formale Sprachen/Coq/theories/Init image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: wg_ScriptView.mli   Sprache: Scala

Original von: PVS©

(pointwise_orders
 (pointwise_preserves_reflexive 0
  (pointwise_preserves_reflexive-1 nil 3314638777
   ("" (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)
    (R formal-type-decl nil pointwise_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (D formal-type-decl nil pointwise_orders nil)
    (pointwise const-decl "bool" pointwise_orders nil)
    (reflexive? const-decl "bool" relations nil))
   nil))
 (pointwise_preserves_transitive 0
  (pointwise_preserves_transitive-1 nil 3314638777
   ("" (skolem-typepred)
    (("" (expand"transitive?" "pointwise")
      (("" (skosimp*)
        (("" (inst - "x!1(x!2)" "y!1(x!2)" "z!1(x!2)")
          (("" (inst?) (("" (inst?) (("" (assertnil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((pointwise const-decl "bool" pointwise_orders nil)
    (D formal-type-decl nil pointwise_orders nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (R formal-type-decl nil pointwise_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (pointwise_preserves_preorder 0
  (pointwise_preserves_preorder-1 nil 3314638777
   ("" (judgement-tcc) nil nil)
   ((pointwise_preserves_transitive application-judgement
     "(transitive?[[D -> R]])" pointwise_orders nil)
    (pointwise_preserves_reflexive application-judgement
     "(reflexive?[[D -> R]])" pointwise_orders nil)
    (preorder? const-decl "bool" orders nil))
   nil))
 (pointwise_preserves_antisymmetric 0
  (pointwise_preserves_antisymmetric-1 nil 3314638777
   ("" (skolem-typepred)
    (("" (expand"antisymmetric?" "pointwise")
      (("" (skosimp*)
        (("" (decompose-equality)
          (("" (inst?)
            (("" (inst?) (("" (inst?) (("" (assertnil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pointwise const-decl "bool" pointwise_orders nil)
    (D formal-type-decl nil pointwise_orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (R formal-type-decl nil pointwise_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (pointwise_preserves_partial_order 0
  (pointwise_preserves_partial_order-1 nil 3314638777
   ("" (judgement-tcc) nil nil)
   ((pointwise_preserves_antisymmetric application-judgement
     "(antisymmetric?[[D -> R]])" pointwise_orders nil)
    (pointwise_preserves_preorder application-judgement
     "(preorder?[[D -> R]])" pointwise_orders nil)
    (partial_order? const-decl "bool" orders nil))
   nil))
 (finiteness_lemma 0
  (finiteness_lemma-1 nil 3314639098
   ("" (skolem!)
    (("" (split)
      (("1" (typepred "nff!1")
        (("1" (expand"nonempty?" "empty?" "member")
          (("1" (skolem!)
            (("1" (inst - "x!2(x!1)") (("1" (inst?) nil nil)) nil))
            nil))
          nil))
        nil)
       ("2"
        (case-replace
         "{s | EXISTS f: nff!1(f) & s = f(x!1)} = image(LAMBDA f: f(x!1), nff!1)")
        (("1" (rewrite "finite_image"nil nil)
         ("2" (hide 2)
          (("2" (decompose-equality)
            (("2" (expand "image")
              (("2" (iff)
                (("2" (prop)
                  (("1" (skosimp* t) (("1" (inst?) nil nil)) nil)
                   ("2" (skolem-typepred)
                    (("2" (inst?) (("2" (assertnil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (D formal-type-decl nil pointwise_orders nil)
    (R formal-type-decl nil pointwise_orders nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (f!1 skolem-const-decl "[D -> R]" pointwise_orders nil)
    (nff!1 skolem-const-decl "non_empty_finite_set[[D -> R]]"
     pointwise_orders nil)
    (finite_image judgement-tcc nil function_image_aux nil)
    (image const-decl "set[R]" function_image nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_image application-judgement "finite_set[R]"
     function_image_aux nil))
   shostak))
 (least_upper_bound_pointwise 0
  (least_upper_bound_pointwise-1 nil 3314639347
   ("" (skolem!)
    (("" (prop)
      (("1" (skolem!)
        (("1" (expand "least_upper_bound?")
          (("1" (prop)
            (("1" (hide -2)
              (("1" (expand "upper_bound?")
                (("1" (skosimp* t)
                  (("1" (inst?)
                    (("1" (expand "pointwise")
                      (("1" (inst?) (("1" (assertnil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp)
              (("2"
                (inst -
                 "LAMBDA x: IF x = x!1 THEN r!1 ELSE f1!1(x) ENDIF")
                (("2" (split)
                  (("1" (expand "pointwise" -1) (("1" (inst?) nil nil))
                    nil)
                   ("2" (expand "upper_bound?")
                    (("2" (skolem-typepred)
                      (("2" (inst? -3)
                        (("2" (inst - "r!2(x!1)")
                          (("1" (expand "pointwise")
                            (("1" (skolem!)
                              (("1"
                                (lift-if)
                                (("1"
                                  (prop)
                                  (("1" (assertnil nil)
                                   ("2" (inst?) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (inst?) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "least_upper_bound?" +)
        (("2" (split)
          (("1"
            (expand"pointwise" "least_upper_bound?" "upper_bound?")
            (("1" (skosimp* t)
              (("1" (inst?)
                (("1" (flatten)
                  (("1" (inst?) (("1" (inst? +) nil nil)) nil)) nil))
                nil))
              nil))
            nil)
           ("2" (expand "pointwise" + :occurrence 2)
            (("2" (skosimp*)
              (("2" (inst?)
                (("2" (expand "least_upper_bound?")
                  (("2" (flatten)
                    (("2" (hide -2)
                      (("2" (inst?)
                        (("2" (assert)
                          (("2" (expand "upper_bound?")
                            (("2" (skosimp* t)
                              (("2"
                                (inst?)
                                (("2"
                                  (expand "pointwise")
                                  (("2"
                                    (inst?)
                                    (("2" (assertnil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((least_upper_bound? const-decl "bool" bounded_orders nil)
    (x!1 skolem-const-decl "D" pointwise_orders nil)
    (r!2 skolem-const-decl "(ff!1)" pointwise_orders nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (R formal-type-decl nil pointwise_orders nil)
    (D formal-type-decl nil pointwise_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (pointwise const-decl "bool" pointwise_orders nil)
    (f!1 skolem-const-decl "[D -> R]" pointwise_orders nil)
    (ff!1 skolem-const-decl "set[[D -> R]]" pointwise_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (r!1 skolem-const-decl "(ff!1)" pointwise_orders nil)
    (x!1 skolem-const-decl "D" pointwise_orders nil)
    (f!1 skolem-const-decl "[D -> R]" pointwise_orders nil))
   shostak))
 (least_bounded_above_pointwise 0
  (least_bounded_above_pointwise-1 nil 3314640074
   ("" (skolem!)
    (("" (expand "least_bounded_above?")
      (("" (prop)
        (("1" (skosimp*)
          (("1" (inst + "t!1(x!1)")
            (("1" (rewrite "least_upper_bound_pointwise")
              (("1" (inst?) nil nil)) nil))
            nil))
          nil)
         ("2" (rewrite "skolemize_exists")
          (("2" (skolem!)
            (("2" (use "least_upper_bound_pointwise")
              (("2" (replace*)
                (("2" (assert) (("2" (inst?) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((least_bounded_above? const-decl "bool" bounded_orders nil)
    (skolemize_exists formula-decl nil skolemization nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (least_upper_bound_pointwise formula-decl nil pointwise_orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (D formal-type-decl nil pointwise_orders nil)
    (R formal-type-decl nil pointwise_orders nil))
   shostak))
 (pointwise_preserves_upper_semilattices 0
  (pointwise_preserves_upper_semilattices-1 nil 3314638777
   ("" (expand "upper_semilattice?")
    (("" (skosimp* t)
      (("" (rewrite "least_bounded_above_pointwise")
        (("" (skolem!)
          (("" (rewrite "all_finite_least_bounded")
            (("" (use "finiteness_lemma")
              (("" (expand "nonempty?") (("" (prop) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pred type-eq-decl nil defined_types nil)
    (R formal-type-decl nil pointwise_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (D formal-type-decl nil pointwise_orders nil)
    (finiteness_lemma formula-decl nil pointwise_orders nil)
    (nonempty? const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (all_finite_least_bounded formula-decl nil bounded_orders nil)
    (least_bounded_above_pointwise formula-decl nil pointwise_orders
     nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (pointwise_preserves_partial_order application-judgement
     "(partial_order?[[D -> R]])" pointwise_orders nil))
   nil))
 (pointwise_preserves_complete_upper_semilattices 0
  (pointwise_preserves_complete_upper_semilattices-1 nil 3314638777
   ("" (expand "complete_upper_semilattice?")
    (("" (skolem-typepred)
      (("" (rewrite "pointwise_preserves_partial_order")
        (("" (skolem!)
          (("" (rewrite "least_bounded_above_pointwise")
            (("" (skolem!) (("" (rewrite "all_least_bounded"nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (R formal-type-decl nil pointwise_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (all_least_bounded formula-decl nil bounded_orders nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (least_bounded_above_pointwise formula-decl nil pointwise_orders
     nil)
    (D formal-type-decl nil pointwise_orders nil)
    (set type-eq-decl nil sets nil)
    (partial_order? const-decl "bool" orders nil)
    (pointwise_preserves_partial_order judgement-tcc nil
     pointwise_orders nil)
    (complete_upper_semilattice? const-decl "bool" bounded_orders nil)
    (pointwise_preserves_upper_semilattices application-judgement
     "(upper_semilattice?[[D -> R]])" pointwise_orders nil))
   nil))
 (greatest_lower_bound_pointwise 0
  (greatest_lower_bound_pointwise-1 nil 3314640323
   ("" (skolem!)
    (("" (prop)
      (("1" (skolem!)
        (("1" (expand "greatest_lower_bound?")
          (("1" (prop)
            (("1" (hide -2)
              (("1" (expand"lower_bound?" "pointwise")
                (("1" (skosimp* t)
                  (("1" (inst?) (("1" (assertnil nil)) nil)) nil))
                nil))
              nil)
             ("2" (skosimp)
              (("2"
                (inst -
                 "LAMBDA x: IF x = x!1 THEN r!1 ELSE f1!1(x) ENDIF")
                (("2" (split)
                  (("1" (expand "pointwise" -1) (("1" (inst?) nil nil))
                    nil)
                   ("2" (expand "lower_bound?")
                    (("2" (skolem-typepred)
                      (("2" (inst? -3)
                        (("2" (inst - "r!2(x!1)")
                          (("1" (expand "pointwise")
                            (("1" (skolem!)
                              (("1"
                                (lift-if)
                                (("1"
                                  (ground)
                                  (("1" (inst?) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (inst?) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "greatest_lower_bound?" +)
        (("2" (split)
          (("1"
            (expand"greatest_lower_bound?" "lower_bound?"
             "pointwise")
            (("1" (skosimp* t)
              (("1" (inst?)
                (("1" (flatten)
                  (("1" (inst?) (("1" (inst? +) nil nil)) nil)) nil))
                nil))
              nil))
            nil)
           ("2" (expand "pointwise" + :occurrence 2)
            (("2" (skosimp*)
              (("2" (inst?)
                (("2" (expand "greatest_lower_bound?")
                  (("2" (flatten)
                    (("2" (hide -2)
                      (("2" (inst?)
                        (("2" (assert)
                          (("2" (expand "lower_bound?")
                            (("2" (skosimp* t)
                              (("2"
                                (inst?)
                                (("2"
                                  (expand "pointwise")
                                  (("2"
                                    (inst?)
                                    (("2" (assertnil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (x!1 skolem-const-decl "D" pointwise_orders nil)
    (r!2 skolem-const-decl "(ff!1)" pointwise_orders nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (R formal-type-decl nil pointwise_orders nil)
    (D formal-type-decl nil pointwise_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (f!1 skolem-const-decl "[D -> R]" pointwise_orders nil)
    (ff!1 skolem-const-decl "set[[D -> R]]" pointwise_orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (pointwise const-decl "bool" pointwise_orders nil)
    (r!1 skolem-const-decl "(ff!1)" pointwise_orders nil)
    (x!1 skolem-const-decl "D" pointwise_orders nil)
    (f!1 skolem-const-decl "[D -> R]" pointwise_orders nil))
   shostak))
 (greatest_bounded_below_pointwise 0
  (greatest_bounded_below_pointwise-1 nil 3314640605
   ("" (skolem!)
    (("" (expand "greatest_bounded_below?")
      (("" (prop)
        (("1" (skosimp*)
          (("1" (inst + "t!1(x!1)")
            (("1" (rewrite "greatest_lower_bound_pointwise")
              (("1" (inst?) nil nil)) nil))
            nil))
          nil)
         ("2" (rewrite "skolemize_exists")
          (("2" (skolem!)
            (("2" (use "greatest_lower_bound_pointwise")
              (("2" (replace*)
                (("2" (assert) (("2" (inst?) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (skolemize_exists formula-decl nil skolemization nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pointwise_preserves_antisymmetric application-judgement
     "(antisymmetric?[[D -> R]])" pointwise_orders nil)
    (greatest_lower_bound_pointwise formula-decl nil pointwise_orders
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (D formal-type-decl nil pointwise_orders nil)
    (R formal-type-decl nil pointwise_orders nil))
   shostak))
 (pointwise_preserves_lower_semilattices 0
  (pointwise_preserves_lower_semilattices-1 nil 3314638777
   ("" (expand "lower_semilattice?")
    (("" (skosimp* t)
      (("" (rewrite "greatest_bounded_below_pointwise")
        (("" (skolem!)
          (("" (rewrite "all_finite_greatest_bounded")
            (("" (use "finiteness_lemma")
              (("" (expand "nonempty?") (("" (prop) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pred type-eq-decl nil defined_types nil)
    (R formal-type-decl nil pointwise_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (D formal-type-decl nil pointwise_orders nil)
    (finiteness_lemma formula-decl nil pointwise_orders nil)
    (nonempty? const-decl "bool" sets nil)
    (all_finite_greatest_bounded formula-decl nil bounded_orders nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (greatest_bounded_below_pointwise formula-decl nil pointwise_orders
     nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (pointwise_preserves_partial_order application-judgement
     "(partial_order?[[D -> R]])" pointwise_orders nil))
   nil))
 (pointwise_preserves_complete_lower_semilattices 0
  (pointwise_preserves_complete_lower_semilattices-1 nil 3314638777
   ("" (expand "complete_lower_semilattice?")
    (("" (skolem-typepred)
      (("" (rewrite "pointwise_preserves_partial_order")
        (("" (skolem!)
          (("" (rewrite "greatest_bounded_below_pointwise")
            (("" (skolem!)
              (("" (rewrite "all_greatest_bounded"nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (R formal-type-decl nil pointwise_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (all_greatest_bounded formula-decl nil bounded_orders nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (D formal-type-decl nil pointwise_orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (greatest_bounded_below_pointwise formula-decl nil pointwise_orders
     nil)
    (partial_order? const-decl "bool" orders nil)
    (pointwise_preserves_partial_order judgement-tcc nil
     pointwise_orders nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (pointwise_preserves_lower_semilattices application-judgement
     "(lower_semilattice?[[D -> R]])" pointwise_orders nil))
   nil))
 (pointwise_preserves_lattices 0
  (pointwise_preserves_lattices-1 nil 3314638777
   ("" (judgement-tcc) nil nil)
   ((pointwise_preserves_upper_semilattices application-judgement
     "(upper_semilattice?[[D -> R]])" pointwise_orders nil)
    (pointwise_preserves_lower_semilattices application-judgement
     "(lower_semilattice?[[D -> R]])" pointwise_orders nil)
    (lattice? const-decl "bool" bounded_orders nil))
   nil))
 (pointwise_preserves_complete_lattices 0
  (pointwise_preserves_complete_lattices-1 nil 3314638777
   ("" (judgement-tcc) nil nil)
   ((pointwise_preserves_complete_upper_semilattices
     application-judgement "(complete_upper_semilattice?[[D -> R]])"
     pointwise_orders nil)
    (pointwise_preserves_lattices application-judgement
     "(lattice?[[D -> R]])" pointwise_orders nil)
    (pointwise_preserves_complete_lower_semilattices
     application-judgement "(complete_lower_semilattice?[[D -> R]])"
     pointwise_orders nil)
    (complete_lattice? const-decl "bool" bounded_orders nil))
   nil))
 (lub_pointwise_def_TCC1 0
  (lub_pointwise_def_TCC1-1 nil 3314638777
   ("" (skosimp)
    (("" (rewrite "least_bounded_above_pointwise"nil nil)) nil)
   ((least_bounded_above_pointwise formula-decl nil pointwise_orders
     nil)
    (D formal-type-decl nil pointwise_orders nil)
    (R formal-type-decl nil pointwise_orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil))
   nil))
 (lub_pointwise_def_TCC2 0
  (lub_pointwise_def_TCC2-1 nil 3314638777 ("" (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)
    (R formal-type-decl nil pointwise_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations 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))
 (lub_pointwise_def 0
  (lub_pointwise_def-1 nil 3314640889
   ("" (skosimp)
    (("" (invoke (name-replace "L" "%1" :hide? nil) (! 1 2))
      (("" (rewrite "lub_def[[D -> R]]")
        (("" (rewrite "least_upper_bound_pointwise")
          (("" (skolem!)
            (("" (decompose-equality)
              (("" (inst?) (("" (rewrite "lub_def[R]"nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
     bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (R formal-type-decl nil pointwise_orders nil)
    (D formal-type-decl nil pointwise_orders nil)
    (least_upper_bound_pointwise formula-decl nil pointwise_orders nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pointwise const-decl "bool" pointwise_orders nil)
    (lub_def formula-decl nil bounded_orders nil)
    (pointwise_preserves_antisymmetric application-judgement
     "(antisymmetric?[[D -> R]])" pointwise_orders nil))
   shostak))
 (glb_pointwise_def_TCC1 0
  (glb_pointwise_def_TCC1-1 nil 3314638777
   ("" (skosimp)
    (("" (rewrite "greatest_bounded_below_pointwise"nil nil)) nil)
   ((greatest_bounded_below_pointwise formula-decl nil pointwise_orders
     nil)
    (R formal-type-decl nil pointwise_orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (D formal-type-decl nil pointwise_orders nil)
    (set type-eq-decl nil sets nil))
   nil))
 (glb_pointwise_def_TCC2 0
  (glb_pointwise_def_TCC2-1 nil 3314638777 ("" (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)
    (R formal-type-decl nil pointwise_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil))
   nil))
 (glb_pointwise_def 0
  (glb_pointwise_def-1 nil 3314641025
   ("" (skosimp)
    (("" (invoke (name-replace "L" "%1" :hide? nil) (! 1 2))
      (("" (rewrite "glb_def[[D -> R]]")
        (("" (rewrite "greatest_lower_bound_pointwise")
          (("" (skolem!)
            (("" (decompose-equality)
              (("" (inst?) (("" (rewrite "glb_def[R]"nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (R formal-type-decl nil pointwise_orders nil)
    (D formal-type-decl nil pointwise_orders nil)
    (greatest_lower_bound_pointwise formula-decl nil pointwise_orders
     nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pointwise const-decl "bool" pointwise_orders nil)
    (glb_def formula-decl nil bounded_orders nil)
    (pointwise_preserves_antisymmetric application-judgement
     "(antisymmetric?[[D -> R]])" pointwise_orders nil))
   shostak)))


¤ Dauer der Verarbeitung: 0.89 Sekunden  (vorverarbeitet)  ¤





Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff