映射集合归纳方法咨询及归并排序逆序计数算法验证超时问题

我正在验证一个归并排序逆序计数算法的实现，感觉pairMapSize引理已经满足所有必要条件，但验证过程还是超时了。我尝试过对数组切片做归纳，不过需要定义函数生成另一个集合——比如所有以(xs[0], YY)开头的逆序对集合，但本质上还是集合大小比较的场景。

相关代码（Dafny） #

predicate IsInverted(xs: seq<int>, i: int, j: int) {
    0 <= i < j < |xs| && xs[i] > xs[j]
}

function inversionSet(xs: seq<int>): set<(int,int)> {
    set i,j | 0 <= i < j < |xs| && IsInverted(xs, i, j) :: (i,j)
}

function pairSetMap(ss: set<(int, int)>, i: int): set<(int, int)> 
{
    set pair | pair in ss :: (pair.0 + i, pair.1 + i)
}

lemma {:verify } {:timelimit 30} {:vcs_split_on_every_assert} pairMapSize(xs: seq<int>, i: int)
    requires 0 <= i
    ensures |pairSetMap(inversionSet(xs), i)| == |inversionSet(xs)|
{
    if inversionSet(xs) == {} {
        assert |inversionSet(xs)| == 0;
        assert pairSetMap(inversionSet(xs), i) == {};
        assert |pairSetMap(inversionSet(xs), i)| == 0;
    }else{
        // forall x | x in inversionSet(xs)
        //     ensures (x.0+i, x.1+i) in pairSetMap(inversionSet(xs), i)
        // {

        // }

        // forall x | x in pairSetMap(inversionSet(xs), i)
        //     ensures (x.0-i, x.1-i) in inversionSet(xs)
        // {

        // }
        var ixs := inversionSet(xs);
        var pxs := pairSetMap(inversionSet(xs), i);
        var x :| x in inversionSet(xs);
        assert (x.0+i, x.1+i) in pxs;
        assert |ixs| == 1 + |ixs-{x}|;
        assert |pxs| == 1 + |pxs-{(x.0+i, x.1+i)}|;
        var removed: set<(int, int)> := {};
        var premoved: set<(int, int)> := {};
        var mixs := 0;
        var mpxs := 0;
        while ixs != {} 
            invariant ixs == inversionSet(xs)-removed
            invariant ixs <= inversionSet(xs)
            invariant ixs !! removed
            invariant pxs == pairSetMap(inversionSet(xs), i)-premoved
            invariant pxs <= pairSetMap(inversionSet(xs), i)-premoved
            invariant pxs !! premoved
            invariant forall x :: x in removed ==> (x.0+i, x.1+i) in premoved
            invariant forall x :: x in premoved ==> (x.0-i, x.1-i) in removed
            invariant mixs == |removed|
            invariant mpxs == |premoved|
            invariant mixs == mpxs
        {
            var x :| x in ixs;
            assert x !in removed;
            var mx := (x.0+i, x.1+i);
            assert mx !in premoved by {
                if mx in premoved {
                    assert x in removed;
                    assert false;
                }
            }
            assert mx in pxs;
            ixs := ixs - {x};
            pxs := pxs - {mx};
            mixs := mixs + 1;
            mpxs := mpxs + 1;
            removed := removed + {x};
            premoved := premoved + {mx};
        }
        assert ixs == {};
        assert pxs == {};
        assert removed == inversionSet(xs);
        assert premoved == pairSetMap(inversionSet(xs), i);
        calc {
            |inversionSet(xs)|;
            |removed|;
            mixs;
            mpxs;
            |premoved|;
            |pairSetMap(inversionSet(xs), i)|;
        }

    }
}

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