module sort open util/ints one sig ONE, ZERO, NEGONE in Int {} sig ListInt extends Int {} fact { ONE = Int 1 && ZERO = Int 0 && NEGONE = negate(Int 1) } pred isList(list: ListInt -> ListInt) { list: ListInt lone -> lone ListInt no i: ListInt | i in i.^list some start: ListInt | ListInt in start.*list } run isList for 4 ListInt, 7 Int fun first(list: ListInt -> ListInt) : ListInt { ListInt - ListInt.^list } pred sorted(list: ListInt -> ListInt) { all i: ListInt.^list | lte(list.i, i) } run sorted for 4 ListInt, 7 Int fun cost(list: ListInt -> ListInt) : Int { Int (sum i: ListInt.^list | int sgn(sub(list.i, i))) } pred costMin(list: ListInt -> ListInt) { no list': ListInt -> ListInt | isList(list') && lt(cost(list'), cost(list)) } assert costMinImpliesSorted { all list: ListInt -> ListInt | (isList(list) && costMin(list)) => sorted(list) } check costMinImpliesSorted for 4 ListInt, 7 Int assert sortedImpliesCostMin { all list: Int -> Int | (some cost(list) && isList(list) && sorted(list)) => costMin(list) } check sortedImpliesCostMin for 4 ListInt, 7 Int