Unrolling

The first tool that Imandra makes available in our verification toolbox is recursive function unrolling, a form of bounded model checking backed by Satisfiability Modulo Theories (SMT) solving. This technique is completely automatic, and is in general not influenced by the presence of proved rules or enabled/disabled functions (except with used in conjunction with the [@@simp] attribute).

Completeness

For many classes of problems, unrolling is "complete" in various senses. For example, for goals involving only non-recursive functions, algebraic datatypes and linear arithmetic, unrolling will always be able to prove a true goal or refute a false goal in a finite amount of time and space. Moreover, for an even wider class of problems involving recursive functions, datatypes and arithmetic, unrolling is "complete for counterexamples." This means that if a counterexample to a goal exists, unrolling will in principle always be able to synthesize one. This relies on Imandra's "fair" strategy for incrementally expanding the "interpretation call-graph" of a goal.

That said, part of the beauty of unrolling is that you don't need to understand it to apply it!

Strategy

In general, it's recommended to apply unrolling to a goal before you attempt other methods such as the inductive waterfall ([@@auto]). It's amazing how often seemingly true goals are false due to subtle edge cases, and the ability of unrolling to construct concrete counterexamples can be an invaluable filter on your conjectures.

Examples

To use unrolling, we simply use the verify or instance commands.

Let's use unrolling to find an instance of two lists of integers, whose sum equals the length of the two lists concatenated. We shall constrain the total length of the two lists to be positive (for fun, at least 10), so we obtain something more interesting than the simple x=[],y=[] solution!

In [1]:
instance
  (fun x y -> List.length (x@y) > 10
    && List.fold_left (+) 0 (x@y) = List.length (x@y))
Out[1]:
- : int list -> int list -> bool = <fun>
module CX : sig val x : int list val y : int list end
Instance (after 31 steps, 0.103s):
 let (x : int list) = []
 let (y : int list) =
  [11770; 38; 138473; (-30612); (-28100); (-8945); (-17677); 14680; (-18457);
   (-28881); (-32278)]
