open util/ordering[Index]
open util/ordering[Value]

sig Index {}
sig Value {}
sig Array { data: Index -> Value }

pred inv[a:Array] {
	all i:Index | i not in a.data.Value =>
		( i->(a.data.Value) in ^next or (a.data.Value)->i in ^next )

	~(a.data).(a.data) in iden
}

pred sorted[a:Array] { all i,i':a.data.Value | i->i' in ^next => a.data[i]->a.data[i'] in *next}

// split <a> into two non-empty arrays <h>, <t>
pred split[a,h,t:Array] {
	some h.data and some t.data
	h.data in a.data and  t.data in a.data
	(h+t).data = a.data
	no Index.(h.data) & Index.(t.data)
	h.data.Value -> t.data.Value in ^next
}

pred merge[h,t,a] {
/*	some h',t',a':Array |

		merge[h',t',a']*/
}

pred mergesort[a, a': Array] {
	a.data.Value = a'.data.Value
	Index.(a.data) = Index.(a'.data)
    some h,t:Array | split[a,h,t]
	sorted[a']
}

assert mergesort_safe { all a,a':Array | (inv[a] && mergesort[a,a']) => (inv[a'] && sorted[a']) }
assert split_safe { all h,t,a:Array | inv[a] && split[a,h,t] => inv[h] && inv[t] }

pred mergesort_consistent[a,a':Array] { inv[a] && mergesort[a,a'] }
pred split_consistent[h,t,a:Array] { inv[a] && split[a,h,t] }

run split_consistent for 5
check split_safe for 5

run mergesort_consistent for 5 but exactly 2 Array, exactly 3 Index, exactly 2 Value
check mergesort_safe for 5