Nuprl Definition : llex
llex(A;a,b.<[a; b]) ==
λL1,L2. ((||L1|| < ||L2|| ∧ (∀i:ℕ||L1||. (L1[i] = L2[i] ∈ A)))
∨ (∃i:ℕ. (i < ||L1|| ∧ i < ||L2|| ∧ (∀j:ℕi. (L1[j] = L2[j] ∈ A)) ∧ <[L1[i]; L2[i]])))
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
lambda: λx.A[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
or: P ∨ Q,
exists: ∃x:A. B[x],
nat: ℕ,
less_than: a < b,
length: ||as||,
and: P ∧ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
equal: s = t ∈ T,
select: L[n]
FDL editor aliases :
llex
Latex:
llex(A;a,b.<[a; b]) ==
\mlambda{}L1,L2. ((||L1|| < ||L2|| \mwedge{} (\mforall{}i:\mBbbN{}||L1||. (L1[i] = L2[i])))
\mvee{} (\mexists{}i:\mBbbN{}. (i < ||L1|| \mwedge{} i < ||L2|| \mwedge{} (\mforall{}j:\mBbbN{}i. (L1[j] = L2[j])) \mwedge{} <[L1[i]; L2[i]])))
Date html generated:
2016_05_15-PM-04_17_11
Last ObjectModification:
2015_09_23-AM-07_47_49
Theory : general
Home
Index