Instance
proof attempt
ground_instances31
definitions0
inductions0
search_time
0.103s
details
Expand
smt_stats
num checks63
arith-make-feasible75
arith-max-columns65
arith-conflicts20
rlimit count19929
arith-cheap-eqs3
mk clause164
datatype occurs check132
mk bool var664
arith-lower71
arith-diseq23
datatype splits16
decisions481
arith-propagations1
propagations324
arith-bound-propagations-cheap1
arith-max-rows36
conflicts52
datatype accessor ax83
datatype constructor ax174
num allocs973172
final checks46
added eqs1258
del clause134
arith eq adapter94
arith-upper94
memory5.720000
max memory5.720000
Expand
  • start[0.103s]
      let (_x_0 : int list) = List.append ( :var_0: ) ( :var_1: ) in
      let (_x_1 : int) = List.length _x_0 in
      _x_1 > 10 && List.fold_left ( + ) 0 _x_0 = _x_1
  • simplify

    into
    let (_x_0 : int list) = List.append ( :var_0: ) ( :var_1: ) in
    let (_x_1 : int) = List.length _x_0 in
    not (_x_1 <= 10) && List.fold_left ( + ) 0 _x_0 = _x_1
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`List.fold_left ( + )[0]`_1646| 0 (|List.append_1637| x_14 y_15))
        expansions
        • unroll
          expr
          (|List.append_1637| x_14 y_15)
          expansions
          • unroll
            expr
            (|List.length_1642| (|List.append_1637| x_14 y_15))
            expansions
            • unroll
              expr
              (|`List.fold_left ( + )[0]`_1646|
                (|get.::.0_1635| (|List.append_1637| x_14 y_15))
                (|get.::.1_16…
              expansions
              • unroll
                expr
                (|List.append_1637| (|get.::.1_1636| x_14) y_15)
                expansions
                • unroll
                  expr
                  (|List.length_1642| (|get.::.1_1636| (|List.append_1637| x_14 y_15)))
                  expansions
                  • unroll
                    expr
                    (let ((a!1 (+ (|get.::.0_1635| (|List.append_1637| x_14 y_15))
                                  (|get.::.0_1635| (|get.…
                    expansions
                    • unroll
                      expr
                      (|List.length_1642|
                        (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637| x_14 y_15))))
                      expansions
                      • unroll
                        expr
                        (let ((a!1 (|get.::.0_1635| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                          …
                        expansions
                        • unroll
                          expr
                          (|List.append_1637| (|get.::.1_1636| (|get.::.1_1636| x_14)) y_15)
                          expansions
                          • unroll
                            expr
                            (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                              …
                            expansions
                            • unroll
                              expr
                              (let ((a!1 (|get.::.0_1635| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                …
                              expansions
                              • unroll
                                expr
                                (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                  …
                                expansions
                                • unroll
                                  expr
                                  (let ((a!1 (|get.::.0_1635| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                    …
                                  expansions
                                  • unroll
                                    expr
                                    (|List.append_1637|
                                      (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| x_14)))
                                      y_15)
                                    expansions
                                    • unroll
                                      expr
                                      (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                        …
                                      expansions
                                      • unroll
                                        expr
                                        (let ((a!1 (|get.::.0_1635| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                          …
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                            …
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|get.::.0_1635| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                              …
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| x_14))))))
                                                (|List.a…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                                  …
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|get.::.0_1635| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                                    …
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                                      …
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (let ((a!1 (|get.::.0_1635| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                                        …
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| x_14))))))
                                                          (|List.a…
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                                            …
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (let ((a!1 (|get.::.0_1635| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                                              …
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                                                …
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (let ((a!1 (|get.::.0_1635| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                                                  …
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| x_14))))))
                                                                    (|List.a…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (|get.::.1_1636| (|get.::.1_1636| (|get.::.1_1636| (|List.append_1637|
                                                                                      …
                                                                    expansions
                                                                    • Sat (Some let (x : int list) = [] let (y : int list) = [11770; 38; 138473; (-30612); (-28100); (-8945); (-17677); 14680; (-18457); (-28881); (-32278)] )

                                                                    Imandra was able to find a solution instantly, and reflected it into our runtime in the CX module. Let's compute with it to better understand it:

                                                                    In [2]:
                                                                    List.length (CX.x@CX.y);;
                                                                    List.fold_left (+) 0 (CX.x@CX.y);;
                                                                    
                                                                    Out[2]:
                                                                    - : int = 11
                                                                    - : int = 11
                                                                    

                                                                    Unrolling limits

                                                                    Unrolling works by creating a symbolic call graph for the negation of the goal we've asked Imandra to verify (or dually the positive version of the goal in the case of instance), and by iteratively extending this graph with incremental interpretations of recursive functions, up to a given unrolling bound, checking at each step for satisfiability.

                                                                    The unrolling bound defaults to 100 and can be controlled globally using the #unroll <n> directive, or local to a given verify or instance call using the ~upto:<n> parameter.

                                                                    If at any step of the unrolling process the negation of our original goal is satisfiable w.r.t. the interpreted approximations of the recursive functions, then Imandra has found a counterexample for our original goal, which has thus been refuted. In this case, Imandra will report Counterexample (after m steps) and install the found counterexample in the CX module.

                                                                    If, on the other hand, Imandra is able to prove that there is no counterexample in a manner that is independent of the bound on the approximations, then our original goal is indeed a theorem valid for all possible inputs, and Imandra will report Theorem Proved. This can always be done for a wide class of theorems on catamorphisms (e.g., List.fold_right), for example.

                                                                    Otherwise, if Imandra failed to find a counterexample or proof and stopped unrolling at the unrolling bound, we obtain a weaker result of the form Unknown (verified up to depth k), which effectively means: this may or may not be a theorem, but there are no counterexamples up to depth k. Such bounded results can nevertheless be very useful.

                                                                    Let's try to understand in practice how the unrolling bound plays into unrolling. Consider this simple function that recursively decreases an integer until it reaches 0, then returns 1:

                                                                    In [3]:
                                                                    let rec f x =
                                                                      if x <= 0 then
                                                                        1
                                                                      else
                                                                        f (x - 1)
                                                                    
                                                                    Out[3]:
                                                                    val f : int -> int = <fun>
                                                                    
                                                                    termination proof

                                                                    Termination proof

                                                                    call `f (x - 1)` from `f x`
                                                                    originalf x
                                                                    subf (x - 1)
                                                                    original ordinalOrdinal.Int (_cnt x)
                                                                    sub ordinalOrdinal.Int (_cnt (x - 1))
                                                                    path[not (x <= 0)]
                                                                    proof
                                                                    detailed proof
                                                                    ground_instances1
                                                                    definitions0
                                                                    inductions0
                                                                    search_time
                                                                    0.022s
                                                                    details
                                                                    Expand
                                                                    smt_stats
                                                                    num checks3
                                                                    arith-make-feasible5
                                                                    arith-max-columns11
                                                                    arith-conflicts1
                                                                    rlimit count987
                                                                    mk clause5
                                                                    datatype occurs check2
                                                                    mk bool var18
                                                                    arith-lower3
                                                                    decisions2
                                                                    arith-propagations3
                                                                    propagations2
                                                                    arith-bound-propagations-cheap3
                                                                    arith-max-rows4
                                                                    conflicts2
                                                                    datatype accessor ax2
                                                                    num allocs3453611
                                                                    final checks1
                                                                    added eqs6
                                                                    del clause5
                                                                    arith eq adapter2
                                                                    arith-upper6
                                                                    memory8.530000
                                                                    max memory8.530000
                                                                    Expand
                                                                    • start[0.022s]
                                                                        let (_x_0 : int) = if x >= 0 then x else 0 in
                                                                        let (_x_1 : int) = x - 1 in
                                                                        let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
                                                                        not (x <= 0) && _x_0 >= 0 && _x_2 >= 0
                                                                        ==> _x_1 <= 0 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                    • simplify
                                                                      into
                                                                      (x <= 0 || x <= 1)
                                                                      || Ordinal.( << ) (Ordinal.Int (if x >= 1 then -1 + x else 0))
                                                                         (Ordinal.Int (if x >= 0 then x else 0))
                                                                      expansions
                                                                      []
                                                                      rewrite_steps
                                                                        forward_chaining
                                                                        • unroll
                                                                          expr
                                                                          (|Ordinal.<<_119| (|Ordinal.Int_108| (ite (>= x_1918 1) (+ (- 1) x_1918) 0))
                                                                                            (|Ord…
                                                                          expansions
                                                                          • Unsat

                                                                          Let's verify that for all x < 100, the function will return 1:

                                                                          In [4]:
                                                                          verify (fun x -> x < 100 ==> f x = 1)
                                                                          
                                                                          Out[4]:
                                                                          - : int -> bool = <fun>
                                                                          
                                                                          Proved
                                                                          proof
                                                                          ground_instances100
                                                                          definitions0
                                                                          inductions0
                                                                          search_time
                                                                          0.512s
                                                                          details
                                                                          Expand
                                                                          smt_stats
                                                                          num checks201
                                                                          arith-make-feasible200
                                                                          arith-max-columns104
                                                                          rlimit count34098
                                                                          arith-cheap-eqs2
                                                                          mk clause300
                                                                          mk bool var504
                                                                          arith-lower1
                                                                          arith-propagations98
                                                                          propagations297
                                                                          arith-bound-propagations-cheap98
                                                                          arith-max-rows99
                                                                          conflicts101
                                                                          num allocs12840067
                                                                          final checks100
                                                                          added eqs301
                                                                          del clause297
                                                                          arith-upper99
                                                                          memory10.720000
                                                                          max memory10.720000
                                                                          Expand
                                                                          • start[0.512s] ( :var_0: ) < 100 ==> f ( :var_0: ) = 1
                                                                          • simplify

                                                                            into
                                                                            100 <= ( :var_0: ) || f ( :var_0: ) = 1
                                                                            expansions
                                                                            []
                                                                            rewrite_steps
                                                                              forward_chaining
                                                                              • unroll
                                                                                expr
                                                                                (f_17 x_19)
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (f_17 (+ (- 1) x_19))
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (f_17 (+ (- 2) x_19))
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (f_17 (+ (- 3) x_19))
                                                                                      expansions
                                                                                      • unroll
                                                                                        expr
                                                                                        (f_17 (+ (- 4) x_19))
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (f_17 (+ (- 5) x_19))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (f_17 (+ (- 6) x_19))
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (f_17 (+ (- 7) x_19))
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (f_17 (+ (- 8) x_19))
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (f_17 (+ (- 9) x_19))
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (f_17 (+ (- 10) x_19))
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (f_17 (+ (- 11) x_19))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (f_17 (+ (- 12) x_19))
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (f_17 (+ (- 13) x_19))
                                                                                                          expansions
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (f_17 (+ (- 14) x_19))
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (f_17 (+ (- 15) x_19))
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (f_17 (+ (- 16) x_19))
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (f_17 (+ (- 17) x_19))
                                                                                                                  expansions
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (f_17 (+ (- 18) x_19))
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (f_17 (+ (- 19) x_19))
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (f_17 (+ (- 20) x_19))
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (f_17 (+ (- 21) x_19))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (f_17 (+ (- 22) x_19))
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (f_17 (+ (- 23) x_19))
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (f_17 (+ (- 24) x_19))
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (f_17 (+ (- 25) x_19))
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (f_17 (+ (- 26) x_19))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (f_17 (+ (- 27) x_19))
                                                                                                                                      expansions
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (f_17 (+ (- 28) x_19))
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (f_17 (+ (- 29) x_19))
                                                                                                                                          expansions
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (f_17 (+ (- 30) x_19))
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (f_17 (+ (- 31) x_19))
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (f_17 (+ (- 32) x_19))
                                                                                                                                                expansions
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (f_17 (+ (- 33) x_19))
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (f_17 (+ (- 34) x_19))
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (f_17 (+ (- 35) x_19))
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (f_17 (+ (- 36) x_19))
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (f_17 (+ (- 37) x_19))
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (f_17 (+ (- 38) x_19))
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (f_17 (+ (- 39) x_19))
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (f_17 (+ (- 40) x_19))
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (f_17 (+ (- 41) x_19))
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (f_17 (+ (- 42) x_19))
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (f_17 (+ (- 43) x_19))
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (f_17 (+ (- 44) x_19))
                                                                                                                                                                        expansions
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (f_17 (+ (- 45) x_19))
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (f_17 (+ (- 46) x_19))
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (f_17 (+ (- 47) x_19))
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (f_17 (+ (- 48) x_19))
                                                                                                                                                                                expansions
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (f_17 (+ (- 49) x_19))
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (f_17 (+ (- 50) x_19))
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (f_17 (+ (- 51) x_19))
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (f_17 (+ (- 52) x_19))
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (f_17 (+ (- 53) x_19))
                                                                                                                                                                                          expansions
                                                                                                                                                                                          • unroll
                                                                                                                                                                                            expr
                                                                                                                                                                                            (f_17 (+ (- 54) x_19))
                                                                                                                                                                                            expansions
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (f_17 (+ (- 55) x_19))
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (f_17 (+ (- 56) x_19))
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unroll
                                                                                                                                                                                                  expr
                                                                                                                                                                                                  (f_17 (+ (- 57) x_19))
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                    expr
                                                                                                                                                                                                    (f_17 (+ (- 58) x_19))
                                                                                                                                                                                                    expansions
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr
                                                                                                                                                                                                      (f_17 (+ (- 59) x_19))
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (f_17 (+ (- 60) x_19))
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (f_17 (+ (- 61) x_19))
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                            expr
                                                                                                                                                                                                            (f_17 (+ (- 62) x_19))
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                              expr
                                                                                                                                                                                                              (f_17 (+ (- 63) x_19))
                                                                                                                                                                                                              expansions
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr
                                                                                                                                                                                                                (f_17 (+ (- 64) x_19))
                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                  (f_17 (+ (- 65) x_19))
                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                    (f_17 (+ (- 66) x_19))
                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                      (f_17 (+ (- 67) x_19))
                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                        (f_17 (+ (- 68) x_19))
                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                          (f_17 (+ (- 69) x_19))
                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                            (f_17 (+ (- 70) x_19))
                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                              (f_17 (+ (- 71) x_19))
                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                (f_17 (+ (- 72) x_19))
                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                  (f_17 (+ (- 73) x_19))
                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                    (f_17 (+ (- 74) x_19))
                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                      (f_17 (+ (- 75) x_19))
                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                        (f_17 (+ (- 76) x_19))
                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                          (f_17 (+ (- 77) x_19))
                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                            (f_17 (+ (- 78) x_19))
                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                              (f_17 (+ (- 79) x_19))
                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                (f_17 (+ (- 80) x_19))
                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                  (f_17 (+ (- 81) x_19))
                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                    (f_17 (+ (- 82) x_19))
                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                      (f_17 (+ (- 83) x_19))
                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                        (f_17 (+ (- 84) x_19))
                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                          (f_17 (+ (- 85) x_19))
                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                            (f_17 (+ (- 86) x_19))
                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                              (f_17 (+ (- 87) x_19))
                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                (f_17 (+ (- 88) x_19))
                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                  (f_17 (+ (- 89) x_19))
                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                    (f_17 (+ (- 90) x_19))
                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                      (f_17 (+ (- 91) x_19))
                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                        (f_17 (+ (- 92) x_19))
                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                          (f_17 (+ (- 93) x_19))
                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                            (f_17 (+ (- 94) x_19))
                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                              (f_17 (+ (- 95) x_19))
                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                (f_17 (+ (- 96) x_19))
                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                  (f_17 (+ (- 97) x_19))
                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                    (f_17 (+ (- 98) x_19))
                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                      (f_17 (+ (- 99) x_19))
                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                      • Unsat

                                                                                                                                                                                                                                                                                      But watch what happens if we ask Imandra to verify this for x < 101, thus exceding the number of recursive calls that Imandra unrolls by default:

                                                                                                                                                                                                                                                                                      In [5]:
                                                                                                                                                                                                                                                                                      verify (fun x -> x < 101 ==> f x = 1)
                                                                                                                                                                                                                                                                                      
                                                                                                                                                                                                                                                                                      Out[5]:
                                                                                                                                                                                                                                                                                      - : int -> bool = <fun>
                                                                                                                                                                                                                                                                                      
                                                                                                                                                                                                                                                                                      Unknown (Verified up to bound 100)
                                                                                                                                                                                                                                                                                      Expand
                                                                                                                                                                                                                                                                                      expanded
                                                                                                                                                                                                                                                                                      • f (-54 + x)
                                                                                                                                                                                                                                                                                      • f (-92 + x)
                                                                                                                                                                                                                                                                                      • f (-5 + x)
                                                                                                                                                                                                                                                                                      • f (-79 + x)
                                                                                                                                                                                                                                                                                      • f (-1 + x)
                                                                                                                                                                                                                                                                                      • f (-97 + x)
                                                                                                                                                                                                                                                                                      • f (-84 + x)
                                                                                                                                                                                                                                                                                      • f (-93 + x)
                                                                                                                                                                                                                                                                                      • f (-71 + x)
                                                                                                                                                                                                                                                                                      • f (-94 + x)
                                                                                                                                                                                                                                                                                      • f x
                                                                                                                                                                                                                                                                                      • f (-85 + x)
                                                                                                                                                                                                                                                                                      • f (-60 + x)
                                                                                                                                                                                                                                                                                      • f (-43 + x)
                                                                                                                                                                                                                                                                                      • f (-78 + x)
                                                                                                                                                                                                                                                                                      • f (-47 + x)
                                                                                                                                                                                                                                                                                      • f (-51 + x)
                                                                                                                                                                                                                                                                                      • f (-53 + x)
                                                                                                                                                                                                                                                                                      • f (-8 + x)
                                                                                                                                                                                                                                                                                      • f (-59 + x)
                                                                                                                                                                                                                                                                                      • f (-30 + x)
                                                                                                                                                                                                                                                                                      • f (-6 + x)
                                                                                                                                                                                                                                                                                      • f (-15 + x)
                                                                                                                                                                                                                                                                                      • f (-40 + x)
                                                                                                                                                                                                                                                                                      • f (-29 + x)
                                                                                                                                                                                                                                                                                      • f (-22 + x)
                                                                                                                                                                                                                                                                                      • f (-10 + x)
                                                                                                                                                                                                                                                                                      • f (-4 + x)
                                                                                                                                                                                                                                                                                      • f (-75 + x)
                                                                                                                                                                                                                                                                                      • f (-38 + x)
                                                                                                                                                                                                                                                                                      • f (-24 + x)
                                                                                                                                                                                                                                                                                      • f (-45 + x)
                                                                                                                                                                                                                                                                                      • f (-19 + x)
                                                                                                                                                                                                                                                                                      • f (-73 + x)
                                                                                                                                                                                                                                                                                      • f (-83 + x)
                                                                                                                                                                                                                                                                                      • f (-82 + x)
                                                                                                                                                                                                                                                                                      • f (-48 + x)
                                                                                                                                                                                                                                                                                      • f (-68 + x)
                                                                                                                                                                                                                                                                                      • f (-67 + x)
                                                                                                                                                                                                                                                                                      • f (-21 + x)
                                                                                                                                                                                                                                                                                      • f (-98 + x)
                                                                                                                                                                                                                                                                                      • f (-50 + x)
                                                                                                                                                                                                                                                                                      • f (-14 + x)
                                                                                                                                                                                                                                                                                      • f (-69 + x)
                                                                                                                                                                                                                                                                                      • f (-81 + x)
                                                                                                                                                                                                                                                                                      • f (-58 + x)
                                                                                                                                                                                                                                                                                      • f (-17 + x)
                                                                                                                                                                                                                                                                                      • f (-64 + x)
                                                                                                                                                                                                                                                                                      • f (-44 + x)
                                                                                                                                                                                                                                                                                      • f (-96 + x)
                                                                                                                                                                                                                                                                                      • f (-32 + x)
                                                                                                                                                                                                                                                                                      • f (-23 + x)
                                                                                                                                                                                                                                                                                      • f (-2 + x)
                                                                                                                                                                                                                                                                                      • f (-52 + x)
                                                                                                                                                                                                                                                                                      • f (-28 + x)
                                                                                                                                                                                                                                                                                      • f (-70 + x)
                                                                                                                                                                                                                                                                                      • f (-49 + x)
                                                                                                                                                                                                                                                                                      • f (-72 + x)
                                                                                                                                                                                                                                                                                      • f (-74 + x)
                                                                                                                                                                                                                                                                                      • f (-36 + x)
                                                                                                                                                                                                                                                                                      • f (-87 + x)
                                                                                                                                                                                                                                                                                      • f (-56 + x)
                                                                                                                                                                                                                                                                                      • f (-55 + x)
                                                                                                                                                                                                                                                                                      • f (-33 + x)
                                                                                                                                                                                                                                                                                      • f (-11 + x)
                                                                                                                                                                                                                                                                                      • f (-95 + x)
                                                                                                                                                                                                                                                                                      • f (-20 + x)
                                                                                                                                                                                                                                                                                      • f (-12 + x)
                                                                                                                                                                                                                                                                                      • f (-88 + x)
                                                                                                                                                                                                                                                                                      • f (-65 + x)
                                                                                                                                                                                                                                                                                      • f (-39 + x)
                                                                                                                                                                                                                                                                                      • f (-25 + x)
                                                                                                                                                                                                                                                                                      • f (-91 + x)
                                                                                                                                                                                                                                                                                      • f (-35 + x)
                                                                                                                                                                                                                                                                                      • f (-7 + x)
                                                                                                                                                                                                                                                                                      • f (-90 + x)
                                                                                                                                                                                                                                                                                      • f (-77 + x)
                                                                                                                                                                                                                                                                                      • f (-57 + x)
                                                                                                                                                                                                                                                                                      • f (-26 + x)
                                                                                                                                                                                                                                                                                      • f (-86 + x)
                                                                                                                                                                                                                                                                                      • f (-62 + x)
                                                                                                                                                                                                                                                                                      • f (-42 + x)
                                                                                                                                                                                                                                                                                      • f (-9 + x)
                                                                                                                                                                                                                                                                                      • f (-16 + x)
                                                                                                                                                                                                                                                                                      • f (-76 + x)
                                                                                                                                                                                                                                                                                      • f (-61 + x)
                                                                                                                                                                                                                                                                                      • f (-18 + x)
                                                                                                                                                                                                                                                                                      • f (-46 + x)
                                                                                                                                                                                                                                                                                      • f (-37 + x)
                                                                                                                                                                                                                                                                                      • f (-31 + x)
                                                                                                                                                                                                                                                                                      • f (-99 + x)
                                                                                                                                                                                                                                                                                      • f (-34 + x)
                                                                                                                                                                                                                                                                                      • f (-27 + x)
                                                                                                                                                                                                                                                                                      • f (-80 + x)
                                                                                                                                                                                                                                                                                      • f (-66 + x)
                                                                                                                                                                                                                                                                                      • f (-89 + x)
                                                                                                                                                                                                                                                                                      • f (-3 + x)
                                                                                                                                                                                                                                                                                      • f (-63 + x)
                                                                                                                                                                                                                                                                                      • f (-41 + x)
                                                                                                                                                                                                                                                                                      • f (-13 + x)
                                                                                                                                                                                                                                                                                      blocked
                                                                                                                                                                                                                                                                                      • f (-100 + x)
                                                                                                                                                                                                                                                                                      proof attempt
                                                                                                                                                                                                                                                                                      ground_instances100
                                                                                                                                                                                                                                                                                      definitions0
                                                                                                                                                                                                                                                                                      inductions0
                                                                                                                                                                                                                                                                                      search_time
                                                                                                                                                                                                                                                                                      0.264s
                                                                                                                                                                                                                                                                                      Expand
                                                                                                                                                                                                                                                                                      • start[0.264s] ( :var_0: ) < 101 ==> f ( :var_0: ) = 1
                                                                                                                                                                                                                                                                                      • simplify

                                                                                                                                                                                                                                                                                        into
                                                                                                                                                                                                                                                                                        101 <= ( :var_0: ) || f ( :var_0: ) = 1
                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                        []
                                                                                                                                                                                                                                                                                        rewrite_steps
                                                                                                                                                                                                                                                                                          forward_chaining
                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                            (f_17 x_21)
                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                              (f_17 (+ (- 1) x_21))
                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                (f_17 (+ (- 2) x_21))
                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 3) x_21))
                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 4) x_21))
                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 5) x_21))
                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 6) x_21))
                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 7) x_21))
                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 8) x_21))
                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 9) x_21))
                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 10) x_21))
                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 11) x_21))
                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 12) x_21))
                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 13) x_21))
                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 14) x_21))
                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 15) x_21))
                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 16) x_21))
                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 17) x_21))
                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 18) x_21))
                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 19) x_21))
                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 20) x_21))
                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 21) x_21))
                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 22) x_21))
                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 23) x_21))
                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 24) x_21))
                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 25) x_21))
                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 26) x_21))
                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 27) x_21))
                                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 28) x_21))
                                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 29) x_21))
                                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 30) x_21))
                                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 31) x_21))
                                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 32) x_21))
                                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 33) x_21))
                                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 34) x_21))
                                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 35) x_21))
                                                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 36) x_21))
                                                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 37) x_21))
                                                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 38) x_21))
                                                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 39) x_21))
                                                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 40) x_21))
                                                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 41) x_21))
                                                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 42) x_21))
                                                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 43) x_21))
                                                                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 44) x_21))
                                                                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 45) x_21))
                                                                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 46) x_21))
                                                                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 47) x_21))
                                                                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 48) x_21))
                                                                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 49) x_21))
                                                                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 50) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 51) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 52) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 53) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 54) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 55) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 56) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 57) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 58) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 59) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 60) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 61) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 62) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 63) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 64) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 65) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 66) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 67) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 68) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 69) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 70) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 71) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 72) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 73) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 74) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 75) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 76) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 77) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 78) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 79) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 80) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 81) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 82) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 83) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 84) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 85) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 86) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 87) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 88) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 89) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 90) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 91) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    (f_17 (+ (- 92) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      (f_17 (+ (- 93) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        (f_17 (+ (- 94) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          (f_17 (+ (- 95) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            (f_17 (+ (- 96) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              (f_17 (+ (- 97) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                (f_17 (+ (- 98) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  (f_17 (+ (- 99) x_21))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  expansions

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  As expected, since the recursion depth needed to prove this exceeds the unrolling bound we set, Imandra could only prove this property up to bound k. This goal is in fact a property that is better suited for verification by induction (indeed, you might try adding the [@@auto] annotation to the above goal to invoke the Imandra's inductive waterfall and prove it).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  As a minor note, if we reach a local unrolling depth instead of hitting the global one, Imandra will be a bit more positive in its message, telling us that the conjecture has been proved up to the number of steps we've specified instead of a weaker "Unknown":

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  In [6]:
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  verify ~upto:100 (fun x -> x < 101 ==> f x = 1)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Out[6]:
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  - : int -> bool = <fun>
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Proved up to 100 steps

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Datatype bounds

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Imandra offers an orthogonal, more advanced form of bounding for unrolling, using ~upto_bound:<n>. This bound works in a fundamentally different way than the "normal" unrolling limit: instead of acting as a limit on the number of recursive steps that Imandra unrolls, this limit instructs Imandra to synthesize a recursive depth function for the datatypes involved in the goal and to transform the goal such that it will include this bound check as part of the hypotheses.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  This means that Imandra will be actually proving a bounded theorem involving the depth of datatypes.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  In [7]:
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  verify ~upto_bound:5 (fun x -> List.rev (List.rev x) = x)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Out[7]:
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  - : 'a list -> bool = <fun>
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Proved up to bound 5

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  When using unrolling with ~upto_bound, one should remember that the global unrolling limit still applies and may cause Imandra to abort solving before reaching the datatype bound.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  This datatype bound limit can also be used with the blast strategy, while the unrolling limit can't, as blast doesn't work by recursive unrolling.