Step
*
1
2
2
2
1
2
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. w : T
22. R[z1;w]
23. R[z2;w]
⊢ ∃w:T. ((λx,y. R[x;y]^* y w) ∧ (λx,y. R[x;y]^* z w))
BY
{ (InstHyp [⌜z2⌝;⌜y⌝;⌜w⌝] 7⋅ THENA 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. w : T
22. R[z1;w]
23. R[z2;w]
⊢ m z2 < d - 1
2
.....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]
⊢ λx,y. R[x;y]^* z2 w
3
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))
⊢ ∃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. 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]
\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{}w\mkleeneclose{}] 7\mcdot{} THENA Auto)
Home
Index