Use the array-component assignment axiom two times to find the (most general) sufficient pre-condition P for the following code fragment:

ASSERT( P ) /* determine what is P */

A[i] = x;

A[j] = 2;

ASSERT( A[k] >= x )

Assume that x is an integer variable, A is an array of integers, and all the subscripts are within the range of subscripts for A.

Write first the assertion P using the notation from the array-component assignment axiom, and then rewrite P in a logically equivalent and simplified form that does not contain any notation (A| I ? E).