# Welcome to Imandra!¶

Imandra is both a programming language and a reasoning engine with which you can analyse and verify properties of your programs.

As a programming language, Imandra is a subset of the functional language OCaml. We call this subset of OCaml “IML” or “ImandraML” (for “Imandra Modelling Language”).

With Imandra, you write your code and verification goals in the same language, and pursue programming and reasoning together.

Imandra has many advanced features, including first-class computable counterexamples, symbolic model checking, support for polymorphic higher-order recursive functions, automated induction, a powerful simplifier and symbolic execution engine with lemma-based conditional rewriting and forward-chaining, first-class state-space decompositions, decision procedures for algebraic datatypes, floating point arithmetic, and much more.

Before starting to use Imandra, it may be helpful to read this short Introduction.

This section will give you a quick, 5 minute overview of what Imandra can do. If you want to play around with the code in any of the examples hit the 'Try this!' buttons throughout, and you'll get a Jupyter notebook session where you can experiment. (If you got here via try.imandra.ai, you're already in one of these notebook sessions - if that's the case just run the cells using the Jupyter controls!)

## Your first proof and counterexample¶

Let's define a couple of simple arithmetic functions and analyse them with Imandra:

In [1]:
let g x =
if x > 22 then 9
else 100 + x

let f x =
if x > 99 then
100
else if x < 70 && x > 23
then 89 + x
else if x > 20
then g x + 20
else if x > -2 then
103
else 99

Out[1]:
val g : Z.t -> Z.t = <fun>
val f : Z.t -> Z.t = <fun>


Here, g and f are the names of our functions, and they each take a single integer argument x. In Imandra,

let g x = <body>

is the equivalent of something like

function g (x : Int) { <body> }

in many other languages.

Notice how we did not have to declare the type of x in the definition of f and g. Imandra's type system has inferred that x is an integer automatically from how x is used. Sometimes it's advantageous to annotate our definitions with types manually. We could write this explicitly by defining g with an explicit type annotation, e.g.,

let g (x : int) = <body>

As f and g are functions, we can of course compute with them:

In [2]:
g 5

Out[2]:
- : Z.t = 105

In [3]:
g 23017263820

Out[3]:
- : Z.t = 9

In [4]:
f (- 1)

Out[4]:
- : Z.t = 103


However, functions in Imandra are more than just code: they're also mathematical objects that can be analysed and subjected to the rigours of mathematical proof.

For example, let's verify that for all possible integer inputs x, g x never goes above 122, which corresponds to the logical statement (forall (x : int), g x <= 122). We represent logical statements like these with OCaml functions:

In [5]:
let g_upper_bound x =
g x <= 122

Out[5]:
val g_upper_bound : Z.t -> bool = <fun>


Now let's ask Imandra to verify our statement!

In [6]:
verify g_upper_bound

Out[6]:
- : Z.t -> bool = <fun>

Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.017s
details:
Expand
smt_stats:
 rlimit count: 32 num allocs: 5.6447e+06 time: 0.007 memory: 15.6 max memory: 15.6
Expand
• start[0.017s] (if ( :var_0: ) > 22 then 9 else 100 + ( :var_0: )) <= 122
• #### simplify

 into: true expansions: [] rewrite_steps: forward_chaining:
• Unsat

Imandra has verified this fact for us automatically, by directly examining the definition of our statement and the definitions of the other functions it refers to (in this case, g).

Now, let's ask Imandra to verify that there exists no x such that f x is equal to 158. Giving our statements names can sometimes be a bit unwieldy (although it can be helpfully descriptive in some situations). For simple statements like these, the statements themselves are descriptive enough, so we can also pass an anonymous function (a lambda term) to verify that represents our statement. In Imandra, we use fun to create an anonymous function:

In [7]:
verify (fun x -> f x <> 158)

Out[7]:
- : Z.t -> bool = <fun>
module CX : sig val x : Z.t end

Counterexample (after 0 steps, 0.017s):
let x : int = 69

Refuted
proof attempt
ground_instances:0
definitions:0
inductions:0
search_time:
0.017s
details:
Expand
smt_stats:
 num checks: 1 arith assert lower: 6 rlimit count: 677 mk clause: 28 mk bool var: 12 arith assert upper: 3 decisions: 2 propagations: 19 conflicts: 1 num allocs: 1.13248e+07 final checks: 1 time: 0.009 memory: 15.79 max memory: 16.1
