amavect

  size_t i = size;
  while(i-- > 0){
    // loop body, possibly break
  }
  use(i); // i wraps below 0

  size_t i = size;
  while(i > 0){
    i--;
    // loop body, possibly break
  }
  use(i); // i doesn't wrap

  Ensure y+x ≤ INT_MAX.
  If x ≤ UINT_MAX-y, then x+y evaluates correctly:
  ∀x∀y(x ≤ UINT_MAX-y → ∃z(z = y+x))

  Ensure y-x ≤ INT_MAX.
  If x≤y, then y-x evaluates correctly:
  ∀x∀y(x≤y → ∃z(z = y-x))

  Ensure INT_MIN ≤ y+x and y+x ≤ INT_MAX.
  To avoid overflow or underflow, first compare x to 0.
  In the case x≤0, INT_MIN-x cannot underflow, and y+x cannot overflow. If y compares greater than INT_MIN-x, then y+x evaluates correctly.
  In the case 0≤x, then INT_MAX-x cannot overflow, and y+x cannot underflow. And if y compares less than INT_MAX-x, then y+x evaluates correctly.
  ∀x∀y((x≤0 ∧ INT_MIN-x≤y)∨(0≤x ∧ y≤INT_MAX-x) → ∃z(z = y-x))

  Ensure INT_MIN ≤ y-x and y-x ≤ INT_MAX.
  To avoid overflow or underflow, first compare x to 0.
  In the case 0≤x, INT_MIN+x cannot underflow, and y-x cannot overflow. If y compares greater than INT_MIN+x, then y-x evaluates correctly.
  In the case x≤0, INT_MAX+x cannot overflow, and y-x cannot underflow. If y compares less than INT_MAX+x, then y-x evaluates correctly.
  ∀x∀y((0≤x ∧ INT_MIN-x≤y)∨(x≤0 ∧ y≤INT_MAX+x) → ∃z(z = y-x))

  for(size_t i = 0; i < size; i++){
    // loop body
  }
  for(size_t i = size; i > 0;){ i--;
    // loop body
  }

  dB_P = log(10)/10
  dB_F = log(10)/20
  log(10*V) = log(V) + 20*dB_F  // the level of 10 V equals 20 dB more than the power level of 1 V.

  SPL = 20*10^-6 * Pa
  hearing_damage = log(SPL) + 90*dB_F  // hearing damage occurs over 90 dB_F above SPL (neglecting A-weighting)
  pow(hearing_damage) = pow(log(SPL) + 90*dB_F))
  pow(hearing_damage) = pow(log(SPL) + 90*log(10)/20))
  pow(hearing_damage) = SPL*pow(90*log(10)/20))
  pow(hearing_damage) = SPL*31622.7766  // the pressure of hearing damage occurs above 31622 times SPL
  pow(hearing_damage) = 0.632455532 Pa  // the pressure of hearing damage occurs above 0.632 Pa

  log(reference_unit) + value*dB_F (or dB_P)
  log(reference_unit) - value*dB_F (or dB_P)

  log(freq) = pitch
  freq = pow(pitch)
  octave = log(2)

  400*Hz = 100*Hz*4  // the frequency 400 Hz equals 4 times 100 Hz
  log(400*Hz) = log(100*Hz) + log(4)
  log(400*Hz) = log(100*Hz) + 2*log(2)
  log(400*Hz) = log(100*Hz) + 2*octave
  log(400*Hz) = log(100*Hz) + 2*octave  // the pitch of 400 Hz equals 2 octaves above the pitch of 100 Hz

  cent = log(2)/1200
  A4 = log(440*Hz)
  B4 = A4 + 200*cent  // the pitch B4 equals 200 cents above A4
  B4 = log(440*Hz) + 200*log(2)/1200
  B4 = log(440*Hz) + log(2^(2/12))
  B4 = log(440*Hz * 2^(2/12))
  pow(B4) = 493.883 Hz  // the frequency of B4 equals 493.883 Hz

  pow(log(440*Hz) + 200*log(2)/1200)
  exp(ln(440) + 200*ln(2)/1200)

  import ln, floor
  define log := (num,base) -> ln(num) / ln(base)
  define digits := (num,base) -> floor(log(num,base) + 1)
  define tobits := (base) -> log(base,2)
  define infocost := (num,base) -> digits(num,base) * tobits(base)
  define infocost_wikipedia := (num,base) -> digits(num,base) * base
  define infocost_tbwtc := (num, base) -> (digits(num,base) - 1) * tobits(base) + tobits(base- 1)