---

Step * 2 1 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)
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) ∈ ℤ} 
BY
{ TACTIC:(BHyp -1 THEN Auto) }

---

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)
7.  \mforall{}[l:\{L:\mBbbZ{}  List|  ||L||  =  n\}    List].  \mforall{}[y:\{L:\mBbbZ{}  List|  ||L||  =  (n  -  1)\}  ].  \mforall{}[f:\{L:\mBbbZ{}  List| 
                                                                                                                                                      ||L||  =  (n  -  1)\} 
                                                                                                                                                    {}\mrightarrow{}  \{L:\mBbbZ{}  List|  ||L||  =  n\} 
                                                                                                                                                    {}\mrightarrow{}  \{L:\mBbbZ{}  List| 
                                                                                                                                                            ||L||  =  (n  -  1)\}  ].
          (accumulate  (with  value  x  and  list  item  a):
              f[x;a]
            over  list:
                l
            with  starting  value:
              y)  \mmember{}  \{L:\mBbbZ{}  List|  ||L||  =  (n  -  1)\}  )
\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:(BHyp  -1  THEN  Auto)

---

Home Index