---

Step * 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))
⊢ x = y ∈ T
BY
{ ((FLemma `rel_star_iff` [-3] THENA Auto) THEN D -1 THEN Auto THEN (InstHyp [⌜x⌝] (-2)⋅ THENA Auto) THEN D -1) }

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. ((x (R^*) z) ∧ (z R y))
⊢ 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))
\mvdash{}  x  =  y


By

---

Latex:
((FLemma  `rel\_star\_iff`  [-3]  THENA  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index