#lang ivy1.6

include order

module sequence_numbers = {

    type t
    instance props : totally_ordered_with_zero(t)
    instance iter : order_iterator(this)

    action next(seq:t) returns (res:t)

    object spec = {

	after next {
	    assume exists X. seq < X;
	    assert seq < res & (X < res -> X <= seq)
	}
    }

    object impl = {
	interpret t->bv[16]
	implement next {
	    res := seq + 1
	}
    }

    isolate iso_props = iter,props,spec,impl
}