---

Step * of Lemma rmax-assoc

∀[x,y,z:ℝ].  (rmax(rmax(x;y);z) = rmax(x;rmax(y;z)))
BY
{ (Auto⋅
   THEN (BLemma `req_weakening` THEN Auto)
   THEN (Assert rmax(rmax(x;y);z) ∈ ℝ BY
               Auto)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN (Ext THENM RepUR ``rmax`` 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbR{}].    (rmax(rmax(x;y);z)  =  rmax(x;rmax(y;z)))


By

---

Latex:
(Auto\mcdot{}
  THEN  (BLemma  `req\_weakening`  THEN  Auto)
  THEN  (Assert  rmax(rmax(x;y);z)  \mmember{}  \mBbbR{}  BY
                          Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  (Ext  THENM  RepUR  ``rmax``  0)
  THEN  Auto)

---

Home Index