# Using Imandra Discover¶

Imandra Discover is a tool for theory exploration and producing conjectures. Sometimes, it is not entirely clear what lemmas are necessary for a proof to succeed, or what the properties of a program are. Discover intends to help with this problem, giving the user potential properties to be proved and themselves used as lemmas.

## Balanced Binary Trees¶

In this example, we will define a type of binary trees, and a function that creates a balanced binary tree of a given number of nodes. Balanced binary trees are trees where the subtrees to the left and right of the root have either the same number of nodes, or differ by one. We will then demonstrate how to use Discover for the discovery of properties of these functions.

# Demonstration¶

You may need to #require the Discover bridge. This may not be necessary if you are using Try Imandra or Imandra through a Docker image. The command is commented out here for reference so that you can easily use it if needed.

In [1]:
(* #require "imandra-discover-bridge";; *)

Out[1]:

This function loads some other things necessary for Discover to run, including the Imandra rand_gen plugin.

In [2]:
Imandra_discover_bridge.Top.init ();;

Out[2]:
- : unit = ()


It is common to restrict induction used by Imandra using #max_induct.

In [3]:
#max_induct 1;;

Out[3]:

This is our type of binary trees. The content of the binary trees is immaterial.

Keep in mind that Discover instantiates polymorphic types with int. This means that if this was a polymorphic binary tree whose values were of 'a, Discover would replace the type variable 'a with int. If Discover gives you unexpected output or seems to lack things that it should have, take a look at the signature used by Discover. You can specify the types of your functions to prevent this.

In [4]:
type bt = | Empty
| Branch of
{value : int;
left : bt;
right : bt;};;

Out[4]:
type bt = Empty | Branch of { value : Z.t; left : bt; right : bt; }
val pp_bt : bt Fmt.printer = <fun>
val string_of_bt : bt -> string = <fun>
val rand_bound_bt : Z.t -> Gen_rand_Random.t -> bt = <fun>
val rand_bt : Gen_rand_Random.t -> bt = <fun>


Let's define some functions that we will use in the construction of balanced binary trees.

In [5]:
let lhs_split n = n/2;;
let rhs_split n = n - lhs_split n;;

Out[5]:
val lhs_split : Z.t -> Z.t = <fun>
val rhs_split : Z.t -> Z.t = <fun>


What are some properties that hold of these functions? We should ask Discover to suggest some things. We invoke Discover with the events database db and pass it a list of the string function names we would like Discover to investigate.

In [6]:
discover db ~iterations:2i ["+";"lhs_split";"rhs_split"];;

Out[6]:
Making dfuns...
Finding function names...
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: +, type: int -> int -> int, [Int x0; Int x1], Int (( + ) x0 x1)
Done making type definitions for Discover.
Finding function names...
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: lhs_split, type: int -> int, [Int x0], Int (( lhs_split ) x0)
Done making type definitions for Discover.
Finding function names...
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: rhs_split, type: int -> int, [Int x0], Int (( rhs_split ) x0)
Done making type definitions for Discover.
Making dfuns_ty...
Making present types...
Making present types string...
Making dummy types...
Making signature string...
Making discover constant...
type discover_int = Z.t
val pp_discover_int : discover_int Fmt.printer = <fun>
val string_of_discover_int : discover_int -> string = <fun>
val rand_bound_discover_int :
discover_int -> Gen_rand_Random.t -> discover_int = <fun>
val rand_discover_int : Gen_rand_Random.t -> discover_int = <fun>
type discover_type = Int of discover_int
val pp_discover_type : discover_type Fmt.printer = <fun>
val string_of_discover_type : discover_type -> string = <fun>
val rand_bound_discover_type :
discover_int -> Gen_rand_Random.t -> discover_type = <fun>
val rand_discover_type : Gen_rand_Random.t -> discover_type = <fun>
Making discover evaluator...
Making random generator...
Making sprint...
Making defaults string...
Making defaults...
Making condition and condition types string...
val condition : 'a -> bool = <fun>
Making Discover instances of type...
val discover_instances : 'a list = []
Making random condition string...
let condition _cl = true
let condition_types = []
Making random condition with types...
Making options...
val discover_rand_t : string -> discover_type = <fun>
val eval : string -> discover_type list -> discover_type = <fun>
- : discover_type -> string = <fun>
val signature : (string * string) list =
[("+", "int->int->int");("lhs_split", "int->int");("rhs_split", "int->int")]
val condition_types : 'a list = []
val condition_rand : unit -> discover_type list = <fun>
val condition_rand_with_ty : (string * discover_type) list = []
val default_l : (string * discover_type) list = [("int", Int -2)]
val default : string -> discover_type = <fun>
val packed_discover_module :
(module Imandra_discover_lib.Module.Discover_module) = <module>
module CurrentProblem : Imandra_discover_lib.Module.Discover_module
Making new variable x0 of type int
Making new variable x1 of type int
Making new variable x2 of type int
Making new variable x3 of type int
(lhs_split (x0 + x0)) = x0
(rhs_split (x0 + x0)) = x0
((lhs_split x0) + (rhs_split x0)) = x0
(x1 + x0) = (x0 + x1)
(x1 + (x0 + x2)) = (x0 + (x1 + x2))
((x0 + x1) + x2) = (x0 + (x1 + x2))
val discover_result : string list =
["fun x0 -> (lhs_split (x0 + x0)) = x0";
"fun x0 -> (rhs_split (x0 + x0)) = x0";
"fun x0 -> ((lhs_split x0) + (rhs_split x0)) = x0";
"fun x0 x1 -> (x1 + x0) = (x0 + x1)";
"fun x0 x1 x2 -> (x1 + (x0 + x2)) = (x0 + (x1 + x2))";
"fun x0 x1 x2 -> ((x0 + x1) + x2) = (x0 + (x1 + x2))"]
These are the conjectures found by Discover.
discover_result contains the conjectures before filtering.
discover_result_simplified contains the conjectures after simplification by Imandra.
val discover_result_simplified : string list = []
- : Top_result.t list = []


Discover finishes after running for a few seconds and gives us some conjectures we could try to prove. One of them states that the sum of the lhs_split and rhs_split of some x0 is equal to x0. Great, we can ask Imandra to prove it for us.

In [7]:
lemma discover__2 x0 = ((lhs_split x0) + (rhs_split x0)) = x0 [@@rewrite]  [@@auto];;

Out[7]:
val discover__2 : discover_int -> bool = <fun>
Goal:

lhs_split x0 + rhs_split x0 = x0.

1 tautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
true

But this is obviously true.


Proved
proof
 ground_instances: 0 definitions: 0 inductions: 0 search_time: 0.000s
Expand
• start[0.000s, "Goal"]
let (_x_0 : int) = ( :var_0: ) / 2 in
_x_0 + ( :var_0: ) - _x_0 = ( :var_0: )
• #### subproof

true
• start[0.000s, "1"] true
• ##### simplify
 into: true expansions: [] rewrite_steps: forward_chaining:

#### Warning

Pattern will match only if lhs_split is disabled
(non-recursive function)
See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

#### Warning

Pattern will match only if rhs_split is disabled
(non-recursive function)
See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

Now, we will make a function that should return a balanced binary tree with n nodes, given n.

In [8]:
let rec cbal n =
if n < 0 then Empty else
match n with
| 0 -> Empty
| 1 -> Branch {value=1; left = Empty; right = Empty}
| _ -> let left_split = lhs_split (n-1) in
let right_split = rhs_split (n-1) in
let left = cbal left_split in
let right = cbal right_split in
Branch {value=1; left; right};;

Out[8]:
val cbal : discover_int -> bt = <fun>

termination proof

### Termination proof

call cbal (lhs_split (n - 1)) from cbal n
original:cbal n
sub:cbal (lhs_split (n - 1))
original ordinal:Ordinal.Int (_cnt n)
sub ordinal:Ordinal.Int (_cnt (lhs_split (n - 1)))
path:[not (1 = n) && not (0 = n) && not (n < 0)]
proof:
detailed proof
ground_instances:1
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 3 arith assert lower: 10 arith tableau max rows: 4 arith tableau max columns: 11 arith pivots: 1 rlimit count: 3090 mk clause: 11 datatype occurs check: 2 mk bool var: 23 arith assert upper: 3 arith row summations: 4 propagations: 5 conflicts: 2 arith fixed eqs: 1 datatype accessor ax: 2 arith conflicts: 1 arith num rows: 4 arith assert diseq: 6 num allocs: 2.67276e+06 final checks: 1 added eqs: 9 del clause: 11 arith eq adapter: 5 memory: 5.51 max memory: 5.51
Expand
• start[0.009s]
let (_x_0 : int) = if n >= 0 then n else 0 in
let (_x_1 : int) = (n - 1) / 2 in
let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
let (_x_3 : bool)
= not (not (1 = _x_1) && not (0 = _x_1) && not (_x_1 < 0))
in
not (1 = n) && not (0 = n) && not (n < 0) && _x_0 >= 0 && _x_2 >= 0
==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int) = ((-1) + n) / 2 in (not ((not (1 = _x_0) && not (0 = _x_0)) && 0 <= _x_0) || Ordinal.( << ) (Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)) (Ordinal.Int (if n >= 0 then n else 0))) || not ((not (1 = n) && not (0 = n)) && 0 <= n) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (ite (>= (div (+ (- 1) n_1651/server) 2) 0) (div (+ (- 1) n_1651/server) … expansions:
• Unsat
call cbal (rhs_split (n - 1)) from cbal n
original:cbal n
sub:cbal (rhs_split (n - 1))
original ordinal:Ordinal.Int (_cnt n)
sub ordinal:Ordinal.Int (_cnt (rhs_split (n - 1)))
path:[not (1 = n) && not (0 = n) && not (n < 0)]
proof:
detailed proof
ground_instances:1
definitions:0
inductions:0
search_time:
0.011s
details:
Expand
smt_stats:
 num checks: 3 arith assert lower: 10 arith tableau max rows: 5 arith tableau max columns: 12 arith pivots: 3 rlimit count: 1686 mk clause: 16 datatype occurs check: 2 mk bool var: 23 arith assert upper: 3 arith row summations: 9 propagations: 6 conflicts: 2 arith fixed eqs: 1 datatype accessor ax: 2 arith conflicts: 1 arith num rows: 5 arith assert diseq: 4 num allocs: 796503 final checks: 1 added eqs: 9 del clause: 16 arith eq adapter: 5 memory: 5.48 max memory: 5.48
Expand
• start[0.011s]
let (_x_0 : int) = if n >= 0 then n else 0 in
let (_x_1 : int) = n - 1 in
let (_x_2 : int) = _x_1 - (_x_1 / 2) in
let (_x_3 : int) = if _x_2 >= 0 then _x_2 else 0 in
let (_x_4 : bool)
= not (not (1 = _x_2) && not (0 = _x_2) && not (_x_2 < 0))
in
not (1 = n) && not (0 = n) && not (n < 0) && _x_0 >= 0 && _x_3 >= 0
==> _x_4 && _x_4 || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int) = (-1) + n in let (_x_1 : int) = (-1) * _x_0 / 2 in let (_x_2 : int) = n + _x_1 in (not ((not (2 = _x_2) && not (1 = _x_2)) && 1 <= _x_2) || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 1 then _x_0 + _x_1 else 0)) (Ordinal.Int (if n >= 0 then n else 0))) || not ((not (1 = n) && not (0 = n)) && 0 <= n) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (+ n_1651/server (* (- 1) (div (+ (- 1) n_1651/server) 2)))) (a!2 (+ (- 1) n_1651/s… expansions:
• Unsat

This is simply the size of the tree.

In [9]:
let rec nodes tree =
match tree with
| Empty -> 0
| Branch {left; right; _} -> 1 + (nodes left) + (nodes right);;

Out[9]:
val nodes : bt -> discover_int = <fun>

termination proof

### Termination proof

call nodes (Destruct(Branch, 1, tree)) from nodes tree
original:nodes tree
sub:nodes (Destruct(Branch, 1, tree))
original ordinal:Ordinal.Int (_cnt tree)
sub ordinal:Ordinal.Int (_cnt (Destruct(Branch, 1, tree)))
path:[not Is_a(Empty, tree)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 22 arith tableau max rows: 6 arith tableau max columns: 21 arith pivots: 17 rlimit count: 9290 mk clause: 28 datatype occurs check: 22 mk bool var: 86 arith gcd tests: 4 arith assert upper: 20 datatype splits: 3 decisions: 20 arith row summations: 28 arith branch var: 1 propagations: 20 arith patches: 1 conflicts: 9 arith fixed eqs: 8 datatype accessor ax: 7 minimized lits: 1 arith conflicts: 4 arith num rows: 6 arith assert diseq: 1 datatype constructor ax: 11 num allocs: 9.48286e+06 final checks: 5 added eqs: 55 del clause: 19 arith ineq splits: 1 arith eq adapter: 15 memory: 5.6 max memory: 5.6
Expand
• start[0.010s]
let (_x_0 : int) = count.bt tree in
let (_x_1 : bt) = Destruct(Branch, 1, tree) in
let (_x_2 : int) = count.bt _x_1 in
let (_x_3 : bool) = Is_a(Empty, _x_1) in
not Is_a(Empty, tree) && _x_0 >= 0 && _x_2 >= 0
==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : bt) = Destruct(Branch, 1, tree) in let (_x_1 : int) = count.bt tree in let (_x_2 : int) = count.bt _x_0 in (Is_a(Empty, _x_0) || not ((not Is_a(Empty, tree) && _x_1 >= 0) && _x_2 >= 0)) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_1) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<_129/client| (|Ordinal.Int_114/client| (|count.bt_1351/client| (|get.Branch.left_1… expansions:
• unroll
 expr: (|count.bt_1351/client| (|get.Branch.left_1649/server| tree_1720/server)) expansions:
• unroll
 expr: (|count.bt_1351/client| tree_1720/server) expansions:
• Unsat
call nodes (Destruct(Branch, 2, tree)) from nodes tree
original:nodes tree
sub:nodes (Destruct(Branch, 2, tree))
original ordinal:Ordinal.Int (_cnt tree)
sub ordinal:Ordinal.Int (_cnt (Destruct(Branch, 2, tree)))
path:[not Is_a(Empty, tree)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 22 arith tableau max rows: 6 arith tableau max columns: 21 arith pivots: 17 rlimit count: 6167 mk clause: 28 datatype occurs check: 18 mk bool var: 86 arith gcd tests: 4 arith assert upper: 20 datatype splits: 3 decisions: 20 arith row summations: 28 arith branch var: 1 propagations: 20 arith patches: 1 conflicts: 9 arith fixed eqs: 8 datatype accessor ax: 7 minimized lits: 1 arith conflicts: 4 arith num rows: 6 arith assert diseq: 1 datatype constructor ax: 11 num allocs: 5.59133e+06 final checks: 5 added eqs: 55 del clause: 19 arith ineq splits: 1 arith eq adapter: 15 memory: 5.57 max memory: 5.57
Expand
• start[0.010s]
let (_x_0 : int) = count.bt tree in
let (_x_1 : bt) = Destruct(Branch, 2, tree) in
let (_x_2 : int) = count.bt _x_1 in
let (_x_3 : bool) = Is_a(Empty, _x_1) in
not Is_a(Empty, tree) && _x_0 >= 0 && _x_2 >= 0
==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int) = count.bt tree in let (_x_1 : bt) = Destruct(Branch, 2, tree) in let (_x_2 : int) = count.bt _x_1 in (not ((not Is_a(Empty, tree) && _x_0 >= 0) && _x_2 >= 0) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)) || Is_a(Empty, _x_1) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<_129/client| (|Ordinal.Int_114/client| (|count.bt_1351/client| (|get.Branch.right_… expansions:
• unroll
 expr: (|count.bt_1351/client| (|get.Branch.right_1650/server| tree_1720/server)) expansions:
• unroll
 expr: (|count.bt_1351/client| tree_1720/server) expansions:
• Unsat

In our function cbal, we always return Empty if n < 0. This suggests that we will want to have a predicate capturing the interesting case where the input to cbal is nonnegative, and a predicate for the zero or negative case.

In [10]:
let nonnegative x = x >= 0;;
let leq_zero x = x <= 0;;

Out[10]:
val nonnegative : discover_int -> bool = <fun>
val leq_zero : discover_int -> bool = <fun>


Now that we have the functions nodes and cbal, we should ask Discover to find some properties that may hold. Since cbal is only really interesting if the input is nonnegative, we invoke Discover with the labeled argument ~condition set to the string literal "nonnegative". This string argument lets Discover know to always instantiate a fixed variable with values satisfying the predicate we just defined. We specify nodes and cbal for investigation.

In [11]:
discover db ~condition:"nonnegative" ["nodes";"cbal"];;

Out[11]:
Making dfuns...
Finding function names...
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: nodes, type: bt -> int, [Bt x0], Int (( nodes ) x0)
Done making type definitions for Discover.
Finding function names...
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: cbal, type: int -> bt, [Int x0], Bt (( cbal ) x0)
Done making type definitions for Discover.
Making dfuns_ty...
Making present types...
Making present types string...
Making dummy types...
Making signature string...
Making discover constant...
type discover_bt = bt
val pp_discover_bt : discover_bt Fmt.printer = <fun>
val string_of_discover_bt : discover_bt -> string = <fun>
val rand_bound_discover_bt : discover_int -> Gen_rand_Random.t -> discover_bt =
<fun>
val rand_discover_bt : Gen_rand_Random.t -> discover_bt = <fun>
type discover_int = discover_int
val pp_discover_int_1 : discover_int Fmt.printer = <fun>
val string_of_discover_int : discover_int -> string = <fun>
val rand_bound_discover_int_1 :
discover_int -> Gen_rand_Random.t -> discover_int = <fun>
val rand_discover_int_1 : Gen_rand_Random.t -> discover_int = <fun>
type discover_type = Bt of discover_bt | Int of discover_int
val pp_discover_type_1 : discover_type Fmt.printer = <fun>
val string_of_discover_type : discover_type -> string = <fun>
val rand_bound_discover_type_1 :
discover_int -> Gen_rand_Random.t -> discover_type = <fun>
val rand_discover_type_1 : Gen_rand_Random.t -> discover_type = <fun>
Making discover evaluator...
Making random generator...
Making sprint...
Making defaults string...
Making defaults...
Making condition and condition types string...
create_cond_constructors: name: nonnegative, type: int -> bool, [Int x0], (( nonnegative ) x0)
val condition : discover_type list -> bool = <fun>
Making Discover instances of type...
Int
Making instances satisfying the condition with Imandra...
val n_models_diff_f :
('a -> discover_int) -> ('a -> bool) -> 'a list -> discover_int -> bool =
<fun>
- : discover_type list list -> (discover_type list -> discover_int) -> bool =
<fun>
module CX :
sig
val f : discover_type list -> discover_int
val discover_instances : discover_type list list
end
val discover_instances : 'a list = []
- : unit = ()
Making random condition string...
let condition cl : bool =
match cl with
| [Int x0] -> (( nonnegative ) x0)
| _ -> false
let condition_types =
[
"int";
]
Making random condition with types...
Making options...
val discover_rand_t : string -> discover_type = <fun>
val eval : string -> discover_type list -> discover_type = <fun>
- : discover_type -> string = <fun>
val signature : (string * string) list =
[("nodes", "bt->int");("cbal", "int->bt")]
val condition_types : string list = ["int"]
val condition_rand : unit -> discover_type list = <fun>
val condition_rand_with_ty : (string * discover_type) list = [("int", Int 7)]
val default_l : (string * discover_type) list =
[("bt",
Bt
(Branch
{value = 31;
left =
Branch
{value = -33;
left = Branch {value = -36; left = Empty; right = Empty};
right = Empty};
right = Empty}));("int", Int -1)]
val default : string -> discover_type = <fun>
val packed_discover_module :
(module Imandra_discover_lib.Module.Discover_module) = <module>
module CurrentProblem : Imandra_discover_lib.Module.Discover_module
Making new variable x0 of type int
Making new variable x1 of type int
Making new variable x2 of type bt
Making new variable x3 of type int
Making new variable x4 of type bt
Making new variable x5 of type int
Making new variable x6 of type bt
(nodes (cbal x0)) = x0
val discover_result : string list =
["fun x0 -> (nonnegative x0) ==> (nodes (cbal x0)) = x0"]
These are the conjectures found by Discover.
discover_result contains the conjectures before filtering.
discover_result_simplified contains the conjectures after simplification by Imandra.
val discover_result_simplified : string list =
["not (x0 >= 0) || nodes (cbal x0) = x0"]
- : Top_result.t list = []


Great, Discover suggests that the balanced binary trees produced by cbal have the correct number of nodes! It's often helpful to tweak the lemmas suggested by Discover. In this case we'll replace the predicate condition with its body. Let's have Imandra prove it.

In [12]:
lemma discover__0 x0 = x0 >= 0 ==> (nodes (cbal x0)) = x0   [@@auto];;

Out[12]:
val discover__0 : discover_int -> bool = <fun>
Goal:

x0 >= 0 ==> nodes (cbal x0) = x0.

1 nontautological subgoal.

Subgoal 1:

H0. x0 >= 0
|---------------------------------------------------------------------------
nodes (cbal x0) = x0

Must try induction.

We shall induct according to a scheme derived from cbal.

Induction scheme:

(not (not (1 = x0) && not (0 = x0) && not (x0 < 0)) ==> φ x0)
&& (not (x0 < 0)
&& not (0 = x0)
&& not (1 = x0) && φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1))
==> φ x0).

2 nontautological subgoals.

Subgoal 1.2:

H0. x0 >= 0
|---------------------------------------------------------------------------
C0. (not (1 = x0) && not (0 = x0)) && 0 <= x0
C1. nodes (cbal x0) = x0

But simplification reduces this to true, using the definitions of cbal and
nodes.

Subgoal 1.1:

H0. x0 >= 0
H1. 0 <= x0
H2. not (0 = x0)
H3. not (1 = x0)
H4. (x0 + (-1) * ((-1) + x0) / 2) >= 1
==> nodes (cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)) =
(-1) + x0 + (-1) * ((-1) + x0) / 2
H5. (((-1) + x0) / 2) >= 0
==> nodes (cbal (((-1) + x0) / 2)) = ((-1) + x0) / 2
|---------------------------------------------------------------------------
nodes (cbal x0) = x0

But simplification reduces this to true, using the definitions of cbal and
nodes.

ⓘ  Rules:
(:def cbal)
(:def nodes)
(:induct cbal)


Proved
proof
 ground_instances: 0 definitions: 6 inductions: 1 search_time: 0.147s
Expand
• start[0.147s, "Goal"]
( :var_0: ) >= 0 ==> nodes (cbal ( :var_0: )) = ( :var_0: )
• #### subproof

not (x0 >= 0) || nodes (cbal x0) = x0
• start[0.147s, "1"] not (x0 >= 0) || nodes (cbal x0) = x0
• induction on (functional ?)
:scheme (not (not (1 = x0) && not (0 = x0) && not (x0 < 0)) ==> φ x0)
&& (not (x0 < 0)
&& not (0 = x0)
&& not (1 = x0)
&& φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1))
==> φ x0)
• Split (let (_x_0 : bool) = not (1 = x0) in
let (_x_1 : bool) = not (0 = x0) in
let (_x_2 : bool) = 0 <= x0 in
let (_x_3 : bool) = nodes (cbal x0) = x0 in
let (_x_4 : bool) = not (x0 >= 0) in
let (_x_5 : int) = (-1) + x0 in
let (_x_6 : int) = _x_5 / 2 in
let (_x_7 : int) = (-1) * _x_6 in
let (_x_8 : int) = _x_5 + _x_7 in
(((_x_0 && _x_1) && _x_2 || _x_3) || _x_4)
&& ((_x_3 || _x_4)
|| not
((((_x_2 && _x_1) && _x_0)
&& (not ((x0 + _x_7) >= 1) || nodes (cbal _x_8) = _x_8))
&& (not (_x_6 >= 0) || nodes (cbal _x_6) = _x_6)))
:cases [(not (x0 >= 0) || (not (1 = x0) && not (0 = x0)) && 0 <= x0)
|| nodes (cbal x0) = x0;
let (_x_0 : int) = (-1) + x0 in
let (_x_1 : int) = _x_0 / 2 in
let (_x_2 : int) = (-1) * _x_1 in
let (_x_3 : int) = _x_0 + _x_2 in
(((((not (x0 >= 0) || not (0 <= x0)) || 0 = x0) || 1 = x0)
|| not ((x0 + _x_2) >= 1 ==> nodes (cbal _x_3) = _x_3))
|| not (_x_1 >= 0 ==> nodes (cbal _x_1) = _x_1))
|| nodes (cbal x0) = x0])
• ##### subproof
let (_x_0 : int) = (-1) + x0 in let (_x_1 : int) = _x_0 / 2 in let (_x_2 : int) = (-1) * _x_1 in let (_x_3 : int) = _x_0 + _x_2 in (((((not (x0 >= 0) || not (0 <= x0)) || 0 = x0) || 1 = x0) || not ((x0 + _x_2) >= 1 ==> nodes (cbal _x_3) = _x_3)) || not (_x_1 >= 0 ==> nodes (cbal _x_1) = _x_1)) || nodes (cbal x0) = x0
• start[0.086s, "1.1"]
let (_x_0 : int) = (-1) + x0 in
let (_x_1 : int) = _x_0 / 2 in
let (_x_2 : int) = (-1) * _x_1 in
let (_x_3 : int) = _x_0 + _x_2 in
(((((not (x0 >= 0) || not (0 <= x0)) || 0 = x0) || 1 = x0)
|| not ((x0 + _x_2) >= 1 ==> nodes (cbal _x_3) = _x_3))
|| not (_x_1 >= 0 ==> nodes (cbal _x_1) = _x_1))
|| nodes (cbal x0) = x0
• ###### simplify
 into: true expansions: [nodes, cbal] rewrite_steps: forward_chaining:
• ##### subproof
(not (x0 >= 0) || (not (1 = x0) && not (0 = x0)) && 0 <= x0) || nodes (cbal x0) = x0
• start[0.086s, "1.2"]
(not (x0 >= 0) || (not (1 = x0) && not (0 = x0)) && 0 <= x0)
|| nodes (cbal x0) = x0
• ###### simplify
 into: true expansions: [nodes, nodes, nodes, cbal] rewrite_steps: forward_chaining:

What about the zero or negative case?

In [13]:
discover db ~condition:"leq_zero" ["nodes";"cbal";"Empty"];;

Out[13]:
Making dfuns...
Finding function names...
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: nodes, type: bt -> int, [Bt x0], Int (( nodes ) x0)
Done making type definitions for Discover.
Finding function names...
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: cbal, type: int -> bt, [Int x0], Bt (( cbal ) x0)
Done making type definitions for Discover.
Finding function names...
val dummy_Empty : discover_bt = Empty
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: Empty, type: bt, [], Bt (( Empty ) )
Done making type definitions for Discover.
Making dfuns_ty...
Making present types...
Making present types string...
Making dummy types...
Making signature string...
Making discover constant...
type discover_bt = discover_bt
val pp_discover_bt_1 : discover_bt Fmt.printer = <fun>
val string_of_discover_bt : discover_bt -> string = <fun>
val rand_bound_discover_bt_1 :
discover_int -> Gen_rand_Random.t -> discover_bt = <fun>
val rand_discover_bt_1 : Gen_rand_Random.t -> discover_bt = <fun>
type discover_int = discover_int
val pp_discover_int_2 : discover_int Fmt.printer = <fun>
val string_of_discover_int : discover_int -> string = <fun>
val rand_bound_discover_int_2 :
discover_int -> Gen_rand_Random.t -> discover_int = <fun>
val rand_discover_int_2 : Gen_rand_Random.t -> discover_int = <fun>
type discover_type = Bt of discover_bt | Int of discover_int
val pp_discover_type_2 : discover_type Fmt.printer = <fun>
val string_of_discover_type : discover_type -> string = <fun>
val rand_bound_discover_type_2 :
discover_int -> Gen_rand_Random.t -> discover_type = <fun>
val rand_discover_type_2 : Gen_rand_Random.t -> discover_type = <fun>
Making discover evaluator...
Making random generator...
Making sprint...
Making defaults string...
Making defaults...
Making condition and condition types string...
create_cond_constructors: name: leq_zero, type: int -> bool, [Int x0], (( leq_zero ) x0)
val condition : discover_type list -> bool = <fun>
Making Discover instances of type...
Int
Making instances satisfying the condition with Imandra...
val n_models_diff_f :
('a -> discover_int) -> ('a -> bool) -> 'a list -> discover_int -> bool =
<fun>
- : discover_type list list -> (discover_type list -> discover_int) -> bool =
<fun>
module CX :
sig
val f : discover_type list -> discover_int
val discover_instances : discover_type list list
end
val discover_instances : 'a list = []
- : unit = ()
Making random condition string...
let condition cl : bool =
match cl with
| [Int x0] -> (( leq_zero ) x0)
| _ -> false
let condition_types =
[
"int";
]
Making random condition with types...
Making options...
val discover_rand_t : string -> discover_type = <fun>
val eval : string -> discover_type list -> discover_type = <fun>
- : discover_type -> string = <fun>
val signature : (string * string) list =
[("Empty", "bt");("nodes", "bt->int");("cbal", "int->bt")]
val condition_types : string list = ["int"]
val condition_rand : unit -> discover_type list = <fun>
val condition_rand_with_ty : (string * discover_type) list =
[("int", Int -3)]
val default_l : (string * discover_type) list =
[("bt", Bt (Branch {value = 23; left = Empty; right = Empty}));
("int", Int -3)]
val default : string -> discover_type = <fun>
val packed_discover_module :
(module Imandra_discover_lib.Module.Discover_module) = <module>
module CurrentProblem : Imandra_discover_lib.Module.Discover_module
Making new variable x0 of type int
Making new variable x1 of type int
Making new variable x2 of type bt
Making new variable x3 of type int
Making new variable x4 of type bt
Making new variable x5 of type int
Making new variable x6 of type bt
(cbal x0) = Empty
val discover_result : string list =
["fun x0 -> (leq_zero x0) ==> (cbal x0) = Empty"]
These are the conjectures found by Discover.
discover_result contains the conjectures before filtering.
discover_result_simplified contains the conjectures after simplification by Imandra.
val discover_result_simplified : string list =
["not (x0 <= 0) || cbal x0 = Empty"]
- : Top_result.t list = []


Discover suggests exactly what cbal does in the less than or equal to zero case, so we can have Imandra prove this as well.

In [14]:
lemma discover__0_neg x0 = x0 <= 0 ==> (cbal x0) = Empty [@@auto];;

Out[14]:
val discover__0_neg : discover_int -> bool = <fun>
Goal:

x0 <= 0 ==> cbal x0 = Empty.

1 nontautological subgoal.

Subgoal 1:

H0. x0 <= 0
|---------------------------------------------------------------------------
cbal x0 = Empty

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

ⓘ  Rules:
(:def cbal)


Proved
proof
 ground_instances: 0 definitions: 1 inductions: 0 search_time: 0.012s
Expand
• start[0.012s, "Goal"] ( :var_0: ) <= 0 ==> cbal ( :var_0: ) = Empty
• #### subproof

not (x0 <= 0) || cbal x0 = Empty
• start[0.012s, "1"] not (x0 <= 0) || cbal x0 = Empty
• ##### simplify
 into: true expansions: cbal rewrite_steps: forward_chaining:

We were interested in verifying that the trees produced by cbal are actually balanced, so here is a predicate capturing that idea.

In [15]:
let is_balanced tree =
match tree with
| Empty -> true
| Branch {left; right; _} ->
let lnodes = nodes left in
let rnodes = nodes right in
rnodes = lnodes || rnodes - lnodes = 1;;

Out[15]:
val is_balanced : discover_bt -> bool = <fun>


Now we can ask Discover to find a relationship between is_balanced, cbal, and true. We include true so that Discover can suggest predicates as equations. Similarly, you can include false to find things that don't hold.

In [16]:
discover db ["is_balanced";"cbal";"true"];;

Out[16]:
Making dfuns...
Finding function names...
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: is_balanced, type: bt -> bool, [Bt x0], Bool (( is_balanced ) x0)
Done making type definitions for Discover.
Finding function names...
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: cbal, type: int -> bt, [Int x0], Bt (( cbal ) x0)
Done making type definitions for Discover.
Finding function names...
val dummy_true : bool = true
Instantiating polymorphism...
Creating discover type...
Getting definition depth...
Creating constructors...
create_constructors: name: true, type: bool, [], Bool (( true ) )
Done making type definitions for Discover.
Making dfuns_ty...
Making present types...
Making present types string...
Making dummy types...
Making signature string...
Making discover constant...
type discover_bool = bool
val pp_discover_bool : discover_bool Fmt.printer = <fun>
val string_of_discover_bool : discover_bool -> string = <fun>
val rand_bound_discover_bool :
discover_int -> Gen_rand_Random.t -> discover_bool = <fun>
val rand_discover_bool : Gen_rand_Random.t -> discover_bool = <fun>
type discover_bt = discover_bt
val pp_discover_bt_2 : discover_bt Fmt.printer = <fun>
val string_of_discover_bt : discover_bt -> string = <fun>
val rand_bound_discover_bt_2 :
discover_int -> Gen_rand_Random.t -> discover_bt = <fun>
val rand_discover_bt_2 : Gen_rand_Random.t -> discover_bt = <fun>
type discover_int = discover_int
val pp_discover_int_3 : discover_int Fmt.printer = <fun>
val string_of_discover_int : discover_int -> string = <fun>
val rand_bound_discover_int_3 :
discover_int -> Gen_rand_Random.t -> discover_int = <fun>
val rand_discover_int_3 : Gen_rand_Random.t -> discover_int = <fun>
type discover_type =
Bool of discover_bool
| Bt of discover_bt
| Int of discover_int
val pp_discover_type_3 : discover_type Fmt.printer = <fun>
val string_of_discover_type : discover_type -> string = <fun>
val rand_bound_discover_type_3 :
discover_int -> Gen_rand_Random.t -> discover_type = <fun>
val rand_discover_type_3 : Gen_rand_Random.t -> discover_type = <fun>
Making discover evaluator...
Making random generator...
Making sprint...
Making defaults string...
Making defaults...
Making condition and condition types string...
val condition : 'a -> discover_bool = <fun>
Making Discover instances of type...
val discover_instances : 'a list = []
Making random condition string...
let condition _cl = true
let condition_types = []
Making random condition with types...
Making options...
val discover_rand_t : string -> discover_type = <fun>
val eval : string -> discover_type list -> discover_type = <fun>
- : discover_type -> string = <fun>
val signature : (string * string) list =
[("true", "bool");("is_balanced", "bt->bool");("cbal", "int->bt")]
val condition_types : 'a list = []
val condition_rand : unit -> discover_type list = <fun>
val condition_rand_with_ty : (string * discover_type) list = []
val default_l : (string * discover_type) list =
[("bool", Bool false);("bt", Bt Empty);("int", Int 25)]
val default : string -> discover_type = <fun>
val packed_discover_module :
(module Imandra_discover_lib.Module.Discover_module) = <module>
module CurrentProblem : Imandra_discover_lib.Module.Discover_module
Making new variable x0 of type bool
Making new variable x1 of type bt
Making new variable x2 of type bool
Making new variable x3 of type bt
Making new variable x4 of type bool
Making new variable x5 of type bt
Making new variable x6 of type int
(is_balanced (cbal x6)) = true
val discover_result : string list =
["fun x6 -> (is_balanced (cbal x6)) = true"]
These are the conjectures found by Discover.
discover_result contains the conjectures before filtering.
discover_result_simplified contains the conjectures after simplification by Imandra.
val discover_result_simplified : string list =
["let (_x_0 : bt) = cbal x6 in\nlet (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in\nlet (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in\n(Is_a(Empty, _x_0) || _x_1 = _x_2) || _x_1 + (-1) * _x_2 = 1"]
- : Top_result.t list = []


Discover suggests that every tree produced by cbal is balanced. We can prove this too!

In [17]:
lemma discover_cbal_balanced_0 x0 = x0 >= 0 ==> (is_balanced (cbal x0)) [@@auto];;

Out[17]:
val discover_cbal_balanced_0 : discover_int -> discover_bool = <fun>
Goal:

x0 >= 0 ==> is_balanced (cbal x0).

1 nontautological subgoal.

Subgoal 1:

H0. x0 >= 0
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal x0)
C1. nodes (Destruct(Branch, 2, cbal x0)) =
nodes (Destruct(Branch, 1, cbal x0))
C2. nodes (Destruct(Branch, 2, cbal x0))
+ (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1

Must try induction.

We shall induct according to a scheme derived from cbal.

Induction scheme:

(not (not (1 = x0) && not (0 = x0) && not (x0 < 0)) ==> φ x0)
&& (not (x0 < 0)
&& not (0 = x0)
&& not (1 = x0) && φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1))
==> φ x0).

