---

Step * 1 of Lemma imax-list-append2


1. u : ℤ
2. v : ℤ List
3. ∀[bs:ℤ List]. (imax-list(v @ bs) = imax(imax-list(v);imax-list(bs)) ∈ ℤ) supposing (0 < ||bs|| and 0 < ||v||)
4. bs : ℤ List
5. 0 < ||v|| + 1
6. 0 < ||bs||
⊢ imax-list([u / (v @ bs)]) = imax(imax-list([u / v]);imax-list(bs)) ∈ ℤ
BY
{ (Decide 0 < ||v|| THENA Auto) }

1
1. u : ℤ
2. v : ℤ List
3. ∀[bs:ℤ List]. (imax-list(v @ bs) = imax(imax-list(v);imax-list(bs)) ∈ ℤ) supposing (0 < ||bs|| and 0 < ||v||)
4. bs : ℤ List
5. 0 < ||v|| + 1
6. 0 < ||bs||
7. 0 < ||v||
⊢ imax-list([u / (v @ bs)]) = imax(imax-list([u / v]);imax-list(bs)) ∈ ℤ

2
1. u : ℤ
2. v : ℤ List
3. ∀[bs:ℤ List]. (imax-list(v @ bs) = imax(imax-list(v);imax-list(bs)) ∈ ℤ) supposing (0 < ||bs|| and 0 < ||v||)
4. bs : ℤ List
5. 0 < ||v|| + 1
6. 0 < ||bs||
7. ¬0 < ||v||
⊢ imax-list([u / (v @ bs)]) = imax(imax-list([u / v]);imax-list(bs)) ∈ ℤ

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[bs:\mBbbZ{}  List]
          (imax-list(v  @  bs)  =  imax(imax-list(v);imax-list(bs)))  supposing  (0  <  ||bs||  and  0  <  ||v||)
4.  bs  :  \mBbbZ{}  List
5.  0  <  ||v||  +  1
6.  0  <  ||bs||
\mvdash{}  imax-list([u  /  (v  @  bs)])  =  imax(imax-list([u  /  v]);imax-list(bs))


By

---

Latex:
(Decide  0  <  ||v||  THENA  Auto)

---

Home Index