ii. For il=L. all incidences of x in functions other than f which have
 11
an index depending on ii, have index values less than the lowest valued

index output (by condition 1), and thus are decisions. Since 1i is

nested outside function type (by condition 2), the first pass for il

can be completed without tearing x for functions other than f. Now

assume that k passes through the i1 loop have been completed without

tearing any x's for functions other than f. The index outputs for il

in x, for iteration k, were greater than any of the other index offsets

for ii in x. Thus these index outputs of x are greater than or equal to

any of the index values for x in functions other than f for iteration

k+l. The functions other than f, then, do not require any tear of x

for iteration k+l. The if part is proved.

 Only if part The proof will be by contradiction. Assume 1)

does not hold. The index output offset for x in f is less than or

equal to some other index value for il in an incidence of x in a

function, other than f, which must be solved before

f. The variable x in this function must be torn for iteration k since

there are index values of x present which will be outputs for iteration

k. This contradicts the definition of decoupling, so condition 1)

is required for decoupling. Assume 2) does not hold. Then a function

not f, which contains the variable x must be solved for all values of

ii before any function f is solved. This would require tearing x which

would contradict the definition of decoupling, thus condition 2) is

required. The theorem is proved.

 This theorem provides the basis for algorithms which discover

 conditions which allow decoupling.