feedback image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: copy_bw.xpm   Sprache: Unknown

(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)))

[ Dauer der Verarbeitung: 0.29 Sekunden  (vorverarbeitet)  ]