Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: results_normal_form.prf Sprache: Lisp

Original von: PVS^©

(results_normal_form
(NF_doesnot_rewrite 0
  (NF_doesnot_rewrite-1 nil 3374065344
   ("" (skeep)
    (("" (expand "is_normal_form?")
      (("" (expand* "RTC" "IUnion")
        (("" (skolem * "i")
          (("" (expand "reducible?")
            (("" (case "i = 0")
              (("1" (replace -1)
                (("1" (expand "iterate") (("1" (propax) nil nil)) nil))
                nil)
               ("2" (lemma "iterate_add_one")
                (("2" (inst? -1 ("R" "R" "n" "i -1"))
                  (("1" (assert)
                    (("1" (decompose-equality)
                      (("1" (inst? -1 ("x" "(x,y)"))
                        (("1" (iff)
                          (("1" (prop)
                            (("1" (expand "o")
                              (("1"
                                (skolem * "z")
                                (("1"
                                  (flatten)
                                  (("1" (inst 2 "z") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil) ("3" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_normal_form? const-decl "bool" ars_terminology 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (i skolem-const-decl "nat" results_normal_form nil)
    (PRED type-eq-decl nil defined_types nil)
    (pred type-eq-decl nil defined_types nil)
    (O const-decl "bool" relation_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (T formal-type-decl nil results_normal_form nil)
    (iterate_add_one formula-decl nil relation_iterate "orders/")
    (reducible? const-decl "bool" ars_terminology nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (IUnion const-decl "set[T]" indexed_sets nil))
   shostak))
(NF_implies_RTC 0
  (NF_implies_RTC-1 nil 3374065407
   ("" (skeep)
    (("" (lemma "CR_iff_Confluent")
      (("" (inst?)
        (("" (prop)
          (("" (hide (-2 -3))
            (("" (expand "church_rosser?")
              (("" (inst -1 "x" "y")
                (("" (prop)
                  (("" (expand "joinable?")
                    (("" (skolem * "z")
                      (("" (flatten)
                        (("" (lemma "NF_doesnot_rewrite")
                          (("" (inst -1 "R" "y" "z")
                            (("" (prop)
                              ((""
                                (replace -1)
                                (("" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil results_normal_form nil)
    (CR_iff_Confluent formula-decl nil results_confluence nil)
    (church_rosser? const-decl "bool" ars_terminology nil)
    (NF_doesnot_rewrite formula-decl nil results_normal_form nil)
    (joinable? const-decl "bool" ars_terminology 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))
(NFs_implies_Equal 0
  (NFs_implies_Equal-1 nil 3374065575
   ("" (skeep)
    (("" (lemma "CR_iff_Confluent")
      (("" (inst?)
        (("" (prop)
          (("" (hide (-2 -3))
            (("" (expand "church_rosser?")
              (("" (inst -1 "x" "y")
                (("" (prop)
                  (("" (hide -2)
                    (("" (expand "joinable?")
                      (("" (skolem * "z")
                        (("" (flatten)
                          (("" (lemma "NF_doesnot_rewrite")
                            (("" (copy -1)
                              ((""
                                (inst -1 "R" "y" "z")
                                ((""
                                  (inst -2 "R" "x" "z")
                                  ((""
                                    (prop)
                                    (("" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil results_normal_form nil)
    (CR_iff_Confluent formula-decl nil results_confluence nil)
    (church_rosser? const-decl "bool" ars_terminology nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (NF_doesnot_rewrite formula-decl nil results_normal_form 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))
(Norm_and_Confl_implies_UNF 0
  (Norm_and_Confl_implies_UNF-1 nil 3374065658
   ("" (skeep)
    (("" (skeep)
      (("" (expand "has_unique_nf?")
        (("" (expand "normalizing?")
          (("" (inst -1 "x")
            (("" (skolem * "y")
              (("" (inst 1 "y")
                (("" (assert)
                  (("" (skeep)
                    (("" (expand "normal_form?")
                      (("" (flatten)
                        (("" (expand "confluent?")
                          (("" (inst -3 "x" "y" "z")
                            (("" (assert)
                              ((""
                                (hide (-1 -4))
                                ((""
                                  (expand "joinable?")
                                  ((""
                                    (skolem * "r")
                                    ((""
                                      (lemma "NF_doesnot_rewrite")
                                      ((""
                                        (copy -1)
                                        ((""
                                          (inst -1 "R" "y" "r")
                                          ((""
                                            (inst -2 "R" "z" "r")
                                            ((""
                                              (prop)
                                              (("" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((normalizing? const-decl "bool" ars_terminology nil)
    (normal_form? const-decl "bool" ars_terminology nil)
    (confluent? const-decl "bool" ars_terminology nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (NF_doesnot_rewrite formula-decl nil results_normal_form 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 results_normal_form nil)
    (has_unique_nf? const-decl "bool" ars_terminology nil))
   shostak))
(Normalizing_and_Confl 0
  (Normalizing_and_Confl-1 nil 3374065828
   ("" (skeep)
    (("" (lemma "Norm_and_Confl_implies_UNF")
      (("" (copy -1)
        (("" (inst?)
          (("" (inst?)
            (("" (assert)
              (("" (inst -1 "x")
                (("" (inst -2 "y")
                  (("" (expand "has_unique_nf?")
                    (("" (skolem * "u")
                      (("" (skolem * "v")
                        (("" (inst 1 "u" "v")
                          (("" (prop)
                            (("1" (expand "normal_form?")
                              (("1"
                                (flatten)
                                (("1"
                                  (hide (-1 -2 -6 -9 -10))
                                  (("1"
                                    (lemma "CR_iff_Confluent")
                                    (("1"
                                      (inst?)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (expand "church_rosser?")
                                          (("1"
                                            (inst -1 "x" "y")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (expand "joinable?")
                                                (("1"
                                                  (skolem * "z")
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (copy -8)
                                                      (("1"
                                                        (expand
                                                         "confluent?"
                                                         -9)
                                                        (("1"
                                                          (copy -9)
                                                          (("1"
                                                            (inst
                                                             -1
                                                             "x"
                                                             "z"
                                                             "u")
                                                            (("1"
                                                              (inst
                                                               -10
                                                               "y"
                                                               "z"
                                                               "v")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (hide-all-but
                                                                   (-1
                                                                    -2
                                                                    -7
                                                                    -9
                                                                    -10
                                                                    1))
                                                                  (("1"
                                                                    (lemma
                                                                     "Joinable_implies_Equiv")
                                                                    (("1"
                                                                      (copy
                                                                       -1)
                                                                      (("1"
                                                                        (inst
                                                                         -1
                                                                         "R"
                                                                         "z"
                                                                         "u")
                                                                        (("1"
                                                                          (inst
                                                                           -2
                                                                           "R"
                                                                           "z"
                                                                           "v")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (hide
                                                                               (-3
                                                                                -7))
                                                                              (("1"
                                                                                (typepred
                                                                                 "EC(R)")
                                                                                (("1"
                                                                                  (expand
                                                                                   "equivalence?")
                                                                                  (("1"
                                                                                    (flatten)
                                                                                    (("1"
                                                                                      (hide
                                                                                       -1)
                                                                                      (("1"
                                                                                        (expand*
                                                                                         "symmetric?"
                                                                                         "transitive?")
                                                                                        (("1"
                                                                                          (copy
                                                                                           -1)
                                                                                          (("1"
                                                                                            (inst
                                                                                             -1
                                                                                             "z"
                                                                                             "u")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -2
                                                                                               "z"
                                                                                               "v")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (hide
                                                                                                   (-4
                                                                                                    -5))
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     -3
                                                                                                     "u"
                                                                                                     "z"
                                                                                                     "v")
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      (("1"
                                                                                                        (hide
                                                                                                         (-1
                                                                                                          -2))
                                                                                                        (("1"
                                                                                                          (lemma
                                                                                                           "NFs_implies_Equal")
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -1
                                                                                                             "R"
                                                                                                             "u"
                                                                                                             "v")
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but (-2 -3 1))
                              (("2"
                                (expand "unique_nf?")
                                (("2" (assert) nil nil))
                                nil))
                              nil)
                             ("3" (hide-all-but (-4 -5 1))
                              (("3"
                                (expand "unique_nf?")
                                (("3" (assert) nil nil))
                                nil))
                              nil)
                             ("4" (replace -1)
                              (("4"
                                (expand "normal_form?")
                                (("4"
                                  (flatten)
                                  (("4"
                                    (hide-all-but (-2 -5 1))
                                    (("4"
                                      (case "joinable?(R)(x,y)")
                                      (("1"
                                        (lemma
                                         "Joinable_implies_Equiv")
                                        (("1"
                                          (inst -1 "R" "x" "y")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (expand "joinable?")
                                          (("2"
                                            (inst 1 "v")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Norm_and_Confl_implies_UNF formula-decl nil results_normal_form
     nil)
    (T formal-type-decl nil results_normal_form nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (unique_nf? const-decl "bool" ars_terminology nil)
    (normal_form? const-decl "bool" ars_terminology nil)
    (church_rosser? const-decl "bool" ars_terminology nil)
    (NFs_implies_Equal formula-decl nil results_normal_form nil)
    (symmetric? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Joinable_implies_Equiv formula-decl nil results_confluence nil)
    (confluent? const-decl "bool" ars_terminology nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (CR_iff_Confluent formula-decl nil results_confluence nil)
    (has_unique_nf? const-decl "bool" ars_terminology nil))
   shostak))
(Normal_Confl_iff_UNF 0
  (Normal_Confl_iff_UNF-1 nil 3374065911
   ("" (skeep)
    (("" (prop)
      (("1" (rewrite "Norm_and_Confl_implies_UNF") nil nil)
       ("2" (expand "normalizing?")
        (("2" (skeep)
          (("2" (inst -1 "x")
            (("2" (expand "has_unique_nf?")
              (("2" (skolem * "u")
                (("2" (inst 1 "u") (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (copy -1)
        (("3" (copy -1)
          (("3" (expand "confluent?")
            (("3" (skeep)
              (("3" (inst -1 "y")
                (("3" (inst -2 "z")
                  (("3" (inst -5 "x")
                    (("3" (expand "has_unique_nf?")
                      (("3" (skolem * "y1")
                        (("3" (skolem * "z1")
                          (("3" (skolem * "x1")
                            (("3" (flatten)
                              (("3"
                                (hide (-2 -4))
                                (("3"
                                  (expand "normal_form?")
                                  (("3"
                                    (flatten)
                                    (("3"
                                      (typepred "RTC(R)")
                                      (("3"
                                        (expand
                                         "reflexive_transitive?")
                                        (("3"
                                          (flatten)
                                          (("3"
                                            (hide -1)
                                            (("3"
                                              (expand "transitive?")
                                              (("3"
                                                (copy -1)
                                                (("3"
                                                  (inst
                                                   -1
                                                   "x"
                                                   "y"
                                                   "y1")
                                                  (("3"
                                                    (inst
                                                     -2
                                                     "x"
                                                     "z"
                                                     "z1")
                                                    (("3"
                                                      (assert)
                                                      (("3"
                                                        (copy -11)
                                                        (("3"
                                                          (inst
                                                           -1
                                                           "y1")
                                                          (("3"
                                                            (inst
                                                             -12
                                                             "z1")
                                                            (("3"
                                                              (assert)
                                                              (("3"
                                                                (replace
                                                                 -1)
                                                                (("3"
                                                                  (replace
                                                                   -12
                                                                   -6
                                                                   rl)
                                                                  (("3"
                                                                    (hide-all-but
                                                                     (-4
                                                                      -6
                                                                      1))
                                                                    (("3"
                                                                      (expand
                                                                       "joinable?")
                                                                      (("3"
                                                                        (inst
                                                                         1
                                                                         "y1")
                                                                        (("3"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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 results_normal_form nil)
    (Norm_and_Confl_implies_UNF formula-decl nil results_normal_form
     nil)
    (has_unique_nf? const-decl "bool" ars_terminology nil)
    (normalizing? const-decl "bool" ars_terminology nil)
    (normal_form? const-decl "bool" ars_terminology nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (reflexive_transitive type-eq-decl nil relations_closure nil)
    (reflexive_transitive? const-decl "bool" relations_closure nil)
    (pred type-eq-decl nil defined_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (transitive? const-decl "bool" relations nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (confluent? const-decl "bool" ars_terminology nil))
   shostak))
(Noetherian_implies_normalizing 0
  (Noetherian_implies_normalizing-1 nil 3374068005
   ("" (skeep)
    (("" (expand "normalizing?")
      (("" (skeep)
        (("" (expand "noetherian?")
          (("" (expand "well_founded?")
            (("" (inst -1 "reduct?(R)(x)")
              (("" (split)
                (("1" (skolem * "a")
                  (("1" (inst 1 "a")
                    (("1" (typepred "a")
                      (("1" (expand "reduct?")
                        (("1" (expand "normal_form?")
                          (("1" (split)
                            (("1" (propax) nil nil)
                             ("2" (expand "is_normal_form?")
                              (("2"
                                (expand "reducible?")
                                (("2"
                                  (skolem * "b")
                                  (("2"
                                    (inst -3 "b")
                                    (("1"
                                      (expand "converse")
                                      (("1" (propax) nil nil))
                                      nil)
                                     ("2"
                                      (lemma "R_subset_RTC")
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (expand* "subset?" "member")
                                          (("2"
                                            (inst -1 "(a, b)")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (typepred "RTC(R)")
                                                (("2"
                                                  (expand
                                                   "reflexive_transitive?")
                                                  (("2"
                                                    (flatten)
                                                    (("2"
                                                      (hide -1)
                                                      (("2"
                                                        (expand
                                                         "transitive?")
                                                        (("2"
                                                          (inst
                                                           -1
                                                           "x"
                                                           "a"
                                                           "b")
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (expand
                                                               "reduct?")
                                                              (("2"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (inst 1 "x")
                    (("2" (expand "reduct?")
                      (("2" (expand* "RTC" "IUnion")
                        (("2" (inst 1 "0")
                          (("2" (expand "iterate")
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((normalizing? const-decl "bool" ars_terminology nil)
    (noetherian? const-decl "bool" noetherian nil)
    (T formal-type-decl nil results_normal_form 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)
    (reduct? const-decl "PRED[T]" ars_terminology 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 "orders/")
    (IUnion const-decl "set[T]" indexed_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (normal_form? const-decl "bool" ars_terminology nil)
    (is_normal_form? const-decl "bool" ars_terminology nil)
    (R_subset_RTC formula-decl nil relations_closure nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (transitive? const-decl "bool" relations nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (reflexive_transitive type-eq-decl nil relations_closure nil)
    (reflexive_transitive? const-decl "bool" relations_closure nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (b skolem-const-decl "T" results_normal_form nil)
    (x skolem-const-decl "T" results_normal_form nil)
    (R skolem-const-decl "PRED[[T, T]]" results_normal_form nil)
    (reducible? const-decl "bool" ars_terminology nil)
    (well_founded? const-decl "bool" orders nil))
   shostak))
(Convergent_UNF 0
  (Convergent_UNF-1 nil 3374068143
   ("" (skeep)
    (("" (expand "convergent?")
      (("" (flatten)
        (("" (lemma "Noetherian_implies_normalizing")
          (("" (inst?)
            (("" (assert)
              (("" (lemma "Norm_and_Confl_implies_UNF")
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" noetherian nil)
    (Noetherian_implies_normalizing formula-decl nil
     results_normal_form nil)
    (Norm_and_Confl_implies_UNF formula-decl nil results_normal_form
     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 results_normal_form nil))
   shostak))
(Noet_and_Confl_iff_UNF 0
  (Noet_and_Confl_iff_UNF-1 nil 3374068168
   ("" (skeep)
    (("" (lemma "Noetherian_implies_normalizing")
      (("" (inst?)
        (("" (assert)
          (("" (hide -2)
            (("" (lemma "Normal_Confl_iff_UNF")
              (("" (inst?) (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Noetherian_implies_normalizing formula-decl nil
     results_normal_form nil)
    (Normal_Confl_iff_UNF formula-decl nil results_normal_form 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 results_normal_form nil))
   shostak))
(Convergent_iff_eqNF 0
  (Convergent_iff_eqNF-1 nil 3374068205
   ("" (skeep)
    (("" (split)
      (("1" (flatten)
        (("1" (skeep)
          (("1" (expand "normal_form?")
            (("1" (flatten)
              (("1" (lemma "RTC_subset_EC")
                (("1" (inst?)
                  (("1" (copy -1)
                    (("1" (expand* "subset?" "member")
                      (("1" (inst -1 "(x, u)")
                        (("1" (inst -2 "(y, v)")
                          (("1" (assert)
                            (("1" (hide (-4 -6))
                              (("1"
                                (typepred "EC(R)")
                                (("1"
                                  (expand "equivalence?")
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (expand*
                                         "symmetric?"
                                         "transitive?")
                                        (("1"
                                          (inst -1 "x" "u")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (copy -2)
                                              (("1"
                                                (inst -1 "u" "x" "y")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (inst
                                                     -3
                                                     "u"
                                                     "y"
                                                     "v")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (expand
                                                         "convergent?")
                                                        (("1"
                                                          (flatten)
                                                          (("1"
                                                            (hide-all-but
                                                             (-3
                                                              -7
                                                              -8
                                                              -9
                                                              1))
                                                            (("1"
                                                              (lemma
                                                               "NFs_implies_Equal")
                                                              (("1"
                                                                (inst?)
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (flatten)
        (("2" (expand "convergent?")
          (("2" (flatten)
            (("2" (lemma "Noetherian_implies_normalizing")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (expand "normalizing?")
                    (("2" (copy -1)
                      (("2" (inst -1 "x")
                        (("2" (inst -2 "y")
                          (("2" (skolem * "u")
                            (("2" (skolem * "v")
                              (("2"
                                (inst -3 "u" "v")
                                (("2"
                                  (assert)
                                  (("2"
                                    (expand "normal_form?")
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (replaces -5)
                                        (("2"
                                          (hide-all-but (-1 -3 1))
                                          (("2"
                                            (case "joinable?(R)(x, y)")
                                            (("1"
                                              (rewrite
                                               "Joinable_implies_Equiv")
                                              nil
                                              nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (expand "joinable?")
                                                (("2"
                                                  (inst 1 "v")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (NFs_implies_Equal formula-decl nil results_normal_form nil)
    (convergent? const-decl "bool" noetherian nil)
    (symmetric? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (equivalence? const-decl "bool" relations nil)
    (equivalence type-eq-decl nil relations_closure nil)
    (EC const-decl "equivalence" relations_closure nil)
    (RTC_subset_EC formula-decl nil relations_closure nil)
    (T formal-type-decl nil results_normal_form nil)
    (normal_form? const-decl "bool" ars_terminology nil)
    (Noetherian_implies_normalizing formula-decl nil
     results_normal_form nil)
    (Joinable_implies_Equiv formula-decl nil results_confluence nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (normalizing? const-decl "bool" ars_terminology nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.51 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.