---

Step * 1 of Lemma diamond-implies-TC-confluent


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. rel-diamond-property(T;x,y.R[x;y])
4. ∃m:T ⟶ ℕ. ∀x,y:T.  (R[x;y] ⇒ m y < m x)
⊢ ∀x,y,z:T.  ((λx,y. R[x;y]^* x y) ⇒ (λx,y. R[x;y]^* x z) ⇒ (∃w:T. ((λx,y. R[x;y]^* y w) ∧ (λx,y. R[x;y]^* z w))))
BY
{ (D -1
   THEN (Assert ⌜∀d:ℕ. ∀x:T.
                   (m x < d
                   ⇒ (∀y,z:T.
                         ((λx,y. R[x;y]^* x y) ⇒ (λx,y. R[x;y]^* x z) ⇒ (∃w:T. ((λx,y. R[x;y]^* y w) ∧ (λx,y. R[x;y]^*\000C z w))))))⌝⋅
   THENM ((D 0 THENA Auto) THEN InstHyp [⌜(m x) + 1⌝;⌜x⌝] (-2)⋅ THEN Auto)
   )
   THEN InductionOnNat
   THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. rel-diamond-property(T;x,y.R[x;y])
4. m : T ⟶ ℕ
5. ∀x,y:T.  (R[x;y] ⇒ m y < m x)
6. x : T
7. m x < 0
8. y : T
9. z : T
10. λx,y. R[x;y]^* x y
11. λx,y. R[x;y]^* x z
⊢ ∃w:T. ((λx,y. R[x;y]^* y w) ∧ (λx,y. R[x;y]^* z w))

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. rel-diamond-property(T;x,y.R[x;y])
4. m : T ⟶ ℕ
5. ∀x,y:T.  (R[x;y] ⇒ m y < m x)
6. d : ℤ
7. [%4] : 0 < d
8. ∀x:T
     (m x < d - 1 ⇒ (∀y,z:T.  ((λx,y. R[x;y]^* x y) ⇒ (λx,y. R[x;y]^* x z) ⇒ (∃w:T. ((λx,y. R[x;y]^* y w) ∧ (λx,y. R[\000Cx;y]^* z w))))))
9. x : T
10. m x < d
11. y : T
12. z : T
13. λx,y. R[x;y]^* x y
14. λx,y. R[x;y]^* x z
⊢ ∃w:T. ((λx,y. R[x;y]^* y w) ∧ (λx,y. R[x;y]^* z w))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  rel-diamond-property(T;x,y.R[x;y])
4.  \mexists{}m:T  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x,y:T.    (R[x;y]  {}\mRightarrow{}  m  y  <  m  x)
\mvdash{}  \mforall{}x,y,z:T.    ((\mlambda{}x,y.  R[x;y]\^{}*  x  y)  {}\mRightarrow{}  (\mlambda{}x,y.  R[x;y]\^{}*  x  z)  {}\mRightarrow{}  (\mexists{}w:T.  ((\mlambda{}x,y.  R[x;y]\^{}*  y  w)  \mwedge{}  (\mlambda{}x,y.  \000CR[x;y]\^{}*  z  w))))


By

---

Latex:
(D  -1
  THEN  (Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}x:T.
                                  (m  x  <  d
                                  {}\mRightarrow{}  (\mforall{}y,z:T.
                                              ((\mlambda{}x,y.  R[x;y]\^{}*  x  y)
                                              {}\mRightarrow{}  (\mlambda{}x,y.  R[x;y]\^{}*  x  z)
                                              {}\mRightarrow{}  (\mexists{}w:T.  ((\mlambda{}x,y.  R[x;y]\^{}*  y  w)  \mwedge{}  (\mlambda{}x,y.  R[x;y]\^{}*  z  w))))))\mkleeneclose{}\mcdot{}
  THENM  ((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}(m  x)  +  1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto)

---

Home Index