---

Step * of Lemma rel_star_order

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (WellFnd{i}(T;x,y.x R y) ⇒ Order(T;x,y.x (R^*) y))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN D 0
   THEN Auto
   THEN Try ((BLemma `rel_star_weakening` THEN Complete (Auto)))
   THEN Try ((Using [`y',⌜b⌝] (BLemma `rel_star_transitivity`)⋅ THEN 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
⊢ x = y ∈ T

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  Try  ((BLemma  `rel\_star\_weakening`  THEN  Complete  (Auto)))
  THEN  Try  ((Using  [`y',\mkleeneopen{}b\mkleeneclose{}]  (BLemma  `rel\_star\_transitivity`)\mcdot{}  THEN  Auto)))

---

Home Index