---

Step * 2 1 of Lemma imax-list_functionality

.....antecedent..... 
1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. set-equal(ℤ;L;L')
5. imax-list(L) ≤ imax-list(L')
⊢ 0 < ||L'||
BY
{ (DVar `L'
   THEN All Reduce
   THEN Auto
   THEN Unfold `set-equal` (-2)
   THEN (InstHyp [⌜u⌝] (-2)⋅ THENA Auto)
   THEN D (-1)
   THEN D -2
   THEN Auto
   THEN (D 3 THEN Reduce 0 THEN Auto')
   THEN AutoSimpHyp Auto (-1)
   ⋅) }

---

Latex:

---

Latex:
.....antecedent..... 
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')
\mvdash{}  0  <  ||L'||


By

---

Latex:
(DVar  `L'
  THEN  All  Reduce
  THEN  Auto
  THEN  Unfold  `set-equal`  (-2)
  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  D  -2
  THEN  Auto
  THEN  (D  3  THEN  Reduce  0  THEN  Auto')
  THEN  AutoSimpHyp  Auto  (-1)
  \mcdot{})

---

Home Index