Nuprl Rule : remainderBounds3

H  ⊢ if (b) < (a rem b)  then True  else False

  BY remainderBounds3 ()
  
  H  ⊢ if (a) < (0)  then True  else False
  H  ⊢ if (b) < (0)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ



Definitions occuring in rule :  remainder: rem m less: if (a) < (b)  then c  else d natural_number: $n true: True false: False member: t ∈ T int: axiom: Ax

Latex:
H    \mvdash{}  if  (b)  <  (a  rem  b)    then  True    else  False

    BY  remainderBounds3  ()
   
    H    \mvdash{}  if  (a)  <  (0)    then  True    else  False
    H    \mvdash{}  if  (b)  <  (0)    then  True    else  False
    H    \mvdash{}  a  \mmember{}  \mBbbZ{}
    H    \mvdash{}  b  \mmember{}  \mBbbZ{}



Date html generated: 2019_06_20-PM-04_12_23
Last ObjectModification: 2018_08_20-AM-11_34_08

Theory : rules


Home Index