Nuprl Definition : poss-maj

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

Definitions occuring in Statement :  list_accum: list_accum ifthenelse: if then else fi  eq_int: (i =z j) apply: a spread: spread def pair: <a, b> subtract: m add: m natural_number: $n
Definitions occuring in definition :  list_accum: list_accum spread: spread def apply: a add: m ifthenelse: if then else fi  eq_int: (i =z j) subtract: m pair: <a, b> natural_number: $n
FDL editor aliases :  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  =\msubz{}  0)  then  ə,  z>
            else  <n  -  1,  x>
    over  list:
    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