Induction

While techniques such as unrolling and simplification can get us a long way towards formally verifying our software, variants of mathematical induction are in general required for verifying properties of systems with infinite state-spaces.

Induction is a proof technique that can be used to prove that some property φ(x) holds for all the elements x of a recursively defined structure (e.g. natural numbers, lists, trees, execution traces, etc). The proof consists of:

  • a proof that φ(base) is true for each base case
  • a proof that if φ(c) is true (called the inductive hypothesis), then φ(step(c)) is also true, for all the recursive steps of the property we're trying to prove

Induction can be done in many ways, and finding the "right" way to induct is often the key to difficult problems. Imandra has deep automation for finding and applying the "right" induction for a problem. If this fails, the user can instruct Imandra how to induct, with various forms of instructions.

A method of induction is given by an induction scheme.

Induction schemes can automatically be derived by Imandra in many ways. By default, with [@@auto] or [@@induct], Imandra analyses the recursive functions involved in the conjecture and constructs a functional induction scheme derived from their recursive structure, in a manner that is justified by the ordinal measures used to prove their termination. Imandra also supports structural induction principles derived from the definitions of (well-founded) algebraic datatypes such as lists and trees.

Some example induction schemes are:

  • for the natural numbers, φ(Zero) && φ(n) ==> φ(Succ(n))
  • for lists, φ([]) && (lst <> [] && φ(List.tl(lst)) ==> φ (lst))
  • for the function repeat as defined below, n <= 0 ==> φ(n, c) && (n > 0 && φ(n - 1, c)) ==> φ(n, c)
In [1]:
let rec repeat c n =
  if n <= 0 then
    []
  else
    c :: (repeat c (n-1))
Out[1]:
val repeat : 'a -> Z.t -> 'a list = <fun>
termination proof

Termination proof

