• Need to reason about residuals. Try Rustans axioms from krml178. Problem: need additional axioms like
  (forall a:int, b:int :: (((a%n)-b)%n==(a-b)%n));
(forall a:int, b:int :: ((0==(a-b)%n && 0≤a && 0≤b && a<n && b<n) ⇒ a==b));
  to prove lemmas needed for invariance of transitions from A to B. But introduction of those axioms leads to divergence of Z3 on other lemmas needed for invariance of transitions from A to B.
  Solution: Use axioms that partially describe what a%n means for absolute values of a between -3n and 4n, since the proof does not require more.
• Some lemmas need auxiliary forall statements. Solution: use call forall.
  Note: call forall allows writing manual induction. For example:
  procedure TwoPowerXIsPositive(a:int)
requires 0≤a;
ensures TwoPowerX(a)>0;
{
  if(0<a) { call forall TwoPowerXIsPositive(a-1); }
}
procedure TwoPowerXIsMonotone(a:int,b:int)
requires 0≤a && 0≤b && a<b;
ensures TwoPowerX(a)<TwoPowerX(b);
{
  if(a>0) { call forall TwoPowerXIsMonotone(a-1,b-1); }
  else { call forall TwoPowerXIsPositive(b-1); }
}
• Boogie program verifier, version 2011-03-17, finished in 1.7 seconds.
• Boogie program verifier, version 2.2.30705.1126, distributed on 2012-10-22, refused to accept the reminder after division % syntactically. We changed % to Mod. This version finished in 1.03 seconds on an Intel^® Core™ i5-3320M CPU clocked at 2.6 GHz with 8 GB DDR3 RAM clocked at 1600 MHz.