# Verifying Merge Sort in Imandra¶

Merge sort is a widely used efficient general purpose sorting algorithm invented by John von Neumann in 1945. It is a prototypical divide and conquer algorithm and forms the basis of standard library sorting functions in languages like OCaml, Java and Python.

Let's verify it in Imandra! ## The main idea¶

The main idea of merge sort is as follows:

• Divide the input list into sublists
• Sort the sublists
• Merge the sorted sublists to obtain a sorted version of the original list

## Merging two lists¶

We'll start by defining a function to merge two lists in a "sorted" way. Note that our termination proof involves both arguments l and m, using a lexicographic product (via the [@@adm l,m] admission annotation).

In :
let rec merge (l : int list) (m : int list) =
match l, m with
| [], _ -> m
| _, [] -> l
| a :: ls, b :: ms ->
if a < b then
a :: (merge ls m)
else
b :: (merge l ms)

Out:
val merge : int list -> int list -> int list = <fun>

termination proof

### Termination proof

call merge (List.tl l) m from merge l m
originalmerge l m
submerge (List.tl l) m
original ordinalOrdinal.of_list [Ordinal.Int (Ordinal.count l); Ordinal.Int (Ordinal.count m)]
sub ordinalOrdinal.of_list [Ordinal.Int (Ordinal.count (List.tl l)); Ordinal.Int (Ordinal.count m)]
path[List.hd l < List.hd m && not (m = []) && not (l = [])]
proof
detailed proof
ground_instances8
definitions0
inductions0
search_time
0.036s
details
Expand
smt_stats
 arith offset eqs 36 num checks 18 arith assert lower 156 arith pivots 85 rlimit count 59824 mk clause 304 datatype occurs check 348 mk bool var 700 arith assert upper 147 datatype splits 59 decisions 420 arith add rows 324 arith bound prop 12 propagations 589 interface eqs 13 conflicts 50 arith fixed eqs 104 datatype accessor ax 70 minimized lits 3 arith conflicts 7 arith assert diseq 21 datatype constructor ax 87 num allocs 5.91834e+06 final checks 41 added eqs 923 del clause 196 arith eq adapter 120 memory 6.58 max memory 6.59
Expand
• start[0.036s]
List.hd l < List.hd m
&& not (m = [])
&& not (l = [])
&& Ordinal.count l >= 0
&& Ordinal.count m >= 0
&& Ordinal.count (List.tl l) >= 0 && Ordinal.count m >= 0
==> not
(List.hd (List.tl l) < List.hd m
&& not (m = []) && not (List.tl l = []))
&& not
(not (List.hd (List.tl l) < List.hd m)
&& not (m = []) && not (List.tl l = []))
|| Ordinal.( << )
(if [Ordinal.Int (Ordinal.count (List.tl l));
Ordinal.Int (Ordinal.count m)]
= []
then … else …)
…
• ##### simplify
 into (not (((((not (List.hd m <= List.hd l) && not (m = [])) && not (l = [])) && Ordinal.count l >= 0) && Ordinal.count m >= 0) && Ordinal.count (List.tl l) >= 0) || not ((not (List.hd m <= List.hd (List.tl l)) && not (m = [])) && not (List.tl l = [])) && not ((List.hd m <= List.hd (List.tl l) && not (m = [])) && not (List.tl l = []))) || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int (Ordinal.count (List.tl l))) (Ordinal.Int 1)) (Ordinal.Int (Ordinal.count m))) (Ordinal.plus (Ordinal.shift (Ordinal.Int (Ordinal.count l)) (Ordinal.Int 1)) (Ordinal.Int (Ordinal.count m))) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.shift_127| (|Ordinal.Int_93| (|count_int list_1206| l_1193)) (|Ordinal.Int_93| 1)) expansions
