# 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 :
let rec repeat c n =
if n <= 0 then
[]
else
c :: (repeat c (n-1))

Out:
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 (if n >= 0 then n else 0)
sub ordinalOrdinal.Int (if (n - 1) >= 0 then n - 1 else 0)
path[not (n <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.012s
details
Expand
smt_stats
 num checks 3 arith assert lower 8 arith pivots 2 rlimit count 1027 mk clause 4 datatype occurs check 2 mk bool var 20 arith assert upper 3 decisions 2 arith add rows 3 propagations 2 conflicts 2 arith fixed eqs 2 datatype accessor ax 2 arith conflicts 1 num allocs 880241 final checks 1 added eqs 6 del clause 4 arith eq adapter 2 memory 5.74 max memory 5.74
Expand
• start[0.012s]
not (n <= 0)
&& (if n >= 0 then n else 0) >= 0
&& (if (n - 1) >= 0 then n - 1 else 0) >= 0
==> (n - 1) <= 0
|| Ordinal.( << ) (Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0))
(Ordinal.Int (if n >= 0 then n else 0))
• ##### simplify
 into (not ((not (n <= 0) && (if n >= 0 then n else 0) >= 0) && (if n >= 1 then -1 + n else 0) >= 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.<<_102| (|Ordinal.Int_93| (ite (>= n_1198 1) (+ (- 1) n_1198) 0)) (|Ordi… expansions
• ##### unsat
(let ((a!1 (not (= n_1198 (ite (>= n_1198 0) n_1198 0))))
(a!2 (+ n_1198 (* (- 1) (ite (>= n_1…

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 :
lemma assoc_append x y z =
x @ (y @ z) = (x @ y) @ z [@@auto] [@@rw]

Out:
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 = [] ==> φ z y x) && (not (x = []) && φ z y (List.tl x) ==> φ z y x).

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_instances 0 definitions 5 inductions 1 search_time 0.093s
Expand
• start[0.093s, "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.093s, "1"]
List.append x (List.append y z) = List.append (List.append x y) z
• induction on (functional )
:scheme (x = [] ==> φ z y x)
&& (not (x = []) && φ z y (List.tl x) ==> φ z y x)
• Split ((not (x = [])
|| List.append x (List.append y z) = List.append (List.append x y) z)
&& (not
(not (x = [])
&& 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)
:cases [not (x = [])
|| List.append x (List.append y z) =
List.append (List.append x y) z;
(x = []
|| not
(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])
• ##### subproof
(x = [] || not (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
• start[0.051s, "1.1"]
(x = []
|| not
(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
• ###### 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.051s, "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 :
lemma rev_append x y =
List.rev (x @ y) = List.rev y @ List.rev x
[@@auto]

Out:
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 = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x).

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_instances 0 definitions 6 inductions 1 search_time 0.155s
Expand
• start[0.155s, "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.154s, "1"]
List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
• induction on (functional )
:scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
• Split ((not (x = [])
|| List.rev (List.append x y) = List.append (List.rev y) (List.rev x))
&& (not
(not (x = [])
&& 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))
:cases [not (x = [])
|| List.rev (List.append x y) =
List.append (List.rev y) (List.rev x);
(x = []
|| not
(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)])
• ##### subproof
(x = [] || not (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)
• start[0.109s, "1.1"]
(x = []
|| not
(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)
• ###### simplify
 into (x = [] || not (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]) 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.109s, "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 :
verify (fun lst ->
List.for_all (fun x -> x > 0) lst ==>
List.fold_right (+) ~base:1 lst > 0)
[@@auto]

Out:
- : 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. lst = []
H1. List.for_all (fun x -> x > 0) lst
H2. List.fold_right + 1 lst <= 0
|---------------------------------------------------------------------------
false

But simplification reduces this to true, using the definition of
List.fold_right.

Subgoal 1.1:

H0. not (lst = [])
H1. not (List.for_all (fun x -> x > 0) (List.tl lst))
|| not (List.fold_right + 1 (List.tl lst) <= 0)
H2. List.for_all (fun x -> x > 0) lst
H3. List.fold_right + 1 lst <= 0
|---------------------------------------------------------------------------
false

But simplification reduces this to true, using the definitions of
List.fold_right and List.for_all.

ⓘ  Rules:
(:def List.fold_right)
(:def List.for_all)
(:induct List.for_all)


Proved
proof
 ground_instances 0 definitions 3 inductions 1 search_time 0.092s
Expand
• start[0.092s, "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.092s, "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 (((not (lst = []) || not (List.for_all (fun x -> x > 0) lst))
|| not (List.fold_right + 1 lst <= 0))
&& ((not
(not (lst = [])
&& (not (List.for_all (fun x -> x > 0) (List.tl lst))
|| not (List.fold_right + 1 (List.tl lst) <= 0)))
|| not (List.for_all (fun x -> x > 0) lst))
|| not (List.fold_right + 1 lst <= 0))
:cases [(not (lst = []) || 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) (List.tl lst))
|| not (List.fold_right + 1 (List.tl lst) <= 0)))
|| not (List.for_all (fun x -> x > 0) lst))
|| not (List.fold_right + 1 lst <= 0)])
• ##### subproof
((lst = [] || not (not (List.for_all (fun x -> x > 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)
• start[0.029s, "1.1"]
((lst = []
|| not
(not (List.for_all (fun x -> x > 0) (List.tl lst))
|| not (List.fold_right + 1 (List.tl lst) <= 0)))
|| not (List.for_all (fun x -> x > 0) lst))
|| not (List.fold_right + 1 lst <= 0)
• ###### simplify
 into true expansions [List.for_all, List.fold_right] rewrite_steps forward_chaining
• ##### subproof
(not (lst = []) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)
• start[0.029s, "1.2"]
(not (lst = []) || not (List.for_all (fun x -> x > 0) lst))
|| not (List.fold_right + 1 lst <= 0)
• ###### 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 :
lemma repeat_len c n =
n >= 0 ==>
List.length (repeat c n) = n [@@auto]

Out:
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 ==> φ n c) && (not (n <= 0) && φ (n - 1) c ==> φ n c).

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_instances 0 definitions 4 inductions 1 search_time 0.103s
Expand
• start[0.103s, "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.103s, "1"] not (n >= 0) || List.length (repeat c n) = n
• induction on (functional )
:scheme (n <= 0 ==> φ n c) && (not (n <= 0) && φ (n - 1) c ==> φ n c)
• Split (((not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n)
&& ((not
(not (n <= 0)
&& (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n))
|| not (n >= 0))
|| List.length (repeat c n) = n)
:cases [(not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n;
((n <= 0
|| not
(not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n))
|| not (n >= 0))
|| List.length (repeat c n) = n])
• ##### subproof
((n <= 0 || not (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n)) || not (n >= 0)) || List.length (repeat c n) = n
• start[0.031s, "1.1"]
((n <= 0 || not (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n))
|| not (n >= 0))
|| List.length (repeat c n) = n
• ###### simplify
 into true expansions [List.length, repeat] rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegative
• ##### subproof
(not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n
• start[0.031s, "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 :
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:
val sum : int -> Z.t = <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 (if n >= 0 then n else 0)
sub ordinalOrdinal.Int (if (n - 1) >= 0 then n - 1 else 0)
path[not (n <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.010s
details
Expand
smt_stats
 num checks 3 arith assert lower 8 arith pivots 2 rlimit count 1027 mk clause 4 datatype occurs check 2 mk bool var 20 arith assert upper 3 decisions 2 arith add rows 3 propagations 2 conflicts 2 arith fixed eqs 2 datatype accessor ax 2 arith conflicts 1 num allocs 4.05199e+08 final checks 1 added eqs 6 del clause 4 arith eq adapter 2 memory 20.17 max memory 31.88
Expand
• start[0.010s]
not (n <= 0)
&& (if n >= 0 then n else 0) >= 0
&& (if (n - 1) >= 0 then n - 1 else 0) >= 0
==> (n - 1) <= 0
|| Ordinal.( << ) (Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0))
(Ordinal.Int (if n >= 0 then n else 0))
• ##### simplify
 into (not ((not (n <= 0) && (if n >= 0 then n else 0) >= 0) && (if n >= 1 then -1 + n else 0) >= 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.<<_102| (|Ordinal.Int_93| (ite (>= n_1485 1) (+ (- 1) n_1485) 0)) (|Ordi… expansions
• ##### unsat
(let ((a!1 (not (= n_1485 (ite (>= n_1485 0) n_1485 0))))
(a!2 (+ n_1485 (* (- 1) (ite (>= n_1…

termination proof

### Termination proof

call induct_scheme (n - 1) from induct_scheme n
originalinduct_scheme n
subinduct_scheme (n - 1)
original ordinalOrdinal.Int (if n >= 0 then n else 0)
sub ordinalOrdinal.Int (if (n - 1) >= 0 then n - 1 else 0)
path[not (n = 1) && not (n <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.010s
details
Expand
smt_stats
 num checks 3 arith assert lower 10 arith pivots 2 rlimit count 1133 mk clause 7 datatype occurs check 2 mk bool var 24 arith assert upper 3 decisions 2 arith add rows 3 propagations 3 conflicts 2 arith fixed eqs 2 datatype accessor ax 2 arith conflicts 1 arith assert diseq 3 num allocs 4.41241e+08 final checks 1 added eqs 6 del clause 7 arith eq adapter 4 memory 20.55 max memory 31.88
Expand
• start[0.010s]
not (n = 1)
&& not (n <= 0)
&& (if n >= 0 then n else 0) >= 0
&& (if (n - 1) >= 0 then n - 1 else 0) >= 0
==> not (not (n - 1 = 1) && not ((n - 1) <= 0))
|| Ordinal.( << ) (Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0))
(Ordinal.Int (if n >= 0 then n else 0))
• ##### simplify
 into (not (((not (n = 1) && not (n <= 0)) && (if n >= 0 then n else 0) >= 0) && (if n >= 1 then -1 + n else 0) >= 0) || 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)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (ite (>= n_1496 1) (+ (- 1) n_1496) 0)) (|Ordi… expansions
• ##### unsat
(let ((a!1 (not (= n_1496 (ite (>= n_1496 0) n_1496 0))))
(a!2 (+ n_1496 (* (- 1) (ite (>= n_1…

In :
verify (fun n -> n >= 0 ==> sum n = (n * (n+1)) / 2) [@@induct functional induct_scheme]

Out:
- : 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. not (n <= 0)
H1. not (n = 1)
H2. n >= 1 ==> sum (-1 + n) = (n * (-1 + n)) / 2
H3. n >= 0
|---------------------------------------------------------------------------
sum n = (n * (1 + n)) / 2

But simplification reduces this to true, using the definition of sum.

ⓘ  Rules:
(:def sum)
(:induct induct_scheme)


Proved
proof
 ground_instances 0 definitions 4 inductions 1 search_time 0.098s
Expand
• start[0.098s, "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.098s, "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 (((not (n = 1) && not (n <= 0) || not (n >= 0))
|| sum n = (n * (1 + n)) / 2)
&& ((not
((not (n <= 0) && not (n = 1))
&& (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2))
|| not (n >= 0))
|| sum n = (n * (1 + n)) / 2)
:cases [(not (n >= 0) || not (n = 1) && not (n <= 0))
|| sum n = (n * (1 + n)) / 2;
(((n <= 0 || n = 1)
|| not (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2))
|| not (n >= 0))
|| sum n = (n * (1 + n)) / 2])
• ##### subproof
(((n <= 0 || n = 1) || not (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2)) || not (n >= 0)) || sum n = (n * (1 + n)) / 2
• start[0.096s, "1"]
(((n <= 0 || n = 1)
|| not (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2))
|| not (n >= 0))
|| 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.096s, "2"]
(not (n >= 0) || not (n = 1) && not (n <= 0)) || sum n = (n * (1 + n)) / 2
• ###### simplify
 into (not (n = 1) || sum n = (n * (1 + n)) / 2) && (((not (n >= 0) || not (n <= 0)) || n = 1) || sum n = (n * (1 + n)) / 2) 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 :
type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf

Out:
type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf

In :
let rec size (x : 'a tree) =
match x with
| Node (_, a,b) -> size a + size b
| Leaf -> 1

Out:
val size : 'a tree -> Z.t = <fun>

termination proof

### Termination proof

call size (Destruct(Node, 1, x)) from size x
originalsize x
subsize (Destruct(Node, 1, x))
original ordinalOrdinal.Int (Ordinal.count x)
sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 1, x)))
path[Is_a(Node, x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.012s
details
Expand
smt_stats
 num checks 8 arith assert lower 12 arith pivots 12 rlimit count 5064 mk clause 17 datatype occurs check 12 mk bool var 68 arith gcd tests 4 arith assert upper 10 datatype splits 3 decisions 15 arith add rows 22 propagations 11 arith patches 1 conflicts 6 arith fixed eqs 4 datatype accessor ax 7 arith conflicts 2 datatype constructor ax 11 num allocs 7.85054e+08 final checks 5 added eqs 42 del clause 10 arith ineq splits 1 arith eq adapter 7 memory 21.41 max memory 35.85
Expand
• start[0.012s]
Is_a(Node, x)
&& Ordinal.count x >= 0 && Ordinal.count (Destruct(Node, 1, x)) >= 0
==> not Is_a(Node, Destruct(Node, 1, x))
&& not Is_a(Node, Destruct(Node, 1, x))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, x))))
(Ordinal.Int (Ordinal.count x))
• ##### simplify
 into (not ((Is_a(Node, x) && Ordinal.count x >= 0) && Ordinal.count (Destruct(Node, 1, x)) >= 0) || not Is_a(Node, Destruct(Node, 1, x))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, x)))) (Ordinal.Int (Ordinal.count x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 tree_1569| … expansions
• unroll
 expr (|count_ty_0 tree_1569| (|get.Node.1_1552| x_1558)) expansions
• unroll
 expr (|count_ty_0 tree_1569| x_1558) expansions
• ##### unsat
(let ((a!1 (ite (>= (|count_ty_0 tree_1569| (|get.Node.2_1553| x_1558)) 0)
(|count…

call size (Destruct(Node, 2, x)) from size x
originalsize x
subsize (Destruct(Node, 2, x))
original ordinalOrdinal.Int (Ordinal.count x)
sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 2, x)))
path[Is_a(Node, x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 8 arith assert lower 12 arith pivots 12 rlimit count 2532 mk clause 17 datatype occurs check 12 mk bool var 68 arith gcd tests 4 arith assert upper 10 datatype splits 3 decisions 15 arith add rows 22 propagations 11 arith patches 1 conflicts 6 arith fixed eqs 4 datatype accessor ax 7 arith conflicts 2 datatype constructor ax 11 num allocs 7.5988e+08 final checks 5 added eqs 42 del clause 10 arith ineq splits 1 arith eq adapter 7 memory 18.52 max memory 35.85
Expand
• start[0.013s]
Is_a(Node, x)
&& Ordinal.count x >= 0 && Ordinal.count (Destruct(Node, 2, x)) >= 0
==> not Is_a(Node, Destruct(Node, 2, x))
&& not Is_a(Node, Destruct(Node, 2, x))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 2, x))))
(Ordinal.Int (Ordinal.count x))
• ##### simplify
 into (not ((Is_a(Node, x) && Ordinal.count x >= 0) && Ordinal.count (Destruct(Node, 2, x)) >= 0) || not Is_a(Node, Destruct(Node, 2, x))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 2, x)))) (Ordinal.Int (Ordinal.count x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 tree_1569| … expansions
• unroll
 expr (|count_ty_0 tree_1569| (|get.Node.2_1553| x_1558)) expansions
• unroll
 expr (|count_ty_0 tree_1569| x_1558) expansions
• ##### unsat
(let ((a!1 (ite (>= (|count_ty_0 tree_1569| (|get.Node.1_1552| x_1558)) 0)
(|count…

In :
verify (fun x -> size x > 0) [@@induct structural x]

Out:
- : '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. Is_a(Node, x)
H1. not (size (Destruct(Node, 1, x)) <= 0)
H2. not (size (Destruct(Node, 2, x)) <= 0)
H3. size x <= 0
|---------------------------------------------------------------------------
false

But simplification reduces this to true, using the definition of size.

ⓘ  Rules:
(:def size)
(:induct struct tree)


Proved
proof
 ground_instances 0 definitions 2 inductions 1 search_time 0.012s
Expand
• start[0.012s, "Goal"] size :var_0: > 0
• #### subproof

not (size x <= 0)
• start[0.012s, "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
((Is_a(Node, x) && not (size (Destruct(Node, 1, x)) <= 0))
&& not (size (Destruct(Node, 2, x)) <= 0))
|| not (size x <= 0))
:cases [not (size Leaf <= 0);
((not Is_a(Node, x) || size (Destruct(Node, 1, x)) <= 0)
|| size (Destruct(Node, 2, x)) <= 0)
|| not (size x <= 0)])
• ##### subproof
((not Is_a(Node, x) || size (Destruct(Node, 1, x)) <= 0) || size (Destruct(Node, 2, x)) <= 0) || not (size x <= 0)
• start[0.012s, "1"]
((not Is_a(Node, x) || size (Destruct(Node, 1, x)) <= 0)
|| size (Destruct(Node, 2, x)) <= 0)
|| not (size x <= 0)
• ###### simplify
 into true expansions size rewrite_steps forward_chaining
• ##### subproof
not (size Leaf <= 0)
• start[0.012s, "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 :
let rec interleave_strict x y = match x, y with
| [], _ | _ , [] -> []
| x::xs, y::ys -> x::y::(interleave_strict xs ys)

Out:
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 (Ordinal.count x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
path[not (x = [] || y = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.023s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 3 rlimit count 2053 mk clause 3 datatype occurs check 27 mk bool var 70 arith assert upper 5 datatype splits 6 decisions 15 arith add rows 7 propagations 1 conflicts 11 arith fixed eqs 4 datatype accessor ax 7 arith conflicts 1 datatype constructor ax 17 num allocs 9.06221e+08 final checks 6 added eqs 57 del clause 1 arith eq adapter 3 memory 19.16 max memory 35.85
Expand
• start[0.023s]
not (x = [] || y = [])
&& Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
==> (List.tl x = [] || List.tl y = [])
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
(Ordinal.Int (Ordinal.count x))
• ##### simplify
 into ((not ((not (x = [] || y = []) && Ordinal.count x >= 0) && Ordinal.count (List.tl x) >= 0) || List.tl x = []) || List.tl y = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x))) (Ordinal.Int (Ordinal.count x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_1634| … expansions
• unroll
 expr (|count_ty_0 list_1634| (|get.::.1_1615| x_1623)) expansions
• unroll
 expr (|count_ty_0 list_1634| x_1623) expansions
• ##### unsat
(let ((a!1 (= (|count_ty_0 list_1634| x_1623)
(+ 1 (|count_ty_0 list_1634| (|get.:…

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 :
verify (fun x y ->
List.length @@ interleave_strict x y <= List.length x + List.length y)

Out:
- : '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 []
&& φ [] x && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x).

3 nontautological subgoals.

Subgoal 3:

|---------------------------------------------------------------------------
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:

|---------------------------------------------------------------------------
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. x <> []
H1. y <> []
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. x <> []
H1. y <> []
H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
(List.length (List.tl x) + List.length (List.tl y))
|---------------------------------------------------------------------------
List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <=
((1 + List.length (List.tl x)) + List.length (List.tl y))

But simplification reduces this to true, using the definition of List.length.

ⓘ  Rules:
(:def List.length)
(:def interleave_strict)
(:fc List.len_nonnegative)
(:induct struct list)


Proved
proof
 ground_instances 0 definitions 11 inductions 1 search_time 0.145s
Expand
• start[0.145s, "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.145s, "1"]
List.length (interleave_strict x y) <= (List.length x + List.length y)
• induction on (structural+ x, y)
:scheme φ y []
&& φ [] x
&& (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x)
• Split ((List.length (interleave_strict [] y) <=
(List.length [] + List.length y)
&& List.length (interleave_strict x []) <=
(List.length x + List.length []))
&& (not
((x <> [] && y <> [])
&& 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))
:cases [List.length (interleave_strict [] y) <=
(List.length [] + List.length y);
List.length (interleave_strict x []) <=
(List.length x + List.length []);
((not (x <> []) || not (y <> []))
|| not
(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)])
• ##### subproof
((not (x <> []) || not (y <> [])) || not (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)
• start[0.144s, "1"]
((not (x <> []) || not (y <> []))
|| not
(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)
• ###### simplify
 into ((not (x <> []) || not (y <> [])) || not (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)) expansions [List.length, List.length, List.length, interleave_strict] rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ###### simplify
 into true expansions List.length rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
List.length (interleave_strict x []) <= (List.length x + List.length [])
• start[0.144s, "2"]
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_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
List.length (interleave_strict [] y) <= (List.length [] + List.length y)
• start[0.144s, "3"]
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_nonnegativeList.len_nonnegativeList.len_nonnegative
In :
verify (fun x y ->
List.length @@ interleave_strict x y <= List.length x + List.length y)
[@@induct structural_mult (x,y)]

Out:
- : '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 <> [] && φ [] (List.tl x) ==> φ [] x)
&& (y <> [] && φ (List.tl y) [] ==> φ y [])
&& (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x).

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. 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 2:

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 1:

H0. x <> []
H1. y <> []
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. x <> []
H1. y <> []
H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
(List.length (List.tl x) + List.length (List.tl y))
|---------------------------------------------------------------------------
List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <=
((1 + List.length (List.tl x)) + List.length (List.tl y))

But simplification reduces this to true, using the definition of List.length.

ⓘ  Rules:
(:def List.length)
(:def interleave_strict)
(:fc List.len_nonnegative)
(:induct struct list)


Proved
proof
 ground_instances 0 definitions 16 inductions 1 search_time 0.114s
Expand
• start[0.114s, "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.114s, "1"]
List.length (interleave_strict x y) <= (List.length x + List.length y)
• induction on (structural* x, y)
:scheme φ [] []
&& (x <> [] && φ [] (List.tl x) ==> φ [] x)
&& (y <> [] && φ (List.tl y) [] ==> φ y [])
&& (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x)
• Split (((List.length (interleave_strict [] []) <= (2 * List.length [])
&& (not
(x <> []
&& List.length (interleave_strict (List.tl x) []) <=
(List.length (List.tl x) + List.length []))
|| List.length (interleave_strict x []) <=
(List.length x + List.length [])))
&& (not
(y <> []
&& List.length (interleave_strict [] (List.tl y)) <=
(List.length [] + List.length (List.tl y)))
|| List.length (interleave_strict [] y) <=
(List.length [] + List.length y)))
&& (not
((x <> [] && y <> [])
&& List.length (interleave_strict (List.tl x) (List.tl y)) <=
(List.length (List.tl x) + List.length (List.tl y)))
|| List.length … <= …)
:cases [List.length (interleave_strict [] []) <= (2 * List.length []);
(not (x <> [])
|| not
(List.length (interleave_strict (List.tl x) []) <=
(List.length (List.tl x) + List.length [])))
|| List.length (interleave_strict x []) <=
(List.length x + List.length []);
(not (y <> [])
|| not
(List.length (interleave_strict [] (List.tl y)) <=
(List.length [] + List.length (List.tl y))))
|| List.length (interleave_strict [] y) <=
(List.length [] + List.length y);
((not (x <> []) || not (y <> []))
|| not
(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)])
• ##### subproof
((not (x <> []) || not (y <> [])) || not (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)
• start[0.113s, "1"]
((not (x <> []) || not (y <> []))
|| not
(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)
• ###### simplify
 into ((not (x <> []) || not (y <> [])) || not (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)) expansions [List.length, List.length, List.length, interleave_strict] rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ###### simplify
 into true expansions List.length rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
(not (y <> []) || not (List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y)
• start[0.113s, "2"]
(not (y <> [])
|| not
(List.length (interleave_strict [] (List.tl y)) <=
(List.length [] + List.length (List.tl y))))
|| List.length (interleave_strict [] y) <= (List.length [] + List.length y)
• ###### simplify
 into true expansions [List.length, List.length, List.length, interleave_strict] rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
(not (x <> []) || not (List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []))) || List.length (interleave_strict x []) <= (List.length x + List.length [])
• start[0.113s, "3"]
(not (x <> [])
|| not
(List.length (interleave_strict (List.tl x) []) <=
(List.length (List.tl x) + List.length [])))
|| List.length (interleave_strict x []) <= (List.length x + List.length [])
• ###### simplify
 into true expansions [List.length, List.length, List.length, interleave_strict] rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
List.length (interleave_strict [] []) <= (2 * List.length [])
• start[0.113s, "4"]
List.length (interleave_strict [] []) <= (2 * List.length [])
• ###### simplify
 into true expansions [List.length, List.length, interleave_strict] rewrite_steps forward_chaining List.len_nonnegativeList.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.