Nuprl Definition : l_member!
(x ∈! l) == ∃i:ℕ. (i < ||l|| c∧ ((x = l[i] ∈ T) ∧ (∀j:ℕ. (j < ||l|| ⇒ (x = l[j] ∈ T) ⇒ (j = i ∈ ℕ)))))
Definitions occuring in Statement :
select: L[n],
length: ||as||,
nat: ℕ,
less_than: a < b,
cand: A c∧ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
cand: A c∧ B,
and: P ∧ Q,
all: ∀x:A. B[x],
less_than: a < b,
length: ||as||,
implies: P ⇒ Q,
select: L[n],
equal: s = t ∈ T,
nat: ℕ
FDL editor aliases :
l_member!
Latex:
(x \mmember{}! l) == \mexists{}i:\mBbbN{}. (i < ||l|| c\mwedge{} ((x = l[i]) \mwedge{} (\mforall{}j:\mBbbN{}. (j < ||l|| {}\mRightarrow{} (x = l[j]) {}\mRightarrow{} (j = i)))))
Date html generated:
2016_05_14-AM-07_52_07
Last ObjectModification:
2015_09_22-PM-05_54_07
Theory : list_1
Home
Index