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 -> int -> 'a list = <fun>
termination proof

Termination proof

call `repeat c (n - 1)` from `repeat c n`
originalrepeat c n
subrepeat c (n - 1)
original ordinalOrdinal.Int (_cnt n)
sub ordinalOrdinal.Int (_cnt (n - 1))
path[not (n <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.021s
details
Expand
smt_stats
num checks3
arith-make-feasible5
arith-max-columns11
arith-conflicts1
rlimit count1165
mk clause5
datatype occurs check2
mk bool var18
arith-lower3
decisions2
arith-propagations3
propagations2
arith-bound-propagations-cheap3
arith-max-rows4
conflicts2
datatype accessor ax2
num allocs934569839
final checks1
added eqs6
del clause5
arith eq adapter2
arith-upper6
memory11.290000
max memory24.340000
Expand
  • start[0.021s]
      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.<<_119| (|Ordinal.Int_108| (ite (>= n_2675 1) (+ (- 1) n_2675) 0))
                          (|Ord…
        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:
        
         (x = [] ==> φ x y z) && (not (x = []) && φ (List.tl x) y z ==> φ x y z).
        
        2 nontautological subgoals.
        
        Subgoal 1.2:
        
         H0. x = []
        |---------------------------------------------------------------------------
         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. not (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_instances0
        definitions5
        inductions1
        search_time
        0.320s
        Expand
        • start[0.320s, "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.320s, "1"]
              List.append x (List.append y z) = List.append (List.append x y) z
          • induction on (functional )
            :scheme (x = [] ==> φ x y z)
                    && (not (x = []) && φ (List.tl x) y z ==> φ x y z)
          • Split (let (_x_0 : bool) = not (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 [not (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
                           (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 (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.083s, "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
                  (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
                  not (x = []) || List.append x (List.append y z) = List.append (List.append x y) z
                  • start[0.083s, "1.2"]
                      not (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:
                
                 (x = [] ==> φ x y) && (not (x = []) && φ (List.tl x) y ==> φ x y).
                
                2 nontautological subgoals.
                
                Subgoal 1.2:
                
                 H0. x = []
                |---------------------------------------------------------------------------
                 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. not (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_instances0
                definitions6
                inductions1
                search_time
                0.284s
                Expand
                • start[0.284s, "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.284s, "1"]
                      List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                  • induction on (functional )
                    :scheme (x = [] ==> φ x y) && (not (x = []) && φ (List.tl x) y ==> φ x y)
                  • Split (let (_x_0 : bool) = not (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 [not (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
                                   (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 (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.217s, "1.1"]
                          let (_x_0 : sko_ty_0 list) = List.tl x in
                          let (_x_1 : sko_ty_0 list) = List.rev y in
                          (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.hd x] in
                        let (_x_3 : sko_ty_0 list) = List.rev y in
                        let (_x_4 : sko_ty_0 list) = List.rev _x_0 in
                        (List.append _x_1 _x_2 = List.append _x_3 (List.append _x_4 _x_2) || x = [])
                        || not (_x_1 = 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
                            not (x = []) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                            • start[0.217s, "1.2"]
                                not (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]:
                        - : int 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:
                        
                         (lst = [] ==> φ lst) && (not (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
                         H2. lst = []
                        |---------------------------------------------------------------------------
                         false
                        
                        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. List.fold_right ( + ) 1 lst <= 0
                         H2. not (lst = [])
                         H3. not (List.for_all (fun x -> x > 0) (List.tl lst))
                             || not (List.fold_right ( + ) 1 (List.tl 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_instances0
                        definitions5
                        inductions1
                        search_time
                        0.162s
                        Expand
                        • start[0.162s, "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.162s, "1"]
                              not (List.for_all (fun x -> x > 0) lst)
                              || not (List.fold_right ( + ) 1 lst <= 0)
                          • induction on (functional )
                            :scheme (lst = [] ==> φ lst)
                                    && (not (lst = []) && φ (List.tl lst) ==> φ lst)
                          • Split (let (_x_0 : bool)
                                       = not (List.for_all (fun x -> x > 0) lst)
                                         || not (List.fold_right ( + ) 1 lst <= 0)
                                   in
                                   let (_x_1 : bool) = not (lst = []) in
                                   let (_x_2 : int list) = List.tl lst in
                                   (_x_0 || _x_1)
                                   && (_x_0
                                       || not
                                          (_x_1
                                           && (not (List.for_all (fun x -> x > 0) _x_2)
                                               || not (List.fold_right ( + ) 1 _x_2 <= 0))))
                                   :cases [(not (List.for_all (fun x -> x > 0) lst)
                                            || not (List.fold_right ( + ) 1 lst <= 0))
                                           || not (lst = []);
                                           let (_x_0 : int list) = List.tl lst in
                                           ((not (List.for_all (fun x -> x > 0) lst)
                                             || not (List.fold_right ( + ) 1 lst <= 0))
                                            || lst = [])
                                           || not
                                              (not (List.for_all (fun x -> x > 0) _x_0)
                                               || not (List.fold_right ( + ) 1 _x_0 <= 0))])
                            • subproof
                              let (_x_0 : int list) = List.tl lst in ((not (List.for_all (fun x -> x > 0) lst) || not (List.fold_right ( + ) 1 lst <= 0)) || lst = []) || not (not (List.for_all (fun x -> x > 0) _x_0) || not (List.fold_right ( + ) 1 _x_0 <= 0))
                              • start[0.098s, "1.1"]
                                  let (_x_0 : int list) = List.tl lst in
                                  ((not (List.for_all (fun x -> x > 0) lst)
                                    || not (List.fold_right ( + ) 1 lst <= 0))
                                   || lst = [])
                                  || not
                                     (not (List.for_all (fun x -> x > 0) _x_0)
                                      || not (List.fold_right ( + ) 1 _x_0 <= 0))
                              • simplify
                                into
                                true
                                expansions
                                [List.for_all, List.fold_right, 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)) || not (lst = [])
                                  • start[0.098s, "1.2"]
                                      (not (List.for_all (fun x -> x > 0) lst)
                                       || not (List.fold_right ( + ) 1 lst <= 0))
                                      || not (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 -> int -> 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. not (n <= 0)
                                 H1. n >= 1 ==> List.length (repeat c (-1 + n)) = -1 + n
                                 H2. n >= 0
                                |---------------------------------------------------------------------------
                                 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_instances0
                                definitions4
                                inductions1
                                search_time
                                0.128s
                                Expand
                                • start[0.128s, "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.128s, "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)
                                           && ((not
                                                (_x_1 && (not (n >= 1) || List.length (repeat c _x_3) = _x_3))
                                                || _x_0)
                                               || _x_2)
                                           :cases [(not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n;
                                                   let (_x_0 : int) = -1 + n in
                                                   ((n <= 0
                                                     || not (n >= 1 ==> List.length (repeat c _x_0) = _x_0))
                                                    || not (n >= 0))
                                                   || List.length (repeat c n) = n])
                                    • subproof
                                      let (_x_0 : int) = -1 + n in ((n <= 0 || not (n >= 1 ==> List.length (repeat c _x_0) = _x_0)) || not (n >= 0)) || List.length (repeat c n) = n
                                      • start[0.067s, "1.1"]
                                          let (_x_0 : int) = -1 + n in
                                          ((n <= 0 || not (n >= 1 ==> List.length (repeat c _x_0) = _x_0))
                                           || not (n >= 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
                                          • List.len_nonnegative
                                          • List.len_nonnegative
                                      • subproof
                                        (not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n
                                        • start[0.067s, "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 : int -> int = <fun>
                                    val induct_scheme : int -> bool = <fun>
                                    
                                    termination proof

                                    Termination proof

                                    call `sum (n - 1)` from `sum n`
                                    originalsum n
                                    subsum (n - 1)
                                    original ordinalOrdinal.Int (_cnt n)
                                    sub ordinalOrdinal.Int (_cnt (n - 1))
                                    path[not (n <= 0)]
                                    proof
                                    detailed proof
                                    ground_instances1
                                    definitions0
                                    inductions0
                                    search_time
                                    0.017s
                                    details
                                    Expand
                                    smt_stats
                                    num checks3
                                    arith-make-feasible5
                                    arith-max-columns11
                                    arith-conflicts1
                                    rlimit count1165
                                    mk clause5
                                    datatype occurs check2
                                    mk bool var18
                                    arith-lower3
                                    decisions2
                                    arith-propagations3
                                    propagations2
                                    arith-bound-propagations-cheap3
                                    arith-max-rows4
                                    conflicts2
                                    datatype accessor ax2
                                    num allocs2796939456
                                    final checks1
                                    added eqs6
                                    del clause5
                                    arith eq adapter2
                                    arith-upper6
                                    memory26.380000
                                    max memory46.450000
                                    Expand
                                    • start[0.017s]
                                        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.<<_119| (|Ordinal.Int_108| (ite (>= n_3108 1) (+ (- 1) n_3108) 0))
                                                            (|Ord…
                                          expansions
                                          • Unsat

                                          termination proof

                                          Termination proof

                                          call `induct_scheme (n - 1)` from `induct_scheme n`
                                          originalinduct_scheme n
                                          subinduct_scheme (n - 1)
                                          original ordinalOrdinal.Int (_cnt n)
                                          sub ordinalOrdinal.Int (_cnt (n - 1))
                                          path[not (n = 1) && not (n <= 0)]
                                          proof
                                          detailed proof
                                          ground_instances1
                                          definitions0
                                          inductions0
                                          search_time
                                          0.033s
                                          details
                                          Expand
                                          smt_stats
                                          num checks3
                                          arith-make-feasible5
                                          arith-max-columns12
                                          arith-conflicts1
                                          rlimit count1277
                                          mk clause5
                                          datatype occurs check2
                                          mk bool var22
                                          arith-lower3
                                          arith-diseq3
                                          decisions2
                                          arith-propagations5
                                          propagations3
                                          arith-bound-propagations-cheap5
                                          arith-max-rows5
                                          conflicts2
                                          datatype accessor ax2
                                          num allocs2873533680
                                          final checks1
                                          added eqs6
                                          del clause5
                                          arith eq adapter4
                                          arith-upper8
                                          memory26.640000
                                          max memory46.450000
                                          Expand
                                          • start[0.033s]
                                              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 = 2) && not (n <= 1))
                                             || Ordinal.( << ) (Ordinal.Int (if n >= 1 then -1 + n else 0))
                                                (Ordinal.Int (if n >= 0 then n else 0)))
                                            || not (not (n = 1) && not (n <= 0))
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|Ordinal.<<_119| (|Ordinal.Int_108| (ite (>= n_3134 1) (+ (- 1) n_3134) 0))
                                                                  (|Ord…
                                                expansions
                                                • Unsat

                                                In [7]:
                                                verify (fun n -> n >= 0 ==> sum n = (n * (n+1)) / 2) [@@induct functional induct_scheme]
                                                
                                                Out[7]:
                                                - : int -> 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!
                                                
                                                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_instances0
                                                definitions4
                                                inductions1
                                                search_time
                                                0.249s
                                                Expand
                                                • start[0.249s, "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.248s, "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.247s, "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.247s, "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 -> int = <fun>
                                                        
                                                        termination proof

                                                        Termination proof

                                                        call `size (Destruct(Node, 1, x))` from `size x`
                                                        originalsize x
                                                        subsize (Destruct(Node, 1, x))
                                                        original ordinalOrdinal.Int (_cnt x)
                                                        sub ordinalOrdinal.Int (_cnt (Destruct(Node, 1, x)))
                                                        path[Is_a(Node, x)]
                                                        proof
                                                        detailed proof
                                                        ground_instances3
                                                        definitions0
                                                        inductions0
                                                        search_time
                                                        0.017s
                                                        details
                                                        Expand
                                                        smt_stats
                                                        num checks8
                                                        arith-make-feasible34
                                                        arith-max-columns17
                                                        arith-conflicts3
                                                        rlimit count5874
                                                        mk clause40
                                                        datatype occurs check19
                                                        mk bool var121
                                                        arith-lower33
                                                        arith-diseq4
                                                        datatype splits5
                                                        decisions37
                                                        arith-propagations2
                                                        propagations27
                                                        arith-bound-propagations-cheap2
                                                        arith-max-rows5
                                                        conflicts11
                                                        datatype accessor ax11
                                                        datatype constructor ax25
                                                        num allocs3680931165
                                                        final checks5
                                                        added eqs110
                                                        del clause23
                                                        arith eq adapter23
                                                        arith-upper24
                                                        memory30.010000
                                                        max memory46.450000
                                                        Expand
                                                        • start[0.017s]
                                                            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
                                                          (not Is_a(Node, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                          || not ((Is_a(Node, x) && _x_2 >= 0) && _x_1 >= 0)
                                                          expansions
                                                          []
                                                          rewrite_steps
                                                            forward_chaining
                                                            • unroll
                                                              expr
                                                              (|`count.tree (const 0)[0]`_3259| x_3246)
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (|`count.tree (const 0)[0]`_3259| (|get.Node.1_3240| x_3246))
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (|Ordinal.<<_119| (|Ordinal.Int_108|
                                                                                      (|`count.tree (const 0)[0]`_3259|
                                                                           …
                                                                  expansions
                                                                  • Unsat

                                                                  call `size (Destruct(Node, 2, x))` from `size x`
                                                                  originalsize x
                                                                  subsize (Destruct(Node, 2, x))
                                                                  original ordinalOrdinal.Int (_cnt x)
                                                                  sub ordinalOrdinal.Int (_cnt (Destruct(Node, 2, x)))
                                                                  path[Is_a(Node, x)]
                                                                  proof
                                                                  detailed proof
                                                                  ground_instances3
                                                                  definitions0
                                                                  inductions0
                                                                  search_time
                                                                  0.016s
                                                                  details
                                                                  Expand
                                                                  smt_stats
                                                                  num checks8
                                                                  arith-make-feasible34
                                                                  arith-max-columns17
                                                                  arith-conflicts3
                                                                  rlimit count2937
                                                                  mk clause40
                                                                  datatype occurs check19
                                                                  mk bool var121
                                                                  arith-lower33
                                                                  arith-diseq4
                                                                  datatype splits5
                                                                  decisions37
                                                                  arith-propagations2
                                                                  propagations27
                                                                  arith-bound-propagations-cheap2
                                                                  arith-max-rows5
                                                                  conflicts11
                                                                  datatype accessor ax11
                                                                  datatype constructor ax25
                                                                  num allocs3637218984
                                                                  final checks5
                                                                  added eqs110
                                                                  del clause23
                                                                  arith eq adapter23
                                                                  arith-upper24
                                                                  memory27.440000
                                                                  max memory46.450000
                                                                  Expand
                                                                  • start[0.016s]
                                                                      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 : ty_0 tree) = Destruct(Node, 2, x) in
                                                                    let (_x_1 : int) = count.tree (const 0) _x_0 in
                                                                    let (_x_2 : int) = count.tree (const 0) x in
                                                                    (not Is_a(Node, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                    || not ((Is_a(Node, x) && _x_2 >= 0) && _x_1 >= 0)
                                                                    expansions
                                                                    []
                                                                    rewrite_steps
                                                                      forward_chaining
                                                                      • unroll
                                                                        expr
                                                                        (|`count.tree (const 0)[0]`_3259| x_3246)
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|`count.tree (const 0)[0]`_3259| (|get.Node.2_3241| x_3246))
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (|Ordinal.<<_119| (|Ordinal.Int_108|
                                                                                                (|`count.tree (const 0)[0]`_3259|
                                                                                     …
                                                                            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_instances0
                                                                            definitions2
                                                                            inductions1
                                                                            search_time
                                                                            0.033s
                                                                            Expand
                                                                            • start[0.033s, "Goal"] size :var_0: > 0
                                                                            • subproof

                                                                              not (size x <= 0)
                                                                              • start[0.033s, "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.032s, "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.032s, "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`
                                                                                    originalinterleave_strict x y
                                                                                    subinterleave_strict (List.tl x) (List.tl y)
                                                                                    original ordinalOrdinal.Int (_cnt x)
                                                                                    sub ordinalOrdinal.Int (_cnt (List.tl x))
                                                                                    path[not (x = [] || y = [])]
                                                                                    proof
                                                                                    detailed proof
                                                                                    ground_instances3
                                                                                    definitions0
                                                                                    inductions0
                                                                                    search_time
                                                                                    0.013s
                                                                                    details
                                                                                    Expand
                                                                                    smt_stats
                                                                                    num checks7
                                                                                    arith-make-feasible10
                                                                                    arith-max-columns13
                                                                                    arith-conflicts1
                                                                                    rlimit count2129
                                                                                    mk clause3
                                                                                    datatype occurs check31
                                                                                    mk bool var66
                                                                                    arith-lower4
                                                                                    datatype splits6
                                                                                    decisions17
                                                                                    propagations2
                                                                                    arith-max-rows5
                                                                                    conflicts11
                                                                                    datatype accessor ax7
                                                                                    datatype constructor ax17
                                                                                    num allocs4016207494
                                                                                    final checks6
                                                                                    added eqs55
                                                                                    del clause1
                                                                                    arith eq adapter3
                                                                                    arith-upper6
                                                                                    memory27.990000
                                                                                    max memory46.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
                                                                                        not (x = [] || y = []) && _x_0 >= 0 && _x_2 >= 0
                                                                                        ==> (_x_1 = [] || List.tl y = [])
                                                                                            || 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
                                                                                      ((_x_0 = [] || List.tl y = [])
                                                                                       || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                      || not ((not (x = [] || y = []) && _x_2 >= 0) && _x_1 >= 0)
                                                                                      expansions
                                                                                      []
                                                                                      rewrite_steps
                                                                                        forward_chaining
                                                                                        • unroll
                                                                                          expr
                                                                                          (|`count.list (const 0)[0]`_3386| x_3373)
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|`count.list (const 0)[0]`_3386| (|get.::.1_3365| x_3373))
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (|Ordinal.<<_119| (|Ordinal.Int_108|
                                                                                                                  (|`count.list (const 0)[0]`_3386| (|get.::.…
                                                                                              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_instances0
                                                                                              definitions11
                                                                                              inductions1
                                                                                              search_time
                                                                                              0.127s
                                                                                              Expand
                                                                                              • start[0.127s, "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.127s, "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.127s, "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.127s, "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.127s, "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_instances0
                                                                                                      definitions16
                                                                                                      inductions1
                                                                                                      search_time
                                                                                                      0.129s
                                                                                                      Expand
                                                                                                      • start[0.129s, "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.129s, "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.128s, "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.128s, "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.128s, "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.128s, "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.