predicate exist1(a: array<int>, x:int) 
    reads a;
{
    multiset(a[..])[x] == 1
}

predicate exist2(a: array<int>, x:int) 
    reads a;
{
    multiset(a[..])[x] >= 2
}

predicate tail(a: array<int>) 
    reads a;
{
    forall i : int :: 0 <= i < a.Length ==> 
        (a[i] != 0 || multiset(a[i..])[0] == a.Length - i)
}

method test1() 
{
    var a := new int[3][1, 2, 2];
    assert a[..] == [1, 2, 2];

    assert !exist1(a, 0);
    assert exist1(a, 1);
    assert !exist1(a, 2);
}

method test2() 
{
    var a := new int[6][1, 2, 2, 3, 3, 3];
    assert a[..] == [1, 2, 2, 3, 3, 3];

    assert !exist2(a, 0);
    assert !exist2(a, 1);
    assert exist2(a, 2);
    assert exist2(a, 3);
}

method test3()
{
    var a := new int[4][1, 2, 3, 0];
    assert a[..] == [1, 2, 3, 0];
    assert tail(a);

    // "no zeros is vacuously true"
    var b := new int[4][1, 2, 3, 4];
    assert b[..] == [1, 2, 3, 4];
    assert tail(b);

    var c := new int[6][1, 2, 3, 0, 5, 6];
    assert c[..] == [1, 2, 3, 0, 5, 6];
    assert c[3..] == [0, 5, 6];
    assert !tail(c);

    var d := new int[6][1, 2, 0, 0, 5, 0];
    assert d[..] == [1, 2, 0, 0, 5, 0];
    assert d[2..] == [0, 0, 5, 0];
    assert !tail(d);
}