Expand
• start[0.017s]
not
((if ( :var_0: ) > 99 then 100
else
if (( :var_0: ) < 70) && (( :var_0: ) > 23) then 89 + ( :var_0: )
else
if ( :var_0: ) > 20 then (if ( :var_0: ) > 22 then 9 else …) + 20
else if ( :var_0: ) > (-2) then 103 else 99)
= 158)
• #### simplify

 into: not ((( :var_0: ) <= 99) && ((if not (70 <= ( :var_0: )) && not (( :var_0: ) <= 23) then 89 + ( :var_0: ) else if ( :var_0: ) <= 20 then if ( :var_0: ) <= (-2) then 99 else 103 else 20 + (if ( :var_0: ) <= 22 then … else 9)) = 158)) expansions: [] rewrite_steps: forward_chaining:
• Sat (Some let x : int = (Z.of_nativeint (69n)) )

Imandra has found our statement to be false, and has also found us a concrete counterexample to demonstrate. Let's try executing f with that value to confirm:

In [8]:
f 69

Out[8]:
- : Z.t = 158


Imandra has derived for us that if x=69, then f x is equal to 158, so the conjecture (fun x -> f x <> 158) is not true! Imandra has given us a concrete counterexample refuting this conjecture.

In Imandra, all counterexamples are "first-class" values, and are automatically reflected into the runtime in a module (namespace) called CX. So, another way to experiment with that counterexample is to utilise the CX module that the verify command constructed for us:

In [9]:
CX.x

Out[9]:
- : Z.t = 69

In [10]:
f CX.x

Out[10]:
- : Z.t = 158


## Region Decomposition¶

We can also ask Imandra to decompose our function to get a symbolic representation of its state-space. This decomposes the (potentially infinite) state-space into a finite number of symbolically described regions, each describing a class of behaviours of the function.

For each region it is proved that if the inputs of the function satisfy the constraints, then the output of the function satisfies the invariant. Furthermore, Imandra proves coverage: every possible concrete behaviour of the function is represented by a region in the decomposition:

In [11]:
Modular_decomp.top "f"

Out[11]:
- : Modular_decomp_intf.decomp_ref = <abstr>

Regions details

No group selected.

