Dafny数组插入方法编写遇阻：循环不变量验证失败求助

我正尝试在Dafny中编写一个方法，用于将一个数组的内容插入到另一个数组的指定索引位置。例如：给定Array1=[1,2,3]、Array2=[6,7,8,9,0]，插入索引为1时，输出数组应为[1,6,7,8,9,0,2,3]。

我编写了如下代码：

method insertArrayIntoIndex(a: array<int>, index: int, add_these: array<int>) returns (result: array<int>)
    requires 0 <= index < a.Length;
    ensures result.Length == a.Length + add_these.Length;
    ensures forall i :: 0 <= i < index ==> a[i] == result[i];
    ensures forall i :: 0 <= i < add_these.Length ==> add_these[i] == result[i + index];
    ensures forall i :: index <= i < a.Length ==> a[i] == result[i + add_these.Length];
{
    result := new int[a.Length + add_these.Length];

    // copy first part in
    var pos := 0;
    while (pos < index)
        invariant 0 <= pos <= index
        invariant 1 <= pos < index ==> result[pos-1] == a[pos-1]
    {
        result[pos] := a[pos];
        pos := pos + 1;
    }

    // copy in the addition
    pos := 0;
    while (pos < add_these.Length)
        invariant 0 <= pos <= add_these.Length
        invariant 1 <= pos < add_these.Length ==> result[index + pos-1] == add_these[pos-1]
    {
        result[index + pos] := add_these[pos];
        pos := pos + 1;
    }

    // copy the last part in
    pos := index;
    while (pos < a.Length)
        invariant index <= pos <= a.Length
        invariant index < pos < a.Length ==> result[pos-1 + add_these.Length] == a[pos-1]
    {
        result[pos + add_these.Length] := a[pos];
        pos := pos + 1;
    }
}

但我在编写合适的循环不变量以让代码通过验证时遇到了问题。我尝试在每个代码段末尾添加断言来验证功能（代码如下），但不确定为何这些断言验证失败。我在第一个循环内添加的断言均通过，这让我对外部断言失败的原因感到困惑，恳请提供帮助。

method insertArrayIntoIndex(a: array<int>, index: int, add_these: array<int>) returns (result: array<int>)
    requires 0 <= index < a.Length;
    ensures result.Length == a.Length + add_these.Length;
    ensures forall i :: 0 <= i < index ==> a[i] == result[i];
    ensures forall i :: 0 <= i < add_these.Length ==> add_these[i] == result[i + index];
    ensures forall i :: index <= i < a.Length ==> a[i] == result[i + add_these.Length];
{
    result := new int[a.Length + add_these.Length];

    // copy first part in
    var pos := 0;
    while (pos < index)
        invariant 0 <= pos <= index
        invariant 1 <= pos < index ==> result[pos-1] == a[pos-1]
    {
        result[pos] := a[pos];
                assert result[pos] == a[pos];
                assert pos >1 ==> result[pos-1] == a[pos-1];
                assert forall i :: 0 <= i < pos ==> result[i] == a[i];
        pos := pos + 1;
    }
        assert forall i :: 0 <= i < index ==> a[i] == result[i];

    // copy in the addition
    pos := 0;
    while (pos < add_these.Length)
        invariant 0 <= pos <= add_these.Length
        invariant 1 <= pos < add_these.Length ==> result[index + pos-1] == add_these[pos-1]
    {
        result[index + pos] := add_these[pos];
        pos := pos + 1;
    }
         assert forall i :: 0 <= i < add_these.Length ==> result[index + i] == add_these[i];

    // copy the last part in
    pos := index;
    while (pos < a.Length)
        invariant index <= pos <= a.Length
        invariant index < pos < a.Length ==> result[pos-1 + add_these.Length] == a[pos-1]
    {
        result[pos + add_these.Length] := a[pos];
        pos := pos + 1;
    }
        assert forall i :: index <= i < a.Length ==> result[add_these.Length + i] == a[i];
}

内容的提问来源于stack exchange，提问作者Zippy232223