---

Step * 1 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
11. x (R^*) z
12. z R y
13. z R+ x
⊢ x R+ x
BY
{ (FLemma `rel-star-rel-plus3` [-3;-1] THEN Auto)⋅ }

---

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.  z  :  T
11.  x  rel\_star(T;  R)  z
12.  z  R  y
13.  z  R\msupplus{}  x
\mvdash{}  x  R\msupplus{}  x


By

---

Latex:
(FLemma  `rel-star-rel-plus3`  [-3;-1]  THEN  Auto)\mcdot{}

---

Home Index