(def-recursive-constant br%partial%trans%closure 
    "lambda(f:[nn,sets[ind_1,ind_1],sets[ind_1,ind_1]],
          lambda(n:nn,r:sets[ind_1,ind_1],
              if(n=0, 
                    r, 
                    lambda(s:sets[ind_1,ind_1],
                        lambda(x,y:ind_1, 
                            if(forsome(z:ind_1, #(s(x,z)) and #(r(z,y))),
                                  an%individual, 
                                  ?unit%sort)))
                        (f(n-1,r)))))"
    (theory generic-theory-1)
    (definition-name br%partial%trans%closure))

(def-theorem br%partial%trans%closure-total-aux 
    "forall(r:sets[ind_1,ind_1],n:zz,
          0<=n implies #(br%partial%trans%closure(n,r)))"
    (theory generic-theory-1)
    (proof
      (
        (induction integer-inductor ("n"))
        )))

(def-theorem br%partial%trans%closure-is-total 
    "total_q{br%partial%trans%closure,[nn,sets[ind_1,ind_1],sets[ind_1,ind_1]]}"
    (theory generic-theory-1)
    (usages d-r-convergence)
    (proof
      (
        insistent-direct-inference
        (apply-macete-with-minor-premises br%partial%trans%closure-total-aux)
        (apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic)
        )))

(def-theorem br%partial%trans%closure-lemma-1 
    "forall(m:nn,n:zz,r:sets[ind_1,ind_1],
          0<=n
            implies
          forall(x,y,z:ind_1,
            #(br%partial%trans%closure(m,r)(x,y))
              and
            #(br%partial%trans%closure(n,r)(y,z))
              implies
            #(br%partial%trans%closure(m+n+1,r)(x,z))))"
    (theory generic-theory-1)
    (proof
      (
        (induction trivial-integer-inductor ("n"))
        beta-reduce-repeatedly
        (unfold-single-defined-constant (1 2) br%partial%trans%closure)
        simplify
        (unfold-single-defined-constant (0) br%partial%trans%closure)
        simplify
        (instantiate-existential ("z_$0"))
        (backchain "with(p:prop,forall(x,z:ind_1,p))")
        (instantiate-existential ("y"))
        )))

(def-theorem br%partial%trans%closure-lemma-2 
    "forall(n:zz,r:sets[ind_1,ind_1],
          br%symmetric(r)
            and
          0<=n
            implies
          forall(x,y:ind_1,
            #(br%partial%trans%closure(n,r)(x,y))
              implies
            #(br%partial%trans%closure(n,r)(y,x))))"
    (theory generic-theory-1)
    (proof
      (
        (unfold-single-defined-constant (0) br%symmetric)
        (induction trivial-integer-inductor ("n"))
        beta-reduce-repeatedly
        (unfold-single-defined-constant-globally br%partial%trans%closure)
        (instantiate-existential ("z_$0"))
        (move-to-ancestor 8)
        (unfold-single-defined-constant (0) br%partial%trans%closure)
        simplify
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent 
          "with(r:sets[ind_1,ind_1],forall(x,y:ind_1,#(r(x,y)) implies #(r(y,x))))"
          ("z_$0" "y"))
        (instantiate-universal-antecedent 
          "with(p:prop,forall(x,y:ind_1,p))" ("x" "z_$0"))
        (cut-with-single-formula "#(br%partial%trans%closure(0,r)(y,z_$0))")
        (force-substitution "1+t" "0+t+1" (0))
        (apply-macete-with-minor-premises br%partial%trans%closure-lemma-1)
        auto-instantiate-existential
        simplify
        (unfold-single-defined-constant (0) br%partial%trans%closure)
        )))

(def-constant br%trans%closure 
    "lambda(r:sets[ind_1,ind_1],
          lambda(x,y:ind_1, 
              if(forsome(n:nn, #(br%partial%trans%closure(n,r)(x,y))),
                    an%individual, 
                    ?unit%sort)))"
    (theory generic-theory-1))

(def-theorem transitive-closure-is-transitive 
    "forall(r:sets[ind_1,ind_1], 
          br%transitive(br%trans%closure(r)))"
    (theory generic-theory-1)
    (proof
      (
        unfold-defined-constants
        (raise-conditional (0))
        (raise-conditional (0))
        (raise-conditional (0))
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:prop,not(p))")
        (instantiate-existential ("n_$0+n+1"))
        (apply-macete-with-minor-premises br%partial%trans%closure-lemma-1)
        auto-instantiate-existential
        (apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic)
        )))

(def-theorem trans-closure-of-reflexive-relation-is-reflexive 
    "forall(r:sets[ind_1,ind_1], 
          br%reflexive(r) implies br%reflexive(br%trans%closure(r)))"
    (theory generic-theory-1)
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        simplify
        (instantiate-existential ("0"))
        (unfold-single-defined-constant (0) br%partial%trans%closure)
        )))

(def-theorem trans-closure-of-symmetric-relation-is-symmetric 
    "forall(r:sets[ind_1,ind_1], 
          br%symmetric(r) implies br%symmetric(br%trans%closure(r)))"
    (theory generic-theory-1)
    (proof
      (
        unfold-defined-constants
        simplify
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("n"))
        (apply-macete-with-minor-premises br%partial%trans%closure-lemma-2)
        direct-inference
        (unfold-single-defined-constant (0) br%symmetric)
        (apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic)
        )))

(def-constant br%union 
    "lambda(r,s:sets[ind_1,ind_1],
          lambda(x,y:ind_1, if(#(r(x,y)) or #(s(x,y)), an%individual, ?unit%sort)))"
    (theory generic-theory-1))

(def-theorem union-of-reflexive-relations-is-reflexive 
    "forall(r,s:sets[ind_1,ind_1],
          br%reflexive(r) and br%reflexive(s) implies br%reflexive(br%union(r,s)))"
    (theory generic-theory-1)
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (case-split-on-conditionals (0))
        )))

(def-theorem union-of-symmetric-relations-is-symmetric 
    "forall(r,s:sets[ind_1,ind_1],
          br%symmetric(r) and br%symmetric(s) implies br%symmetric(br%union(r,s)))"
    (theory generic-theory-1)
    (proof
      (
        unfold-defined-constants
        (raise-conditional (0))
        direct-and-antecedent-inference-strategy
        (case-split-on-conditionals (0))
        (case-split-on-conditionals (0))
        )))

(def-theorem trans-closure-of-union-of-equiv-rels-is-an-equiv-rel 
    "forall(r,s:sets[ind_1,ind_1],
          br%equiv%relation(r) and br%equiv%relation(s)
            implies
          br%equiv%relation(br%trans%closure(br%union(r,s))))"
    (theory generic-theory-1)
    (proof
      (
        (unfold-single-defined-constant-globally br%equiv%relation)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises 
          trans-closure-of-reflexive-relation-is-reflexive)
        (apply-macete-with-minor-premises 
          union-of-reflexive-relations-is-reflexive)
        direct-inference
        (apply-macete-with-minor-premises 
          trans-closure-of-symmetric-relation-is-symmetric)
        (apply-macete-with-minor-premises 
          union-of-symmetric-relations-is-symmetric)
        direct-inference
        (apply-macete-with-minor-premises transitive-closure-is-transitive)
        )))