class Queue {
    var items: seq<int>
    var items_set: set<int>

    ghost predicate RepOk()
        reads this
    {
        && (forall i, j | 0 <= i < j < |items| :: items[i] != items[j])
        && (forall x :: x in items[..] <==> x in items_set)
    }

    constructor() 
        ensures RepOk()
        ensures items == []
    {
        items := [];
        items_set := {};
    }
    
    method Contains(x: int) returns (b: bool)
        requires RepOk()
        ensures b <==> x in items
    {
        return x in items_set;
    }

    method Enqueue(x: int)
        requires RepOk()
        requires x !in items
        modifies this
        ensures RepOk()
        ensures items == old(items) + [x]
    {
        items := items + [x];
        items_set := items_set + {x};
    }






    method Dequeue() returns (x: int)
        requires RepOk()
        requires |items| > 0
        modifies this
        ensures RepOk()
        ensures items == old(items)[1..]
        ensures x == old(items)[0]
    {
        x := items[0];
        items := items[1..];
        items_set := items_set - {x};
    }
}

method QueueMain() {
    var q := new Queue();
    q.Enqueue(3);
    q.Enqueue(4);
    var z := q.Dequeue();
    assert z == 3;
    q.Enqueue(3);
}