Quelle  modulo_equivalence.prf

(modulo_equivalence
 (van_oostrom94 0
  (van_oostrom94-1 nil 3383390315
   ("" (skeep)
    (("" (expand* "diamond_property?" "confluent_m?")
      (("" (skeep)
        (("" (copy -1)
          (("" (inst -1 "x" "y" "z")
            (("" (typepred "Eq")
              (("" (expand "equivalence?")
                (("" (flatten)
                  (("" (prop)
                    (("1" (skolem * "u1")
                      (("1" (flatten)
                        (("1" (expand "o" (-1 -2))
                          (("1" (skolem * "u2")
                            (("1" (skolem * "u")
                              (("1"
                                (flatten)
                                (("1"
                                  (copy -7)
                                  (("1"
                                    (expand "transitive?" -1)
                                    (("1"
                                      (copy -7)
                                      (("1"
                                        (expand "symmetric?" -1)
                                        (("1"
                                          (inst -1 "u" "u1")
                                          (("1"
                                            (inst -2 "u2" "u1" "u")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (hide (-1 -4 -6))
                                                (("1"
                                                  (inst -7 "y" "u" "w")
                                                  (("1"
                                                    (prop)
                                                    (("1"
                                                      (skolem * "v2")
                                                      (("1"
                                                        (flatten)
                                                        (("1"
                                                          (expand "o")
                                                          (("1"
                                                            (skolem
                                                             *
                                                             "v1")
                                                            (("1"
                                                              (skolem
                                                               *
                                                               "v")
                                                              (("1"
                                                                (flatten)
                                                                (("1"
                                                                  (copy
                                                                   -10)
                                                                  (("1"
                                                                    (expand
                                                                     "transitive?"
                                                                     -1)
                                                                    (("1"
                                                                      (copy
                                                                       -10)
                                                                      (("1"
                                                                        (expand
                                                                         "symmetric?"
                                                                         -1)
                                                                        (("1"
                                                                          (inst
                                                                           -1
                                                                           "v"
                                                                           "v2")
                                                                          (("1"
                                                                            (inst
                                                                             -2
                                                                             "v1"
                                                                             "v2"
                                                                             "v")
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (typepred
                                                                                 "RTC(R)")
                                                                                (("1"
                                                                                  (expand
                                                                                   "reflexive_transitive?")
                                                                                  (("1"
                                                                                    (flatten)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "transitive?"
                                                                                       -2)
                                                                                      (("1"
                                                                                        (inst
                                                                                         -2
                                                                                         "z"
                                                                                         "u"
                                                                                         "v1")
                                                                                        (("1"
                                                                                          (assert)
                                                                                          (("1"
                                                                                            (hide-all-but
                                                                                             (-2
                                                                                              -4
                                                                                              -7
                                                                                              1))
                                                                                            (("1"
                                                                                              (expand
                                                                                               "joinable_m?")
                                                                                              (("1"
                                                                                                (inst
                                                                                                 1
                                                                                                 "v1"
                                                                                                 "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)
                                                     ("2"
                                                      (expand "o")
                                                      (("2"
                                                        (inst 1 "u2")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (expand "o")
                                                      (("3"
                                                        (inst 1 "w")
                                                        (("3"
                                                          (expand
                                                           "reflexive?")
                                                          (("3"
                                                            (inst
                                                             -4
                                                             "w")
                                                            (("3"
                                                              (assert)
                                                              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 (-6 1))
                      (("2" (expand "o" 1)
                        (("2" (inst 1 "x")
                          (("2" (typepred "RTC(R)")
                            (("2" (expand "reflexive_transitive?")
                              (("2"
                                (flatten)
                                (("2"
                                  (expand "reflexive?")
                                  (("2"
                                    (inst -1 "x")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("3" (hide-all-but (-1 -5 1))
                      (("3" (expand "o" 1)
                        (("3" (inst 1 "z")
                          (("3" (expand "reflexive?")
                            (("3" (inst -1 "z")
                              (("3" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((confluent_m? const-decl "bool" modulo_equivalence nil)
    (diamond_property? const-decl "bool" ars_terminology nil)
    (equivalence type-eq-decl nil relations_closure nil)
    (equivalence? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (O const-decl "bool" relation_props nil)
    (reflexive? const-decl "bool" relations nil)
    (joinable_m? const-decl "bool" modulo_equivalence 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)
    (symmetric? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (T formal-type-decl nil modulo_equivalence nil))
   shostak))
 (newman_lemma_general 0
  (newman_lemma_general-1 nil 3383388017
   ("" (skeep)
    (("" (split)
      (("1" (flatten)
        (("1" (lemma "van_oostrom94")
          (("1" (inst?)
            (("1" (assert)
              (("1" (hide 2)
                (("1" (lemma "noetherian_induction")
                  (("1" (inst?)
                    (("1" (expand "diamond_property?")
                      (("1" (skeep)
                        (("1"
                          (inst -1
                           "(LAMBDA (a: T): (FORALL (b, c: T):(RTC(R) o Eq)(a, b) AND (RTC(R) o Eq)(a, c) IMPLIES joinable_m?(R, Eq)(c, b)))")
                          (("1" (split)
                            (("1" (inst -1 "x" "y" "z")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "joinable_m?")
                                  (("1"
                                    (skolem -1 ("u" "v"))
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (inst 1 "u")
                                        (("1"
                                          (split)
                                          (("1"
                                            (expand "o" 1)
                                            (("1"
                                              (inst 1 "v")
                                              (("1"
                                                (typepred "Eq")
                                                (("1"
                                                  (expand*
                                                   "equivalence?"
                                                   "symmetric?")
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (inst -2 "u" "v")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "o" 1)
                                            (("2"
                                              (inst 1 "u")
                                              (("2"
                                                (typepred "Eq")
                                                (("2"
                                                  (expand*
                                                   "equivalence?"
                                                   "reflexive?")
                                                  (("2"
                                                    (flatten)
                                                    (("2"
                                                      (inst -1 "u")
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2)
                              (("2"
                                (skolem 1 "a")
                                (("2"
                                  (flatten)
                                  (("2"
                                    (skeep)
                                    (("2"
                                      (hide (-4 -5))
                                      (("2"
                                        (expand "o" (-2 -3))
                                        (("2"
                                          (skolem * "b2")
                                          (("2"
                                            (skolem * "c2")
                                            (("2"
                                              (flatten)
                                              (("2"
                                                (expand "RTC" (-2 -4))
                                                (("2"
                                                  (expand
                                                   "IUnion"
                                                   (-2 -4))
                                                  (("2"
                                                    (skolem * "i")
                                                    (("2"
                                                      (skolem * "j")
                                                      (("2"
                                                        (case-replace
                                                         "i = 0"
                                                         :hide?
                                                         t)
                                                        (("1"
                                                          (case-replace
                                                           "j = 0"
                                                           :hide?
                                                           t)
                                                          (("1"
                                                            (expand
                                                             "iterate")
                                                            (("1"
                                                              (replace
                                                               -2
                                                               -3
                                                               rl)
                                                              (("1"
                                                                (replace
                                                                 -4
                                                                 -5
                                                                 rl)
                                                                (("1"
                                                                  (hide-all-but
                                                                   (-3
                                                                    -5
                                                                    1))
                                                                  (("1"
                                                                    (expand
                                                                     "joinable_m?")
                                                                    (("1"
                                                                      (inst
                                                                       1
                                                                       "c"
                                                                       "b")
                                                                      (("1"
                                                                        (typepred
                                                                         "RTC(R)")
                                                                        (("1"
                                                                          (typepred
                                                                           "Eq")
                                                                          (("1"
                                                                            (expand
                                                                             "reflexive_transitive?")
                                                                            (("1"
                                                                              (flatten)
                                                                              (("1"
                                                                                (hide
                                                                                 -3)
                                                                                (("1"
                                                                                  (expand*
                                                                                   "equivalence?"
                                                                                   "transitive?"
                                                                                   "reflexive?"
                                                                                   "symmetric?")
                                                                                  (("1"
                                                                                    (flatten)
                                                                                    (("1"
                                                                                      (inst
                                                                                       -2
                                                                                       "a"
                                                                                       "c")
                                                                                      (("1"
                                                                                        (inst
                                                                                         -3
                                                                                         "c"
                                                                                         "a"
                                                                                         "b")
                                                                                        (("1"
                                                                                          (copy
                                                                                           -4)
                                                                                          (("1"
                                                                                            (inst
                                                                                             -1
                                                                                             "c")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -5
                                                                                               "b")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "iterate"
                                                             -2)
                                                            (("2"
                                                              (replace
                                                               -2
                                                               -3
                                                               rl)
                                                              (("2"
                                                                (hide
                                                                 -2)
                                                                (("2"
                                                                  (lemma
                                                                   iterate_add_one)
                                                                  (("2"
                                                                    (inst?
                                                                     -1
                                                                     ("R"
                                                                      "R"
                                                                      "n"
                                                                      "j - 1"))
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (decompose-equality)
                                                                        (("1"
                                                                          (inst
                                                                           -1
                                                                           "(a, c2)")
                                                                          (("1"
                                                                            (replaces
                                                                             -1)
                                                                            (("1"
                                                                              (expand
                                                                               "o"
                                                                               -3)
                                                                              (("1"
                                                                                (skolem
                                                                                 -3
                                                                                 "c1")
                                                                                (("1"
                                                                                  (flatten)
                                                                                  (("1"
                                                                                    (lemma
                                                                                     "iterate_RTC")
                                                                                    (("1"
                                                                                      (inst
                                                                                       -1
                                                                                       "R"
                                                                                       "j - 1")
                                                                                      (("1"
                                                                                        (expand*
                                                                                         "subset?"
                                                                                         "member")
                                                                                        (("1"
                                                                                          (inst
                                                                                           -1
                                                                                           "(c1, c2)")
                                                                                          (("1"
                                                                                            (expand
                                                                                             "locally_coherent?")
                                                                                            (("1"
                                                                                              (typepred
                                                                                               "Eq")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "equivalence?")
                                                                                                (("1"
                                                                                                  (flatten)
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     -12
                                                                                                     "a"
                                                                                                     "c1"
                                                                                                     "b")
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      (("1"
                                                                                                        (hide
                                                                                                         (-8
                                                                                                          -11))
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "joinable_m?")
                                                                                                          (("1"
                                                                                                            (skolem
                                                                                                             -10
                                                                                                             ("d1"
                                                                                                              "d2"))
                                                                                                            (("1"
                                                                                                              (flatten)
                                                                                                              (("1"
                                                                                                                (inst
                                                                                                                 -5
                                                                                                                 "c1")
                                                                                                                (("1"
                                                                                                                  (lemma
                                                                                                                   "R_subset_TC")
                                                                                                                  (("1"
                                                                                                                    (inst?)
                                                                                                                    (("1"
                                                                                                                      (expand*
                                                                                                                       "subset?"
                                                                                                                       "member")
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -1
                                                                                                                         "(a, c1)")
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          (("1"
                                                                                                                            (inst
                                                                                                                             -6
                                                                                                                             "d2"
                                                                                                                             "c")
                                                                                                                            (("1"
                                                                                                                              (prop)
                                                                                                                              (("1"
                                                                                                                                (skolem
                                                                                                                                 *
                                                                                                                                 ("r1"
                                                                                                                                  "r2"))
                                                                                                                                (("1"
                                                                                                                                  (flatten)
                                                                                                                                  (("1"
                                                                                                                                    (typepred
                                                                                                                                     "RTC(R)")
                                                                                                                                    (("1"
                                                                                                                                      (expand
                                                                                                                                       "reflexive_transitive?")
                                                                                                                                      (("1"
                                                                                                                                        (flatten)
                                                                                                                                        (("1"
                                                                                                                                          (expand
                                                                                                                                           "transitive?"
                                                                                                                                           -2)
                                                                                                                                          (("1"
                                                                                                                                            (inst
                                                                                                                                             -2
                                                                                                                                             "b"
                                                                                                                                             "d2"
                                                                                                                                             "r2")
                                                                                                                                            (("1"
                                                                                                                                              (inst
                                                                                                                                               2
                                                                                                                                               "r1"
                                                                                                                                               "r2")
                                                                                                                                              (("1"
                                                                                                                                                (assert)
                                                                                                                                                nil
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil)
                                                                                                                               ("2"
                                                                                                                                (expand
                                                                                                                                 "o"
                                                                                                                                 1)
                                                                                                                                (("2"
                                                                                                                                  (inst
                                                                                                                                   1
                                                                                                                                   "d1")
                                                                                                                                  (("2"
                                                                                                                                    (assert)
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil)
                                                                                                                               ("3"
                                                                                                                                (expand
                                                                                                                                 "o"
                                                                                                                                 1)
                                                                                                                                (("3"
                                                                                                                                  (inst
                                                                                                                                   1
                                                                                                                                   "c2")
                                                                                                                                  (("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)
                                                                     ("2"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("3"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (lemma
                                                           iterate_add_one)
                                                          (("2"
                                                            (inst?
                                                             -1
                                                             ("R"
                                                              "R"
                                                              "n"
                                                              "i - 1"))
                                                            (("1"
                                                              (decompose-equality)
                                                              (("1"
                                                                (inst
                                                                 -1
                                                                 "(a, b2)")
                                                                (("1"
                                                                  (replaces
                                                                   -1)
                                                                  (("1"
                                                                    (expand
                                                                     "o"
                                                                     -2)
                                                                    (("1"
                                                                      (skolem
                                                                       -2
                                                                       "b3")
                                                                      (("1"
                                                                        (flatten)
                                                                        (("1"
                                                                          (lemma
                                                                           "iterate_RTC")
                                                                          (("1"
                                                                            (inst
                                                                             -1
                                                                             "R"
                                                                             "i - 1")
                                                                            (("1"
                                                                              (expand*
                                                                               "subset?"
                                                                               "member")
                                                                              (("1"
                                                                                (inst
                                                                                 -1
                                                                                 "(b3, b2)")
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (hide
                                                                                     -4)
                                                                                    (("1"
                                                                                      (case-replace
                                                                                       "j = 0"
                                                                                       :hide?
                                                                                       t)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "iterate")
                                                                                        (("1"
                                                                                          (replace
                                                                                           -5
                                                                                           -6
                                                                                           rl)
                                                                                          (("1"
                                                                                            (expand
                                                                                             "locally_coherent?")
                                                                                            (("1"
                                                                                              (typepred
                                                                                               "Eq")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "equivalence?")
                                                                                                (("1"
                                                                                                  (flatten)
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     -12
                                                                                                     "a"
                                                                                                     "b3"
                                                                                                     "c")
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      (("1"
                                                                                                        (hide
                                                                                                         (-8
                                                                                                          -11))
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "joinable_m?")
                                                                                                          (("1"
                                                                                                            (skolem
                                                                                                             -10
                                                                                                             ("d1"
                                                                                                              "d2"))
                                                                                                            (("1"
                                                                                                              (flatten)
                                                                                                              (("1"
                                                                                                                (inst
                                                                                                                 -5
                                                                                                                 "b3")
                                                                                                                (("1"
                                                                                                                  (lemma
                                                                                                                   "R_subset_TC")
                                                                                                                  (("1"
                                                                                                                    (inst?)
                                                                                                                    (("1"
                                                                                                                      (expand*
                                                                                                                       "subset?"
                                                                                                                       "member")
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -1
                                                                                                                         "(a, b3)")
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          (("1"
                                                                                                                            (inst
                                                                                                                             -6
                                                                                                                             "d2"
                                                                                                                             "b")
                                                                                                                            (("1"
                                                                                                                              (prop)
                                                                                                                              (("1"
                                                                                                                                (skolem
                                                                                                                                 *
                                                                                                                                 ("r1"
                                                                                                                                  "r2"))
                                                                                                                                (("1"
                                                                                                                                  (flatten)
                                                                                                                                  (("1"
                                                                                                                                    (typepred
                                                                                                                                     "RTC(R)")
                                                                                                                                    (("1"
                                                                                                                                      (expand
                                                                                                                                       "reflexive_transitive?")
                                                                                                                                      (("1"
                                                                                                                                        (flatten)
                                                                                                                                        (("1"
                                                                                                                                          (expand
                                                                                                                                           "transitive?"
                                                                                                                                           -2)
                                                                                                                                          (("1"
                                                                                                                                            (inst
                                                                                                                                             -2
                                                                                                                                             "c"
                                                                                                                                             "d2"
                                                                                                                                             "r2")
                                                                                                                                            (("1"
                                                                                                                                              (expand
                                                                                                                                               "symmetric?"
                                                                                                                                               -8)
                                                                                                                                              (("1"
                                                                                                                                                (inst
                                                                                                                                                 -8
                                                                                                                                                 "r1"
                                                                                                                                                 "r2")
                                                                                                                                                (("1"
                                                                                                                                                  (inst
                                                                                                                                                   2
                                                                                                                                                   "r2"
                                                                                                                                                   "r1")
                                                                                                                                                  (("1"
                                                                                                                                                    (assert)
                                                                                                                                                    nil
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil)
                                                                                                                               ("2"
                                                                                                                                (expand
                                                                                                                                 "o"
                                                                                                                                 1)
                                                                                                                                (("2"
                                                                                                                                  (inst
                                                                                                                                   1
                                                                                                                                   "d1")
                                                                                                                                  (("2"
                                                                                                                                    (assert)
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil)
                                                                                                                               ("3"
                                                                                                                                (expand
                                                                                                                                 "o"
                                                                                                                                 1)
                                                                                                                                (("3"
                                                                                                                                  (inst
                                                                                                                                   1
                                                                                                                                   "b2")
                                                                                                                                  (("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)
                                                                                       ("2"
                                                                                        (lemma
                                                                                         iterate_add_one)
                                                                                        (("2"
                                                                                          (inst?
                                                                                           -1
                                                                                           ("R"
                                                                                            "R"
                                                                                            "n"
                                                                                            "j - 1"))
                                                                                          (("1"
                                                                                            (assert)
                                                                                            (("1"
                                                                                              (decompose-equality)
                                                                                              (("1"
                                                                                                (inst
                                                                                                 -1
                                                                                                 "(a, c2)")
                                                                                                (("1"
                                                                                                  (replaces
                                                                                                   -1)
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "o"
                                                                                                     -5)
                                                                                                    (("1"
                                                                                                      (skolem
                                                                                                       -5
                                                                                                       "c1")
                                                                                                      (("1"
                                                                                                        (flatten)
                                                                                                        (("1"
                                                                                                          (lemma
                                                                                                           "iterate_RTC")
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -1
                                                                                                             "R"
                                                                                                             "j - 1")
                                                                                                            (("1"
                                                                                                              (expand*
                                                                                                               "subset?"
                                                                                                               "member")
                                                                                                              (("1"
                                                                                                                (inst
                                                                                                                 -1
                                                                                                                 "(c1, c2)")
                                                                                                                (("1"
                                                                                                                  (assert)
                                                                                                                  (("1"
                                                                                                                    (hide
                                                                                                                     -7)
                                                                                                                    (("1"
                                                                                                                      (expand
                                                                                                                       "local_confluent_m?")
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -8
                                                                                                                         "a"
                                                                                                                         "c1"
                                                                                                                         "b3")
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "joinable_m?")
                                                                                                                            (("1"
                                                                                                                              (skolem
                                                                                                                               *
                                                                                                                               ("d1"
                                                                                                                                "d2"))
                                                                                                                              (("1"
                                                                                                                                (flatten)
                                                                                                                                (("1"
                                                                                                                                  (copy
                                                                                                                                   -3)
                                                                                                                                  (("1"
                                                                                                                                    (inst
                                                                                                                                     -4
                                                                                                                                     "b3")
                                                                                                                                    (("1"
                                                                                                                                      (lemma
                                                                                                                                       "R_subset_TC")
                                                                                                                                      (("1"
                                                                                                                                        (inst?)
                                                                                                                                        (("1"
                                                                                                                                          (expand*
                                                                                                                                           "subset?"
                                                                                                                                           "member")
                                                                                                                                          (("1"
                                                                                                                                            (inst
                                                                                                                                             -1
                                                                                                                                             "(a, b3)")
                                                                                                                                            (("1"
                                                                                                                                              (assert)
                                                                                                                                              (("1"
                                                                                                                                                (inst
                                                                                                                                                 -5
                                                                                                                                                 "b"
                                                                                                                                                 "d1")
                                                                                                                                                (("1"
                                                                                                                                                  (prop)
                                                                                                                                                  (("1"
                                                                                                                                                    (skolem
                                                                                                                                                     *
                                                                                                                                                     ("d3"
                                                                                                                                                      "d4"))
                                                                                                                                                    (("1"
                                                                                                                                                      (flatten)
                                                                                                                                                      (("1"
                                                                                                                                                        (inst
                                                                                                                                                         -5
                                                                                                                                                         "c1")
                                                                                                                                                        (("1"
                                                                                                                                                          (lemma
                                                                                                                                                           "R_subset_TC")
                                                                                                                                                          (("1"
                                                                                                                                                            (inst?)
                                                                                                                                                            (("1"
                                                                                                                                                              (expand*
                                                                                                                                                               "subset?"
                                                                                                                                                               "member")
                                                                                                                                                              (("1"
                                                                                                                                                                (inst
                                                                                                                                                                 -1
                                                                                                                                                                 "(a, c1)")
                                                                                                                                                                (("1"
                                                                                                                                                                  (assert)
                                                                                                                                                                  (("1"
                                                                                                                                                                    (inst
                                                                                                                                                                     -6
                                                                                                                                                                     "d4"
                                                                                                                                                                     "c")
                                                                                                                                                                    (("1"
                                                                                                                                                                      (prop)
                                                                                                                                                                      (("1"
                                                                                                                                                                        (skolem
                                                                                                                                                                         *
                                                                                                                                                                         ("u1"
                                                                                                                                                                          "u2"))
                                                                                                                                                                        (("1"
                                                                                                                                                                          (flatten)
                                                                                                                                                                          (("1"
                                                                                                                                                                            (typepred
                                                                                                                                                                             "RTC(R)")
                                                                                                                                                                            (("1"
                                                                                                                                                                              (expand
                                                                                                                                                                               "reflexive_transitive?")
                                                                                                                                                                              (("1"
                                                                                                                                                                                (flatten)
                                                                                                                                                                                (("1"
                                                                                                                                                                                  (expand
                                                                                                                                                                                   "transitive?"
                                                                                                                                                                                   -2)
                                                                                                                                                                                  (("1"
                                                                                                                                                                                    (inst
                                                                                                                                                                                     -2
                                                                                                                                                                                     "b"
                                                                                                                                                                                     "d4"
                                                                                                                                                                                     "u2")
                                                                                                                                                                                    (("1"
                                                                                                                                                                                      (inst
                                                                                                                                                                                       3
                                                                                                                                                                                       "u1"
                                                                                                                                                                                       "u2")
                                                                                                                                                                                      (("1"
                                                                                                                                                                                        (assert)
                                                                                                                                                                                        nil
                                                                                                                                                                                        nil))
                                                                                                                                                                                      nil))
                                                                                                                                                                                    nil))
                                                                                                                                                                                  nil))
                                                                                                                                                                                nil))
                                                                                                                                                                              nil))
                                                                                                                                                                            nil))
                                                                                                                                                                          nil))
                                                                                                                                                                        nil)
                                                                                                                                                                       ("2"
                                                                                                                                                                        (expand
                                                                                                                                                                         "o"
                                                                                                                                                                         1)
                                                                                                                                                                        (("2"
                                                                                                                                                                          (inst
                                                                                                                                                                           1
                                                                                                                                                                           "d3")
                                                                                                                                                                          (("2"
                                                                                                                                                                            (typepred
                                                                                                                                                                             "RTC(R)")
                                                                                                                                                                            (("2"
                                                                                                                                                                              (expand
                                                                                                                                                                               "reflexive_transitive?")
                                                                                                                                                                              (("2"
                                                                                                                                                                                (flatten)
                                                                                                                                                                                (("2"
                                                                                                                                                                                  (expand
                                                                                                                                                                                   "transitive?"
                                                                                                                                                                                   -2)
                                                                                                                                                                                  (("2"
                                                                                                                                                                                    (inst
                                                                                                                                                                                     -2
                                                                                                                                                                                     "c1"
                                                                                                                                                                                     "d1"
                                                                                                                                                                                     "d3")
                                                                                                                                                                                    (("2"
                                                                                                                                                                                      (assert)
                                                                                                                                                                                      nil
                                                                                                                                                                                      nil))
                                                                                                                                                                                    nil))
                                                                                                                                                                                  nil))
                                                                                                                                                                                nil))
                                                                                                                                                                              nil))
                                                                                                                                                                            nil))
                                                                                                                                                                          nil))
                                                                                                                                                                        nil)
                                                                                                                                                                       ("3"
                                                                                                                                                                        (expand
                                                                                                                                                                         "o"
                                                                                                                                                                         1)
                                                                                                                                                                        (("3"
                                                                                                                                                                          (inst
                                                                                                                                                                           1
                                                                                                                                                                           "c2")
                                                                                                                                                                          (("3"
                                                                                                                                                                            (assert)
                                                                                                                                                                            nil
                                                                                                                                                                            nil))
                                                                                                                                                                          nil))
                                                                                                                                                                        nil))
                                                                                                                                                                      nil))
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil)
                                                                                                                                                   ("2"
                                                                                                                                                    (expand
                                                                                                                                                     "o"
                                                                                                                                                     1)
                                                                                                                                                    (("2"
                                                                                                                                                      (inst
                                                                                                                                                       1
                                                                                                                                                       "b2")
                                                                                                                                                      (("2"
                                                                                                                                                        (assert)
                                                                                                                                                        nil
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil)
                                                                                                                                                   ("3"
                                                                                                                                                    (expand
                                                                                                                                                     "o"
                                                                                                                                                     1)
                                                                                                                                                    (("3"
                                                                                                                                                      (inst
                                                                                                                                                       1
                                                                                                                                                       "d2")
                                                                                                                                                      (("3"
                                                                                                                                                        (typepred
                                                                                                                                                         "Eq")
                                                                                                                                                        (("3"
                                                                                                                                                          (expand*
                                                                                                                                                           "equivalence?"
                                                                                                                                                           "symmetric?")
                                                                                                                                                          (("3"
                                                                                                                                                            (flatten)
                                                                                                                                                            (("3"
                                                                                                                                                              (inst
                                                                                                                                                               -2
                                                                                                                                                               "d1"
                                                                                                                                                               "d2")
                                                                                                                                                              (("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)
                                                                                           ("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("3"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (assert)
                                                              nil
                                                              nil)
                                                             ("3"
                                                              (hide -2)
                                                              (("3"
                                                                (expand*
                                                                 "confluent_m?"
                                                                 "local_confluent_m?")
                                                                (("3"
                                                                  (lemma
                                                                   "R_subset_RTC")
                                                                  (("3"
                                                                    (inst?)
                                                                    (("3"
                                                                      (lemma
                                                                       "R_subset_RTC")
                                                                      (("3"
                                                                        (inst?)
                                                                        (("3"
                                                                          (expand*
                                                                           "subset?"
                                                                           "member")
                                                                          (("3"
                                                                            (inst
                                                                             -1
                                                                             "(x, y)")
                                                                            (("3"
                                                                              (inst
                                                                               -2
                                                                               "(x, z)")
                                                                              (("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))
        nil)
       ("2" (flatten)
        (("2" (split)
          (("1" (hide -2)
            (("1" (expand* "confluent_m?" "local_confluent_m?")
              (("1" (skeep)
                (("1" (inst -3 "x" "x" "y" "z")
                  (("1" (typepred "Eq")
                    (("1" (expand "equivalence?")
                      (("1" (flatten)
                        (("1" (expand "reflexive?")
                          (("1" (inst?)
                            (("1" (lemma "R_subset_RTC")
                              (("1"
                                (lemma "R_subset_RTC")
                                (("1"
                                  (inst?)
                                  (("1"
                                    (inst?)
                                    (("1"
                                      (expand* "subset?" "member")
                                      (("1"
                                        (inst -1 "(x, y)")
                                        (("1"
                                          (inst -2 "(x, z)")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide -2)
            (("2" (expand* "confluent_m?" "locally_coherent?")
              (("2" (typepred "Eq")
                (("2" (expand "equivalence?")
                  (("2" (prop)
                    (("2" (skeep)
                      (("2" (inst -6 "x" "z" "y" "z")
                        (("2" (lemma "R_subset_RTC")
                          (("2" (inst?)
                            (("2" (expand* "subset?" "member")
                              (("2"
                                (inst -1 "(x, y)")
                                (("2"
                                  (assert)
                                  (("2"
                                    (hide-all-but 2)
                                    (("2"
                                      (expand* "RTC" "IUnion")
                                      (("2"
                                        (inst 1 "0")
                                        (("2"
                                          (expand "iterate" 1)
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((van_oostrom94 formula-decl nil modulo_equivalence nil)
    (noetherian_induction formula-decl nil noetherian nil)
    (diamond_property? const-decl "bool" ars_terminology nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (O const-decl "bool" relation_props 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)
    (joinable_m? const-decl "bool" modulo_equivalence nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (R_subset_RTC formula-decl nil relations_closure nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (local_confluent_m? const-decl "bool" modulo_equivalence nil)
    (i skolem-const-decl "nat" modulo_equivalence nil)
    (transitive? const-decl "bool" relations nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (iterate_add_one formula-decl nil relation_iterate "orders/")
    (int_plus_int_is_int application-judgement "int" integers nil)
    (R_subset_TC formula-decl nil relations_closure nil)
    (locally_coherent? const-decl "bool" modulo_equivalence nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (iterate_RTC formula-decl nil relations_closure nil)
    (j skolem-const-decl "nat" modulo_equivalence nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (symmetric? const-decl "bool" relations nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (reflexive? const-decl "bool" relations nil)
    (noetherian? const-decl "bool" noetherian nil)
    (noetherian type-eq-decl nil noetherian nil)
    (equivalence type-eq-decl nil relations_closure 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)
    (T formal-type-decl nil modulo_equivalence nil)
    (confluent_m? const-decl "bool" modulo_equivalence nil))
   shostak)))