---

Step * 2 of Lemma max_tl_coeffs_wf


1. n : ℕ+
2. u : {L:ℤ List| ||L|| = n ∈ ℤ} 
3. v : {L:ℤ List| ||L|| = n ∈ ℤ}  List
4. 0 < ||[u / v]||
⊢ max_tl_coeffs([u / v]) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} 
BY
{ TACTIC:(DVar `u'
          THEN Unfold `max_tl_coeffs` 0
          THEN (Assert valueall-type(ℤ List) BY
                      Auto)
          THEN (RWO "eager-accum-list_accum" 0 THENA Auto)
          THEN Try (Hypothesis)
          THEN Reduce 0) }

1
1. n : ℕ+
2. u : ℤ List
3. ||u|| = n ∈ ℤ
4. v : {L:ℤ List| ||L|| = n ∈ ℤ}  List
5. 0 < ||[u / v]||
6. valueall-type(ℤ List)
⊢ accumulate (with value L1 and list item ineq):
   map2(λx,y. imax(x;|y|);L1;tl(ineq))
  over list:
    v
  with starting value:
   map(λx.|x|;tl(u))) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} 

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  u  :  \{L:\mBbbZ{}  List|  ||L||  =  n\} 
3.  v  :  \{L:\mBbbZ{}  List|  ||L||  =  n\}    List
4.  0  <  ||[u  /  v]||
\mvdash{}  max\_tl\_coeffs([u  /  v])  \mmember{}  \{L:\mBbbZ{}  List|  ||L||  =  (n  -  1)\} 


By

---

Latex:
TACTIC:(DVar  `u'
                THEN  Unfold  `max\_tl\_coeffs`  0
                THEN  (Assert  valueall-type(\mBbbZ{}  List)  BY
                                        Auto)
                THEN  (RWO  "eager-accum-list\_accum"  0  THENA  Auto)
                THEN  Try  (Hypothesis)
                THEN  Reduce  0)

---

Home Index