---

Step * 1 of Lemma test-arith


1. x : ℤ
2. y : ℤ
3. z : ℤ
4. (y + 1) ≤ x@i
5. (z + 1) ≤ y@i
6. (x + (-1)) ≤ z@i
⊢ False
BY
{ ArithAux
THEN Auto }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  z  :  \mBbbZ{}
4.  (y  +  1)  \mleq{}  x@i
5.  (z  +  1)  \mleq{}  y@i
6.  (x  +  (-1))  \mleq{}  z@i
\mvdash{}  False


By

---

Latex:
ArithAux
THEN  Auto

---

Home Index