# Re: [isabelle] Well-foundedness of Relational Composition

Just for the record: Sorry, I introduced a typo in my (sorry) lemma. (Actually hinted at by quickcheck, since my formulation is not correct.)
```
```
The problem was (once again) to adapt the orientation from the rewriting literature (where "smaller" is on the right) to the orientation of "wf" (where "smaller" is on the left).
```
It should actually be:

lemma qc_wf_relto_iff:
assumes "R O S â (R â S)â* O R"
shows "wf (Sâ* O R O Sâ*) â wf R"
...

```
This still implies Tjark's lemma and I hope it is provable ;) (I'll give it a try).
```
cheers

chris

On 04/27/2015 03:05 PM, Tobias Nipkow wrote:
```
```I have just added it. You are welcome to send me an improved version later.

Tobias

On 26/04/2015 15:51, Tjark Weber wrote:
```
```Tobias,

On Sun, 2015-04-26 at 09:24 +0200, Tobias Nipkow wrote:
```
```I'll be happy to include it in HOL/Wellfounded.thy if you do me the
favour of
getting rid of metis - it is not available at that theory yet.
```
```
Certainly. A proof that uses only simp and blast is attached.

```
```Maybe somebody can also think of a more telling name suffix than
"_compatible".
```
```
This was inspired by the existing lemma wf_union_compatible. Of course,
it is a terrible name.

Best,
Tjark

===== 8< =====

lemma wf_relcomp_compatible:
assumes "wf R" and "R O S \<subseteq> S O R"
shows "wf (S O R)"
proof (rule wfI_pf)
fix A assume A: "A \<subseteq> (S O R) `` A"
{
fix n have "(S ^^ n) `` A \<subseteq> R `` (S ^^ Suc n) `` A"
proof (induction n)
case 0 show ?case
using A by (simp add: relcomp_Image)
next
case (Suc n)
then have "S `` (S ^^ n) `` A \<subseteq> S `` R `` (S ^^ Suc n)
`` A"
also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A"
using assms(2) by (simp add: Image_mono O_assoc
relcomp_Image[symmetric] relcomp_mono)
finally show ?case
qed
}
then have "(\<Union>n. (S ^^ n) `` A) \<subseteq> R `` (\<Union>n. (S
^^ n) `` A)"
by blast
then have "(\<Union>n. (S ^^ n) `` A) = {}"
using assms(1) by (simp only: wfE_pf)
then show "A = {}"
using relpow.simps(1) by blast
qed

```
```
```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.