---

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

.....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. [%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. w : T
22. R[z1;w]
23. R[z2;w]
24. ∃w@0:T. ((λx,y. R[x;y]^* y w@0) ∧ (λx,y. R[x;y]^* w w@0))
⊢ λx,y. R[x;y]^* z1 w
BY
{ (BLemma `transitive-reflexive-closure-base-case` THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
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.  w  :  T
22.  R[z1;w]
23.  R[z2;w]
24.  \mexists{}w@0:T.  ((\mlambda{}x,y.  R[x;y]\^{}*  y  w@0)  \mwedge{}  (\mlambda{}x,y.  R[x;y]\^{}*  w  w@0))
\mvdash{}  \mlambda{}x,y.  R[x;y]\^{}*  z1  w


By

---

Latex:
(BLemma  `transitive-reflexive-closure-base-case`  THEN  Auto)

---

Home Index