Quelle closure_ops.prf Sprache: Lisp

(closure_ops
(reflexive_closure_TCC1 0
  (reflexive_closure_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (reflexive? const-decl "bool" relations nil))
   nil))
(irreflexive_kernel_TCC1 0
  (irreflexive_kernel_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (irreflexive? const-decl "bool" relations nil))
   nil))
(symmetric_closure_TCC1 0
  (symmetric_closure_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (union const-decl "set" sets nil)
    (symmetric? const-decl "bool" relations nil))
   nil))
(symmetric_kernel_TCC1 0
  (symmetric_kernel_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (intersection const-decl "set" sets nil)
    (symmetric? const-decl "bool" relations nil))
   nil))
(asymmetric_kernel_TCC1 0
  (asymmetric_kernel_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (difference const-decl "set" sets nil)
    (T formal-type-decl nil closure_ops nil)
    (asymmetric? const-decl "bool" relations_extra nil))
   nil))
(transitive_closure_TCC1 0
  (transitive_closure_TCC1-1 nil 3315150742
   ("" (expand* "transitive?" "IUnion")
    (("" (skosimp*)
      (("" (forward-chain "iterate_add_applied") (("" (inst?) nil nil))
        nil))
      nil))
    nil)
   ((numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (T formal-type-decl nil closure_ops nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (iterate_add_applied formula-decl nil relation_iterate nil)
    (transitive? const-decl "bool" relations nil)
    (IUnion const-decl "set[T]" indexed_sets nil))
   nil))
(preorder_closure_TCC1 0
  (preorder_closure_TCC1-1 nil 3315150742
   ("" (expand "preorder?")
    (("" (skolem!)
      (("" (split)
        (("1" (expand* "reflexive?" "IUnion")
          (("1" (skolem!)
            (("1" (inst + "0")
              (("1" (expand "iterate") (("1" (propax) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (expand* "transitive?" "IUnion")
          (("2" (skosimp*)
            (("2" (forward-chain "iterate_add_applied")
              (("2" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((transitive? const-decl "bool" relations nil)
    (iterate_add_applied formula-decl nil relation_iterate nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (reflexive? const-decl "bool" relations nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate nil)
    (preorder? const-decl "bool" orders nil))
   nil))
(reflexive_irreflexive 0
  (reflexive_irreflexive-1 nil 3315150906 ("" (grind-with-ext) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (reflexive? const-decl "bool" relations nil)
    (member const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (difference const-decl "set" sets nil)
    (union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil))
   shostak))
(irreflexive_reflexive 0
  (irreflexive_reflexive-1 nil 3315150924 ("" (grind-with-ext) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (irreflexive? const-decl "bool" relations nil)
    (member const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (union const-decl "set" sets nil)
    (difference const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil))
   shostak))
(reflexive_closure_preserves_transitive 0
  (reflexive_closure_preserves_transitive-1 nil 3315150742
   ("" (skolem-typepred)
    ((""
      (expand* "preorder?" "transitive?" "reflexive_closure" "union"
       "member")
      (("" (skosimp)
        (("" (inst - "x!1" "y!1" "z!1") (("" (ground) nil nil)) nil))
        nil))
      nil))
    nil)
   ((union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (preorder? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(reflexive_closure_preserves_antisymmetric 0
  (reflexive_closure_preserves_antisymmetric-1 nil 3315150742
   ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (antisymmetric? const-decl "bool" relations nil))
   nil))
(order_to_partial_order 0
  (order_to_partial_order-1 nil 3315150742
   ("" (skolem-typepred)
    ((""
      (expand* "partial_order?" "preorder?" "antisymmetric?"
       "reflexive_closure" "union" "member")
      nil nil))
    nil)
   ((reflexive_closure_preserves_antisymmetric application-judgement
     "(antisymmetric?)" closure_ops nil)
    (reflexive_closure_preserves_transitive application-judgement
     "(preorder?)" closure_ops nil)
    (partial_order? const-decl "bool" orders nil)
    (order? const-decl "bool" relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(reflexive_closure_dichotomous 0
  (reflexive_closure_dichotomous-1 nil 3315150742
   ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (pred type-eq-decl nil defined_types nil)
    (trichotomous? const-decl "bool" orders nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (dichotomous? const-decl "bool" orders nil))
   nil))
(linear_order_to_total_order 0
  (linear_order_to_total_order-1 nil 3315150742
   ("" (skolem-typepred)
    ((""
      (expand* "linear_order?" "order?" "total_order?"
       "partial_order?")
      (("" (flatten)
        (("" (assert)
          ((""
            (lemma "reflexive_closure_preserves_transitive"
             ("R" "R!1"))
            ((""
              (lemma "reflexive_closure_preserves_antisymmetric"
               ("R" "R!1"))
              (("" (lemma "reflexive_closure_dichotomous" ("R" "R!1"))
                (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((order? const-decl "bool" relations_extra nil)
    (partial_order? const-decl "bool" orders nil)
    (total_order? const-decl "bool" orders nil)
    (reflexive_closure_preserves_antisymmetric judgement-tcc nil
     closure_ops nil)
    (antisymmetric? const-decl "bool" relations nil)
    (trichotomous? const-decl "bool" orders nil)
    (reflexive_closure_dichotomous judgement-tcc nil closure_ops nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (reflexive_closure_preserves_transitive judgement-tcc nil
     closure_ops nil)
    (linear_order? const-decl "bool" relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(order_to_strict_order 0
  (order_to_strict_order-1 nil 3315150742
   ("" (skolem-typepred)
    ((""
      (expand* "order?" "antisymmetric?" "strict_order?" "transitive?"
       "irreflexive_kernel" "difference" "member")
      (("" (skosimp)
        (("" (inst - "x!1" "y!1" "z!1")
          (("" (inst - "y!1" "z!1") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((antisymmetric? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (difference const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (strict_order? const-decl "bool" orders nil)
    (order? const-decl "bool" relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(irreflexive_kernel_of_antisymmetric 0
  (irreflexive_kernel_of_antisymmetric-1 nil 3315150742
   ("" (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)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (T formal-type-decl nil closure_ops nil)
    (asymmetric? const-decl "bool" relations_extra nil))
   nil))
(irreflexive_kernel_trichotomous 0
  (irreflexive_kernel_trichotomous-1 nil 3315150742
   ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (pred type-eq-decl nil defined_types nil)
    (dichotomous? const-decl "bool" orders nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (trichotomous? const-decl "bool" orders nil))
   nil))
(linear_order_to_strict_total_order 0
  (total_order_to_strict_total_order-1 nil 3315150742
   ("" (skolem!)
    (("" (expand "strict_total_order?") (("" (propax) nil nil)) nil))
    nil)
   ((irreflexive_kernel_trichotomous application-judgement
     "(trichotomous?)" closure_ops nil)
    (irreflexive_kernel_of_antisymmetric application-judgement
     "(asymmetric?)" closure_ops nil)
    (order_to_strict_order application-judgement "(strict_order?)"
     closure_ops nil)
    (strict_total_order? const-decl "bool" orders nil))
   nil))
(symmetric_kernel_of_preorder 0
  (symmetric_kernel_of_preorder-1 nil 3315150742
   ("" (skolem-typepred)
    (("" (expand "equivalence?")
      (("" (split)
        (("1"
          (expand* "preorder?" "reflexive?" "symmetric_kernel"
           "intersection" "converse" "member")
          (("1" (skosimp) (("1" (inst?) (("1" (assert) nil nil)) nil))
            nil))
          nil)
         ("2"
          (expand* "preorder?" "transitive?" "symmetric_kernel"
           "intersection" "converse" "member")
          (("2" (skosimp)
            (("2" (inst-cp - "x!1" "y!1" "z!1")
              (("2" (inst - "z!1" "y!1" "x!1") (("2" (ground) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((equivalence? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (reflexive? const-decl "bool" relations nil)
    (intersection const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (symmetric_kernel const-decl "(symmetric?)" closure_ops nil)
    (preorder? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(asymmetric_kernel_of_preorder 0
  (asymmetric_kernel_of_preorder-1 nil 3315150742
   ("" (skolem-typepred)
    (("" (expand "strict_order?")
      (("" (rewrite "asymmetric_is_irreflexive")
        ((""
          (expand* "preorder?" "transitive?" "asymmetric_kernel"
           "difference" "converse" "member")
          (("" (skosimp)
            (("" (inst-cp - "x!1" "y!1" "z!1")
              (("" (inst - "z!1" "x!1" "y!1") (("" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_order? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (difference const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (asymmetric_kernel const-decl "(asymmetric?)" closure_ops nil)
    (asymmetric? const-decl "bool" relations_extra nil)
    (asymmetric_is_irreflexive judgement-tcc nil relations_extra nil)
    (preorder? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(preorder_closure_converse 0
  (preorder_closure_converse-1 nil 3315151634
   ("" (skolem!)
    (("" (expand "preorder_closure")
      (("" (decompose-equality)
        (("" (expand "IUnion")
          (("" (iff)
            (("" (prop)
              (("1" (skolem!)
                (("1" (rewrite "iterate_converse")
                  (("1" (expand "converse") (("1" (inst?) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "converse" -)
                (("2" (skolem!)
                  (("2" (inst?)
                    (("2" (rewrite "iterate_converse")
                      (("2" (expand "converse")
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((preorder_closure const-decl "(preorder?)" closure_ops nil)
    (iterate_converse formula-decl nil relation_iterate nil)
    (T formal-type-decl nil closure_ops nil)
    (boolean nonempty-type-decl nil booleans nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate nil)
    (pred type-eq-decl nil defined_types nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (set type-eq-decl nil sets nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(symmetry_char 0
  (symmetry_char-1 nil 3315151700
   ("" (skolem!)
    (("" (expand* "subset?" "member" "converse" "symmetric?") nil nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (symmetric? const-decl "bool" relations nil))
   shostak))
(transitive_closure_of_reflexive 0
  (transitive_closure_of_reflexive-1 nil 3315150742
   ("" (skolem-typepred)
    ((""
      (expand* "preorder?" "reflexive?" "transitive_closure" "IUnion")
      (("" (skolem!)
        (("" (inst + 1)
          (("" (assert)
            (("" (inst?)
              (("" (expand* "iterate" "o" "iterate")
                (("" (inst?) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((IUnion const-decl "set[T]" indexed_sets nil)
    (transitive_closure const-decl "(transitive?)" closure_ops nil)
    (preorder? const-decl "bool" orders nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate nil)
    (O const-decl "bool" relation_props nil)
    (reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(transitive_closure_is_monotone 0
  (transitive_closure_is_monotone-1 nil 3315151790
   ("" (skosimp)
    (("" (expand "transitive_closure")
      (("" (rewrite "IUnion_is_monotone")
        (("" (skolem!) (("" (rewrite "iterate_is_monotone") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((transitive_closure const-decl "(transitive?)" closure_ops nil)
    (iterate_is_monotone formula-decl nil relation_iterate nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (T formal-type-decl nil closure_ops nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (IUnion_is_monotone formula-decl nil indexed_sets_extra nil))
   shostak))
(preorder_closure_is_monotone 0
  (preorder_closure_is_monotone-1 nil 3315151831
   ("" (skosimp)
    (("" (expand "preorder_closure")
      (("" (rewrite "IUnion_is_monotone")
        (("" (skolem!) (("" (rewrite "iterate_is_monotone") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((preorder_closure const-decl "(preorder?)" closure_ops nil)
    (iterate_is_monotone formula-decl nil relation_iterate nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (T formal-type-decl nil closure_ops nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (IUnion_is_monotone formula-decl nil indexed_sets_extra nil))
   shostak))
(preorder_closure_preserves_symmetry 0
  (preorder_closure_preserves_symmetry-1 nil 3315150742
   ("" (skolem-typepred)
    (("" (expand "equivalence?")
      (("" (typepred "preorder_closure(R!1)")
        (("" (expand "preorder?")
          (("" (prop)
            (("" (rewrite "symmetry_char")
              (("" (rewrite "symmetry_char")
                (("" (rewrite "preorder_closure_converse" :dir rl)
                  (("" (rewrite "preorder_closure_is_monotone") nil
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((equivalence? const-decl "bool" relations nil)
    (symmetry_char formula-decl nil closure_ops nil)
    (reflexive_converse application-judgement "(reflexive?[T])"
     relation_converse_props nil)
    (transitive_converse application-judgement "(transitive?[T])"
     relation_converse_props nil)
    (preorder_converse application-judgement "(preorder?[T])"
     relation_converse_props nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (preorder_closure_converse formula-decl nil closure_ops nil)
    (preorder_closure_is_monotone formula-decl nil closure_ops nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (symmetric_converse application-judgement "(symmetric?[T])"
     relation_converse_props nil)
    (pred type-eq-decl nil defined_types nil)
    (preorder? const-decl "bool" orders nil)
    (preorder_closure const-decl "(preorder?)" closure_ops nil)
    (symmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(transitive_closure_step_r 0
  (transitive_closure_step_r-1 nil 3315151963
   ("" (skolem!)
    (("" (decompose-equality)
      (("" (expand* "transitive_closure" "preorder_closure" "IUnion")
        (("" (expand "iterate" 1 1)
          (("" (expand "o")
            (("" (iff)
              (("" (prop)
                (("1" (skosimp*)
                  (("1" (inst?)
                    (("1" (assert) (("1" (inst?) nil nil)) nil)) nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pred type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (transitive_closure const-decl "(transitive?)" closure_ops nil)
    (O const-decl "bool" relation_props nil)
    (preorder? const-decl "bool" orders nil)
    (preorder_closure const-decl "(preorder?)" closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (IUnion const-decl "set[T]" indexed_sets nil))
   shostak))
(transitive_closure_step_l 0
  (transitive_closure_step_l-1 nil 3315152043
   ("" (skolem!)
    (("" (decompose-equality)
      (("" (expand* "transitive_closure" "preorder_closure" "IUnion")
        (("" (iff)
          (("" (prop)
            (("1" (skolem!)
              (("1" (rewrite "iterate_add_one")
                (("1" (expand "o")
                  (("1" (skosimp)
                    (("1" (inst?)
                      (("1" (assert) (("1" (inst?) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "o")
              (("2" (skosimp*)
                (("2" (inst + "i!1 + 1")
                  (("2" (rewrite "iterate_add_one")
                    (("2" (expand "o")
                      (("2" (inst?) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pred type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (transitive_closure const-decl "(transitive?)" closure_ops nil)
    (O const-decl "bool" relation_props nil)
    (preorder? const-decl "bool" orders nil)
    (preorder_closure const-decl "(preorder?)" closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (iterate_add_one formula-decl nil relation_iterate nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (IUnion const-decl "set[T]" indexed_sets nil))
   shostak))
(preorder_closure_reflexive_transitive 0
  (preorder_closure_reflexive_transitive-1 nil 3315152113
   ("" (skolem!)
    (("" (decompose-equality)
      ((""
        (expand* "preorder_closure" "reflexive_closure"
         "transitive_closure" "union" "member" "IUnion")
        (("" (iff)
          (("" (prop)
            (("1" (skolem!)
              (("1" (inst?)
                (("1" (assert)
                  (("1" (expand "iterate") (("1" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skolem!) (("2" (inst?) nil nil)) nil)
             ("3" (inst + 0)
              (("3" (expand "iterate") (("3" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((reflexive_closure_preserves_transitive application-judgement
     "(preorder?)" closure_ops nil)
    (preorder? const-decl "bool" orders nil)
    (preorder_closure const-decl "(preorder?)" closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (reflexive? const-decl "bool" relations nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (transitive? const-decl "bool" relations nil)
    (transitive_closure const-decl "(transitive?)" closure_ops nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate nil)
    (i!1 skolem-const-decl "nat" closure_ops nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (member const-decl "bool" sets nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (union const-decl "set" sets nil))
   shostak))
(preorder_closure_transitive_reflexive 0
  (preorder_closure_transitive_reflexive-1 nil 3315152170
   ("" (skolem!)
    (("" (decompose-equality)
      (("" (iff)
        (("" (prop)
          (("1" (rewrite "preorder_closure_reflexive_transitive")
            (("1" (expand "reflexive_closure" -)
              (("1" (expand* "union" "member")
                (("1" (split)
                  (("1" (lemma "transitive_closure_is_monotone")
                    (("1" (inst - "R!1" "reflexive_closure(R!1)")
                      (("1" (split)
                        (("1" (expand* "subset?" "member")
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil)
                         ("2" (hide-all-but 1)
                          (("2"
                            (expand* "subset?" "reflexive_closure"
                             "union" "member")
                            (("2" (skosimp) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (replace -1)
                    (("2"
                      (lemma "transitive_closure_of_reflexive"
                       ("R" "reflexive_closure(R!1)"))
                      (("2" (expand* "preorder?" "reflexive?")
                        (("2" (flatten) (("2" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand* "transitive_closure" "IUnion")
            (("2" (skolem!)
              (("2" (generalize-skolem-constants)
                (("2" (induct "i_1")
                  (("1" (assert) nil nil) ("2" (assert) nil nil)
                   ("3" (skosimp*)
                    (("3" (expand "iterate" -3)
                      (("3" (expand "o")
                        (("3" (skosimp)
                          (("3"
                            (case "preorder_closure(R!2)(x!4, y!1)")
                            (("1" (hide -2 -3 -4)
                              (("1"
                                (expand*
                                 "reflexive_closure"
                                 "union"
                                 "member"
                                 "preorder_closure"
                                 "IUnion")
                                (("1"
                                  (skolem!)
                                  (("1"
                                    (split)
                                    (("1"
                                      (inst + "i!2 + 1")
                                      (("1"
                                        (expand "iterate" +)
                                        (("1"
                                          (expand "o")
                                          (("1"
                                            (inst?)
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (inst?)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2)
                              (("2"
                                (splash -1)
                                (("1"
                                  (inst?)
                                  (("1" (assert) nil nil))
                                  nil)
                                 ("2"
                                  (assert)
                                  (("2"
                                    (expand "iterate")
                                    (("2"
                                      (expand*
                                       "preorder_closure"
                                       "IUnion")
                                      (("2"
                                        (inst + 0)
                                        (("2"
                                          (expand "iterate")
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((transitive_closure_of_reflexive application-judgement
     "(preorder?)" closure_ops nil)
    (preorder? const-decl "bool" orders nil)
    (preorder_closure const-decl "(preorder?)" closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (transitive_closure const-decl "(transitive?)" closure_ops nil)
    (reflexive? const-decl "bool" relations nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (subset? const-decl "bool" sets nil)
    (transitive_closure_is_monotone formula-decl nil closure_ops nil)
    (transitive_closure_of_reflexive judgement-tcc nil closure_ops nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (reflexive_closure_preserves_transitive application-judgement
     "(preorder?)" closure_ops nil)
    (preorder_closure_reflexive_transitive formula-decl nil closure_ops
     nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (O const-decl "bool" relation_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (IUnion const-decl "set[T]" indexed_sets nil))
   shostak))
(reflexive_closure_identity 0
  (reflexive_closure_identity-1 nil 3315152617
   ("" (grind-with-ext) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (reflexive? const-decl "bool" relations nil)
    (member const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil))
   shostak))
(irreflexive_kernel_identity 0
  (irreflexive_kernel_identity-1 nil 3315152638
   ("" (grind-with-ext) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (irreflexive? const-decl "bool" relations nil)
    (member const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (difference const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil))
   shostak))
(symmetric_closure_identity 0
  (symmetric_closure_identity-1 nil 3315152643
   ("" (grind-with-ext) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (symmetric? const-decl "bool" relations nil)
    (symmetric_converse application-judgement "(symmetric?[T])"
     relation_converse_props nil)
    (member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (symmetric_closure const-decl "(symmetric?)" closure_ops nil))
   shostak))
(symmetric_kernel_identity 0
  (symmetric_kernel_identity-1 nil 3315152648
   ("" (grind-with-ext :if-match all) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (PRED type-eq-decl nil defined_types nil)
    (symmetric? const-decl "bool" relations nil)
    (symmetric_converse application-judgement "(symmetric?[T])"
     relation_converse_props nil)
    (member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (intersection const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (symmetric_kernel const-decl "(symmetric?)" closure_ops nil))
   shostak))
(asymmetric_kernel_identity 0
  (asymmetric_kernel_identity-1 nil 3315152663
   ("" (grind-with-ext) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil closure_ops nil)
    (pred type-eq-decl nil defined_types nil)
    (asymmetric? const-decl "bool" relations_extra nil)
    (irreflexive_converse application-judgement "(irreflexive?[T])"
     relation_converse_props nil)
    (antisymmetric_converse application-judgement "(antisymmetric?[T])"
     relation_converse_props nil)
    (member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (difference const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (asymmetric_kernel const-decl "(asymmetric?)" closure_ops nil))
   shostak))
(transitive_closure_identity 0
  (transitive_closure_identity-1 nil 3315152670
   ("" (skolem-typepred)
    (("" (expand* "transitive_closure" "IUnion")
      (("" (decompose-equality)
        (("" (iff)
          (("" (prop)
            (("1"
              (case "FORALL (i: posnat), (a, b: T): iterate(lessp!1, i)(a, b) IMPLIES lessp!1(a, b)")
              (("1" (skolem!)
                (("1" (inst - "i!1" "x!1" "x!2")
                  (("1" (assert) nil nil)) nil))
                nil)
               ("2" (hide -1 2)
                (("2" (induct "i")
                  (("1" (assert) nil nil) ("2" (assert) nil nil)
                   ("3" (skosimp*)
                    (("3" (expand "iterate" -3)
                      (("3" (expand "o")
                        (("3" (skosimp)
                          (("3" (splash -1)
                            (("1" (inst - "a!1" "y!1")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "transitive?")
                                  (("1"
                                    (inst - "a!1" "y!1" "b!1")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "iterate")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst + 1) (("2" (rewrite "iterate_1") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((IUnion const-decl "set[T]" indexed_sets nil)
    (transitive_closure const-decl "(transitive?)" closure_ops nil)
    (iterate_1 formula-decl nil relation_iterate nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (O const-decl "bool" relation_props nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(preorder_closure_identity 0
  (preorder_closure_identity-1 nil 3315153008
   ("" (skolem!)
    (("" (rewrite "preorder_closure_reflexive_transitive")
      (("" (use "transitive_closure_identity")
        (("" (use "reflexive_closure_identity") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((preorder_closure_reflexive_transitive formula-decl nil closure_ops
     nil)
    (T formal-type-decl nil closure_ops nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (preorder? const-decl "bool" orders nil)
    (transitive_closure_of_reflexive application-judgement
     "(preorder?)" closure_ops nil)
    (reflexive_closure_preserves_transitive application-judgement
     "(preorder?)" closure_ops nil)
    (reflexive_closure_identity formula-decl nil closure_ops nil)
    (reflexive? const-decl "bool" relations nil)
    (transitive_closure const-decl "(transitive?)" closure_ops nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (transitive_closure_identity formula-decl nil closure_ops nil))
   shostak))
(preorder_closure_reflexive 0
  (preorder_closure_reflexive-1 nil 3318256600
   ("" (skolem-typepred)
    (("" (expand "order?")
      (("" (flatten)
        (("" (rewrite "preorder_closure_reflexive_transitive")
          (("" (rewrite "transitive_closure_identity") nil nil)) nil))
        nil))
      nil))
    nil)
   ((preorder_closure_reflexive_transitive formula-decl nil closure_ops
     nil)
    (reflexive_closure_preserves_transitive application-judgement
     "(preorder?)" closure_ops nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (transitive_closure_identity formula-decl nil closure_ops nil)
    (order? const-decl "bool" relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(equivalence_closure_identity 0
  (equivalence_closure_identity-1 nil 3315153106
   ("" (skolem-typepred)
    (("" (expand* "equivalence?" "equivalence_closure")
      (("" (flatten)
        (("" (use "symmetric_closure_identity")
          (("" (replace -1)
            (("" (use "preorder_closure_identity") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((equivalence_closure const-decl "(equivalence?)" closure_ops nil)
    (symmetric_closure_identity formula-decl nil closure_ops nil)
    (symmetric? const-decl "bool" relations nil)
    (preorder_closure_preserves_symmetry application-judgement
     "(equivalence?)" closure_ops nil)
    (pred type-eq-decl nil defined_types nil)
    (preorder? const-decl "bool" orders nil)
    (preorder_closure_identity formula-decl nil closure_ops nil)
    (equivalence? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil closure_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.32 Sekunden (vorverarbeitet) ¤

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.