#ifndef EXISTENCE_H
#define EXISTENCE_H

#include "types.h"

/*@
	axiomatic SomeNone {
		predicate SomeEqual{A}(value_type* a, integer m, integer n, value_type v) =
			\exists integer i; m <= i < n && a[i] == v;

		predicate SomeEqual{A}(value_type* a, integer n, value_type v) =
			SomeEqual(a, 0, n, v);

		predicate NoneEqual(value_type* a, integer m, integer n, value_type v) =
			\forall integer i; m <= i < n ==> a[i] != v;

		predicate NoneEqual(value_type* a, integer n, value_type v) =
			NoneEqual(a, 0, n, v);

		lemma
		NotSomeEqual_NoneEqual:
			\forall value_type *a, v, integer m, n;
			!SomeEqual(a, m, n, v) ==> NoneEqual(a, m, n, v);

		lemma
		NoneEqual_NotSomeEqual:
			\forall value_type *a, v, integer m, n;
			NoneEqual(a, m, n, v) ==> !SomeEqual(a, m, n, v);
	}
*/

#endif