---

Step * 1 2 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||
7. ¬0 < ||v||
⊢ imax-list([u / (v @ bs)]) = imax(imax-list([u / v]);imax-list(bs)) ∈ ℤ
BY
{ (DVar `v' THEN All Reduce THEN Try ((D (-1) THEN Complete (Auto')))) }

1
1. u : ℤ
2. ∀[bs:ℤ List]. (imax-list(bs) = imax(imax-list([]);imax-list(bs)) ∈ ℤ) supposing (0 < ||bs|| and 0 < 0)
3. bs : ℤ List
4. 0 < 1
5. 0 < ||bs||
6. ¬0 < 0
⊢ imax-list([u / bs]) = imax(u;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||
7.  \mneg{}0  <  ||v||
\mvdash{}  imax-list([u  /  (v  @  bs)])  =  imax(imax-list([u  /  v]);imax-list(bs))


By

---

Latex:
(DVar  `v'  THEN  All  Reduce  THEN  Try  ((D  (-1)  THEN  Complete  (Auto'))))

---

Home Index