---

Step * of Lemma rmin-assoc

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

---

Latex:

---

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


By

---

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

---

Home Index