Quelle upper_semilattices.prf Sprache: Lisp

(upper_semilattices
(finite_set_is_least_bounded_above 0
  (finite_set_is_least_bounded_above-1 nil 3314553924
   ("" (skolem!)
    (("" (typepred "<=")
      (("" (expand "upper_semilattice?")
        (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
      nil))
    nil)
   ((<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil upper_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans 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))
   nil))
(least_upper_bound_singleton 0
  (least_upper_bound_singleton-1 nil 3314553965
   ("" (skolem!)
    (("" (expand* "least_upper_bound?" "upper_bound?")
      (("" (split)
        (("1" (typepred "<=")
          (("1"
            (expand* "upper_semilattice?" "partial_order?" "preorder?"
             "reflexive?")
            (("1" (skosimp :preds? t)
              (("1" (expand "singleton")
                (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil)
         ("2" (skosimp)
          (("2" (inst - "t!1")
            (("2" (expand "singleton") (("2" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_bound? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (t!1 skolem-const-decl "T" upper_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil upper_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (preorder? const-decl "bool" orders nil)
    (reflexive? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil))
   shostak))
(lub_singleton 0
  (lub_singleton-1 nil 3314554034
   ("" (skolem!)
    (("" (invoke (typepred "%1") (! 1 l))
      (("" (rewrite "unique_least_upper_bound")
        (("" (rewrite "least_upper_bound_singleton") nil nil)) nil))
      nil))
    nil)
   ((nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" upper_semilattices 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 upper_semilattices nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types 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)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (least_upper_bound_singleton formula-decl nil upper_semilattices
     nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (unique_least_upper_bound formula-decl nil bounded_orders nil))
   shostak))
(lub_le 0
  (lub_le-1 nil 3314554072
   ("" (skolem!)
    (("" (expand "lub")
      (("" (invoke (typepred "%1") (! 1 l l))
        (("" (invoke (name-replace "L" "%1") (! 1 l l))
          (("" (expand "least_upper_bound?")
            (("" (typepred "<=")
              (("" (prop)
                (("1" (hide -4)
                  (("1" (expand "upper_bound?")
                    (("1" (inst - "t!1")
                      (("1"
                        (expand* "upper_semilattice?" "partial_order?"
                         "preorder?" "transitive?")
                        (("1" (flatten)
                          (("1" (inst - "t!1" "L" "s!1")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (expand* "union" "singleton" "member") nil
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide -4)
                  (("2" (expand "upper_bound?")
                    (("2" (inst - "u!1")
                      (("1"
                        (expand* "upper_semilattice?" "partial_order?"
                         "preorder?" "transitive?")
                        (("1" (flatten)
                          (("1" (inst - "u!1" "L" "s!1")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (expand* "union" "singleton" "member") nil
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (hide -4)
                  (("3" (inst - "s!1")
                    (("3" (assert)
                      (("3" (expand "upper_bound?")
                        (("3" (skolem-typepred)
                          (("3" (expand* "union" "singleton" "member")
                            (("3" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lub const-decl "T" upper_semilattices nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (t!1 skolem-const-decl "T" upper_semilattices nil)
    (u!1 skolem-const-decl "T" upper_semilattices nil)
    (preorder? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (member const-decl "bool" sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (upper_semilattice? const-decl "bool" bounded_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)
    (T formal-type-decl nil upper_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty_finite_union1 application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     upper_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil))
   shostak))
(le_lub_1 0
  (le_lub_1-1 nil 3314554256
   ("" (skosimp)
    (("" (expand "lub")
      (("" (invoke (typepred "%1") (! 1 r))
        (("" (invoke (name-replace "L" "%1") (! 1 r))
          (("" (expand "least_upper_bound?")
            (("" (flatten)
              (("" (hide -2)
                (("" (expand "upper_bound?")
                  (("" (inst - "t!1")
                    (("1" (typepred "<=")
                      (("1"
                        (expand* "upper_semilattice?" "partial_order?"
                         "preorder?" "transitive?")
                        (("1" (flatten)
                          (("1" (inst - "s!1" "t!1" "L")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand* "union" "singleton" "member") nil
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lub const-decl "T" upper_semilattices nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (preorder? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (u!1 skolem-const-decl "T" upper_semilattices nil)
    (t!1 skolem-const-decl "T" upper_semilattices nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (upper_semilattice? const-decl "bool" bounded_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)
    (T formal-type-decl nil upper_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty_finite_union1 application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     upper_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil))
   shostak))
(le_lub_2 0
  (le_lub_2-1 nil 3314554321
   ("" (skosimp)
    (("" (expand "lub")
      (("" (invoke (typepred "%1") (! 1 r))
        (("" (invoke (name-replace "L" "%1") (! 1 r))
          (("" (expand "least_upper_bound?")
            (("" (flatten)
              (("" (hide -2)
                (("" (expand "upper_bound?")
                  (("" (inst - "u!1")
                    (("1" (typepred "<=")
                      (("1"
                        (expand* "upper_semilattice?" "partial_order?"
                         "preorder?" "transitive?")
                        (("1" (flatten)
                          (("1" (inst - "s!1" "u!1" "L")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand* "union" "singleton" "member") nil
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lub const-decl "T" upper_semilattices nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (preorder? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (u!1 skolem-const-decl "T" upper_semilattices nil)
    (t!1 skolem-const-decl "T" upper_semilattices nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (upper_semilattice? const-decl "bool" bounded_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)
    (T formal-type-decl nil upper_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty_finite_union1 application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     upper_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil))
   shostak))
(union_preserves_bounded_above 0
  (union_preserves_bounded_above-1 nil 3314553924
   ("" (skolem-typepred)
    (("" (expand "bounded_above?")
      (("" (skosimp*)
        (("" (inst + "lub(t!1, t!2)")
          (("" (expand "upper_bound?")
            (("" (skolem-typepred)
              (("" (expand* "union" "member")
                (("" (split)
                  (("1" (inst?) (("1" (rewrite "le_lub_1") nil nil))
                    nil)
                   ("2" (inst? -3) (("2" (rewrite "le_lub_2") nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lub const-decl "T" upper_semilattices nil)
    (union const-decl "set" sets nil)
    (le_lub_1 formula-decl nil upper_semilattices nil)
    (r!1 skolem-const-decl "(union[T](S1!1, S2!1))" upper_semilattices
     nil)
    (S2!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
     nil)
    (S1!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
     nil)
    (le_lub_2 formula-decl nil upper_semilattices nil)
    (member const-decl "bool" sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil upper_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(add_preserves_bounded_above 0
  (add_preserves_bounded_above-1 nil 3314553924
   ("" (skolem-typepred)
    (("" (rewrite "add_as_union")
      (("" (rewrite "union_preserves_bounded_above") nil nil)) nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     upper_semilattices nil)
    (union_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
     nil)
    (union_preserves_bounded_above judgement-tcc nil upper_semilattices
     nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil upper_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(least_upper_bound_union 0
  (least_upper_bound_union-1 nil 3314556714
   ("" (skosimp)
    (("" (expand "least_upper_bound?")
      (("" (prop)
        (("1" (hide -4 -2)
          (("1" (expand "upper_bound?")
            (("1" (skolem-typepred)
              (("1" (expand* "union" "member")
                (("1" (inst - "r!1")
                  (("1" (rewrite "le_lub_1") nil nil)
                   ("2" (assert)
                    (("2" (inst - "r!1")
                      (("2" (rewrite "le_lub_2") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp)
          (("2" (rewrite "lub_le")
            (("2" (split)
              (("1" (hide -5 -4 -2)
                (("1" (inst?)
                  (("1" (assert)
                    (("1" (expand "upper_bound?")
                      (("1" (skolem!)
                        (("1" (inst - "r!2")
                          (("1" (expand* "union" "member") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide -4 -3 -2)
                (("2" (inst?)
                  (("2" (assert)
                    (("2" (expand "upper_bound?")
                      (("2" (skolem!)
                        (("2" (inst - "r!2")
                          (("2" (expand* "union" "member") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((least_upper_bound? const-decl "bool" bounded_orders nil)
    (r!2 skolem-const-decl "(S1!1)" upper_semilattices nil)
    (union_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
     nil)
    (r!2 skolem-const-decl "(S2!1)" upper_semilattices nil)
    (lub_le formula-decl nil upper_semilattices 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 upper_semilattices nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
    (pred type-eq-decl nil defined_types nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (S1!1 skolem-const-decl
     "(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
     upper_semilattices nil)
    (S2!1 skolem-const-decl
     "(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
     upper_semilattices nil)
    (r!1 skolem-const-decl "(union(S1!1, S2!1))" upper_semilattices
     nil)
    (le_lub_1 formula-decl nil upper_semilattices nil)
    (le_lub_2 formula-decl nil upper_semilattices nil)
    (member const-decl "bool" sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil))
   shostak))
(least_upper_bound_add 0
  (least_upper_bound_add-1 nil 3314556833
   ("" (skosimp)
    (("" (rewrite "add_as_union")
      (("" (rewrite "least_upper_bound_union")
        (("" (rewrite "least_upper_bound_singleton") nil nil)) nil))
      nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas 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)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (T formal-type-decl nil upper_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     upper_semilattices nil)
    (union_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
     nil)
    (least_upper_bound_singleton formula-decl nil upper_semilattices
     nil)
    (least_upper_bound_union formula-decl nil upper_semilattices nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil))
   shostak))
(union_preserves_least_bounded_above 0
  (union_preserves_least_bounded_above-1 nil 3314553924
   ("" (skolem-typepred)
    (("" (expand "least_bounded_above?")
      (("" (skosimp*)
        (("" (inst + "lub(t!1, t!2)")
          (("" (rewrite "least_upper_bound_union") nil nil)) nil))
        nil))
      nil))
    nil)
   ((lub const-decl "T" upper_semilattices nil)
    (least_upper_bound_union formula-decl nil upper_semilattices nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil upper_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(add_preserves_least_bounded_above 0
  (add_preserves_least_bounded_above-1 nil 3314553924
   ("" (skolem-typepred)
    (("" (rewrite "add_as_union")
      (("" (rewrite "union_preserves_least_bounded_above") nil nil))
      nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     upper_semilattices nil)
    (union_preserves_least_bounded_above application-judgement
     "(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
     upper_semilattices nil)
    (union_preserves_least_bounded_above judgement-tcc nil
     upper_semilattices nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil upper_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(lub_union 0
  (lub_union-1 nil 3314556944
   ("" (skolem!)
    (("" (invoke (typepred "%1" "%2" "%3") (! 1 l) (! 1 r 1) (! 1 r 2))
      (("" (invoke (name-replace "LU" "%1") (! 1 l))
        (("" (invoke (name-replace "L1" "%1") (! 1 r 1))
          (("" (invoke (name-replace "L2" "%1") (! 1 r 2))
            (("" (use "least_upper_bound_union")
              (("" (assert)
                (("" (use "unique_least_upper_bound") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((union_preserves_least_bounded_above application-judgement
     "(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
     upper_semilattices 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 upper_semilattices nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types 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)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (union const-decl "set" sets nil)
    (least_upper_bound_union formula-decl nil upper_semilattices nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (lub const-decl "T" upper_semilattices nil)
    (unique_least_upper_bound formula-decl nil bounded_orders nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   shostak))
(lub_add 0
  (lub_add-1 nil 3314557004
   ("" (skolem!)
    (("" (rewrite "add_as_union")
      (("" (rewrite "lub_union")
        (("" (rewrite "lub_singleton") nil nil)) nil))
      nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas 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)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
        nil)
    (T formal-type-decl nil upper_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" upper_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     upper_semilattices nil)
    (union_preserves_least_bounded_above application-judgement
     "(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
     upper_semilattices nil)
    (lub_singleton formula-decl nil upper_semilattices nil)
    (lub_union formula-decl nil upper_semilattices nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil))
   shostak)))

quality88%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Normalansicht

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.