ASSUME a1 a2

INVARIANT i1