Nuprl Definition : strict-majority-or-max

strict-majority-or-max(L) ==
  case strict-majority(IntDeq;L) of inl(x) => inr(z) => if null(L) then 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 then else fi  decide: case of inl(x) => s[x] inr(y) => t[y] natural_number: $n
Definitions occuring in definition :  decide: case of inl(x) => s[x] inr(y) => t[y] strict-majority: strict-majority(eq;L) int-deq: IntDeq ifthenelse: if then else fi  null: null(as) natural_number: $n imax-list: imax-list(L)
FDL editor aliases :  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 

Date html generated: 2016_05_14-PM-03_23_50
Last ObjectModification: 2015_09_22-PM-05_59_31

Theory : decidable!equality

Home Index