Welcome to Imandra!¶

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

Imandra scope

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:

Try this!

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:

Try this!

In [2]:

g 5

Out[2]:

- : Z.t = 105

Try this!

In [3]:

g 23017263820

Out[3]:

- : Z.t = 9

Try this!

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:

Try this!

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!

Try this!

In [6]:

verify g_upper_bound

Out[6]:

- : Z.t -> bool = <fun>

Proved

proof
call graph

proof

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.017s

details:

Expand

smt_stats:

rlimit count:	32
num allocs:	5644696
time:	0.007000
memory:	15.600000
max memory:	15.600000

Expand

start[0.017s] (if ( :var_0: ) > 22 then 9 else 100 + ( :var_0: )) <= 122

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

Loading..

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:

Try this!

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

call graph
proof

Loading..

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:	11324763
final checks:	1
time:	0.009000
memory:	15.790000
max memory:	16.100000

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)) )

digraph "proof" {
p_5 [label="Start (not\l       ((if ( :var_0: ) \> 99 then 100\l         else\l         if (( :var_0: ) \< 70) && (( :var_0: ) \> 23) then 89 + ( :var_0: )\l         else\l         if ( :var_0: ) \> 20 then (if ( :var_0: ) \> 22 then 9 else …) + 20\l         else if ( :var_0: ) \> (-2) then 103 else 99)\l        = 158)\l       :time 0.017s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_5 -> p_4 [label=""];
p_4 [label="Simplify (not\l          ((( :var_0: ) \<= 99)\l           && ((if not (70 \<= ( :var_0: )) && not (( :var_0: ) \<= 23)\l                then 89 + ( :var_0: )\l                else\l                if ( :var_0: ) \<= 20\l                then if ( :var_0: ) \<= (-2) then 99 else 103\l                else 20 + (if ( :var_0: ) \<= 22 then … else 9))\l               = 158))\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_4 -> p_3 [label=""];
p_3 [label="Sat (Some let x : int = (Z.of_nativeint (69n))\l)",shape=box,style=filled,fontname="courier",fontsize=14];
}

Loading..

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:

Try this!

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:

Try this!

In [9]:

CX.x

Out[9]:

- : Z.t = 69

Try this!

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:

Try this!

In [11]:

Modular_decomp.top "f"

Out[11]:

- : Modular_decomp_intf.decomp_ref = <abstr>

Voronoi (7 of 7)
Table

{
  "regions": [
    {
      "constraints": [ "x > 99" ],
      "region": { "constraints": [ "x > 99" ], "invariant": "F = 100" },
      "groups": [],
      "label": "7",
      "weight": 1
    },
    {
      "constraints": [ "x <= -2" ],
      "region": { "constraints": [ "x <= -2" ], "invariant": "F = 99" },
      "groups": [],
      "label": "6",
      "weight": 1
    },
    {
      "constraints": [ "70 <= x <= 99" ],
      "region": { "constraints": [ "70 <= x <= 99" ], "invariant": "F = 29" },
      "groups": [],
      "label": "5",
      "weight": 1
    },
    {
      "constraints": [ "23 < x < 70" ],
      "region": {
        "constraints": [ "23 < x < 70" ],
        "invariant": "F = x + 89"
      },
      "groups": [],
      "label": "4",
      "weight": 1
    },
    {
      "constraints": [ "22 < x <= 23" ],
      "region": { "constraints": [ "22 < x <= 23" ], "invariant": "F = 29" },
      "groups": [],
      "label": "3",
      "weight": 1
    },
    {
      "constraints": [ "20 < x <= 22" ],
      "region": {
        "constraints": [ "20 < x <= 22" ],
        "invariant": "F = x + 120"
      },
      "groups": [],
      "label": "2",
      "weight": 1
    },
    {
      "constraints": [ "-2 < x <= 20" ],
      "region": { "constraints": [ "-2 < x <= 20" ], "invariant": "F = 103" },
      "groups": [],
      "label": "1",
      "weight": 1
    }
  ]
}

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_id	Constraints	Invariant
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.

Try this!

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

summary
full

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:	18694685
final checks:	4
added eqs:	49
del clause:	11
arith eq adapter:	12
memory:	16.300000
max memory:	16.300000

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

Try this!

In [13]:

sum []

Out[13]:

- : Z.t = 0

Try this!

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:

Try this!

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

call graph
proof

digraph "call graph" {
goal [label="let (_x_0 : int) = List.length x in (_x_0 \>= 10) && (sum x = 17 + _x_0)",shape=box,style=filled,color="cyan",fontname="courier",fontsize=14];
goal -> call_20 [label="calls"];
goal -> call_16 [label="calls"];
call_20 [label="List.length x",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_20 -> call_107 [label="calls"];
call_16 [label="sum x",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_16 -> call_178 [label="calls"];
call_107 [label="List.length (List.tl x)",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_107 -> call_234 [label="calls"];
call_178 [label="sum (List.tl x)",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_178 -> call_308 [label="calls"];
call_234 [label="List.length (List.tl (List.tl x))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_234 -> call_409 [label="calls"];
call_308 [label="sum (List.tl (List.tl x))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_308 -> call_490 [label="calls"];
call_409 [label="List.length (List.tl (List.tl (List.tl x)))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_409 -> call_568 [label="calls"];
call_490 [label="sum (List.tl (List.tl (List.tl x)))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_490 -> call_635 [label="calls"];
call_568 [label="List.length (List.tl (List.tl (List.tl (List.tl x))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_568 -> call_711 [label="calls"];
call_635 [label="sum (List.tl (List.tl (List.tl (List.tl x))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_635 -> call_815 [label="calls"];
call_711 [label="List.length (List.tl (List.tl (List.tl (List.tl (List.tl x)))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_711 -> call_897 [label="calls"];
call_815 [label="sum (List.tl (List.tl (List.tl (List.tl (List.tl x)))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_815 -> call_962 [label="calls"];
call_897 [label="List.length (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_897 -> call_1042 [label="calls"];
call_962 [label="sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_962 -> call_1125 [label="calls"];
call_1042 [label="List.length\l(List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1042 -> call_1213 [label="calls"];
call_1125 [label="sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1125 -> call_1276 [label="calls"];
call_1213 [label="List.length\l(List.tl\l (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1213 -> call_1358 [label="calls"];
call_1276 [label="sum\l(List.tl\l (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1276 -> call_1337 [label="calls"];
call_1358 [label="List.length\l(List.tl\l (List.tl\l  (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1358 -> call_1510 [label="calls"];
call_1337 [label="sum\l(List.tl\l (List.tl\l  (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1337 -> call_1583 [label="calls"];
call_1510 [label="List.length\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1510 -> call_1680 [label="calls"];
call_1583 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1583 -> call_1654 [label="calls"];
call_1680 [label="List.length\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))",shape=box,style=filled,color="yellow",fontname="courier",fontsize=14];
call_1654 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))",shape=box,style=filled,color="yellow",fontname="courier",fontsize=14];
}

Loading..

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:	28195182
final checks:	61
added eqs:	734
del clause:	222
arith eq adapter:	144
memory:	17.070000
max memory:	17.070000

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))] )

digraph "proof" {
p_36 [label="Start (let (_x_0 : int) = List.length ( :var_0: ) in\l       (_x_0 \>= 10) && (sum ( :var_0: ) = _x_0 + 17) :time 0.025s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_36 -> p_35 [label=""];
p_35 [label="Simplify (let (_x_0 : int) = List.length ( :var_0: ) in\l          (_x_0 \>= 10) && (sum ( :var_0: ) = 17 + _x_0) :expansions [] \l          :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_35 -> p_34 [label=""];
p_34 [label="Unroll ([List.length x], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_34 -> p_33 [label=""];
p_33 [label="Unroll ([sum x], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_33 -> p_32 [label=""];
p_32 [label="Unroll ([List.length (List.tl x)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_32 -> p_31 [label=""];
p_31 [label="Unroll ([sum (List.tl x)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_31 -> p_30 [label=""];
p_30 [label="Unroll ([List.length (List.tl (List.tl x))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_30 -> p_29 [label=""];
p_29 [label="Unroll ([sum (List.tl (List.tl x))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_29 -> p_28 [label=""];
p_28 [label="Unroll ([List.length (List.tl (List.tl (List.tl x)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_28 -> p_27 [label=""];
p_27 [label="Unroll ([sum (List.tl (List.tl (List.tl x)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_27 -> p_26 [label=""];
p_26 [label="Unroll ([List.length (List.tl (List.tl (List.tl (List.tl x))))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_26 -> p_25 [label=""];
p_25 [label="Unroll ([sum (List.tl (List.tl (List.tl (List.tl x))))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_25 -> p_24 [label=""];
p_24 [label="Unroll ([List.length (List.tl (List.tl (List.tl (List.tl (List.tl x)))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_24 -> p_23 [label=""];
p_23 [label="Unroll ([sum (List.tl (List.tl (List.tl (List.tl (List.tl x)))))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_23 -> p_22 [label=""];
p_22 [label="Unroll ([List.length\l         (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_22 -> p_21 [label=""];
p_21 [label="Unroll ([sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_21 -> p_20 [label=""];
p_20 [label="Unroll ([List.length\l         (List.tl\l          (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_20 -> p_19 [label=""];
p_19 [label="Unroll ([sum\l         (List.tl\l          (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_19 -> p_18 [label=""];
p_18 [label="Unroll ([List.length\l         (List.tl\l          (List.tl\l           (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_18 -> p_17 [label=""];
p_17 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_17 -> p_16 [label=""];
p_16 [label="Unroll ([List.length\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_16 -> p_15 [label=""];
p_15 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_15 -> p_14 [label=""];
p_14 [label="Unroll ([List.length\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_14 -> p_13 [label=""];
p_13 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_13 -> p_12 [label=""];
p_12 [label="Sat (Some let x : int list =\l  [(Z.of_nativeint (-30577n)); (Z.of_nativeint (8365n));\l   (Z.of_nativeint (609n)); (Z.of_nativeint (281n));\l   (Z.of_nativeint (8945n)); (Z.of_nativeint (974n));\l   (Z.of_nativeint (5904n)); (Z.of_nativeint (2240n));\l   (Z.of_nativeint (2446n)); (Z.of_nativeint (840n))]\l)",shape=box,style=filled,fontname="courier",fontsize=14];
}

Loading..

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

Try this!

In [16]:

List.length CX.x

Out[16]:

- : Z.t = 10

Try this!

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?

Try this!

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

call graph
proof

Loading..

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:	40287651
final checks:	4
added eqs:	29
del clause:	4
arith eq adapter:	5
memory:	17.020000
max memory:	17.070000

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))] )

Loading..

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

Try this!

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:

Try 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:

Try this!

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 x
List.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 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 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))))))))))))))))))))))))))))))))))))))))))))))))))

