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 -> int = <fun>
val f : int -> int = <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]:
- : int = 105
In [3]:
g 23017263820
Out[3]:
- : int = 9
In [4]:
f (- 1)
Out[4]:
- : int = 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.022s
details
Expand
smt_stats
rlimit count36
num allocs724552
time0.011000
memory5.460000
max memory5.460000
Expand
  • start[0.022s] (if ( :var_0: ) > 22 then 9 else (100 + ( :var_0: ))) <= 122
  • simplify

    into
    true
    expansions
    []
    rewrite_steps
      forward_chaining
      • Unsat

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

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

      In [7]:
      verify (fun x -> f x <> 158)
      
      Out[7]:
      - : int -> bool = <fun>
      module CX : sig val x : int end
      
      Counterexample (after 0 steps, 0.024s):
       let (x : int) = 69
      
      Refuted
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.024s
      details
      Expand
      smt_stats
      num checks1
      arith assert lower6
      rlimit count660
      mk clause28
      mk bool var12
      arith assert upper3
      decisions2
      propagations19
      conflicts1
      num allocs2642139
      final checks1
      time0.012000
      memory8.030000
      max memory8.340000
      Expand
      • start[0.024s]
          not
          ((if ( :var_0: ) > 99 then 100
            else
            if ( :var_0: ) < 70 && ( :var_0: ) > 23 then 89 + ( :var_0: )
            else
            if ( :var_0: ) > 20 then (if ( :var_0: ) > 22 then 9 else …) + 20
            else if ( :var_0: ) > -2 then 103 else 99)
           = 158)
      • simplify

        into
        not
        (( :var_0: ) <= 99
         && (if not (70 <= ( :var_0: )) && not (( :var_0: ) <= 23)
             then 89 + ( :var_0: )
             else
             if ( :var_0: ) <= 20 then if ( :var_0: ) <= -2 then 99 else 103
             else 20 + (if ( :var_0: ) <= 22 then … else 9))
            = 158)
        expansions
        []
        rewrite_steps
          forward_chaining
          • Sat (Some let (x : int) = 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]:
          - : int = 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]:
          - : int = 158
          

          Region Decomposition

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

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

          In [11]:
          Modular_decomp.top "f"
          
          Out[11]:
          - : Modular_decomposition.t =
          {Imandra_interactive.Modular_decomp.MD.md_session = 1i;
           md_f =
            {Imandra_surface.Uid.name = "f"; id = <abstr>; special_tag = <abstr>;
             namespace = <abstr>;
             chash = Some V7gqDTV4QAclxvM2x2wBCYJSzEyw4LY5X8nK6408tKw;
             depth = (4i, 1i)};
           md_args = [(x : int)]; md_regions = <abstr>}
          
          Regions details

          No group selected.

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

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

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

          Recursion and Induction

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

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

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

          Termination proof

          call `sum (List.tl x)` from `sum x`
          originalsum x
          subsum (List.tl x)
          original ordinalOrdinal.Int (_cnt x)
          sub ordinalOrdinal.Int (_cnt (List.tl x))
          path[not Is_a([], x)]
          proof
          detailed proof
          ground_instances3
          definitions0
          inductions0
          search_time
          0.014s
          details
          Expand
          smt_stats
          num checks8
          arith-make-feasible18
          arith-max-columns16
          arith-conflicts2
          rlimit count2024
          mk clause20
          datatype occurs check12
          mk bool var56
          arith-lower15
          arith-diseq1
          datatype splits1
          decisions15
          propagations14
          arith-max-rows4
          conflicts7
          datatype accessor ax7
          datatype constructor ax5
          num allocs7528349
          final checks4
          added eqs38
          del clause13
          arith eq adapter10
          arith-upper12
          memory8.530000
          max memory8.530000
          Expand
          • start[0.014s]
              let (_x_0 : int) = count.list mk_nat x in
              let (_x_1 : int list) = List.tl x in
              let (_x_2 : int) = count.list mk_nat _x_1 in
              not Is_a([], x) && _x_0 >= 0 && _x_2 >= 0
              ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
          • simplify
            into
            let (_x_0 : int list) = List.tl x in
            let (_x_1 : int) = count.list mk_nat _x_0 in
            let (_x_2 : int) = count.list mk_nat x in
            (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
            || not ((not Is_a([], x) && _x_2 >= 0) && _x_1 >= 0)
            expansions
            []
            rewrite_steps
              forward_chaining
              • unroll
                expr
                (|`count.list mk_nat[0]`_1698| x_1687)
                expansions
                • unroll
                  expr
                  (|`count.list mk_nat[0]`_1698| (|get.::.1_1686| x_1687))
                  expansions
                  • unroll
                    expr
                    (|Ordinal.<<_126| (|Ordinal.Int_111|
                                        (|`count.list mk_nat[0]`_1698| (|get.::.1_1…
                    expansions
                    • Unsat

                    In [13]:
                    sum []
                    
                    Out[13]:
                    - : int = 0
                    
                    In [14]:
                    sum [1;2;3]
                    
                    Out[14]:
                    - : int = 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]:
                    - : int list -> bool = <fun>
                    module CX : sig val x : int list end
                    
                    Instance (after 22 steps, 0.050s):
                     let (x : int list) = [27; 0; 0; 0; 0; 0; 0; 0; 0; 0]
                    
                    Instance
                    proof attempt
                    ground_instances22
                    definitions0
                    inductions0
                    search_time
                    0.050s
                    details
                    Expand
                    smt_stats
                    num checks45
                    arith-assume-eqs198
                    arith-make-feasible420
                    arith-max-columns100
                    arith-conflicts13
                    rlimit count21284
                    arith-cheap-eqs742
                    mk clause1018
                    datatype occurs check219
                    mk bool var1430
                    arith-lower314
                    arith-diseq36
                    datatype splits18
                    decisions539
                    arith-propagations11
                    propagations658
                    interface eqs198
                    arith-bound-propagations-cheap11
                    arith-max-rows60
                    conflicts52
                    datatype accessor ax101
                    minimized lits1
                    arith-bound-propagations-lp2
                    datatype constructor ax110
                    num allocs14620669
                    final checks239
                    added eqs1123
                    del clause942
                    arith eq adapter357
                    arith-upper353
                    time0.001000
                    memory9.480000
                    max memory9.480000
                    Expand
                    • start[0.050s]
                        let (_x_0 : int) = List.length ( :var_0: ) in
                        _x_0 >= 10 && sum ( :var_0: ) = _x_0 + 17
                    • simplify

                      into
                      let (_x_0 : int) = List.length ( :var_0: ) in
                      _x_0 >= 10 && sum ( :var_0: ) = 17 + _x_0
                      expansions
                      []
                      rewrite_steps
                        forward_chaining
                        • unroll
                          expr
                          (sum_24 x_30)
                          expansions
                          • unroll
                            expr
                            (|List.length_1730| x_30)
                            expansions
                            • unroll
                              expr
                              (sum_24 (|get.::.1_1729| x_30))
                              expansions
                              • unroll
                                expr
                                (|List.length_1730| (|get.::.1_1729| x_30))
                                expansions
                                • unroll
                                  expr
                                  (sum_24 (|get.::.1_1729| (|get.::.1_1729| x_30)))
                                  expansions
                                  • unroll
                                    expr
                                    (|List.length_1730| (|get.::.1_1729| (|get.::.1_1729| x_30)))
                                    expansions
                                    • unroll
                                      expr
                                      (sum_24 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))
                                      expansions
                                      • unroll
                                        expr
                                        (|List.length_1730| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                            (|List.l…
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                              (sum_24 …
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                (|List.l…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                  (sum_24 …
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                    (|List.l…
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                      (sum_24 …
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                        (|List.l…
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                          (sum_24 …
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                          (let ((a!2…
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                            (let ((a!2…
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                              (let ((a!2…
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                                (let ((a!2…
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                                  (let ((a!2…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| (|get.::.1_1729| x_30))))))
                                                                    (let ((a!2…
                                                                    expansions
                                                                    • Sat (Some let (x : int list) = [27; 0; 0; 0; 0; 0; 0; 0; 0; 0] )

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

                                                                    In [16]:
                                                                    List.length CX.x
                                                                    
                                                                    Out[16]:
                                                                    - : int = 10
                                                                    
                                                                    In [17]:
                                                                    sum CX.x
                                                                    
                                                                    Out[17]:
                                                                    - : int = 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]:
                                                                    - : int list -> bool = <fun>
                                                                    module CX : sig val x : int list end
                                                                    
                                                                    Counterexample (after 2 steps, 0.015s):
                                                                     let (x : int list) = [(-1)]
                                                                    
                                                                    Refuted
                                                                    proof attempt
                                                                    ground_instances2
                                                                    definitions0
                                                                    inductions0
                                                                    search_time
                                                                    0.015s
                                                                    details
                                                                    Expand
                                                                    smt_stats
                                                                    num checks5
                                                                    arith-make-feasible4
                                                                    arith-max-columns12
                                                                    rlimit count766
                                                                    arith-cheap-eqs1
                                                                    mk clause9
                                                                    datatype occurs check3
                                                                    mk bool var35
                                                                    arith-lower4
                                                                    datatype splits1
                                                                    decisions5
                                                                    propagations9
                                                                    arith-max-rows3
                                                                    conflicts2
                                                                    datatype accessor ax5
                                                                    datatype constructor ax5
                                                                    num allocs19734230
                                                                    final checks4
                                                                    added eqs29
                                                                    del clause1
                                                                    arith eq adapter4
                                                                    arith-upper3
                                                                    memory12.260000
                                                                    max memory12.260000
                                                                    Expand
                                                                    • start[0.015s] sum ( :var_0: ) >= 0
                                                                    • unroll
                                                                      expr
                                                                      (sum_24 x_32)
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (sum_24 (|get.::.1_1765| x_32))
                                                                        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]:
                                                                        - : int = -1
                                                                        

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

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

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

                                                                        In [21]:
                                                                        verify (fun x -> psd x ==> sum x >= 0)
                                                                        
                                                                        Out[21]:
                                                                        - : int list -> bool = <fun>
                                                                        
                                                                        Unknown (Verified up to bound 100)
                                                                        Expand
                                                                        expanded
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 (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 (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 x))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl 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 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 x)))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl x)))
                                                                        • sum (List.tl (List.tl x))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))
                                                                        • sum x
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (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 (List.tl (List.tl (List.tl (List.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 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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 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 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 (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))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl x)))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl 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 (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 (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 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 x)))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.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 x))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl 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 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))))))))))))))))))))
                                                                        • 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 (List.tl x))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl x)))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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 x)))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (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 (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (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))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))))))))))))
                                                                        • List.for_all (fun x -> x >= 0) x
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))))))))))))))))))))))))))))))))))
                                                                        • List.for_all (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)))))))))))))))))))))))))))))))))
                                                                        • sum (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))
                                                                        • List.for_all (fun x -> x >= 0) (List.tl 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.519s
                                                                        Expand
                                                                        • start[0.519s]
                                                                            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_38)
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (|`List.for_all anon_fun.psd.1[0]`_1709| x_38)
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (sum_24 (|get.::.1_1708| x_38))
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (|`List.for_all anon_fun.psd.1[0]`_1709| (|get.::.1_1708| x_38))
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (sum_24 (|get.::.1_1708| (|get.::.1_1708| x_38)))
                                                                                      expansions
                                                                                      • unroll
                                                                                        expr
                                                                                        (|`List.for_all anon_fun.psd.1[0]`_1709|
                                                                                          (|get.::.1_1708| (|get.::.1_1708| x_38)))
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (sum_24 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|`List.for_all anon_fun.psd.1[0]`_1709|
                                                                                              (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))…
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                (sum_24 …
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                  (|`List.…
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                    (sum_24 …
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                      (|`List.…
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                        (sum_24 …
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                          (|`List.…
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                            (sum_24 …
                                                                                                          expansions
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                              (|`List.…
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                              (let ((a!2…
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                (let ((a!2…
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                  (let ((a!2…
                                                                                                                  expansions
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                    (let ((a!2…
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                      (let ((a!2…
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                        (let ((a!2…
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                          (let ((a!2…
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                            (let ((a!2…
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                              (let ((a!2…
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                (let ((a!2…
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                  (let ((a!2…
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                    (let ((a!2…
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                      (let ((a!2…
                                                                                                                                      expansions
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                        (let ((a!2…
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                          (let ((a!2…
                                                                                                                                          expansions
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                            (let ((a!2…
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                              (let ((a!2…
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                (let ((a!2…
                                                                                                                                                expansions
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                  (let ((a!2…
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                    (let ((a!2…
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                      (let ((a!2…
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                        (let ((a!2…
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                          (let ((a!2…
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                            (let ((a!2…
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                              (let ((a!2…
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                (let ((a!2…
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                        expansions
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                expansions
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                          expansions
                                                                                                                                                                                          • unroll
                                                                                                                                                                                            expr
                                                                                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                            expansions
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unroll
                                                                                                                                                                                                  expr
                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                    expr
                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                    expansions
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr
                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                            expr
                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                              expr
                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                              expansions
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr
                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                    (let ((a!2…
                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                      (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                      (let ((a!2…
                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                        (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                        (let ((a!2…
                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                          (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                          (let ((a!2…
                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                            (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                            (let ((a!2…
                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                              (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                              (let ((a!2…
                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                                (let ((a!2…
                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                  (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                                  (let ((a!2…
                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                    (let ((a!1 (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| (|get.::.1_1708| x_38))))))
                                                                                                                                                                                                                                                                                    (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 List.for_all.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Induction scheme:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     (Is_a([], x) ==> φ x) && (not Is_a([], x) && φ (List.tl x) ==> φ x).
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    2 nontautological subgoals.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Subgoal 1.2:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     H0. List.for_all (fun x -> x >= 0) x
                                                                                                                                                                                                                                                                                     H1. Is_a([], x)
                                                                                                                                                                                                                                                                                    |---------------------------------------------------------------------------
                                                                                                                                                                                                                                                                                     sum x >= 0
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    But simplification reduces this to true, using the definition of sum.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Subgoal 1.1:
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     H0. List.for_all (fun x -> x >= 0) x
                                                                                                                                                                                                                                                                                     H1. not Is_a([], x)
                                                                                                                                                                                                                                                                                     H2. List.for_all (fun x -> x >= 0) (List.tl x) ==> sum (List.tl x) >= 0
                                                                                                                                                                                                                                                                                    |---------------------------------------------------------------------------
                                                                                                                                                                                                                                                                                     sum x >= 0
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    But simplification reduces this to true, using the definitions of
                                                                                                                                                                                                                                                                                    List.for_all and sum.
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                     Rules:
                                                                                                                                                                                                                                                                                        (:def List.for_all)
                                                                                                                                                                                                                                                                                        (:def sum)
                                                                                                                                                                                                                                                                                        (:induct List.for_all)
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                    Proved
                                                                                                                                                                                                                                                                                    proof
                                                                                                                                                                                                                                                                                    ground_instances0
                                                                                                                                                                                                                                                                                    definitions5
                                                                                                                                                                                                                                                                                    inductions1
                                                                                                                                                                                                                                                                                    search_time
                                                                                                                                                                                                                                                                                    0.219s
                                                                                                                                                                                                                                                                                    Expand
                                                                                                                                                                                                                                                                                    • start[0.219s, "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.219s, "1"] not (List.for_all (fun x -> x >= 0) x) || sum x >= 0
                                                                                                                                                                                                                                                                                      • induction on (functional )
                                                                                                                                                                                                                                                                                        :scheme (Is_a([], x) ==> φ x)
                                                                                                                                                                                                                                                                                                && (not Is_a([], x) && φ (List.tl x) ==> φ x)
                                                                                                                                                                                                                                                                                      • Split (let (_x_0 : bool)
                                                                                                                                                                                                                                                                                                   = not (List.for_all (fun x -> x >= 0) x) || sum x >= 0
                                                                                                                                                                                                                                                                                               in
                                                                                                                                                                                                                                                                                               let (_x_1 : bool) = not Is_a([], x) in
                                                                                                                                                                                                                                                                                               let (_x_2 : int list) = List.tl x in
                                                                                                                                                                                                                                                                                               (_x_0 || _x_1)
                                                                                                                                                                                                                                                                                               && (_x_0
                                                                                                                                                                                                                                                                                                   || not
                                                                                                                                                                                                                                                                                                      (_x_1
                                                                                                                                                                                                                                                                                                       && (not (List.for_all (fun x -> x >= 0) _x_2) || sum _x_2 >= 0)))
                                                                                                                                                                                                                                                                                               :cases [(not (List.for_all (fun x -> x >= 0) x) || not Is_a([], x))
                                                                                                                                                                                                                                                                                                       || sum x >= 0;
                                                                                                                                                                                                                                                                                                       let (_x_0 : int list) = List.tl x in
                                                                                                                                                                                                                                                                                                       ((not (List.for_all (fun x -> x >= 0) x) || Is_a([], x))
                                                                                                                                                                                                                                                                                                        || not
                                                                                                                                                                                                                                                                                                           (List.for_all (fun x -> x >= 0) _x_0 ==> sum _x_0 >= 0))
                                                                                                                                                                                                                                                                                                       || sum x >= 0])
                                                                                                                                                                                                                                                                                        • subproof
                                                                                                                                                                                                                                                                                          let (_x_0 : int list) = List.tl x in ((not (List.for_all (fun x -> x >= 0) x) || Is_a([], x)) || not (List.for_all (fun x -> x >= 0) _x_0 ==> sum _x_0 >= 0)) || sum x >= 0
                                                                                                                                                                                                                                                                                          • start[0.133s, "1.1"]
                                                                                                                                                                                                                                                                                              let (_x_0 : int list) = List.tl x in
                                                                                                                                                                                                                                                                                              ((not (List.for_all (fun x -> x >= 0) x) || Is_a([], x))
                                                                                                                                                                                                                                                                                               || not (List.for_all (fun x -> x >= 0) _x_0 ==> sum _x_0 >= 0))
                                                                                                                                                                                                                                                                                              || sum x >= 0
                                                                                                                                                                                                                                                                                          • simplify
                                                                                                                                                                                                                                                                                            into
                                                                                                                                                                                                                                                                                            true
                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                            [List.for_all, sum, List.for_all, sum]
                                                                                                                                                                                                                                                                                            rewrite_steps
                                                                                                                                                                                                                                                                                              forward_chaining
                                                                                                                                                                                                                                                                                            • subproof
                                                                                                                                                                                                                                                                                              (not (List.for_all (fun x -> x >= 0) x) || not Is_a([], x)) || sum x >= 0
                                                                                                                                                                                                                                                                                              • start[0.133s, "1.2"]
                                                                                                                                                                                                                                                                                                  (not (List.for_all (fun x -> x >= 0) x) || not Is_a([], 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!