2 nontautological subgoals.

Subgoal 1.2:

H0. x0 >= 0
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 2, cbal x0))
+ (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
C1. Is_a(Empty, cbal x0)
C2. nodes (Destruct(Branch, 2, cbal x0)) =
nodes (Destruct(Branch, 1, cbal x0))
C3. (not (1 = x0) && not (0 = x0)) && 0 <= x0

But simplification reduces this to true, using the definitions of cbal and
nodes.

Subgoal 1.1:

H0. x0 >= 0
H1. 0 <= x0
H2. not (0 = x0)
H3. not (1 = x0)
H4. ((nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
|| nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))))
|| Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
|| not ((x0 + (-1) * ((-1) + x0) / 2) >= 1)
H5. ((Is_a(Empty, cbal (((-1) + x0) / 2)) || not ((((-1) + x0) / 2) >= 0))
|| nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))))
|| nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) =
1
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 2, cbal x0))
+ (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
C1. Is_a(Empty, cbal x0)
C2. nodes (Destruct(Branch, 2, cbal x0)) =
nodes (Destruct(Branch, 1, cbal x0))

This simplifies, using the definitions of cbal and nodes to the following 8
subgoals:

Subgoal 1.1.8:

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C3. 0 = x0
C4. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
=
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C5. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
C6. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

This simplifies to:

Subgoal 1.1.8':

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C2. 0 = x0
C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

But we verify Subgoal 1.1.8' by recursive unrolling.

Subgoal 1.1.7:

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C3. 0 = x0
C4. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
=
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C5. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

This simplifies to:

Subgoal 1.1.7':

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. 0 = x0
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
=
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

Cross-fertilizing with:

nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))

