---

Step * 1 of Lemma ranked-eo-first


1. L : Top
2. rk : Top
3. e : Id × ℤ
⊢ first(e) ~ (snd(e) =z 0)
BY
{ (D -1 THEN RepUR ``es-first`` 0 THEN (RWO "ranked-eo-dom" 0 THENA Auto) THEN Reduce 0) }

1
1. L : Top
2. rk : Top
3. e1 : Id
4. e2 : ℤ
⊢ pred(<e1, e2>) = <e1, e2> ∨bff ~ (e2 =z 0)

---

Latex:

---

Latex:

1.  L  :  Top
2.  rk  :  Top
3.  e  :  Id  \mtimes{}  \mBbbZ{}
\mvdash{}  first(e)  \msim{}  (snd(e)  =\msubz{}  0)


By

---

Latex:
(D  -1  THEN  RepUR  ``es-first``  0  THEN  (RWO  "ranked-eo-dom"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index