• Concrete regions are numbered
• Unnumbered regions are groups whose children share a particular constraint
• Click on a region to view its details
• Double click on a region to zoom in on it
• Shift+double click to zoom out
• Hit escape to reset back to the top
decomp of (f x
Reg_idConstraintsInvariant
6
• x > 99
100
5
• x > 23
• x < 70
• not (x > 99)
89 + x
4
• not (x > 22)
• x > 20
• not (x > 23)
• x < 70
• not (x > 99)
120 + x
3
• x > 22
• x > 20
• not (x > 23)
• x < 70
• not (x > 99)
29
2
• x > (-2)
• not (x > 20)
• not (x > 23)
• x < 70
• not (x > 99)
103
1
• not (x > (-2))
• not (x > 20)
• not (x > 23)
• x < 70
• not (x > 99)
99
0
• x > 22
• x > 20
• not (x < 70)
• not (x > 99)
29

Click on the different full regions (those sub-diagrams of the Voronoi diagram starting with R) and inspect their constraints and invariant. Note that the invariant may depend on the input value (x), e.g., in regions corresponding to branches of the function f where it returns x plus some constant.

Region decompositions form the basis of many powerful Imandra features, including forms of reachability analysis and automated test-suite generation and auditing.

## Recursion and Induction¶

Imandra's reasoning power really shines in the analysis of recursive functions.

Let's define a simple recursive summation function, sum : int list -> int, and reason about it.

In [12]:
let rec sum x = match x with
| [] -> 0
| x :: xs -> x + sum xs

Out[12]:
val sum : Z.t list -> Z.t = <fun>

termination proof

### Termination proof

call sum (List.tl x) from sum x
original:sum x
sub:sum (List.tl x)
original ordinal:Ordinal.Int (_cnt x)
sub ordinal:Ordinal.Int (_cnt (List.tl x))
path:[x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.011s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 11 arith tableau max rows: 5 arith tableau max columns: 16 arith pivots: 9 rlimit count: 2210 mk clause: 21 datatype occurs check: 12 mk bool var: 75 arith assert upper: 12 datatype splits: 1 decisions: 18 arith row summations: 12 propagations: 24 conflicts: 10 arith fixed eqs: 5 datatype accessor ax: 10 arith conflicts: 2 arith num rows: 5 arith assert diseq: 1 datatype constructor ax: 9 num allocs: 1.86947e+07 final checks: 4 added eqs: 49 del clause: 11 arith eq adapter: 12 memory: 16.3 max memory: 16.3
Expand
• start[0.011s]
let (_x_0 : int) = count.list mk_nat x in
let (_x_1 : int list) = List.tl x in
let (_x_2 : int) = count.list mk_nat _x_1 in
x <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
==> not (_x_1 <> [])
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int list) = List.tl x in let (_x_1 : int) = count.list mk_nat _x_0 in let (_x_2 : int) = count.list mk_nat x in not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (x <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_393/server| (|get.::.1_381/server|… expansions:
• unroll
 expr: (|count.list_393/server| (|get.::.1_381/server| x_382/server)) expansions:
• unroll
 expr: (|count.list_393/server| x_382/server) expansions:
• Unsat
In [13]:
sum []

Out[13]:
- : Z.t = 0

In [14]:
sum [1;2;3]

Out[14]:
- : Z.t = 6


We can ask Imandra lots of interesting questions about our functions. For example, we can use Imandra's instance command to ask Imandra to "solve" for inputs satisfying various constraints:

In [15]:
instance (fun x -> List.length x >= 10 && sum x = List.length x + 17)

Out[15]:
- : Z.t list -> bool = <fun>
module CX : sig val x : Z.t list end

Instance (after 22 steps, 0.025s):
let x : int list =
[(-30577); 8365; 609; 281; 8945; 974; 5904; 2240; 2446; 840]

Instance
proof attempt
ground_instances:22
definitions:0
inductions:0
search_time:
0.025s
details:
Expand
smt_stats:
 arith offset eqs: 20 num checks: 45 arith assert lower: 132 arith tableau max rows: 44 arith tableau max columns: 82 arith pivots: 106 rlimit count: 36840 mk clause: 230 datatype occurs check: 80 mk bool var: 729 arith assert upper: 109 datatype splits: 20 decisions: 227 arith row summations: 962 propagations: 261 interface eqs: 18 conflicts: 46 arith fixed eqs: 89 arith assume eqs: 18 datatype accessor ax: 40 minimized lits: 1 arith conflicts: 20 arith num rows: 44 arith assert diseq: 22 datatype constructor ax: 91 num allocs: 2.81952e+07 final checks: 61 added eqs: 734 del clause: 222 arith eq adapter: 144 memory: 17.07 max memory: 17.07
Expand
• start[0.025s]
let (_x_0 : int) = List.length ( :var_0: ) in
(_x_0 >= 10) && (sum ( :var_0: ) = _x_0 + 17)
• #### simplify

 into: let (_x_0 : int) = List.length ( :var_0: ) in (_x_0 >= 10) && (sum ( :var_0: ) = 17 + _x_0) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|List.length_425/server| x_1270/client) expansions:
• unroll
 expr: (sum_1266/client x_1270/client) expansions:
• unroll
 expr: (|List.length_425/server| (|get.::.1_424/server| x_1270/client)) expansions:
• unroll
 expr: (sum_1266/client (|get.::.1_424/server| x_1270/client)) expansions:
• unroll
 expr: (|List.length_425/server| (|get.::.1_424/server| (|get.::.1_424/server| x_1270/client))) expansions:
• unroll
 expr: (sum_1266/client (|get.::.1_424/server| (|get.::.1_424/server| x_1270/client))) expansions:
• unroll
 expr: (|List.length_425/server| (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/server|… expansions:
• unroll
 expr: (sum_1266/client (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/ser… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_424/server| (|get.::.1_424/server| (|get.::.1_424/… expansions:
• Sat (Some let x : int list = [(Z.of_nativeint (-30577n)); (Z.of_nativeint (8365n)); (Z.of_nativeint (609n)); (Z.of_nativeint (281n)); (Z.of_nativeint (8945n)); (Z.of_nativeint (974n)); (Z.of_nativeint (5904n)); (Z.of_nativeint (2240n)); (Z.of_nativeint (2446n)); (Z.of_nativeint (840n))] )

We can compute with this synthesized instance, as Imandra installs it in the CX module:

In [16]:
List.length CX.x

Out[16]:
- : Z.t = 10

In [17]:
sum CX.x

Out[17]:
- : Z.t = 27


Now, let's ask Imandra to prove a conjecture we have about sum.

For example, is it always the case that sum x >= 0?

In [18]:
verify (fun x -> sum x >= 0)

Out[18]:
- : Z.t list -> bool = <fun>
module CX : sig val x : Z.t list end

Counterexample (after 2 steps, 0.009s):
let x : int list = [(-1)]

Refuted
proof attempt
ground_instances:2
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 arith offset eqs: 2 num checks: 5 arith assert lower: 2 arith tableau max rows: 3 arith tableau max columns: 10 arith pivots: 2 rlimit count: 765 mk clause: 8 datatype occurs check: 3 mk bool var: 34 arith assert upper: 4 datatype splits: 1 decisions: 3 arith row summations: 2 propagations: 9 conflicts: 3 arith fixed eqs: 1 datatype accessor ax: 5 arith num rows: 3 arith assert diseq: 2 datatype constructor ax: 5 num allocs: 4.02877e+07 final checks: 4 added eqs: 29 del clause: 4 arith eq adapter: 5 memory: 17.02 max memory: 17.07
Expand
• start[0.009s] sum ( :var_0: ) >= 0
• unroll
 expr: (sum_1266/client x_1272/client) expansions:
• unroll
 expr: (sum_1266/client (|get.::.1_460/server| x_1272/client)) expansions:
• Sat (Some let x : int list = [(Z.of_nativeint (-1n))] )

Imandra tells us the (obvious) answer: This conjecture is false! Indeed, we can compute with the counterexample to see:

In [19]:
sum CX.x

Out[19]:
- : Z.t = -1


Ah, of course! How can we refine this conjecture to make it true? Well, we can add an additional hypothesis that every element of the list x is non-negative. Let's define a function psd to express this:

In [20]:
let psd = List.for_all (fun x -> x >= 0)

Out[20]:
val psd : Z.t list -> bool = <fun>


Now, let's ask Imandra to prove our improved conjecture:

In [21]:
verify (fun x -> psd x ==> sum x >= 0)

Out[21]:
- : Z.t list -> bool = <fun>

Unknown (Verified up to bound 100)
Expand
 expanded: List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))sum xList.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl x)))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))sum (List.tl x)sum (List.tl (List.tl (List.tl (List.tl x))))List.for_all anon_fun.psd.1 (List.tl (List.tl x))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))List.for_all anon_fun.psd.1 xsum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl x)List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl x))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl x)))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl x)))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl x)))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl x))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))) blocked: sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))))List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))))
