---

Step * of Lemma qmin-assoc

Assoc(ℚ;λx,y. qmin(x;y))
BY
{ ((D 0 THEN Auto) THEN RepUR ``qmin`` 0 THEN RepeatFor 4 (AutoSplit))⋅ }

1
1. x : ℚ
2. y : ℚ
3. ¬(x ≤ y)
4. z : ℚ
5. ¬(y ≤ z)
6. ¬(y ≤ z)
7. x ≤ z
⊢ x = z ∈ ℚ

---

Latex:

---

Latex:
Assoc(\mBbbQ{};\mlambda{}x,y.  qmin(x;y))


By

---

Latex:
((D  0  THEN  Auto)  THEN  RepUR  ``qmin``  0  THEN  RepeatFor  4  (AutoSplit))\mcdot{}

---

Home Index