Nuprl Definition : strict-majority
strict-majority(eq;L) ==
let ms = filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)) in
if null(ms) then inr ⋅ else inl (fst(hd(ms))) fi
Definitions occuring in Statement :
count-repeats: count-repeats(L,eq),
hd: hd(l),
length: ||as||,
null: null(as),
filter: filter(P;l),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
let: let,
it: ⋅,
pi1: fst(t),
pi2: snd(t),
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
let: let,
filter: filter(P;l),
lambda: λx.A[x],
lt_int: i <z j,
length: ||as||,
multiply: n * m,
natural_number: $n,
pi2: snd(t),
count-repeats: count-repeats(L,eq),
ifthenelse: if b then t else f fi ,
null: null(as),
inr: inr x ,
it: ⋅,
inl: inl x,
pi1: fst(t),
hd: hd(l)
FDL editor aliases :
strict-majority
Latex:
strict-majority(eq;L) ==
let ms = filter(\mlambda{}p.||L|| <z 2 * (snd(p));count-repeats(L,eq)) in
if null(ms) then inr \mcdot{} else inl (fst(hd(ms))) fi
Date html generated:
2016_05_14-PM-03_23_22
Last ObjectModification:
2015_09_22-PM-05_59_30
Theory : decidable!equality
Home
Index