Problems
Modulo arithmetic
Simple inequalities don't hold!
i < base+size ⇔ i-base < size ?
base ≤ i ⇒ base ≤ i+1 ?
Termination checking
Used forms of recursion not recognized by the termination checker.