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