proof attempt
 ground_instances: 100 definitions: 0 inductions: 0 search_time: 0.143s
Expand
• start[0.143s]
List.for_all anon_fun.psd.1 ( :var_0: ) ==> sum ( :var_0: ) >= 0
• #### simplify

 into: not (List.for_all anon_fun.psd.1 ( :var_0: )) || (sum ( :var_0: ) >= 0) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (sum_1266/client x_374/server) expansions:
• unroll
 expr: (|List.for_all_375/server| x_374/server) expansions:
• unroll
 expr: (sum_1266/client (|get.::.1_373/server| x_374/server)) expansions:
• unroll
 expr: (|List.for_all_375/server| (|get.::.1_373/server| x_374/server)) expansions:
• unroll
 expr: (sum_1266/client (|get.::.1_373/server| (|get.::.1_373/server| x_374/server))) expansions:
• unroll
 expr: (|List.for_all_375/server| (|get.::.1_373/server| (|get.::.1_373/server| x_374/server))) expansions:
• unroll
 expr: (sum_1266/client (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/ser… expansions:
• unroll
 expr: (|List.for_all_375/server| (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/server… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_373/server| (|get.::.1_373/server| (|get.::.1_373/… expansions:

When we gave this fact to Imandra, it attempted to prove it using a form of bounded model checking. As it turns out, this type of reasoning is not sufficient for establishing this conjecture. However, Imandra tells us something very useful: that up to its current recursion unrolling bound of 100, there exist no counterexamples to this conjecture.

For many practical problems, this type of bounded model checking establishing there exist no counterexamples up to depth k is sufficient. You may enjoy inspecting the call graph of this bounded verification to understand the structure of Imandra's state-space exploration.

But, we can do even better. We'll ask Imandra to prove this fact for all possible cases. To do this, we'll ask Imandra to use induction. In fact, Imandra has a powerful [@@auto] proof strategy which will apply induction automatically. Let's use it!

In [22]:
verify (fun x -> psd x ==> sum x >= 0) [@@auto]

Out[22]:
- : Z.t list -> bool = <fun>
Goal:

psd x ==> sum x >= 0.

1 nontautological subgoal.

Subgoal 1:

H0. List.for_all anon_fun.psd.1 x
|---------------------------------------------------------------------------
sum x >= 0

Must try induction.

The recursive terms in the conjecture suggest 2 inductions.
Subsumption and merging reduces this to 1.

We shall induct according to a scheme derived from List.for_all.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 1.2:

H0. List.for_all anon_fun.psd.1 x
|---------------------------------------------------------------------------
C0. x <> []
C1. sum x >= 0

But simplification reduces this to true, using the definitions of
List.for_all and sum.

Subgoal 1.1:

H0. x <> []
H1. List.for_all anon_fun.psd.1 (List.tl x) ==> sum (List.tl x) >= 0
H2. List.for_all anon_fun.psd.1 x
|---------------------------------------------------------------------------
sum x >= 0

But simplification reduces this to true, using the definitions of
List.for_all and sum.

ⓘ  Rules:
(:def List.for_all)
(:def sum)
(:induct List.for_all)


Proved
proof
 ground_instances: 0 definitions: 5 inductions: 1 search_time: 0.132s
Expand
• start[0.132s, "Goal"]
List.for_all anon_fun.psd.1 ( :var_0: ) ==> sum ( :var_0: ) >= 0
• #### subproof

not (List.for_all anon_fun.psd.1 x) || (sum x >= 0)
• start[0.132s, "1"] not (List.for_all anon_fun.psd.1 x) || (sum x >= 0)
• induction on (functional ?)
:scheme (not (x <> []) ==> φ x) && (x <> [] && φ (List.tl x) ==> φ x)
• Split (let (_x_0 : bool) = x <> [] in
let (_x_1 : bool) = sum x >= 0 in
let (_x_2 : bool) = not (List.for_all anon_fun.psd.1 x) in
let (_x_3 : int list) = List.tl x in
(_x_0 || _x_1 || _x_2)
&& (not
(_x_0
&& (not (List.for_all anon_fun.psd.1 _x_3) || (sum _x_3 >= 0)))
|| _x_1 || _x_2)
:cases [not (List.for_all anon_fun.psd.1 x) || x <> [] || (sum x >= 0);
let (_x_0 : int list) = List.tl x in
not (x <> [])
|| not (List.for_all anon_fun.psd.1 _x_0 ==> sum _x_0 >= 0)
|| not (List.for_all anon_fun.psd.1 x) || (sum x >= 0)])
• ##### subproof
let (_x_0 : int list) = List.tl x in not (x <> []) || not (List.for_all anon_fun.psd.1 _x_0 ==> sum _x_0 >= 0) || not (List.for_all anon_fun.psd.1 x) || (sum x >= 0)
• start[0.082s, "1.1"]
let (_x_0 : int list) = List.tl x in
not (x <> []) || not (List.for_all anon_fun.psd.1 _x_0 ==> sum _x_0 >= 0)
|| not (List.for_all anon_fun.psd.1 x) || (sum x >= 0)
• ###### simplify
 into: true expansions: [List.for_all, sum, List.for_all] rewrite_steps: forward_chaining:
• ##### subproof
not (List.for_all anon_fun.psd.1 x) || x <> [] || (sum x >= 0)
• start[0.082s, "1.2"]
not (List.for_all anon_fun.psd.1 x) || x <> [] || (sum x >= 0)
• ###### simplify
 into: true expansions: [sum, List.for_all] rewrite_steps: forward_chaining:

Excellent. Imandra has proved this property for us for all possible inputs automatically by induction.

We hope you enjoyed this quick introduction!