---

Step * 1 of Lemma ranked-eo-info-before

.....subterm..... T:t
1:n
1. L : Id ─→ (Top List)
2. rk : Top
3. e : E
⊢ (snd(e)) = imin(||L (fst(e))||;snd(e)) ∈ ℤ
BY
{ ((RWO "ranked-eo-E-sq" (-1) THENA Auto) THEN D -1 THEN D (-2)⋅ THEN Reduce 0) }

1
1. L : Id ─→ (Top List)
2. rk : Top
3. i : Id
4. e1 : ℕ||L i||
5. True
⊢ e1 = imin(||L i||;e1) ∈ ℤ

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  L  :  Id  {}\mrightarrow{}  (Top  List)
2.  rk  :  Top
3.  e  :  E
\mvdash{}  (snd(e))  =  imin(||L  (fst(e))||;snd(e))


By

---

Latex:
((RWO  "ranked-eo-E-sq"  (-1)  THENA  Auto)  THEN  D  -1  THEN  D  (-2)\mcdot{}  THEN  Reduce  0)

---

Home Index