---

Step * of Lemma rel_star_closure2

∀[T:Type]. ∀[R,R2:T ⟶ T ⟶ ℙ].
  (Refl(T)(R2[_1;_2]) ⇒ Trans(T)(R2[_1;_2]) ⇒ (∀x,y:T.  ((x R y) ⇒ R2[x;y])) ⇒ (∀x,y:T.  ((x (R^*) y) ⇒ R2[x;y])))
BY
{ (((Auto THEN InstLemma `rel_star_closure` [T;R;R2;x;y]) THENA Auto) THEN D (-1)) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [R2] : T ⟶ T ⟶ ℙ
4. Refl(T)(R2[_1;_2])
5. Trans(T)(R2[_1;_2])
6. ∀x,y:T.  ((x R y) ⇒ R2[x;y])
7. x : T
8. y : T
9. x (R^*) y
10. x R2 y
⊢ R2[x;y]

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [R2] : T ⟶ T ⟶ ℙ
4. Refl(T)(R2[_1;_2])
5. Trans(T)(R2[_1;_2])
6. ∀x,y:T.  ((x R y) ⇒ R2[x;y])
7. x : T
8. y : T
9. x (R^*) y
10. x = y ∈ T
⊢ R2[x;y]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (Refl(T)(R2[$_{1}$;$_{2}$])
    {}\mRightarrow{}  Trans(T)(R2[$_{1}$;$_{2}$])
    {}\mRightarrow{}  (\mforall{}x,y:T.    ((x  R  y)  {}\mRightarrow{}  R2[x;y]))
    {}\mRightarrow{}  (\mforall{}x,y:T.    ((x  rel\_star(T;  R)  y)  {}\mRightarrow{}  R2[x;y])))


By

---

Latex:
(((Auto  THEN  InstLemma  `rel\_star\_closure`  [T;R;R2;x;y])  THENA  Auto)  THEN  D  (-1))

---

Home Index