Quellcodebibliothek Statistik Leitseite    (Beweissystem der NASA Version 6.0.9©)  

 relations_closure.prf   Interaktion und
PortierbarkeitLisp

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

97%


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

*Eine klare Vorstellung vom Zielzustand




Normalansicht

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.