---

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


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

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

---

Latex:



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


By

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

---

Home Index