Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: class_equation_scaf.prf Sprache: Lisp

Original von: PVS^©

(partial_order_props
(partial_order_reflexive 0
  (partial_order_reflexive-1 nil 3352693343
   ("" (typepred "<=")
    (("" (expand "partial_order?")
      (("" (expand "preorder?")
        (("" (expand "reflexive?") (("" (flatten) nil nil)) nil)) nil))
      nil))
    nil)
   ((reflexive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders 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 partial_order_props nil)
    (pred type-eq-decl nil defined_types nil)
    (partial_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(partial_order?[T])" partial_order_props
        nil))
   shostak))
(partial_order_antisymmetric 0
  (partial_order_antisymmetric-1 nil 3352693360
   ("" (typepred "<=")
    (("" (expand "partial_order?")
      (("" (expand "preorder?")
        (("" (flatten)
          (("" (expand "antisymmetric?") (("" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((antisymmetric? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders 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 partial_order_props nil)
    (pred type-eq-decl nil defined_types nil)
    (partial_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(partial_order?[T])" partial_order_props
        nil))
   shostak))
(partial_order_transitive 0
  (partial_order_transitive-1 nil 3352693400
   ("" (typepred "<=")
    (("" (expand "partial_order?")
      (("" (expand "preorder?")
        (("" (flatten)
          (("" (expand "transitive?") (("" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((transitive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders 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 partial_order_props nil)
    (pred type-eq-decl nil defined_types nil)
    (partial_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(partial_order?[T])" partial_order_props
        nil))
   shostak))
(lower_set_TCC1 0
  (lower_set_TCC1-1 nil 3330491210 ("" (grind) nil nil)
   ((emptyset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (lower_set? const-decl "bool" partial_order_props nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   shostak))
(upper_set_TCC1 0
  (upper_set_TCC1-1 nil 3330491210 ("" (grind) nil nil)
   ((emptyset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (upper_set? const-decl "bool" partial_order_props nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   shostak))
(lower_sets_TCC1 0
  (lower_sets_TCC1-1 nil 3330495937
   ("" (expand "lower_sets?")
    (("" (expand "every")
      (("" (skosimp)
        (("" (typepred "x!1")
          (("" (expand "emptyset") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((every const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (lower_sets? const-decl "bool" partial_order_props nil))
   shostak))
(upper_sets_TCC1 0
  (upper_sets_TCC1-1 nil 3330495937
   ("" (expand "upper_sets?")
    (("" (expand "every")
      (("" (skosimp)
        (("" (typepred "x!1")
          (("" (expand "emptyset") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((every const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (upper_sets? const-decl "bool" partial_order_props nil))
   shostak))
(complement_lower_set 0
  (complement_lower_set-1 nil 3330492744
   ("" (skosimp)
    (("" (typepred "L!1")
      (("" (expand "complement")
        (("" (expand "upper_set?")
          (("" (expand "lower_set?")
            (("" (skosimp)
              (("" (expand "member")
                (("" (inst - "y!1" "x!1") (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_set nonempty-type-eq-decl nil partial_order_props nil)
    (lower_set? const-decl "bool" partial_order_props nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (upper_set? const-decl "bool" partial_order_props nil)
    (member const-decl "bool" sets nil)
    (complement const-decl "set" sets nil))
   shostak))
(complement_upper_set 0
  (complement_upper_set-1 nil 3330492800
   ("" (skosimp)
    (("" (typepred "U!1")
      (("" (expand "upper_set?")
        (("" (expand "lower_set?")
          (("" (expand "complement")
            (("" (expand "member")
              (("" (skosimp*)
                (("" (inst - "y!1" "x!1")
                  (("" (replace -2) (("" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_set nonempty-type-eq-decl nil partial_order_props nil)
    (upper_set? const-decl "bool" partial_order_props nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (lower_set? const-decl "bool" partial_order_props nil)
    (member const-decl "bool" sets nil)
    (complement const-decl "set" sets nil))
   shostak))
(Complement_lower_sets 0
  (Complement_lower_sets-1 nil 3330512630
   ("" (skosimp)
    (("" (typepred "LS!1")
      (("" (expand "Complement")
        (("" (expand "upper_sets?")
          (("" (expand "lower_sets?")
            (("" (expand "every")
              (("" (skosimp)
                (("" (typepred "x!1")
                  (("" (skosimp)
                    (("" (inst - "b!1")
                      (("" (assert)
                        (("" (replace -1)
                          (("" (rewrite "complement_lower_set") nil
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_sets nonempty-type-eq-decl nil partial_order_props nil)
    (lower_sets? const-decl "bool" partial_order_props nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (upper_sets? const-decl "bool" partial_order_props nil)
    (every const-decl "bool" sets nil)
    (complement const-decl "set" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (complement_lower_set judgement-tcc nil partial_order_props nil)
    (lower_set? const-decl "bool" partial_order_props nil)
    (lower_set nonempty-type-eq-decl nil partial_order_props nil)
    (Complement const-decl "setofsets[T]" sets_lemmas nil))
   shostak))
(Complement_upper_sets 0
  (Complement_upper_sets-1 nil 3330512736
   ("" (skosimp)
    (("" (typepred "US!1")
      (("" (expand "upper_sets?")
        (("" (expand "Complement")
          (("" (expand "lower_sets?")
            (("" (expand "every")
              (("" (skosimp)
                (("" (typepred "x!1")
                  (("" (skosimp)
                    (("" (replace -1)
                      (("" (inst - "b!1")
                        (("" (rewrite "complement_upper_set") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_sets nonempty-type-eq-decl nil partial_order_props nil)
    (upper_sets? const-decl "bool" partial_order_props nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Complement const-decl "setofsets[T]" sets_lemmas nil)
    (every const-decl "bool" sets nil)
    (complement const-decl "set" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (upper_set nonempty-type-eq-decl nil partial_order_props nil)
    (upper_set? const-decl "bool" partial_order_props nil)
    (complement_upper_set judgement-tcc nil partial_order_props nil)
    (lower_sets? const-decl "bool" partial_order_props nil))
   shostak))
(down_TCC1 0
  (down_TCC1-1 nil 3352692970
   ("" (expand "lower_set?")
    (("" (expand "member")
      (("" (skosimp*)
        (("" (assert)
          ((""
            (lemma "partial_order_transitive"
             ("x" "y!1" "y" "x!2" "z" "x!1"))
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (partial_order_transitive formula-decl nil partial_order_props nil)
    (T formal-type-decl nil partial_order_props nil)
    (lower_set? const-decl "bool" partial_order_props nil))
   nil))
(up_TCC1 0
  (up_TCC1-1 nil 3352692970 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (partial_order_transitive formula-decl nil partial_order_props nil)
    (upper_set? const-decl "bool" partial_order_props nil))
   nil))
(down_subset 0
  (down_subset-1 nil 3330493353
   ("" (expand "down")
    (("" (expand "subset?")
      (("" (expand "member")
        (("" (skosimp*)
          (("" (assert)
            ((""
              (lemma "partial_order_transitive"
               ("x" "x!2" "y" "x!1" "z" "y!1"))
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (partial_order_transitive formula-decl nil partial_order_props nil)
    (T formal-type-decl nil partial_order_props nil)
    (member const-decl "bool" sets nil)
    (down const-decl "lower_set" partial_order_props nil))
   shostak))
(up_subset 0
  (up_subset-1 nil 3330493409
   ("" (expand "up")
    (("" (expand "subset?")
      (("" (expand "member")
        (("" (skosimp*)
          ((""
            (lemma "partial_order_transitive"
             ("x" "x!1" "y" "y!1" "z" "x!2"))
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (T formal-type-decl nil partial_order_props nil)
    (partial_order_transitive formula-decl nil partial_order_props nil)
    (member const-decl "bool" sets nil)
    (up const-decl "upper_set" partial_order_props nil))
   shostak))
(lower_set_def 0
  (lower_set_def-1 nil 3330493656
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (apply-extensionality :hide? t)
          (("1" (case-replace "S!1(x!1)")
            (("1" (expand "Union")
              (("1" (inst + "down(x!1)")
                (("1" (expand "down") (("1" (assert) nil nil)) nil)
                 ("2" (expand "image")
                  (("2" (expand "extend")
                    (("2" (inst + "x!1") nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (expand "Union")
                (("2" (skosimp)
                  (("2" (typepred "a!1")
                    (("2" (expand "extend")
                      (("2" (prop)
                        (("2" (expand "image")
                          (("2" (skosimp)
                            (("2" (replace -2 -3)
                              (("2"
                                (hide -1 -2)
                                (("2"
                                  (expand "lower_set?")
                                  (("2"
                                    (inst - "x!2" "x!1")
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (expand "down")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (flatten)
        (("2" (expand "lower_set?")
          (("2" (skosimp)
            (("2" (expand "member")
              (("2" (replace -1)
                (("2" (hide -1)
                  (("2" (expand "Union")
                    (("2" (skosimp)
                      (("2" (typepred "a!1")
                        (("2" (expand "extend")
                          (("2" (case-replace "lower_set?(a!1)")
                            (("1" (expand "lower_set?")
                              (("1"
                                (inst - "x!1" "y!1")
                                (("1"
                                  (expand "member")
                                  (("1"
                                    (replace -4 -1)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (expand "image")
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (inst + "a!1")
                                            nil
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil partial_order_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (down const-decl "lower_set" partial_order_props nil)
    (image const-decl "set[R]" function_image nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (lower_set nonempty-type-eq-decl nil partial_order_props nil)
    (lower_set? const-decl "bool" partial_order_props nil)
    (Union const-decl "set" sets nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (partial_order_reflexive formula-decl nil partial_order_props nil)
    (x!1 skolem-const-decl "T" partial_order_props nil)
    (S!1 skolem-const-decl "set[T]" partial_order_props nil))
   shostak))
(upper_set_def 0
  (upper_set_def-1 nil 3330494189
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (apply-extensionality :hide? t)
          (("1" (case-replace "S!1(x!1)")
            (("1" (expand "Union")
              (("1" (inst + "up(x!1)")
                (("1" (expand "up") (("1" (assert) nil nil)) nil)
                 ("2" (expand "image")
                  (("2" (expand "extend")
                    (("2" (inst + "x!1") nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (expand "Union")
                (("2" (skosimp)
                  (("2" (typepred "a!1")
                    (("2" (expand "extend")
                      (("2" (prop)
                        (("2" (expand "image")
                          (("2" (skosimp)
                            (("2" (expand "upper_set?")
                              (("2"
                                (typepred "x!2")
                                (("2"
                                  (replace -3 -4)
                                  (("2"
                                    (hide -2 -3)
                                    (("2"
                                      (inst - "x!2" "x!1")
                                      (("2"
                                        (expand "member")
                                        (("2"
                                          (expand "up")
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (flatten)
        (("2" (expand "upper_set?")
          (("2" (skosimp)
            (("2" (expand "member")
              (("2" (replace -1)
                (("2" (hide -1)
                  (("2" (expand "Union")
                    (("2" (skosimp)
                      (("2" (typepred "a!1")
                        (("2" (expand "extend")
                          (("2" (case-replace "upper_set?(a!1)")
                            (("1" (expand "image")
                              (("1"
                                (skosimp)
                                (("1"
                                  (inst + "a!1")
                                  (("1"
                                    (expand "upper_set?")
                                    (("1"
                                      (inst - "x!1" "y!1")
                                      (("1"
                                        (replace -4 -1)
                                        (("1"
                                          (expand "member")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil partial_order_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (up const-decl "upper_set" partial_order_props nil)
    (image const-decl "set[R]" function_image nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (upper_set nonempty-type-eq-decl nil partial_order_props nil)
    (upper_set? const-decl "bool" partial_order_props nil)
    (Union const-decl "set" sets nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (partial_order_reflexive formula-decl nil partial_order_props nil)
    (x!1 skolem-const-decl "T" partial_order_props nil)
    (S!1 skolem-const-decl "set[T]" partial_order_props nil))
   shostak))
(Union_lower_set 0
  (Union_lower_set-1 nil 3330495938
   ("" (skosimp)
    (("" (typepred "LS!1")
      (("" (expand "lower_sets?")
        (("" (expand "lower_set?")
          (("" (expand "every")
            (("" (expand "member")
              (("" (expand "Union")
                (("" (skosimp*)
                  (("" (typepred "a!1")
                    (("" (inst - "a!1")
                      (("" (inst - "x!1" "y!1")
                        (("" (replace -4)
                          (("" (assert) (("" (inst + "a!1") nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_sets nonempty-type-eq-decl nil partial_order_props nil)
    (lower_sets? const-decl "bool" partial_order_props nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (lower_set? const-decl "bool" partial_order_props nil)
    (member const-decl "bool" sets nil)
    (Union const-decl "set" sets nil)
    (every const-decl "bool" sets nil))
   shostak))
(Union_upper_set 0
  (Union_upper_set-1 nil 3330495938
   ("" (skosimp)
    (("" (typepred "US!1")
      (("" (expand "upper_sets?")
        (("" (expand "upper_set?")
          (("" (expand "Union")
            (("" (expand "every")
              (("" (expand "member")
                (("" (skosimp*)
                  (("" (inst - "a!1")
                    (("" (inst - "x!1" "y!1")
                      (("" (replace -3)
                        (("" (assert) (("" (inst + "a!1") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_sets nonempty-type-eq-decl nil partial_order_props nil)
    (upper_sets? const-decl "bool" partial_order_props nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (upper_set? const-decl "bool" partial_order_props nil)
    (every const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (Union const-decl "set" sets nil))
   shostak))
(Intersection_lower_set 0
  (Intersection_lower_set-1 nil 3330495938
   ("" (skosimp)
    (("" (typepred "LS!1")
      (("" (expand "lower_sets?")
        (("" (expand "lower_set?")
          (("" (expand "Intersection")
            (("" (expand "member")
              (("" (skosimp*)
                (("" (expand "every")
                  (("" (typepred "a!1")
                    (("" (inst - "a!1")
                      (("" (inst - "a!1")
                        (("" (inst - "x!1" "y!1")
                          (("" (replace -4) (("" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_sets nonempty-type-eq-decl nil partial_order_props nil)
    (lower_sets? const-decl "bool" partial_order_props nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (lower_set? const-decl "bool" partial_order_props nil)
    (member const-decl "bool" sets nil)
    (every const-decl "bool" sets nil)
    (Intersection const-decl "set" sets nil))
   shostak))
(Intersection_upper_set 0
  (Intersection_upper_set-1 nil 3330495938
   ("" (skosimp)
    (("" (typepred "US!1")
      (("" (expand "upper_sets?")
        (("" (expand "every")
          (("" (expand "upper_set?")
            (("" (expand "Intersection")
              (("" (expand "member")
                (("" (skosimp*)
                  (("" (inst - "a!1")
                    (("" (inst - "a!1")
                      (("" (inst - "x!1" "y!1")
                        (("" (replace -3) (("" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_sets nonempty-type-eq-decl nil partial_order_props nil)
    (upper_sets? const-decl "bool" partial_order_props nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (every const-decl "bool" sets nil)
    (Intersection const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (upper_set? const-decl "bool" partial_order_props nil))
   shostak))
(union_lower_set 0
  (union_lower_set-1 nil 3330496447
   ("" (skosimp)
    (("" (typepred "L1!1")
      (("" (typepred "L2!1")
        (("" (expand "lower_set?")
          (("" (expand "union")
            (("" (expand "member")
              (("" (skosimp*)
                (("" (inst - "x!1" "y!1")
                  (("" (inst - "x!1" "y!1")
                    (("" (replace -4)
                      (("" (split -3)
                        (("1" (assert) nil nil) ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_set nonempty-type-eq-decl nil partial_order_props nil)
    (lower_set? const-decl "bool" partial_order_props nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil))
   shostak))
(union_upper_set 0
  (union_upper_set-1 nil 3330496447
   ("" (skosimp)
    (("" (typepred "U1!1")
      (("" (typepred "U2!1")
        (("" (expand "union")
          (("" (expand "upper_set?")
            (("" (expand "member")
              (("" (skosimp*)
                (("" (inst - "x!1" "y!1")
                  (("" (inst - "x!1" "y!1")
                    (("" (replace -4)
                      (("" (split -3)
                        (("1" (assert) nil nil) ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_set nonempty-type-eq-decl nil partial_order_props nil)
    (upper_set? const-decl "bool" partial_order_props nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil))
   shostak))
(intersection_lower_set 0
  (intersection_lower_set-1 nil 3330496447
   ("" (skosimp)
    (("" (typepred "L1!1")
      (("" (typepred "L2!1")
        (("" (expand "intersection")
          (("" (expand "lower_set?")
            (("" (expand "member")
              (("" (skosimp)
                (("" (inst - "x!1" "y!1")
                  (("" (inst - "x!1" "y!1")
                    (("" (replace -5) (("" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_set nonempty-type-eq-decl nil partial_order_props nil)
    (lower_set? const-decl "bool" partial_order_props nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (intersection const-decl "set" sets nil)
    (member const-decl "bool" sets nil))
   shostak))
(intersection_upper_set 0
  (intersection_upper_set-1 nil 3330496447
   ("" (skosimp)
    (("" (typepred "U1!1")
      (("" (typepred "U2!1")
        (("" (expand "upper_set?")
          (("" (expand "intersection")
            (("" (expand "member")
              (("" (skosimp)
                (("" (inst - "x!1" "y!1")
                  (("" (inst - "x!1" "y!1")
                    (("" (replace -5) (("" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_set nonempty-type-eq-decl nil partial_order_props nil)
    (upper_set? const-decl "bool" partial_order_props nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil partial_order_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.42 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.