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

```Okay, here is a little bit more:

```
The following is Lemma 2 from Bachmair and Dershowitz 1986 (I left the hard part of the proof as an exercise ;) ... I hope it works similar to what Tjark did before, but since it was proved on paper it has to be correct \o/ right?):
```
lemma qc_wf_relto_iff:
assumes "R O S â S O (R â S)â*" -- âR quasi-commutes over Sâ
shows "wf (Sâ* O R O Sâ*) â wf R"
proof
assume "wf (Sâ* O R O Sâ*)"
moreover have "R â Sâ* O R O Sâ*" by auto
ultimately show "wf R" using wf_subset by auto
next
assume "wf R"
then show "wf (Sâ* O R O Sâ*)" sorry
qed

It can be used to proof "Tjark's Lemma" :)

corollary
assumes "wf R" and "R O S â S O R"
shows "wf (S O R)"
proof -
have "R O S â S O (R â S)â*" using âR O S â S O Râ by auto
then have "wf (Sâ* O R O Sâ*)"
using âwf Râ by (simp add: qc_wf_relto_iff)
moreover have "S O R â Sâ* O R O Sâ*" by auto
ultimately show ?thesis using wf_subset by auto
qed

Depending on who you cite the "subset assumption" could be called:

- R commutes over S (BD86)
```
- R strictly locally commutes over S (Geser, PhD); which actually denotes: R O S â S^* O R^+
```- ...

hope this helps

chris

On 04/27/2015 11:58 AM, Christian Sternagel wrote:
```
```Dear Tjark and Tobias,

This is my first impression: I've definitely seen this fact applied
(although implicitly) and think it counts as, as they say, "folklore".

Especially so, since the paper "proof" is trivial ;):

Assume: RS RS RS RS RS RS ...
Rearrange into: R SR SR SR SR SR ...
Apply "RS <= SR": R RS RS RS RS RS ...
Repeat this process to obtain: R R R R R R ...

I checked IsaFoR by hypersearch but didn't find anything that looks
alike immediately. That is, I'm not aware of any formalized proof.

After investigating a little further, I found some relevant literature.
Commutation has been investigated by Rosen , but as far as I can tell
on a short glance only w.r.t. confluence. Bachmair and Dershowitz 
pronounce "RS <= SR" as "R *commutes over* S" (whereas "commutation"
without "over" would result in a "diamond" diagram). And Geser 
something similar to your lemma on page 38:

If R is Noetherian, it is more convenient to check for strict
local commutation than for quasi-commutation: They are
equivalent, and checking for strict local commutation is
less complex ...

But also here I did not find a proof by skimming through. Maybe a closer
look would reveal something.

 Alfons Geser. Relative Termination. PhD-Thesis. 1990.
 Leo Bachmair, Nachum Dershowitz. Commutation, Transformation, and
 Barry K. Rosen. Tree-Manipulating Systems and Church-Rosser
Theorems. J. ACM (JACM) 20(1):160-187 (1973).
http://doi.acm.org/10.1145/321738.321750

cheers

chris

On 04/26/2015 03:51 PM, 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.