---

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


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

1
1. v : ℤ List
2. ¬(v = [] ∈ (ℤ List))
⊢ ¬(imax-list(v) + 1 ∈ v)

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}  List
\mvdash{}  \mneg{}(if  null(v)  then  0  else  imax-list(v)  +  1  fi    \mmember{}  v)


By

---

Latex:
AutoSplit

---

Home Index