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:

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

let f x =
  if x > 99 then
    100
  else if x < 70 && x > 23
  then 89 + x
  else if x > 20
  then g x + 20
  else if x > -2 then
    103
  else 99
Out[1]:
val g : Z.t -> Z.t = <fun>
val f : Z.t -> Z.t = <fun>

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

let g x = <body>

is the equivalent of something like

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

in many other languages.

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

let g (x : int) = <body>

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

In [2]:
g 5
Out[2]:
- : Z.t = 105
In [3]:
g 23017263820
Out[3]:
- : Z.t = 9
In [4]:
f (- 1)
Out[4]:
- : Z.t = 103

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

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

In [5]:
let g_upper_bound x =
   g x <= 122
Out[5]:
val g_upper_bound : Z.t -> bool = <fun>

Now let's ask Imandra to verify our statement!

In [6]:
verify g_upper_bound
Out[6]:
- : Z.t -> bool = <fun>
Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.012s
details:
Expand
smt_stats:
rlimit count:32
num allocs:5644696
time:0.005000
memory:15.600000
max memory:15.600000
Expand
  • start[0.012s] (if ( :var_0: ) > 22 then 9 else 100 + ( :var_0: )) <= 122
  • simplify

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

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

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

      In [7]:
      verify (fun x -> f x <> 158)
      
      Out[7]:
      - : Z.t -> bool = <fun>
      module CX : sig val x : Z.t end
      
      Counterexample (after 0 steps, 0.012s):
      let x : int = 69
      
      Refuted
      proof attempt
      ground_instances:0
      definitions:0
      inductions:0
      search_time:
      0.012s
      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:11324765
      final checks:1
      time:0.005000
      memory:15.790000
      max memory:16.100000
      Expand
      • start[0.012s]
          not
          ((if ( :var_0: ) > 99 then 100
            else
            if (( :var_0: ) < 70) && (( :var_0: ) > 23) then 89 + ( :var_0: )
            else
            if ( :var_0: ) > 20 then (if ( :var_0: ) > 22 then 9 else …) + 20
            else if ( :var_0: ) > (-2) then 103 else 99)
           = 158)
      • simplify

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

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

          In [8]:
          f 69
          
          Out[8]:
          - : Z.t = 158
          

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

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

          In [9]:
          CX.x
          
          Out[9]:
          - : Z.t = 69
          
          In [10]:
          f CX.x
          
          Out[10]:
          - : Z.t = 158
          

          Region Decomposition

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

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

          In [11]:
          Modular_decomp.top "f"
          
          Out[11]:
          - : Modular_decomp_intf.decomp_ref = <abstr>
          
          Regions details

          No group selected.

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

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

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

          Recursion and Induction

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

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

          In [12]:
          let rec sum x = match x with
           | [] -> 0
           | x :: xs -> x + sum xs
          
          Out[12]:
          val sum : Z.t list -> Z.t = <fun>
          
          termination proof

          Termination proof

          call `sum (List.tl x)` from `sum x`
          original:sum x
          sub:sum (List.tl x)
          original ordinal:Ordinal.Int (_cnt x)
          sub ordinal:Ordinal.Int (_cnt (List.tl x))
          path:[x <> []]
          proof:
          detailed proof
          ground_instances:3
          definitions:0
          inductions:0
          search_time:
          0.008s
          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:18696605
          final checks:4
          added eqs:49
          del clause:11
          arith eq adapter:12
          memory:16.290000
          max memory:16.290000
          Expand
          • start[0.008s]
              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_387/server| (|get.::.1_375/server|…
                expansions:
                • unroll
                  expr:
                  (|count.list_387/server| (|get.::.1_375/server| x_376/server))
                  expansions:
                  • unroll
                    expr:
                    (|count.list_387/server| x_376/server)
                    expansions:
                    • Unsat
                    In [13]:
                    sum []
                    
                    Out[13]:
                    - : Z.t = 0
                    
                    In [14]:
                    sum [1;2;3]
                    
                    Out[14]:
                    - : Z.t = 6
                    

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

                    In [15]:
                    instance (fun x -> List.length x >= 10 && sum x = List.length x + 17)
                    
                    Out[15]:
                    - : Z.t list -> bool = <fun>
                    module CX : sig val x : Z.t list end
                    
                    Instance (after 22 steps, 0.020s):
                    let x : int list =
                      [(-10620); 3583; 609; (-1221); (-10318); 1888; 5904; 5481; 2275; 2446]
                    
                    Instance
                    proof attempt
                    ground_instances:22
                    definitions:0
                    inductions:0
                    search_time:
                    0.020s
                    details:
                    Expand
                    smt_stats:
                    arith offset eqs:24
                    num checks:45
                    arith assert lower:172
                    arith tableau max rows:44
                    arith tableau max columns:83
                    arith pivots:125
                    rlimit count:27809
                    mk clause:270
                    datatype occurs check:68
                    mk bool var:872
                    arith assert upper:147
                    datatype splits:16
                    decisions:255
                    arith row summations:696
                    propagations:343
                    interface eqs:16
                    conflicts:50
                    arith fixed eqs:100
                    arith assume eqs:16
                    datatype accessor ax:51
                    minimized lits:1
                    arith conflicts:28
                    arith num rows:44
                    arith assert diseq:28
                    datatype constructor ax:110
                    num allocs:28198943
                    final checks:55
                    added eqs:942
                    del clause:261
                    arith eq adapter:177
                    memory:17.050000
                    max memory:17.050000
                    Expand
                    • start[0.020s]
                        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:
                          (sum_1254/client x_1258/client)
                          expansions:
                          • unroll
                            expr:
                            (|List.length_419/server| x_1258/client)
                            expansions:
                            • unroll
                              expr:
                              (sum_1254/client (|get.::.1_418/server| x_1258/client))
                              expansions:
                              • unroll
                                expr:
                                (|List.length_419/server| (|get.::.1_418/server| x_1258/client))
                                expansions:
                                • unroll
                                  expr:
                                  (sum_1254/client (|get.::.1_418/server| (|get.::.1_418/server| x_1258/client)))
                                  expansions:
                                  • unroll
                                    expr:
                                    (|List.length_419/server|
                                      (|get.::.1_418/server| (|get.::.1_418/server| x_1258/client)))
                                    expansions:
                                    • unroll
                                      expr:
                                      (sum_1254/client (|get.::.1_418/server|
                                                         (|get.::.1_418/server| (|get.::.1_418/ser…
                                      expansions:
                                      • unroll
                                        expr:
                                        (|List.length_419/server|
                                          (|get.::.1_418/server|
                                            (|get.::.1_418/server| (|get.::.1_418/server|…
                                        expansions:
                                        • unroll
                                          expr:
                                          (let ((a!1 (|get.::.1_418/server|
                                                       (|get.::.1_418/server|
                                                         (|get.::.1_418/…
                                          expansions:
                                          • unroll
                                            expr:
                                            (let ((a!1 (|get.::.1_418/server|
                                                         (|get.::.1_418/server|
                                                           (|get.::.1_418/…
                                            expansions:
                                            • unroll
                                              expr:
                                              (let ((a!1 (|get.::.1_418/server|
                                                           (|get.::.1_418/server|
                                                             (|get.::.1_418/…
                                              expansions:
                                              • unroll
                                                expr:
                                                (let ((a!1 (|get.::.1_418/server|
                                                             (|get.::.1_418/server|
                                                               (|get.::.1_418/…
                                                expansions:
                                                • unroll
                                                  expr:
                                                  (let ((a!1 (|get.::.1_418/server|
                                                               (|get.::.1_418/server|
                                                                 (|get.::.1_418/…
                                                  expansions:
                                                  • unroll
                                                    expr:
                                                    (let ((a!1 (|get.::.1_418/server|
                                                                 (|get.::.1_418/server|
                                                                   (|get.::.1_418/…
                                                    expansions:
                                                    • unroll
                                                      expr:
                                                      (let ((a!1 (|get.::.1_418/server|
                                                                   (|get.::.1_418/server|
                                                                     (|get.::.1_418/…
                                                      expansions:
                                                      • unroll
                                                        expr:
                                                        (let ((a!1 (|get.::.1_418/server|
                                                                     (|get.::.1_418/server|
                                                                       (|get.::.1_418/…
                                                        expansions:
                                                        • unroll
                                                          expr:
                                                          (let ((a!1 (|get.::.1_418/server|
                                                                       (|get.::.1_418/server|
                                                                         (|get.::.1_418/…
                                                          expansions:
                                                          • unroll
                                                            expr:
                                                            (let ((a!1 (|get.::.1_418/server|
                                                                         (|get.::.1_418/server|
                                                                           (|get.::.1_418/…
                                                            expansions:
                                                            • unroll
                                                              expr:
                                                              (let ((a!1 (|get.::.1_418/server|
                                                                           (|get.::.1_418/server|
                                                                             (|get.::.1_418/…
                                                              expansions:
                                                              • unroll
                                                                expr:
                                                                (let ((a!1 (|get.::.1_418/server|
                                                                             (|get.::.1_418/server|
                                                                               (|get.::.1_418/…
                                                                expansions:
                                                                • unroll
                                                                  expr:
                                                                  (let ((a!1 (|get.::.1_418/server|
                                                                               (|get.::.1_418/server|
                                                                                 (|get.::.1_418/…
                                                                  expansions:
                                                                  • unroll
                                                                    expr:
                                                                    (let ((a!1 (|get.::.1_418/server|
                                                                                 (|get.::.1_418/server|
                                                                                   (|get.::.1_418/…
                                                                    expansions:
                                                                    • Sat (Some let x : int list = [(Z.of_nativeint (-10620n)); (Z.of_nativeint (3583n)); (Z.of_nativeint (609n)); (Z.of_nativeint (-1221n)); (Z.of_nativeint (-10318n)); (Z.of_nativeint (1888n)); (Z.of_nativeint (5904n)); (Z.of_nativeint (5481n)); (Z.of_nativeint (2275n)); (Z.of_nativeint (2446n))] )

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

                                                                    In [16]:
                                                                    List.length CX.x
                                                                    
                                                                    Out[16]:
                                                                    - : Z.t = 10
                                                                    
                                                                    In [17]:
                                                                    sum CX.x
                                                                    
                                                                    Out[17]:
                                                                    - : Z.t = 27
                                                                    

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

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

                                                                    In [18]:
                                                                    verify (fun x -> sum x >= 0)
                                                                    
                                                                    Out[18]:
                                                                    - : Z.t list -> bool = <fun>
                                                                    module CX : sig val x : Z.t list end
                                                                    
                                                                    Counterexample (after 2 steps, 0.007s):
                                                                    let x : int list = [(-1)]
                                                                    
                                                                    Refuted
                                                                    proof attempt
                                                                    ground_instances:2
                                                                    definitions:0
                                                                    inductions:0
                                                                    search_time:
                                                                    0.007s
                                                                    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:39938536
                                                                    final checks:4
                                                                    added eqs:29
                                                                    del clause:4
                                                                    arith eq adapter:5
                                                                    memory:17.010000
                                                                    max memory:17.050000
                                                                    Expand
                                                                    • start[0.007s] sum ( :var_0: ) >= 0
                                                                    • unroll
                                                                      expr:
                                                                      (sum_1254/client x_1260/client)
                                                                      expansions:
                                                                      • unroll
                                                                        expr:
                                                                        (sum_1254/client (|get.::.1_454/server| x_1260/client))
                                                                        expansions:
                                                                        • Sat (Some let x : int list = [(Z.of_nativeint (-1n))] )

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

                                                                        In [19]:
                                                                        sum CX.x
                                                                        
                                                                        Out[19]:
                                                                        - : Z.t = -1
                                                                        

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

                                                                        In [20]:
                                                                        let psd = List.for_all (fun x -> x >= 0)
                                                                        
                                                                        Out[20]:
                                                                        val psd : Z.t list -> bool = <fun>
                                                                        

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

                                                                        In [21]:
                                                                        verify (fun x -> psd x ==> sum x >= 0)
                                                                        
                                                                        Out[21]:
                                                                        - : Z.t list -> bool = <fun>
                                                                        
                                                                        Unknown (Verified up to bound 100)
                                                                        Expand
                                                                        expanded:
                                                                        • List.for_all anon_fun.psd.1 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl 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)))))))))))))))))))))))))))))))))))))))
                                                                        • 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)))))))))))))))))))))))))))))))
                                                                        • 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)))))))))))))))))))))))
                                                                        • 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)))))))))))))))
                                                                        • 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 (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 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)))))))))))))))))))))))))))
                                                                        • 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)))))))))))))))))))
                                                                        • 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 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 (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))))))))))))))))))))))))))
                                                                        • 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 x))))))))))
                                                                        • List.for_all anon_fun.psd.1 (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 (List.tl (List.tl (List.tl (List.tl (List.tl (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 (List.tl (List.tl (List.tl (List.tl (List.tl (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))))))))))))))
                                                                        • sum (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 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)))))))))))))))))))))))))))))))))))))))))
                                                                        • 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 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 x)))))))))
                                                                        • List.for_all anon_fun.psd.1 (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)))))))))))))))))))))))))))))))))))))))))))))
                                                                        • 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)))))))))))))))))))))))))))))))))))))
                                                                        • 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)))))))))))))))))))))))))))))
                                                                        • 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)))))))))))))))))))))
                                                                        • 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)))))))))))))
                                                                        • 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))
                                                                        • 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))))))))))))
                                                                        • List.for_all anon_fun.psd.1 (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))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))))))
                                                                        • 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 x))))))))))))))))
                                                                        • sum (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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 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)))))))))))))))))))
                                                                        • 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 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)))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • 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 (List.tl (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)))))))))))))))))))))))
                                                                        • 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 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))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))))
                                                                        • 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 x))))))))))))))
                                                                        • List.for_all anon_fun.psd.1 (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))))))))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))
                                                                        • sum (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 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)))))))))))))))))))))))))))))))))))))
                                                                        • 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)))))))))))))))))))))))))))))
                                                                        • 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)))))))))))))))))))))
                                                                        • 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)))))))))))))
                                                                        • 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 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 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 x)))))))))
                                                                        • sum (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))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))))))))))))))
                                                                        • 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 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 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 (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))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))
                                                                        • 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))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl x))))
                                                                        blocked:
                                                                        • 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))))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        proof attempt
                                                                        ground_instances:100
                                                                        definitions:0
                                                                        inductions:0
                                                                        search_time:
                                                                        0.121s
                                                                        Expand
                                                                        • start[0.121s]
                                                                            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_1254/client x_368/server)
                                                                              expansions:
                                                                              • unroll
                                                                                expr:
                                                                                (|List.for_all_369/server| x_368/server)
                                                                                expansions:
                                                                                • unroll
                                                                                  expr:
                                                                                  (sum_1254/client (|get.::.1_367/server| x_368/server))
                                                                                  expansions:
                                                                                  • unroll
                                                                                    expr:
                                                                                    (|List.for_all_369/server| (|get.::.1_367/server| x_368/server))
                                                                                    expansions:
                                                                                    • unroll
                                                                                      expr:
                                                                                      (sum_1254/client (|get.::.1_367/server| (|get.::.1_367/server| x_368/server)))
                                                                                      expansions:
                                                                                      • unroll
                                                                                        expr:
                                                                                        (|List.for_all_369/server|
                                                                                          (|get.::.1_367/server| (|get.::.1_367/server| x_368/server)))
                                                                                        expansions:
                                                                                        • unroll
                                                                                          expr:
                                                                                          (sum_1254/client (|get.::.1_367/server|
                                                                                                             (|get.::.1_367/server| (|get.::.1_367/ser…
                                                                                          expansions:
                                                                                          • unroll
                                                                                            expr:
                                                                                            (|List.for_all_369/server|
                                                                                              (|get.::.1_367/server|
                                                                                                (|get.::.1_367/server| (|get.::.1_367/server…
                                                                                            expansions:
                                                                                            • unroll
                                                                                              expr:
                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                           (|get.::.1_367/server|
                                                                                                             (|get.::.1_367/…
                                                                                              expansions:
                                                                                              • unroll
                                                                                                expr:
                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                             (|get.::.1_367/server|
                                                                                                               (|get.::.1_367/…
                                                                                                expansions:
                                                                                                • unroll
                                                                                                  expr:
                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                               (|get.::.1_367/server|
                                                                                                                 (|get.::.1_367/…
                                                                                                  expansions:
                                                                                                  • unroll
                                                                                                    expr:
                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                 (|get.::.1_367/server|
                                                                                                                   (|get.::.1_367/…
                                                                                                    expansions:
                                                                                                    • unroll
                                                                                                      expr:
                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                   (|get.::.1_367/server|
                                                                                                                     (|get.::.1_367/…
                                                                                                      expansions:
                                                                                                      • unroll
                                                                                                        expr:
                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                     (|get.::.1_367/server|
                                                                                                                       (|get.::.1_367/…
                                                                                                        expansions:
                                                                                                        • unroll
                                                                                                          expr:
                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                       (|get.::.1_367/server|
                                                                                                                         (|get.::.1_367/…
                                                                                                          expansions:
                                                                                                          • unroll
                                                                                                            expr:
                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                         (|get.::.1_367/server|
                                                                                                                           (|get.::.1_367/…
                                                                                                            expansions:
                                                                                                            • unroll
                                                                                                              expr:
                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                           (|get.::.1_367/server|
                                                                                                                             (|get.::.1_367/…
                                                                                                              expansions:
                                                                                                              • unroll
                                                                                                                expr:
                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                             (|get.::.1_367/server|
                                                                                                                               (|get.::.1_367/…
                                                                                                                expansions:
                                                                                                                • unroll
                                                                                                                  expr:
                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                               (|get.::.1_367/server|
                                                                                                                                 (|get.::.1_367/…
                                                                                                                  expansions:
                                                                                                                  • unroll
                                                                                                                    expr:
                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                   (|get.::.1_367/…
                                                                                                                    expansions:
                                                                                                                    • unroll
                                                                                                                      expr:
                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                     (|get.::.1_367/…
                                                                                                                      expansions:
                                                                                                                      • unroll
                                                                                                                        expr:
                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                       (|get.::.1_367/…
                                                                                                                        expansions:
                                                                                                                        • unroll
                                                                                                                          expr:
                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                         (|get.::.1_367/…
                                                                                                                          expansions:
                                                                                                                          • unroll
                                                                                                                            expr:
                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                           (|get.::.1_367/…
                                                                                                                            expansions:
                                                                                                                            • unroll
                                                                                                                              expr:
                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                             (|get.::.1_367/…
                                                                                                                              expansions:
                                                                                                                              • unroll
                                                                                                                                expr:
                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                               (|get.::.1_367/…
                                                                                                                                expansions:
                                                                                                                                • unroll
                                                                                                                                  expr:
                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                  expansions:
                                                                                                                                  • unroll
                                                                                                                                    expr:
                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                    expansions:
                                                                                                                                    • unroll
                                                                                                                                      expr:
                                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                                     (|get.::.1_367/…
                                                                                                                                      expansions:
                                                                                                                                      • unroll
                                                                                                                                        expr:
                                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                                       (|get.::.1_367/…
                                                                                                                                        expansions:
                                                                                                                                        • unroll
                                                                                                                                          expr:
                                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                                         (|get.::.1_367/…
                                                                                                                                          expansions:
                                                                                                                                          • unroll
                                                                                                                                            expr:
                                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                                           (|get.::.1_367/…
                                                                                                                                            expansions:
                                                                                                                                            • unroll
                                                                                                                                              expr:
                                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                                             (|get.::.1_367/…
                                                                                                                                              expansions:
                                                                                                                                              • unroll
                                                                                                                                                expr:
                                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                                               (|get.::.1_367/…
                                                                                                                                                expansions:
                                                                                                                                                • unroll
                                                                                                                                                  expr:
                                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                                  expansions:
                                                                                                                                                  • unroll
                                                                                                                                                    expr:
                                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                                    expansions:
                                                                                                                                                    • unroll
                                                                                                                                                      expr:
                                                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                                                     (|get.::.1_367/…
                                                                                                                                                      expansions:
                                                                                                                                                      • unroll
                                                                                                                                                        expr:
                                                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                                                       (|get.::.1_367/…
                                                                                                                                                        expansions:
                                                                                                                                                        • unroll
                                                                                                                                                          expr:
                                                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                                                         (|get.::.1_367/…
                                                                                                                                                          expansions:
                                                                                                                                                          • unroll
                                                                                                                                                            expr:
                                                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                                                           (|get.::.1_367/…
                                                                                                                                                            expansions:
                                                                                                                                                            • unroll
                                                                                                                                                              expr:
                                                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                                                             (|get.::.1_367/…
                                                                                                                                                              expansions:
                                                                                                                                                              • unroll
                                                                                                                                                                expr:
                                                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                                                               (|get.::.1_367/…
                                                                                                                                                                expansions:
                                                                                                                                                                • unroll
                                                                                                                                                                  expr:
                                                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                                                  expansions:
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr:
                                                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                                                    expansions:
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr:
                                                                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                                                                     (|get.::.1_367/…
                                                                                                                                                                      expansions:
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr:
                                                                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                                                                       (|get.::.1_367/…
                                                                                                                                                                        expansions:
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr:
                                                                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                                                                         (|get.::.1_367/…
                                                                                                                                                                          expansions:
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr:
                                                                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                                                                           (|get.::.1_367/…
                                                                                                                                                                            expansions:
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr:
                                                                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                                                                             (|get.::.1_367/…
                                                                                                                                                                              expansions:
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr:
                                                                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                                                                               (|get.::.1_367/…
                                                                                                                                                                                expansions:
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr:
                                                                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                                                                  expansions:
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr:
                                                                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                                                                    expansions:
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr:
                                                                                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                                                                                     (|get.::.1_367/…
                                                                                                                                                                                      expansions:
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr:
                                                                                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                                                                                       (|get.::.1_367/…
                                                                                                                                                                                        expansions:
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr:
                                                                                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                                                                                         (|get.::.1_367/…
                                                                                                                                                                                          expansions:
                                                                                                                                                                                          • unroll
                                                                                                                                                                                            expr:
                                                                                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                                                                                           (|get.::.1_367/…
                                                                                                                                                                                            expansions:
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr:
                                                                                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                                                                                             (|get.::.1_367/…
                                                                                                                                                                                              expansions:
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr:
                                                                                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                                                                                               (|get.::.1_367/…
                                                                                                                                                                                                expansions:
                                                                                                                                                                                                • unroll
                                                                                                                                                                                                  expr:
                                                                                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                                                                                  expansions:
                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                    expr:
                                                                                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                                                                                    expansions:
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr:
                                                                                                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                                                                                                     (|get.::.1_367/…
                                                                                                                                                                                                      expansions:
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr:
                                                                                                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                                                                                                       (|get.::.1_367/…
                                                                                                                                                                                                        expansions:
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr:
                                                                                                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                                                                                                         (|get.::.1_367/…
                                                                                                                                                                                                          expansions:
                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                            expr:
                                                                                                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                                                                                                           (|get.::.1_367/…
                                                                                                                                                                                                            expansions:
                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                              expr:
                                                                                                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                                                                                                             (|get.::.1_367/…
                                                                                                                                                                                                              expansions:
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr:
                                                                                                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                                                                                                               (|get.::.1_367/…
                                                                                                                                                                                                                expansions:
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr:
                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                                                                                                  expansions:
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr:
                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                                                                                                    expansions:
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr:
                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                                                                                                                     (|get.::.1_367/…
                                                                                                                                                                                                                      expansions:
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr:
                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                                                                                                                       (|get.::.1_367/…
                                                                                                                                                                                                                        expansions:
                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                          expr:
                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                                                                                                                         (|get.::.1_367/…
                                                                                                                                                                                                                          expansions:
                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                            expr:
                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                                                                                                                           (|get.::.1_367/…
                                                                                                                                                                                                                            expansions:
                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                              expr:
                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                                                                                                                             (|get.::.1_367/…
                                                                                                                                                                                                                              expansions:
                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                expr:
                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                                                                                                                               (|get.::.1_367/…
                                                                                                                                                                                                                                expansions:
                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                  expr:
                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                                                                                                                  expansions:
                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                    expr:
                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                                                                                                                    expansions:
                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                      expr:
                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                                                                                                                                     (|get.::.1_367/…
                                                                                                                                                                                                                                      expansions:
                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                        expr:
                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                                                                                                                                       (|get.::.1_367/…
                                                                                                                                                                                                                                        expansions:
                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                          expr:
                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                                                                                                                                         (|get.::.1_367/…
                                                                                                                                                                                                                                          expansions:
                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                            expr:
                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                                                                                                                                           (|get.::.1_367/…
                                                                                                                                                                                                                                            expansions:
                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                              expr:
                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                                                                                                                                             (|get.::.1_367/…
                                                                                                                                                                                                                                              expansions:
                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                expr:
                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                                                                                                                                               (|get.::.1_367/…
                                                                                                                                                                                                                                                expansions:
                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                  expr:
                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                                                                                                                                  expansions:
                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                    expr:
                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                                                                                                                                    expansions:
                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                      expr:
                                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                                                                                                                                                     (|get.::.1_367/…
                                                                                                                                                                                                                                                      expansions:
                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                        expr:
                                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                                                                                                                                                       (|get.::.1_367/…
                                                                                                                                                                                                                                                        expansions:
                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                          expr:
                                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                                                                                                                                                         (|get.::.1_367/…
                                                                                                                                                                                                                                                          expansions:
                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                            expr:
                                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                                                                                                                                                           (|get.::.1_367/…
                                                                                                                                                                                                                                                            expansions:
                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                              expr:
                                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                                                                                                                                                             (|get.::.1_367/…
                                                                                                                                                                                                                                                              expansions:
                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                expr:
                                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                                                                                                                                                               (|get.::.1_367/…
                                                                                                                                                                                                                                                                expansions:
                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                  expr:
                                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                                                                                                                                                  expansions:
                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                    expr:
                                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                                                                                                                                                    expansions:
                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                      expr:
                                                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                   (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                     (|get.::.1_367/…
                                                                                                                                                                                                                                                                      expansions:
                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                        expr:
                                                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                     (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                       (|get.::.1_367/…
                                                                                                                                                                                                                                                                        expansions:
                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                          expr:
                                                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                       (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                         (|get.::.1_367/…
                                                                                                                                                                                                                                                                          expansions:
                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                            expr:
                                                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                         (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                           (|get.::.1_367/…
                                                                                                                                                                                                                                                                            expansions:
                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                              expr:
                                                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                           (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                             (|get.::.1_367/…
                                                                                                                                                                                                                                                                              expansions:
                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                expr:
                                                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                             (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                               (|get.::.1_367/…
                                                                                                                                                                                                                                                                                expansions:
                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                  expr:
                                                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                               (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                                 (|get.::.1_367/…
                                                                                                                                                                                                                                                                                  expansions:
                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                    expr:
                                                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                                 (|get.::.1_367/server|
                                                                                                                                                                                                                                                                                                   (|get.::.1_367/…
                                                                                                                                                                                                                                                                                    expansions:

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

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

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

                                                                                                                                                                                                                                                                                    In [22]:
                                                                                                                                                                                                                                                                                    verify (fun x -> psd x ==> sum x >= 0) [@@auto]
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Out[22]:
                                                                                                                                                                                                                                                                                    - : Z.t list -> bool = <fun>
                                                                                                                                                                                                                                                                                    Goal:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    psd x ==> sum x >= 0.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    1 nontautological subgoal.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Subgoal 1:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     H0. List.for_all anon_fun.psd.1 x
                                                                                                                                                                                                                                                                                    |---------------------------------------------------------------------------
                                                                                                                                                                                                                                                                                     sum x >= 0
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Must try induction.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    The recursive terms in the conjecture suggest 2 inductions.
                                                                                                                                                                                                                                                                                    Subsumption and merging reduces this to 1.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    We shall induct according to a scheme derived from List.for_all.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Induction scheme:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     (not (x <> []) ==> φ x) && (x <> [] && φ (List.tl x) ==> φ x).
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    2 nontautological subgoals.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Subgoal 1.2:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     H0. List.for_all anon_fun.psd.1 x
                                                                                                                                                                                                                                                                                    |---------------------------------------------------------------------------
                                                                                                                                                                                                                                                                                     C0. x <> []
                                                                                                                                                                                                                                                                                     C1. sum x >= 0
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    But simplification reduces this to true, using the definitions of
                                                                                                                                                                                                                                                                                    List.for_all and sum.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Subgoal 1.1:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     H0. x <> []
                                                                                                                                                                                                                                                                                     H1. List.for_all anon_fun.psd.1 (List.tl x) ==> sum (List.tl x) >= 0
                                                                                                                                                                                                                                                                                     H2. List.for_all anon_fun.psd.1 x
                                                                                                                                                                                                                                                                                    |---------------------------------------------------------------------------
                                                                                                                                                                                                                                                                                     sum x >= 0
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    But simplification reduces this to true, using the definitions of
                                                                                                                                                                                                                                                                                    List.for_all and sum.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     Rules:
                                                                                                                                                                                                                                                                                        (:def List.for_all)
                                                                                                                                                                                                                                                                                        (:def sum)
                                                                                                                                                                                                                                                                                        (:induct List.for_all)
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Proved
                                                                                                                                                                                                                                                                                    proof
                                                                                                                                                                                                                                                                                    ground_instances:0
                                                                                                                                                                                                                                                                                    definitions:4
                                                                                                                                                                                                                                                                                    inductions:1
                                                                                                                                                                                                                                                                                    search_time:
                                                                                                                                                                                                                                                                                    0.071s
                                                                                                                                                                                                                                                                                    Expand
                                                                                                                                                                                                                                                                                    • start[0.071s, "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.071s, "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.036s, "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:
                                                                                                                                                                                                                                                                                            [sum, List.for_all]
                                                                                                                                                                                                                                                                                            rewrite_steps:
                                                                                                                                                                                                                                                                                              forward_chaining:
                                                                                                                                                                                                                                                                                            • subproof
                                                                                                                                                                                                                                                                                              not (List.for_all anon_fun.psd.1 x) || x <> [] || (sum x >= 0)
                                                                                                                                                                                                                                                                                              • start[0.036s, "1.2"]
                                                                                                                                                                                                                                                                                                  not (List.for_all anon_fun.psd.1 x) || x <> [] || (sum x >= 0)
                                                                                                                                                                                                                                                                                              • simplify
                                                                                                                                                                                                                                                                                                into:
                                                                                                                                                                                                                                                                                                true
                                                                                                                                                                                                                                                                                                expansions:
                                                                                                                                                                                                                                                                                                [sum, List.for_all]
                                                                                                                                                                                                                                                                                                rewrite_steps:
                                                                                                                                                                                                                                                                                                  forward_chaining:

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

                                                                                                                                                                                                                                                                                            We hope you enjoyed this quick introduction!