Nuprl Definition : no_rel_repeats
no_rel_repeats(T;R;l) == ∀i,j:ℕ. (i < ||l|| ⇒ j < ||l|| ⇒ (¬(i = j ∈ ℕ)) ⇒ (¬(R l[i] l[j])))
Definitions occuring in Statement :
select: L[n],
length: ||as||,
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
less_than: a < b,
length: ||as||,
implies: P ⇒ Q,
equal: s = t ∈ T,
nat: ℕ,
not: ¬A,
apply: f a,
select: L[n]
FDL editor aliases :
no_rel_repeats
Latex:
no\_rel\_repeats(T;R;l) == \mforall{}i,j:\mBbbN{}. (i < ||l|| {}\mRightarrow{} j < ||l|| {}\mRightarrow{} (\mneg{}(i = j)) {}\mRightarrow{} (\mneg{}(R l[i] l[j])))
Date html generated:
2016_05_14-PM-03_25_32
Last ObjectModification:
2015_09_22-PM-05_59_43
Theory : decidable!equality
Home
Index