---

Step * of Lemma imax-list-append

∀[as,bs:ℤ List].  imax-list(as @ bs) = imax-list(bs @ as) ∈ ℤ supposing 0 < ||as @ bs||
BY
{ (Auto
   THEN RepUR ``imax-list`` 0
   THEN BLemma `combine-list-append`
   THEN Auto
   THEN RepUR ``assoc comm`` 0
   THEN Auto
   THEN (BLemma `imax_com`⋅ ORELSE BLemma `imax_assoc`)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``imax-list``  0
  THEN  BLemma  `combine-list-append`
  THEN  Auto
  THEN  RepUR  ``assoc  comm``  0
  THEN  Auto
  THEN  (BLemma  `imax\_com`\mcdot{}  ORELSE  BLemma  `imax\_assoc`)
  THEN  Auto)

---

Home Index