---

Step * of Lemma imax-list-append2

∀[as,bs:ℤ List].  (imax-list(as @ bs) = imax(imax-list(as);imax-list(bs)) ∈ ℤ) supposing (0 < ||bs|| and 0 < ||as||)
BY
{ (InductionOnList THEN Reduce 0 THEN 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||
⊢ imax-list([u / (v @ bs)]) = imax(imax-list([u / v]);imax-list(bs)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[as,bs:\mBbbZ{}  List].
    (imax-list(as  @  bs)  =  imax(imax-list(as);imax-list(bs)))  supposing  (0  <  ||bs||  and  0  <  ||as||)


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index