Каков возможный инвариант цикла

Question

Может кто-то обеспечить возможный инвариант цикла для следующего простого алгоритма:

ввода: A[0,...,n-1] и B[0,...,m-1], каждый из них может содержать повторяющиеся элементы

Выход: первая пара (I, j) такой, что A[i] == B[j].

Алгоритм:

for i <- 0 to n-1 
    for j <- 0 to m-1 
     if A[i] = B[j] then 
      return (i,j) 
     endif 
    endfor 
endfor 
return null 

До сих пор, у меня есть только одно решение, которое может или не может работать:

S = {(i,j) | A[0,...,i-1] and B[0,...,j-1] has no common elements}

Answer 1

В начале qth итерации второго контура внутри pth итерация первого контура, A[i] != B[j] для всех i = 0...p - 1, j = 0...q - 1.