Nuprl Definition : count_pairs
count(x < y in L | P[x; y]) == sum(if i <z j ∧b P[L[i]; L[j]] then 1 else 0 fi | i < ||L||; j < ||L||)
Definitions occuring in Statement :
double_sum: sum(f[x; y] | x < n; y < m),
select: L[n],
length: ||as||,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
natural_number: $n
Definitions occuring in definition :
double_sum: sum(f[x; y] | x < n; y < m),
length: ||as||,
ifthenelse: if b then t else f fi ,
band: p ∧b q,
lt_int: i <z j,
select: L[n],
natural_number: $n
FDL editor aliases :
count_pairs
Latex:
count(x < y in L | P[x; y]) ==
sum(if i <z j \mwedge{}\msubb{} P[L[i]; L[j]] then 1 else 0 fi | i < ||L||; j < ||L||)
Date html generated:
2016_05_15-PM-02_05_31
Last ObjectModification:
2015_09_23-AM-07_37_50
Theory : list!
Home
Index