Nuprl Definition : agree_on
agree_on(T;x.P[x]) == λL1,L2. ((||L1|| = ||L2|| ∈ ℤ) c∧ (∀i:ℕ||L1||. ((P[L1[i]] ∨ P[L2[i]]) ⇒ (L1[i] = L2[i] ∈ T))))
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
cand: A c∧ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
lambda: λx.A[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
cand: A c∧ B,
int: ℤ,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
implies: P ⇒ Q,
or: P ∨ Q,
equal: s = t ∈ T,
select: L[n]
FDL editor aliases :
agree_on
Latex:
agree\_on(T;x.P[x]) ==
\mlambda{}L1,L2. ((||L1|| = ||L2||) c\mwedge{} (\mforall{}i:\mBbbN{}||L1||. ((P[L1[i]] \mvee{} P[L2[i]]) {}\mRightarrow{} (L1[i] = L2[i]))))
Date html generated:
2016_05_15-PM-02_05_54
Last ObjectModification:
2015_09_23-AM-07_37_54
Theory : list!
Home
Index