Nuprl Rule : remNegative

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

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

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

    BY  remNegative  ()
   
    H    \mvdash{}  if  (a)  <  (0)    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_23
Last ObjectModification: 2018_08_20-AM-11_20_45

Theory : rules


Home Index