无法解决有关实现 O(n) 算法的 Dafny 问题

Question

predicate Asc(a: array<int>)
  reads a
{
  forall i,j:: 0<=i<j<a.Length ==> a[i] <= a[j]
}

method occursInBoth(a: array<int>, b: array<int>) returns (r : bool)
  requires Asc(a) && Asc(b)
  ensures r == (exists i,j:: 0 <=i<a.Length && 0<=j<b.Length && a[i]==b[j])
{
  ... // implement yourself
}

谓词 Asc 将任何数组按升序排序。这意味着该方法应该查找 2 个单独的列表（按升序）是否具有相同的元素。如果它们具有相同的元素，我们应该返回 True，否则返回 False。

问题： 实现方法genesisInBoth，以便调用genesisInBoth(a,b) 执行 最多a.Length + b.Length计算步骤.