SSL relations_closure.prf

(relations_closure
 (RC_TCC1 0
  (RC_TCC1-1 nil 3370210023 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (reflexive? const-decl "bool" relations nil))
   nil))
 (change_to_RC 0
  (change_to_RC-1 nil 3375182313
   ("" (expand* "reflexive_closure" "RC") nil nil)
   ((RC const-decl "reflexive" relations_closure nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops
     "orders/"))
   shostak))
 (R_subset_RC 0
  (R_subset_RC-1 nil 3371210190
   ("" (skeep)
    (("" (expand* "subset?" "member")
      (("" (skeep)
        (("" (expand* "RC" "union" "member") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (RC const-decl "reflexive" relations_closure nil))
   shostak))
 (RC_idempotent 0
  (RC_idempotent-1 nil 3370210197
   ("" (skeep)
    (("" (lemma "reflexive_closure_identity")
      (("" (inst -1 "RC(R)")
        (("" (rewrite-lemma "change_to_RC" ("R" "RC(R)")) nil nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil relations_closure nil)
    (reflexive_closure_identity formula-decl nil closure_ops "orders/")
    (change_to_RC formula-decl nil relations_closure nil)
    (RC const-decl "reflexive" relations_closure nil)
    (reflexive type-eq-decl nil relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (RC_characterization 0
  (RC_characterization-1 nil 3370210321
   ("" (skeep)
    (("" (prop)
      (("1" (lemma "reflexive_closure_identity")
        (("1" (inst?)
          (("1" (rewrite-lemma "change_to_RC" ("R" "S"))
            (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (change_to_RC formula-decl nil relations_closure nil)
    (reflexive_closure_identity formula-decl nil closure_ops "orders/")
    (T formal-type-decl nil relations_closure nil))
   shostak))
 (SC_TCC1 0
  (SC_TCC1-1 nil 3370210023 ("" (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))
 (change_to_SC 0
  (change_to_SC-1 nil 3375182425
   ("" (expand* "symmetric_closure" "SC") nil nil)
   ((SC const-decl "symmetric" relations_closure nil)
    (symmetric_closure const-decl "(symmetric?)" closure_ops
     "orders/"))
   shostak))
 (R_subset_SC 0
  (R_subset_SC-1 nil 3371210082
   ("" (skeep)
    (("" (expand* "subset?" "member")
      (("" (skeep)
        (("" (expand* "SC" "union" "member") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (SC const-decl "symmetric" relations_closure nil))
   shostak))
 (SC_idempotent 0
  (SC_idempotent-1 nil 3370210671
   ("" (skeep)
    (("" (lemma "symmetric_closure_identity")
      (("" (inst -1 "SC(R)")
        (("" (rewrite-lemma "change_to_SC" ("R" "SC(R)")) nil nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil relations_closure nil)
    (symmetric_closure_identity formula-decl nil closure_ops "orders/")
    (change_to_SC formula-decl nil relations_closure nil)
    (SC const-decl "symmetric" relations_closure nil)
    (symmetric type-eq-decl nil relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (symmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (SC_characterization 0
  (SC_characterization-1 nil 3370210710
   ("" (skeep)
    (("" (prop)
      (("1" (lemma "symmetric_closure_identity")
        (("1" (inst?)
          (("1" (rewrite-lemma "change_to_SC" ("R" "S"))
            (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (symmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (change_to_SC formula-decl nil relations_closure nil)
    (symmetric_closure_identity formula-decl nil closure_ops "orders/")
    (T formal-type-decl nil relations_closure nil))
   shostak))
 (TC_TCC1 0
  (TC_TCC1-1 nil 3370210023
   ("" (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 relations_closure 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 "orders/")
    (transitive? const-decl "bool" relations nil)
    (IUnion const-decl "set[T]" indexed_sets nil))
   nil))
 (change_to_TC 0
  (change_to_TC-1 nil 3375182475
   ("" (expand* "transitive_closure" "TC") nil nil)
   ((TC const-decl "transitive" relations_closure nil)
    (transitive_closure const-decl "(transitive?)" closure_ops
     "orders/"))
   shostak))
 (R_subset_TC 0
  (R_subset_TC-1 nil 3371210276
   ("" (skeep)
    (("" (expand* "subset?" "member")
      (("" (skeep)
        (("" (expand* "TC" "IUnion")
          (("" (inst 1 "1") (("" (rewrite "iterate_1") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (TC const-decl "transitive" relations_closure nil)
    (T formal-type-decl nil relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (iterate_1 formula-decl nil relation_iterate "orders/")
    (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))
   shostak))
 (TC_converse 0
  (TC_converse-1 nil 3372708950
   ("" (skeep)
    (("" (decompose-equality)
      (("" (expand* "TC" "IUnion")
        (("" (iff)
          (("" (prop)
            (("1" (skolem * "i")
              (("1" (rewrite "iterate_converse")
                (("1" (expand "converse") (("1" (inst?) nil nil)) nil))
                nil))
              nil)
             ("2" (expand "converse" -1)
              (("2" (skolem * "i")
                (("2" (inst?)
                  (("2" (rewrite "iterate_converse")
                    (("2" (expand "converse") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((transitive_converse application-judgement "(transitive?[T])"
     relation_converse_props nil)
    (pred type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (transitive type-eq-decl nil relations_closure nil)
    (TC const-decl "transitive" relations_closure nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs 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 relations_closure 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)
    (iterate_converse formula-decl nil relation_iterate "orders/")
    (IUnion const-decl "set[T]" indexed_sets nil))
   shostak))
 (TC_idempotent 0
  (TC_idempotent-1 nil 3370214273
   ("" (skeep)
    (("" (lemma "transitive_closure_identity")
      (("" (inst -1 "TC(R)")
        (("" (rewrite-lemma "change_to_TC" ("R" "TC(R)")) nil nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil relations_closure nil)
    (transitive_closure_identity formula-decl nil closure_ops
     "orders/")
    (change_to_TC formula-decl nil relations_closure nil)
    (TC const-decl "transitive" relations_closure nil)
    (transitive type-eq-decl nil relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (TC_characterization 0
  (TC_characterization-1 nil 3370211587
   ("" (skeep)
    (("" (prop)
      (("1" (lemma "transitive_closure_identity")
        (("1" (inst?)
          (("1" (rewrite-lemma "change_to_TC" ("R" "S"))
            (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (change_to_TC formula-decl nil relations_closure nil)
    (transitive_closure_identity formula-decl nil closure_ops
     "orders/")
    (T formal-type-decl nil relations_closure nil))
   shostak))
 (RTC_TCC1 0
  (RTC_TCC1-1 nil 3370210023
   ("" (expand "reflexive_transitive?")
    (("" (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 "orders/")
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_closure 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 "orders/")
    (reflexive_transitive? const-decl "bool" relations_closure nil))
   nil))
 (change_to_RTC 0
  (change_to_RTC-1 nil 3375182493
   ("" (expand* "preorder_closure" "RTC") nil nil)
   ((RTC const-decl "reflexive_transitive" relations_closure nil)
    (preorder_closure const-decl "(preorder?)" closure_ops "orders/"))
   shostak))
 (R_subset_RTC 0
  (R_subset_RTC-1 nil 3371209765
   ("" (skeep)
    (("" (expand* "subset?" "member")
      (("" (skeep)
        (("" (expand* "RTC" "IUnion")
          (("" (inst 1 "1") (("" (rewrite "iterate_1") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (T formal-type-decl nil relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (iterate_1 formula-decl nil relation_iterate "orders/")
    (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))
   shostak))
 (iterate_RTC 0
  (iterate_RTC-1 nil 3372720815
   ("" (skeep)
    (("" (expand* "subset?" "member" "RTC" "IUnion")
      (("" (skeep) (("" (inst 1 "n") nil nil)) nil)) nil))
    nil)
   ((member const-decl "bool" sets nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (subset? const-decl "bool" sets 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))
   shostak))
 (RTC_idempotent 0
  (RTC_idempotent-1 nil 3370216879
   ("" (skeep)
    (("" (lemma " preorder_closure_identity")
      (("" (inst -1 "RTC(R)")
        (("1" (rewrite-lemma "change_to_RTC" ("R" "RTC(R)")) nil nil)
         ("2" (assert)
          (("2" (expand "preorder?")
            (("2" (hide 2)
              (("2" (typepred "RTC(R)")
                (("2" (expand "reflexive_transitive?")
                  (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil relations_closure nil)
    (preorder_closure_identity formula-decl nil closure_ops "orders/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (change_to_RTC formula-decl nil relations_closure 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)
    (reflexive_transitive? const-decl "bool" relations_closure nil)
    (reflexive_transitive type-eq-decl nil relations_closure nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (R skolem-const-decl "pred[[T, T]]" relations_closure nil))
   shostak))
 (RTC_characterization 0
  (RTC_characterization-1 nil 3370216958
   ("" (skeep)
    (("" (prop)
      (("1" (lemma " preorder_closure_identity")
        (("1" (inst?)
          (("1" (rewrite-lemma "change_to_RTC" ("R" "S"))
            (("1" (assert) nil nil)) nil)
           ("2" (expand* "reflexive_transitive?" "preorder?") nil nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
    (preorder? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (change_to_RTC formula-decl nil relations_closure nil)
    (reflexive_transitive? const-decl "bool" relations_closure nil)
    (preorder_closure_identity formula-decl nil closure_ops "orders/")
    (T formal-type-decl nil relations_closure nil))
   shostak))
 (EC_TCC1 0
  (EC_TCC1-1 nil 3375182313
   ("" (skeep)
    (("" (lemma "preorder_closure_preserves_symmetry")
      (("" (inst -1 "SC(R)")
        (("" (rewrite-lemma "change_to_RTC" ("R" "SC(R)")) nil nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil relations_closure nil)
    (preorder_closure_preserves_symmetry judgement-tcc nil closure_ops
     "orders/")
    (change_to_RTC formula-decl nil relations_closure nil)
    (SC const-decl "symmetric" relations_closure nil)
    (symmetric type-eq-decl nil relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (symmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (change_to_EC 0
  (change_to_EC-1 nil 3375182512
   ("" (skeep)
    (("" (expand* "equivalence_closure" "EC")
      (("" (rewrite-lemma "change_to_SC" ("R" "R"))
        (("" (rewrite-lemma "change_to_RTC" ("R" "SC(R)")) nil nil))
        nil))
      nil))
    nil)
   ((EC const-decl "equivalence" relations_closure nil)
    (equivalence_closure const-decl "(equivalence?)" closure_ops
     "orders/")
    (change_to_RTC formula-decl nil relations_closure nil)
    (PRED type-eq-decl nil defined_types nil)
    (symmetric? const-decl "bool" relations nil)
    (symmetric type-eq-decl nil relations_closure nil)
    (SC const-decl "symmetric" relations_closure 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 relations_closure nil)
    (change_to_SC formula-decl nil relations_closure nil))
   shostak))
 (R_subset_EC 0
  (R_subset_EC-1 nil 3371210430
   ("" (skeep)
    (("" (lemma "R_subset_SC")
      (("" (inst?)
        (("" (expand* "subset?" "member")
          (("" (skeep)
            (("" (inst?)
              (("" (expand "EC")
                (("" (expand* "RTC" "IUnion")
                  (("" (inst 1 "1")
                    (("" (rewrite "iterate_1") (("" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((R_subset_SC formula-decl nil relations_closure nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (SC const-decl "symmetric" relations_closure nil)
    (symmetric type-eq-decl nil relations_closure nil)
    (symmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (iterate_1 formula-decl nil relation_iterate "orders/")
    (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)
    (EC const-decl "equivalence" relations_closure 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 relations_closure nil))
   shostak))
 (RTC_subset_EC 0
  (RTC_subset_EC-1 nil 3372883240
   ("" (skeep)
    (("" (expand "EC")
      (("" (lemma "R_subset_SC")
        (("" (inst?)
          (("" (lemma "preorder_closure_is_monotone")
            (("" (inst -1 "R" "SC(R)")
              (("" (rewrite-lemma "change_to_RTC" ("R" "R"))
                (("" (rewrite-lemma "change_to_RTC" ("R" "SC(R)"))
                  (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((EC const-decl "equivalence" relations_closure nil)
    (T formal-type-decl nil relations_closure nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (PRED type-eq-decl nil defined_types nil)
    (symmetric? const-decl "bool" relations nil)
    (symmetric type-eq-decl nil relations_closure nil)
    (SC const-decl "symmetric" relations_closure nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (change_to_RTC formula-decl nil relations_closure nil)
    (preorder_closure_is_monotone formula-decl nil closure_ops
     "orders/")
    (R_subset_SC formula-decl nil relations_closure nil))
   shostak))
 (EC_idempotent 0
  (EC_idempotent-1 nil 3370261011
   ("" (skeep)
    (("" (lemma "equivalence_closure_identity")
      (("" (inst -1 "EC(R)")
        (("" (rewrite-lemma "change_to_EC" ("R" "EC(R)")) nil nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil relations_closure nil)
    (equivalence_closure_identity formula-decl nil closure_ops
     "orders/")
    (change_to_EC formula-decl nil relations_closure nil)
    (EC const-decl "equivalence" relations_closure nil)
    (equivalence type-eq-decl nil relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (equivalence? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (EC_characterization 0
  (EC_characterization-1 nil 3370261180
   ("" (skeep)
    (("" (prop)
      (("1" (lemma "equivalence_closure_identity")
        (("1" (inst?)
          (("1" (rewrite-lemma "change_to_EC" ("R" "S"))
            (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (equivalence? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (change_to_EC formula-decl nil relations_closure nil)
    (equivalence_closure_identity formula-decl nil closure_ops
     "orders/")
    (T formal-type-decl nil relations_closure nil))
   shostak)))