Nuprl Rule : remainderBounds1

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

  BY remainderBounds1 ()
  
  H  ⊢ if (0) < (a)  then True  else False
  H  ⊢ if (0) < (b)  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  (a  rem  b)  <  (b)    then  True    else  False

    BY  remainderBounds1  ()
   
    H    \mvdash{}  if  (0)  <  (a)    then  True    else  False
    H    \mvdash{}  if  (0)  <  (b)    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_05

Theory : rules


Home Index