This produces the modified subgoal:

Subgoal 1.1.7'':

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. 0 = x0
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
=
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

This simplifies to:

Subgoal 1.1.7''':

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. 0 = x0
C2. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
C3. 2
* nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
=
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))

But we verify Subgoal 1.1.7''' by recursive unrolling.

Subgoal 1.1.6:

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C2. 0 = x0
C3. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
=
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
C5. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

This simplifies to:

Subgoal 1.1.6':

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. 0 = x0
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
=
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

But we verify Subgoal 1.1.6' by recursive unrolling.

Subgoal 1.1.5:

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C2. 0 = x0
C3. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
=
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C4. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

This simplifies to:

Subgoal 1.1.5':

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C2. 0 = x0
C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

But we verify Subgoal 1.1.5' by recursive unrolling.

Subgoal 1.1.4:

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
H2. Is_a(Empty, cbal (((-1) + x0) / 2))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 0
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= (-1)
C3. 0 = x0
C4. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

This simplifies to:

Subgoal 1.1.4':

H0. x0 >= 0
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
H2. Is_a(Empty, cbal (((-1) + x0) / 2))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 0
C1. 0 = x0
C2. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

But we verify Subgoal 1.1.4' by recursive unrolling.

Subgoal 1.1.3:

H0. x0 >= 0
H1. Is_a(Empty, cbal (((-1) + x0) / 2))
H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 0
C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= (-1)
C2. 0 = x0
C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

