Nuprl Rule : remPositive

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

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

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

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


Date html generated: 2019_06_20-PM-04_12_22
Last ObjectModification: 2018_08_20-AM-11_34_12

Theory : rules


Home Index