Nuprl Definition : greatest-p-zero

greatest-p-zero(n;a) ==  primrec(n;0;λi,v. if (a (i + 1) =z 0) then i + 1 else v fi )


Definitions occuring in Statement :  primrec: primrec(n;b;c),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x],  add: n + m,  natural_number: $n
Definitions occuring in definition :  primrec: primrec(n;b;c),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  add: n + m,  natural_number: $n
FDL editor aliases :  greatest-p-zero
Latex:
greatest-p-zero(n;a)  ==    primrec(n;0;\mlambda{}i,v.  if  (a  (i  +  1)  =\msubz{}  0)  then  i  +  1  else  v  fi  )


Date html generated: 2018_05_21-PM-03_22_00
Last ObjectModification: 2018_01_29-AM-09_39_25

Theory : rings_1


Home Index