---

Step * of Lemma null-mklist

∀[n:ℤ]. ∀[f:Top].  (null(mklist(n;f)) ~ n ≤z 0)
BY
{ xxx(Auto THEN BoolCase ⌜n ≤z 0⌝⋅ THEN Auto)xxx }

1
1. n : ℤ
2. f : Top
3. n ≤ 0
⊢ null(mklist(n;f)) ~ tt

2
1. n : ℤ
2. ¬(n ≤ 0)
3. f : Top
⊢ null(mklist(n;f)) ~ ff

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[f:Top].    (null(mklist(n;f))  \msim{}  n  \mleq{}z  0)


By

---

Latex:
xxx(Auto  THEN  BoolCase  \mkleeneopen{}n  \mleq{}z  0\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index