Nuprl Definition : is_power
is_power(n;z) ==  if (z) < (0)  then (n mod 2 =z 1) ∧b is-power(n;-z)  else is-power(n;z)
Definitions occuring in Statement : 
is-power: is-power(n;x)
, 
band: p ∧b q
, 
modulus: a mod n
, 
eq_int: (i =z j)
, 
less: if (a) < (b)  then c  else d
, 
minus: -n
, 
natural_number: $n
Definitions occuring in definition : 
less: if (a) < (b)  then c  else d
, 
band: p ∧b q
, 
eq_int: (i =z j)
, 
modulus: a mod n
, 
natural_number: $n
, 
minus: -n
, 
is-power: is-power(n;x)
FDL editor aliases : 
is_power
Latex:
is\_power(n;z)  ==    if  (z)  <  (0)    then  (n  mod  2  =\msubz{}  1)  \mwedge{}\msubb{}  is-power(n;-z)    else  is-power(n;z)
Date html generated:
2019_06_20-PM-02_34_26
Last ObjectModification:
2019_03_19-AM-11_34_08
Theory : num_thy_1
Home
Index