Как вставить содержимое массива в другой массив?

Я пытаюсь создать метод в Dafny, который позволяет мне вводить содержимое одного массива в другой. Например, если Array1= [1,2,3], Array2 = [6,7,8,9,0] и index = 1, выходной массив будет [1,6,7,8,9,0 ,2,3], так как метод вставляет содержимое Array2 в Array1 с заданным индексом вставки.

Код указан ниже:

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];
}