Nuprl Definition : poss-maj

poss-maj(eq;L;x) ==
  accumulate (with value p and list item z):
   let n,x = p 
   in if eq z x then <n + 1, x>
      if (n =z 0) then <1, z>
      else <n - 1, x>
      fi 
  over list:
    L
  with starting value:
   <0, x>)


Definitions occuring in Statement :  list_accum: list_accum,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  spread: spread def,  pair: <a, b>,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  list_accum: list_accum,  spread: spread def,  apply: f a,  add: n + m,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  subtract: n - m,  pair: <a, b>,  natural_number: $n
FDL editor aliases :  poss-maj
Latex:
poss-maj(eq;L;x)  ==
    accumulate  (with  value  p  and  list  item  z):
      let  n,x  =  p 
      in  if  eq  z  x  then  <n  +  1,  x>
            if  (n  =\msubz{}  0)  then  ə,  z>
            else  <n  -  1,  x>
            fi 
    over  list:
        L
    with  starting  value:
      ɘ,  x>)


Date html generated: 2016_05_14-PM-03_22_13
Last ObjectModification: 2015_09_22-PM-05_59_28

Theory : decidable!equality


Home Index