---

Step * 1 1 1 of Lemma rel_star_order


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;x,y.x R y)@i'
4. Trans(T;x,y.x (R^*) y)
5. x : T@i
6. y : T@i
7. x (R^*) y@i
8. y (R^*) x@i
9. ∀x:T. (¬(x R+ x))
10. ∃z:T. ((x (R^*) z) ∧ (z R y))
⊢ x R+ x
BY
{ (ExRepD THEN (FLemma `rel-star-rel-plus2` [-1;8]  THENA Auto))⋅ }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;x,y.x R y)@i'
4. Trans(T;x,y.x (R^*) y)
5. x : T@i
6. y : T@i
7. x (R^*) y@i
8. y (R^*) x@i
9. ∀x:T. (¬(x R+ x))
10. z : T
11. x (R^*) z
12. z R y
13. z R+ x
⊢ x R+ x

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  WellFnd\{i\}(T;x,y.x  R  y)@i'
4.  Trans(T;x,y.x  rel\_star(T;  R)  y)
5.  x  :  T@i
6.  y  :  T@i
7.  x  rel\_star(T;  R)  y@i
8.  y  rel\_star(T;  R)  x@i
9.  \mforall{}x:T.  (\mneg{}(x  R\msupplus{}  x))
10.  \mexists{}z:T.  ((x  rel\_star(T;  R)  z)  \mwedge{}  (z  R  y))
\mvdash{}  x  R\msupplus{}  x


By

---

Latex:
(ExRepD  THEN  (FLemma  `rel-star-rel-plus2`  [-1;8]    THENA  Auto))\mcdot{}

---

Home Index