call `repeat c (n - 1)` from `repeat c n`
original:repeat c n
sub:repeat c (n - 1)
original ordinal:Ordinal.Int (_cnt n)
sub ordinal:Ordinal.Int (_cnt (n - 1))
path:[not (n <= 0)]
proof:
detailed proof
ground_instances:1
definitions:0
inductions:0
search_time:
0.012s
details:
Expand
smt_stats:
num checks:3
arith assert lower:6
arith tableau max rows:4
arith tableau max columns:9
arith pivots:2
rlimit count:1097
mk clause:5
datatype occurs check:2
mk bool var:17
arith assert upper:3
decisions:2
arith row summations:3
propagations:2
conflicts:2
arith fixed eqs:2
datatype accessor ax:2
arith conflicts:1
arith num rows:4
num allocs:657366
final checks:1
added eqs:4
del clause:5
arith eq adapter:2
memory:5.100000
max memory:5.100000
Expand
  • start[0.012s]
      let (_x_0 : int) = if n >= 0 then n else 0 in
      let (_x_1 : int) = n - 1 in
      let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
      not (n <= 0) && _x_0 >= 0 && _x_2 >= 0
      ==> _x_1 <= 0 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into:
    (n <= 0 || n <= 1)
    || Ordinal.( << ) (Ordinal.Int (if n >= 1 then (-1) + n else 0))
       (Ordinal.Int (if n >= 0 then n else 0))
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • unroll
        expr:
        (|Ordinal.<<_129/client|
          (|Ordinal.Int_114/client|
            (ite (>= n_1631/server 1) (+ (- 1) n_1631/s…
        expansions:
        • Unsat

        In Imandra, induction schemes are "destructor style." So, an actual scheme Imandra would produce for a goal involving n : nat (where type nat = Zero | Succ of nat) is:

         (n = Zero ==> φ n)
         && (not (n = Zero) && φ (Destruct(Succ, 0, n)) ==> φ n).

        Let us see a few example inductions.

        In [2]:
        lemma assoc_append x y z =
         x @ (y @ z) = (x @ y) @ z [@@auto] [@@rw]
        
        Out[2]:
        val assoc_append : 'a list -> 'a list -> 'a list -> bool = <fun>
        Goal:
        
        x @ y @ z = (x @ y) @ z.
        
        1 nontautological subgoal.
        
        Subgoal 1:
        
        |---------------------------------------------------------------------------
         List.append x (List.append y z) = List.append (List.append x y) z
        
        
        Must try induction.
        
        The recursive terms in the conjecture suggest 3 inductions.
        Subsumption and merging reduces this to 2.
        
        Only 1 of those schemes are unflawed.
        We shall induct according to a scheme derived from List.append.
        
        Induction scheme:
        
         (not (x <> []) ==> φ x y z) && (x <> [] && φ (List.tl x) y z ==> φ x y z).
        
        2 nontautological subgoals.
        
        Subgoal 1.2:
        
        |---------------------------------------------------------------------------
         C0. x <> []
         C1. List.append x (List.append y z) = List.append (List.append x y) z
        
        But simplification reduces this to true, using the definition of List.append.
        
        Subgoal 1.1:
        
         H0. x <> []
         H1. List.append (List.tl x) (List.append y z) =
             List.append (List.append (List.tl x) y) z
        |---------------------------------------------------------------------------
         List.append x (List.append y z) = List.append (List.append x y) z
        
        But simplification reduces this to true, using the definition of List.append.
        
         Rules:
            (:def List.append)
            (:induct List.append)
        
        
        Proved
        proof
        ground_instances:0
        definitions:5
        inductions:1
        search_time:
        0.064s
        Expand
        • start[0.064s, "Goal"]
            List.append ( :var_0: ) (List.append ( :var_1: ) ( :var_2: )) =
            List.append (List.append ( :var_0: ) ( :var_1: )) ( :var_2: )
        • subproof

          List.append x (List.append y z) = List.append (List.append x y) z
          • start[0.064s, "1"]
              List.append x (List.append y z) = List.append (List.append x y) z
          • induction on (functional ?)
            :scheme (not (x <> []) ==> φ x y z)
                    && (x <> [] && φ (List.tl x) y z ==> φ x y z)
          • Split (let (_x_0 : bool) = x <> [] in
                   let (_x_1 : sko_ty_0 list) = List.append y z in
                   let (_x_2 : bool)
                       = List.append x _x_1 = List.append (List.append x y) z
                   in
                   let (_x_3 : sko_ty_0 list) = List.tl x in
                   (_x_0 || _x_2)
                   && (not
                       (_x_0
                        && List.append _x_3 _x_1 = List.append (List.append _x_3 y) z)
                       || _x_2)
                   :cases [x <> []
                           || List.append x (List.append y z) =
                              List.append (List.append x y) z;
                           let (_x_0 : sko_ty_0 list) = List.tl x in
                           let (_x_1 : sko_ty_0 list) = List.append y z in
                           (not (x <> [])
                            || not
                               (List.append _x_0 _x_1 =
                                List.append (List.append _x_0 y) z))
                           || List.append x _x_1 = List.append (List.append x y) z])
            • subproof
              let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : sko_ty_0 list) = List.append y z in (not (x <> []) || not (List.append _x_0 _x_1 = List.append (List.append _x_0 y) z)) || List.append x _x_1 = List.append (List.append x y) z
              • start[0.033s, "1.1"]
                  let (_x_0 : sko_ty_0 list) = List.tl x in
                  let (_x_1 : sko_ty_0 list) = List.append y z in
                  (not (x <> [])
                   || not (List.append _x_0 _x_1 = List.append (List.append _x_0 y) z))
                  || List.append x _x_1 = List.append (List.append x y) z
              • simplify
                into:
                true
                expansions:
                [List.append, List.append, List.append]
                rewrite_steps:
                  forward_chaining:
                • subproof
                  x <> [] || List.append x (List.append y z) = List.append (List.append x y) z
                  • start[0.033s, "1.2"]
                      x <> []
                      || List.append x (List.append y z) = List.append (List.append x y) z
                  • simplify
                    into:
                    true
                    expansions:
                    [List.append, List.append]
                    rewrite_steps:
                      forward_chaining:
                In [3]:
                lemma rev_append x y =
                 List.rev (x @ y) = List.rev y @ List.rev x
                 [@@auto]
                
                Out[3]:
                val rev_append : 'a list -> 'a list -> bool = <fun>
                Goal:
                
                List.rev (x @ y) = List.rev y @ List.rev x.
                
                1 nontautological subgoal.
                
                Subgoal 1:
                
                |---------------------------------------------------------------------------
                 List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                
                
                Must try induction.
                
                The recursive terms in the conjecture suggest 3 inductions.
                Subsumption and merging reduces this to 2.
                
                Only 1 of those schemes are unflawed.
                We shall induct according to a scheme derived from List.append.
                
                Induction scheme:
                
                 (not (x <> []) ==> φ x y) && (x <> [] && φ (List.tl x) y ==> φ x y).
                
                2 nontautological subgoals.
                
                Subgoal 1.2:
                
                |---------------------------------------------------------------------------
                 C0. x <> []
                 C1. List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                
                But simplification reduces this to true, using the definitions of List.append
                and List.rev, and the rewrite rule List.append_to_nil.
                
                Subgoal 1.1:
                
                 H0. x <> []
                 H1. List.rev (List.append (List.tl x) y) =
                     List.append (List.rev y) (List.rev (List.tl x))
                |---------------------------------------------------------------------------
                 List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                
                This simplifies, using the definitions of List.append and List.rev to:
                
                Subgoal 1.1':
                
                 H0. x <> []
                 H1. List.rev (List.append (List.tl x) y) =
                     List.append (List.rev y) (List.rev (List.tl x))
                |---------------------------------------------------------------------------
                 List.append (List.rev (List.append (List.tl x) y)) [List.hd x] =
                 List.append (List.rev y) (List.append (List.rev (List.tl x)) [List.hd x])
                
                But simplification reduces this to true, using the rewrite rule assoc_append.
                
                 Rules:
                    (:def List.append)
                    (:def List.rev)
                    (:rw List.append_to_nil)
                    (:rw assoc_append)
                    (:induct List.append)
                
                
                Proved
                proof
                ground_instances:0
                definitions:6
                inductions:1
                search_time:
                0.127s
                Expand
                • start[0.127s, "Goal"]
                    List.rev (List.append ( :var_0: ) ( :var_1: )) =
                    List.append (List.rev ( :var_1: )) (List.rev ( :var_0: ))
                • subproof

                  List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                  • start[0.127s, "1"]
                      List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                  • induction on (functional ?)
                    :scheme (not (x <> []) ==> φ x y)
                            && (x <> [] && φ (List.tl x) y ==> φ x y)
                  • Split (let (_x_0 : bool) = x <> [] in
                           let (_x_1 : sko_ty_0 list) = List.rev y in
                           let (_x_2 : bool)
                               = List.rev (List.append x y) = List.append _x_1 (List.rev x)
                           in
                           let (_x_3 : sko_ty_0 list) = List.tl x in
                           (_x_0 || _x_2)
                           && (not
                               (_x_0
                                && List.rev (List.append _x_3 y) =
                                   List.append _x_1 (List.rev _x_3))
                               || _x_2)
                           :cases [x <> []
                                   || List.rev (List.append x y) =
                                      List.append (List.rev y) (List.rev x);
                                   let (_x_0 : sko_ty_0 list) = List.tl x in
                                   let (_x_1 : sko_ty_0 list) = List.rev y in
                                   (not (x <> [])
                                    || not
                                       (List.rev (List.append _x_0 y) =
                                        List.append _x_1 (List.rev _x_0)))
                                   || List.rev (List.append x y) = List.append _x_1 (List.rev x)])
                    • subproof
                      let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : sko_ty_0 list) = List.rev y in (not (x <> []) || not (List.rev (List.append _x_0 y) = List.append _x_1 (List.rev _x_0))) || List.rev (List.append x y) = List.append _x_1 (List.rev x)
                      • start[0.093s, "1.1"]
                          let (_x_0 : sko_ty_0 list) = List.tl x in
                          let (_x_1 : sko_ty_0 list) = List.rev y in
                          (not (x <> [])
                           || not (List.rev (List.append _x_0 y) = List.append _x_1 (List.rev _x_0)))
                          || List.rev (List.append x y) = List.append _x_1 (List.rev x)
                      • simplify
                        into:
                        let (_x_0 : sko_ty_0 list) = List.tl x in
                        let (_x_1 : sko_ty_0 list) = List.rev (List.append _x_0 y) in
                        let (_x_2 : sko_ty_0 list) = List.rev y in
                        let (_x_3 : sko_ty_0 list) = List.rev _x_0 in
                        let (_x_4 : sko_ty_0 list) = [List.hd x] in
                        (not (x <> []) || not (_x_1 = List.append _x_2 _x_3))
                        || List.append _x_1 _x_4 = List.append _x_2 (List.append _x_3 _x_4)
                        expansions:
                        [List.rev, List.rev, List.append]
                        rewrite_steps:
                          forward_chaining:
                          • simplify
                            into:
                            true
                            expansions:
                            []
                            rewrite_steps:
                            assoc_append
                            forward_chaining:
                          • subproof
                            x <> [] || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                            • start[0.093s, "1.2"]
                                x <> []
                                || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                            • simplify
                              into:
                              true
                              expansions:
                              [List.append, List.rev, List.append]
                              rewrite_steps:
                              List.append_to_nil
                              forward_chaining:
                        In [4]:
                        verify (fun lst ->
                          List.for_all (fun x -> x > 0) lst ==>
                            List.fold_right (+) ~base:1 lst > 0)
                        [@@auto]
                        
                        Out[4]:
                        - : Z.t list -> bool = <fun>
                        Goal:
                        
                        List.for_all (fun x -> x > 0) lst ==> List.fold_right ( + ) 1 lst > 0.
                        
                        1 nontautological subgoal.
                        
                        Subgoal 1:
                        
                         H0. List.for_all (fun x -> x > 0) lst
                         H1. List.fold_right ( + ) 1 lst <= 0
                        |---------------------------------------------------------------------------
                         false
                        
                        
                        Must try induction.
                        
                        The recursive terms in the conjecture suggest 2 inductions.
                        Subsumption and merging reduces this to 1.
                        
                        We shall induct according to a scheme derived from List.for_all.
                        
                        Induction scheme:
                        
                         (not (lst <> []) ==> φ lst) && (lst <> [] && φ (List.tl lst) ==> φ lst).
                        
                        2 nontautological subgoals.
                        
                        Subgoal 1.2:
                        
                         H0. List.for_all (fun x -> x > 0) lst
                         H1. List.fold_right ( + ) 1 lst <= 0
                        |---------------------------------------------------------------------------
                         lst <> []
                        
                        But simplification reduces this to true, using the definition of
                        List.fold_right.
                        
                        Subgoal 1.1:
                        
                         H0. List.for_all (fun x -> x > 0) lst
                         H1. lst <> []
                         H2. not (List.for_all (fun x -> x > 0) (List.tl lst))
                             || not (List.fold_right ( + ) 1 (List.tl lst) <= 0)
                         H3. List.fold_right ( + ) 1 lst <= 0
                        |---------------------------------------------------------------------------
                         false
                        
                        But simplification reduces this to true, using the definitions of
                        List.fold_right and List.for_all.
                        
                         Rules:
                            (:def List.fold_right)
                            (:def List.for_all)
                            (:induct List.for_all)
                        
                        
                        Proved
                        proof
                        ground_instances:0
                        definitions:3
                        inductions:1
                        search_time:
                        0.089s
                        Expand
                        • start[0.089s, "Goal"]
                            List.for_all (fun x -> x > 0) ( :var_0: )
                            ==> List.fold_right ( + ) 1 ( :var_0: ) > 0
                        • subproof

                          not (List.for_all (fun x -> x > 0) lst) || not (List.fold_right ( + ) 1 lst <= 0)
                          • start[0.089s, "1"]
                              not (List.for_all (fun x -> x > 0) lst)
                              || not (List.fold_right ( + ) 1 lst <= 0)
                          • induction on (functional ?)
                            :scheme (not (lst <> []) ==> φ lst)
                                    && (lst <> [] && φ (List.tl lst) ==> φ lst)
                          • Split (let (_x_0 : bool) = not (List.for_all (fun x -> x > 0) lst) in
                                   let (_x_1 : bool) = not (List.fold_right ( + ) 1 lst <= 0) in
                                   let (_x_2 : bool) = lst <> [] in
                                   let (_x_3 : int list) = List.tl lst in
                                   ((_x_0 || _x_1) || _x_2)
                                   && ((_x_0
                                        || not
                                           (_x_2
                                            && (not (List.for_all (fun x -> x > 0) _x_3)
                                                || not (List.fold_right ( + ) 1 _x_3 <= 0))))
                                       || _x_1)
                                   :cases [(not (List.for_all (fun x -> x > 0) lst)
                                            || not (List.fold_right ( + ) 1 lst <= 0))
                                           || lst <> [];
                                           let (_x_0 : int list) = List.tl lst in
                                           ((not (List.for_all (fun x -> x > 0) lst) || not (lst <> []))
                                            || not
                                               (not (List.for_all (fun x -> x > 0) _x_0)
                                                || not (List.fold_right ( + ) 1 _x_0 <= 0)))
                                           || not (List.fold_right ( + ) 1 lst <= 0)])
                            • subproof
                              let (_x_0 : int list) = List.tl lst in ((not (List.for_all (fun x -> x > 0) lst) || not (lst <> [])) || not (not (List.for_all (fun x -> x > 0) _x_0) || not (List.fold_right ( + ) 1 _x_0 <= 0))) || not (List.fold_right ( + ) 1 lst <= 0)
                              • start[0.045s, "1.1"]
                                  let (_x_0 : int list) = List.tl lst in
                                  ((not (List.for_all (fun x -> x > 0) lst) || not (lst <> []))
                                   || not
                                      (not (List.for_all (fun x -> x > 0) _x_0)
                                       || not (List.fold_right ( + ) 1 _x_0 <= 0)))
                                  || not (List.fold_right ( + ) 1 lst <= 0)
                              • simplify
                                into:
                                true
                                expansions:
                                [List.for_all, List.fold_right]
                                rewrite_steps:
                                  forward_chaining:
                                • subproof
                                  (not (List.for_all (fun x -> x > 0) lst) || not (List.fold_right ( + ) 1 lst <= 0)) || lst <> []
                                  • start[0.045s, "1.2"]
                                      (not (List.for_all (fun x -> x > 0) lst)
                                       || not (List.fold_right ( + ) 1 lst <= 0))
                                      || lst <> []
                                  • simplify
                                    into:
                                    true
                                    expansions:
                                    List.fold_right
                                    rewrite_steps:
                                      forward_chaining:

                                Functional Induction

                                By default, Imandra uses functional induction (also known as recursion induction).

                                A functional induction scheme is one derived from the recursive structure of a function definition. The termination measure used to admit the function is also used to justify the soundness of the functional induction scheme. Unless instructed otherwise, Imandra will consider all recursive functions in a goal, analyse their recursions and instances, and apply various heuristics to merge and score them and adapt them to the conjecture being proved. In general, there may be more than one plausible induction scheme to choose from, and selecting the "right" way to induct can often be a key step in difficult proofs. Imandra will often make the "right" decision. However, in case it doesn't, it is also possible to manually specify the induction that Imandra should do.

                                Let us return to the function repeat above and see functional induction in action.

                                In [5]:
                                lemma repeat_len c n =
                                  n >= 0 ==>
                                  List.length (repeat c n) = n [@@auto]
                                
                                Out[5]:
                                val repeat_len : 'a -> Z.t -> bool = <fun>
                                Goal:
                                
                                n >= 0 ==> List.length (repeat c n) = n.
                                
                                1 nontautological subgoal.
                                
                                Subgoal 1:
                                
                                 H0. n >= 0
                                |---------------------------------------------------------------------------
                                 List.length (repeat c n) = n
                                
                                
                                Must try induction.
                                
                                We shall induct according to a scheme derived from repeat.
                                
                                Induction scheme:
                                
                                 (n <= 0 ==> φ c n) && (not (n <= 0) && φ c (n - 1) ==> φ c n).
                                
                                2 nontautological subgoals.
                                
                                Subgoal 1.2:
                                
                                 H0. n <= 0
                                 H1. n >= 0
                                |---------------------------------------------------------------------------
                                 List.length (repeat c n) = n
                                
                                But simplification reduces this to true, using the definitions of List.length
                                and repeat.
                                
                                Subgoal 1.1:
                                
                                 H0. n >= 0
                                 H1. not (n <= 0)
                                 H2. n >= 1 ==> List.length (repeat c ((-1) + n)) = (-1) + n
                                |---------------------------------------------------------------------------
                                 List.length (repeat c n) = n
                                
                                But simplification reduces this to true, using the definitions of List.length
                                and repeat.
                                
                                 Rules:
                                    (:def List.length)
                                    (:def repeat)
                                    (:fc List.len_nonnegative)
                                    (:induct repeat)
                                
                                
                                Proved
                                proof
                                ground_instances:0
                                definitions:4
                                inductions:1
                                search_time:
                                0.076s
                                Expand
                                • start[0.076s, "Goal"]
                                    ( :var_0: ) >= 0
                                    ==> List.length (repeat ( :var_1: ) ( :var_0: )) = ( :var_0: )
                                • subproof

                                  not (n >= 0) || List.length (repeat c n) = n
                                  • start[0.076s, "1"] not (n >= 0) || List.length (repeat c n) = n
                                  • induction on (functional ?)
                                    :scheme (n <= 0 ==> φ c n) && (not (n <= 0) && φ c (n - 1) ==> φ c n)
                                  • Split (let (_x_0 : bool) = List.length (repeat c n) = n in
                                           let (_x_1 : bool) = not (n <= 0) in
                                           let (_x_2 : bool) = not (n >= 0) in
                                           let (_x_3 : int) = (-1) + n in
                                           ((_x_0 || _x_1) || _x_2)
                                           && ((_x_0 || _x_2)
                                               || not
                                                  (_x_1 && (not (n >= 1) || List.length (repeat c _x_3) = _x_3)))
                                           :cases [(not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n;
                                                   let (_x_0 : int) = (-1) + n in
                                                   ((not (n >= 0) || n <= 0)
                                                    || not (n >= 1 ==> List.length (repeat c _x_0) = _x_0))
                                                   || List.length (repeat c n) = n])
                                    • subproof
                                      let (_x_0 : int) = (-1) + n in ((not (n >= 0) || n <= 0) || not (n >= 1 ==> List.length (repeat c _x_0) = _x_0)) || List.length (repeat c n) = n
                                      • start[0.033s, "1.1"]
                                          let (_x_0 : int) = (-1) + n in
                                          ((not (n >= 0) || n <= 0)
                                           || not (n >= 1 ==> List.length (repeat c _x_0) = _x_0))
                                          || List.length (repeat c n) = n
                                      • simplify
                                        into:
                                        true
                                        expansions:
                                        [List.length, repeat]
                                        rewrite_steps:
                                          forward_chaining:
                                          • List.len_nonnegative
                                          • List.len_nonnegative
                                          • List.len_nonnegative
                                          • List.len_nonnegative
                                      • subproof
                                        (not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n
                                        • start[0.033s, "1.2"]
                                            (not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n
                                        • simplify
                                          into:
                                          true
                                          expansions:
                                          [List.length, repeat]
                                          rewrite_steps:
                                            forward_chaining:
                                            List.len_nonnegative

                                    Functional induction schemes tailored to a problem can also be manually specified.

                                    In order to manually specify a functional induction, one must define a recursive function encoding the recursion scheme one wants available in induction (Imandra doesn't care what the function does, it only looks at how it recurses). As always, Imandra must be able to prove that the recursive function terminates in order for it to be admitted into the logic. The ordinal measures used in the termination proof are then used to justify subsequent functional induction schemes derived from the function.

                                    Let's see a simple example. Note that we could trivially prove this goal with [@@auto], but we shall use it to illustrate the process of manual induction schemes nevertheless! For fun, we'll make our custom induction scheme have two base-cases.

                                    In [6]:
                                    let rec sum n =
                                     if n <= 0 then 0
                                     else n + sum (n-1)
                                    
                                    let rec induct_scheme (n : int) =
                                     if n <= 0 then true
                                     else if n = 1 then true
                                     else induct_scheme (n-1)
                                    
                                    Out[6]:
                                    val sum : Z.t -> Z.t = <fun>
                                    val induct_scheme : Z.t -> bool = <fun>
                                    
                                    termination proof

                                    Termination proof

                                    call `sum (n - 1)` from `sum n`
                                    original:sum n
                                    sub:sum (n - 1)
                                    original ordinal:Ordinal.Int (_cnt n)
                                    sub ordinal:Ordinal.Int (_cnt (n - 1))
                                    path:[not (n <= 0)]
                                    proof:
                                    detailed proof
                                    ground_instances:1
                                    definitions:0
                                    inductions:0
                                    search_time:
                                    0.010s
                                    details:
                                    Expand
                                    smt_stats:
                                    num checks:3
                                    arith assert lower:6
                                    arith tableau max rows:4
                                    arith tableau max columns:9
                                    arith pivots:2
                                    rlimit count:12393
                                    mk clause:4
                                    datatype occurs check:2
                                    mk bool var:18
                                    arith assert upper:3
                                    decisions:2
                                    arith row summations:3
                                    propagations:2
                                    conflicts:2
                                    arith fixed eqs:2
                                    datatype accessor ax:2
                                    arith conflicts:1
                                    arith num rows:4
                                    num allocs:524722150
                                    final checks:1
                                    added eqs:5
                                    arith eq adapter:2
                                    memory:7.540000
                                    max memory:8.060000
                                    Expand
                                    • start[0.010s]
                                        let (_x_0 : int) = if n >= 0 then n else 0 in
                                        let (_x_1 : int) = n - 1 in
                                        let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
                                        not (n <= 0) && _x_0 >= 0 && _x_2 >= 0
                                        ==> _x_1 <= 0 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                    • simplify
                                      into:
                                      (n <= 0
                                       || Ordinal.( << ) (Ordinal.Int (if n >= 1 then (-1) + n else 0))
                                          (Ordinal.Int (if n >= 0 then n else 0)))
                                      || n <= 1
                                      expansions:
                                      []
                                      rewrite_steps:
                                        forward_chaining:
                                        • unroll
                                          expr:
                                          (|Ordinal.<<_129/client|
                                            (|Ordinal.Int_114/client|
                                              (ite (>= n_2055/server 1) (+ (- 1) n_2055/s…
                                          expansions:
                                          • Unsat
                                          termination proof

                                          Termination proof

                                          call `induct_scheme (n - 1)` from `induct_scheme n`
                                          original:induct_scheme n
                                          sub:induct_scheme (n - 1)
                                          original ordinal:Ordinal.Int (_cnt n)
                                          sub ordinal:Ordinal.Int (_cnt (n - 1))
                                          path:[not (n = 1) && not (n <= 0)]
                                          proof:
                                          detailed proof
                                          ground_instances:1
                                          definitions:0
                                          inductions:0
                                          search_time:
                                          0.010s
                                          details:
                                          Expand
                                          smt_stats:
                                          num checks:3
                                          arith assert lower:8
                                          arith tableau max rows:4
                                          arith tableau max columns:11
                                          arith pivots:2
                                          rlimit count:13659
                                          mk clause:7
                                          datatype occurs check:2
                                          mk bool var:22
                                          arith assert upper:3
                                          decisions:2
                                          arith row summations:3
                                          propagations:3
                                          conflicts:2
                                          arith fixed eqs:2
                                          datatype accessor ax:2
                                          arith conflicts:1
                                          arith num rows:4
                                          arith assert diseq:3
                                          num allocs:557993489
                                          final checks:1
                                          added eqs:5
                                          arith eq adapter:4
                                          memory:7.560000
                                          max memory:8.060000
                                          Expand
                                          • start[0.010s]
                                              let (_x_0 : int) = if n >= 0 then n else 0 in
                                              let (_x_1 : int) = n - 1 in
                                              let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
                                              not (n = 1) && not (n <= 0) && _x_0 >= 0 && _x_2 >= 0
                                              ==> not (not (_x_1 = 1) && not (_x_1 <= 0))
                                                  || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                          • simplify
                                            into:
                                            (not (not (n = 1) && not (n <= 0))
                                             || Ordinal.( << ) (Ordinal.Int (if n >= 1 then (-1) + n else 0))
                                                (Ordinal.Int (if n >= 0 then n else 0)))
                                            || not (not (n = 2) && not (n <= 1))
                                            expansions:
                                            []
                                            rewrite_steps:
                                              forward_chaining:
                                              • unroll
                                                expr:
                                                (|Ordinal.<<_129/client|
                                                  (|Ordinal.Int_114/client|
                                                    (ite (>= n_2081/server 1) (+ (- 1) n_2081/s…
                                                expansions:
                                                • Unsat
                                                In [7]:
                                                verify (fun n -> n >= 0 ==> sum n = (n * (n+1)) / 2) [@@induct functional induct_scheme]
                                                
                                                Out[7]:
                                                - : Z.t -> bool = <fun>
                                                Goal:
                                                
                                                n >= 0 ==> sum n = (n * (n + 1)) / 2.
                                                
                                                1 nontautological subgoal.
                                                
                                                Note: Thank you for your explicit request for a non-present functional
                                                induction on `induct_scheme`!
                                                
                                                We shall induct according to a scheme derived from induct_scheme.
                                                
                                                Induction scheme:
                                                
                                                 (not (not (n = 1) && not (n <= 0)) ==> φ n)
                                                 && (not (n <= 0) && not (n = 1) && φ (n - 1) ==> φ n).
                                                
                                                2 nontautological subgoals.
                                                
                                                Subgoal 2:
                                                
                                                 H0. n >= 0
                                                |---------------------------------------------------------------------------
                                                 C0. not (n = 1) && not (n <= 0)
                                                 C1. sum n = (n * (1 + n)) / 2
                                                
                                                This simplifies to the following 2 subgoals:
                                                
                                                Subgoal 2.2:
                                                
                                                 H0. n = 1
                                                |---------------------------------------------------------------------------
                                                 sum n = (n * (1 + n)) / 2
                                                
                                                But simplification reduces this to true, using the definition of sum.
                                                
                                                Subgoal 2.1:
                                                
                                                 H0. n <= 0
                                                 H1. n >= 0
                                                |---------------------------------------------------------------------------
                                                 C0. n = 1
                                                 C1. sum n = (n * (1 + n)) / 2
                                                
                                                But simplification reduces this to true, using the definition of sum.
                                                
                                                Subgoal 1:
                                                
                                                 H0. n >= 0
                                                 H1. not (n <= 0)
                                                 H2. not (n = 1)
                                                 H3. n >= 1 ==> sum ((-1) + n) = (n * ((-1) + n)) / 2
                                                |---------------------------------------------------------------------------
                                                 sum n = (n * (1 + n)) / 2
                                                
                                                But simplification reduces this to true, using the definition of sum.
                                                
                                                 Rules:
                                                    (:def sum)
                                                    (:induct induct_scheme)
                                                
                                                
                                                Proved
                                                proof
                                                ground_instances:0
                                                definitions:4
                                                inductions:1
                                                search_time:
                                                0.084s
                                                Expand
                                                • start[0.084s, "Goal"]
                                                    ( :var_0: ) >= 0
                                                    ==> sum ( :var_0: ) = (( :var_0: ) * (( :var_0: ) + 1)) / 2
                                                • subproof

                                                  not (n >= 0) || sum n = (n * (1 + n)) / 2
                                                  • start[0.083s, "1"] not (n >= 0) || sum n = (n * (1 + n)) / 2
                                                  • induction on (functional induct_scheme)
                                                    :scheme (not (not (n = 1) && not (n <= 0)) ==> φ n)
                                                            && (not (n <= 0) && not (n = 1) && φ (n - 1) ==> φ n)
                                                  • Split (let (_x_0 : bool) = not (n = 1) in
                                                           let (_x_1 : bool) = not (n <= 0) in
                                                           let (_x_2 : bool) = not (n >= 0) in
                                                           let (_x_3 : bool) = sum n = (n * (1 + n)) / 2 in
                                                           let (_x_4 : int) = (-1) + n in
                                                           ((_x_0 && _x_1 || _x_2) || _x_3)
                                                           && ((_x_2 || _x_3)
                                                               || not
                                                                  ((_x_1 && _x_0) && (not (n >= 1) || sum _x_4 = (n * _x_4) / 2)))
                                                           :cases [(not (n >= 0) || not (n = 1) && not (n <= 0))
                                                                   || sum n = (n * (1 + n)) / 2;
                                                                   let (_x_0 : int) = (-1) + n in
                                                                   (((not (n >= 0) || n <= 0) || n = 1)
                                                                    || not (n >= 1 ==> sum _x_0 = (n * _x_0) / 2))
                                                                   || sum n = (n * (1 + n)) / 2])
                                                    • subproof
                                                      let (_x_0 : int) = (-1) + n in (((not (n >= 0) || n <= 0) || n = 1) || not (n >= 1 ==> sum _x_0 = (n * _x_0) / 2)) || sum n = (n * (1 + n)) / 2
                                                      • start[0.082s, "1"]
                                                          let (_x_0 : int) = (-1) + n in
                                                          (((not (n >= 0) || n <= 0) || n = 1)
                                                           || not (n >= 1 ==> sum _x_0 = (n * _x_0) / 2))
                                                          || sum n = (n * (1 + n)) / 2
                                                      • simplify
                                                        into:
                                                        true
                                                        expansions:
                                                        sum
                                                        rewrite_steps:
                                                          forward_chaining:
                                                        • subproof
                                                          (not (n >= 0) || not (n = 1) && not (n <= 0)) || sum n = (n * (1 + n)) / 2
                                                          • start[0.082s, "2"]
                                                              (not (n >= 0) || not (n = 1) && not (n <= 0)) || sum n = (n * (1 + n)) / 2
                                                          • simplify
                                                            into:
                                                            let (_x_0 : bool) = n = 1 in
                                                            let (_x_1 : bool) = sum n = (n * (1 + n)) / 2 in
                                                            (not _x_0 || _x_1) && (((_x_0 || not (n <= 0)) || not (n >= 0)) || _x_1)
                                                            expansions:
                                                            []
                                                            rewrite_steps:
                                                              forward_chaining:
                                                                • Subproof
                                                                • Subproof

                                                        Note that it's rare to have to manually instruct Imandra how to induct in this way. Usually, if you need to instruct Imandra to use a different scheme than the one it automatically picked, you'll simply need to give Imandra the hint of "inducting following key recursive function foo" in your goal. For example, if Imandra had made a wrong selection in a goal involving sum and some other recursive functions, we might tell Imandra [@@induct functional sum] to get it to select a scheme derived from the recursive structure of sum.

                                                        Structural Induction

                                                        Imandra also supports structural induction. Unlike functional induction schemes which are derived from recursive functions, structural induction schemes are derived from type definitions.

                                                        For example, we can define a type of binary trees and prove a property about them by structural induction.

                                                        In [8]:
                                                        type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf
                                                        
                                                        Out[8]:
                                                        type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf
                                                        
                                                        In [9]:
                                                        let rec size (x : 'a tree) =
                                                         match x with
                                                         | Node (_, a,b) -> size a + size b
                                                         | Leaf -> 1
                                                        
                                                        Out[9]:
                                                        val size : 'a tree -> Z.t = <fun>
                                                        
                                                        termination proof

                                                        Termination proof

                                                        call `size (Destruct(Node, 1, x))` from `size x`
                                                        original:size x
                                                        sub:size (Destruct(Node, 1, x))
                                                        original ordinal:Ordinal.Int (_cnt x)
                                                        sub ordinal:Ordinal.Int (_cnt (Destruct(Node, 1, x)))
                                                        path:[Is_a(Node, x)]
                                                        proof:
                                                        detailed proof
                                                        ground_instances:3
                                                        definitions:0
                                                        inductions:0
                                                        search_time:
                                                        0.016s
                                                        details:
                                                        Expand
                                                        smt_stats:
                                                        num checks:8
                                                        arith assert lower:17
                                                        arith tableau max rows:5
                                                        arith tableau max columns:15
                                                        arith pivots:17
                                                        rlimit count:11305
                                                        mk clause:23
                                                        datatype occurs check:27
                                                        mk bool var:74
                                                        arith assert upper:12
                                                        datatype splits:9
                                                        decisions:18
                                                        arith row summations:22
                                                        propagations:15
                                                        interface eqs:1
                                                        conflicts:6
                                                        arith fixed eqs:7
                                                        arith assume eqs:1
                                                        datatype accessor ax:7
                                                        arith conflicts:2
                                                        arith num rows:5
                                                        datatype constructor ax:11
                                                        num allocs:936032054
                                                        final checks:7
                                                        added eqs:54
                                                        del clause:11
                                                        arith eq adapter:10
                                                        memory:7.850000
                                                        max memory:8.360000
                                                        Expand
                                                        • start[0.016s]
                                                            let (_x_0 : int) = count.tree (const 0) x in
                                                            let (_x_1 : ty_0 tree) = Destruct(Node, 1, x) in
                                                            let (_x_2 : int) = count.tree (const 0) _x_1 in
                                                            let (_x_3 : bool) = not Is_a(Node, _x_1) in
                                                            Is_a(Node, x) && _x_0 >= 0 && _x_2 >= 0
                                                            ==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                        • simplify
                                                          into:
                                                          let (_x_0 : ty_0 tree) = Destruct(Node, 1, x) in
                                                          let (_x_1 : int) = count.tree (const 0) _x_0 in
                                                          let (_x_2 : int) = count.tree (const 0) x in
                                                          (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                           || not ((Is_a(Node, x) && _x_2 >= 0) && _x_1 >= 0))
                                                          || not Is_a(Node, _x_0)
                                                          expansions:
                                                          []
                                                          rewrite_steps:
                                                            forward_chaining:
                                                            • unroll
                                                              expr:
                                                              (|count.tree_2203/server| (|get.Node.1_2183/server| x_2190/server))
                                                              expansions:
                                                              • unroll
                                                                expr:
                                                                (|Ordinal.<<_129/client|
                                                                  (|Ordinal.Int_114/client|
                                                                    (|count.tree_2203/server| (|get.Node.1_2183…
                                                                expansions:
                                                                • unroll
                                                                  expr:
                                                                  (|count.tree_2203/server| x_2190/server)
                                                                  expansions:
                                                                  • Unsat
                                                                  call `size (Destruct(Node, 2, x))` from `size x`
                                                                  original:size x
                                                                  sub:size (Destruct(Node, 2, x))
                                                                  original ordinal:Ordinal.Int (_cnt x)
                                                                  sub ordinal:Ordinal.Int (_cnt (Destruct(Node, 2, x)))
                                                                  path:[Is_a(Node, x)]
                                                                  proof:
                                                                  detailed proof
                                                                  ground_instances:3
                                                                  definitions:0
                                                                  inductions:0
                                                                  search_time:
                                                                  0.019s
                                                                  details:
                                                                  Expand
                                                                  smt_stats:
                                                                  num checks:8
                                                                  arith assert lower:17
                                                                  arith tableau max rows:5
                                                                  arith tableau max columns:15
                                                                  arith pivots:17
                                                                  rlimit count:8771
                                                                  mk clause:20
                                                                  datatype occurs check:27
                                                                  mk bool var:74
                                                                  arith assert upper:12
                                                                  datatype splits:9
                                                                  decisions:16
                                                                  arith row summations:22
                                                                  propagations:14
                                                                  conflicts:6
                                                                  arith fixed eqs:7
                                                                  datatype accessor ax:7
                                                                  arith conflicts:2
                                                                  arith num rows:5
                                                                  datatype constructor ax:11
                                                                  num allocs:894578203
                                                                  final checks:6
                                                                  added eqs:56
                                                                  del clause:8
                                                                  arith eq adapter:10
                                                                  memory:7.840000
                                                                  max memory:8.360000
                                                                  Expand
                                                                  • start[0.019s]
                                                                      let (_x_0 : int) = count.tree (const 0) x in
                                                                      let (_x_1 : ty_0 tree) = Destruct(Node, 2, x) in
                                                                      let (_x_2 : int) = count.tree (const 0) _x_1 in
                                                                      let (_x_3 : bool) = not Is_a(Node, _x_1) in
                                                                      Is_a(Node, x) && _x_0 >= 0 && _x_2 >= 0
                                                                      ==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                  • simplify
                                                                    into:
                                                                    let (_x_0 : int) = count.tree (const 0) x in
                                                                    let (_x_1 : ty_0 tree) = Destruct(Node, 2, x) in
                                                                    let (_x_2 : int) = count.tree (const 0) _x_1 in
                                                                    (not ((Is_a(Node, x) && _x_0 >= 0) && _x_2 >= 0)
                                                                     || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0))
                                                                    || not Is_a(Node, _x_1)
                                                                    expansions:
                                                                    []
                                                                    rewrite_steps:
                                                                      forward_chaining:
                                                                      • unroll
                                                                        expr:
                                                                        (|count.tree_2203/server| (|get.Node.2_2184/server| x_2190/server))
                                                                        expansions:
                                                                        • unroll
                                                                          expr:
                                                                          (|Ordinal.<<_129/client|
                                                                            (|Ordinal.Int_114/client|
                                                                              (|count.tree_2203/server| (|get.Node.2_2184…
                                                                          expansions:
                                                                          • unroll
                                                                            expr:
                                                                            (|count.tree_2203/server| x_2190/server)
                                                                            expansions:
                                                                            • Unsat
                                                                            In [10]:
                                                                            verify (fun x -> size x > 0) [@@induct structural x]
                                                                            
                                                                            Out[10]:
                                                                            - : 'a tree -> bool = <fun>
                                                                            Goal:
                                                                            
                                                                            size x > 0.
                                                                            
                                                                            1 nontautological subgoal.
                                                                            
                                                                            Induction scheme:
                                                                            
                                                                             φ Leaf
                                                                             && (Is_a(Node, x) && φ (Destruct(Node, 1, x)) && φ (Destruct(Node, 2, x))
                                                                                 ==> φ x).
                                                                            
                                                                            2 nontautological subgoals.
                                                                            
                                                                            Subgoal 2:
                                                                            
                                                                            |---------------------------------------------------------------------------
                                                                             not (size Leaf <= 0)
                                                                            
                                                                            But simplification reduces this to true, using the definition of size.
                                                                            
                                                                            Subgoal 1:
                                                                            
                                                                             H0. size x <= 0
                                                                             H1. Is_a(Node, x)
                                                                             H2. not (size (Destruct(Node, 1, x)) <= 0)
                                                                             H3. not (size (Destruct(Node, 2, x)) <= 0)
                                                                            |---------------------------------------------------------------------------
                                                                             false
                                                                            
                                                                            But simplification reduces this to true, using the definition of size.
                                                                            
                                                                             Rules:
                                                                                (:def size)
                                                                                (:induct struct tree)
                                                                            
                                                                            
                                                                            Proved
                                                                            proof
                                                                            ground_instances:0
                                                                            definitions:2
                                                                            inductions:1
                                                                            search_time:
                                                                            0.025s
                                                                            Expand
                                                                            • start[0.025s, "Goal"] size ( :var_0: ) > 0
                                                                            • subproof

                                                                              not (size x <= 0)
                                                                              • start[0.025s, "1"] not (size x <= 0)
                                                                              • induction on (structural+ x)
                                                                                :scheme φ Leaf
                                                                                        && (Is_a(Node, x)
                                                                                            && φ (Destruct(Node, 1, x)) && φ (Destruct(Node, 2, x))
                                                                                            ==> φ x)
                                                                              • Split (not (size Leaf <= 0)
                                                                                       && (not (size x <= 0)
                                                                                           || not
                                                                                              ((Is_a(Node, x) && not (size (Destruct(Node, 1, x)) <= 0))
                                                                                               && not (size (Destruct(Node, 2, x)) <= 0)))
                                                                                       :cases [not (size Leaf <= 0);
                                                                                               ((not (size x <= 0) || not Is_a(Node, x))
                                                                                                || size (Destruct(Node, 1, x)) <= 0)
                                                                                               || size (Destruct(Node, 2, x)) <= 0])
                                                                                • subproof
                                                                                  ((not (size x <= 0) || not Is_a(Node, x)) || size (Destruct(Node, 1, x)) <= 0) || size (Destruct(Node, 2, x)) <= 0
                                                                                  • start[0.025s, "1"]
                                                                                      ((not (size x <= 0) || not Is_a(Node, x))
                                                                                       || size (Destruct(Node, 1, x)) <= 0)
                                                                                      || size (Destruct(Node, 2, x)) <= 0
                                                                                  • simplify
                                                                                    into:
                                                                                    true
                                                                                    expansions:
                                                                                    size
                                                                                    rewrite_steps:
                                                                                      forward_chaining:
                                                                                    • subproof
                                                                                      not (size Leaf <= 0)
                                                                                      • start[0.025s, "2"] not (size Leaf <= 0)
                                                                                      • simplify
                                                                                        into:
                                                                                        true
                                                                                        expansions:
                                                                                        size
                                                                                        rewrite_steps:
                                                                                          forward_chaining:

                                                                                    Structural induction comes in both additive and multiplicative flavors.

                                                                                    This distinction only manifests when one is performing structural induction over multiple variables simultaneously. It affects the way base cases and inductive steps are mixed. Let's assume one needs to do induction on x, y:

                                                                                    • addictive structural induction gives you 3 cases: two base cases φ(x_base, y), φ(x, y_base) and one inductive step φ(x,y) ==> φ(step(x), step(y))

                                                                                    • multiplicative structural induction gives you 4 cases: one base case φ(x_base, y_base) and three inductive steps φ(x, y_base) ==> φ(step(x), y_base), φ(x_base, y) ==> φ(x_base, step(y)) and φ(x,y) ==> φ(step(x), step(y))

                                                                                    We can see the difference using the following function:

                                                                                    In [11]:
                                                                                    let rec interleave_strict x y = match x, y with
                                                                                      | [], _ | _ , [] -> []
                                                                                      | x::xs, y::ys -> x::y::(interleave_strict xs ys)
                                                                                    
                                                                                    Out[11]:
                                                                                    val interleave_strict : 'a list -> 'a list -> 'a list = <fun>
                                                                                    
                                                                                    termination proof

                                                                                    Termination proof

                                                                                    call `interleave_strict (List.tl x) (List.tl y)` from `interleave_strict x y`
                                                                                    original:interleave_strict x y
                                                                                    sub:interleave_strict (List.tl x) (List.tl y)
                                                                                    original ordinal:Ordinal.Int (_cnt x)
                                                                                    sub ordinal:Ordinal.Int (_cnt (List.tl x))
                                                                                    path:[y <> [] && x <> []]
                                                                                    proof:
                                                                                    detailed proof
                                                                                    ground_instances:3
                                                                                    definitions:0
                                                                                    inductions:0
                                                                                    search_time:
                                                                                    0.013s
                                                                                    details:
                                                                                    Expand
                                                                                    smt_stats:
                                                                                    num checks:8
                                                                                    arith assert lower:10
                                                                                    arith tableau max rows:5
                                                                                    arith tableau max columns:12
                                                                                    arith pivots:7
                                                                                    rlimit count:3724
                                                                                    mk clause:18
                                                                                    datatype occurs check:40
                                                                                    mk bool var:93
                                                                                    arith assert upper:13
                                                                                    datatype splits:6
                                                                                    decisions:20
                                                                                    arith row summations:13
                                                                                    propagations:26
                                                                                    conflicts:10
                                                                                    arith fixed eqs:10
                                                                                    datatype accessor ax:13
                                                                                    minimized lits:2
                                                                                    arith conflicts:1
                                                                                    arith num rows:5
                                                                                    arith assert diseq:1
                                                                                    datatype constructor ax:15
                                                                                    num allocs:1078678742
                                                                                    final checks:6
                                                                                    added eqs:86
                                                                                    del clause:11
                                                                                    arith eq adapter:13
                                                                                    memory:8.090000
                                                                                    max memory:8.450000
                                                                                    Expand
                                                                                    • start[0.013s]
                                                                                        let (_x_0 : int) = count.list (const 0) x in
                                                                                        let (_x_1 : ty_0 list) = List.tl x in
                                                                                        let (_x_2 : int) = count.list (const 0) _x_1 in
                                                                                        y <> [] && x <> [] && _x_0 >= 0 && _x_2 >= 0
                                                                                        ==> not ((List.tl y) <> [] && _x_1 <> [])
                                                                                            || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                    • simplify
                                                                                      into:
                                                                                      let (_x_0 : ty_0 list) = List.tl x in
                                                                                      let (_x_1 : int) = count.list (const 0) _x_0 in
                                                                                      let (_x_2 : int) = count.list (const 0) x in
                                                                                      (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                       || not ((List.tl y) <> [] && _x_0 <> []))
                                                                                      || not (((y <> [] && x <> []) && _x_2 >= 0) && _x_1 >= 0)
                                                                                      expansions:
                                                                                      []
                                                                                      rewrite_steps:
                                                                                        forward_chaining:
                                                                                        • unroll
                                                                                          expr:
                                                                                          (|count.list_2341/server| (|get.::.1_2314/server| x_2328/server))
                                                                                          expansions:
                                                                                          • unroll
                                                                                            expr:
                                                                                            (|Ordinal.<<_129/client|
                                                                                              (|Ordinal.Int_114/client|
                                                                                                (|count.list_2341/server| (|get.::.1_2314/s…
                                                                                            expansions:
                                                                                            • unroll
                                                                                              expr:
                                                                                              (|count.list_2341/server| x_2328/server)
                                                                                              expansions:
                                                                                              • Unsat

                                                                                              Let's prove that the length of interleave_strict x y is always less than or equal to the sum of the lengths of x and y. We'll do it first using additive and then using multiplicative structural induction:

                                                                                              In [12]:
                                                                                              verify (fun x y ->
                                                                                                List.length @@ interleave_strict x y <= List.length x + List.length y)
                                                                                              [@@induct structural_add (x,y)]
                                                                                              
                                                                                              Out[12]:
                                                                                              - : 'a list -> 'a list -> bool = <fun>
                                                                                              Goal:
                                                                                              
                                                                                              (List.length @@ interleave_strict x y) <= (List.length x + List.length y).
                                                                                              
                                                                                              1 nontautological subgoal.
                                                                                              
                                                                                              Induction scheme:
                                                                                              
                                                                                               φ x []
                                                                                               && φ [] y && (y <> [] && x <> [] && φ (List.tl x) (List.tl y) ==> φ x y).
                                                                                              
                                                                                              3 nontautological subgoals.
                                                                                              
                                                                                              Subgoal 3:
                                                                                              
                                                                                              |---------------------------------------------------------------------------
                                                                                               List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                              
                                                                                              But simplification reduces this to true, using the definitions of List.length
                                                                                              and interleave_strict.
                                                                                              
                                                                                              Subgoal 2:
                                                                                              
                                                                                              |---------------------------------------------------------------------------
                                                                                               List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                              
                                                                                              But simplification reduces this to true, using the definitions of List.length
                                                                                              and interleave_strict.
                                                                                              
                                                                                              Subgoal 1:
                                                                                              
                                                                                               H0. y <> []
                                                                                               H1. x <> []
                                                                                               H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                   (List.length (List.tl x) + List.length (List.tl y))
                                                                                              |---------------------------------------------------------------------------
                                                                                               List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                              
                                                                                              This simplifies, using the definitions of List.length and interleave_strict
                                                                                              to:
                                                                                              
                                                                                              Subgoal 1':
                                                                                              
                                                                                               H0. y <> []
                                                                                               H1. x <> []
                                                                                               H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                   (List.length (List.tl x) + List.length (List.tl y))
                                                                                              |---------------------------------------------------------------------------
                                                                                               List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <=
                                                                                               (1 + List.length (List.tl x) + List.length (List.tl y))
                                                                                              
                                                                                              But simplification reduces this to true, using the definition of List.length.
                                                                                              
                                                                                               Rules:
                                                                                                  (:def List.length)
                                                                                                  (:def interleave_strict)
                                                                                                  (:fc List.len_nonnegative)
                                                                                                  (:induct struct list)
                                                                                              
                                                                                              
                                                                                              Proved
                                                                                              proof
                                                                                              ground_instances:0
                                                                                              definitions:11
                                                                                              inductions:1
                                                                                              search_time:
                                                                                              0.103s
                                                                                              Expand
                                                                                              • start[0.103s, "Goal"]
                                                                                                  List.length (interleave_strict ( :var_0: ) ( :var_1: )) <=
                                                                                                  (List.length ( :var_0: ) + List.length ( :var_1: ))
                                                                                              • subproof

                                                                                                List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                • start[0.103s, "1"]
                                                                                                    List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                • induction on (structural+ x, y)
                                                                                                  :scheme φ x []
                                                                                                          && φ [] y
                                                                                                             && (y <> [] && x <> [] && φ (List.tl x) (List.tl y) ==> φ x y)
                                                                                                • Split (let (_x_0 : int) = List.length x in
                                                                                                         let (_x_1 : int) = List.length [] in
                                                                                                         let (_x_2 : int) = List.length y in
                                                                                                         let (_x_3 : sko_ty_0 list) = List.tl x in
                                                                                                         let (_x_4 : sko_ty_0 list) = List.tl y in
                                                                                                         (List.length (interleave_strict x []) <= (_x_0 + _x_1)
                                                                                                          && List.length (interleave_strict [] y) <= (_x_1 + _x_2))
                                                                                                         && (not
                                                                                                             ((y <> [] && x <> [])
                                                                                                              && List.length (interleave_strict _x_3 _x_4) <=
                                                                                                                 (List.length _x_3 + List.length _x_4))
                                                                                                             || List.length (interleave_strict x y) <= (_x_0 + _x_2))
                                                                                                         :cases [List.length (interleave_strict x []) <=
                                                                                                                 (List.length x + List.length []);
                                                                                                                 List.length (interleave_strict [] y) <=
                                                                                                                 (List.length [] + List.length y);
                                                                                                                 let (_x_0 : sko_ty_0 list) = List.tl x in
                                                                                                                 let (_x_1 : sko_ty_0 list) = List.tl y in
                                                                                                                 ((not (y <> []) || not (x <> []))
                                                                                                                  || not
                                                                                                                     (List.length (interleave_strict _x_0 _x_1) <=
                                                                                                                      (List.length _x_0 + List.length _x_1)))
                                                                                                                 || List.length (interleave_strict x y) <=
                                                                                                                    (List.length x + List.length y)])
                                                                                                  • subproof
                                                                                                    let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : sko_ty_0 list) = List.tl y in ((not (y <> []) || not (x <> [])) || not (List.length (interleave_strict _x_0 _x_1) <= (List.length _x_0 + List.length _x_1))) || List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                    • start[0.103s, "1"]
                                                                                                        let (_x_0 : sko_ty_0 list) = List.tl x in
                                                                                                        let (_x_1 : sko_ty_0 list) = List.tl y in
                                                                                                        ((not (y <> []) || not (x <> []))
                                                                                                         || not
                                                                                                            (List.length (interleave_strict _x_0 _x_1) <=
                                                                                                             (List.length _x_0 + List.length _x_1)))
                                                                                                        || List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                    • simplify
                                                                                                      into:
                                                                                                      let (_x_0 : sko_ty_0 list) = List.tl x in
                                                                                                      let (_x_1 : sko_ty_0 list) = List.tl y in
                                                                                                      let (_x_2 : sko_ty_0 list) = interleave_strict _x_0 _x_1 in
                                                                                                      let (_x_3 : int) = List.length _x_0 in
                                                                                                      let (_x_4 : int) = List.length _x_1 in
                                                                                                      ((not (y <> []) || not (x <> [])) || not (List.length _x_2 <= (_x_3 + _x_4)))
                                                                                                      || List.length ((List.hd y) :: _x_2) <= (1 + _x_3 + _x_4)
                                                                                                      expansions:
                                                                                                      [List.length, List.length, List.length, interleave_strict]
                                                                                                      rewrite_steps:
                                                                                                        forward_chaining:
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                      • simplify
                                                                                                        into:
                                                                                                        true
                                                                                                        expansions:
                                                                                                        List.length
                                                                                                        rewrite_steps:
                                                                                                          forward_chaining:
                                                                                                          • List.len_nonnegative
                                                                                                          • List.len_nonnegative
                                                                                                          • List.len_nonnegative
                                                                                                          • List.len_nonnegative
                                                                                                      • subproof
                                                                                                        List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                                        • start[0.103s, "2"]
                                                                                                            List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                                        • simplify
                                                                                                          into:
                                                                                                          true
                                                                                                          expansions:
                                                                                                          [List.length, List.length, interleave_strict]
                                                                                                          rewrite_steps:
                                                                                                            forward_chaining:
                                                                                                            • List.len_nonnegative
                                                                                                            • List.len_nonnegative
                                                                                                            • List.len_nonnegative
                                                                                                        • subproof
                                                                                                          List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                                          • start[0.103s, "3"]
                                                                                                              List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                                          • simplify
                                                                                                            into:
                                                                                                            true
                                                                                                            expansions:
                                                                                                            [List.length, List.length, interleave_strict]
                                                                                                            rewrite_steps:
                                                                                                              forward_chaining:
                                                                                                              • List.len_nonnegative
                                                                                                              • List.len_nonnegative
                                                                                                              • List.len_nonnegative
                                                                                                      In [13]:
                                                                                                      verify (fun x y ->
                                                                                                        List.length @@ interleave_strict x y <= List.length x + List.length y)
                                                                                                      [@@induct structural_mult (x,y)]
                                                                                                      
                                                                                                      Out[13]:
                                                                                                      - : 'a list -> 'a list -> bool = <fun>
                                                                                                      Goal:
                                                                                                      
                                                                                                      (List.length @@ interleave_strict x y) <= (List.length x + List.length y).
                                                                                                      
                                                                                                      1 nontautological subgoal.
                                                                                                      
                                                                                                      Induction scheme:
                                                                                                      
                                                                                                       φ [] []
                                                                                                       && (y <> [] && φ [] (List.tl y) ==> φ [] y)
                                                                                                          && (x <> [] && φ (List.tl x) [] ==> φ x [])
                                                                                                             && (y <> [] && x <> [] && φ (List.tl x) (List.tl y) ==> φ x y).
                                                                                                      
                                                                                                      4 nontautological subgoals.
                                                                                                      
                                                                                                      Subgoal 4:
                                                                                                      
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length (interleave_strict [] []) <= (2 * List.length [])
                                                                                                      
                                                                                                      But simplification reduces this to true, using the definitions of List.length
                                                                                                      and interleave_strict.
                                                                                                      
                                                                                                      Subgoal 3:
                                                                                                      
                                                                                                       H0. y <> []
                                                                                                       H1. List.length (interleave_strict [] (List.tl y)) <=
                                                                                                           (List.length [] + List.length (List.tl y))
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                                      
                                                                                                      But simplification reduces this to true, using the definitions of List.length
                                                                                                      and interleave_strict.
                                                                                                      
                                                                                                      Subgoal 2:
                                                                                                      
                                                                                                       H0. x <> []
                                                                                                       H1. List.length (interleave_strict (List.tl x) []) <=
                                                                                                           (List.length (List.tl x) + List.length [])
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                                      
                                                                                                      But simplification reduces this to true, using the definitions of List.length
                                                                                                      and interleave_strict.
                                                                                                      
                                                                                                      Subgoal 1:
                                                                                                      
                                                                                                       H0. y <> []
                                                                                                       H1. x <> []
                                                                                                       H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                           (List.length (List.tl x) + List.length (List.tl y))
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                      
                                                                                                      This simplifies, using the definitions of List.length and interleave_strict
                                                                                                      to:
                                                                                                      
                                                                                                      Subgoal 1':
                                                                                                      
                                                                                                       H0. y <> []
                                                                                                       H1. x <> []
                                                                                                       H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                           (List.length (List.tl x) + List.length (List.tl y))
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <=
                                                                                                       (1 + List.length (List.tl x) + List.length (List.tl y))
                                                                                                      
                                                                                                      But simplification reduces this to true, using the definition of List.length.
                                                                                                      
                                                                                                       Rules:
                                                                                                          (:def List.length)
                                                                                                          (:def interleave_strict)
                                                                                                          (:fc List.len_nonnegative)
                                                                                                          (:induct struct list)
                                                                                                      
                                                                                                      
                                                                                                      Proved
                                                                                                      proof
                                                                                                      ground_instances:0
                                                                                                      definitions:16
                                                                                                      inductions:1
                                                                                                      search_time:
                                                                                                      0.093s
                                                                                                      Expand
                                                                                                      • start[0.093s, "Goal"]
                                                                                                          List.length (interleave_strict ( :var_0: ) ( :var_1: )) <=
                                                                                                          (List.length ( :var_0: ) + List.length ( :var_1: ))
                                                                                                      • subproof

                                                                                                        List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                        • start[0.093s, "1"]
                                                                                                            List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                        • induction on (structural* x, y)
                                                                                                          :scheme φ [] []
                                                                                                                  && (y <> [] && φ [] (List.tl y) ==> φ [] y)
                                                                                                                     && (x <> [] && φ (List.tl x) [] ==> φ x [])
                                                                                                                        && (y <> [] && x <> [] && φ (List.tl x) (List.tl y) ==> φ x y)
                                                                                                        • Split (let (_x_0 : int) = List.length [] in
                                                                                                                 let (_x_1 : bool) = y <> [] in
                                                                                                                 let (_x_2 : sko_ty_0 list) = List.tl y in
                                                                                                                 let (_x_3 : int) = List.length _x_2 in
                                                                                                                 let (_x_4 : int) = List.length y in
                                                                                                                 let (_x_5 : bool) = x <> [] in
                                                                                                                 let (_x_6 : sko_ty_0 list) = List.tl x in
                                                                                                                 let (_x_7 : int) = List.length _x_6 in
                                                                                                                 let (_x_8 : int) = List.length x in
                                                                                                                 ((List.length (interleave_strict [] []) <= (2 * _x_0)
                                                                                                                   && (not
                                                                                                                       (_x_1
                                                                                                                        && List.length (interleave_strict [] _x_2) <= (_x_0 + _x_3))
                                                                                                                       || List.length (interleave_strict [] y) <= (_x_0 + _x_4)))
                                                                                                                  && (not
                                                                                                                      (_x_5 && List.length (interleave_strict _x_6 []) <= (_x_7 + _x_0))
                                                                                                                      || List.length (interleave_strict x []) <= (_x_8 + _x_0)))
                                                                                                                 && (not
                                                                                                                     ((_x_1 && _x_5)
                                                                                                                      && List.length (interleave_strict _x_6 _x_2) <= (_x_7 + _x_3))
                                                                                                                     || List.length (interleave_strict x y) <= (_x_8 + _x_4))
                                                                                                                 :cases [List.length (interleave_strict [] []) <= (2 * List.length []);
                                                                                                                         let (_x_0 : sko_ty_0 list) = List.tl y in
                                                                                                                         let (_x_1 : int) = List.length [] in
                                                                                                                         (not (y <> [])
                                                                                                                          || not
                                                                                                                             (List.length (interleave_strict [] _x_0) <=
                                                                                                                              (_x_1 + List.length _x_0)))
                                                                                                                         || List.length (interleave_strict [] y) <=
                                                                                                                            (_x_1 + List.length y);
                                                                                                                         let (_x_0 : sko_ty_0 list) = List.tl x in
                                                                                                                         let (_x_1 : int) = List.length [] in
                                                                                                                         (not (x <> [])
                                                                                                                          || not
                                                                                                                             (List.length (interleave_strict _x_0 []) <=
                                                                                                                              (List.length _x_0 + _x_1)))
                                                                                                                         || List.length (interleave_strict x []) <=
                                                                                                                            (List.length x + _x_1);
                                                                                                                         let (_x_0 : sko_ty_0 list) = List.tl x in
                                                                                                                         let (_x_1 : sko_ty_0 list) = List.tl y in
                                                                                                                         ((not (y <> []) || not (x <> []))
                                                                                                                          || not
                                                                                                                             (List.length (interleave_strict _x_0 _x_1) <=
                                                                                                                              (List.length _x_0 + List.length _x_1)))
                                                                                                                         || List.length (interleave_strict x y) <=
                                                                                                                            (List.length x + List.length y)])
                                                                                                          • subproof
                                                                                                            let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : sko_ty_0 list) = List.tl y in ((not (y <> []) || not (x <> [])) || not (List.length (interleave_strict _x_0 _x_1) <= (List.length _x_0 + List.length _x_1))) || List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                            • start[0.093s, "1"]
                                                                                                                let (_x_0 : sko_ty_0 list) = List.tl x in
                                                                                                                let (_x_1 : sko_ty_0 list) = List.tl y in
                                                                                                                ((not (y <> []) || not (x <> []))
                                                                                                                 || not
                                                                                                                    (List.length (interleave_strict _x_0 _x_1) <=
                                                                                                                     (List.length _x_0 + List.length _x_1)))
                                                                                                                || List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                            • simplify
                                                                                                              into:
                                                                                                              let (_x_0 : sko_ty_0 list) = List.tl x in
                                                                                                              let (_x_1 : sko_ty_0 list) = List.tl y in
                                                                                                              let (_x_2 : sko_ty_0 list) = interleave_strict _x_0 _x_1 in
                                                                                                              let (_x_3 : int) = List.length _x_0 in
                                                                                                              let (_x_4 : int) = List.length _x_1 in
                                                                                                              ((not (y <> []) || not (x <> [])) || not (List.length _x_2 <= (_x_3 + _x_4)))
                                                                                                              || List.length ((List.hd y) :: _x_2) <= (1 + _x_3 + _x_4)
                                                                                                              expansions:
                                                                                                              [List.length, List.length, List.length, interleave_strict]
                                                                                                              rewrite_steps:
                                                                                                                forward_chaining:
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                              • simplify
                                                                                                                into:
                                                                                                                true
                                                                                                                expansions:
                                                                                                                List.length
                                                                                                                rewrite_steps:
                                                                                                                  forward_chaining:
                                                                                                                  • List.len_nonnegative
                                                                                                                  • List.len_nonnegative
                                                                                                                  • List.len_nonnegative
                                                                                                                  • List.len_nonnegative
                                                                                                              • subproof
                                                                                                                let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : int) = List.length [] in (not (x <> []) || not (List.length (interleave_strict _x_0 []) <= (List.length _x_0 + _x_1))) || List.length (interleave_strict x []) <= (List.length x + _x_1)
                                                                                                                • start[0.093s, "2"]
                                                                                                                    let (_x_0 : sko_ty_0 list) = List.tl x in
                                                                                                                    let (_x_1 : int) = List.length [] in
                                                                                                                    (not (x <> [])
                                                                                                                     || not
                                                                                                                        (List.length (interleave_strict _x_0 []) <= (List.length _x_0 + _x_1)))
                                                                                                                    || List.length (interleave_strict x []) <= (List.length x + _x_1)
                                                                                                                • simplify
                                                                                                                  into:
                                                                                                                  true
                                                                                                                  expansions:
                                                                                                                  [List.length, List.length, List.length, interleave_strict]
                                                                                                                  rewrite_steps:
                                                                                                                    forward_chaining:
                                                                                                                    • List.len_nonnegative
                                                                                                                    • List.len_nonnegative
                                                                                                                    • List.len_nonnegative
                                                                                                                    • List.len_nonnegative
                                                                                                                    • List.len_nonnegative
                                                                                                                • subproof
                                                                                                                  let (_x_0 : sko_ty_0 list) = List.tl y in let (_x_1 : int) = List.length [] in (not (y <> []) || not (List.length (interleave_strict [] _x_0) <= (_x_1 + List.length _x_0))) || List.length (interleave_strict [] y) <= (_x_1 + List.length y)
                                                                                                                  • start[0.093s, "3"]
                                                                                                                      let (_x_0 : sko_ty_0 list) = List.tl y in
                                                                                                                      let (_x_1 : int) = List.length [] in
                                                                                                                      (not (y <> [])
                                                                                                                       || not
                                                                                                                          (List.length (interleave_strict [] _x_0) <= (_x_1 + List.length _x_0)))
                                                                                                                      || List.length (interleave_strict [] y) <= (_x_1 + List.length y)
                                                                                                                  • simplify
                                                                                                                    into:
                                                                                                                    true
                                                                                                                    expansions:
                                                                                                                    [List.length, List.length, List.length, interleave_strict]
                                                                                                                    rewrite_steps:
                                                                                                                      forward_chaining:
                                                                                                                      • List.len_nonnegative
                                                                                                                      • List.len_nonnegative
                                                                                                                      • List.len_nonnegative
                                                                                                                      • List.len_nonnegative
                                                                                                                      • List.len_nonnegative
                                                                                                                  • subproof
                                                                                                                    List.length (interleave_strict [] []) <= (2 * List.length [])
                                                                                                                    • start[0.093s, "4"]
                                                                                                                        List.length (interleave_strict [] []) <= (2 * List.length [])
                                                                                                                    • simplify
                                                                                                                      into:
                                                                                                                      true
                                                                                                                      expansions:
                                                                                                                      [List.length, List.length, interleave_strict]
                                                                                                                      rewrite_steps:
                                                                                                                        forward_chaining:
                                                                                                                        • List.len_nonnegative
                                                                                                                        • List.len_nonnegative

                                                                                                                Imandra was able to prove the property using both flavors of structural induction, but we can see that the proof using the additive flavor was shorter. Multiplicative schemes will often result in longer proofs than additive schemes, and thus Imandra uses the additive flavor by default when [@@induct structural ...] is used.