---

Step * 3 1 1 1 1 1 of Lemma mFOL-bound-rename


1. v : ℤ List
⊢ ∃z':ℤ. (¬(z' ∈ v))
BY
{ (With ⌜if null(v) then 0 else imax-list(v) + 1 fi ⌝ (D 0)⋅ THEN Auto) }

1
1. u : ℤ
2. v : ℤ List
⊢ 0 < ||[u / v]||

2
1. v : ℤ List
⊢ ¬(if null(v) then 0 else imax-list(v) + 1 fi  ∈ v)

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}  List
\mvdash{}  \mexists{}z':\mBbbZ{}.  (\mneg{}(z'  \mmember{}  v))


By

---

Latex:
(With  \mkleeneopen{}if  null(v)  then  0  else  imax-list(v)  +  1  fi  \mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index