Step * 1 1 of Lemma imax-list-append2


1. : ℤ
2. : ℤ 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
(RWW "imax-list-cons imax_assoc" THEN Auto) }


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.  0  <  ||v||
\mvdash{}  imax-list([u  /  (v  @  bs)])  =  imax(imax-list([u  /  v]);imax-list(bs))


By


Latex:
(RWW  "imax-list-cons  4  imax\_assoc"  0  THEN  Auto)




Home Index