products/Sources/formale Sprachen/PVS/TRS image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: relations_closure.prf   Sprache: Lisp

Original von: PVS©

(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") (("" (assertnil 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" (assertnil nil)) nil))
          nil))
        nil)
       ("2" (assertnil 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") (("" (assertnil 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" (assertnil nil)) nil))
          nil))
        nil)
       ("2" (assertnil 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" (assertnil nil)) nil))
          nil))
        nil)
       ("2" (assertnil 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" (assertnil nil)) nil)
           ("2" (expand"reflexive_transitive?" "preorder?"nil nil))
          nil))
        nil)
       ("2" (assertnil 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") (("" (assertnil 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)"))
                  (("" (assertnil 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" (assertnil nil)) nil))
          nil))
        nil)
       ("2" (assertnil 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)))


¤ Dauer der Verarbeitung: 0.13 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff