ASSUME a1 a2 INVARIANT i1