Welcome to Imandra!

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

Imandra scope

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

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

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

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

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

Your first proof and counterexample

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

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

let f x =
  if x > 99 then
    100
  else if x < 70 && x > 23
  then 89 + x
  else if x > 20
  then g x + 20
  else if x > -2 then
    103
  else 99
Out[1]:
val g : 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.031s
details
Expand
smt_stats
rlimit count81
mk bool var5
num allocs2189125
memory6.050000
max memory6.350000
Expand
  • start[0.031s] (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_21 22) (+ 100 x_21) 9) 122))
              (a!3 (ite (<= x_21 22) (<= (+ 100 x_21)…

      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 : int end
      
      Counterexample (after 0 steps, 0.030s):
       let (x : int) = 69
      
      Refuted
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.030s
      details
      Expand
      smt_stats
      num checks1
      arith assert lower6
      rlimit count602
      mk clause28
      mk bool var18
      arith assert upper3
      decisions2
      propagations19
      conflicts1
      num allocs7581028
      final checks1
      memory9.090000
      max memory9.470000
      Expand
      • start[0.030s]
          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 : int) = 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]:
          - : int = 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_interactive.Decompose.t list =
          [<region>; <region>; <region>; <region>; <region>; <region>; <region>]
          
          Regions details

          No group selected.

          • Concrete regions are numbered
          • Unnumbered regions are groups whose children share a particular constraint
          • Click on a region to view its details
          • Double click on a region to zoom in on it
          • Shift+double click to zoom out
          • Hit escape to reset back to the top
          ConstraintsInvariant
          • not (x <= 99)
          100
          • x <= 99
          • 70 <= x
          • not (x <= 20)
          • not (x <= 22)
          29
          • x <= 99
          • not (70 <= x)
          • x <= 23
          • not (x <= 20)
          • not (x <= 22)
          29
          • x <= 99
          • not (70 <= x)
          • x <= 23
          • not (x <= 20)
          • x <= 22
          120 + x
          • x <= 99
          • not (70 <= x)
          • x <= 23
          • x <= 20
          • not (x <= -2)
          103
          • x <= 99
          • not (70 <= x)
          • x <= 23
          • x <= 20
          • x <= -2
          99
          • x <= 99
          • not (70 <= x)
          • not (x <= 23)
          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.014s
          details
          Expand
          smt_stats
          num checks8
          arith assert lower16
          arith pivots9
          rlimit count2429
          mk clause19
          datatype occurs check21
          mk bool var78
          arith assert upper14
          datatype splits3
          decisions14
          arith add rows18
          propagations14
          conflicts9
          arith fixed eqs7
          datatype accessor ax5
          arith conflicts2
          datatype constructor ax8
          num allocs1873581216
          final checks6
          added eqs50
          del clause8
          arith eq adapter11
          memory29.090000
          max memory81.500000
          Expand
          • start[0.014s]
              not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
              ==> List.tl x = []
                  || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
                     (Ordinal.Int (Ordinal.count x))
          • simplify
            into
            (not
             ((not (x = []) && Ordinal.count x >= 0) && Ordinal.count (List.tl x) >= 0)
             || List.tl x = [])
            || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
               (Ordinal.Int (Ordinal.count x))
            expansions
            []
            rewrite_steps
              forward_chaining
              • unroll
                expr
                (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`int list`_1222|
                                                      (…
                expansions
                • unroll
                  expr
                  (|count_`int list`_1222| (|get.::.1_1212| x_1213))
                  expansions
                  • unroll
                    expr
                    (|count_`int list`_1222| x_1213)
                    expansions
                    • unsat
                      (let ((a!1 (>= (ite (>= (|get.::.0_1211| x_1213) 0) (|get.::.0_1211| x_1213) 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 : int list end
                    
                    Instance (after 22 steps, 0.065s):
                     let (x : int list) =
                       [(-11365); 7719; 3067; 1142; (-29424); 8945; 1888; 8879; 590; 8586]
                    
                    Instance
                    proof attempt
                    ground_instances22
                    definitions0
                    inductions0
                    search_time
                    0.065s
                    details
                    Expand
                    smt_stats
                    arith offset eqs80
                    num checks45
                    arith assert lower222
                    arith pivots144
                    rlimit count29430
                    mk clause363
                    datatype occurs check280
                    mk bool var1569
                    arith assert upper213
                    datatype splits213
                    decisions438
                    arith add rows655
                    arith bound prop2
                    propagations647
                    interface eqs22
                    conflicts80
                    arith fixed eqs163
                    datatype accessor ax187
                    minimized lits1
                    arith conflicts16
                    arith assert diseq73
                    datatype constructor ax223
                    num allocs1928804605
                    final checks90
                    added eqs1814
                    del clause350
                    arith eq adapter224
                    memory32.990000
                    max memory81.500000
                    Expand
                    • start[0.065s]
                        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_24 x_28)
                          expansions
                          • unroll
                            expr
                            (|List.length_1229| x_28)
                            expansions
                            • unroll
                              expr
                              (sum_24 (|get.::.1_1228| x_28))
                              expansions
                              • unroll
                                expr
                                (|List.length_1229| (|get.::.1_1228| x_28))
                                expansions
                                • unroll
                                  expr
                                  (sum_24 (|get.::.1_1228| (|get.::.1_1228| x_28)))
                                  expansions
                                  • unroll
                                    expr
                                    (|List.length_1229| (|get.::.1_1228| (|get.::.1_1228| x_28)))
                                    expansions
                                    • unroll
                                      expr
                                      (sum_24 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))
                                      expansions
                                      • unroll
                                        expr
                                        (|List.length_1229| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                            (|List.l…
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                              (sum_24 …
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                (|List.l…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                  (sum_24 …
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                    (|List.l…
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                      (sum_24 …
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                        (|List.l…
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                          (sum_24 …
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                          (let ((a!2…
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                            (let ((a!2…
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                              (let ((a!2…
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                                (let ((a!2…
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                                  (let ((a!2…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| (|get.::.1_1228| x_28))))))
                                                                    (let ((a!2…
                                                                    expansions
                                                                    • Sat (Some let (x : int list) = [(-11365); 7719; 3067; 1142; (-29424); 8945; 1888; 8879; 590; 8586] )

                                                                    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 : int list end
                                                                    
                                                                    Counterexample (after 2 steps, 0.023s):
                                                                     let (x : int list) = [(-1)]
                                                                    
                                                                    Refuted
                                                                    proof attempt
                                                                    ground_instances2
                                                                    definitions0
                                                                    inductions0
                                                                    search_time
                                                                    0.023s
                                                                    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 allocs2009939042
                                                                    final checks6
                                                                    added eqs28
                                                                    del clause1
                                                                    arith eq adapter4
                                                                    memory33.140000
                                                                    max memory81.500000
                                                                    Expand
                                                                    • start[0.023s] sum :var_0: >= 0
                                                                    • unroll
                                                                      expr
                                                                      (sum_24 x_30)
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (sum_24 (|get.::.1_1238| x_30))
                                                                        expansions
                                                                        • Sat (Some let (x : int list) = [(-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
                                                                        • 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 x))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (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))))))))))))))))))))))))
                                                                        • 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)))))))))))))))))))))
                                                                        • 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 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 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (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 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 (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 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))))))))))))))))))))))
                                                                        • 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 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))))))))))))
                                                                        • 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 (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 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 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 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))))))))))))))
                                                                        • 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 x)))
                                                                        • List.for_all (fun x -> x >= 0) (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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))
                                                                        • List.for_all (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 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 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) 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 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 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 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 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))))))))))))))))))))))))))))))))))
                                                                        • 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 (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 x)))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 x))))))))))))))))))))))))))
                                                                        • sum (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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl x)))
                                                                        • sum (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 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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)))))))))))))))
                                                                        • 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 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 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 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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)))))))))))))))))))))))))))))))))))))))
                                                                        • 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 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)))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))))))
                                                                        • 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))))))))))))))))))))))))))))))))))))))
                                                                        blocked
                                                                        • 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))))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        proof attempt
                                                                        ground_instances100
                                                                        definitions0
                                                                        inductions0
                                                                        search_time
                                                                        0.362s
                                                                        Expand
                                                                        • start[0.362s] 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_24 x_39)
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (|`List.for_all anon_fun.psd.0[0]`_1230| x_39)
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (sum_24 (|get.::.1_1229| x_39))
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (|`List.for_all anon_fun.psd.0[0]`_1230| (|get.::.1_1229| x_39))
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (sum_24 (|get.::.1_1229| (|get.::.1_1229| x_39)))
                                                                                      expansions
                                                                                      • unroll
                                                                                        expr
                                                                                        (|`List.for_all anon_fun.psd.0[0]`_1230|
                                                                                          (|get.::.1_1229| (|get.::.1_1229| x_39)))
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (sum_24 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|`List.for_all anon_fun.psd.0[0]`_1230|
                                                                                              (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))…
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                (sum_24 …
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                  (|`List.…
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                    (sum_24 …
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                      (|`List.…
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                        (sum_24 …
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                          (|`List.…
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                            (sum_24 …
                                                                                                          expansions
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                              (|`List.…
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                              (let ((a!2…
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                (let ((a!2…
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                  (let ((a!2…
                                                                                                                  expansions
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                    (let ((a!2…
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                      (let ((a!2…
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                        (let ((a!2…
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                          (let ((a!2…
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                            (let ((a!2…
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                              (let ((a!2…
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                (let ((a!2…
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                  (let ((a!2…
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                    (let ((a!2…
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                      (let ((a!2…
                                                                                                                                      expansions
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                        (let ((a!2…
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                          (let ((a!2…
                                                                                                                                          expansions
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                            (let ((a!2…
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                              (let ((a!2…
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                (let ((a!2…
                                                                                                                                                expansions
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                  (let ((a!2…
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                    (let ((a!2…
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                      (let ((a!2…
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                        (let ((a!2…
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                          (let ((a!2…
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                            (let ((a!2…
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                              (let ((a!2…
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                (let ((a!2…
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                        expansions
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                expansions
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                          expansions
                                                                                                                                                                                          • unroll
                                                                                                                                                                                            expr
                                                                                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                            expansions
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unroll
                                                                                                                                                                                                  expr
                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                    expr
                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                    expansions
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr
                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                            expr
                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                              expr
                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                              expansions
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr
                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| (|get.::.1_1229| x_39))))))
                                                                                                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                                                                                                    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
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    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 definition of 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.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     Rules:
                                                                                                                                                                                                                                                                                        (:def List.for_all)
                                                                                                                                                                                                                                                                                        (:def sum)
                                                                                                                                                                                                                                                                                        (:induct sum)
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Proved
                                                                                                                                                                                                                                                                                    proof
                                                                                                                                                                                                                                                                                    ground_instances0
                                                                                                                                                                                                                                                                                    definitions3
                                                                                                                                                                                                                                                                                    inductions1
                                                                                                                                                                                                                                                                                    search_time
                                                                                                                                                                                                                                                                                    0.151s
                                                                                                                                                                                                                                                                                    Expand
                                                                                                                                                                                                                                                                                    • start[0.151s, "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.151s, "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.044s, "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]
                                                                                                                                                                                                                                                                                            rewrite_steps
                                                                                                                                                                                                                                                                                              forward_chaining
                                                                                                                                                                                                                                                                                            • subproof
                                                                                                                                                                                                                                                                                              (not (x = []) || not (List.for_all (fun x -> x >= 0) x)) || sum x >= 0
                                                                                                                                                                                                                                                                                              • start[0.044s, "1.2"]
                                                                                                                                                                                                                                                                                                  (not (x = []) || not (List.for_all (fun x -> x >= 0) x)) || sum x >= 0
                                                                                                                                                                                                                                                                                              • simplify
                                                                                                                                                                                                                                                                                                into
                                                                                                                                                                                                                                                                                                true
                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                sum
                                                                                                                                                                                                                                                                                                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!