• 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. E.g.
  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 finished in 1.7 seconds.