digraph "call graph" {
goal [label="not (not (List.for_all anon_fun.psd.1 x) \|\| (sum x \>= 0))",shape=box,style=filled,color="cyan",fontname="courier",fontsize=14];
goal -> call_16 [label="calls"];
goal -> call_18 [label="calls"];
call_16 [label="List.for_all anon_fun.psd.1 x",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_16 -> call_172 [label="calls"];
call_18 [label="sum x",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_18 -> call_105 [label="calls"];
call_172 [label="List.for_all anon_fun.psd.1 (List.tl x)",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_172 -> call_386 [label="calls"];
call_105 [label="sum (List.tl x)",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_105 -> call_264 [label="calls"];
call_386 [label="List.for_all anon_fun.psd.1 (List.tl (List.tl x))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_386 -> call_575 [label="calls"];
call_264 [label="sum (List.tl (List.tl x))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_264 -> call_480 [label="calls"];
call_575 [label="List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl x)))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_575 -> call_764 [label="calls"];
call_480 [label="sum (List.tl (List.tl (List.tl x)))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_480 -> call_680 [label="calls"];
call_764 [label="List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl x))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_764 -> call_957 [label="calls"];
call_680 [label="sum (List.tl (List.tl (List.tl (List.tl x))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_680 -> call_875 [label="calls"];
call_957 [label="List.for_all anon_fun.psd.1\l(List.tl (List.tl (List.tl (List.tl (List.tl x)))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_957 -> call_1154 [label="calls"];
call_875 [label="sum (List.tl (List.tl (List.tl (List.tl (List.tl x)))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_875 -> call_1071 [label="calls"];
call_1154 [label="List.for_all anon_fun.psd.1\l(List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1154 -> call_1347 [label="calls"];
call_1071 [label="sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1071 -> call_1268 [label="calls"];
call_1347 [label="List.for_all anon_fun.psd.1\l(List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1347 -> call_1428 [label="calls"];
call_1268 [label="sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1268 -> call_1464 [label="calls"];
call_1428 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1428 -> call_1740 [label="calls"];
call_1464 [label="sum\l(List.tl\l (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1464 -> call_1660 [label="calls"];
call_1740 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1740 -> call_1931 [label="calls"];
call_1660 [label="sum\l(List.tl\l (List.tl\l  (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1660 -> call_1856 [label="calls"];
call_1931 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1931 -> call_2123 [label="calls"];
call_1856 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_1856 -> call_2052 [label="calls"];
call_2123 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2123 -> call_2323 [label="calls"];
call_2052 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2052 -> call_2247 [label="calls"];
call_2323 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2323 -> call_2520 [label="calls"];
call_2247 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2247 -> call_2449 [label="calls"];
call_2520 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2520 -> call_2721 [label="calls"];
call_2449 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2449 -> call_2649 [label="calls"];
call_2721 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2721 -> call_2926 [label="calls"];
call_2649 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2649 -> call_2850 [label="calls"];
call_2926 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2926 -> call_3123 [label="calls"];
call_2850 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_2850 -> call_3051 [label="calls"];
call_3123 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3123 -> call_3324 [label="calls"];
call_3051 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3051 -> call_3252 [label="calls"];
call_3324 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3324 -> call_3520 [label="calls"];
call_3252 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3252 -> call_3448 [label="calls"];
call_3520 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3520 -> call_3716 [label="calls"];
call_3448 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3448 -> call_3644 [label="calls"];
call_3716 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3716 -> call_3909 [label="calls"];
call_3644 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3644 -> call_3837 [label="calls"];
call_3909 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3909 -> call_4105 [label="calls"];
call_3837 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_3837 -> call_4033 [label="calls"];
call_4105 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4105 -> call_4301 [label="calls"];
call_4033 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4033 -> call_4229 [label="calls"];
call_4301 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4301 -> call_4497 [label="calls"];
call_4229 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4229 -> call_4425 [label="calls"];
call_4497 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4497 -> call_4697 [label="calls"];
call_4425 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4425 -> call_4621 [label="calls"];
call_4697 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4697 -> call_4893 [label="calls"];
call_4621 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4621 -> call_4817 [label="calls"];
call_4893 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4893 -> call_5089 [label="calls"];
call_4817 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_4817 -> call_5013 [label="calls"];
call_5089 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5089 -> call_5281 [label="calls"];
call_5013 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5013 -> call_5209 [label="calls"];
call_5281 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5281 -> call_5481 [label="calls"];
call_5209 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5209 -> call_5405 [label="calls"];
call_5481 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5481 -> call_5677 [label="calls"];
call_5405 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5405 -> call_5601 [label="calls"];
call_5677 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5677 -> call_5873 [label="calls"];
call_5601 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5601 -> call_5797 [label="calls"];
call_5873 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5873 -> call_6069 [label="calls"];
call_5797 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5797 -> call_5993 [label="calls"];
call_6069 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6069 -> call_6261 [label="calls"];
call_5993 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_5993 -> call_6194 [label="calls"];
call_6261 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6261 -> call_6457 [label="calls"];
call_6194 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6194 -> call_6385 [label="calls"];
call_6457 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6457 -> call_6653 [label="calls"];
call_6385 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6385 -> call_6581 [label="calls"];
call_6653 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6653 -> call_6849 [label="calls"];
call_6581 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6581 -> call_6777 [label="calls"];
call_6849 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6849 -> call_7045 [label="calls"];
call_6777 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6777 -> call_6973 [label="calls"];
call_7045 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_7045 -> call_7245 [label="calls"];
call_6973 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_6973 -> call_7169 [label="calls"];
call_7245 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_7245 -> call_7437 [label="calls"];
call_7169 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_7169 -> call_7365 [label="calls"];
call_7437 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_7437 -> call_7633 [label="calls"];
call_7365 [label="sum\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_7365 -> call_7561 [label="calls"];
call_7633 [label="List.for_all anon_fun.psd.1\l(List.tl\l (List.tl\l  (List.tl\l   (List.tl\l    (List.tl\l     (List.tl\l      (List.tl\l       (List.tl\l        (List.tl\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))",shape=box,style=filled,color="green",fontname="courier",fontsize=14];
call_7633 -> call_7833 [label="calls"];
call_7561 [label="\<…\> (skipped 11)",shape=box,style=filled,color="cyan",fontname="courier",fontsize=14];
call_7833 [label="\<…\> (skipped 10)",shape=box,style=filled,color="cyan",fontname="courier",fontsize=14];
}

Loading..

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:

digraph "proof" {
p_101 [label="Start (List.for_all anon_fun.psd.1 ( :var_0: ) ==\> sum ( :var_0: ) \>= 0\l       :time 0.143s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_101 -> p_100 [label=""];
p_100 [label="Simplify (not (List.for_all anon_fun.psd.1 ( :var_0: ))\l          \|\| (sum ( :var_0: ) \>= 0) :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_100 -> p_99 [label=""];
p_99 [label="Unroll ([sum x], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_99 -> p_98 [label=""];
p_98 [label="Unroll ([List.for_all anon_fun.psd.1 x], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_98 -> p_97 [label=""];
p_97 [label="Unroll ([sum (List.tl x)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_97 -> p_96 [label=""];
p_96 [label="Unroll ([List.for_all anon_fun.psd.1 (List.tl x)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_96 -> p_95 [label=""];
p_95 [label="Unroll ([sum (List.tl (List.tl x))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_95 -> p_94 [label=""];
p_94 [label="Unroll ([List.for_all anon_fun.psd.1 (List.tl (List.tl x))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_94 -> p_93 [label=""];
p_93 [label="Unroll ([sum (List.tl (List.tl (List.tl x)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_93 -> p_92 [label=""];
p_92 [label="Unroll ([List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl x)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_92 -> p_91 [label=""];
p_91 [label="Unroll ([sum (List.tl (List.tl (List.tl (List.tl x))))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_91 -> p_90 [label=""];
p_90 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl (List.tl (List.tl (List.tl x))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_90 -> p_89 [label=""];
p_89 [label="Unroll ([sum (List.tl (List.tl (List.tl (List.tl (List.tl x)))))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_89 -> p_88 [label=""];
p_88 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl (List.tl (List.tl (List.tl (List.tl x)))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_88 -> p_87 [label=""];
p_87 [label="Unroll ([sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_87 -> p_86 [label=""];
p_86 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_86 -> p_85 [label=""];
p_85 [label="Unroll ([sum\l         (List.tl\l          (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_85 -> p_84 [label=""];
p_84 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_84 -> p_83 [label=""];
p_83 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_83 -> p_82 [label=""];
p_82 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_82 -> p_81 [label=""];
p_81 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_81 -> p_80 [label=""];
p_80 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_80 -> p_79 [label=""];
p_79 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_79 -> p_78 [label=""];
p_78 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_78 -> p_77 [label=""];
p_77 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_77 -> p_76 [label=""];
p_76 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_76 -> p_75 [label=""];
p_75 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_75 -> p_74 [label=""];
p_74 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_74 -> p_73 [label=""];
p_73 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_73 -> p_72 [label=""];
p_72 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_72 -> p_71 [label=""];
p_71 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_71 -> p_70 [label=""];
p_70 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_70 -> p_69 [label=""];
p_69 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_69 -> p_68 [label=""];
p_68 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_68 -> p_67 [label=""];
p_67 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_67 -> p_66 [label=""];
p_66 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_66 -> p_65 [label=""];
p_65 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_65 -> p_64 [label=""];
p_64 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_64 -> p_63 [label=""];
p_63 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_63 -> p_62 [label=""];
p_62 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_62 -> p_61 [label=""];
p_61 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_61 -> p_60 [label=""];
p_60 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_60 -> p_59 [label=""];
p_59 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_59 -> p_58 [label=""];
p_58 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_58 -> p_57 [label=""];
p_57 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_57 -> p_56 [label=""];
p_56 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_56 -> p_55 [label=""];
p_55 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_55 -> p_54 [label=""];
p_54 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_54 -> p_53 [label=""];
p_53 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_53 -> p_52 [label=""];
p_52 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_52 -> p_51 [label=""];
p_51 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_51 -> p_50 [label=""];
p_50 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_50 -> p_49 [label=""];
p_49 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_49 -> p_48 [label=""];
p_48 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_48 -> p_47 [label=""];
p_47 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_47 -> p_46 [label=""];
p_46 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_46 -> p_45 [label=""];
p_45 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_45 -> p_44 [label=""];
p_44 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_44 -> p_43 [label=""];
p_43 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_43 -> p_42 [label=""];
p_42 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_42 -> p_41 [label=""];
p_41 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_41 -> p_40 [label=""];
p_40 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_40 -> p_39 [label=""];
p_39 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_39 -> p_38 [label=""];
p_38 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_38 -> p_37 [label=""];
p_37 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_37 -> p_36 [label=""];
p_36 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_36 -> p_35 [label=""];
p_35 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_35 -> p_34 [label=""];
p_34 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_34 -> p_33 [label=""];
p_33 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_33 -> p_32 [label=""];
p_32 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_32 -> p_31 [label=""];
p_31 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_31 -> p_30 [label=""];
p_30 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_30 -> p_29 [label=""];
p_29 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_29 -> p_28 [label=""];
p_28 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_28 -> p_27 [label=""];
p_27 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_27 -> p_26 [label=""];
p_26 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_26 -> p_25 [label=""];
p_25 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_25 -> p_24 [label=""];
p_24 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_24 -> p_23 [label=""];
p_23 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_23 -> p_22 [label=""];
p_22 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_22 -> p_21 [label=""];
p_21 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_21 -> p_20 [label=""];
p_20 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_20 -> p_19 [label=""];
p_19 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_19 -> p_18 [label=""];
p_18 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_18 -> p_17 [label=""];
p_17 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_17 -> p_16 [label=""];
p_16 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_16 -> p_15 [label=""];
p_15 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_15 -> p_14 [label=""];
p_14 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_14 -> p_13 [label=""];
p_13 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_13 -> p_12 [label=""];
p_12 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_12 -> p_11 [label=""];
p_11 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_11 -> p_10 [label=""];
p_10 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_10 -> p_9 [label=""];
p_9 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_9 -> p_8 [label=""];
p_8 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_8 -> p_7 [label=""];
p_7 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl\l                                                     (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_7 -> p_6 [label=""];
p_6 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl\l                                                     (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_6 -> p_5 [label=""];
p_5 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl\l                                                     (List.tl\l                                                      (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_5 -> p_4 [label=""];
p_4 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl\l                                                     (List.tl\l                                                      (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_4 -> p_3 [label=""];
p_3 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl\l                                                     (List.tl\l                                                      (List.tl\l                                                       (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_3 -> p_2 [label=""];
p_2 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl\l                                                     (List.tl\l                                                      (List.tl\l                                                       (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_2 -> p_1 [label=""];
p_1 [label="Unroll ([sum\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl\l                                                     (List.tl\l                                                      (List.tl\l                                                       (List.tl\l                                                        (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_1 -> p_0 [label=""];
p_0 [label="Unroll ([List.for_all anon_fun.psd.1\l         (List.tl\l          (List.tl\l           (List.tl\l            (List.tl\l             (List.tl\l              (List.tl\l               (List.tl\l                (List.tl\l                 (List.tl\l                  (List.tl\l                   (List.tl\l                    (List.tl\l                     (List.tl\l                      (List.tl\l                       (List.tl\l                        (List.tl\l                         (List.tl\l                          (List.tl\l                           (List.tl\l                            (List.tl\l                             (List.tl\l                              (List.tl\l                               (List.tl\l                                (List.tl\l                                 (List.tl\l                                  (List.tl\l                                   (List.tl\l                                    (List.tl\l                                     (List.tl\l                                      (List.tl\l                                       (List.tl\l                                        (List.tl\l                                         (List.tl\l                                          (List.tl\l                                           (List.tl\l                                            (List.tl\l                                             (List.tl\l                                              (List.tl\l                                               (List.tl\l                                                (List.tl\l                                                 (List.tl\l                                                  (List.tl\l                                                   (List.tl\l                                                    (List.tl\l                                                     (List.tl\l                                                      (List.tl\l                                                       (List.tl\l                                                        (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
}

Loading..

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!

Try this!

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:

digraph "proof" {
p_162 [label="Start (List.for_all anon_fun.psd.1 ( :var_0: ) ==\> sum ( :var_0: ) \>= 0\l       :name \"Goal\" :time 0.132s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_162 -> p_160 [label=""];
subgraph cluster_161 {
  color=blue;
p_160 [label="Start (not (List.for_all anon_fun.psd.1 x) \|\| (sum x \>= 0) :name \"1\"\l       :time 0.132s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_160 -> p_159 [label=""];
p_159 [label="Induct ((functional ?),\l        :scheme (not (x \<\> []) ==\> φ x)\l                && (x \<\> [] && φ (List.tl x) ==\> φ x))",shape=box,style=filled,fontname="courier",fontsize=14];
p_159 -> p_158 [label=""];
p_158 [label="Split (let (_x_0 : bool) = x \<\> [] in\l       let (_x_1 : bool) = sum x \>= 0 in\l       let (_x_2 : bool) = not (List.for_all anon_fun.psd.1 x) in\l       let (_x_3 : int list) = List.tl x in\l       (_x_0 \|\| _x_1 \|\| _x_2)\l       && (not\l           (_x_0\l            && (not (List.for_all anon_fun.psd.1 _x_3) \|\| (sum _x_3 \>= 0)))\l           \|\| _x_1 \|\| _x_2)\l       :cases [not (List.for_all anon_fun.psd.1 x) \|\| x \<\> [] \|\| (sum x \>= 0);\l               let (_x_0 : int list) = List.tl x in\l               not (x \<\> [])\l               \|\| not (List.for_all anon_fun.psd.1 _x_0 ==\> sum _x_0 \>= 0)\l               \|\| not (List.for_all anon_fun.psd.1 x) \|\| (sum x \>= 0)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_158 -> p_153 [label=""];
subgraph cluster_154 {
  color=blue;
p_153 [label="Start (let (_x_0 : int list) = List.tl x in\l       not (x \<\> [])\l       \|\| not (List.for_all anon_fun.psd.1 _x_0 ==\> sum _x_0 \>= 0)\l       \|\| not (List.for_all anon_fun.psd.1 x) \|\| (sum x \>= 0) :name \"1.1\"\l       :time 0.082s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_153 -> p_152 [label=""];
p_152 [label="Simplify (true :expansions [List.for_all; sum; List.for_all] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_158 -> p_156 [label=""];
subgraph cluster_157 {
  color=blue;
p_156 [label="Start (not (List.for_all anon_fun.psd.1 x) \|\| x \<\> [] \|\| (sum x \>= 0)\l       :name \"1.2\" :time 0.082s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_156 -> p_155 [label=""];
p_155 [label="Simplify (true :expansions [sum; List.for_all] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Loading..

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

We hope you enjoyed this quick introduction!

into:	true
expansions:	[List.for_all, sum, List.for_all]
rewrite_steps:
forward_chaining: