Quelle  confluence_commute.prf

(confluence_commute
 (RC_RTC_is_RTC 0
  (RC_RTC_is_RTC-1 nil 3390042971
   ("" (lemma "RTC_characterization")
    (("" (skeep)
      (("" (inst -1 "RTC(R)")
        (("" (lemma "RTC_idempotent")
          (("" (inst -1 "R")
            (("" (prop)
              (("1" (expand reflexive_transitive?)
                (("1" (flatten)
                  (("1" (lemma "RC_characterization")
                    (("1" (inst -1 "RTC(R)") (("1" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((RTC_idempotent formula-decl nil relations_closure nil)
    (RC_characterization formula-decl nil relations_closure nil)
    (PRED type-eq-decl nil defined_types 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (RTC_characterization formula-decl nil relations_closure nil)
    (T formal-type-decl nil confluence_commute nil))
   shostak))
 (RTC_o_RTC_is_RTC 0
  (RTC_o_RTC_is_RTC-1 nil 3401787428
   ("" (skeep)
    (("" (expand "RTC")
      (("" (expand "IUnion")
        (("" (skosimp*)
          (("" (inst 1 "i!1 + i!2")
            (("" (lemma iterate_add)
              (("" (inst -1 "R" "i!1" "i!2")
                (("" (assert) (("" (grind) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((RTC const-decl "reflexive_transitive" relations_closure nil)
    (iterate_add formula-decl nil relation_iterate "orders/")
    (T formal-type-decl nil confluence_commute nil)
    (O const-decl "bool" relation_props nil)
    (pred type-eq-decl nil defined_types nil)
    (PRED type-eq-decl nil defined_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (IUnion const-decl "set[T]" indexed_sets nil))
   shostak))
 (RC_o_RTC_is_RTC 0
  (RC_o_RTC_is_RTC-1 nil 3417283391
   ("" (skeep)
    (("" (expand "RTC")
      (("" (expand "RC")
        (("" (expand "IUnion")
          (("" (expand "union")
            (("" (prop)
              (("1" (expand member)
                (("1" (skosimp*)
                  (("1" (inst 1 "i!1 + 1")
                    (("1" (lemma iterate_add)
                      (("1" (inst -1 "R" "1" "i!1")
                        (("1" (assert)
                          (("1" (replace -1)
                            (("1" (hide -1)
                              (("1"
                                (expand o)
                                (("1"
                                  (assert)
                                  (("1"
                                    (inst 1 y)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (hide -2)
                                        (("1" (grind) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (skosimp*)
                (("2" (inst 1 "0+i!1")
                  (("2" (lemma iterate_add)
                    (("2" (inst -1 "R" "0" "i!1")
                      (("2" (replace -1)
                        (("2" (hide -1)
                          (("2" (expand member)
                            (("2" (replace -1) (("2" (propax) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((RTC const-decl "reflexive_transitive" relations_closure nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (iterate_add formula-decl nil relation_iterate "orders/")
    (T formal-type-decl nil confluence_commute nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (O const-decl "bool" relation_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (pred type-eq-decl nil defined_types nil)
    (PRED type-eq-decl nil defined_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (member const-decl "bool" sets nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (union const-decl "set" sets nil)
    (RC const-decl "reflexive" relations_closure nil))
   shostak))
 (RTC_converse_RTC_R 0
  (RTC_converse_RTC_R-1 nil 3417861331
   ("" (skolem 1 ("R" "_" "_"))
    ((""
      (case "FORALL (i: nat, x,y : T) : (iterate(R,i)(x,y) <=> iterate(converse(R), i)(y, x))")
      (("1" (skeep)
        (("1" (inst -1 "_" x y)
          (("1" (expand RTC)
            (("1" (expand IUnion)
              (("1" (prop)
                (("1" (skosimp)
                  (("1" (inst 1 i!1)
                    (("1" (inst -2 i!1) (("1" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (skosimp)
                  (("2" (inst -2 i!1)
                    (("2" (inst 1 i!1) (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (induct i)
          (("1" (skeep)
            (("1" (expand iterate) (("1" (grind) nil nil)) nil)) nil)
           ("2" (skeep)
            (("2" (skeep)
              (("2" (lemma iterate_add)
                (("2" (inst -1 R j 1)
                  (("2" (replace -1 1)
                    (("2" (expand o)
                      (("2" (prop)
                        (("1" (skosimp -1)
                          (("1" (inst -4 "x" "y!1")
                            (("1" (hide -3)
                              (("1"
                                (prop)
                                (("1"
                                  (lemma iterate_add)
                                  (("1"
                                    (inst -1 "converse(R)" "1" "j")
                                    (("1"
                                      (decompose-equality -1)
                                      (("1"
                                        (inst -1 "(y,x)")
                                        (("1"
                                          (expand o -1)
                                          (("1"
                                            (replace -1 1)
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (inst 1 y!1)
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (hide -1 -2 -3)
                                                    (("1"
                                                      (expand iterate)
                                                      (("1"
                                                        (expand o -1)
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (expand
                                                             iterate
                                                             -1)
                                                            (("1"
                                                              (replace
                                                               -1
                                                               -2
                                                               rl)
                                                              (("1"
                                                                (hide
                                                                 -1)
                                                                (("1"
                                                                  (expand
                                                                   o)
                                                                  (("1"
                                                                    (inst
                                                                     1
                                                                     y)
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (expand
                                                                         iterate)
                                                                        (("1"
                                                                          (expand
                                                                           converse)
                                                                          (("1"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide -2)
                          (("2" (lemma iterate_add)
                            (("2" (inst -1 "converse(R)" 1 j)
                              (("2"
                                (decompose-equality)
                                (("2"
                                  (inst -1 "(y,x)")
                                  (("2"
                                    (expand o -1)
                                    (("2"
                                      (replace -1 -2)
                                      (("2"
                                        (hide -1)
                                        (("2"
                                          (skosimp -1)
                                          (("2"
                                            (inst -3 x y!1)
                                            (("2"
                                              (assert)
                                              (("2"
                                                (inst 1 y!1)
                                                (("2"
                                                  (assert)
                                                  (("2"
                                                    (hide -2 -3)
                                                    (("2"
                                                      (expand iterate)
                                                      (("2"
                                                        (expand o -1)
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (expand
                                                             iterate
                                                             -1)
                                                            (("2"
                                                              (replace
                                                               -1
                                                               -2
                                                               rl)
                                                              (("2"
                                                                (hide
                                                                 -1)
                                                                (("2"
                                                                  (expand
                                                                   iterate)
                                                                  (("2"
                                                                    (expand
                                                                     o)
                                                                    (("2"
                                                                      (inst
                                                                       1
                                                                       y!1)
                                                                      (("2"
                                                                        (expand
                                                                         converse)
                                                                        (("2"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (PRED type-eq-decl nil defined_types nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (pred type-eq-decl nil defined_types nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil confluence_commute nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (O const-decl "bool" relation_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (iterate_add formula-decl nil relation_iterate "orders/"))
   shostak))
 (semi_comm_implies_comm 0
  (semi_comm_implies_comm-1 nil 3386429566
   ("" (skeep)
    (("" (expand commute?)
      (("" (skeep)
        (("" (expand "RTC" -2)
          (("" (expand "IUnion" -2)
            (("" (skolem * "i")
              ((""
                (case "FORALL (j: nat, a, b, c: T) : (iterate(R1,j)(a,b) AND RTC(R2)(a,c)) => EXISTS (d: T): RTC(R2)(b, d) & RTC(R1)(c, d)")
                (("1" (inst -1 "i" "x" "y" "z")
                  (("1" (assert) nil nil)) nil)
                 ("2" (induct j)
                  (("1" (hide 2 -2 -3)
                    (("1" (assert)
                      (("1" (skeep)
                        (("1" (expand iterate)
                          (("1" (replace -1 -2)
                            (("1" (inst 1 "c")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "RTC" 1)
                                  (("1"
                                    (expand "IUnion")
                                    (("1"
                                      (inst 1 "0")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (expand iterate)
                                          (("1" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -2 -3 2)
                    (("2" (skeep)
                      (("2" (skeep)
                        (("2" (rewrite "iterate_add_one")
                          (("2" (expand o)
                            (("2" (skolem * "a1")
                              (("2"
                                (expand semi_commute?)
                                (("2"
                                  (inst -4 "a" "a1" "c")
                                  (("2"
                                    (flatten)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (skolem * "c1")
                                        (("2"
                                          (flatten)
                                          (("2"
                                            (inst -1 "a1" "b" "c1")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (skolem * "d1")
                                                (("2"
                                                  (flatten)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (hide
                                                       -3
                                                       -4
                                                       -5
                                                       -6)
                                                      (("2"
                                                        (inst 1 "d1")
                                                        (("2"
                                                          (assert)
                                                          (("2"
                                                            (hide -1)
                                                            (("2"
                                                              (expand
                                                               "RTC")
                                                              (("2"
                                                                (expand
                                                                 "IUnion")
                                                                (("2"
                                                                  (skolem
                                                                   *
                                                                   "n")
                                                                  (("2"
                                                                    (skolem
                                                                     *
                                                                     "m")
                                                                    (("2"
                                                                      (inst
                                                                       1
                                                                       "m + n")
                                                                      (("2"
                                                                        (lemma
                                                                         iterate_add)
                                                                        (("2"
                                                                          (inst
                                                                           -1
                                                                           "R1"
                                                                           "m"
                                                                           "n")
                                                                          (("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (grind)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((commute? const-decl "bool" ars_terminology nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (iterate_add_one formula-decl nil relation_iterate "orders/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (iterate_add formula-decl nil relation_iterate "orders/")
    (semi_commute? const-decl "bool" confluence_commute nil)
    (O const-decl "bool" relation_props nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil confluence_commute 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)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (PRED type-eq-decl nil defined_types nil)
    (reflexive_transitive? const-decl "bool" relations_closure nil)
    (reflexive_transitive type-eq-decl nil relations_closure nil)
    (IUnion const-decl "set[T]" indexed_sets nil))
   shostak))
 (sub_comm_rtc_implies_conf 0
  (sub_comm_rtc_implies_conf-1 nil 3390042462
   ("" (skeep)
    (("" (expand confluent?)
      (("" (expand sub_commutative?)
        (("" (rewrite "RC_RTC_is_RTC")
          (("" (expand joinable?) (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((confluent? const-decl "bool" ars_terminology nil)
    (RC_RTC_is_RTC formula-decl nil confluence_commute nil)
    (T formal-type-decl nil confluence_commute nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (sub_commutative? const-decl "bool" confluence_commute nil))
   shostak))
 (conf_local_request_implies_request 0
  (conf_local_request_implies_request-2 ": y" 3390555429
   ("" (skeep)
    (("" (expand request?)
      (("" (expand "RTC" 1 2)
        (("" (expand "IUnion")
          (("" (skeep)
            ((""
              (case "FORALL (n : nat, x,y,z : T) : confluent?(R2) & RTC(R1)(x, y) & iterate(R2, n)(x, z) =>
                                                   EXISTS r, s: RTC(R2)(y, r) & RTC(R1)(z, s) & RTC(R2)(s, r)")
              (("1" (assert)
                (("1" (skosimp* -5)
                  (("1" (inst -2 "i!1" "x" "y" "z")
                    (("1" (assert) nil nil)) nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (induct n)
                  (("1" (skosimp*)
                    (("1" (hide -4 -6)
                      (("1" (hide -5)
                        (("1" (expand iterate)
                          (("1" (replace -3)
                            (("1" (inst 1 "y!1" "y!1")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "RTC")
                                  (("1"
                                    (hide -4)
                                    (("1"
                                      (expand "IUnion")
                                      (("1"
                                        (hide-all-but 1)
                                        (("1"
                                          (prop)
                                          (("1"
                                            (inst 1 0)
                                            (("1" (grind) nil nil))
                                            nil)
                                           ("2"
                                            (inst 1 0)
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skeep)
                    (("2" (skosimp*)
                      (("2" (hide -5 -6 -7 -8)
                        (("2" (assert)
                          (("2" (expand iterate -4)
                            (("2" (expand o -4)
                              (("2"
                                (skosimp* -4)
                                (("2"
                                  (inst -1 "x!1" "y!1" "y!2")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (skosimp* -1)
                                      (("2"
                                        (reveal -3)
                                        (("2"
                                          (inst -1 "y!2" "s!1" "z!1")
                                          (("2"
                                            (assert)
                                            (("2"
                                              (skosimp* -1)
                                              (("2"
                                                (expand confluent?)
                                                (("2"
                                                  (inst
                                                   -7
                                                   "s!1"
                                                   "r!1"
                                                   "r!2")
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (expand
                                                       joinable?)
                                                      (("2"
                                                        (skosimp* -7)
                                                        (("2"
                                                          (inst
                                                           1
                                                           "z!2"
                                                           "s!2")
                                                          (("2"
                                                            (hide-all-but
                                                             (-4
                                                              -7
                                                              -2
                                                              -8
                                                              -3
                                                              1))
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (hide
                                                                 -1)
                                                                (("2"
                                                                  (lemma
                                                                   "RTC_o_RTC_is_RTC")
                                                                  (("2"
                                                                    (copy
                                                                     -1)
                                                                    (("2"
                                                                      (inst
                                                                       -1
                                                                       "R2"
                                                                       "y!1"
                                                                       "r!1"
                                                                       "z!2")
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (inst
                                                                           -2
                                                                           "R2"
                                                                           "s!2"
                                                                           "r!2"
                                                                           "z!2")
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((request? const-decl "bool" confluence_commute nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (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)
    (confluent? const-decl "bool" ars_terminology nil)
    (PRED type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil confluence_commute nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (O const-decl "bool" relation_props nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (RTC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil))
   shostak)
  (conf_local_request_implies_request-1 nil 3390044720
   ("" (skeep)
    (("" (expand request?)
      (("" (expand "RTC" 1 2)
        (("" (expand "IUnion")
          (("" (skeep)
            ((""
              (case "FORALL (n : nat) : confluent?(R2) & RTC(R1)(x, y) & iterate(R2, n)(x, z) =>
         EXISTS r, s: RTC(R2)(y, r) & RTC(R1)(z, s) & RTC(R2)(s, r)")
              (("1" (assert)
                (("1" (inst -3 "x" "y" "z")
                  (("1" (assert)
                    (("1" (skosimp* -5)
                      (("1" (inst -2 "i!1") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (postpone) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
 (comp_rtc_req_conf_impl_diamond 0
  (comp_rtc_req_conf_impl_diamond-2 "" 3400255840
   ("" (assert)
    (("" (skeep)
      (("" (expand diamond_property?)
        (("" (skeep)
          (("" (expand o -4)
            (("" (expand o -5)
              (("" (skosimp*)
                (("" (inst -3 "x" "y!1" "y!2")
                  (("" (assert)
                    (("" (skosimp*)
                      (("" (expand o -3)
                        (("" (expand o -4)
                          (("" (skosimp*)
                            (("" (hide -7 -9)
                              ((""
                                (copy -1)
                                ((""
                                  (expand request? -1)
                                  ((""
                                    (inst -1 "y!1" "y!3" "y")
                                    ((""
                                      (assert)
                                      ((""
                                        (skosimp*)
                                        ((""
                                          (hide -6 -10)
                                          ((""
                                            (expand request?)
                                            ((""
                                              (inst -4 "y!2" "y!4" "z")
                                              ((""
                                                (assert)
                                                ((""
                                                  (skosimp*)
                                                  ((""
                                                    (hide -9 -11)
                                                    ((""
                                                      (copy -7)
                                                      ((""
                                                        (copy -1)
                                                        ((""
                                                          (expand
                                                           confluent?
                                                           -1)
                                                          ((""
                                                            (inst
                                                             -1
                                                             "y!4"
                                                             "r!1"
                                                             "r!3")
                                                            ((""
                                                              (assert)
                                                              ((""
                                                                (expand
                                                                 joinable?)
                                                                ((""
                                                                  (skosimp*)
                                                                  ((""
                                                                    (hide
                                                                     -7
                                                                     -12)
                                                                    ((""
                                                                      (expand
                                                                       confluent?
                                                                       -3)
                                                                      ((""
                                                                        (inst
                                                                         -3
                                                                         "y!3"
                                                                         "r!2"
                                                                         "r!1")
                                                                        ((""
                                                                          (assert)
                                                                          ((""
                                                                            (expand
                                                                             joinable?)
                                                                            ((""
                                                                              (skosimp*)
                                                                              ((""
                                                                                (hide
                                                                                 -5
                                                                                 -11)
                                                                                ((""
                                                                                  (expand
                                                                                   confluent?)
                                                                                  ((""
                                                                                    (inst
                                                                                     -9
                                                                                     "r!1"
                                                                                     "z!2"
                                                                                     "z!1")
                                                                                    ((""
                                                                                      (assert)
                                                                                      ((""
                                                                                        (expand
                                                                                         joinable?)
                                                                                        ((""
                                                                                          (skosimp*)
                                                                                          ((""
                                                                                            (hide
                                                                                             -1
                                                                                             -4)
                                                                                            ((""
                                                                                              (inst
                                                                                               1
                                                                                               "z!3")
                                                                                              ((""
                                                                                                (expand
                                                                                                 o)
                                                                                                ((""
                                                                                                  (split)
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     1
                                                                                                     "s!1")
                                                                                                    (("1"
                                                                                                      (lemma
                                                                                                       "RTC_o_RTC_is_RTC")
                                                                                                      (("1"
                                                                                                        (copy
                                                                                                         -1)
                                                                                                        (("1"
                                                                                                          (inst
                                                                                                           -1
                                                                                                           "R2"
                                                                                                           "s!1"
                                                                                                           "r!2"
                                                                                                           "z!2")
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -2
                                                                                                             "R2"
                                                                                                             "s!1"
                                                                                                             "z!2"
                                                                                                             "z!3")
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (inst
                                                                                                     1
                                                                                                     "s!2")
                                                                                                    (("2"
                                                                                                      (lemma
                                                                                                       "RTC_o_RTC_is_RTC")
                                                                                                      (("2"
                                                                                                        (copy
                                                                                                         -1)
                                                                                                        (("2"
                                                                                                          (inst
                                                                                                           -1
                                                                                                           "R2"
                                                                                                           "s!2"
                                                                                                           "r!3"
                                                                                                           "z!1")
                                                                                                          (("2"
                                                                                                            (inst
                                                                                                             -2
                                                                                                             "R2"
                                                                                                             "s!2"
                                                                                                             "z!1"
                                                                                                             "z!3")
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            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)
   ((T formal-type-decl nil confluence_commute nil)
    (request? const-decl "bool" confluence_commute nil)
    (confluent? const-decl "bool" ars_terminology nil)
    (RTC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (O const-decl "bool" relation_props nil)
    (diamond_property? const-decl "bool" ars_terminology nil))
   shostak)
  (comp_rtc_req_conf_impl_diamond-1 nil 3400001153
   ("" (skeep)
    (("" (assert)
      (("" (flatten)
        (("" (expand diamond_property?)
          (("" (skeep)
            (("" (expand o -4)
              (("" (expand o -5)
                (("" (skosimp*)
                  (("" (inst -3 "x" "y!1" "y!2")
                    (("" (assert)
                      (("" (skosimp*)
                        (("" (expand o -3)
                          (("" (expand o -4)
                            (("" (skosimp*)
                              ((""
                                (copy -1)
                                ((""
                                  (expand request? -1)
                                  ((""
                                    (inst -1 "y!1" "y!3" "y")
                                    ((""
                                      (assert)
                                      ((""
                                        (skosimp*)
                                        ((""
                                          (expand request?)
                                          ((""
                                            (inst -4 "y!2" "y!4" "z")
                                            ((""
                                              (assert)
                                              ((""
                                                (skosimp*)
                                                ((""
                                                  (copy -7)
                                                  ((""
                                                    (expand confluent?)
                                                    ((""
                                                      (inst
                                                       -1
                                                       "y!4"
                                                       "r!1"
                                                       "r!3")
                                                      ((""
                                                        (assert)
                                                        ((""
                                                          (postpone)
                                                          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 shostak))
 (union_req_conf_is_confluent 0
  (union_req_conf_is_confluent-1 nil 3401714997
   ("" (skeep)
    (("" (assert)
      (("" (lemma "comp_rtc_req_conf_impl_diamond")
        (("" (inst -1 "R1" "R2")
          (("" (assert)
            (("" (prop)
              (("" (hide-all-but (-1) -)
                (("" (lemma "DP_implies_StC")
                  (("" (inst -1 "RTC(R1) o RTC(R2)")
                    (("" (assert)
                      (("" (hide -2)
                        (("" (lemma "R1_R2_RTC_R1_R2")
                          (("" (inst -1 "R1" "R2")
                            ((""
                              (lemma "R2_Str_Confl_implies_R1_Confl")
                              ((""
                                (inst
                                 -1
                                 "union(R1,R2)"
                                 "RTC(R1) o RTC(R2)")
                                (("" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil confluence_commute nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (DP_implies_StC formula-decl nil results_confluence nil)
    (R1_R2_RTC_R1_R2 formula-decl nil results_confluence nil)
    (R2_Str_Confl_implies_R1_Confl formula-decl nil results_confluence
     nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets 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)
    (O const-decl "bool" relation_props nil)
    (pred type-eq-decl nil defined_types nil)
    (comp_rtc_req_conf_impl_diamond formula-decl nil confluence_commute
     nil))
   shostak))
 (comp_rtc_confs_req_impl_diamond 0
  (comp_rtc_confs_req_impl_diamond-1 nil 3401736142
   ("" (assert)
    (("" (skeep)
      (("" (expand diamond_property?)
        (("" (skeep)
          (("" (expand o -4)
            (("" (expand o -5)
              (("" (skosimp*)
                (("" (expand confluent? -1)
                  (("" (inst -1 "x" "y!1" "y!2")
                    (("" (assert)
                      (("" (expand joinable?)
                        (("" (skosimp*)
                          (("" (hide -5 -7)
                            (("" (copy -4)
                              ((""
                                (expand request? -1)
                                ((""
                                  (inst -1 "y!1" "z!1" "y")
                                  ((""
                                    (assert)
                                    ((""
                                      (skosimp*)
                                      ((""
                                        (hide -4 -8)
                                        ((""
                                          (expand request?)
                                          ((""
                                            (inst -6 "y!2" "z!1" "z")
                                            ((""
                                              (assert)
                                              ((""
                                                (skosimp*)
                                                ((""
                                                  (hide -4 -9)
                                                  ((""
                                                    (expand confluent?)
                                                    ((""
                                                      (inst
                                                       -4
                                                       "z!1"
                                                       "r!1"
                                                       "r!2")
                                                      ((""
                                                        (assert)
                                                        ((""
                                                          (expand
                                                           joinable?)
                                                          ((""
                                                            (skosimp*)
                                                            ((""
                                                              (hide
                                                               -1
                                                               -6)
                                                              ((""
                                                                (inst
                                                                 1
                                                                 "z!2")
                                                                ((""
                                                                  (expand
                                                                   o)
                                                                  ((""
                                                                    (split)
                                                                    (("1"
                                                                      (lemma
                                                                       "RTC_o_RTC_is_RTC")
                                                                      (("1"
                                                                        (inst
                                                                         -1
                                                                         "R2"
                                                                         "s!1"
                                                                         "r!1"
                                                                         "z!2")
                                                                        (("1"
                                                                          (inst
                                                                           1
                                                                           "s!1")
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (lemma
                                                                       "RTC_o_RTC_is_RTC")
                                                                      (("2"
                                                                        (inst
                                                                         -1
                                                                         "R2"
                                                                         "s!2"
                                                                         "r!2"
                                                                         "z!2")
                                                                        (("2"
                                                                          (inst
                                                                           1
                                                                           "s!2")
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((confluent? const-decl "bool" ars_terminology nil)
    (RTC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (request? const-decl "bool" confluence_commute nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (T formal-type-decl nil confluence_commute nil)
    (O const-decl "bool" relation_props nil)
    (diamond_property? const-decl "bool" ars_terminology nil))
   shostak))
 (union_confs_req_is_confluent 0
  (union_confs_req_is_confluent-1 nil 3401738133
   ("" (assert)
    (("" (skeep)
      (("" (lemma "comp_rtc_confs_req_impl_diamond")
        (("" (inst -1 "R1" "R2")
          (("" (assert)
            (("" (hide -2 -3 -4)
              (("" (lemma "DP_implies_StC")
                (("" (inst -1 "RTC(R1) o RTC(R2)")
                  (("" (assert)
                    (("" (hide -2)
                      (("" (lemma "R1_R2_RTC_R1_R2")
                        (("" (lemma "R2_Str_Confl_implies_R1_Confl")
                          (("" (inst -2 "R1" "R2")
                            ((""
                              (inst -1 "union(R1,R2)"
                               "RTC(R1) o RTC(R2)")
                              (("" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil confluence_commute nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (pred type-eq-decl nil defined_types nil)
    (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)
    (R2_Str_Confl_implies_R1_Confl formula-decl nil results_confluence
     nil)
    (union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (R1_R2_RTC_R1_R2 formula-decl nil results_confluence nil)
    (DP_implies_StC formula-decl nil results_confluence nil)
    (comp_rtc_confs_req_impl_diamond formula-decl nil
     confluence_commute nil))
   shostak))
 (CR_iff_PP 0
  (CR_iff_PP-1 nil 3405325672
   ("" (skeep)
    (("" (prop)
      (("1" (expand church_rosser?)
        (("1" (expand postponement?)
          (("1" (skeep)
            (("1" (inst -1 "x" "y")
              (("1" (expand "EC")
                (("1" (expand "SC")
                  (("1" (assert)
                    (("1" (expand joinable?)
                      (("1" (skosimp)
                        (("1" (inst 1 "z!1")
                          (("1" (assert)
                            (("1" (lemma "RTC_converse_RTC_R")
                              (("1"
                                (inst -1 "R" "y" "z!1")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand postponement?)
        (("2" (expand church_rosser?)
          (("2" (skosimp)
            (("2" (inst -1 "x!1" "y!1")
              (("2" (expand "EC")
                (("2" (expand "SC")
                  (("2" (assert)
                    (("2" (lemma "RTC_converse_RTC_R")
                      (("2" (skosimp)
                        (("2" (inst -1 "R" "y!1" "z!1")
                          (("2" (assert)
                            (("2" (expand joinable?)
                              (("2"
                                (inst 1 "z!1")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((postponement? const-decl "bool" confluence_commute nil)
    (T formal-type-decl nil confluence_commute nil)
    (SC const-decl "symmetric" relations_closure nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (RTC_converse_RTC_R formula-decl nil confluence_commute nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (EC const-decl "equivalence" relations_closure nil)
    (church_rosser? const-decl "bool" ars_terminology nil))
   shostak))
 (confluent_iff_postponement 0
  (confluent_iff_postponement-1 nil 3405327616
   ("" (skeep)
    (("" (prop)
      (("1" (lemma "CR_iff_Confluent")
        (("1" (inst -1 "R")
          (("1" (assert)
            (("1" (lemma "CR_iff_PP")
              (("1" (inst -1 "R") (("1" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil)
       ("2" (lemma "CR_iff_PP")
        (("2" (lemma "CR_iff_Confluent")
          (("2" (inst -1 "R")
            (("2" (inst -2 "R") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (CR_iff_PP formula-decl nil confluence_commute nil)
    (CR_iff_Confluent formula-decl nil results_confluence nil)
    (T formal-type-decl nil confluence_commute nil))
   shostak))
 (hip_Hindley_implies_semi_comm 0
  (hip_Hindley_implies_semi_comm-1 nil 3418465491
   ("" (skeep)
    ((""
      (case "FORALL (i : nat, x, y, z : T) : (RC(R1)(x, y) & iterate(R2, i)(x, z) => EXISTS (r : T) : (RTC(R2)(y, r) & RTC(R1)(z, r)))")
      (("1" (expand semi_commute?)
        (("1" (skosimp*)
          (("1" (expand RTC -4)
            (("1" (expand IUnion)
              (("1" (skolem -4 i)
                (("1" (inst -1 i x!1 y!1 z!1)
                  (("1" (expand RC -1)
                    (("1" (expand union)
                      (("1" (expand member) (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (induct i)
          (("1" (skosimp*)
            (("1" (expand iterate)
              (("1" (replaces -2)
                (("1" (inst 1 y!1)
                  (("1" (assert)
                    (("1" (hide -2 2)
                      (("1" (expand RC)
                        (("1" (expand union)
                          (("1" (expand member)
                            (("1" (prop)
                              (("1"
                                (hide -1)
                                (("1"
                                  (grind)
                                  (("1"
                                    (inst 1 0)
                                    (("1"
                                      (expand iterate)
                                      (("1" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand RTC)
                                (("2"
                                  (expand IUnion)
                                  (("2"
                                    (inst 1 1)
                                    (("2"
                                      (expand iterate)
                                      (("2"
                                        (expand o)
                                        (("2"
                                          (inst 1 z!1)
                                          (("2"
                                            (expand iterate)
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (grind)
                                (("3"
                                  (inst 1 0)
                                  (("3" (grind) nil nil))
                                  nil))
                                nil)
                               ("4"
                                (replaces -1)
                                (("4"
                                  (grind)
                                  (("4"
                                    (inst 1 0)
                                    (("4" (grind) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (skeep)
            (("2" (skeep)
              (("2" (lemma iterate_add_one)
                (("2" (inst -1 R2 j)
                  (("2" (replaces -1)
                    (("2" (expand o)
                      (("2" (skolem -3 v)
                        (("2" (flatten)
                          (("2" (expand RC)
                            (("2" (expand union)
                              (("2"
                                (expand member)
                                (("2"
                                  (split)
                                  (("1"
                                    (inst -5 x y v)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (skolem -5 w)
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (inst -2 v w z)
                                            (("1"
                                              (assert)
                                              (("1"
                                                (prop)
                                                (("1"
                                                  (skolem -2 r)
                                                  (("1"
                                                    (inst 1 r)
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (lemma
                                                         RC_o_RTC_is_RTC)
                                                        (("1"
                                                          (inst
                                                           -1
                                                           R2
                                                           y
                                                           w
                                                           r)
                                                          (("1"
                                                            (expand
                                                             RC
                                                             -1)
                                                            (("1"
                                                              (expand
                                                               union)
                                                              (("1"
                                                                (expand
                                                                 member)
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (inst 1 z)
                                                  (("2"
                                                    (replaces -1)
                                                    (("2"
                                                      (split)
                                                      (("1"
                                                        (hide-all-but
                                                         (-5 -4 1))
                                                        (("1"
                                                          (lemma
                                                           RC_o_RTC_is_RTC)
                                                          (("1"
                                                            (inst
                                                             -1
                                                             R2
                                                             y
                                                             w
                                                             z)
                                                            (("1"
                                                              (expand
                                                               RC
                                                               -1)
                                                              (("1"
                                                                (expand
                                                                 union)
                                                                (("1"
                                                                  (expand
                                                                   member)
                                                                  (("1"
                                                                    (expand
                                                                     RTC
                                                                     -1
                                                                     1)
                                                                    (("1"
                                                                      (expand
                                                                       IUnion)
                                                                      (("1"
                                                                        (split)
                                                                        (("1"
                                                                          (propax)
                                                                          nil
                                                                          nil)
                                                                         ("2"
                                                                          (inst
                                                                           1
                                                                           j)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide-all-but
                                                         (1))
                                                        (("2"
                                                          (expand RTC)
                                                          (("2"
                                                            (expand
                                                             IUnion)
                                                            (("2"
                                                              (inst
                                                               1
                                                               0)
                                                              (("2"
                                                                (grind)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (inst 1 z)
                                    (("2"
                                      (replaces -1)
                                      (("2"
                                        (hide-all-but (-2 -3 1))
                                        (("2"
                                          (lemma RC_o_RTC_is_RTC)
                                          (("2"
                                            (inst -1 R2 y v z)
                                            (("2"
                                              (expand RC -1)
                                              (("2"
                                                (expand union)
                                                (("2"
                                                  (expand member)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (expand RTC -1 1)
                                                      (("2"
                                                        (expand IUnion)
                                                        (("2"
                                                          (prop)
                                                          (("1"
                                                            (hide-all-but
                                                             (1))
                                                            (("1"
                                                              (expand
                                                               RTC)
                                                              (("1"
                                                                (expand
                                                                 IUnion)
                                                                (("1"
                                                                  (inst
                                                                   1
                                                                   0)
                                                                  (("1"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide -1 1)
                                                            (("2"
                                                              (inst
                                                               1
                                                               j)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("3"
                                                            (hide-all-but
                                                             (1))
                                                            (("3"
                                                              (expand
                                                               RTC)
                                                              (("3"
                                                                (expand
                                                                 IUnion)
                                                                (("3"
                                                                  (inst
                                                                   1
                                                                   0)
                                                                  (("3"
                                                                    (grind)
                                                                    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)
   ((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)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (RC const-decl "reflexive" relations_closure nil)
    (reflexive type-eq-decl nil relations_closure nil)
    (reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (pred type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil confluence_commute nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (semi_commute? const-decl "bool" confluence_commute nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (O const-decl "bool" relation_props nil)
    (RC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (iterate_add_one formula-decl nil relation_iterate "orders/"))
   shostak))
 (lemma_Hindley_1964 0
  (lemma_Hindley_1964-1 nil 3418464701
   ("" (skeep)
    (("" (lemma hip_Hindley_implies_semi_comm)
      (("" (assert)
        (("" (inst -1 R1 R2)
          (("" (prop)
            (("" (hide -2)
              (("" (rewrite semi_comm_implies_comm) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((hip_Hindley_implies_semi_comm formula-decl nil confluence_commute
     nil)
    (T formal-type-decl nil confluence_commute nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (semi_comm_implies_comm formula-decl nil confluence_commute nil))
   shostak))
 (ref_condition_to_refcomp 0
  (ref_condition_to_refcomp-1 nil 3418462830
   ("" (skeep)
    (("" (split)
      (("1" (flatten)
        (("1" (skeep)
          (("1" (expand ref_compatible?)
            (("1" (assert)
              (("1" (expand refinement?)
                (("1" (expand o)
                  (("1" (skolem -2 v)
                    (("1" (flatten)
                      (("1" (expand RTC -3)
                        (("1" (expand IUnion)
                          (("1" (skolem -3 i)
                            (("1"
                              (case "FORALL (i : nat, x, y : T) : iterate(R1,i)(x, y) => RTC(R2)(x, y)")
                              (("1"
                                (inst -1 i v y)
                                (("1"
                                  (assert)
                                  (("1"
                                    (lemma RC_o_RTC_is_RTC)
                                    (("1"
                                      (inst -1 R2 x v y)
                                      (("1"
                                        (expand RC)
                                        (("1"
                                          (expand union)
                                          (("1"
                                            (expand member)
                                            (("1"
                                              (inst -3 x y)
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (induct i)
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (expand iterate -1)
                                    (("1"
                                      (replaces -1)
                                      (("1"
                                        (expand RTC 1)
                                        (("1"
                                          (expand IUnion)
                                          (("1"
                                            (inst 1 0)
                                            (("1"
                                              (expand iterate 1)
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skeep)
                                  (("2"
                                    (skosimp*)
                                    (("2"
                                      (lemma iterate_add_one)
                                      (("2"
                                        (inst -1 R1 j)
                                        (("2"
                                          (replaces -1)
                                          (("2"
                                            (expand o)
                                            (("2"
                                              (hide -4 -3 -5 2)
                                              (("2"
                                                (skolem -2 w)
                                                (("2"
                                                  (flatten)
                                                  (("2"
                                                    (inst -1 w y!1)
                                                    (("2"
                                                      (inst -4 x!1 w)
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (lemma
                                                           RTC_o_RTC_is_RTC)
                                                          (("2"
                                                            (inst
                                                             -1
                                                             R2
                                                             x!1
                                                             w
                                                             y!1)
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (flatten)
        (("2" (expand ref_compatible?)
          (("2" (split)
            (("1" (propax) nil nil)
             ("2" (skeep)
              (("2" (expand RTC -1)
                (("2" (expand IUnion)
                  (("2" (skolem -1 i)
                    (("2"
                      (case "FORALL (i : nat, x, y : T) : iterate(R2, i)(x, y) => joinable?(R1)(x, y)")
                      (("1" (inst -1 i x y) (("1" (assert) nil nil))
                        nil)
                       ("2" (hide 2 -1 -3)
                        (("2" (induct i)
                          (("1" (skosimp*)
                            (("1" (hide -2)
                              (("1"
                                (expand iterate)
                                (("1"
                                  (replaces -1)
                                  (("1"
                                    (expand joinable?)
                                    (("1"
                                      (inst 1 y!1)
                                      (("1"
                                        (expand RTC)
                                        (("1"
                                          (expand IUnion)
                                          (("1"
                                            (split)
                                            (("1"
                                              (inst 1 0)
                                              (("1" (grind) nil nil))
                                              nil)
                                             ("2"
                                              (inst 1 0)
                                              (("2" (grind) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skeep)
                            (("2" (skosimp*)
                              (("2"
                                (lemma iterate_add_one)
                                (("2"
                                  (inst -1 R2 j)
                                  (("2"
                                    (replaces -1)
                                    (("2"
                                      (expand o)
                                      (("2"
                                        (skolem -2 v)
                                        (("2"
                                          (flatten)
                                          (("2"
                                            (inst -1 v y!1)
                                            (("2"
                                              (assert)
                                              (("2"
                                                (expand joinable? -1)
                                                (("2"
                                                  (skolem -1 w)
                                                  (("2"
                                                    (flatten)
                                                    (("2"
                                                      (inst -5 x!1 w)
                                                      (("2"
                                                        (split)
                                                        (("1"
                                                          (expand
                                                           joinable?)
                                                          (("1"
                                                            (skolem
                                                             -1
                                                             r)
                                                            (("1"
                                                              (inst
                                                               1
                                                               r)
                                                              (("1"
                                                                (flatten)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (hide-all-but
                                                                     (-2
                                                                      -4
                                                                      1))
                                                                    (("1"
                                                                      (lemma
                                                                       RTC_o_RTC_is_RTC)
                                                                      (("1"
                                                                        (inst
                                                                         -1
                                                                         R1
                                                                         y!1
                                                                         w
                                                                         r)
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (inst 1 v)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "bool" relation_props nil)
    (IUnion const-decl "set[T]" indexed_sets 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)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil confluence_commute nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (RC const-decl "reflexive" relations_closure nil)
    (RC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (iterate_add_one formula-decl nil relation_iterate "orders/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (RTC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (refinement? const-decl "bool" confluence_commute nil)
    (ref_compatible? const-decl "bool" confluence_commute nil)
    (joinable? const-decl "bool" ars_terminology nil))
   shostak))
 (semi_implies_CR 0
  (semi_implies_CR-1 nil 3418553977
   ("" (skeep)
    (("" (lemma CR_iff_Confluent)
      (("" (inst -1 R)
        (("" (assert)
          (("" (hide 2)
            (("" (expand confluent?)
              (("" (skeep)
                ((""
                  (case "FORALL (i : nat, x, y, z : T) : iterate(R, i)(x, y) & RTC(R)(x, z) => joinable?(R)(y, z)")
                  (("1" (expand RTC -2)
                    (("1" (expand IUnion)
                      (("1" (skolem -2 i)
                        (("1" (inst -1 i x y z)
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -1 -2 2)
                    (("2" (induct i)
                      (("1" (skosimp*)
                        (("1" (expand iterate)
                          (("1" (replaces -1)
                            (("1" (expand joinable?)
                              (("1"
                                (inst 1 z!1)
                                (("1"
                                  (expand RTC 1 2)
                                  (("1"
                                    (expand IUnion)
                                    (("1"
                                      (split)
                                      (("1" (propax) nil nil)
                                       ("2"
                                        (inst 1 0)
                                        (("2" (grind) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skeep)
                        (("2" (skosimp*)
                          (("2" (lemma iterate_add_one)
                            (("2" (inst -1 R j)
                              (("2"
                                (replaces -1)
                                (("2"
                                  (expand o)
                                  (("2"
                                    (skolem -2 v)
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (expand semi_confluent?)
                                        (("2"
                                          (inst -5 x!1 v z!1)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (expand joinable?)
                                              (("2"
                                                (skolem -5 w)
                                                (("2"
                                                  (flatten)
                                                  (("2"
                                                    (inst -1 v y!1 w)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (skolem -1 r)
                                                        (("2"
                                                          (flatten)
                                                          (("2"
                                                            (inst 1 r)
                                                            (("2"
                                                              (split)
                                                              (("1"
                                                                (propax)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 (-2
                                                                  -7
                                                                  1))
                                                                (("2"
                                                                  (lemma
                                                                   RTC_o_RTC_is_RTC)
                                                                  (("2"
                                                                    (inst
                                                                     -1
                                                                     R
                                                                     z!1
                                                                     w
                                                                     r)
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil confluence_commute nil)
    (CR_iff_Confluent formula-decl nil results_confluence nil)
    (confluent? const-decl "bool" ars_terminology nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (reflexive_transitive type-eq-decl nil relations_closure nil)
    (reflexive_transitive? const-decl "bool" relations_closure nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (pred type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (O const-decl "bool" relation_props nil)
    (RTC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (semi_confluent? const-decl "bool" ars_terminology nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (iterate_add_one formula-decl nil relation_iterate "orders/")
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (semi_implies_conf 0
  (semi_implies_conf-1 nil 3427724691
   ("" (skeep)
    (("" (expand confluent?)
      (("" (skeep)
        (("" (expand RTC -2)
          (("" (expand IUnion)
            (("" (skolem -2 i)
              ((""
                (case "FORALL (i: nat, x, y, z: T) : iterate(R, i)(x, y) & RTC(R)(x, z) => joinable?(R)(y, z)")
                (("1" (inst -1 i x y z) (("1" (assert) nil nil)) nil)
                 ("2" (hide 2 -2 -3)
                  (("2" (induct i)
                    (("1" (skosimp*)
                      (("1" (expand iterate)
                        (("1" (replaces -1)
                          (("1" (expand joinable?)
                            (("1" (inst 1 z!1)
                              (("1"
                                (split)
                                (("1" (propax) nil nil)
                                 ("2"
                                  (hide -1 -2)
                                  (("2"
                                    (expand RTC)
                                    (("2"
                                      (expand IUnion)
                                      (("2"
                                        (inst 1 0)
                                        (("2"
                                          (expand iterate)
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skeep)
                      (("2" (skosimp*)
                        (("2" (lemma iterate_add_one)
                          (("2" (inst -1 R j)
                            (("2" (replaces -1)
                              (("2"
                                (expand o)
                                (("2"
                                  (skolem -2 v)
                                  (("2"
                                    (flatten)
                                    (("2"
                                      (expand semi_confluent?)
                                      (("2"
                                        (inst -5 x!1 v z!1)
                                        (("2"
                                          (assert)
                                          (("2"
                                            (expand joinable? -5)
                                            (("2"
                                              (skolem -5 w)
                                              (("2"
                                                (flatten)
                                                (("2"
                                                  (inst -1 v y!1 w)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (expand
                                                       joinable?)
                                                      (("2"
                                                        (skolem -1 r)
                                                        (("2"
                                                          (inst 1 r)
                                                          (("2"
                                                            (flatten)
                                                            (("2"
                                                              (split)
                                                              (("1"
                                                                (propax)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 (-2
                                                                  -7
                                                                  1))
                                                                (("2"
                                                                  (lemma
                                                                   RTC_o_RTC_is_RTC)
                                                                  (("2"
                                                                    (inst
                                                                     -1
                                                                     R
                                                                     z!1
                                                                     w
                                                                     r)
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((confluent? const-decl "bool" ars_terminology nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (iterate_add_one formula-decl nil relation_iterate "orders/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (semi_confluent? const-decl "bool" ars_terminology nil)
    (RTC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (O const-decl "bool" relation_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil confluence_commute 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)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (PRED type-eq-decl nil defined_types nil)
    (reflexive_transitive? const-decl "bool" relations_closure nil)
    (reflexive_transitive type-eq-decl nil relations_closure nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (IUnion const-decl "set[T]" indexed_sets nil))
   shostak))
 (sub_comm_implies_semi_conf 0
  (sub_comm_implies_semi_conf-1 nil 3418399734
   ("" (skeep)
    (("" (expand semi_confluent?)
      (("" (skeep)
        (("" (expand RTC)
          (("" (expand IUnion)
            ((""
              (case "FORALL (i : nat, x, y, z : T) : RC(R)(x, y) & iterate(R, i)(x, z) => joinable?(R)(y, z)")
              (("1" (skolem -4 i)
                (("1" (inst -1 i x y z)
                  (("1" (expand RC)
                    (("1" (expand union)
                      (("1" (expand member) (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide -2 -3 2)
                (("2" (induct i)
                  (("1" (skosimp*)
                    (("1" (expand iterate)
                      (("1" (replaces -2)
                        (("1" (expand joinable?)
                          (("1" (expand RC)
                            (("1" (expand union)
                              (("1"
                                (expand member)
                                (("1"
                                  (split)
                                  (("1"
                                    (inst 1 y!1)
                                    (("1"
                                      (split)
                                      (("1"
                                        (expand RTC)
                                        (("1"
                                          (expand IUnion)
                                          (("1"
                                            (inst 1 0)
                                            (("1"
                                              (expand iterate)
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand RTC)
                                        (("2"
                                          (expand IUnion)
                                          (("2"
                                            (inst 1 1)
                                            (("2"
                                              (expand iterate)
                                              (("2"
                                                (expand o)
                                                (("2"
                                                  (inst 1 z!1)
                                                  (("2"
                                                    (expand iterate)
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (inst 1 y!1)
                                    (("2"
                                      (split)
                                      (("1"
                                        (expand RTC)
                                        (("1"
                                          (expand IUnion)
                                          (("1"
                                            (inst 1 0)
                                            (("1"
                                              (expand iterate)
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand RTC)
                                        (("2"
                                          (expand IUnion)
                                          (("2"
                                            (inst 1 0)
                                            (("2"
                                              (replaces -1)
                                              (("2"
                                                (expand iterate)
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skeep)
                    (("2" (skosimp*)
                      (("2" (lemma iterate_add_one)
                        (("2" (inst -1 R j)
                          (("2" (replaces -1)
                            (("2" (expand o)
                              (("2"
                                (skolem -3 v)
                                (("2"
                                  (flatten)
                                  (("2"
                                    (expand sub_commutative?)
                                    (("2"
                                      (inst -5 x!1 y!1 v)
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand RC)
                                          (("2"
                                            (expand union)
                                            (("2"
                                              (expand member)
                                              (("2"
                                                (split)
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (expand joinable?)
                                                    (("1"
                                                      (skolem -5 w)
                                                      (("1"
                                                        (flatten)
                                                        (("1"
                                                          (inst
                                                           -2
                                                           v
                                                           w
                                                           z!1)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (split)
                                                              (("1"
                                                                (skolem
                                                                 -1
                                                                 r)
                                                                (("1"
                                                                  (flatten)
                                                                  (("1"
                                                                    (split)
                                                                    (("1"
                                                                      (split)
                                                                      (("1"
                                                                        (inst
                                                                         1
                                                                         r)
                                                                        (("1"
                                                                          (split)
                                                                          (("1"
                                                                            (hide-all-but
                                                                             (-2
                                                                              -3
                                                                              1))
                                                                            (("1"
                                                                              (lemma
                                                                               RC_o_RTC_is_RTC)
                                                                              (("1"
                                                                                (inst
                                                                                 -1
                                                                                 R
                                                                                 y!1
                                                                                 w
                                                                                 r)
                                                                                (("1"
                                                                                  (expand
                                                                                   RC)
                                                                                  (("1"
                                                                                    (expand
                                                                                     union)
                                                                                    (("1"
                                                                                      (expand
                                                                                       member)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (inst
                                                                         1
                                                                         r)
                                                                        (("2"
                                                                          (split)
                                                                          (("1"
                                                                            (hide-all-but
                                                                             (-2
                                                                              -3
                                                                              1))
                                                                            (("1"
                                                                              (lemma
                                                                               RC_o_RTC_is_RTC)
                                                                              (("1"
                                                                                (inst
                                                                                 -1
                                                                                 R
                                                                                 y!1
                                                                                 w
                                                                                 r)
                                                                                (("1"
                                                                                  (expand
                                                                                   RC)
                                                                                  (("1"
                                                                                    (expand
                                                                                     union)
                                                                                    (("1"
                                                                                      (expand
                                                                                       member)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (inst
                                                                       1
                                                                       r)
                                                                      (("2"
                                                                        (split)
                                                                        (("1"
                                                                          (hide-all-but
                                                                           (-2
                                                                            -1
                                                                            1))
                                                                          (("1"
                                                                            (replaces
                                                                             -1)
                                                                            nil
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand joinable?)
                                                  (("2"
                                                    (inst 1 z!1)
                                                    (("2"
                                                      (split)
                                                      (("1"
                                                        (hide-all-but
                                                         (-1 -3 -4 1))
                                                        (("1"
                                                          (replaces -1)
                                                          (("1"
                                                            (lemma
                                                             RC_o_RTC_is_RTC)
                                                            (("1"
                                                              (inst
                                                               -1
                                                               R
                                                               y!1
                                                               v
                                                               z!1)
                                                              (("1"
                                                                (expand
                                                                 RC)
                                                                (("1"
                                                                  (expand
                                                                   union)
                                                                  (("1"
                                                                    (expand
                                                                     member)
                                                                    (("1"
                                                                      (expand
                                                                       RTC
                                                                       -1
                                                                       1)
                                                                      (("1"
                                                                        (expand
                                                                         IUnion)
                                                                        (("1"
                                                                          (assert)
                                                                          (("1"
                                                                            (inst
                                                                             1
                                                                             j)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide-all-but
                                                         1)
                                                        (("2"
                                                          (expand RTC)
                                                          (("2"
                                                            (expand
                                                             IUnion)
                                                            (("2"
                                                              (inst
                                                               1
                                                               0)
                                                              (("2"
                                                                (expand
                                                                 iterate)
                                                                (("2"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((semi_confluent? const-decl "bool" ars_terminology nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (RC const-decl "reflexive" relations_closure nil)
    (reflexive type-eq-decl nil relations_closure nil)
    (reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (pred type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil confluence_commute nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (O const-decl "bool" relation_props nil)
    (RC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (sub_commutative? const-decl "bool" confluence_commute nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (iterate_add_one formula-decl nil relation_iterate "orders/")
    (IUnion const-decl "set[T]" indexed_sets nil))
   shostak))
 (sub_comm_implies_conf 0
  (sub_comm_implies_conf-1 nil 3418459410
   ("" (skeep)
    (("" (lemma sub_comm_implies_semi_conf)
      (("" (inst -1 R)
        (("" (assert)
          (("" (lemma semi_implies_conf)
            (("" (inst -1 R) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((sub_comm_implies_semi_conf formula-decl nil confluence_commute
     nil)
    (semi_implies_conf formula-decl nil confluence_commute 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 confluence_commute nil))
   shostak))
 (lemma_Rosen_1973 0
  (lemma_Rosen_1973-1 nil 3418459655
   ("" (skeep)
    (("" (lemma sub_comm_implies_conf)
      (("" (inst -1 R1)
        (("" (assert)
          (("" (expand confluent?)
            (("" (skeep)
              (("" (inst -1 x y z)
                (("" (replace -2 -1)
                  (("" (assert)
                    (("" (expand joinable?)
                      (("" (skolem -1 r)
                        (("" (inst 1 r)
                          (("" (replace -2 -1) (("" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sub_comm_implies_conf formula-decl nil confluence_commute nil)
    (joinable? const-decl "bool" ars_terminology nil)
    (confluent? const-decl "bool" ars_terminology nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil confluence_commute nil))
   shostak))
 (lcomm_and_snunion_implies_comm 0
  (lcomm_and_snunion_implies_comm-1 nil 3418382215
   ("" (skeep)
    (("" (lemma noetherian_induction)
      (("" (inst -1 "union(R1, R2)" "_")
        ((""
          (inst -1
           "(LAMBDA (x : T): (FORALL (y, z: T): RTC(R1)(x, y) AND RTC(R2)(x, z) IMPLIES EXISTS (r : T) : (RTC(R2)(y, r) & RTC(R1)(z, r))))")
          (("" (split)
            (("1" (hide -2 -3)
              (("1" (expand commute?)
                (("1" (skeep)
                  (("1" (inst -1 x)
                    (("1" (inst -1 y z) (("1" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (skeep)
                (("2" (skeep)
                  (("2" (hide -5)
                    (("2" (expand RTC (-2 -3))
                      (("2" (expand IUnion)
                        (("2" (skolem -2 i)
                          (("2" (skolem -3 j)
                            (("2" (case "i = 0")
                              (("1"
                                (replaces -1)
                                (("1"
                                  (hide-all-but (-2 -3 1))
                                  (("1"
                                    (expand iterate -1)
                                    (("1"
                                      (replaces -1)
                                      (("1"
                                        (inst 1 z)
                                        (("1"
                                          (split)
                                          (("1"
                                            (expand RTC)
                                            (("1"
                                              (expand IUnion)
                                              (("1"
                                                (inst 1 j)
                                                nil
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand RTC)
                                            (("2"
                                              (expand IUnion)
                                              (("2"
                                                (inst 1 0)
                                                (("2"
                                                  (expand iterate)
                                                  (("2"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (case "j = 0")
                                (("1"
                                  (replaces -1)
                                  (("1"
                                    (hide-all-but (-2 -3 2))
                                    (("1"
                                      (inst 1 y)
                                      (("1"
                                        (split)
                                        (("1"
                                          (expand RTC)
                                          (("1"
                                            (expand IUnion)
                                            (("1"
                                              (inst 1 0)
                                              (("1"
                                                (expand iterate 1)
                                                (("1"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (expand iterate -2)
                                          (("2"
                                            (replaces -2)
                                            (("2"
                                              (expand RTC)
                                              (("2"
                                                (expand IUnion)
                                                (("2"
                                                  (inst 1 i)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (lemma iterate_add_one)
                                  (("2"
                                    (lemma iterate_add_one)
                                    (("2"
                                      (inst -1 R1 "i - 1")
                                      (("1"
                                        (inst -2 R2 "j - 1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (replaces -1)
                                            (("1"
                                              (replaces -1)
                                              (("1"
                                                (expand o)
                                                (("1"
                                                  (skolem -2 a)
                                                  (("1"
                                                    (skolem -3 b)
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (lemma
                                                         iterate_RTC)
                                                        (("1"
                                                          (lemma
                                                           iterate_RTC)
                                                          (("1"
                                                            (inst
                                                             -1
                                                             R1
                                                             "i - 1")
                                                            (("1"
                                                              (inst
                                                               -2
                                                               R2
                                                               "j - 1")
                                                              (("1"
                                                                (expand
                                                                 subset?)
                                                                (("1"
                                                                  (inst
                                                                   -1
                                                                   "(a, y)")
                                                                  (("1"
                                                                    (inst
                                                                     -2
                                                                     "(b, z)")
                                                                    (("1"
                                                                      (expand
                                                                       member)
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (expand
                                                                           locally_commute?)
                                                                          (("1"
                                                                            (inst
                                                                             -8
                                                                             x_1
                                                                             a
                                                                             b)
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (skolem
                                                                                 -8
                                                                                 c)
                                                                                (("1"
                                                                                  (flatten)
                                                                                  (("1"
                                                                                    (hide
                                                                                     -5
                                                                                     -7)
                                                                                    (("1"
                                                                                      (copy
                                                                                       -3)
                                                                                      (("1"
                                                                                        (inst
                                                                                         -1
                                                                                         a)
                                                                                        (("1"
                                                                                          (split)
                                                                                          (("1"
                                                                                            (inst
                                                                                             -1
                                                                                             y
                                                                                             c)
                                                                                            (("1"
                                                                                              (assert)
                                                                                              (("1"
                                                                                                (skolem
                                                                                                 -1
                                                                                                 d)
                                                                                                (("1"
                                                                                                  (flatten)
                                                                                                  (("1"
                                                                                                    (lemma
                                                                                                     "RTC_o_RTC_is_RTC")
                                                                                                    (("1"
                                                                                                      (inst
                                                                                                       -1
                                                                                                       R1
                                                                                                       b
                                                                                                       c
                                                                                                       d)
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        (("1"
                                                                                                          (inst
                                                                                                           -6
                                                                                                           b)
                                                                                                          (("1"
                                                                                                            (split)
                                                                                                            (("1"
                                                                                                              (inst
                                                                                                               -1
                                                                                                               d
                                                                                                               z)
                                                                                                              (("1"
                                                                                                                (assert)
                                                                                                                (("1"
                                                                                                                  (skolem
                                                                                                                   -1
                                                                                                                   r)
                                                                                                                  (("1"
                                                                                                                    (flatten)
                                                                                                                    (("1"
                                                                                                                      (inst
                                                                                                                       3
                                                                                                                       r)
                                                                                                                      (("1"
                                                                                                                        (split)
                                                                                                                        (("1"
                                                                                                                          (hide-all-but
                                                                                                                           (-4
                                                                                                                            -1
                                                                                                                            1))
                                                                                                                          (("1"
                                                                                                                            (lemma
                                                                                                                             "RTC_o_RTC_is_RTC")
                                                                                                                            (("1"
                                                                                                                              (inst
                                                                                                                               -1
                                                                                                                               R2
                                                                                                                               y
                                                                                                                               d
                                                                                                                               r)
                                                                                                                              (("1"
                                                                                                                                (assert)
                                                                                                                                nil
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil)
                                                                                                                         ("2"
                                                                                                                          (propax)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil)
                                                                                                             ("2"
                                                                                                              (hide-all-but
                                                                                                               (-7
                                                                                                                1))
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 TC)
                                                                                                                (("2"
                                                                                                                  (expand
                                                                                                                   IUnion)
                                                                                                                  (("2"
                                                                                                                    (inst
                                                                                                                     1
                                                                                                                     1)
                                                                                                                    (("2"
                                                                                                                      (expand
                                                                                                                       union)
                                                                                                                      (("2"
                                                                                                                        (expand
                                                                                                                         member)
                                                                                                                        (("2"
                                                                                                                          (grind)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             (-4
                                                                                              1))
                                                                                            (("2"
                                                                                              (expand
                                                                                               TC)
                                                                                              (("2"
                                                                                                (expand
                                                                                                 IUnion)
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   union)
                                                                                                  (("2"
                                                                                                    (inst
                                                                                                     1
                                                                                                     1)
                                                                                                    (("2"
                                                                                                      (grind)
                                                                                                      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))
                                        nil)
                                       ("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil confluence_commute nil)
    (noetherian_induction formula-decl nil noetherian 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (iterate_add_one formula-decl nil relation_iterate "orders/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (i skolem-const-decl "nat" confluence_commute nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (member const-decl "bool" sets nil)
    (locally_commute? const-decl "bool" ars_terminology nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (TC const-decl "transitive" relations_closure nil)
    (RTC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
    (subset? const-decl "bool" sets nil)
    (iterate_RTC formula-decl nil relations_closure nil)
    (O const-decl "bool" relation_props nil)
    (j skolem-const-decl "nat" confluence_commute nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (commute? const-decl "bool" ars_terminology nil)
    (noetherian type-eq-decl nil noetherian nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (noetherian? const-decl "bool" noetherian nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
    (R1 skolem-const-decl "PRED[[T, T]]" confluence_commute nil)
    (R2 skolem-const-decl "PRED[[T, T]]" confluence_commute nil))
   shostak))
 (UN_implies_UNseta 0
  (UN_implies_UNseta-1 nil 3419153716
   ("" (skeep)
    (("" (expand UNseta_terese?)
      (("" (skeep)
        (("" (expand UN_terese?)
          (("" (skolem -4 z)
            (("" (inst -1 x y)
              (("" (assert)
                (("" (hide -1 -2 2)
                  (("" (flatten)
                    (("" (lemma RTC_subset_EC)
                      (("" (inst -1 R)
                        (("" (expand* "subset?" "member")
                          (("" (copy -1)
                            (("" (inst -1 "(z, x)")
                              ((""
                                (inst -2 "(z, y)")
                                ((""
                                  (assert)
                                  ((""
                                    (hide -3 -4)
                                    ((""
                                      (lemma EC_characterization)
                                      ((""
                                        (inst -1 "EC(R)")
                                        ((""
                                          (lemma EC_idempotent)
                                          ((""
                                            (inst -1 R)
                                            ((""
                                              (prop)
                                              (("1"
                                                (hide -2 -3)
                                                (("1"
                                                  (expand equivalence?)
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (expand
                                                       symmetric?)
                                                      (("1"
                                                        (inst -2 z x)
                                                        (("1"
                                                          (hide -1)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (hide -3)
                                                              (("1"
                                                                (expand
                                                                 transitive?)
                                                                (("1"
                                                                  (inst
                                                                   -2
                                                                   x
                                                                   z
                                                                   y)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide -2 -3 2 3)
                                                (("2"
                                                  (replaces -1)
                                                  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)
   ((UNseta_terese? const-decl "bool" confluence_commute nil)
    (UN_terese? const-decl "bool" confluence_commute nil)
    (T formal-type-decl nil confluence_commute nil)
    (RTC_subset_EC formula-decl nil relations_closure nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (EC_characterization formula-decl nil relations_closure nil)
    (EC_idempotent formula-decl nil relations_closure nil)
    (symmetric? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (equivalence? const-decl "bool" relations nil)
    (equivalence type-eq-decl nil relations_closure nil)
    (EC const-decl "equivalence" relations_closure nil)
    (PRED type-eq-decl nil defined_types nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak)))