---

Step * of Lemma utrans_imp_sp_utrans

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (UniformlyTrans(T;a,b.R[a;b]) ⇒ UniformlyTrans(T;a,b.strict_part(x,y.R[x;y];a;b)))
BY
{ ((Unfolds ``utrans strict_part`` 0 THEN GenRepD) THENA Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀[a,b,c:T].  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
4. [a] : T
5. [b] : T
6. [c] : T
7. R[a;b]
8. ¬R[b;a]
9. R[b;c]
10. ¬R[c;b]
⊢ R[a;c]

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀[a,b,c:T].  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
4. a : T
5. b : T
6. c : T
7. R[a;b]
8. ¬R[b;a]
9. R[b;c]
10. ¬R[c;b]
⊢ ¬R[c;a]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (UniformlyTrans(T;a,b.R[a;b])  {}\mRightarrow{}  UniformlyTrans(T;a,b.strict\_part(x,y.R[x;y];a;b)))


By

---

Latex:
((Unfolds  ``utrans  strict\_part``  0  THEN  GenRepD)  THENA  Auto)

---

Home Index