• unroll
 expr (|Ordinal.plus_113| (|Ordinal.shift_127| (|Ordinal.Int_93| (|count_int list_1206| l_1193)) … expansions
• unroll
 expr (|Ordinal.shift_127| (|Ordinal.Int_93| (|count_int list_1206| (|get.::.1_1192| l_1193))) (|Ord… expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (|count_int list_1206| … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (|count_int list_1206| … expansions
• unroll
 expr (|count_int list_1206| (|get.::.1_1192| l_1193)) expansions
• unroll
 expr (|count_int list_1206| m_1194) expansions
• unroll
 expr (|count_int list_1206| l_1193) expansions
• ##### unsat
(let ((a!1 (|get.Ordinal.Cons.1_1198|
(|Ordinal.shift_127|
(|Ordinal.Int…

call merge l (List.tl m) from merge l m
originalmerge l m
submerge l (List.tl m)
original ordinalOrdinal.of_list [Ordinal.Int (Ordinal.count l); Ordinal.Int (Ordinal.count m)]
sub ordinalOrdinal.of_list [Ordinal.Int (Ordinal.count l); Ordinal.Int (Ordinal.count (List.tl m))]
path[not (List.hd l < List.hd m) && not (m = []) && not (l = [])]
proof
detailed proof
ground_instances13
definitions0
inductions0
search_time
0.085s
details
Expand
smt_stats
 arith offset eqs 19 num checks 28 arith assert lower 398 arith pivots 174 rlimit count 39156 mk clause 583 datatype occurs check 681 mk bool var 1570 arith assert upper 391 datatype splits 137 decisions 987 arith add rows 543 arith bound prop 21 propagations 1504 interface eqs 11 conflicts 73 arith fixed eqs 223 datatype accessor ax 196 minimized lits 5 arith conflicts 11 arith assert diseq 58 datatype constructor ax 240 num allocs 1.24705e+06 final checks 57 added eqs 1998 del clause 341 arith eq adapter 302 memory 6.59 max memory 6.59
Expand
• start[0.085s]
not (List.hd l < List.hd m)
&& not (m = [])
&& not (l = [])
&& Ordinal.count l >= 0
&& Ordinal.count m >= 0
&& Ordinal.count l >= 0 && Ordinal.count (List.tl m) >= 0
==> not
(List.hd l < List.hd (List.tl m)
&& not (List.tl m = []) && not (l = []))
&& not
(not (List.hd l < List.hd (List.tl m))
&& not (List.tl m = []) && not (l = []))
|| Ordinal.( << )
(if [Ordinal.Int (Ordinal.count l);
Ordinal.Int (Ordinal.count (List.tl m))]
= []
then … else …)
…
• ##### simplify
 into (not (((((List.hd m <= List.hd l && not (m = [])) && not (l = [])) && Ordinal.count l >= 0) && Ordinal.count m >= 0) && Ordinal.count (List.tl m) >= 0) || not ((not (List.hd (List.tl m) <= List.hd l) && not (List.tl m = [])) && not (l = [])) && not ((List.hd (List.tl m) <= List.hd l && not (List.tl m = [])) && not (l = []))) || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int (Ordinal.count l)) (Ordinal.Int 1)) (Ordinal.Int (Ordinal.count (List.tl m)))) (Ordinal.plus (Ordinal.shift (Ordinal.Int (Ordinal.count l)) (Ordinal.Int 1)) (Ordinal.Int (Ordinal.count m))) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.plus_113| (|Ordinal.shift_127| (|Ordinal.Int_93| (|count_int list_1206| l_1193)) … expansions
• unroll
 expr (|Ordinal.shift_127| (|Ordinal.Int_93| (|count_int list_1206| l_1193)) (|Ordinal.Int_93| 1)) expansions
• unroll
 expr (|Ordinal.plus_113| (|Ordinal.shift_127| (|Ordinal.Int_93| (|count_int list_1206| l_1193)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.plus_113| (|Ordinal.shift_127| (|Ordinal.Int_93| (|… expansions
• unroll
 expr (|count_int list_1206| (|get.::.1_1192| m_1194)) expansions
• unroll
 expr (|count_int list_1206| m_1194) expansions
• unroll
 expr (|count_int list_1206| l_1193) expansions
• unroll
 expr (|count_int list_1206| (|get.::.1_1192| l_1193)) expansions
• unroll
 expr (|count_int list_1206| (|get.::.1_1192| (|get.::.1_1192| m_1194))) expansions
• unroll
 expr (let ((a!1 (|get.Ordinal.Cons.2_1199| (|Ordinal.shift_127| (|Ordinal.Int… expansions
• unroll
 expr (let ((a!1 (|get.Ordinal.Cons.2_1199| (|Ordinal.shift_127| (|Ordinal.Int… expansions
• unroll
 expr (let ((a!1 (|Ordinal.plus_113| (|Ordinal.shift_127| (|Ordinal.Int_93| (|… expansions
• unroll
 expr (let ((a!1 (|Ordinal.plus_113| (|Ordinal.shift_127| (|Ordinal.Int_93| (|… expansions
• ##### unsat
(let ((a!1 (|Ordinal.plus_113|
(|Ordinal.shift_127|
(|Ordinal.Int_93| (|…

Let's experiment a bit with merge.

In :
merge [1;2;3] [4;5;6]

Out:
- : int list = [1; 2; 3; 4; 5; 6]

In :
merge [1;4;5] [2;3;4]

Out:
- : int list = [1; 2; 3; 4; 4; 5]

In :
merge [1;5;2] [2;3]

Out:
- : int list = [1; 2; 3; 5; 2]


Observe that merge will merge sorted lists in a manner that respects their sortedness. But, if the lists given to merge aren't sorted, the output of merge need not be sorted.

# Dividing into sublists¶

In merge sort, we need to divide a list into sublists. We'll do this in a simple way using the function odds which computes "every other" element of a list. We'll then be able to split a list x into sublists by taking odds x and odds (List.tl x).

In :
let rec odds l =
match l with
| []  -> []
| [x] -> [x]
| x :: y :: rst -> x :: odds rst

Out:
val odds : 'a list -> 'a list = <fun>

termination proof

### Termination proof

call odds (List.tl (List.tl l)) from odds l
originalodds l
subodds (List.tl (List.tl l))
original ordinalOrdinal.Int (Ordinal.count l)
sub ordinalOrdinal.Int (Ordinal.count (List.tl (List.tl l)))
path[not (l <> [] && List.tl l = []) && not (l = [])]
proof
detailed proof
ground_instances6
definitions0
inductions0
search_time
0.028s
details
Expand
smt_stats
 arith offset eqs 4 num checks 14 arith assert lower 27 arith pivots 16 rlimit count 5304 mk clause 73 datatype occurs check 45 mk bool var 174 arith assert upper 26 datatype splits 11 decisions 51 arith add rows 37 arith bound prop 5 propagations 47 interface eqs 1 conflicts 18 arith fixed eqs 23 datatype accessor ax 11 minimized lits 1 arith conflicts 3 arith assert diseq 3 datatype constructor ax 21 num allocs 2.31784e+07 final checks 12 added eqs 113 del clause 21 arith eq adapter 20 memory 8.24 max memory 8.24
Expand
• start[0.028s]
not (l <> [] && List.tl l = [])
&& not (l = [])
&& Ordinal.count l >= 0 && Ordinal.count (List.tl (List.tl l)) >= 0
==> not
(not
((List.tl (List.tl l)) <> [] && List.tl (List.tl (List.tl l)) = [])
&& not (List.tl (List.tl l) = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl (List.tl l))))
(Ordinal.Int (Ordinal.count l))
• ##### simplify
 into (not (((not (l <> [] && List.tl l = []) && not (l = [])) && Ordinal.count l >= 0) && Ordinal.count (List.tl (List.tl l)) >= 0) || not (not ((List.tl (List.tl l)) <> [] && List.tl (List.tl (List.tl l)) = []) && not (List.tl (List.tl l) = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl (List.tl l)))) (Ordinal.Int (Ordinal.count l)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (let ((a!1 (|Ordinal.Int_93| (|count_ty_0 list_1244| (|get.::.1_122… expansions
• unroll
 expr (|count_ty_0 list_1244| (|get.::.1_1228| (|get.::.1_1228| l_1235))) expansions
• unroll
 expr (|count_ty_0 list_1244| l_1235) expansions
• unroll
 expr (|count_ty_0 list_1244| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| l_1235)))) expansions
• unroll
 expr (let ((a!1 (|Ordinal.Int_93| (|count_ty_0 list_1244| (|get.::.1_122… expansions
• unroll
 expr (|count_ty_0 list_1244| (|get.::.1_1228| l_1235)) expansions
• ##### unsat
(let ((a!1 (ite (>= (|count_ty_0 list_1244| (|get.::.1_1228| l_1235)) 0)
(|count_…

Let's compute a bit with odds to better understand how it works.

In :
odds [1;2;3;4;5;6]

Out:
- : Z.t list = [1; 3; 5]

In :
odds (List.tl [1;2;3;4;5;6])

Out:
- : Z.t list = [2; 4; 6]


# Defining Merge Sort¶

We can now put the pieces together and define our main merge_sort function, as follows:

In :
let rec merge_sort l =
match l with
| []  -> []
| [_] -> l
| _ :: ls -> merge (merge_sort (odds l)) (merge_sort (odds ls))

Out:
val merge_sort : int list -> int list = <fun>
File "jupyter cell 8", line 1, characters 0-129:
Error: rejected definition for function merge_sort,
Imandra could not prove termination.
hint: problematic sub-call from merge_sort l
to merge_sort (odds (List.tl l))  under path
not (l <> [] && List.tl l = []) and not (l = [])
could not be proved to decrease (measured subset: (l))
See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/


To admit merge_sort into Imandra, we must prove it terminating. We can do this with a custom measure function which we'll call merge_sort_measure. We'll prove a lemma about odds (by functional induction) to make it clear why the measure is decreasing in every recursive call. We'll install the lemma as a forward_chaining rule, which is a good strategy for making it effective during termination analysis.

In :
let merge_sort_measure x =
Ordinal.of_int (List.length x)

Out:
val merge_sort_measure : 'a list -> Ordinal.t = <fun>

In :
theorem odds_len_1 x =
x <> [] && List.tl x <> []
==>
(List.length (odds x) [@trigger]) < List.length x
[@@induct functional odds] [@@forward_chaining]

Out:
val odds_len_1 : 'a list -> bool = <fun>
Goal:

x <> [] && List.tl x <> [] ==> List.length (odds x) < List.length x.

1 nontautological subgoal.

We shall induct according to a scheme derived from odds.

Induction scheme:

(not (not (x <> [] && List.tl x = []) && not (x = [])) ==> φ x)
&& (not (x = [])
&& not (x <> [] && List.tl x = []) && φ (List.tl (List.tl x)) ==>
φ x).

2 nontautological subgoals.

Subgoal 2:

H0. not (x = [])
H1. not (List.tl x = [])
H2. List.length x <= List.length (odds x)
|---------------------------------------------------------------------------
not (x <> [] && List.tl x = []) && not (x = [])

But simplification reduces this to true, using the forward-chaining rule
List.len_nonnegative.

Subgoal 1:

H0. not (x = [])
H1. not (x <> [] && List.tl x = [])
H2. not
(not (List.tl (List.tl x) = [])
&& not (List.tl (List.tl (List.tl x)) = []))
|| not
(List.length (List.tl (List.tl x)) <=
List.length (odds (List.tl (List.tl x))))
H3. not (x = [])
H4. not (List.tl x = [])
H5. List.length x <= List.length (odds x)
|---------------------------------------------------------------------------
false

This simplifies, using the definitions of List.length and odds to the
following 3 subgoals:

Subgoal 1.3:

H0. x <> []
H1. (List.tl x) <> []
H2. List.tl (List.tl x) = []
H3. List.length (List.tl x) <= List.length (odds (List.tl (List.tl x)))
|---------------------------------------------------------------------------
false

But simplification reduces this to true, using the definitions of List.length
and odds.

Subgoal 1.2:

H0. x <> []
H1. (List.tl x) <> []
H2. (List.tl (List.tl x)) <> []
H3. (List.tl (List.tl (List.tl x))) <> []
H4. List.length (List.tl x) <= List.length (odds (List.tl (List.tl x)))
|---------------------------------------------------------------------------
List.length (List.tl (List.tl x)) <=
List.length (odds (List.tl (List.tl x)))

This simplifies, using the definition of List.length to:

Subgoal 1.2':

H0. x <> []
H1. (List.tl x) <> []
H2. (List.tl (List.tl x)) <> []
H3. (List.tl (List.tl (List.tl x))) <> []
H4. List.length (List.tl (List.tl x)) <=
(-1 + List.length (odds (List.tl (List.tl x))))
|---------------------------------------------------------------------------
List.length (List.tl (List.tl (List.tl x))) <=
(-1 + List.length (odds (List.tl (List.tl x))))

But simplification reduces this to true, using the definition of List.length.

Subgoal 1.1:

H0. x <> []
H1. (List.tl x) <> []
H2. (List.tl (List.tl x)) <> []
H3. List.tl (List.tl (List.tl x)) = []
H4. List.length (List.tl x) <= List.length (odds (List.tl (List.tl x)))
|---------------------------------------------------------------------------
false

This simplifies, using the definitions of List.length and odds to:

Subgoal 1.1':

H0. x <> []
H1. (List.tl x) <> []
H2. (List.tl (List.tl x)) <> []
H3. List.tl (List.tl (List.tl x)) = []
H4. List.length (List.tl (List.tl x)) <=
List.length (List.tl (List.tl (List.tl x)))
|---------------------------------------------------------------------------
false

But simplification reduces this to true, using the definition of List.length.

ⓘ  Rules:
(:def List.length)
(:def odds)
(:fc List.len_nonnegative)
(:induct odds)


Proved
proof
 ground_instances 0 definitions 13 inductions 1 search_time 0.387s
Expand
• start[0.387s, "Goal"]
not (:var_0: = []) && not (List.tl :var_0: = [])
==> List.length (odds :var_0:) < List.length :var_0:
• #### subproof

(x = [] || List.tl x = []) || not (List.length x <= List.length (odds x))
• start[0.386s, "1"]
(x = [] || List.tl x = []) || not (List.length x <= List.length (odds x))
• induction on (functional odds)
:scheme (not (not (x <> [] && List.tl x = []) && not (x = [])) ==> φ x)
&& (not (x = [])
&& not (x <> [] && List.tl x = []) && φ (List.tl (List.tl x))
==> φ x)
• Split (((not (x <> [] && List.tl x = []) && not (x = [])
|| not (not (x = []) && not (List.tl x = [])))
|| not (List.length x <= List.length (odds x)))
&& ((not
((not (x = []) && not (x <> [] && List.tl x = []))
&& (not
(not (List.tl (List.tl x) = [])
&& not (List.tl (List.tl (List.tl x)) = []))
|| not
(List.length (List.tl (List.tl x)) <=
List.length (odds (List.tl (List.tl x))))))
|| not (not (x = []) && not (List.tl x = [])))
|| not (List.length x <= List.length (odds x)))
:cases [((x = [] || List.tl x = [])
|| not (List.length x <= List.length (odds x)))
|| not (x <> [] && List.tl x = []) && not (x = []);
(((x = [] || x <> [] && List.tl x = [])
|| not
(not
(not (List.tl (List.tl x) = [])
&& not (List.tl (List.tl (List.tl x)) = []))
|| not
(List.length (List.tl (List.tl x)) <=
List.length (odds (List.tl (List.tl x))))))
|| List.tl x = [])
|| not (List.length x <= List.length (odds x))])
• ##### subproof
(((x = [] || x <> [] && List.tl x = []) || not (not (not (List.tl (List.tl x) = []) && not (List.tl (List.tl (List.tl x)) = [])) || not (List.length (List.tl (List.tl x)) <= List.length (odds (List.tl (List.tl x)))))) || List.tl x = []) || not (List.length x <= List.length (odds x))
• start[0.386s, "1"]
(((x = [] || x <> [] && List.tl x = [])
|| not
(not
(not (List.tl (List.tl x) = [])
&& not (List.tl (List.tl (List.tl x)) = []))
|| not
(List.length (List.tl (List.tl x)) <=
List.length (odds (List.tl (List.tl x))))))
|| List.tl x = [])
|| not (List.length x <= List.length (odds x))
• ###### simplify
 into ((((x = [] || List.tl x = []) || not (List.tl (List.tl x) = [])) || not (List.length (List.tl x) <= List.length (odds (List.tl (List.tl x))))) && (((((x = [] || List.tl x = []) || List.length (List.tl (List.tl x)) <= List.length (odds (List.tl (List.tl x)))) || List.tl (List.tl x) = []) || List.tl (List.tl (List.tl x)) = []) || not (List.length (List.tl x) <= List.length (odds (List.tl (List.tl x)))))) && ((((x = [] || List.tl x = []) || List.tl (List.tl x) = []) || not (List.tl (List.tl (List.tl x)) = [])) || not (List.length (List.tl x) <= List.length (odds (List.tl (List.tl x))))) expansions [List.length, odds, List.length] rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• Subproof
• Subproof
• Subproof
• ##### subproof
((x = [] || List.tl x = []) || not (List.length x <= List.length (odds x))) || not (x <> [] && List.tl x = []) && not (x = [])
• start[0.386s, "2"]
((x = [] || List.tl x = []) || not (List.length x <= List.length (odds x)))
|| not (x <> [] && List.tl x = []) && not (x = [])
• ###### simplify
 into true expansions [] rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegative

Now we're ready to define merge_sort. Imandra is able prove it terminating using our custom measure (and lemma!).

In :
let rec merge_sort l =
match l with
| []  -> []
| [_] -> l
| _ :: ls -> merge (merge_sort (odds l)) (merge_sort (odds ls))
[@@measure merge_sort_measure l]

Out:
val merge_sort : int list -> int list = <fun>

termination proof

### Termination proof

call merge_sort (odds l) from merge_sort l
originalmerge_sort l
submerge_sort (odds l)
original ordinalmerge_sort_measure l
sub ordinalmerge_sort_measure (odds l)
path[not (l <> [] && List.tl l = []) && not (l = [])]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.011s
details
Expand
smt_stats
 num checks 3 arith assert lower 3 arith pivots 1 rlimit count 5065 mk clause 3 datatype occurs check 28 mk bool var 51 datatype splits 9 decisions 15 propagations 3 conflicts 8 datatype accessor ax 7 datatype constructor ax 13 num allocs 3.71719e+09 final checks 6 added eqs 39 del clause 3 memory 40.96 max memory 52.67
Expand
• start[0.011s]
not (l <> [] && List.tl l = [])
&& not (l = [])
&& (if List.length l >= 0 then List.length l else 0) >= 0
&& (if List.length (odds l) >= 0 then List.length (odds l) else 0) >=
0
==> not
(not ((odds l) <> [] && List.tl (odds l) = []) && not (odds l = []))
&& not
(not ((odds l) <> [] && List.tl (odds l) = []) && not (odds l = []))
|| Ordinal.( << )
(Ordinal.Int
(if List.length (odds l) >= 0 then List.length (odds l) else 0))
(Ordinal.Int (if List.length l >= 0 then List.length l else 0))
• ##### simplify
 into (not (((not (l <> [] && List.tl l = []) && not (l = [])) && (if List.length l >= 0 then List.length l else 0) >= 0) && (if List.length (odds l) >= 0 then List.length (odds l) else 0) >= 0) || not (not ((odds l) <> [] && List.tl (odds l) = []) && not (odds l = []))) || Ordinal.( << ) (Ordinal.Int (if List.length (odds l) >= 0 then List.length (odds l) else 0)) (Ordinal.Int (if List.length l >= 0 then List.length l else 0)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (let ((a!1 (ite (>= (|List.length_1510| (odds_1514 l_1520)) 0) (|List.length_1510| (… expansions
• ##### unsat
(let ((a!1 (and (not (= l_1520 |[]_2|))
(not (= (|get.::.1_1503| l_1520) |[]_2|))))
…

call merge_sort (odds (List.tl l)) from merge_sort l
originalmerge_sort l
submerge_sort (odds (List.tl l))
original ordinalmerge_sort_measure l
sub ordinalmerge_sort_measure (odds (List.tl l))
path[not (l <> [] && List.tl l = []) && not (l = [])]
proof
detailed proof
ground_instances4
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 10 arith assert lower 6 arith pivots 6 rlimit count 3369 mk clause 16 datatype occurs check 83 mk bool var 121 arith assert upper 14 datatype splits 25 decisions 42 arith add rows 8 propagations 35 conflicts 15 datatype accessor ax 12 arith conflicts 1 datatype constructor ax 27 num allocs 3.63581e+09 final checks 18 added eqs 100 del clause 8 arith eq adapter 2 memory 38.03 max memory 52.67
Expand
• start[0.014s]
not (l <> [] && List.tl l = [])
&& not (l = [])
&& (if List.length l >= 0 then List.length l else 0) >= 0
&& (if List.length (odds (List.tl l)) >= 0
then List.length (odds (List.tl l)) else 0)
>= 0
==> not
(not ((odds (List.tl l)) <> [] && List.tl (odds (List.tl l)) = [])
&& not (odds (List.tl l) = []))
&& not
(not ((odds (List.tl l)) <> [] && List.tl (odds (List.tl l)) = [])
&& not (odds (List.tl l) = []))
|| Ordinal.( << )
(Ordinal.Int
(if List.length (odds (List.tl l)) >= 0
then List.length (odds (List.tl l)) else 0))
(Ordinal.Int (if List.length l >= 0 then List.length l else 0))
• ##### simplify
 into (not (((not (l <> [] && List.tl l = []) && not (l = [])) && (if List.length l >= 0 then List.length l else 0) >= 0) && (if List.length (odds (List.tl l)) >= 0 then List.length (odds (List.tl l)) else 0) >= 0) || not (not ((odds (List.tl l)) <> [] && List.tl (odds (List.tl l)) = []) && not (odds (List.tl l) = []))) || Ordinal.( << ) (Ordinal.Int (if List.length (odds (List.tl l)) >= 0 then List.length (odds (List.tl l)) else 0)) (Ordinal.Int (if List.length l >= 0 then List.length l else 0)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (let ((a!1 (>= (|List.length_1510| (odds_1514 (|get.::.1_1503| l_1520))) 0)) (a!3 (|Ordinal.In… expansions
• unroll
 expr (odds_1514 (|get.::.1_1503| l_1520)) expansions
• unroll
 expr (|List.length_1510| (odds_1514 (|get.::.1_1503| l_1520))) expansions
• unroll
 expr (|List.length_1510| l_1520) expansions
• ##### unsat
(let ((a!1 (not (and ((_ is (|::_3| (Int |int list_1501|) |int list_1501|))
…

Let's experiment a bit with merge_sort to gain confidence we've defined it correctly.

In :
merge_sort [1;2;3]

Out:
- : int list = [1; 2; 3]

In :
merge_sort [9;100;6;2;34;19;3;4;7;6]

Out:
- : int list = [2; 3; 4; 6; 6; 7; 9; 19; 34; 100]


This looks pretty good! Let's now use Imandra to prove it correct.

# Proving Merge Sort correct¶

What does it mean for a sorting algorithm to be correct? There are two main components:

• The result is sorted
• The result has the same elements as the original

Let's start by defining what it means for a list to be sorted.

In :
let rec is_sorted (x : int list) =
match x with
| []  -> true
| [_] -> true
| x :: x' :: xs -> x <= x' && is_sorted (x' :: xs)

Out:
val is_sorted : int list -> bool = <fun>

termination proof

### Termination proof

call is_sorted (List.tl x) from is_sorted x
originalis_sorted x
subis_sorted (List.tl x)
original ordinalOrdinal.Int (Ordinal.count x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
path[List.hd x <= List.hd (List.tl x) && not (x <> [] && List.tl x = []) && not (x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 8 arith assert lower 26 arith pivots 9 rlimit count 2914 mk clause 32 datatype occurs check 34 mk bool var 109 arith assert upper 16 datatype splits 11 decisions 23 arith add rows 17 arith bound prop 1 propagations 24 interface eqs 3 conflicts 11 arith fixed eqs 12 datatype accessor ax 6 arith conflicts 2 arith assert diseq 2 datatype constructor ax 10 num allocs 3.93758e+09 final checks 12 added eqs 67 del clause 16 arith eq adapter 16 memory 38.89 max memory 52.67
Expand
• start[0.014s]
List.hd x <= List.hd (List.tl x)
&& not (x <> [] && List.tl x = [])
&& not (x = [])
&& Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
==> not
(List.hd (List.tl x) <= List.hd (List.tl (List.tl x))
&& not ((List.tl x) <> [] && List.tl (List.tl x) = [])
&& not (List.tl x = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
(Ordinal.Int (Ordinal.count x))
• ##### simplify
 into (not ((((List.hd x <= List.hd (List.tl x) && not (x <> [] && List.tl x = [])) && not (x = [])) && Ordinal.count x >= 0) && Ordinal.count (List.tl x) >= 0) || not ((List.hd (List.tl x) <= List.hd (List.tl (List.tl x)) && not ((List.tl x) <> [] && List.tl (List.tl x) = [])) && not (List.tl x = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x))) (Ordinal.Int (Ordinal.count x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_int list_1545| (… expansions
• unroll
 expr (|count_int list_1545| (|get.::.1_1535| x_1536)) expansions
• unroll
 expr (|count_int list_1545| x_1536) expansions
• ##### unsat
(let ((a!1 (>= (ite (>= (|get.::.0_1534| x_1536) 0) (|get.::.0_1534| x_1536) 0)
0))
…

As usual, let's experiment a bit with this definition.

In :
is_sorted [1;2;3;4;5]

Out:
- : bool = true

In :
is_sorted [1;4;2]

Out:
- : bool = false

In :
is_sorted 

Out:
- : bool = true

In :
instance (fun x -> List.length x >= 5 && is_sorted x)

Out:
- : int list -> bool = <fun>
module CX : sig val x : int list end

Instance (after 11 steps, 0.040s):
let (x : int list) = [7719; 7719; 16574; 18856; 24709]

Instance
proof attempt
ground_instances11
definitions0
inductions0
search_time
0.040s
details
Expand
smt_stats
 num checks 23 arith assert lower 60 arith pivots 27 rlimit count 8731 mk clause 104 datatype occurs check 69 mk bool var 315 arith assert upper 38 datatype splits 35 decisions 94 arith add rows 128 propagations 201 interface eqs 1 conflicts 36 arith fixed eqs 35 datatype accessor ax 24 arith conflicts 11 arith assert diseq 10 datatype constructor ax 42 num allocs 4.03571e+09 final checks 36 added eqs 307 del clause 72 arith eq adapter 38 memory 42.55 max memory 52.67
Expand
• start[0.040s] List.length :var_0: >= 5 && is_sorted :var_0:
• unroll
 expr (is_sorted_41 x_46) expansions
• unroll
 expr (|List.length_1552| x_46) expansions
• unroll
 expr (|List.length_1552| (|get.::.1_1551| x_46)) expansions
• unroll
 expr (|List.length_1552| (|get.::.1_1551| (|get.::.1_1551| x_46))) expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1551| x_46)) expansions
• unroll
 expr (|List.length_1552| (|get.::.1_1551| (|get.::.1_1551| (|get.::.1_1551| x_46)))) expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1551| (|get.::.1_1551| x_46))) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1551| (|get.::.1_1551| (|get.::.1_1551| (|get.::.1_1551| x_46)))))) (|List.l… expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1551| (|get.::.1_1551| (|get.::.1_1551| x_46)))) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1551| (|get.::.1_1551| (|get.::.1_1551| (|get.::.1_1551| x_46)))))) (|List.l… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1551| (|get.::.1_1551| (|get.::.1_1551| (|get.::.1_1551| x_46)))))) (is_sort… expansions
• Sat (Some let (x : int list) = [7719; 7719; 16574; 18856; 24709] )
In :
instance (fun x -> List.length x >= 5 && is_sorted x && is_sorted (List.rev x))

Out:
- : int list -> bool = <fun>
module CX : sig val x : int list end

Instance (after 44 steps, 0.222s):
let (x : int list) = [1733; 1733; 1733; 1733; 1733]

Instance
proof attempt
ground_instances44
definitions0
inductions0
search_time
0.222s
details
Expand
smt_stats
 arith offset eqs 158 num checks 89 arith assert lower 563 arith pivots 391 rlimit count 107941 mk clause 1094 datatype occurs check 2466 mk bool var 5164 arith assert upper 664 datatype splits 1056 decisions 2445 arith add rows 2041 arith bound prop 34 propagations 6197 interface eqs 98 conflicts 214 arith fixed eqs 480 datatype accessor ax 760 minimized lits 67 arith conflicts 32 arith assert diseq 138 datatype constructor ax 1035 num allocs 4.2212e+09 final checks 288 added eqs 11649 del clause 848 arith eq adapter 554 memory 44.09 max memory 52.67
Expand
• start[0.222s]
List.length :var_0: >= 5
&& is_sorted :var_0: && is_sorted (List.rev :var_0:)
• #### simplify

 into (List.length :var_0: >= 5 && is_sorted :var_0:) && is_sorted (List.rev :var_0:) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|List.rev_1565| x_48) expansions
• unroll
 expr (is_sorted_41 (|List.rev_1565| x_48)) expansions
• unroll
 expr (is_sorted_41 x_48) expansions
• unroll
 expr (|List.length_1562| x_48) expansions
• unroll
 expr (|List.rev_1565| (|get.::.1_1561| x_48)) expansions
• unroll
 expr (|List.append_1569| (|List.rev_1565| (|get.::.1_1561| x_48)) (|::_3| (|get.::.0_1560| x_48) |[]_… expansions
• unroll
 expr (|List.length_1562| (|get.::.1_1561| x_48)) expansions
• unroll
 expr (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| x_48))) expansions
• unroll
 expr (|List.append_1569| (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| x_48))) (|::_3| (|get.::.… expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1561| (|List.rev_1565| x_48))) expansions
• unroll
 expr (|List.length_1562| (|get.::.1_1561| (|get.::.1_1561| x_48))) expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1561| x_48)) expansions
• unroll
 expr (|List.append_1569| (|get.::.1_1561| (|List.rev_1565| (|get.::.1_1561| x_48))) (|::_3| (|get.::.… expansions
• unroll
 expr (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))) expansions
• unroll
 expr (let ((a!1 (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48))))) (a!2 … expansions
• unroll
 expr (|List.length_1562| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))) expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1561| (|get.::.1_1561| x_48))) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|List.rev_1565| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1561| (|get.::.1_1561| (|List.rev_1565| x_48)))) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.r… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48))))) (a!2 … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.l… expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))) expansions
• unroll
 expr (let ((a!1 (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48))))) (a!2 … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.r… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.l… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|List.rev_1565| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (is_sort… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48))))) (a!2 … expansions
• unroll
 expr (let ((a!1 (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48))))) (a!2 … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|List.rev_1565| x_48)))))) (is_sort… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|List.rev_1565| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.r… expansions
• unroll
 expr (let ((a!1 (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48))))) (a!2 … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|List.rev_1565| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48))))) (a!2 … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| x_48)))))) (|List.l… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1561| (|get.::.1_1561| (|get.::.1_1561| (|List.rev_1565| x_48)))))) (is_sort… expansions
• Sat (Some let (x : int list) = [1733; 1733; 1733; 1733; 1733] )

## Proving Merge Sort sorts¶

Now that we've defined our is_sorted predicate, we're ready to state one of our main verification goals: that merge_sort sorts!

We can write this this way:

theorem merge_sort_sorts x =
is_sorted (merge_sort x)


Before we try to prove this for all possible cases by induction, let's ask Imandra to verify that this property holds up to our current recursion unrolling bound (100).

In :
verify (fun x -> is_sorted (merge_sort x))

Out:
- : int list -> bool = <fun>

Unknown (Verified up to bound 100)
Expand
 expanded merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge_sort (odds (odds (List.tl (odds …))))merge_sort (odds (odds (odds …)))odds (List.tl (List.tl (odds (List.tl (odds x)))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (List.tl (List.tl x)))))odds (List.tl (odds (List.tl (odds (odds …)))))merge (if List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) else if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else merge_sort (odds (List.tl x))) <= List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else List.tl (merge_sort (odds x)) else (List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))))) then if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else List.tl (merge_sort (odds x)) else List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) else (List.tl (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else List.tl (merge_sort (odds x)) else (List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))))))) (if List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) else if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else merge_sort (odds (List.tl x))) <= List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else List.tl (merge_sort (odds x)) else (List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))))) then List.tl (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) else …) else …)merge_sort (odds (List.tl (odds (odds …))))merge_sort (odds (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl (odds (List.tl (odds x))))))odds (odds (odds (List.tl x)))odds (odds (List.tl (odds (List.tl x))))is_sorted (merge_sort x)merge (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else (List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))))) (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) else if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else merge_sort (odds (List.tl (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds xodds (odds (odds (List.tl (odds …))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))merge_sort (odds (List.tl (odds (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (odds (List.tl (odds x)))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (List.tl x)))))))odds (List.tl (List.tl (List.tl (List.tl (odds (List.tl x))))))odds (List.tl (List.tl (odds (List.tl x))))odds (List.tl (List.tl (List.tl (odds (List.tl x)))))odds (odds (List.tl x))odds (List.tl (odds (List.tl x)))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge_sort (odds (odds (List.tl x)))merge_sort (odds (List.tl (odds (List.tl x))))odds (List.tl (odds (odds (odds …))))odds (odds (List.tl (odds (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x))))merge_sort (odds (odds (odds …)))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (odds (List.tl (odds x))))merge_sort xis_sorted (List.tl (List.tl (List.tl (merge_sort x))))odds (List.tl (List.tl (List.tl (List.tl (odds x)))))odds (List.tl (List.tl (odds x)))merge_sort (odds (odds (List.tl (odds …))))odds (odds x)merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))merge_sort (odds (List.tl (odds x)))odds (List.tl (List.tl x))odds (List.tl (odds (odds (List.tl (odds …)))))merge_sort (odds (List.tl x))odds (List.tl (List.tl (List.tl (odds (odds (List.tl x))))))odds (List.tl (List.tl (List.tl (odds (List.tl (odds (List.tl x)))))))odds (List.tl (List.tl (odds (odds x))))merge_sort (odds (odds (odds …)))merge_sort (odds (List.tl (odds (odds …))))merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))odds (List.tl x)odds (odds (odds (odds …)))odds (List.tl (odds (List.tl (odds (List.tl (odds …))))))merge_sort (odds x)odds (List.tl (List.tl (List.tl (odds (odds x)))))merge_sort (odds (odds (List.tl (odds …))))is_sorted (List.tl (List.tl (merge_sort x)))odds (List.tl (List.tl (List.tl (List.tl x))))odds (odds (List.tl (odds (odds …))))odds (odds (odds (odds …)))merge_sort (odds (List.tl (odds (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (odds (odds x))odds (List.tl (odds (odds (List.tl x))))odds (List.tl (odds (List.tl (odds (List.tl x)))))merge (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else List.tl (merge_sort (odds x)) else (List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))))) (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) else if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else merge_sort (odds (List.tl x)))merge_sort (odds (odds (odds …)))merge_sort (odds (odds (List.tl (odds …))))merge (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else (List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))))) (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) else if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else merge_sort (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl x)))odds (odds (List.tl (odds (List.tl (odds …)))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (List.tl (List.tl (odds (odds (List.tl x)))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (List.tl (List.tl (odds (List.tl (odds (List.tl x))))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (odds (odds x)))merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds x))))))merge_sort (odds (odds (odds …)))odds (List.tl (List.tl (List.tl (odds x))))merge_sort (odds (List.tl (odds (odds …))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (odds x))is_sorted (List.tl (merge_sort x))merge (merge_sort (odds x)) (merge_sort (odds (List.tl x)))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))merge_sort (odds (odds x))odds (List.tl (odds (List.tl (odds (odds …)))))odds (List.tl (odds (List.tl (odds (List.tl (odds …))))))odds (List.tl (odds (odds (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …)))) blocked merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge_sort (odds (odds (List.tl (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (odds (List.tl (odds (List.tl (odds …)))))merge (if List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) else if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else merge_sort (odds (List.tl (odds …)))) <= List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else (List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))))) then if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) else (List.tl (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else (List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))))))) (if List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) else if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else merge_sort (odds (List.tl (odds …)))) <= List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else (List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))))) then List.tl (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) else …) else …)odds (List.tl (odds (List.tl (odds (List.tl (odds …))))))odds (odds (List.tl (odds (odds …))))odds (List.tl (List.tl (odds (odds (odds …)))))merge_sort (odds (List.tl (odds (odds …))))odds (List.tl (List.tl (List.tl (odds (List.tl (odds (List.tl (odds …))))))))merge_sort (odds (odds (List.tl (odds …))))merge_sort (odds (List.tl (odds (odds …))))merge_sort (odds (List.tl (odds (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))is_sorted (List.tl (List.tl (List.tl (List.tl (merge_sort x)))))odds (List.tl (odds (odds (odds …))))odds (odds (odds (odds …)))odds (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))merge_sort (odds (odds (odds …)))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (List.tl (odds (List.tl (odds (odds …))))))merge_sort (odds (List.tl (odds (odds …))))odds (List.tl (List.tl (odds (odds (odds …)))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (odds (List.tl x))))))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (List.tl (odds (List.tl x)))))))))odds (List.tl (List.tl (List.tl (List.tl (odds (odds x))))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (odds (List.tl x)))))))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (odds (List.tl x))))))))merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))odds (odds (odds (odds …)))odds (List.tl (odds (List.tl (odds (odds …)))))odds (List.tl (odds (odds (List.tl (odds …)))))merge_sort (odds (odds (List.tl (odds …))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (List.tl (odds (List.tl (odds (List.tl (odds …)))))))merge_sort (odds (odds (odds …)))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (odds (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (odds x)))))))merge_sort (odds (odds (odds …)))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (odds x)))))))merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))odds (odds (odds (List.tl (odds …))))odds (List.tl (odds (List.tl (odds (odds …)))))merge_sort (odds (List.tl (odds (odds …))))odds (List.tl (List.tl (List.tl (odds (List.tl (odds (odds …)))))))odds (List.tl (List.tl (List.tl (odds (List.tl (odds (List.tl (odds …))))))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (odds (odds (odds …))))))merge_sort (odds (odds (List.tl (odds …))))merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge (if List.hd (if List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) else if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else merge_sort (odds (List.tl x))) <= List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else List.tl (merge_sort (odds x)) else (List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))))) then List.tl (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) else if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else merge_sort (odds (List.tl x))) else if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) else if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else merge_sort (odds (List.tl x))) <= List.hd (if List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) else if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else merge_sort (odds (List.tl x))) <= List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then List.tl (merge_sort (odds (List.tl x))) else (merge_sort (odds (List.tl x)))) <= List.hd (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))) then if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else List.tl (merge_sort (odds x)) else (List.tl (if List.hd (merge_sort (odds (List.tl x))) <= List.hd (merge_sort (odds x)) then merge_sort (odds x) else (List.tl (merge_sort (odds x)))))) then … else …) then … else …) …odds (List.tl (odds (odds (odds …))))odds (List.tl (odds (List.tl (odds (List.tl (odds …))))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))odds (odds (List.tl (odds (odds …))))merge_sort (odds (List.tl (odds (odds …))))merge_sort (odds (odds (odds …)))merge_sort (odds (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl (odds (List.tl (odds (odds …)))))))odds (odds (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl (List.tl (odds (odds (List.tl x)))))))odds (List.tl (List.tl (List.tl (List.tl (odds (List.tl (odds (List.tl x))))))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (List.tl (odds (odds (List.tl (odds …)))))odds (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (odds (odds (odds …))))merge_sort (odds (odds (odds …)))merge_sort (odds (List.tl (odds (odds …))))merge_sort (odds (odds (odds …)))odds (List.tl (List.tl (odds (odds (List.tl (odds …))))))odds (odds (List.tl (odds (List.tl (odds …)))))merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (List.tl (odds (List.tl (odds x)))))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (odds (odds (List.tl (odds …))))odds (List.tl (odds (odds (List.tl (odds …)))))odds (odds (odds (odds …)))odds (List.tl (List.tl (List.tl (odds (odds (odds …))))))merge_sort (odds (odds (odds …)))odds (List.tl (List.tl (odds (List.tl (odds (odds …))))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (List.tl (odds x))))))))merge (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …)))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (odds x))))))))odds (odds (List.tl (odds (odds …))))odds (List.tl (odds (List.tl (odds (List.tl (odds …))))))odds (odds (odds (List.tl (odds …))))odds (List.tl (odds (List.tl (odds (odds …)))))merge (if List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) else if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else merge_sort (odds (List.tl (odds …)))) <= List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else (List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))))) then if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) else (List.tl (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else (List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))))))) (if List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) else if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else merge_sort (odds (List.tl (odds …)))) <= List.hd (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else (List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))))) then List.tl (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) else …) else …)merge_sort (odds (odds (List.tl (odds …))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))merge (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else List.tl (merge_sort (odds (odds …))) else (List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))))) (if List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) <= List.hd (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then merge_sort (odds (odds …)) else (List.tl (merge_sort (odds (odds …))))) then List.tl (if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else (merge_sort (odds (List.tl (odds …))))) else if List.hd (merge_sort (odds (List.tl (odds …)))) <= List.hd (merge_sort (odds (odds …))) then List.tl (merge_sort (odds (List.tl (odds …)))) else merge_sort (odds (List.tl (odds …))))merge_sort (odds (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl (odds (odds (List.tl (odds …)))))))
