From bea2001071eecf6fd14d4f2783ac6f4e2767b9fa Mon Sep 17 00:00:00 2001
From: Maximilian Ehlers <2843450+b-m-f@users.noreply.github.com>
Date: Thu, 21 Nov 2024 19:15:55 +0100
Subject: [PATCH 1/2] Update Lambda.lagda.md Diamond and confluence example

The diamond property written in Agda demand a single step from L->(M|N)?
Therefore the verbose text should reflect the picture, which has 3 lines at the top.
---
 src/plfa/part2/Lambda.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md
index 193a7fe36..bcf2fa84f 100644
--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@@ -793,8 +793,8 @@ It can be illustrated as follows:
 Here `L`, `M`, `N` are universally quantified while `P`
 is existentially quantified.  If each line stands for zero
 or more reduction steps, this is called confluence,
-while if the top two lines stand for a single reduction
-step and the bottom two stand for zero or more reduction
+while if the top three lines stand for a single reduction
+step and the bottom three stand for zero or more reduction
 steps it is called the diamond property. In symbols:
 
 ```agda

From 1ca9571c9e72ea52a76c8a0e98bdb87bb9f0ce0f Mon Sep 17 00:00:00 2001
From: Maximilian Ehlers <2843450+b-m-f@users.noreply.github.com>
Date: Fri, 22 Nov 2024 08:47:04 +0100
Subject: [PATCH 2/2] Update Lambda.lagda.md

Make description of picture clearer
---
 src/plfa/part2/Lambda.lagda.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md
index bcf2fa84f..ec91c8904 100644
--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@@ -791,10 +791,10 @@ It can be illustrated as follows:
                P
 
 Here `L`, `M`, `N` are universally quantified while `P`
-is existentially quantified.  If each line stands for zero
+is existentially quantified.  If each of the four lines in the figure above stands for zero
 or more reduction steps, this is called confluence,
-while if the top three lines stand for a single reduction
-step and the bottom three stand for zero or more reduction
+while if the top two lines stand for a single reduction
+step and the bottom two stand for zero or more reduction
 steps it is called the diamond property. In symbols:
 
 ```agda