---

Step * 2 3 1 of Lemma imax-list_functionality

.....assertion..... 
1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. set-equal(ℤ;L;L')
5. imax-list(L) ≤ imax-list(L')
6. imax-list(L') ≤ imax-list(L)
⊢ 0 < ||L'||
BY
{ (D 2 THEN Auto) }

1
1. L : ℤ List
2. 0 < ||L||
3. set-equal(ℤ;L;[])
4. imax-list(L) ≤ imax-list([])
5. imax-list([]) ≤ imax-list(L)
⊢ 0 < ||[]||

---

Latex:

---

Latex:
.....assertion..... 
1.  L  :  \mBbbZ{}  List
2.  L'  :  \mBbbZ{}  List
3.  0  <  ||L||
4.  set-equal(\mBbbZ{};L;L')
5.  imax-list(L)  \mleq{}  imax-list(L')
6.  imax-list(L')  \mleq{}  imax-list(L)
\mvdash{}  0  <  ||L'||


By

---

Latex:
(D  2  THEN  Auto)

---

Home Index