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.

A Quick Tour of Imandra

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.

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 : int -> Z.t = <fun>
val f : int -> 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 : int -> bool = <fun>

Now let's ask Imandra to verify our statement!

In [6]:
verify g_upper_bound
Out[6]:
- : int -> bool = <fun>
Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.021s
details
Expand
smt_stats
rlimit count81
mk bool var5
num allocs1398806765
memory16.070000
max memory18.750000
Expand
  • start[0.021s] (if :var_0: > 22 then 9 else (100 + :var_0:)) <= 122
  • simplify

    into
    (if :var_0: <= 22 then 100 + :var_0: else 9) <= 122
    expansions
    []
    rewrite_steps
      forward_chaining
      • unsat

        (let ((a!1 (<= (ite (<= _x_0_2436 22) (+ 100 _x_0_2436) 9) 122))
              (a!3 (ite (<= _x_0_2436 22) (…

      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]:
      - : int -> bool = <fun>
      module CX : sig val x : Z.t end
      
      Counterexample (after 0 steps, 0.023s):
       let x = 69
      
      Refuted
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.023s
      details
      Expand
      smt_stats
      num checks1
      arith assert lower6
      rlimit count602
      mk clause28
      mk bool var18
      arith assert upper3
      decisions2
      propagations19
      conflicts1
      num allocs1507965598
      final checks1
      memory16.380000
      max memory18.750000
      Expand
      • start[0.023s]
          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
        ((if :var_0: <= 99
          then
            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)
          else 100)
         = 158)
        expansions
        []
        rewrite_steps
          forward_chaining
          • Sat (Some let x = 69 )

          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]:
          Decompose.top "f"
          
          Out[11]:
          - : Imandra_reasoning.Decompose.t list =
          [<region>; <region>; <region>; <region>; <region>; <region>; <region>]
          
          Regions details
          No group selected.
          ConstraintsInvariant
          • not (x <= 99)
          F = 100
          • x <= 99
          • 70 <= x
          • not (x <= 20)
          • not (x <= 22)
          F = 29
          • x <= 99
          • not (70 <= x)
          • x <= 23
          • not (x <= 20)
          • not (x <= 22)
          F = 29
          • x <= 99
          • not (70 <= x)
          • x <= 23
          • not (x <= 20)
          • x <= 22
          F = 120 + x
          • x <= 99
          • not (70 <= x)
          • x <= 23
          • x <= 20
          • not (x <= -2)
          F = 103
          • x <= 99
          • not (70 <= x)
          • x <= 23
          • x <= 20
          • x <= -2
          F = 99
          • x <= 99
          • not (70 <= x)
          • not (x <= 23)
          F = 89 + x

          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`
          originalsum x
          subsum (List.tl x)
          original ordinalOrdinal.Int (Ordinal.count x)
          sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
          path[not (x = [])]
          proof
          detailed proof
          ground_instances3
          definitions0
          inductions0
          search_time
          0.015s
          details
          Expand
          smt_stats
          num checks8
          arith assert lower17
          arith pivots9
          rlimit count22786
          mk clause19
          datatype occurs check21
          mk bool var76
          arith assert upper13
          datatype splits3
          decisions12
          arith add rows18
          propagations14
          conflicts8
          arith fixed eqs7
          datatype accessor ax5
          arith conflicts2
          datatype constructor ax7
          num allocs3225134274
          final checks6
          added eqs47
          del clause8
          arith eq adapter11
          memory27.230000
          max memory64.360000
          Expand
          • start[0.015s]
              not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
              ==> List.tl x = []
                  || Ordinal.Int (Ordinal.count (List.tl x)) Ordinal.<<
                     Ordinal.Int (Ordinal.count x)
          • simplify
            into
            (not
             ((not (x = []) && Ordinal.count x >= 0) && Ordinal.count (List.tl x) >= 0)
             || List.tl x = [])
            || Ordinal.Int (Ordinal.count (List.tl x)) Ordinal.<<
               Ordinal.Int (Ordinal.count x)
            expansions
            []
            rewrite_steps
              forward_chaining
              • unroll
                expr
                (|Ordinal.<<_121| (|Ordinal.Int_112|
                                    (|count_`int list`_2482| (|get.::.1_2472| x…
                expansions
                • unroll
                  expr
                  (|count_`int list`_2482| (|get.::.1_2472| x_2473))
                  expansions
                  • unroll
                    expr
                    (|count_`int list`_2482| x_2473)
                    expansions
                    • unsat
                      (let ((a!1 (>= (ite (>= (|get.::.0_2471| x_2473) 0) (|get.::.0_2471| x_2473) 0)
                                     0))
                       …

                    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.050s):
                     let x =
                       [(-13545); 7719; (-3092); 7056; 6284; (-18755); (-6690); 8879; 9725; 2446]
                    
                    Instance
                    proof attempt
                    ground_instances22
                    definitions0
                    inductions0
                    search_time
                    0.050s
                    details
                    Expand
                    smt_stats
                    arith offset eqs56
                    num checks45
                    arith assert lower415
                    arith pivots211
                    rlimit count39373
                    mk clause524
                    datatype occurs check321
                    mk bool var2146
                    arith assert upper271
                    datatype splits249
                    decisions499
                    arith add rows1015
                    propagations1075
                    interface eqs17
                    conflicts91
                    arith fixed eqs236
                    datatype accessor ax222
                    minimized lits7
                    arith conflicts24
                    arith assert diseq118
                    datatype constructor ax259
                    num allocs3311002418
                    final checks90
                    added eqs2301
                    del clause509
                    arith eq adapter372
                    memory28.250000
                    max memory64.360000
                    Expand
                    • start[0.050s]
                        List.length :var_0: >= 10 && sum :var_0: = List.length :var_0: + 17
                    • simplify

                      into
                      List.length :var_0: >= 10 && sum :var_0: = 17 + List.length :var_0:
                      expansions
                      []
                      rewrite_steps
                        forward_chaining
                        • unroll
                          expr
                          (sum_2465 x_2485)
                          expansions
                          • unroll
                            expr
                            (|List.length_2491| x_2485)
                            expansions
                            • unroll
                              expr
                              (sum_2465 (|get.::.1_2490| x_2485))
                              expansions
                              • unroll
                                expr
                                (|List.length_2491| (|get.::.1_2490| x_2485))
                                expansions
                                • unroll
                                  expr
                                  (sum_2465 (|get.::.1_2490| (|get.::.1_2490| x_2485)))
                                  expansions
                                  • unroll
                                    expr
                                    (|List.length_2491| (|get.::.1_2490| (|get.::.1_2490| x_2485)))
                                    expansions
                                    • unroll
                                      expr
                                      (sum_2465 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))
                                      expansions
                                      • unroll
                                        expr
                                        (|List.length_2491|
                                          (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                            (|List…
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                              (sum_2…
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                (|List…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                  (sum_2…
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                    (|List…
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                      (sum_2…
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                        (|List…
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                          (sum_2…
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                          (let ((a…
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                            (let ((a…
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                              (let ((a…
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                                (let ((a…
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                                  (let ((a…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| (|get.::.1_2490| x_2485))))))
                                                                    (let ((a…
                                                                    expansions
                                                                    • Sat (Some let x = [(-13545); 7719; (-3092); 7056; 6284; (-18755); (-6690); 8879; 9725; 2446] )

                                                                    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.013s):
                                                                     let x = [(-1)]
                                                                    
                                                                    Refuted
                                                                    proof attempt
                                                                    ground_instances2
                                                                    definitions0
                                                                    inductions0
                                                                    search_time
                                                                    0.013s
                                                                    details
                                                                    Expand
                                                                    smt_stats
                                                                    arith offset eqs2
                                                                    num checks5
                                                                    arith assert lower3
                                                                    arith pivots3
                                                                    rlimit count868
                                                                    mk clause10
                                                                    datatype occurs check8
                                                                    mk bool var37
                                                                    arith assert upper4
                                                                    datatype splits3
                                                                    decisions8
                                                                    arith add rows5
                                                                    propagations9
                                                                    conflicts3
                                                                    arith fixed eqs2
                                                                    datatype accessor ax3
                                                                    datatype constructor ax4
                                                                    num allocs3358077060
                                                                    final checks6
                                                                    added eqs28
                                                                    del clause1
                                                                    arith eq adapter4
                                                                    memory31.260000
                                                                    max memory64.360000
                                                                    Expand
                                                                    • start[0.013s] sum :var_0: >= 0
                                                                    • unroll
                                                                      expr
                                                                      (sum_2465 x_2501)
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (sum_2465 (|get.::.1_2506| x_2501))
                                                                        expansions
                                                                        • Sat (Some let x = [(-1)] )

                                                                        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 : int 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]:
                                                                        - : int list -> bool = <fun>
                                                                        
                                                                        Unknown (Verified up to bound 100)
                                                                        Expand
                                                                        expanded
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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)))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (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))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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)))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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)))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl x))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl x)
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))
                                                                        • sum (List.tl (List.tl (List.tl x)))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl x))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 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)))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl x))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl x)
                                                                        • List.for_all (fun x -> x >= 0) (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl x)))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (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)))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))
                                                                        • sum x
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 x))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (List.tl (List.tl x))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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)))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl x)))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) x
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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)))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))
                                                                        blocked
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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_instances100
                                                                        definitions0
                                                                        inductions0
                                                                        search_time
                                                                        0.414s
                                                                        Expand
                                                                        • start[0.414s] List.for_all (fun x -> x >= 0) :var_0: ==> sum :var_0: >= 0
                                                                        • simplify

                                                                          into
                                                                          not (List.for_all (fun x -> x >= 0) :var_0:) || sum :var_0: >= 0
                                                                          expansions
                                                                          []
                                                                          rewrite_steps
                                                                            forward_chaining
                                                                            • unroll
                                                                              expr
                                                                              (sum_2465 x_2524)
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (|`List.for_all anon_fun.psd.0[0]`_2530| x_2524)
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (sum_2465 (|get.::.1_2529| x_2524))
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (|`List.for_all anon_fun.psd.0[0]`_2530| (|get.::.1_2529| x_2524))
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (sum_2465 (|get.::.1_2529| (|get.::.1_2529| x_2524)))
                                                                                      expansions
                                                                                      • unroll
                                                                                        expr
                                                                                        (|`List.for_all anon_fun.psd.0[0]`_2530|
                                                                                          (|get.::.1_2529| (|get.::.1_2529| x_2524)))
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (sum_2465 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|`List.for_all anon_fun.psd.0[0]`_2530|
                                                                                              (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524…
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                (sum_2…
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                  (|`Lis…
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                    (sum_2…
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                      (|`Lis…
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                        (sum_2…
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                          (|`Lis…
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                            (sum_2…
                                                                                                          expansions
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                              (|`Lis…
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                              (let ((a…
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                (let ((a…
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                  (let ((a…
                                                                                                                  expansions
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                    (let ((a…
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                      (let ((a…
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                        (let ((a…
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                          (let ((a…
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                            (let ((a…
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                              (let ((a…
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                (let ((a…
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                  (let ((a…
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                    (let ((a…
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                      (let ((a…
                                                                                                                                      expansions
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                        (let ((a…
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                          (let ((a…
                                                                                                                                          expansions
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                            (let ((a…
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                              (let ((a…
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                (let ((a…
                                                                                                                                                expansions
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                  (let ((a…
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                    (let ((a…
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                      (let ((a…
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                        (let ((a…
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                          (let ((a…
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                            (let ((a…
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                              (let ((a…
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                (let ((a…
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                  (let ((a…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                    (let ((a…
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                      (let ((a…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                        (let ((a…
                                                                                                                                                                        expansions
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                          (let ((a…
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                            (let ((a…
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                              (let ((a…
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                (let ((a…
                                                                                                                                                                                expansions
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                  (let ((a…
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                    (let ((a…
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                      (let ((a…
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                        (let ((a…
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                          (let ((a…
                                                                                                                                                                                          expansions
                                                                                                                                                                                          • unroll
                                                                                                                                                                                            expr
                                                                                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                            (let ((a…
                                                                                                                                                                                            expansions
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                              (let ((a…
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                (let ((a…
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unroll
                                                                                                                                                                                                  expr
                                                                                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                  (let ((a…
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                    expr
                                                                                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                    (let ((a…
                                                                                                                                                                                                    expansions
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr
                                                                                                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                      (let ((a…
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                        (let ((a…
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                          (let ((a…
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                            expr
                                                                                                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                            (let ((a…
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                              expr
                                                                                                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                              (let ((a…
                                                                                                                                                                                                              expansions
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr
                                                                                                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                (let ((a…
                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                  (let ((a…
                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                    (let ((a…
                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                      (let ((a…
                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                        (let ((a…
                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                          (let ((a…
                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                            (let ((a…
                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                              (let ((a…
                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                (let ((a…
                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                  (let ((a…
                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                    (let ((a…
                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                      (let ((a…
                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                        (let ((a…
                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                          (let ((a…
                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                            (let ((a…
                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                              (let ((a…
                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                (let ((a…
                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                  (let ((a…
                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                    (let ((a…
                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                      (let ((a…
                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                        (let ((a…
                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                          (let ((a…
                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                            (let ((a…
                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                              (let ((a…
                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                (let ((a…
                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                  (let ((a…
                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                    (let ((a…
                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                      (let ((a…
                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                        (let ((a…
                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                          (let ((a…
                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                            (let ((a…
                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                              (let ((a…
                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                                (let ((a…
                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                                  (let ((a…
                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| (|get.::.1_2529| x_2524))))))
                                                                                                                                                                                                                                                                                    (let ((a…
                                                                                                                                                                                                                                                                                    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]:
                                                                                                                                                                                                                                                                                    - : int list -> bool = <fun>
                                                                                                                                                                                                                                                                                    Goal:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    psd x ==> sum x >= 0.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    1 nontautological subgoal.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Subgoal 1:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     H0. List.for_all (fun x -> x >= 0) x
                                                                                                                                                                                                                                                                                    |---------------------------------------------------------------------------
                                                                                                                                                                                                                                                                                     sum x >= 0
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Verified up to bound 10 (after 0.023s).
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    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 sum.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Induction scheme:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x).
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    2 nontautological subgoals.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Subgoal 1.2:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     H0. x = []
                                                                                                                                                                                                                                                                                     H1. List.for_all (fun x -> x >= 0) x
                                                                                                                                                                                                                                                                                    |---------------------------------------------------------------------------
                                                                                                                                                                                                                                                                                     sum x >= 0
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    But simplification reduces this to true, using the definitions of
                                                                                                                                                                                                                                                                                    List.for_all and sum.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Subgoal 1.1:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     H0. not (x = [])
                                                                                                                                                                                                                                                                                     H1. List.for_all (fun x -> x >= 0) (List.tl x) ==> sum (List.tl x) >= 0
                                                                                                                                                                                                                                                                                     H2. List.for_all (fun x -> x >= 0) x
                                                                                                                                                                                                                                                                                    |---------------------------------------------------------------------------
                                                                                                                                                                                                                                                                                     sum x >= 0
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    But simplification reduces this to true, using the definitions of
                                                                                                                                                                                                                                                                                    List.for_all and sum.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Proved
                                                                                                                                                                                                                                                                                    proof
                                                                                                                                                                                                                                                                                    ground_instances0
                                                                                                                                                                                                                                                                                    definitions5
                                                                                                                                                                                                                                                                                    inductions1
                                                                                                                                                                                                                                                                                    search_time
                                                                                                                                                                                                                                                                                    0.077s
                                                                                                                                                                                                                                                                                    Expand
                                                                                                                                                                                                                                                                                    • start[0.077s, "Goal"]
                                                                                                                                                                                                                                                                                        List.for_all (fun x -> x >= 0) :var_0: ==> sum :var_0: >= 0
                                                                                                                                                                                                                                                                                    • subproof

                                                                                                                                                                                                                                                                                      not (List.for_all (fun x -> x >= 0) x) || sum x >= 0
                                                                                                                                                                                                                                                                                      • start[0.077s, "1"] not (List.for_all (fun x -> x >= 0) x) || sum x >= 0
                                                                                                                                                                                                                                                                                      • induction on (functional )
                                                                                                                                                                                                                                                                                        :scheme (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x)
                                                                                                                                                                                                                                                                                      • Split (((not (x = []) || not (List.for_all (fun x -> x >= 0) x))
                                                                                                                                                                                                                                                                                                || sum x >= 0)
                                                                                                                                                                                                                                                                                               && ((not
                                                                                                                                                                                                                                                                                                    (not (x = [])
                                                                                                                                                                                                                                                                                                     && (not (List.for_all (fun x -> x >= 0) (List.tl x))
                                                                                                                                                                                                                                                                                                         || sum (List.tl x) >= 0))
                                                                                                                                                                                                                                                                                                    || not (List.for_all (fun x -> x >= 0) x))
                                                                                                                                                                                                                                                                                                   || sum x >= 0)
                                                                                                                                                                                                                                                                                               :cases [(not (x = []) || not (List.for_all (fun x -> x >= 0) x))
                                                                                                                                                                                                                                                                                                       || sum x >= 0;
                                                                                                                                                                                                                                                                                                       ((x = []
                                                                                                                                                                                                                                                                                                         || not
                                                                                                                                                                                                                                                                                                            (not (List.for_all (fun x -> x >= 0) (List.tl x))
                                                                                                                                                                                                                                                                                                             || sum (List.tl x) >= 0))
                                                                                                                                                                                                                                                                                                        || not (List.for_all (fun x -> x >= 0) x))
                                                                                                                                                                                                                                                                                                       || sum x >= 0])
                                                                                                                                                                                                                                                                                        • subproof
                                                                                                                                                                                                                                                                                          ((x = [] || not (not (List.for_all (fun x -> x >= 0) (List.tl x)) || sum (List.tl x) >= 0)) || not (List.for_all (fun x -> x >= 0) x)) || sum x >= 0
                                                                                                                                                                                                                                                                                          • start[0.034s, "1.1"]
                                                                                                                                                                                                                                                                                              ((x = []
                                                                                                                                                                                                                                                                                                || not
                                                                                                                                                                                                                                                                                                   (not (List.for_all (fun x -> x >= 0) (List.tl x))
                                                                                                                                                                                                                                                                                                    || sum (List.tl x) >= 0))
                                                                                                                                                                                                                                                                                               || not (List.for_all (fun x -> x >= 0) x))
                                                                                                                                                                                                                                                                                              || sum x >= 0
                                                                                                                                                                                                                                                                                          • simplify
                                                                                                                                                                                                                                                                                            into
                                                                                                                                                                                                                                                                                            true
                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                            [List.for_all, sum, List.for_all]
                                                                                                                                                                                                                                                                                            rewrite_steps
                                                                                                                                                                                                                                                                                              forward_chaining
                                                                                                                                                                                                                                                                                            • subproof
                                                                                                                                                                                                                                                                                              (not (x = []) || not (List.for_all (fun x -> x >= 0) x)) || sum x >= 0
                                                                                                                                                                                                                                                                                              • start[0.034s, "1.2"]
                                                                                                                                                                                                                                                                                                  (not (x = []) || not (List.for_all (fun x -> x >= 0) 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!