Nuprl Definition : l_succ
y = succ(x) in l⇒ P[y] == ∀i:ℕ. (i + 1 < ||l|| ⇒ (l[i] = x ∈ T) ⇒ P[l[i + 1]])
Definitions occuring in Statement :
select: L[n],
length: ||as||,
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
add: n + m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
nat: ℕ,
less_than: a < b,
length: ||as||,
implies: P ⇒ Q,
equal: s = t ∈ T,
select: L[n],
add: n + m,
natural_number: $n
FDL editor aliases :
l_succ
Latex:
y = succ(x) in l{}\mRightarrow{} P[y] == \mforall{}i:\mBbbN{}. (i + 1 < ||l|| {}\mRightarrow{} (l[i] = x) {}\mRightarrow{} P[l[i + 1]])
Date html generated:
2016_05_15-PM-01_53_46
Last ObjectModification:
2015_09_23-AM-07_37_23
Theory : list!
Home
Index