找到这个简单算法的循环不变量

Question

我确信这是一个非常简单的问题，但我似乎无法破解它。 证明你的算法的正确性；即陈述其循环不变量并通过归纳证明。

下面是我的算法。我知道如何做第二部分（通过归纳证明），但我就是无法找出我一生中的循环不变量。

procedure intersection(A,B: list of integers)

  C= empty list
  for i:=1 to n:
    for j:= 1 to m:
      if Ai = Bj
        if Ai not in C
          C.append(Ai)
  return C

Answer 1

为了让您开始，我只是说明循环不变量之一，这样我就不会完全放弃解决方案。外循环的不变量是：

C = intersection (B, {a1, ..., ai})

您还需要内部循环的不变量。