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