Nuprl Definition : strong_before
x << y ∈ l == ((x ∈ l) ∧ (y ∈ l)) ∧ (∀i,j:ℕ. (i < ||l|| ⇒ j < ||l|| ⇒ (l[i] = x ∈ T) ⇒ (l[j] = y ∈ T) ⇒ i < j))
Definitions occuring in Statement :
l_member: (x ∈ l),
select: L[n],
length: ||as||,
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
l_member: (x ∈ l),
all: ∀x:A. B[x],
nat: ℕ,
length: ||as||,
implies: P ⇒ Q,
equal: s = t ∈ T,
select: L[n],
less_than: a < b
FDL editor aliases :
strong_before
Latex:
x << y \mmember{} l ==
((x \mmember{} l) \mwedge{} (y \mmember{} l)) \mwedge{} (\mforall{}i,j:\mBbbN{}. (i < ||l|| {}\mRightarrow{} j < ||l|| {}\mRightarrow{} (l[i] = x) {}\mRightarrow{} (l[j] = y) {}\mRightarrow{} i < j))
Date html generated:
2016_05_15-PM-01_53_40
Last ObjectModification:
2015_09_23-AM-07_37_22
Theory : list!
Home
Index