This simplifies to:

Subgoal 1.1.3':

H0. x0 >= 0
H1. Is_a(Empty, cbal (((-1) + x0) / 2))
H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= 1
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
= (-1)
C1. 0 = x0
C2. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))

But we verify Subgoal 1.1.3' by recursive unrolling.

Subgoal 1.1.2:

H0. x0 >= 0
H1. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
C2. (-1) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C3. 0 = x0
C4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))

This simplifies to:

Subgoal 1.1.2':

H0. x0 >= 0
H1. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. (-1) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C2. 0 = x0

But we verify Subgoal 1.1.2' by recursive unrolling.

Subgoal 1.1.1:

H0. x0 >= 0
H1. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
C2. (-1) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C3. 0 = x0

This simplifies to:

Subgoal 1.1.1':

H0. x0 >= 0
H1. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. Is_a(Empty, cbal (((-1) + x0) / 2))
C1. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
C2. 0 = x0

But we verify Subgoal 1.1.1' by recursive unrolling.

ⓘ  Rules:
(:def cbal)
(:def nodes)
(:induct cbal)


Proved
proof
ground_instances:36
definitions:20
inductions:1
search_time:
3.489s
details:
Expand
smt_stats:
 num checks: 8 arith-assume-eqs: 1 arith-make-feasible: 31 arith-max-columns: 36 arith-conflicts: 2 rlimit count: 1.0185e+06 arith-gcd-calls: 1 arith-cheap-eqs: 22 mk clause: 217 datatype occurs check: 22 mk bool var: 208 arith-lower: 25 arith-diseq: 39 datatype splits: 9 decisions: 54 arith-propagations: 27 propagations: 172 arith-patches: 1 interface eqs: 1 arith-bound-propagations-cheap: 27 arith-max-rows: 17 conflicts: 15 datatype accessor ax: 7 minimized lits: 4 arith-bound-propagations-lp: 8 datatype constructor ax: 14 final checks: 10 added eqs: 260 del clause: 96 arith eq adapter: 15 arith-upper: 44 arith-branch: 1 memory: 11.15 max memory: 12.63 num allocs: 2.89203e+10