proof attempt
 ground_instances 100 definitions 0 inductions 0 search_time 2.342s
Expand
• start[2.342s] is_sorted (merge_sort :var_0:)
• unroll
 expr (merge_sort_37 x_50) expansions
• unroll
 expr (is_sorted_41 (merge_sort_37 x_50)) expansions
• unroll
 expr (odds_1323 (|get.::.1_1322| x_50)) expansions
• unroll
 expr (merge_sort_37 (odds_1323 (|get.::.1_1322| x_50))) expansions
• unroll
 expr (odds_1323 x_50) expansions
• unroll
 expr (merge_sort_37 (odds_1323 x_50)) expansions
• unroll
 expr (merge_14 (merge_sort_37 (odds_1323 x_50)) (merge_sort_37 (odds_1323 (|get.::.1_1322| x_50… expansions
• unroll
 expr (odds_1323 (|get.::.1_1322| (|get.::.1_1322| x_50))) expansions
• unroll
 expr (odds_1323 (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| x_50)))) expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1322| (merge_sort_37 x_50))) expansions
• unroll
 expr (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))) expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (merge_sort_37 a!1)) expansions
• unroll
 expr (odds_1323 (odds_1323 (|get.::.1_1322| x_50))) expansions
• unroll
 expr (let ((a!1 (merge_sort_37 (odds_1323 (odds_1323 (|get.::.1_1322| x_50))))) (a!2 (odds_1323 (|g… expansions
• unroll
 expr (merge_sort_37 (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))) expansions
• unroll
 expr (let ((a!1 (|get.::.0_1321| (merge_sort_37 (odds_1323 (|get.::.1_1322| x_50))))) (a!4 (|get.::… expansions
• unroll
 expr (odds_1323 (|get.::.1_1322| (odds_1323 x_50))) expansions
• unroll
 expr (merge_sort_37 (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))) expansions
• unroll
 expr (odds_1323 (odds_1323 x_50)) expansions
• unroll
 expr (merge_sort_37 (odds_1323 (odds_1323 x_50))) expansions
• unroll
 expr (let ((a!1 (merge_sort_37 (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (merge_14 (merge_sort_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 a!1… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| x_50)))))) (odds_13… expansions
• unroll
 expr (let ((a!1 (|get.::.0_1321| (merge_sort_37 (odds_1323 (|get.::.1_1322| x_50))))) (a!3 (|get.::… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| x_50)))))) (odds_13… expansions
• unroll
 expr (odds_1323 (|get.::.1_1322| (|get.::.1_1322| (odds_1323 x_50)))) expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50))))) (a!2 (merge_sort_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 a!1… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 a!1)) expansions
• unroll
 expr (is_sorted_41 (|get.::.1_1322| (|get.::.1_1322| (merge_sort_37 x_50)))) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (merge_sort_37 (odds… expansions
• unroll
 expr (odds_1323 (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))) expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (merge_sort_37 a!1)) expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (|get.::.1_1322| (odds_1323 x_50))))) (a!2 (|get.::.1_1322| (… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|g… expansions
• unroll
 expr (odds_1323 (|get.::.1_1322| (odds_1323 (odds_1323 x_50)))) expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (odds_1323 x_50)))))) (merge_sort_37 a!1)) expansions
