---

Step * 1 of Lemma testnlrst


1. es : EO@i'
2. A : Type@i'
3. A ⊆r E@i
4. a : A@i
5. b : A@i
6. c : A@i
7. (a < b)@i
8. (b < c)@i
9. (c < a)@i
⊢ False
BY
{ (RelRST  THEN (RelRST ORELSE AddHiddenLabel `no loop`) THEN Auto) }

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  A  :  Type@i'
3.  A  \msubseteq{}r  E@i
4.  a  :  A@i
5.  b  :  A@i
6.  c  :  A@i
7.  (a  <  b)@i
8.  (b  <  c)@i
9.  (c  <  a)@i
\mvdash{}  False


By

---

Latex:
(RelRST    THEN  (RelRST  ORELSE  AddHiddenLabel  `no  loop`)  THEN  Auto)

---

Home Index