---

Step * 2 1 of Lemma max_tl_coeffs_wf


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) ∈ ℤ} 
BY
{ TACTIC:(InstLemma `list_accum_wf` [⌜{L:ℤ List| ||L|| = n ∈ ℤ} ⌝;⌜{L:ℤ List| ||L|| = (n - 1) ∈ ℤ} ⌝]⋅ THENA Auto) }

1
1. n : ℕ+
2. u : ℤ List
3. ||u|| = n ∈ ℤ
4. v : {L:ℤ List| ||L|| = n ∈ ℤ}  List
5. 0 < ||[u / v]||
6. valueall-type(ℤ List)
7. ∀[l:{L:ℤ List| ||L|| = n ∈ ℤ}  List]. ∀[y:{L:ℤ List| ||L|| = (n - 1) ∈ ℤ} ]. ∀[f:{L:ℤ List| ||L|| = (n - 1) ∈ ℤ} 
                                                                                  ⟶ {L:ℤ List| ||L|| = n ∈ ℤ} 
                                                                                  ⟶ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} ].
     (accumulate (with value x and list item a):
       f[x;a]
      over list:
        l
      with starting value:
       y) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} )
⊢ 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  :  \mBbbZ{}  List
3.  ||u||  =  n
4.  v  :  \{L:\mBbbZ{}  List|  ||L||  =  n\}    List
5.  0  <  ||[u  /  v]||
6.  valueall-type(\mBbbZ{}  List)
\mvdash{}  accumulate  (with  value  L1  and  list  item  ineq):
      map2(\mlambda{}x,y.  imax(x;|y|);L1;tl(ineq))
    over  list:
        v
    with  starting  value:
      map(\mlambda{}x.|x|;tl(u)))  \mmember{}  \{L:\mBbbZ{}  List|  ||L||  =  (n  -  1)\} 


By

---

Latex:
TACTIC:(InstLemma  `list\_accum\_wf`  [\mkleeneopen{}\{L:\mBbbZ{}  List|  ||L||  =  n\}  \mkleeneclose{};\mkleeneopen{}\{L:\mBbbZ{}  List|  ||L||  =  (n  -  1)\}  \mkleeneclose{}]\mcdot{}
                THENA  Auto
                )

---

Home Index