Step * of Lemma rel-star-rel-plus

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y,z:T.  ((x (R^*) y)  (y z)  (x R+ z))
BY
(Unfolds ``rel_star rel_plus`` THEN Reduce THEN Auto THEN ExRepD) }

1
1. [T] Type
2. [R] T ⟶ T ⟶ ℙ
3. T@i
4. T@i
5. T@i
6. : ℕ@i
7. R^n y@i
8. z@i
⊢ ∃n:ℕ+(x R^n z)


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y,z:T.    ((x  rel\_star(T;  R)  y)  {}\mRightarrow{}  (y  R  z)  {}\mRightarrow{}  (x  R\msupplus{}  z))


By


Latex:
(Unfolds  ``rel\_star  rel\_plus``  0  THEN  Reduce  0  THEN  Auto  THEN  ExRepD)




Home Index