验证序列内容是否连续

问：

我遇到了这种情况，我怀疑触发器是一个问题，但我不太明白为什么触发器是一个问题。

以下内容无法验证。

predicate isSlice(ss: string, s: string, i: int, k: int)
    requires 0 <= i <=k <= |s|
{
    ss == s[i..k]
}

predicate inString(ss: string, s: string, sindex: int, index: int)
    requires index <= |s|
{
    exists i,k :: 0 <= i <=k <= sindex <= index  && isSlice(ss, s, i,k)
}

predicate slicesAreSequential(rs: seq<string>, s: string, index: int) 
    requires index <= |s|
{
    forall i :: 0 <= i < |rs| -1 ==> exists m,n,j,k :: 0 <= m < n <= j < k <= index && isSlice(rs[i], s,m,n) && isSlice(rs[i+1], s, j , k)
}

lemma splitTest(s: string, results: seq<string>)
    requires |results| == |s|
    requires forall i :: 0 <= i < |s| ==> s[i..i+1] in results
    requires forall i :: 0 <= i < |s| ==> s[i..i+1] == results[i]
    requires forall ss: string :: ss in results ==> inString(ss,s, |s|, |s|)
    ensures slicesAreSequential(results, s, |s|)
{
    if |s| > 0 {
        forall i | 0 <= i < |results| -1 
            ensures exists m,n,j,k :: 0 <= m < n <= j < k <= |s| && isSlice(results[i], s,m,n) && isSlice(results[i+1], s, j , k)
        {
            var cur := results[i];
            var next := results[i+1];
            assert isSlice(results[i],s, i,i+1);
            assert isSlice(results[i+1],s, i+1,i+2);
        }
        assert slicesAreSequential(results, s, |s|);
    }else{

    }
}

但是，以下版本会进行验证。

predicate slicesAreSequential(rs: seq<string>, s: string, index: int) 
    requires index <= |s|
{
    forall i :: 0 <= i < |rs| -1 ==> bork(rs[i], rs[i+1], s, index)
}

predicate bork(left: string, right: string, s: string, index: int) 
    requires index <= |s|
{
    exists m,n,j,k :: 0 <= m < n <= j < k <= index && isSlice(left, s,m,n) && isSlice(right, s, j , k)
}

lemma splitTest(s: string, results: seq<string>)
    requires |results| == |s|
    requires forall i :: 0 <= i < |s| ==> s[i..i+1] in results
    requires forall i :: 0 <= i < |s| ==> s[i..i+1] == results[i]
    requires forall ss: string :: ss in results ==> inString(ss,s, |s|, |s|)
    ensures slicesAreSequential(results, s, |s|)
{
    if |s| > 0 {
        forall i | 0 <= i < |results| -1 
            ensures exists m,n,j,k :: 0 <= m < n <= j < k <= |s| && isSlice(results[i], s,m,n) && isSlice(results[i+1], s, j , k)
        {
            var cur := results[i];
            var next := results[i+1];
            assert isSlice(results[i],s, i,i+1);
            assert isSlice(results[i+1],s, i+1,i+2);
        }
        assert slicesAreSequential(results, s, |s|);
    }else{

    }
}

是因为 exists 语句不会产生触发器，即使它在那里放置了一些断言？