ComputerDivision: THEORY
 BEGIN
  IMPORTING Int
  IMPORTING Abs
  % do not edit above this line
  
  IMPORTING ints@div, ints@rem
  
  div_total(x: int): int
  
  % Why3 div
  div(x:int,
    x1:int): MACRO int =  IF x1 /= 0 THEN div(x, x1) ELSE div_total(x) ENDIF
  
  % Why3 mod1
  mod1(x:int, x1:int): int
  
  mod_total(x: int): int
  
  % Why3 div_mod
  div_mod: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,
    y)) + mod1(x, y)))
  
  % Why3 div_bound
  div_bound: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y >  0)) =>
    ((0 <= div(x, y)) AND (div(x, y) <= x))
  
  % Why3 mod_bound
  mod_bound: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) =>
    (((-abs(y)) <  mod1(x, y)) AND (mod1(x, y) <  abs(y)))
  
  % Why3 div_sign_pos
  div_sign_pos: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y >  0)) =>
    (div(x, y) >= 0)
  
  % Why3 div_sign_neg
  div_sign_neg: LEMMA FORALL (x:int, y:int): ((x <= 0) AND (y >  0)) =>
    (div(x, y) <= 0)
  
  % Why3 mod_sign_pos
  mod_sign_pos: LEMMA FORALL (x:int, y:int): ((x >= 0) AND NOT (y = 0)) =>
    (mod1(x, y) >= 0)
  
  % Why3 mod_sign_neg
  mod_sign_neg: LEMMA FORALL (x:int, y:int): ((x <= 0) AND NOT (y = 0)) =>
    (mod1(x, y) <= 0)
  
  % Why3 rounds_toward_zero
  rounds_toward_zero: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) =>
    (abs((div(x, y) * y)) <= abs(x))
  
  % Why3 div_1
  div_1: LEMMA FORALL (x:int): (div(x, 1) = x)
  
  % Why3 mod_1
  mod_1: LEMMA FORALL (x:int): (mod1(x, 1) = 0)
  
  % Why3 div_inf
  div_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x <  y)) => (div(x,
    y) = 0)
  
  % Why3 mod_inf
  mod_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x <  y)) => (mod1(x,
    y) = x)
  
  % Why3 div_mult
  div_mult: LEMMA FORALL (x:int, y:int, z:int): ((x >  0) AND ((y >= 0) AND
    (z >= 0))) => (div(((x * y) + z), x) = (y + div(z, x)))
  
  % Why3 mod_mult
  mod_mult: LEMMA FORALL (x:int, y:int, z:int): ((x >  0) AND ((y >= 0) AND
    (z >= 0))) => (mod1(((x * y) + z), x) = mod1(z, x))
  
  
 END ComputerDivision