Quelle lower_semilattices.prf Sprache: Lisp

(lower_semilattices
(finite_set_is_greatest_bounded_below 0
  (finite_set_is_greatest_bounded_below-1 nil 3315157450
   ("" (skolem!)
    (("" (typepred "<=")
      (("" (expand "lower_semilattice?")
        (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
      nil))
    nil)
   ((<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil lower_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))
(greatest_lower_bound_singleton 0
  (greatest_lower_bound_singleton-1 nil 3315157495
   ("" (skolem!)
    (("" (expand "greatest_lower_bound?")
      (("" (split)
        (("1" (typepred "<=")
          (("1"
            (expand* "singleton" "lower_bound?" "lower_semilattice?"
             "partial_order?" "preorder?" "reflexive?")
            (("1" (skosimp :preds? t)
              (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (skosimp)
          (("2" (expand* "singleton" "lower_bound?")
            (("2" (inst?) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil lower_semilattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (lower_bound? const-decl "bool" bounded_orders nil))
   shostak))
(glb_singleton 0
  (glb_singleton-1 nil 3315157548
   ("" (skolem!)
    (("" (invoke (typepred "%1") (! 1 l))
      (("" (rewrite "unique_greatest_lower_bound")
        (("" (rewrite "greatest_lower_bound_singleton") nil nil)) nil))
      nil))
    nil)
   ((nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" lower_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 lower_semilattices nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (greatest_lower_bound_singleton formula-decl nil lower_semilattices
     nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (unique_greatest_lower_bound formula-decl nil bounded_orders nil))
   shostak))
(le_glb 0
  (le_glb-1 nil 3315157580
   ("" (skolem!)
    (("" (expand "glb")
      (("" (invoke (typepred "%1") (! 1 l r))
        (("" (invoke (name-replace "L" "%1") (! 1 l r))
          (("" (typepred "<=")
            (("" (expand "greatest_lower_bound?")
              (("" (prop)
                (("1" (hide -4)
                  (("1" (expand "lower_bound?")
                    (("1" (inst - "t!1")
                      (("1"
                        (expand* "lower_semilattice?" "partial_order?"
                         "preorder?" "transitive?")
                        (("1" (flatten)
                          (("1" (inst - "s!1" "L" "t!1")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (expand* "union" "singleton" "member") nil
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide -4)
                  (("2" (expand "lower_bound?")
                    (("2" (inst - "u!1")
                      (("1"
                        (expand* "lower_semilattice?" "partial_order?"
                         "preorder?" "transitive?")
                        (("1" (flatten)
                          (("1" (inst - "s!1" "L" "u!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* "union" "singleton" "member"
                         "lower_bound?")
                        (("3" (skolem-typepred)
                          (("3" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((glb const-decl "T" lower_semilattices nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (t!1 skolem-const-decl "T" lower_semilattices nil)
    (u!1 skolem-const-decl "T" lower_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)
    (lower_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 "(lower_semilattice?[T])" lower_semilattices
        nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders 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)
    (T formal-type-decl nil lower_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]" lower_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     lower_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" lower_semilattices nil))
   shostak))
(glb_le_1 0
  (glb_le_1-1 nil 3315157701
   ("" (skosimp)
    (("" (expand "glb")
      (("" (invoke (typepred "%1") (! 1 l))
        (("" (invoke (name-replace "L" "%1") (! 1 l))
          (("" (expand* "greatest_lower_bound?" "lower_bound?")
            (("" (flatten)
              (("" (inst - "t!1")
                (("1" (typepred "<=")
                  (("1"
                    (expand* "lower_semilattice?" "partial_order?"
                     "preorder?" "transitive?")
                    (("1" (flatten)
                      (("1" (inst - "L" "t!1" "s!1")
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand* "union" "singleton" "member") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((glb const-decl "T" lower_semilattices nil)
    (= const-decl "[T, T -> boolean]" equalities 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" lower_semilattices nil)
    (t!1 skolem-const-decl "T" lower_semilattices nil)
    (lower_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 "(lower_semilattice?[T])" lower_semilattices
        nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders 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)
    (T formal-type-decl nil lower_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]" lower_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     lower_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" lower_semilattices nil))
   shostak))
(glb_le_2 0
  (glb_le_2-1 nil 3315157757
   ("" (skosimp)
    (("" (expand "glb")
      (("" (invoke (typepred "%1") (! 1 l))
        (("" (invoke (name-replace "L" "%1") (! 1 l))
          (("" (expand* "greatest_lower_bound?" "lower_bound?")
            (("" (flatten)
              (("" (inst - "u!1")
                (("1" (typepred "<=")
                  (("1"
                    (expand* "lower_semilattice?" "partial_order?"
                     "preorder?" "transitive?")
                    (("1" (flatten)
                      (("1" (inst - "L" "u!1" "s!1")
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand* "union" "singleton" "member") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((glb const-decl "T" lower_semilattices nil)
    (= const-decl "[T, T -> boolean]" equalities 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" lower_semilattices nil)
    (t!1 skolem-const-decl "T" lower_semilattices nil)
    (lower_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 "(lower_semilattice?[T])" lower_semilattices
        nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders 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)
    (T formal-type-decl nil lower_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]" lower_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     lower_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" lower_semilattices nil))
   shostak))
(union_preserves_bounded_below 0
  (union_preserves_bounded_below-1 nil 3315157450
   ("" (skolem-typepred)
    (("" (expand "bounded_below?")
      (("" (skosimp*)
        (("" (inst + "glb(t!1, t!2)")
          (("" (expand "lower_bound?")
            (("" (skolem-typepred)
              (("" (expand* "union" "member")
                (("" (inst?)
                  (("1" (rewrite "glb_le_1") nil nil)
                   ("2" (assert)
                    (("2" (inst?) (("2" (rewrite "glb_le_2") nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((glb const-decl "T" lower_semilattices nil)
    (union const-decl "set" sets nil)
    (S1!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
     nil)
    (S2!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
     nil)
    (r!1 skolem-const-decl "(union[T](S1!1, S2!1))" lower_semilattices
     nil)
    (glb_le_1 formula-decl nil lower_semilattices nil)
    (glb_le_2 formula-decl nil lower_semilattices nil)
    (member const-decl "bool" sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (bounded_below? 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 lower_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_below 0
  (add_preserves_bounded_below-1 nil 3315157450
   ("" (skolem-typepred)
    (("" (rewrite "add_as_union")
      (("" (rewrite "union_preserves_bounded_below") nil nil)) nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" lower_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     lower_semilattices nil)
    (union_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
     nil)
    (union_preserves_bounded_below judgement-tcc nil lower_semilattices
     nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (bounded_below? 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 lower_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))
(greatest_lower_bound_union 0
  (greatest_lower_bound_union-1 nil 3315157910
   ("" (skosimp)
    (("" (expand "greatest_lower_bound?")
      (("" (prop)
        (("1" (hide -4 -2)
          (("1" (expand "lower_bound?")
            (("1" (skolem-typepred)
              (("1" (expand* "union" "member")
                (("1" (inst - "r!1")
                  (("1" (rewrite "glb_le_1") nil nil)
                   ("2" (assert)
                    (("2" (inst - "r!1")
                      (("2" (rewrite "glb_le_2") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp)
          (("2" (rewrite "le_glb")
            (("2" (split)
              (("1" (hide -5 -4 -2)
                (("1" (inst?)
                  (("1" (assert)
                    (("1" (expand "lower_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 "lower_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)
   ((greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (r!2 skolem-const-decl "(S1!1)" lower_semilattices nil)
    (union_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
     nil)
    (r!2 skolem-const-decl "(S2!1)" lower_semilattices nil)
    (le_glb formula-decl nil lower_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 lower_semilattices nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
    (pred type-eq-decl nil defined_types nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (S1!1 skolem-const-decl
     "(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
     lower_semilattices nil)
    (S2!1 skolem-const-decl
     "(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
     lower_semilattices nil)
    (r!1 skolem-const-decl "(union(S1!1, S2!1))" lower_semilattices
     nil)
    (glb_le_1 formula-decl nil lower_semilattices nil)
    (glb_le_2 formula-decl nil lower_semilattices nil)
    (member const-decl "bool" sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil))
   shostak))
(greatest_lower_bound_add 0
  (greatest_lower_bound_add-1 nil 3315158032
   ("" (skosimp)
    (("" (rewrite "add_as_union")
      (("" (rewrite "greatest_lower_bound_union")
        (("" (rewrite "greatest_lower_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)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (T formal-type-decl nil lower_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" lower_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     lower_semilattices nil)
    (union_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
     nil)
    (greatest_lower_bound_singleton formula-decl nil lower_semilattices
     nil)
    (greatest_lower_bound_union formula-decl nil lower_semilattices
     nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil))
   shostak))
(union_preserves_greatest_bounded_below 0
  (union_preserves_greatest_bounded_below-1 nil 3315157450
   ("" (skolem-typepred)
    (("" (expand "greatest_bounded_below?")
      (("" (skosimp*)
        (("" (inst + "glb(t!1, t!2)")
          (("" (rewrite "greatest_lower_bound_union") nil nil)) nil))
        nil))
      nil))
    nil)
   ((glb const-decl "T" lower_semilattices nil)
    (greatest_lower_bound_union formula-decl nil lower_semilattices
     nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? 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 lower_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_greatest_bounded_below 0
  (add_preserves_greatest_bounded_below-1 nil 3315157450
   ("" (skolem!)
    (("" (rewrite "add_as_union")
      (("" (rewrite "union_preserves_greatest_bounded_below") 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)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (T formal-type-decl nil lower_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" lower_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     lower_semilattices nil)
    (union_preserves_greatest_bounded_below application-judgement
     "(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
     lower_semilattices nil)
    (union_preserves_greatest_bounded_below judgement-tcc nil
     lower_semilattices nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil))
   nil))
(glb_union 0
  (glb_union-1 nil 3315158151
   ("" (skolem!)
    (("" (invoke (typepred "%1" "%2" "%3") (! 1 l) (! 1 r 1) (! 1 r 2))
      (("" (invoke (name-replace "GU" "%1") (! 1 l))
        (("" (invoke (name-replace "G1" "%1") (! 1 r 1))
          (("" (invoke (name-replace "G2" "%1") (! 1 r 2))
            (("" (use "greatest_lower_bound_union")
              (("" (assert)
                (("" (use "unique_greatest_lower_bound") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((union_preserves_greatest_bounded_below application-judgement
     "(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
     lower_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 lower_semilattices nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (union const-decl "set" sets nil)
    (greatest_lower_bound_union formula-decl nil lower_semilattices
     nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (glb const-decl "T" lower_semilattices nil)
    (unique_greatest_lower_bound formula-decl nil bounded_orders nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   shostak))
(glb_add 0
  (glb_add-1 nil 3315158200
   ("" (skolem!)
    (("" (rewrite "add_as_union")
      (("" (rewrite "glb_union")
        (("" (rewrite "glb_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)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
        nil)
    (T formal-type-decl nil lower_semilattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" lower_semilattices nil)
    (nonempty_union2 application-judgement "(nonempty?)"
     lower_semilattices nil)
    (union_preserves_greatest_bounded_below application-judgement
     "(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
     lower_semilattices nil)
    (glb_singleton formula-decl nil lower_semilattices nil)
    (glb_union formula-decl nil lower_semilattices nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil))
   shostak)))

quality100%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

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.