Expand
• start[3.489s, "Goal"]
let (_x_0 : bt) = cbal ( :var_0: ) in
let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
( :var_0: ) >= 0
==> (if Is_a(Empty, _x_0) then true else _x_1 = _x_2 || _x_1 - _x_2 = 1)
• #### subproof

let (_x_0 : bt) = cbal x0 in let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in ((not (x0 >= 0) || Is_a(Empty, _x_0)) || _x_1 = _x_2) || _x_1 + (-1) * _x_2 = 1
• start[3.487s, "1"]
let (_x_0 : bt) = cbal x0 in
let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
((not (x0 >= 0) || Is_a(Empty, _x_0)) || _x_1 = _x_2)
|| _x_1 + (-1) * _x_2 = 1
• induction on (functional ?)
:scheme (not (not (1 = x0) && not (0 = x0) && not (x0 < 0)) ==> φ x0)
&& (not (x0 < 0)
&& not (0 = x0)
&& not (1 = x0)
&& φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1))
==> φ x0)
• Split (let (_x_0 : bt) = cbal x0 in
let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
let (_x_3 : bool)
= ((not (x0 >= 0) || _x_1 + (-1) * _x_2 = 1) || Is_a(Empty, _x_0))
|| _x_1 = _x_2
in
let (_x_4 : bool) = not (1 = x0) in
let (_x_5 : bool) = not (0 = x0) in
let (_x_6 : bool) = 0 <= x0 in
let (_x_7 : int) = (-1) + x0 in
let (_x_8 : int) = _x_7 / 2 in
let (_x_9 : int) = (-1) * _x_8 in
let (_x_10 : bt) = cbal (_x_7 + _x_9) in
let (_x_11 : int) = nodes (Destruct(Branch, 2, _x_10)) in
let (_x_12 : int) = nodes (Destruct(Branch, 1, _x_10)) in
let (_x_13 : bt) = cbal _x_8 in
let (_x_14 : int) = nodes (Destruct(Branch, 2, _x_13)) in
let (_x_15 : int) = nodes (Destruct(Branch, 1, _x_13)) in
(_x_3 || (_x_4 && _x_5) && _x_6)
&& (_x_3
|| not
((((_x_6 && _x_5) && _x_4)
&& (((_x_11 + (-1) * _x_12 = 1 || _x_11 = _x_12)
|| Is_a(Empty, _x_10))
|| not ((x0 + _x_9) >= 1)))
&& (((Is_a(Empty, _x_13) || not (_x_8 >= 0)) || _x_14 = _x_15)
|| _x_14 + (-1) * _x_15 = 1)))
:cases [let (_x_0 : bt) = cbal x0 in
let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
(((not (x0 >= 0) || _x_1 + (-1) * _x_2 = 1)
|| Is_a(Empty, _x_0))
|| _x_1 = _x_2)
|| (not (1 = x0) && not (0 = x0)) && 0 <= x0;
let (_x_0 : int) = (-1) + x0 in
let (_x_1 : int) = _x_0 / 2 in
let (_x_2 : int) = (-1) * _x_1 in
let (_x_3 : bt) = cbal (_x_0 + _x_2) in
let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in
let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in
let (_x_6 : bt) = cbal _x_1 in
let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_6)) in
let (_x_8 : int) = nodes (Destruct(Branch, 1, _x_6)) in
let (_x_9 : bt) = cbal x0 in
let (_x_10 : int) = nodes (Destruct(Branch, 2, _x_9)) in
let (_x_11 : int) = nodes (Destruct(Branch, 1, _x_9)) in
(((((((not (x0 >= 0) || not (0 <= x0)) || 0 = x0) || 1 = x0)
|| not
(((_x_4 + (-1) * _x_5 = 1 || _x_4 = _x_5)
|| Is_a(Empty, _x_3))
|| not ((x0 + _x_2) >= 1)))
|| not
(((Is_a(Empty, _x_6) || not (_x_1 >= 0)) || _x_7 = _x_8)
|| _x_7 + (-1) * _x_8 = 1))
|| _x_10 + (-1) * _x_11 = 1)
|| Is_a(Empty, _x_9))
|| _x_10 = _x_11])
• ##### subproof
let (_x_0 : int) = (-1) + x0 in let (_x_1 : int) = _x_0 / 2 in let (_x_2 : int) = (-1) * _x_1 in let (_x_3 : bt) = cbal (_x_0 + _x_2) in let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in let (_x_6 : bt) = cbal _x_1 in let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_6)) in let (_x_8 : int) = nodes (Destruct(Branch, 1, _x_6)) in let (_x_9 : bt) = cbal x0 in let (_x_10 : int) = nodes (Destruct(Branch, 2, _x_9)) in let (_x_11 : int) = nodes (Destruct(Branch, 1, _x_9)) in (((((((not (x0 >= 0) || not (0 <= x0)) || 0 = x0) || 1 = x0) || not (((_x_4 + (-1) * _x_5 = 1 || _x_4 = _x_5) || Is_a(Empty, _x_3)) || not ((x0 + _x_2) >= 1))) || not (((Is_a(Empty, _x_6) || not (_x_1 >= 0)) || _x_7 = _x_8) || _x_7 + (-1) * _x_8 = 1)) || _x_10 + (-1) * _x_11 = 1) || Is_a(Empty, _x_9)) || _x_10 = _x_11
• start[3.394s, "1.1"]
let (_x_0 : int) = (-1) + x0 in
let (_x_1 : int) = _x_0 / 2 in
let (_x_2 : int) = (-1) * _x_1 in
let (_x_3 : bt) = cbal (_x_0 + _x_2) in
let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in
let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in
let (_x_6 : bt) = cbal _x_1 in
let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_6)) in
let (_x_8 : int) = nodes (Destruct(Branch, 1, _x_6)) in
let (_x_9 : bt) = cbal x0 in
let (_x_10 : int) = nodes (Destruct(Branch, 2, _x_9)) in
let (_x_11 : int) = nodes (Destruct(Branch, 1, _x_9)) in
(((((((not (x0 >= 0) || not (0 <= x0)) || 0 = x0) || 1 = x0)
|| not
(((_x_4 + (-1) * _x_5 = 1 || _x_4 = _x_5) || Is_a(Empty, _x_3))
|| not ((x0 + _x_2) >= 1)))
|| not
(((Is_a(Empty, _x_6) || not (_x_1 >= 0)) || _x_7 = _x_8)
|| _x_7 + (-1) * _x_8 = 1))
|| _x_10 + (-1) * _x_11 = 1)
|| Is_a(Empty, _x_9))
|| _x_10 = _x_11
• ###### simplify
 into: let (_x_0 : bool) = not (x0 >= 0) in let (_x_1 : int) = (-1) + x0 in let (_x_2 : int) = _x_1 / 2 in let (_x_3 : bt) = cbal _x_2 in let (_x_4 : bool) = Is_a(Empty, _x_3) in let (_x_5 : bool) = _x_0 || _x_4 in let (_x_6 : bt) = cbal (_x_1 + (-1) * _x_2) in let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_6)) in let (_x_8 : int) = nodes (Destruct(Branch, 1, _x_6)) in let (_x_9 : bool) = not (_x_7 = _x_8) in let (_x_10 : bool) = _x_7 + (-1) * _x_8 = 1 in let (_x_11 : int) = _x_8 + _x_7 in let (_x_12 : int) = nodes (Destruct(Branch, 1, _x_3)) in let (_x_13 : int) = (-1) * _x_12 in let (_x_14 : int) = nodes (Destruct(Branch, 2, _x_3)) in let (_x_15 : int) = (-1) * _x_14 in let (_x_16 : bool) = _x_11 + _x_13 + _x_15 = 1 in let (_x_17 : bool) = 0 = x0 in let (_x_18 : int) = _x_12 + _x_14 in let (_x_19 : bool) = _x_11 = _x_18 in let (_x_20 : bool) = _x_14 = _x_12 in let (_x_21 : bool) = not (_x_14 + _x_13 = 1) in let (_x_22 : bool) = Is_a(Empty, _x_6) in let (_x_23 : bool) = not _x_20 in let (_x_24 : bool) = (_x_0 || _x_23) || _x_4 in let (_x_25 : bool) = not _x_10 in let (_x_26 : bool) = _x_11 = 0 in let (_x_27 : bool) = _x_11 = (-1) in let (_x_28 : bool) = not _x_4 in let (_x_29 : bool) = _x_0 || not _x_22 in let (_x_30 : bool) = _x_13 + _x_15 = 2 in let (_x_31 : bool) = (-1) = _x_18 in ((((((((((((((_x_5 || _x_9) || _x_10) || _x_16) || _x_17) || _x_19) || _x_20) || _x_21) || _x_22) && ((((((_x_24 || _x_9) || _x_10) || _x_16) || _x_17) || _x_19) || _x_22)) && (((((((_x_5 || _x_16) || _x_17) || _x_19) || _x_20) || _x_25) || _x_21) || _x_22)) && (((((_x_24 || _x_16) || _x_17) || _x_19) || _x_25) || _x_22)) && (((((((_x_0 || _x_9) || _x_10) || _x_26) || _x_27) || _x_17) || _x_28) || _x_22)) && ((((((_x_0 || _x_26) || _x_27) || _x_17) || _x_28) || _x_25) || _x_22)) && ((((((_x_29 || _x_4) || _x_30) || _x_31) || _x_17) || _x_20) || _x_21)) && (((((_x_29 || _x_23) || _x_4) || _x_30) || _x_31) || _x_17) expansions: [nodes, nodes, cbal, cbal, nodes, nodes, cbal, cbal, nodes, nodes, cbal, cbal, nodes, nodes, cbal] rewrite_steps: forward_chaining:
• Subproof
• Subproof
• Subproof
• Subproof
• Subproof
• Subproof
• Subproof
• Subproof
• ##### subproof
let (_x_0 : bt) = cbal x0 in let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in (((not (x0 >= 0) || _x_1 + (-1) * _x_2 = 1) || Is_a(Empty, _x_0)) || _x_1 = _x_2) || (not (1 = x0) && not (0 = x0)) && 0 <= x0
• start[3.394s, "1.2"]
let (_x_0 : bt) = cbal x0 in
let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
(((not (x0 >= 0) || _x_1 + (-1) * _x_2 = 1) || Is_a(Empty, _x_0))
|| _x_1 = _x_2)
|| (not (1 = x0) && not (0 = x0)) && 0 <= x0
• ###### simplify
 into: true expansions: [cbal, cbal, nodes, nodes, cbal] rewrite_steps: forward_chaining:

In this demonstration we used Discover to suggest conjectures and lemmas used in the verification of some properties of balanced binary trees. We also showed examples of using conditions with Discover and some basic pointers on its use.