KERML11 — SequenceFunctions::includingAt overwrites the element at index instead of inserting

The definition of SequenceFunctions::includingAt in the Kernel Function Library model drops the element at position index, so the function replaces that element instead of inserting the new values before it.

Library model (SysML-v2-Release 2026-08, Kernel Libraries/Kernel Function Library/SequenceFunctions.kerml, line 57; 9.4.14.2 gives only the signature):

function includingAt{ in seq: Anything[0..*] ordered nonunique; in values: Anything[0..*] ordered nonunique;
    in index: Positive[1];
    return : Anything[0..*] ordered nonunique =
        (seq->subsequence(1, index - 1), values, seq->subsequence(index + 1));
}

The result is seq up to index - 1, then values, then seq from index + 1, so element index of seq is lost. Neither the library nor 9.4.14.2 documents the intended semantics, but insertion is the evident intent:

• The name parallels including, which only adds (union(seq, values)).
• excludingAt(seq, i, i) removes exactly one element; with insertion, it undoes includingAt for a single value.
• SequenceFunctions::addAt (p. 389), and through it OccurrenceFunctions::addNewAt ("Add a newly created occurrence to the given ordered group of occurrences at the given index"), are defined by includingAt. As written, addNewAt deletes an existing member of the group.

Example:

package Repro {
    private import SequenceFunctions::*;
    attribute r = includingAt((1, 2, 4), 3, 3);   // expected (1, 2, 3, 4); as defined: (1, 2, 3)
    attribute s = includingAt((1, 2), 9, 1);      // expected (9, 1, 2);    as defined: (9, 2)
}

Proposed resolution: change the second subsequence to start at index:

return : Anything[0..*] ordered nonunique =
    (seq->subsequence(1, index - 1), values, seq->subsequence(index));

subsequence(seq, index) runs to size(seq) by default and is empty for index = size(seq) + 1, so appending at the end still works.