• unroll
 expr (odds_1323 (odds_1323 (odds_1323 x_50))) expansions
• unroll
 expr (merge_sort_37 (odds_1323 (odds_1323 (odds_1323 x_50)))) expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (merge_sort_37 (odds_1323 (odds_1323 (odds_1323 x_50))))) (a!2 (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (merge_sort_37 (odds_1323 (|get.::.1_1322| (odds_1323 x_50))))) (a!2 (|get.::.0_132… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 a!1)) expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (merge_sort_37 (odds… expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 a!1)) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (merge_sort_37 (odds… expansions
• unroll
 expr (odds_1323 (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))) expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (merge_sort_37 a!1)) expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (merge_sort_37 (odds… expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (merge_14 (merge_sor… expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (odds_1323 (|get.::.1_1322| x_50))))) (a!2 (|get.::.1_1322| (… expansions
• unroll
 expr (let ((a!1 (|get.::.0_1321| (merge_sort_37 (odds_1323 (|get.::.1_1322| x_50))))) (a!3 (|get.::… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| (merge_sort_37 x_50)))))) (is_sorted… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|g… expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 (|get.::.1_1322… expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (merge_sort_37 (odds_1323 … expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 a!1)) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (odds_1323 (odds_1323 x_50)))))) (odds_1323 a!1)) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| x_50)))))) (odds_13… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 (|g… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (odds_1323 (odds_1323 x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| x_50)))))) (odds_13… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (odds_1323 x_50)))))) (odds_1323 a!1)) expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50))))) (a!2 (merge_sort_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (odds_1323 x_50)))))) (merge_sort_37 (odds_1323 … expansions
• unroll
 expr (odds_1323 (odds_1323 (odds_1323 (odds_1323 x_50)))) expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (odds_1323 (odds_1323 x_50)))))) (merge_sort_37 a!1)) expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (odds_1323 (odds_1323 x_50))))) (a!2 (|get.::.1_1322| (odds_1… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 (|g… expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (odds_1323 x_50))))) (a!2 (merge_sort_37 (od… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (odds_1323 x_50)))))) (odds_1323 (|get.::.1_1322… expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (odds_1323 x_50)))))) (merge_sort_37 (odds_1323 … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (odds_1323 x_50)))))) (odds_1323 a!1)) expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (odds_1323 x_50)))))) (merge_sort_37 (odds_1323 … expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (odds_1323 x_50)))))) (merge_14 (merge_sort_37 (… expansions
• unroll
 expr (let ((a!1 (merge_sort_37 (odds_1323 (|get.::.1_1322| (odds_1323 x_50))))) (a!2 (|get.::.0_132… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (merge_sort_37 (odds… expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (odds_1323 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (odds_1323 (odds_132… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (|get.::.1_1322| (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|g… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|get.::.… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (merge_sort_37 (odds… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (merge_sort_37 (odds… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (odds_132… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (merge_sort_37 (odds… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (let ((a!2 (merge_sort… expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 (|get.::.1_1322… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1322| (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (let ((a!2 (merge_sort… expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (merge_14 (merge_sort_37 (… expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (merge_sort_37 (odds_1323 … expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (odds_1323 a!1)) expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (odds_1323 (|get.::.1_1322| x_50)))))) (merge_sort_37 (odds_1323 … expansions
• unroll
 expr (let ((a!1 (odds_1323 (odds_1323 (|get.::.1_1322| (odds_1323 x_50)))))) (merge_sort_37 (odds_1323 … expansions

Excellent. This gives us quite some confidence that this result is true. Let's now try to prove it by induction. We'll want to use an induction principle suggested by the definition of merge_sort. Let's use our usual strategy of #max_induct 1, so we can analyse Imandra's output to help us find needed lemmata.

Note, we could prove this theorem directly without any lemmas by using #max_induct 3, but it's good practice to use #max_induct 1 and have Imandra help us develop useful collections of lemmas.

In :
#max_induct 1

Out:

In :
theorem merge_sort_sorts x =
is_sorted (merge_sort x)
[@@induct functional merge_sort]

Out:
val merge_sort_sorts : int list -> bool = <fun>
Goal:

is_sorted (merge_sort x).

1 nontautological subgoal.

We shall induct according to a scheme derived from merge_sort.

Induction scheme:

(not (not (x <> [] && List.tl x = []) && not (x = [])) ==> φ x)
&& (not (x = [])
&& not (x <> [] && List.tl x = [])
&& φ (odds (List.tl x)) && φ (odds x)
==> φ x).

2 nontautological subgoals.

Subgoal 2:

|---------------------------------------------------------------------------
C0. not (x <> [] && List.tl x = []) && not (x = [])
C1. is_sorted (merge_sort x)

But simplification reduces this to true, using the definitions of is_sorted
and merge_sort.

Subgoal 1:

H0. not (x = [])
H1. not (x <> [] && List.tl x = [])
H2. is_sorted (merge_sort (odds (List.tl x)))
H3. is_sorted (merge_sort (odds x))
|---------------------------------------------------------------------------
is_sorted (merge_sort x)

This simplifies, using the definition of merge_sort to:

Subgoal 1':

H0. x <> []
H1. (List.tl x) <> []
H2. is_sorted (merge_sort (odds (List.tl x)))
H3. is_sorted (merge_sort (odds x))
|---------------------------------------------------------------------------
is_sorted (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))

We can eliminate destructors by the following substitution:
x -> x1 :: x2

This produces the modified subgoal:

Subgoal 1'':

H0. x2 <> []
H1. is_sorted (merge_sort (odds x2))
H2. is_sorted (merge_sort (odds (x1 :: x2)))
|---------------------------------------------------------------------------
is_sorted (merge (merge_sort (odds (x1 :: x2))) (merge_sort (odds x2)))

Candidates for generalization:

merge_sort (odds x2)
merge_sort (odds (x1 :: x2))

This produces the modified subgoal:

Subgoal 1''':

H0. x2 <> []
H1. is_sorted gen_1
H2. is_sorted gen_2
|---------------------------------------------------------------------------
is_sorted (merge gen_2 gen_1)

Must try induction.

⚠  Aborting proof attempt for merge_sort_sorts.

ⓘ  Rules:
(:def is_sorted)
(:def merge_sort)
(:induct merge_sort)

Checkpoints:

H0. x2 <> []
H1. is_sorted gen_1
H2. is_sorted gen_2
|---------------------------------------------------------------------------
is_sorted (merge gen_2 gen_1)

Error[/server]: Maximum induction depth reached (1). You can set this with #max_induct.


Analysing the output of this proof attempt, we notice the following components of our Checkpoint:

H1. is_sorted gen_1
H2. is_sorted gen_2
|---------------------------------------------------------------------------
is_sorted (merge gen_2 gen_1)


Ah, of course! We need to prove a lemma that merge respects the sortedness of its inputs.

Let's do this by functional induction following the definition of merge and install it as a rewrite rule. We'll allow nested induction (#max_induct 2), but it's a good exercise to do this proof without it (deriving an additional lemma!).

In :
#max_induct 2;;

theorem merge_sorts x y =
is_sorted x && is_sorted y
==>
is_sorted (merge x y)
[@@induct functional merge]
[@@rewrite]

Out:
val merge_sorts : int list -> int list -> bool = <fun>
Goal:

is_sorted x && is_sorted y ==> is_sorted (merge x y).

1 nontautological subgoal.

We shall induct according to a scheme derived from merge.

Induction scheme:

(not (List.hd x < List.hd y && not (y = []) && not (x = []))
&& not (not (List.hd x < List.hd y) && not (y = []) && not (x = []))
==> φ y x)
&& (not (x = [])
&& not (y = []) && not (List.hd x < List.hd y) && φ (List.tl y) x
==> φ y x)
&& (not (x = [])
&& not (y = []) && List.hd x < List.hd y && φ y (List.tl x)
==> φ y x).

3 nontautological subgoals.

Subgoal 3:

H0. not ((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []))
H1. not ((List.hd y <= List.hd x && not (y = [])) && not (x = []))
H2. is_sorted x
H3. is_sorted y
|---------------------------------------------------------------------------
is_sorted (merge x y)

But simplification reduces this to true, using the definition of merge.

Subgoal 2:

H0. not (x = [])
H1. not (y = [])
H2. List.hd y <= List.hd x
H3. is_sorted x && is_sorted (List.tl y) ==> is_sorted (merge x (List.tl y))
H4. is_sorted x
H5. is_sorted y
|---------------------------------------------------------------------------
is_sorted (merge x y)

This simplifies, using the definitions of is_sorted and merge to the
following 3 subgoals:

Subgoal 2.3:

H0. x <> []
H1. y <> []
H2. List.hd y <= List.hd x
H3. is_sorted (merge x (List.tl y))
H4. is_sorted x
H5. is_sorted (List.tl y)
H6. (List.tl y) <> []
H7. List.hd y <= List.hd (List.tl y)
H8. (merge x (List.tl y)) <> []
|---------------------------------------------------------------------------
List.hd y <= List.hd (merge x (List.tl y))

But we verify Subgoal 2.3 by recursive unrolling.

Subgoal 2.2:

H0. x <> []
H1. y <> []
H2. List.hd y <= List.hd x
H3. is_sorted x
H4. List.tl y = []
H5. (merge x (List.tl y)) <> []
|---------------------------------------------------------------------------
List.hd y <= List.hd (merge x (List.tl y))

But simplification reduces this to true, using the definition of merge.

Subgoal 2.1:

H0. x <> []
H1. y <> []
H2. List.hd y <= List.hd x
H3. is_sorted x
H4. List.tl y = []
H5. (merge x (List.tl y)) <> []
H6. List.hd y <= List.hd (merge x (List.tl y))
|---------------------------------------------------------------------------
is_sorted (merge x (List.tl y))

But simplification reduces this to true, using the definition of merge.

Subgoal 1:

H0. not (x = [])
H1. not (y = [])
H2. not (List.hd y <= List.hd x)
H3. is_sorted (List.tl x) && is_sorted y ==> is_sorted (merge (List.tl x) y)
H4. is_sorted x
H5. is_sorted y
|---------------------------------------------------------------------------
is_sorted (merge x y)

This simplifies, using the definitions of is_sorted and merge to the
following 3 subgoals:

Subgoal 1.3:

H0. x <> []
H1. y <> []
H2. is_sorted (merge (List.tl x) y)
H3. is_sorted (List.tl x)
H4. (List.tl x) <> []
H5. List.hd x <= List.hd (List.tl x)
H6. is_sorted y
H7. (merge (List.tl x) y) <> []
|---------------------------------------------------------------------------
C0. List.hd y <= List.hd x
C1. List.hd x <= List.hd (merge (List.tl x) y)

But we verify Subgoal 1.3 by recursive unrolling.

Subgoal 1.2:

H0. x <> []
H1. y <> []
H2. List.tl x = []
H3. is_sorted y
H4. (merge (List.tl x) y) <> []
|---------------------------------------------------------------------------
C0. List.hd y <= List.hd x
C1. List.hd x <= List.hd (merge (List.tl x) y)

But simplification reduces this to true, using the definition of merge.

Subgoal 1.1:

H0. x <> []
H1. y <> []
H2. List.tl x = []
H3. is_sorted y
H4. (merge (List.tl x) y) <> []
H5. List.hd x <= List.hd (merge (List.tl x) y)
|---------------------------------------------------------------------------
C0. List.hd y <= List.hd x
C1. is_sorted (merge (List.tl x) y)

But simplification reduces this to true, using the definition of merge.

ⓘ  Rules:
(:def is_sorted)
(:def merge)
(:induct merge)


Proved
proof
ground_instances6
definitions21
inductions1
search_time
1.363s
details
Expand
smt_stats
 num checks 8 arith assert lower 7 arith pivots 5 rlimit count 112714 mk clause 23 datatype occurs check 13 mk bool var 79 arith assert upper 6 datatype splits 3 decisions 29 arith add rows 14 propagations 29 conflicts 10 datatype accessor ax 8 arith conflicts 2 arith assert diseq 1 datatype constructor ax 10 final checks 4 added eqs 72 del clause 4 arith eq adapter 5 memory 79.81 max memory 91.78 num allocs 4.40138e+10
Expand
• start[1.363s, "Goal"]
is_sorted :var_0: && is_sorted :var_1:
==> is_sorted (merge :var_0: :var_1:)
• #### subproof

(not (is_sorted x) || not (is_sorted y)) || is_sorted (merge x y)
• start[1.362s, "1"]
(not (is_sorted x) || not (is_sorted y)) || is_sorted (merge x y)
• induction on (functional merge)
:scheme (not (List.hd x < List.hd y && not (y = []) && not (x = []))
&& not (not (List.hd x < List.hd y) && not (y = []) && not (x = []))
==> φ y x)
&& (not (x = [])
&& not (y = [])
&& not (List.hd x < List.hd y) && φ (List.tl y) x
==> φ y x)
&& (not (x = [])
&& not (y = []) && List.hd x < List.hd y && φ y (List.tl x)
==> φ y x)
• Split ((((not
(not
((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []))
&& not ((List.hd y <= List.hd x && not (y = [])) && not (x = [])))
|| not (is_sorted x && is_sorted y))
|| is_sorted (merge x y))
&& ((not
(((not (x = []) && not (y = [])) && List.hd y <= List.hd x)
&& (not (is_sorted x && is_sorted (List.tl y))
|| is_sorted (merge x (List.tl y))))
|| not (is_sorted x && is_sorted y))
|| is_sorted (merge x y)))
&& ((not
(((not (x = []) && not (y = [])) && not (List.hd y <= List.hd x))
&& (not (is_sorted (List.tl x) && is_sorted y)
|| is_sorted (merge (List.tl x) y)))
|| not (is_sorted x && is_sorted y))
|| is_sorted (merge x y))
:cases [((((not (List.hd y <= List.hd x) && not (y = []))
&& not (x = [])
|| (List.hd y <= List.hd x && not (y = [])) && not (x = []))
|| not (is_sorted x))
|| not (is_sorted y))
|| is_sorted (merge x y);
(((((x = [] || y = []) || not (List.hd y <= List.hd x))
|| not
(not (is_sorted x && is_sorted (List.tl y))
|| is_sorted (merge x (List.tl y))))
|| not (is_sorted x))
|| not (is_sorted y))
|| is_sorted (merge x y);
(((((x = [] || y = []) || List.hd y <= List.hd x)
|| not
(not (is_sorted (List.tl x) && is_sorted y)
|| is_sorted (merge (List.tl x) y)))
|| not (is_sorted x))
|| not (is_sorted y))
|| is_sorted (merge x y)])
• ##### subproof
(((((x = [] || y = []) || List.hd y <= List.hd x) || not (not (is_sorted (List.tl x) && is_sorted y) || is_sorted (merge (List.tl x) y))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)
• start[1.359s, "1"]
(((((x = [] || y = []) || List.hd y <= List.hd x)
|| not
(not (is_sorted (List.tl x) && is_sorted y)
|| is_sorted (merge (List.tl x) y)))
|| not (is_sorted x))
|| not (is_sorted y))
|| is_sorted (merge x y)
• ###### simplify
 into ((((((((((x = [] || y = []) || List.hd y <= List.hd x) || not (is_sorted (merge (List.tl x) y))) || not (is_sorted (List.tl x))) || List.tl x = []) || not (List.hd x <= List.hd (List.tl x))) || not (is_sorted y)) || merge (List.tl x) y = []) || List.hd x <= List.hd (merge (List.tl x) y)) && ((((((x = [] || y = []) || List.hd y <= List.hd x) || not (List.tl x = [])) || not (is_sorted y)) || merge (List.tl x) y = []) || List.hd x <= List.hd (merge (List.tl x) y))) && (((((((x = [] || y = []) || List.hd y <= List.hd x) || not (List.tl x = [])) || not (is_sorted y)) || is_sorted (merge (List.tl x) y)) || merge (List.tl x) y = []) || not (List.hd x <= List.hd (merge (List.tl x) y))) expansions [merge, is_sorted, is_sorted, merge, is_sorted, is_sorted, is_sorted, merge] rewrite_steps forward_chaining
• Subproof
• Subproof
• Subproof
• ##### subproof
(((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (not (is_sorted x && is_sorted (List.tl y)) || is_sorted (merge x (List.tl y)))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)
• start[1.359s, "2"]
(((((x = [] || y = []) || not (List.hd y <= List.hd x))
|| not
(not (is_sorted x && is_sorted (List.tl y))
|| is_sorted (merge x (List.tl y))))
|| not (is_sorted x))
|| not (is_sorted y))
|| is_sorted (merge x y)
• ###### simplify
 into ((((((((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (is_sorted (merge x (List.tl y)))) || not (is_sorted x)) || not (is_sorted (List.tl y))) || List.tl y = []) || not (List.hd y <= List.hd (List.tl y))) || merge x (List.tl y) = []) || List.hd y <= List.hd (merge x (List.tl y))) && ((((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (is_sorted x)) || not (List.tl y = [])) || merge x (List.tl y) = []) || List.hd y <= List.hd (merge x (List.tl y)))) && (((((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (is_sorted x)) || not (List.tl y = [])) || is_sorted (merge x (List.tl y))) || merge x (List.tl y) = []) || not (List.hd y <= List.hd (merge x (List.tl y)))) expansions [merge, is_sorted, is_sorted, merge, is_sorted, is_sorted, is_sorted, merge] rewrite_steps forward_chaining
• Subproof
• Subproof
• Subproof
• ##### subproof
((((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []) || (List.hd y <= List.hd x && not (y = [])) && not (x = [])) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)
• start[1.359s, "3"]
((((not (List.hd y <= List.hd x) && not (y = [])) && not (x = [])
|| (List.hd y <= List.hd x && not (y = [])) && not (x = []))
|| not (is_sorted x))
|| not (is_sorted y))
|| is_sorted (merge x y)
• ###### simplify
 into true expansions merge rewrite_steps forward_chaining

Excellent! Now that we have that key lemma proved and available as a rewrite rule, let's return to our original goal:

In :
theorem merge_sort_sorts x =
is_sorted (merge_sort x)
[@@induct functional merge_sort]

Out:
val merge_sort_sorts : int list -> bool = <fun>
Goal:

is_sorted (merge_sort x).

1 nontautological subgoal.

We shall induct according to a scheme derived from merge_sort.

Induction scheme:

(not (not (x <> [] && List.tl x = []) && not (x = [])) ==> φ x)
&& (not (x = [])
&& not (x <> [] && List.tl x = [])
&& φ (odds (List.tl x)) && φ (odds x)
==> φ x).

2 nontautological subgoals.

Subgoal 2:

|---------------------------------------------------------------------------
C0. not (x <> [] && List.tl x = []) && not (x = [])
C1. is_sorted (merge_sort x)

But simplification reduces this to true, using the definitions of is_sorted
and merge_sort.

Subgoal 1:

H0. not (x = [])
H1. not (x <> [] && List.tl x = [])
H2. is_sorted (merge_sort (odds (List.tl x)))
H3. is_sorted (merge_sort (odds x))
|---------------------------------------------------------------------------
is_sorted (merge_sort x)

This simplifies, using the definition of merge_sort to:

Subgoal 1':

H0. x <> []
H1. (List.tl x) <> []
H2. is_sorted (merge_sort (odds (List.tl x)))
H3. is_sorted (merge_sort (odds x))
|---------------------------------------------------------------------------
is_sorted (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))

But simplification reduces this to true, using the rewrite rule merge_sorts.

ⓘ  Rules:
(:def is_sorted)
(:def merge_sort)
(:rw merge_sorts)
(:induct merge_sort)


Proved
proof
 ground_instances 0 definitions 7 inductions 1 search_time 0.723s
Expand
• start[0.723s, "Goal"] is_sorted (merge_sort :var_0:)
• #### subproof

is_sorted (merge_sort x)
• start[0.723s, "1"] is_sorted (merge_sort x)
• induction on (functional merge_sort)
:scheme (not (not (x <> [] && List.tl x = []) && not (x = [])) ==> φ x)
&& (not (x = [])
&& not (x <> [] && List.tl x = [])
&& φ (odds (List.tl x)) && φ (odds x)
==> φ x)
• Split ((not (x <> [] && List.tl x = []) && not (x = [])
|| is_sorted (merge_sort x))
&& (not
(((not (x = []) && not (x <> [] && List.tl x = []))
&& is_sorted (merge_sort (odds (List.tl x))))
&& is_sorted (merge_sort (odds x)))
|| is_sorted (merge_sort x))
:cases [not (x <> [] && List.tl x = []) && not (x = [])
|| is_sorted (merge_sort x);
(((x = [] || x <> [] && List.tl x = [])
|| not (is_sorted (merge_sort (odds (List.tl x)))))
|| not (is_sorted (merge_sort (odds x))))
|| is_sorted (merge_sort x)])
• ##### subproof
(((x = [] || x <> [] && List.tl x = []) || not (is_sorted (merge_sort (odds (List.tl x))))) || not (is_sorted (merge_sort (odds x)))) || is_sorted (merge_sort x)
• start[0.722s, "1"]
(((x = [] || x <> [] && List.tl x = [])
|| not (is_sorted (merge_sort (odds (List.tl x)))))
|| not (is_sorted (merge_sort (odds x))))
|| is_sorted (merge_sort x)
• ###### simplify
 into (((x = [] || List.tl x = []) || not (is_sorted (merge_sort (odds (List.tl x))))) || not (is_sorted (merge_sort (odds x)))) || is_sorted (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x)))) expansions merge_sort rewrite_steps forward_chaining
• ###### simplify
 into true expansions [] rewrite_steps merge_sorts forward_chaining
• ##### subproof
not (x <> [] && List.tl x = []) && not (x = []) || is_sorted (merge_sort x)
• start[0.722s, "2"]
not (x <> [] && List.tl x = []) && not (x = []) || is_sorted (merge_sort x)
• ###### simplify
 into true expansions [is_sorted, merge_sort, is_sorted, merge_sort, is_sorted, merge_sort] rewrite_steps forward_chaining

Beautiful! So now we've proved half of our specification: merge_sort sorts!

# Merge Sort contains the right elements¶

Let's now turn to the second half of our correctness criterion: That merge_sort x contains "the same" elements as x.

What does this mean, and why does it matter?

## An incorrect sorting function¶

Consider the sorting function bad_sort defined as bad_sort x = [].

Clearly, we could prove theorem bad_sort_sorts x = is_sorted (bad_sort x), even though we'd never want to use bad_sort as a sorting function in practice.

That is, computing a sorted list is only one piece of the puzzle. We must also verify that merge_sort x contains exactly the same elements as x, including their multiplicity).

## Multiset equivalence¶

How can we express this concept? We'll use the notion of a multiset and count the number of occurrences of each element of x, and make sure these are respected by merge_sort.

We'll begin by defining a function num_occurs x y which counts the number of times an element x appears in the list y.

In :
let rec num_occurs x y =
match y with
| [] -> 0
| hd :: tl when hd = x ->
1 + num_occurs x tl
| _ :: tl ->
num_occurs x tl

Out:
val num_occurs : 'a -> 'a list -> Z.t = <fun>

termination proof

### Termination proof

call num_occurs x (List.tl y) from num_occurs x y
originalnum_occurs x y
subnum_occurs x (List.tl y)
original ordinalOrdinal.Int (Ordinal.count y)
sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
path[y <> [] && List.hd y = x && not (y = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 8 arith assert lower 8 arith pivots 5 rlimit count 4672 mk clause 28 datatype occurs check 29 mk bool var 88 arith assert upper 11 datatype splits 5 decisions 23 arith add rows 11 propagations 45 conflicts 10 arith fixed eqs 8 datatype accessor ax 9 arith conflicts 1 arith assert diseq 1 datatype constructor ax 12 final checks 8 added eqs 70 del clause 6 arith eq adapter 8 memory 52.98 max memory 91.78 num allocs 5.3081e+10
Expand
• start[0.016s]
(y <> [] && List.hd y = x)
&& not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
==> not
(((List.tl y) <> [] && List.hd (List.tl y) = x) && not (List.tl y = []))
&& not
(not ((List.tl y) <> [] && List.hd (List.tl y) = x)
&& not (List.tl y = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
(Ordinal.Int (Ordinal.count y))
• ##### simplify
 into (not ((((y <> [] && List.hd y = x) && not (y = [])) && Ordinal.count y >= 0) && Ordinal.count (List.tl y) >= 0) || not (((List.tl y) <> [] && List.hd (List.tl y) = x) && not (List.tl y = [])) && not (not ((List.tl y) <> [] && List.hd (List.tl y) = x) && not (List.tl y = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y))) (Ordinal.Int (Ordinal.count y)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_3344| … expansions
• unroll
 expr (|count_ty_0 list_3344| (|get.::.1_3322| y_3332)) expansions
• unroll
 expr (|count_ty_0 list_3344| y_3332) expansions
• ##### unsat
(let ((a!1 (th-lemma (or (= y_3332 |[]_2|)
(not ((_ is (|[]_2| () |ty_0 li…

call num_occurs x (List.tl y) from num_occurs x y
originalnum_occurs x y
subnum_occurs x (List.tl y)
original ordinalOrdinal.Int (Ordinal.count y)
sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
path[not (y <> [] && List.hd y = x) && not (y = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 4 rlimit count 2254 mk clause 23 datatype occurs check 26 mk bool var 62 arith assert upper 7 datatype splits 5 decisions 19 arith add rows 7 propagations 33 conflicts 9 arith fixed eqs 4 datatype accessor ax 5 arith conflicts 1 datatype constructor ax 9 final checks 7 added eqs 41 del clause 5 arith eq adapter 3 memory 50.08 max memory 91.78 num allocs 5.27826e+10
Expand
• start[0.015s]
not (y <> [] && List.hd y = x)
&& not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
==> not
(((List.tl y) <> [] && List.hd (List.tl y) = x) && not (List.tl y = []))
&& not
(not ((List.tl y) <> [] && List.hd (List.tl y) = x)
&& not (List.tl y = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
(Ordinal.Int (Ordinal.count y))
• ##### simplify
 into (not (((not (y <> [] && List.hd y = x) && not (y = [])) && Ordinal.count y >= 0) && Ordinal.count (List.tl y) >= 0) || not (((List.tl y) <> [] && List.hd (List.tl y) = x) && not (List.tl y = [])) && not (not ((List.tl y) <> [] && List.hd (List.tl y) = x) && not (List.tl y = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y))) (Ordinal.Int (Ordinal.count y)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_3344| … expansions
• unroll
 expr (|count_ty_0 list_3344| (|get.::.1_3322| y_3332)) expansions
• unroll
 expr (|count_ty_0 list_3344| y_3332) expansions
• ##### unsat
(let ((a!1 (= (|count_ty_0 list_3344| y_3332)
(+ 1 (|count_ty_0 list_3344| (|get.:…

Anticipating the need to reason about the interplay of num_occurs and merge, let's prove the following nice lemmas characterising their relationship (applying the max_induct 1 strategy to find these lemmas as above is a great exercise).

In :
theorem num_occur_merge a x y =
num_occurs a (merge x y) = num_occurs a x + num_occurs a y
[@@induct functional merge]
[@@rewrite]

Out:
val num_occur_merge : int -> int list -> int list -> bool = <fun>
Goal:

num_occurs a (merge x y) = num_occurs a x + num_occurs a y.

1 nontautological subgoal.

We shall induct according to a scheme derived from merge.

Induction scheme:

(not (List.hd x < List.hd y && not (y = []) && not (x = []))
&& not (not (List.hd x < List.hd y) && not (y = []) && not (x = []))
==> φ y x a)
&& (not (x = [])
&& not (y = []) && not (List.hd x < List.hd y) && φ (List.tl y) x a
==> φ y x a)
&& (not (x = [])
&& not (y = []) && List.hd x < List.hd y && φ y (List.tl x) a
==> φ y x a).

3 nontautological subgoals.

Subgoal 3:

H0. not ((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []))
H1. not ((List.hd y <= List.hd x && not (y = [])) && not (x = []))
|---------------------------------------------------------------------------
num_occurs a (merge x y) = num_occurs a x + num_occurs a y

This simplifies, using the definition of merge to the following 3 subgoals:

Subgoal 3.3:

H0. y = []
H1. x <> []
|---------------------------------------------------------------------------
C0. List.hd y <= List.hd x
C1. 0 = num_occurs a y

But simplification reduces this to true, using the definition of num_occurs.

Subgoal 3.2:

H0. y = []
H1. List.hd y <= List.hd x
H2. x <> []
|---------------------------------------------------------------------------
0 = num_occurs a y

But simplification reduces this to true, using the definition of num_occurs.

Subgoal 3.1:

H0. x = []
|---------------------------------------------------------------------------
0 = num_occurs a x

But simplification reduces this to true, using the definition of num_occurs.

Subgoal 2:

H0. not (x = [])
H1. not (y = [])
H2. List.hd y <= List.hd x
H3. num_occurs a (merge x (List.tl y)) =
num_occurs a x + num_occurs a (List.tl y)
|---------------------------------------------------------------------------
num_occurs a (merge x y) = num_occurs a x + num_occurs a y

But simplification reduces this to true, using the definitions of merge and
num_occurs.

Subgoal 1:

H0. not (x = [])
H1. not (y = [])
H2. not (List.hd y <= List.hd x)
H3. num_occurs a (merge (List.tl x) y) =
num_occurs a (List.tl x) + num_occurs a y
|---------------------------------------------------------------------------
num_occurs a (merge x y) = num_occurs a x + num_occurs a y

But simplification reduces this to true, using the definitions of merge and
num_occurs.

ⓘ  Rules:
(:def merge)
(:def num_occurs)
(:induct merge)


Proved
proof
 ground_instances 0 definitions 10 inductions 1 search_time 0.188s
Expand
• start[0.188s, "Goal"]
num_occurs :var_0: (merge :var_1: :var_2:) =
num_occurs :var_0: :var_1: + num_occurs :var_0: :var_2:
• #### subproof

num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• start[0.187s, "1"] num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• induction on (functional merge)
:scheme (not (List.hd x < List.hd y && not (y = []) && not (x = []))
&& not (not (List.hd x < List.hd y) && not (y = []) && not (x = []))
==> φ y x a)
&& (not (x = [])
&& not (y = [])
&& not (List.hd x < List.hd y) && φ (List.tl y) x a
==> φ y x a)
&& (not (x = [])
&& not (y = []) && List.hd x < List.hd y && φ y (List.tl x) a
==> φ y x a)
• Split (((not
(not
((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []))
&& not ((List.hd y <= List.hd x && not (y = [])) && not (x = [])))
|| num_occurs a (merge x y) = num_occurs a x + num_occurs a y)
&& (not
(((not (x = []) && not (y = [])) && List.hd y <= List.hd x)
&& num_occurs a (merge x (List.tl y)) =
num_occurs a x + num_occurs a (List.tl y))
|| num_occurs a (merge x y) = num_occurs a x + num_occurs a y))
&& (not
(((not (x = []) && not (y = [])) && not (List.hd y <= List.hd x))
&& num_occurs a (merge (List.tl x) y) =
num_occurs a (List.tl x) + num_occurs a y)
|| num_occurs a (merge x y) = num_occurs a x + num_occurs a y)
:cases [((not (List.hd y <= List.hd x) && not (y = []))
&& not (x = [])
|| (List.hd y <= List.hd x && not (y = [])) && not (x = []))
|| num_occurs a (merge x y) = num_occurs a x + num_occurs a y;
(((x = [] || y = []) || not (List.hd y <= List.hd x))
|| not
(num_occurs a (merge x (List.tl y)) =
num_occurs a x + num_occurs a (List.tl y)))
|| num_occurs a (merge x y) = num_occurs a x + num_occurs a y;
(((x = [] || y = []) || List.hd y <= List.hd x)
|| not
(num_occurs a (merge (List.tl x) y) =
num_occurs a (List.tl x) + num_occurs a y))
|| num_occurs a (merge x y) = num_occurs a x + num_occurs a y])
• ##### subproof
(((x = [] || y = []) || List.hd y <= List.hd x) || not (num_occurs a (merge (List.tl x) y) = num_occurs a (List.tl x) + num_occurs a y)) || num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• start[0.186s, "1"]
(((x = [] || y = []) || List.hd y <= List.hd x)
|| not
(num_occurs a (merge (List.tl x) y) =
num_occurs a (List.tl x) + num_occurs a y))
|| num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• ###### simplify
 into true expansions [num_occurs, num_occurs, merge] rewrite_steps forward_chaining
• ##### subproof
(((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (num_occurs a (merge x (List.tl y)) = num_occurs a x + num_occurs a (List.tl y))) || num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• start[0.186s, "2"]
(((x = [] || y = []) || not (List.hd y <= List.hd x))
|| not
(num_occurs a (merge x (List.tl y)) =
num_occurs a x + num_occurs a (List.tl y)))
|| num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• ###### simplify
 into true expansions [num_occurs, num_occurs, merge] rewrite_steps forward_chaining
• ##### subproof
((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []) || (List.hd y <= List.hd x && not (y = [])) && not (x = [])) || num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• start[0.186s, "3"]
((not (List.hd y <= List.hd x) && not (y = [])) && not (x = [])
|| (List.hd y <= List.hd x && not (y = [])) && not (x = []))
|| num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• ###### simplify
 into ((((not (y = []) || List.hd y <= List.hd x) || 0 = num_occurs a y) || x = []) && (((not (y = []) || not (List.hd y <= List.hd x)) || 0 = num_occurs a y) || x = [])) && (0 = num_occurs a x || not (x = [])) expansions merge rewrite_steps forward_chaining
• Subproof
• Subproof
• Subproof
In :
theorem num_occurs_arith (x : int list) (a : int) =
x <> [] && List.tl x <> []
==>
num_occurs a (odds (List.tl x))
=
num_occurs a x - num_occurs a (odds x)
[@@induct functional num_occurs]
[@@rewrite]

Out:
val num_occurs_arith : int list -> int -> bool = <fun>
Goal:

x <> [] && List.tl x <> []
==> num_occurs a (odds (List.tl x)) = num_occurs a x - num_occurs a (odds x).

1 nontautological subgoal.

We shall induct according to a scheme derived from num_occurs.

Induction scheme:

(not ((x <> [] && List.hd x = a) && not (x = []))
&& not (not (x <> [] && List.hd x = a) && not (x = [])) ==> φ a x)
&& (not (x = []) && not (x <> [] && List.hd x = a) && φ a (List.tl x)
==> φ a x)
&& (not (x = []) && (x <> [] && List.hd x = a) && φ a (List.tl x)
==> φ a x).

3 nontautological subgoals.

Subgoal 3:

H0. not ((x <> [] && List.hd x = a) && not (x = []))
H1. not (not (x <> [] && List.hd x = a) && not (x = []))
H2. not (x = [])
H3. not (List.tl x = [])
|---------------------------------------------------------------------------
num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x)

But simplification reduces this to true.

Subgoal 2:

H0. not (x = [])
H1. not (x <> [] && List.hd x = a)
H2. not (List.tl x = []) && not (List.tl (List.tl x) = [])
==> num_occurs a (odds (List.tl (List.tl x))) =
num_occurs a (List.tl x) + -1 * num_occurs a (odds (List.tl x))
H3. not (x = [])
H4. not (List.tl x = [])
|---------------------------------------------------------------------------
num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x)

This simplifies, using the definitions of num_occurs and odds to the
following 3 subgoals:

Subgoal 2.3:

H0. x <> []
H1. num_occurs a (odds (List.tl (List.tl x))) =
num_occurs a (List.tl (List.tl x))
+ -1 * num_occurs a (odds (List.tl x))
H2. (List.tl (List.tl x)) <> []
H3. (List.tl x) <> []
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. List.hd (List.tl x) = a
C2. num_occurs a (odds (List.tl x)) =
num_occurs a (List.tl x)
+ -1 * num_occurs a (odds (List.tl (List.tl x)))

But simplification reduces this to true, using the definition of num_occurs.

Subgoal 2.2:

H0. x <> []
H1. num_occurs a (odds (List.tl (List.tl x))) =
(1 + num_occurs a (List.tl (List.tl x)))
+ -1 * num_occurs a (odds (List.tl x))
H2. (List.tl (List.tl x)) <> []
H3. List.hd (List.tl x) = a
H4. (List.tl x) <> []
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. num_occurs a (odds (List.tl x)) =
num_occurs a (List.tl x)
+ -1 * num_occurs a (odds (List.tl (List.tl x)))

But simplification reduces this to true, using the definition of num_occurs.

Subgoal 2.1:

H0. x <> []
H1. List.tl (List.tl x) = []
H2. (List.tl x) <> []
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. num_occurs a (odds (List.tl x)) =
num_occurs a (List.tl x)
+ -1 * num_occurs a (odds (List.tl (List.tl x)))

But simplification reduces this to true, using the definitions of num_occurs
and odds.

Subgoal 1:

H0. not (x = [])
H1. x <> []
H2. List.hd x = a
H3. not (List.tl x = []) && not (List.tl (List.tl x) = [])
==> num_occurs a (odds (List.tl (List.tl x))) =
num_occurs a (List.tl x) + -1 * num_occurs a (odds (List.tl x))
H4. not (x = [])
H5. not (List.tl x = [])
|---------------------------------------------------------------------------
num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x)

This simplifies, using the definitions of num_occurs and odds to the
following 3 subgoals:

Subgoal 1.3:

H0. x <> []
H1. num_occurs (List.hd x) (odds (List.tl (List.tl x))) =
num_occurs (List.hd x) (List.tl (List.tl x))
+ -1 * num_occurs (List.hd x) (odds (List.tl x))
H2. (List.tl (List.tl x)) <> []
H3. (List.tl x) <> []
|---------------------------------------------------------------------------
C0. List.hd (List.tl x) = List.hd x
C1. num_occurs (List.hd x) (odds (List.tl x)) =
num_occurs (List.hd x) (List.tl x)
+ -1 * num_occurs (List.hd x) (odds (List.tl (List.tl x)))

But simplification reduces this to true, using the definition of num_occurs.

Subgoal 1.2:

H0. x <> []
H1. num_occurs (List.hd x) (odds (List.tl (List.tl x))) =
(1 + num_occurs (List.hd x) (List.tl (List.tl x)))
+ -1 * num_occurs (List.hd x) (odds (List.tl x))
H2. (List.tl (List.tl x)) <> []
H3. List.hd (List.tl x) = List.hd x
H4. (List.tl x) <> []
|---------------------------------------------------------------------------
num_occurs (List.hd x) (odds (List.tl x)) =
num_occurs (List.hd x) (List.tl x)
+ -1 * num_occurs (List.hd x) (odds (List.tl (List.tl x)))

But simplification reduces this to true, using the definition of num_occurs.

Subgoal 1.1:

H0. x <> []
H1. List.tl (List.tl x) = []
H2. (List.tl x) <> []
|---------------------------------------------------------------------------
num_occurs (List.hd x) (odds (List.tl x)) =
num_occurs (List.hd x) (List.tl x)
+ -1 * num_occurs (List.hd x) (odds (List.tl (List.tl x)))

But simplification reduces this to true, using the definitions of num_occurs
and odds.

ⓘ  Rules:
(:def num_occurs)
(:def odds)
(:induct num_occurs)


Proved
proof
 ground_instances 0 definitions 26 inductions 1 search_time 0.499s
Expand
• start[0.499s, "Goal"]
not (:var_0: = []) && not (List.tl :var_0: = [])
==> num_occurs :var_1: (odds (List.tl :var_0:)) =
num_occurs :var_1: :var_0: - num_occurs :var_1: (odds :var_0:)
• #### subproof

(x = [] || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x)
• start[0.498s, "1"]
(x = [] || List.tl x = [])
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x)
• induction on (functional num_occurs)
:scheme (not ((x <> [] && List.hd x = a) && not (x = []))
&& not (not (x <> [] && List.hd x = a) && not (x = [])) ==>
φ a x)
&& (not (x = [])
&& not (x <> [] && List.hd x = a) && φ a (List.tl x) ==>
φ a x)
&& (not (x = []) && (x <> [] && List.hd x = a) && φ a (List.tl x)
==> φ a x)
• Split ((((not
(not ((x <> [] && List.hd x = a) && not (x = []))
&& not (not (x <> [] && List.hd x = a) && not (x = [])))
|| not (not (x = []) && not (List.tl x = [])))
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x))
&& ((not
((not (x = []) && not (x <> [] && List.hd x = a))
&& (not
(not (List.tl x = []) && not (List.tl (List.tl x) = []))
|| num_occurs a (odds (List.tl (List.tl x))) =
num_occurs a (List.tl x)
+ -1 * num_occurs a (odds (List.tl x))))
|| not (not (x = []) && not (List.tl x = [])))
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x)))
&& ((not
(((not (x = []) && x <> []) && List.hd x = a)
&& (not (not (List.tl x = []) && not (List.tl (List.tl x) = []))
|| num_occurs a (odds (List.tl (List.tl x))) =
num_occurs a (List.tl x)
+ -1 * num_occurs a (odds (List.tl x))))
|| not (not (x = []) && not (List.tl x = [])))
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x))
:cases [((((x <> [] && List.hd x = a) && not (x = [])
|| not (x <> [] && List.hd x = a) && not (x = []))
|| x = [])
|| List.tl x = [])
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x);
(((x = [] || x <> [] && List.hd x = a)
|| not
(not
(not (List.tl x = []) && not (List.tl (List.tl x) = []))
|| num_occurs a (odds (List.tl (List.tl x))) =
num_occurs a (List.tl x)
+ -1 * num_occurs a (odds (List.tl x))))
|| List.tl x = [])
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x);
((((x = [] || not (x <> [])) || not (List.hd x = a))
|| not
(not
(not (List.tl x = []) && not (List.tl (List.tl x) = []))
|| num_occurs a (odds (List.tl (List.tl x))) =
num_occurs a (List.tl x)
+ -1 * num_occurs a (odds (List.tl x))))
|| List.tl x = [])
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x)])
• ##### subproof
((((x = [] || not (x <> [])) || not (List.hd x = a)) || not (not (not (List.tl x = []) && not (List.tl (List.tl x) = [])) || num_occurs a (odds (List.tl (List.tl x))) = num_occurs a (List.tl x) + -1 * num_occurs a (odds (List.tl x)))) || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x)
• start[0.496s, "1"]
((((x = [] || not (x <> [])) || not (List.hd x = a))
|| not
(not (not (List.tl x = []) && not (List.tl (List.tl x) = []))
|| num_occurs a (odds (List.tl (List.tl x))) =
num_occurs a (List.tl x) + -1 * num_occurs a (odds (List.tl x))))
|| List.tl x = [])
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x)
• ###### simplify
 into ((((((x = [] || not (num_occurs (List.hd x) (odds (List.tl (List.tl x))) = num_occurs (List.hd x) (List.tl (List.tl x)) + -1 * num_occurs (List.hd x) (odds (List.tl x)))) || List.tl (List.tl x) = []) || List.hd (List.tl x) = List.hd x) || List.tl x = []) || num_occurs (List.hd x) (odds (List.tl x)) = num_occurs (List.hd x) (List.tl x) + -1 * num_occurs (List.hd x) (odds (List.tl (List.tl x)))) && (((((x = [] || not (num_occurs (List.hd x) (odds (List.tl (List.tl x))) = (1 + num_occurs (List.hd x) (List.tl (List.tl x))) + -1 * num_occurs (List.hd x) (odds (List.tl x)))) || List.tl (List.tl x) = []) || not (List.hd (List.tl x) = List.hd x)) || List.tl x = []) || num_occurs (List.hd x) (odds (List.tl x)) = num_occurs (List.hd x) (List.tl x) + -1 * num_occurs (List.hd x) (odds (List.tl (List.tl x))))) && (((x = [] || not (List.tl (List.tl x) = [])) || List.tl x = []) || num_occurs (List.hd x) (odds (List.tl x)) = num_occurs (List.hd x) (List.tl x) + -1 * num_occurs (List.hd x) (odds (List.tl (List.tl x)))) expansions [num_occurs, num_occurs, odds, num_occurs] rewrite_steps forward_chaining
• Subproof
• Subproof
• Subproof
• ##### subproof
(((x = [] || x <> [] && List.hd x = a) || not (not (not (List.tl x = []) && not (List.tl (List.tl x) = [])) || num_occurs a (odds (List.tl (List.tl x))) = num_occurs a (List.tl x) + -1 * num_occurs a (odds (List.tl x)))) || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x)
• start[0.496s, "2"]
(((x = [] || x <> [] && List.hd x = a)
|| not
(not (not (List.tl x = []) && not (List.tl (List.tl x) = []))
|| num_occurs a (odds (List.tl (List.tl x))) =
num_occurs a (List.tl x) + -1 * num_occurs a (odds (List.tl x))))
|| List.tl x = [])
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x)
• ###### simplify
 into (((((((x = [] || List.hd x = a) || not (num_occurs a (odds (List.tl (List.tl x))) = num_occurs a (List.tl (List.tl x)) + -1 * num_occurs a (odds (List.tl x)))) || List.tl (List.tl x) = []) || List.hd (List.tl x) = a) || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a (List.tl x) + -1 * num_occurs a (odds (List.tl (List.tl x)))) && ((((((x = [] || List.hd x = a) || not (num_occurs a (odds (List.tl (List.tl x))) = (1 + num_occurs a (List.tl (List.tl x))) + -1 * num_occurs a (odds (List.tl x)))) || List.tl (List.tl x) = []) || not (List.hd (List.tl x) = a)) || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a (List.tl x) + -1 * num_occurs a (odds (List.tl (List.tl x))))) && ((((x = [] || List.hd x = a) || not (List.tl (List.tl x) = [])) || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a (List.tl x) + -1 * num_occurs a (odds (List.tl (List.tl x)))) expansions [num_occurs, num_occurs, odds, num_occurs] rewrite_steps forward_chaining
• Subproof
• Subproof
• Subproof
• ##### subproof
((((x <> [] && List.hd x = a) && not (x = []) || not (x <> [] && List.hd x = a) && not (x = [])) || x = []) || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x)
• start[0.496s, "3"]
((((x <> [] && List.hd x = a) && not (x = [])
|| not (x <> [] && List.hd x = a) && not (x = []))
|| x = [])
|| List.tl x = [])
|| num_occurs a (odds (List.tl x)) =
num_occurs a x + -1 * num_occurs a (odds x)
• ###### simplify
 into true expansions [] rewrite_steps forward_chaining

Finally, let's put the pieces together and prove our main remaining theorem.

And now, our second main theorem at last:

In :
theorem merge_sort_elements a (x : int list) =
num_occurs a x = num_occurs a (merge_sort x)
[@@induct functional merge_sort]

Out:
val merge_sort_elements : int -> int list -> bool = <fun>
Goal:

num_occurs a x = num_occurs a (merge_sort x).

1 nontautological subgoal.

We shall induct according to a scheme derived from merge_sort.

Induction scheme:

(not (not (x <> [] && List.tl x = []) && not (x = [])) ==> φ x a)
&& (not (x = [])
&& not (x <> [] && List.tl x = [])
&& φ (odds (List.tl x)) a && φ (odds x) a
==> φ x a).

2 nontautological subgoals.

Subgoal 2:

|---------------------------------------------------------------------------
C0. not (x <> [] && List.tl x = []) && not (x = [])
C1. num_occurs a x = num_occurs a (merge_sort x)

But simplification reduces this to true, using the definitions of merge_sort
and num_occurs.

Subgoal 1:

H0. not (x = [])
H1. not (x <> [] && List.tl x = [])
H2. num_occurs a (odds (List.tl x)) =
num_occurs a (merge_sort (odds (List.tl x)))
H3. num_occurs a (odds x) = num_occurs a (merge_sort (odds x))
|---------------------------------------------------------------------------
num_occurs a x = num_occurs a (merge_sort x)

This simplifies, using the definitions of merge_sort and num_occurs, and the
rewrite rule num_occurs_arith to the following 2 subgoals:

Subgoal 1.2:

H0. x <> []
H1. (List.tl x) <> []
H2. num_occurs a (List.tl x) + -1 * num_occurs a (odds x) =
num_occurs a (merge_sort (odds (List.tl x)))
H3. num_occurs a (odds x) = num_occurs a (merge_sort (odds x))
|---------------------------------------------------------------------------
C0. num_occurs a (List.tl x) =
num_occurs a
(merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))
C1. List.hd x = a

But simplification reduces this to true, using the rewrite rule
num_occur_merge.

Subgoal 1.1:

H0. x <> []
H1. (List.tl x) <> []
H2. num_occurs a (List.tl x) + -1 * num_occurs a (odds x) =
-1 + num_occurs a (merge_sort (odds (List.tl x)))
H3. num_occurs a (odds x) = num_occurs a (merge_sort (odds x))
H4. List.hd x = a
|---------------------------------------------------------------------------
num_occurs a (List.tl x) =
-1
+ num_occurs a (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))

But simplification reduces this to true, using the rewrite rule
num_occur_merge.

ⓘ  Rules:
(:def merge_sort)
(:def num_occurs)
(:rw num_occur_merge)
(:rw num_occurs_arith)
(:induct merge_sort)


Proved
proof
 ground_instances 0 definitions 15 inductions 1 search_time 5.452s
Expand
• start[5.452s, "Goal"]
num_occurs :var_0: :var_1: = num_occurs :var_0: (merge_sort :var_1:)
• #### subproof

num_occurs a x = num_occurs a (merge_sort x)
• start[5.452s, "1"] num_occurs a x = num_occurs a (merge_sort x)
• induction on (functional merge_sort)
:scheme (not (not (x <> [] && List.tl x = []) && not (x = [])) ==> φ x a)
&& (not (x = [])
&& not (x <> [] && List.tl x = [])
&& φ (odds (List.tl x)) a && φ (odds x) a
==> φ x a)
• Split ((not (x <> [] && List.tl x = []) && not (x = [])
|| num_occurs a x = num_occurs a (merge_sort x))
&& (not
(((not (x = []) && not (x <> [] && List.tl x = []))
&& num_occurs a (odds (List.tl x)) =
num_occurs a (merge_sort (odds (List.tl x))))
&& num_occurs a (odds x) = num_occurs a (merge_sort (odds x)))
|| num_occurs a x = num_occurs a (merge_sort x))
:cases [not (x <> [] && List.tl x = []) && not (x = [])
|| num_occurs a x = num_occurs a (merge_sort x);
(((x = [] || x <> [] && List.tl x = [])
|| not
(num_occurs a (odds (List.tl x)) =
num_occurs a (merge_sort (odds (List.tl x)))))
|| not
(num_occurs a (odds x) =
num_occurs a (merge_sort (odds x))))
|| num_occurs a x = num_occurs a (merge_sort x)])
• ##### subproof
(((x = [] || x <> [] && List.tl x = []) || not (num_occurs a (odds (List.tl x)) = num_occurs a (merge_sort (odds (List.tl x))))) || not (num_occurs a (odds x) = num_occurs a (merge_sort (odds x)))) || num_occurs a x = num_occurs a (merge_sort x)
• start[5.451s, "1"]
(((x = [] || x <> [] && List.tl x = [])
|| not
(num_occurs a (odds (List.tl x)) =
num_occurs a (merge_sort (odds (List.tl x)))))
|| not (num_occurs a (odds x) = num_occurs a (merge_sort (odds x))))
|| num_occurs a x = num_occurs a (merge_sort x)
• ###### simplify
 into (((((x = [] || List.tl x = []) || not (num_occurs a (List.tl x) + -1 * num_occurs a (odds x) = num_occurs a (merge_sort (odds (List.tl x))))) || not (num_occurs a (odds x) = num_occurs a (merge_sort (odds x)))) || num_occurs a (List.tl x) = num_occurs a (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))) || List.hd x = a) && (((((x = [] || List.tl x = []) || not (num_occurs a (List.tl x) + -1 * num_occurs a (odds x) = -1 + num_occurs a (merge_sort (odds (List.tl x))))) || not (num_occurs a (odds x) = num_occurs a (merge_sort (odds x)))) || num_occurs a (List.tl x) = -1 + num_occurs a (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))) || not (List.hd x = a)) expansions [num_occurs, num_occurs, merge_sort, num_occurs] rewrite_steps num_occurs_arithnum_occurs_arith forward_chaining
• Subproof
• Subproof
• ##### subproof
not (x <> [] && List.tl x = []) && not (x = []) || num_occurs a x = num_occurs a (merge_sort x)
• start[5.451s, "2"]
not (x <> [] && List.tl x = []) && not (x = [])
|| num_occurs a x = num_occurs a (merge_sort x)
• ###### simplify
 into true expansions [num_occurs, merge_sort, num_occurs, num_occurs, merge_sort, num_occurs, num_occurs, num_occurs, num_occurs, merge_sort, num_occurs] rewrite_steps forward_chaining

So now we're sure merge_sort really is a proper sorting function.

# Merge Sort is Correct!¶

To recap, we've proved:

theorem merge_sort_sorts x =
is_sorted (merge_sort x)


and

theorem merge_sort_elements a (x : int list) =
num_occurs a x = num_occurs a (merge_sort x)


Beautiful! Happy proving (and sorting)!