Working on verifying a version of the counting inversions algorithm. I feel like pairMapSize has everything it needs but it times out instead. I could try to do induction on slices of the array but I would need to define a function to produce another set, like the set of all inversions starting at (xs[0], YY) but then it would be just another case of comparing sets sizes.

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

        }