``` ```

# Results about commutation diagrams

``` Require Export Relations. ```
Definitions
``` Section Def1.   Variables X X' Y Y': Type.   Variable RX: relation2 X X'.   Variable R: relation2 X Y.   Variable RY: relation2 Y Y'.   Variable R': relation2 X' Y'.   Definition diagram := forall x x' y, RX x x' -> R x y -> exists2 y', RY y y' & R' x' y'. End Def1. Section Def2.   Variable X: Type.   Variables R S: relation X.   Definition strong_commute := diagram R S R S.   Definition local_commute := diagram R S (star R) (star S).   Definition semi_commute := diagram R S (star R) S.   Definition commute := diagram (star R) (star S) (star R) (star S).   Definition confluent := diagram (star R) (star R) (star R) (star R). End Def2. ```
Variance w.r.t inclusion
``` Section Incl.   Variables X X' Y Y': Type.   Variable RX: relation2 X X'.   Variable R R': relation2 X Y.   Variable RY: relation2 Y Y'.   Variables S S': relation2 X' Y'.   Hypothesis H: diagram RX R RY S.   Hypothesis HR: forall x y, R' x y -> R x y.   Hypothesis HS: forall x y, S x y -> S' x y.   Theorem diagram_incl: diagram RX R' RY S'. End Incl. ```
Reversing diagrams
``` Section Reverse.   Variables X X' Y Y': Type.   Variable RX: relation2 X X'.   Variable R: relation2 X Y.   Variable RY: relation2 Y Y'.   Variable R': relation2 X' Y'.   Hypothesis H: diagram RX R RY R'.   Theorem diagram_reverse: diagram R RX R' RY. End Reverse. ```
Composing diagrams
``` Section Compose.   Variables X Y Z X' Y' Z': Type.   Variable RY: relation2 Y Y'.   Variable RX: relation2 X X'.   Variable R1: relation2 X Y.   Variable R2: relation2 Y Z.   Variable RZ: relation2 Z Z'.   Variable S1: relation2 X' Y'.   Variable S2: relation2 Y' Z'.   Hypothesis H1: diagram RX R1 RY S1.   Hypothesis H2: diagram RY R2 RZ S2.   Theorem diagram_comp: diagram RX (comp R1 R2) RZ (comp S1 S2). End Compose. ```
Merging diagrams
``` Section Union.   Variables X Y X' Y' I: Type.   Variable RX: relation2 X X'.   Variables R: I -> relation2 X Y.   Variable RY: relation2 Y Y'.   Variable S: relation2 X' Y'.   Hypothesis H: forall i, diagram RX (R i) RY S.   Theorem diagram_union: diagram RX (union R) RY S. End Union. ```
Iterating one side of a diagram
``` Section Star.   Variables X X': Type.   Variable RX: relation2 X X'.   Variable R: relation X.   Variable S: relation X'.   Hypothesis H: diagram RX R RX (star S).   Theorem diagram_star: diagram RX (star R) RX (star S). End Star. ```
Iterating strictly one side of a diagram
``` Section Plus.   Variables X X': Type.   Variable RX: relation2 X X'.   Variable R: relation X.   Variable S: relation X'.   Hypothesis HR: diagram RX R RX (plus S).   Theorem diagram_plus: diagram RX (plus R) RX (plus S). End Plus. ```
A First Termination Argument : Subsection 4.1
``` Section PlusWf.   Variable X: Set.   Variable S: relation X.   Variable TX: relation X.   Hypothesis HS: diagram TX S (star TX) (plus S).   Hypothesis Hwf: well_founded (trans S).   Let Hpwf: well_founded (trans (plus S)) := plus_wf Hwf. ```
Lemma 4.1
```   Lemma diagram_plus_wf: diagram (star TX) (plus S) (star TX) (plus S).   Variable TX': relation X.   Hypothesis HS': diagram TX' S (comp (star TX) TX') (plus S). ```
Lemma 4.3
```   Lemma diagram_plus_wf_1: strong_commute (comp (star TX) TX') (plus S).   Variable Y: Type.   Variables R R': relation2 X Y.   Variable TY TY': relation Y.   Hypothesis HR: diagram TX R (star TY) (comp (star S) R).   Hypothesis HR': diagram TX' R (comp (star TY) TY') (comp (star S) R'). ```
Proposition 4.4
```   Theorem diagram_plus_wf_2: diagram (comp (star TX) TX') (comp (star S) R) (comp (star TY) TY') (comp (star S) R'). End PlusWf. ```
A Generalisation of Newmann's Lemma : Subsection 4.2
``` Section StarWf.   Variable X: Set.   Variable S: relation X.   Variable TX: relation X.   Hypothesis HS: local_commute TX S.   Hypothesis Hwf: well_founded (trans (comp (plus S) (plus TX))).   Section Gen.     Variable Y: Type.     Variable R: relation2 X Y.     Variable TY: relation Y.     Let SR := comp (star S) R.     Hypothesis HR: diagram TX R (star TY) SR. ```
Lemma 4.5
```     Lemma diagram_star_wf_1: diagram (star TX) SR (star TY) SR.     Variables X' Y': Type.     Variable TaX: relation2 X X'.     Variable TaY: relation2 Y Y'.     Variable S' : relation2 X' X'.     Variable R' : relation2 X' Y'.     Let SR' := comp (star S') R'.     Let TAX := comp (star TX) TaX.     Let TAY := comp (star TY) TaY.     Hypothesis HT: diagram TaX S TAX (star S').     Hypothesis HRT: diagram TaX R TAY SR'. ```
Proposition 4.8
```     Theorem diagram_star_wf_2: diagram TAX SR TAY SR'.   End Gen. ```
Corollary 4.6
```   Lemma diagram_star_wf: commute TX S. End StarWf. ```