---

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


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. m : T ⟶ ℕ
4. ∀x,y:T.  (R[x;y] ⇒ m y < m x)
5. d : ℤ
6. [%4] : 0 < d
7. ∀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))))))
8. x : T
9. m x < d
10. y : T
11. z : T
12. λx,y. R[x;y]^* x y
13. λx,y. R[x;y]^* x z
14. z2 : T
15. R[x;z2]
16. z2 λx,y. R[x;y]^* y
17. z1 : T
18. R[x;z1]
19. z1 λx,y. R[x;y]^* z
20. ∀y,z:T.  (R[x;y] ⇒ R[x;z] ⇒ ((y = z ∈ T) ∨ (∃w:T. (R[y;w] ∧ R[z;w]))))
21. z1 = z2 ∈ T
⊢ ∃w:T. ((λx,y. R[x;y]^* y w) ∧ (λx,y. R[x;y]^* z w))
BY
{ (InstHyp [⌜z2⌝;⌜y⌝;⌜z⌝] 7 ⋅ THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. m : T ⟶ ℕ
4. ∀x,y:T.  (R[x;y] ⇒ m y < m x)
5. d : ℤ
6. 0 < d
7. ∀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))))))
8. x : T
9. m x < d
10. y : T
11. z : T
12. λx,y. R[x;y]^* x y
13. λx,y. R[x;y]^* x z
14. z2 : T
15. R[x;z2]
16. z2 λx,y. R[x;y]^* y
17. z1 : T
18. R[x;z1]
19. z1 λx,y. R[x;y]^* z
20. ∀y,z:T.  (R[x;y] ⇒ R[x;z] ⇒ ((y = z ∈ T) ∨ (∃w:T. (R[y;w] ∧ R[z;w]))))
21. z1 = z2 ∈ T
⊢ m z2 < d - 1

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  m  :  T  {}\mrightarrow{}  \mBbbN{}
4.  \mforall{}x,y:T.    (R[x;y]  {}\mRightarrow{}  m  y  <  m  x)
5.  d  :  \mBbbZ{}
6.  [\%4]  :  0  <  d
7.  \mforall{}x:T
          (m  x  <  d  -  1
          {}\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[\000Cx;y]\^{}*  z  w))))))
8.  x  :  T
9.  m  x  <  d
10.  y  :  T
11.  z  :  T
12.  \mlambda{}x,y.  R[x;y]\^{}*  x  y
13.  \mlambda{}x,y.  R[x;y]\^{}*  x  z
14.  z2  :  T
15.  R[x;z2]
16.  z2  \mlambda{}x,y.  R[x;y]\^{}*  y
17.  z1  :  T
18.  R[x;z1]
19.  z1  \mlambda{}x,y.  R[x;y]\^{}*  z
20.  \mforall{}y,z:T.    (R[x;y]  {}\mRightarrow{}  R[x;z]  {}\mRightarrow{}  ((y  =  z)  \mvee{}  (\mexists{}w:T.  (R[y;w]  \mwedge{}  R[z;w]))))
21.  z1  =  z2
\mvdash{}  \mexists{}w:T.  ((\mlambda{}x,y.  R[x;y]\^{}*  y  w)  \mwedge{}  (\mlambda{}x,y.  R[x;y]\^{}*  z  w))


By

---

Latex:
(InstHyp  [\mkleeneopen{}z2\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  7  \mcdot{}  THEN  Auto)

---

Home Index