Nuprl Definition : strict-majority-or-max
strict-majority-or-max(L) ==
case strict-majority(IntDeq;L) of inl(x) => x | inr(z) => if null(L) then 0 else imax-list(L) fi
Definitions occuring in Statement :
strict-majority: strict-majority(eq;L),
imax-list: imax-list(L),
null: null(as),
int-deq: IntDeq,
ifthenelse: if b then t else f fi ,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
strict-majority: strict-majority(eq;L),
int-deq: IntDeq,
ifthenelse: if b then t else f fi ,
null: null(as),
natural_number: $n,
imax-list: imax-list(L)
FDL editor aliases :
strict-majority-or-max
Latex:
strict-majority-or-max(L) ==
case strict-majority(IntDeq;L) of inl(x) => x | inr(z) => if null(L) then 0 else imax-list(L) fi
Date html generated:
2016_05_14-PM-03_23_50
Last ObjectModification:
2015_09_22-PM-05_59_31
Theory : decidable!equality
Home
Index