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.

Try this!

In [1]:

(* #require "imandra-discover-bridge";; *)
open Imandra_discover_bridge.User_level;;

Out[1]:

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

Try this!

In [2]:

#max_induct 1;;
#induct_unroll 20;;

Out[2]:

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.

Try this!

In [3]:

type bt = | Empty
          | Branch of
            {value : int;
             left : bt;
             right : bt;};;

Out[3]:

type bt = Empty | Branch of { value : Z.t; left : bt; right : bt; }

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

Try this!

In [4]:

let lhs_split n = n/2;;
let rhs_split n = n - lhs_split n;;

Out[4]:

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.

Try this!

In [5]:

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

Out[5]:

 <===DISCOVER===================================>
 We are running Discover on the following signature:
 
+:int->int->int
lhs_split:int->int
rhs_split:int->int

 We are running Discover with this inferred constant type:
 type nonrec discover_type = | Bool of discover_bool
                            | Int of discover_int
 <==============================================> 
Running Discover on: discover_run
 <===DISCOVER RESULTS===========================> 
The below laws are the result of the condition: No condition. These are the 6 amazing conjectures suggested by Discover for discover_run.
fun x -> (lhs_split (x + x)) = x
fun x -> (rhs_split (x + x)) = x
fun x -> ((lhs_split x) + (rhs_split x)) = x
fun x y -> (y + x) = (x + y)
fun x y z -> (y + (x + z)) = (x + (y + z))
fun x y z -> ((x + y) + z) = (x + (y + z))
These are SUBSUMED laws that may be interesting to the user.
 No subsumed conjectures.
 <==============================================> 
A string list `discover_result` with the conjectures before filtering has been defined.
A string list `discover_result_simplified` contains the conjectures after simplification by Imandra.
- : unit = ()

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.

Try this!

In [6]:

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

Out[6]:

val discover__2 : discover_int -> discover_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.

Try this!

In [7]:

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

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

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.010s

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:	3124
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:	234599799
final checks:	1
added eqs:	9
del clause:	11
arith eq adapter:	5
memory:	22.630000
max memory:	22.630000

Expand

start[0.010s]
  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)) \|\| not (not (1 = n) && not (0 = n) && (0 <= n)) \|\| Ordinal.( << ) (Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)) (Ordinal.Int (if n >= 0 then n else 0))
expansions:	[]
rewrite_steps:
forward_chaining:

unroll

expr:	(let ((a!1 (ite (>= (div (+ (- 1) n_449/server) 2) 0) (div (+ (- 1) n_449/server) 2)…
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

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.012s

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:	1634
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:	207035054
final checks:	1
added eqs:	9
del clause:	16
arith eq adapter:	5
memory:	22.610000
max memory:	22.610000

Expand

start[0.012s]
  let (_x_0 : int) = if n >= 0 then n else 0 in
  let (_x_1 : int) = n - 1 in
  let (_x_2 : int) = _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_449/server (* (- 1) (div (+ (- 1) n_449/server) 2)))) (a!2 (+ (- 1) n_449/serv…
expansions:

Unsat

This is simply the size of the tree.

Try this!

In [8]:

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

Out[8]:

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:

[Is_a(Branch, tree)]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.013s

details:

Expand

smt_stats:

num checks:	8
arith assert lower:	45
arith tableau max rows:	8
arith tableau max columns:	23
arith pivots:	18
rlimit count:	7986
mk clause:	68
datatype occurs check:	24
mk bool var:	199
arith assert upper:	67
datatype splits:	7
decisions:	84
arith row summations:	29
arith bound prop:	1
propagations:	96
conflicts:	21
arith fixed eqs:	15
datatype accessor ax:	13
minimized lits:	1
arith conflicts:	4
arith num rows:	8
arith assert diseq:	7
datatype constructor ax:	34
num allocs:	294612948
final checks:	6
added eqs:	171
del clause:	44
arith eq adapter:	41
memory:	22.990000
max memory:	23.020000

Expand

start[0.013s]
  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) = not Is_a(Branch, _x_1) in
  Is_a(Branch, 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 _x_0 in let (_x_2 : int) = count.bt tree in Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) \|\| not Is_a(Branch, _x_0) \|\| not (Is_a(Branch, tree) && (_x_2 >= 0) && (_x_1 >= 0))
expansions:	[]
rewrite_steps:
forward_chaining:

unroll

expr:	(\|count.bt_1262/client\| (\|get.Branch.left_519/server\| tree_521/server))
expansions:

unroll

expr:	(\|Ordinal.<<\| (\|Ordinal.Int_79/boot\| (\|count.bt_1262/client\| (\|get…
expansions:

unroll

expr:	(\|count.bt_1262/client\| tree_521/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:

[Is_a(Branch, tree)]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.012s

details:

Expand

smt_stats:

num checks:	8
arith assert lower:	27
arith tableau max rows:	9
arith tableau max columns:	24
arith pivots:	21
rlimit count:	3818
mk clause:	50
datatype occurs check:	19
mk bool var:	141
arith assert upper:	37
datatype splits:	5
decisions:	44
arith row summations:	46
arith bound prop:	1
propagations:	47
conflicts:	17
arith fixed eqs:	10
datatype accessor ax:	9
minimized lits:	2
arith conflicts:	5
arith num rows:	9
arith assert diseq:	5
datatype constructor ax:	24
num allocs:	264878116
final checks:	5
added eqs:	103
del clause:	26
arith eq adapter:	27
memory:	23.020000
max memory:	23.020000

Expand

start[0.012s]
  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) = not Is_a(Branch, _x_1) in
  Is_a(Branch, 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, 2, tree) in let (_x_1 : int) = count.bt _x_0 in let (_x_2 : int) = count.bt tree in not Is_a(Branch, _x_0) \|\| Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) \|\| not (Is_a(Branch, tree) && (_x_2 >= 0) && (_x_1 >= 0))
expansions:	[]
rewrite_steps:
forward_chaining:

unroll

expr:	(\|Ordinal.<<\| (\|Ordinal.Int_79/boot\| (\|count.bt_1262/client\| (\|get…
expansions:

unroll

expr:	(\|count.bt_1262/client\| (\|get.Branch.right_520/server\| tree_521/server))
expansions:

unroll

expr:	(\|count.bt_1262/client\| tree_521/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.

Try this!

In [9]:

let nonnegative x = x >= 0;;
let leq_zero x = x <= 0;;

Out[9]:

val nonnegative : discover_int -> discover_bool = <fun>
val leq_zero : discover_int -> discover_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.

Try this!

In [10]:

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

Out[10]:

 <===DISCOVER===================================>
 We are running Discover on the following signature:
 
mk_Empty:bt
mk_Branch:int->bt->bt->bt
nodes:bt->int
cbal:int->bt

 We are running Discover with this inferred constant type:
 type nonrec discover_type =
  | Bool of discover_bool
  | Int of discover_int
  | Bt of discover_bt
 <==============================================> 
Running Discover on: discover_run
 <===DISCOVER RESULTS===========================> 
The below laws are the result of the condition: nonnegative x0
These are the 4 amazing conjectures suggested by Discover for discover_run.
fun x -> (nonnegative x) ==> (cbal (nodes mk_Empty)) = mk_Empty
fun x -> (nonnegative x) ==> (nodes (cbal x)) = x
fun x y z -> (nonnegative x) ==> (nodes (mk_Branch x z y)) = (nodes (mk_Branch x y z))
fun u x y z -> (nonnegative x) ==> (nodes (mk_Branch (nodes u) y z)) = (nodes (mk_Branch x y z))
These are SUBSUMED laws that may be interesting to the user.
 No subsumed conjectures.
 <==============================================> 
A string list `discover_result` with the conjectures before filtering has been defined.
A string list `discover_result_simplified` contains the conjectures after simplification by Imandra.
- : unit = ()

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.

Try this!

In [11]:

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

Out[11]:

val discover__0 : discover_int -> discover_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. 0 <= x0
 H1. not (0 = x0)
 H2. not (1 = x0)
 H3. x0 + (-1) * (((-1) + x0) / 2) >= 1
     ==> nodes (cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
         = (-1) + x0 + (-1) * (((-1) + x0) / 2)
 H4. ((-1) + x0) / 2 >= 0
     ==> nodes (cbal (((-1) + x0) / 2)) = ((-1) + x0) / 2
 H5. x0 >= 0
|---------------------------------------------------------------------------
 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.349s

Expand

start[0.349s, "Goal"]
  ( :var_0: ) >= 0 ==> nodes (cbal ( :var_0: )) = ( :var_0: )

subproof

not (x0 >= 0) || (nodes (cbal x0) = x0)

start[0.349s, "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)
       && (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)))
           || _x_3 || _x_4)
       :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 (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)
               || not (x0 >= 0) || (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 (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) || not (x0 >= 0) || (nodes (cbal x0) = x0)
- start[0.097s, "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 (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) || not (x0 >= 0) || (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.097s, "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:

digraph "proof" {
p_55 [label="Start (( :var_0: ) \>= 0 ==\> nodes (cbal ( :var_0: )) = ( :var_0: )\l       :name \"Goal\" :time 0.349s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_55 -> p_53 [label=""];
subgraph cluster_54 {
  color=blue;
p_53 [label="Start (not (x0 \>= 0) \|\| (nodes (cbal x0) = x0) :name \"1\" :time 0.349s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_53 -> p_52 [label=""];
p_52 [label="Induct ((functional ?),\l        :scheme (not (not (1 = x0) && (not (0 = x0) && not (x0 \< 0)))\l                 ==\> φ x0)\l                && (not (x0 \< 0)\l                    && (not (0 = x0)\l                        && (not (1 = x0)\l                            && (φ (rhs_split (x0 - 1))\l                                && φ (lhs_split (x0 - 1)))))\l                    ==\> φ x0))",shape=box,style=filled,fontname="courier",fontsize=14];
p_52 -> p_51 [label=""];
p_51 [label="Split (let (_x_0 : bool) = not (1 = x0) in\l       let (_x_1 : bool) = not (0 = x0) in\l       let (_x_2 : bool) = 0 \<= x0 in\l       let (_x_3 : bool) = nodes (cbal x0) = x0 in\l       let (_x_4 : bool) = not (x0 \>= 0) in\l       let (_x_5 : int) = (-1) + x0 in\l       let (_x_6 : int) = _x_5 / 2 in\l       let (_x_7 : int) = (-1) * _x_6 in\l       let (_x_8 : int) = _x_5 + _x_7 in\l       ((_x_0 && _x_1 && _x_2) \|\| _x_3 \|\| _x_4)\l       && (not\l           (_x_2 && _x_1 && _x_0\l            && (not (x0 + _x_7 \>= 1) \|\| (nodes (cbal _x_8) = _x_8))\l            && (not (_x_6 \>= 0) \|\| (nodes (cbal _x_6) = _x_6)))\l           \|\| _x_3 \|\| _x_4)\l       :cases [not (x0 \>= 0) \|\| (not (1 = x0) && not (0 = x0) && (0 \<= x0))\l               \|\| (nodes (cbal x0) = x0);\l               let (_x_0 : int) = (-1) + x0 in\l               let (_x_1 : int) = _x_0 / 2 in\l               let (_x_2 : int) = (-1) * _x_1 in\l               let (_x_3 : int) = _x_0 + _x_2 in\l               not (0 \<= x0) \|\| (0 = x0) \|\| (1 = x0)\l               \|\| not (x0 + _x_2 \>= 1 ==\> nodes (cbal _x_3) = _x_3)\l               \|\| not (_x_1 \>= 0 ==\> nodes (cbal _x_1) = _x_1)\l               \|\| not (x0 \>= 0) \|\| (nodes (cbal x0) = x0)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_51 -> p_46 [label=""];
subgraph cluster_47 {
  color=blue;
p_46 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : int) = (-1) * _x_1 in\l       let (_x_3 : int) = _x_0 + _x_2 in\l       not (0 \<= x0) \|\| (0 = x0) \|\| (1 = x0)\l       \|\| not (x0 + _x_2 \>= 1 ==\> nodes (cbal _x_3) = _x_3)\l       \|\| not (_x_1 \>= 0 ==\> nodes (cbal _x_1) = _x_1) \|\| not (x0 \>= 0)\l       \|\| (nodes (cbal x0) = x0) :name \"1.1\" :time 0.097s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_46 -> p_45 [label=""];
p_45 [label="Simplify (true :expansions [nodes; cbal] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_51 -> p_49 [label=""];
subgraph cluster_50 {
  color=blue;
p_49 [label="Start (not (x0 \>= 0) \|\| (not (1 = x0) && not (0 = x0) && (0 \<= x0))\l       \|\| (nodes (cbal x0) = x0) :name \"1.2\" :time 0.097s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_49 -> p_48 [label=""];
p_48 [label="Simplify (true :expansions [nodes; nodes; nodes; cbal] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

What about the zero or negative case?

Try this!

In [12]:

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

Out[12]:

 <===DISCOVER===================================>
 We are running Discover on the following signature:
 
Empty:bt
mk_Empty:bt
mk_Branch:int->bt->bt->bt
nodes:bt->int
cbal:int->bt

 We are running Discover with this inferred constant type:
 type nonrec discover_type =
  | Bool of discover_bool
  | Int of discover_int
  | Bt of discover_bt
 <==============================================> 
Running Discover on: discover_run
 <===DISCOVER RESULTS===========================> 
The below laws are the result of the condition: leq_zero x0
These are the 5 amazing conjectures suggested by Discover for discover_run.
fun x -> (leq_zero x) ==> mk_Empty = Empty
fun x -> (leq_zero x) ==> (cbal x) = Empty
fun x y -> (leq_zero x) ==> (nodes (mk_Branch y Empty Empty)) = (nodes (mk_Branch x Empty Empty))
fun x y z -> (leq_zero x) ==> (nodes (mk_Branch x z y)) = (nodes (mk_Branch x y z))
fun u x y z -> (leq_zero x) ==> (nodes (mk_Branch (nodes u) y z)) = (nodes (mk_Branch x y z))
These are SUBSUMED laws that may be interesting to the user.
 No subsumed conjectures.
 <==============================================> 
A string list `discover_result` with the conjectures before filtering has been defined.
A string list `discover_result_simplified` contains the conjectures after simplification by Imandra.
- : unit = ()

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

Try this!

In [13]:

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

Out[13]:

val discover__0_neg : discover_int -> discover_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.016s

Expand

start[0.016s, "Goal"] ( :var_0: ) <= 0 ==> cbal ( :var_0: ) = Empty

subproof
not (x0 <= 0) || (cbal x0 = Empty)
- start[0.016s, "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.

Try this!

In [14]:

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[14]:

val is_balanced : discover_bt -> discover_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.

Try this!

In [15]:

discover db ["is_balanced";"cbal";"true"];;

Out[15]:

 <===DISCOVER===================================>
 We are running Discover on the following signature:
 
true:bool
mk_Empty:bt
mk_Branch:int->bt->bt->bt
is_balanced:bt->bool
cbal:int->bt

 We are running Discover with this inferred constant type:
 type nonrec discover_type =
  | Bool of discover_bool
  | Int of discover_int
  | Bt of discover_bt
 <==============================================> 
Running Discover on: discover_run
 <===DISCOVER RESULTS===========================> 
The below laws are the result of the condition: No condition. These are the 3 amazing conjectures suggested by Discover for discover_run.
(is_balanced mk_Empty) = true
fun x -> (is_balanced (cbal x)) = true
fun x y -> (is_balanced (mk_Branch x y y)) = true
These are SUBSUMED laws that may be interesting to the user.
 No subsumed conjectures.
 <==============================================> 
A string list `discover_result` with the conjectures before filtering has been defined.
A string list `discover_result_simplified` contains the conjectures after simplification by Imandra.
- : unit = ()

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

Try this!

In [16]:

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

Out[16]:

val discover_cbal_balanced_0 : discover_int -> discover_bool = <fun>
Goal:

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

1 nontautological subgoal.

Subgoal 1:

 H0. Is_a(Branch, cbal x0)
 H1. x0 >= 0
|---------------------------------------------------------------------------
 C0. nodes (Destruct(Branch, 2, cbal x0))
     = nodes (Destruct(Branch, 1, cbal x0))
 C1. 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
 H1. Is_a(Branch, cbal x0)
|---------------------------------------------------------------------------
 C0. not (1 = x0) && not (0 = x0) && (0 <= x0)
 C1. nodes (Destruct(Branch, 2, cbal x0))
     + (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
 C2. nodes (Destruct(Branch, 2, cbal x0))
     = nodes (Destruct(Branch, 1, cbal x0))

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

Subgoal 1.1:

 H0. 0 <= x0
 H1. not (0 = x0)
 H2. not (1 = x0)
 H3. (nodes
      (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
      + (-1)
        * nodes
          (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
      = 1)
     || not (x0 + (-1) * (((-1) + x0) / 2) >= 1)
     || not Is_a(Branch, 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 + (-1) * (((-1) + x0) / 2)))))
 H4. (nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
      + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1)
     || not Is_a(Branch, 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))))
 H5. x0 >= 0
 H6. Is_a(Branch, cbal x0)
|---------------------------------------------------------------------------
 C0. nodes (Destruct(Branch, 2, cbal x0))
     + (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
 C1. 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. Is_a(Branch, cbal (((-1) + x0) / 2))
 H1. x0 >= 0
 H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
 C0. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
 C1. (-1)
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
 C2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
 C3. 0 = x0
 C4. 1 = x0
 C5. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2

This simplifies to:

Subgoal 1.1.8':

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

But we verify Subgoal 1.1.8' by recursive unrolling.

Subgoal 1.1.7:

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

This simplifies to:

Subgoal 1.1.7':

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

But we verify Subgoal 1.1.7' by recursive unrolling.

Subgoal 1.1.6:

 H0. x0 >= 0
 H1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-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(Branch, 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))))
     = 0
 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))))
     = (-1)
 C5. 1 = x0

This simplifies to:

Subgoal 1.1.6':

 H0. x0 >= 0
 H1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-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(Branch, 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))))
     = 0
 C2. 0 = x0

But we verify Subgoal 1.1.6' by recursive unrolling.

Subgoal 1.1.5:

 H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     + (-1)
       * nodes
         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = 1
 H1. x0 >= 0
 H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
 C0. Is_a(Branch, 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))))
     = 0
 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))))
     = (-1)
 C4. 1 = x0

This simplifies to:

Subgoal 1.1.5':

 H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     + (-1)
       * nodes
         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = 1
 H1. x0 >= 0
 H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
 C0. Is_a(Branch, 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))))
     = (-1)

But we verify Subgoal 1.1.5' by recursive unrolling.

Subgoal 1.1.4:

 H0. Is_a(Branch, cbal (((-1) + x0) / 2))
 H1. x0 >= 0
 H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
 H3. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
 H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = nodes
       (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
|---------------------------------------------------------------------------
 C0. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-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))))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
 C2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     + (-1)
       * nodes
         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = 1
 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. 0 = x0
 C5. 1 = x0

This simplifies to:

Subgoal 1.1.4':

 H0. Is_a(Branch, cbal (((-1) + x0) / 2))
 H1. x0 >= 0
 H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
 H3. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
 H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = nodes
       (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-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))))
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
 C1. 0 = x0

But we verify Subgoal 1.1.4' by recursive unrolling.

Subgoal 1.1.3:

 H0. Is_a(Branch, cbal (((-1) + x0) / 2))
 H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
 H2. x0 >= 0
 H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
 H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = nodes
       (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-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))))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
 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))))
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
 C3. 0 = x0
 C4. 1 = x0

This simplifies to:

Subgoal 1.1.3':

 H0. Is_a(Branch, cbal (((-1) + x0) / 2))
 H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
 H2. x0 >= 0
 H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
 H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = nodes
       (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-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))))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
 C1. 0 = x0

But we verify Subgoal 1.1.3' by recursive unrolling.

Subgoal 1.1.2:

 H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     + (-1)
       * nodes
         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = 1
 H1. Is_a(Branch, cbal (((-1) + x0) / 2))
 H2. x0 >= 0
 H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
 H4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
 C0. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-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))))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 2, cbal (((-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))))
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
 C3. 0 = x0
 C4. 1 = x0

This simplifies to:

Subgoal 1.1.2':

 H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     + (-1)
       * nodes
         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = 1
 H1. Is_a(Branch, cbal (((-1) + x0) / 2))
 H2. x0 >= 0
 H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
 H4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     = nodes (Destruct(Branch, 1, 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))))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
 C1. 0 = x0

But we verify Subgoal 1.1.2' by recursive unrolling.

Subgoal 1.1.1:

 H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     + (-1)
       * nodes
         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = 1
 H1. Is_a(Branch, cbal (((-1) + x0) / 2))
 H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
 H3. x0 >= 0
 H4. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-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))))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 2, cbal (((-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))))
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
 C2. 0 = x0
 C3. 1 = x0

This simplifies to:

Subgoal 1.1.1':

 H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     + (-1)
       * nodes
         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
     = 1
 H1. Is_a(Branch, cbal (((-1) + x0) / 2))
 H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
     + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
 H3. x0 >= 0
 H4. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-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))))
     = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
 C1. 0 = x0

But we verify Subgoal 1.1.1' by recursive unrolling.

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

Proved

proof

ground_instances:

definitions:

inductions:

search_time:

3.652s

details:

Expand

smt_stats:

num checks:	6
arith-assume-eqs:	6
arith-make-feasible:	75
arith-max-columns:	48
arith-conflicts:	8
rlimit count:	1112956
arith-gcd-calls:	2
arith-cheap-eqs:	25
mk clause:	349
datatype occurs check:	79
mk bool var:	459
arith-lower:	114
arith-diseq:	74
datatype splits:	46
decisions:	202
arith-propagations:	67
propagations:	429
arith-patches:	2
interface eqs:	6
arith-bound-propagations-cheap:	67
arith-max-rows:	26
conflicts:	39
datatype accessor ax:	23
minimized lits:	14
arith-bound-propagations-lp:	13
datatype constructor ax:	58
final checks:	19
added eqs:	584
del clause:	145
arith eq adapter:	66
arith-upper:	67
arith-branch:	1
time:	0.002000
memory:	53.130000
max memory:	53.840000
num allocs:	60388558788.000000

Expand

start[3.652s, "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(Branch, _x_0) then (_x_1 = _x_2) || (_x_1 - _x_2 = 1)
       else true)

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 Is_a(Branch, _x_0) || not (x0 >= 0) || (_x_1 = _x_2) || (_x_1 + (-1) * _x_2 = 1)

start[3.652s, "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 Is_a(Branch, _x_0) || not (x0 >= 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 : bool) = not (1 = x0) in
       let (_x_1 : bool) = not (0 = x0) in
       let (_x_2 : bool) = 0 <= x0 in
       let (_x_3 : bt) = cbal x0 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 : bool) = _x_4 + (-1) * _x_5 = 1 in
       let (_x_7 : bool) = _x_4 = _x_5 in
       let (_x_8 : bool) = not (x0 >= 0) in
       let (_x_9 : bool) = not Is_a(Branch, _x_3) in
       let (_x_10 : int) = (-1) + x0 in
       let (_x_11 : int) = _x_10 / 2 in
       let (_x_12 : int) = (-1) * _x_11 in
       let (_x_13 : bt) = cbal (_x_10 + _x_12) in
       let (_x_14 : int) = nodes (Destruct(Branch, 2, _x_13)) in
       let (_x_15 : int) = nodes (Destruct(Branch, 1, _x_13)) in
       let (_x_16 : bt) = cbal _x_11 in
       let (_x_17 : int) = nodes (Destruct(Branch, 2, _x_16)) in
       let (_x_18 : int) = nodes (Destruct(Branch, 1, _x_16)) in
       ((_x_0 && _x_1 && _x_2) || _x_6 || _x_7 || _x_8 || _x_9)
       && (not
           (_x_2 && _x_1 && _x_0
            && ((_x_14 + (-1) * _x_15 = 1) || not (x0 + _x_12 >= 1)
                || not Is_a(Branch, _x_13) || (_x_14 = _x_15))
            && ((_x_17 + (-1) * _x_18 = 1) || not Is_a(Branch, _x_16)
                || not (_x_11 >= 0) || (_x_17 = _x_18)))
           || _x_6 || _x_7 || _x_8 || _x_9)
       :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) || not Is_a(Branch, _x_0)
               || (not (1 = x0) && not (0 = x0) && (0 <= x0))
               || (_x_1 + (-1) * _x_2 = 1) || (_x_1 = _x_2);
               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 (0 <= x0) || (0 = x0) || (1 = x0)
               || not
                  ((_x_4 + (-1) * _x_5 = 1) || not (x0 + _x_2 >= 1)
                   || not Is_a(Branch, _x_3) || (_x_4 = _x_5))
               || not
                  ((_x_7 + (-1) * _x_8 = 1) || not Is_a(Branch, _x_6)
                   || not (_x_1 >= 0) || (_x_7 = _x_8))
               || not (x0 >= 0) || not Is_a(Branch, _x_9)
               || (_x_10 + (-1) * _x_11 = 1) || (_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 (0 <= x0) || (0 = x0) || (1 = x0) || not ((_x_4 + (-1) * _x_5 = 1) || not (x0 + _x_2 >= 1) || not Is_a(Branch, _x_3) || (_x_4 = _x_5)) || not ((_x_7 + (-1) * _x_8 = 1) || not Is_a(Branch, _x_6) || not (_x_1 >= 0) || (_x_7 = _x_8)) || not (x0 >= 0) || not Is_a(Branch, _x_9) || (_x_10 + (-1) * _x_11 = 1) || (_x_10 = _x_11)

start[3.330s, "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 (0 <= x0) || (0 = x0) || (1 = x0)
  || not
     ((_x_4 + (-1) * _x_5 = 1) || not (x0 + _x_2 >= 1)
      || not Is_a(Branch, _x_3) || (_x_4 = _x_5))
  || not
     ((_x_7 + (-1) * _x_8 = 1) || not Is_a(Branch, _x_6) || not (_x_1 >= 0)
      || (_x_7 = _x_8))
  || not (x0 >= 0) || not Is_a(Branch, _x_9) || (_x_10 + (-1) * _x_11 = 1)
  || (_x_10 = _x_11)

simplify

into:	let (_x_0 : int) = (-1) + x0 in let (_x_1 : int) = _x_0 / 2 in let (_x_2 : bt) = cbal _x_1 in let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in let (_x_5 : int) = (-1) * _x_4 in let (_x_6 : bool) = _x_3 + _x_5 = 1 in let (_x_7 : bool) = Is_a(Branch, _x_2) in let (_x_8 : bool) = not _x_7 in let (_x_9 : int) = _x_4 + _x_3 in let (_x_10 : bool) = (-1) = _x_9 in let (_x_11 : bool) = not (x0 >= 0) in let (_x_12 : bt) = cbal (_x_0 + (-1) * _x_1) in let (_x_13 : bool) = Is_a(Branch, _x_12) in let (_x_14 : bool) = not (_x_3 = _x_4) in let (_x_15 : bool) = 0 = x0 in let (_x_16 : bool) = 1 = x0 in let (_x_17 : int) = (-1) * _x_3 in let (_x_18 : bool) = _x_5 + _x_17 = 2 in let (_x_19 : bool) = not _x_6 in let (_x_20 : int) = nodes (Destruct(Branch, 2, _x_12)) in let (_x_21 : int) = nodes (Destruct(Branch, 1, _x_12)) in let (_x_22 : bool) = _x_20 + (-1) * _x_21 = 1 in let (_x_23 : int) = _x_21 + _x_20 in let (_x_24 : bool) = _x_23 = 0 in let (_x_25 : bool) = not _x_13 in let (_x_26 : bool) = _x_23 = (-1) in let (_x_27 : bool) = not (_x_20 = _x_21) in let (_x_28 : bool) = not _x_22 in let (_x_29 : bool) = _x_23 + _x_5 + _x_17 = 1 in let (_x_30 : bool) = _x_23 = _x_9 in (_x_6 \|\| _x_8 \|\| _x_10 \|\| _x_11 \|\| _x_13 \|\| _x_14 \|\| _x_15 \|\| _x_16 \|\| _x_18) && (_x_8 \|\| _x_19 \|\| _x_10 \|\| _x_11 \|\| _x_13 \|\| _x_15 \|\| _x_16 \|\| _x_18) && (_x_7 \|\| _x_22 \|\| _x_24 \|\| _x_11 \|\| _x_25 \|\| _x_15 \|\| _x_26 \|\| _x_16 \|\| _x_27) && (_x_28 \|\| _x_7 \|\| _x_24 \|\| _x_11 \|\| _x_25 \|\| _x_15 \|\| _x_26 \|\| _x_16) && (_x_6 \|\| _x_29 \|\| _x_8 \|\| _x_22 \|\| _x_11 \|\| _x_30 \|\| _x_25 \|\| _x_14 \|\| _x_15 \|\| _x_16 \|\| _x_27) && (_x_29 \|\| _x_8 \|\| _x_19 \|\| _x_22 \|\| _x_11 \|\| _x_30 \|\| _x_25 \|\| _x_15 \|\| _x_16 \|\| _x_27) && (_x_28 \|\| _x_6 \|\| _x_29 \|\| _x_8 \|\| _x_11 \|\| _x_30 \|\| _x_25 \|\| _x_14 \|\| _x_15 \|\| _x_16) && (_x_28 \|\| _x_29 \|\| _x_8 \|\| _x_19 \|\| _x_11 \|\| _x_30 \|\| _x_25 \|\| _x_15 \|\| _x_16)
expansions:	[nodes, nodes, cbal, nodes, nodes, cbal, nodes, nodes, cbal, nodes, nodes, cbal, 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) || not Is_a(Branch, _x_0) || (not (1 = x0) && not (0 = x0) && (0 <= x0)) || (_x_1 + (-1) * _x_2 = 1) || (_x_1 = _x_2)
- start[3.330s, "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) || not Is_a(Branch, _x_0) || (not (1 = x0) && not (0 = x0) && (0 <= x0)) || (_x_1 + (-1) * _x_2 = 1) || (_x_1 = _x_2)
- simplify
  into:
  true
  expansions:
  [nodes, nodes, cbal, cbal]
  rewrite_steps:
  forward_chaining:

digraph "proof" {
p_125 [label="Start (let (_x_0 : bt) = cbal ( :var_0: ) in\l       let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in\l       let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in\l       ( :var_0: ) \>= 0\l       ==\> (if Is_a(Branch, _x_0) then (_x_1 = _x_2) \|\| (_x_1 - _x_2 = 1)\l            else true)\l       :name \"Goal\" :time 3.652s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_125 -> p_123 [label=""];
subgraph cluster_124 {
  color=blue;
p_123 [label="Start (let (_x_0 : bt) = cbal x0 in\l       let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in\l       let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in\l       not Is_a(Branch, _x_0) \|\| not (x0 \>= 0) \|\| (_x_1 = _x_2)\l       \|\| (_x_1 + (-1) * _x_2 = 1) :name \"1\" :time 3.652s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_123 -> p_122 [label=""];
p_122 [label="Induct ((functional ?),\l        :scheme (not (not (1 = x0) && (not (0 = x0) && not (x0 \< 0)))\l                 ==\> φ x0)\l                && (not (x0 \< 0)\l                    && (not (0 = x0)\l                        && (not (1 = x0)\l                            && (φ (rhs_split (x0 - 1))\l                                && φ (lhs_split (x0 - 1)))))\l                    ==\> φ x0))",shape=box,style=filled,fontname="courier",fontsize=14];
p_122 -> p_121 [label=""];
p_121 [label="Split (let (_x_0 : bool) = not (1 = x0) in\l       let (_x_1 : bool) = not (0 = x0) in\l       let (_x_2 : bool) = 0 \<= x0 in\l       let (_x_3 : bt) = cbal x0 in\l       let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in\l       let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in\l       let (_x_6 : bool) = _x_4 + (-1) * _x_5 = 1 in\l       let (_x_7 : bool) = _x_4 = _x_5 in\l       let (_x_8 : bool) = not (x0 \>= 0) in\l       let (_x_9 : bool) = not Is_a(Branch, _x_3) in\l       let (_x_10 : int) = (-1) + x0 in\l       let (_x_11 : int) = _x_10 / 2 in\l       let (_x_12 : int) = (-1) * _x_11 in\l       let (_x_13 : bt) = cbal (_x_10 + _x_12) in\l       let (_x_14 : int) = nodes (Destruct(Branch, 2, _x_13)) in\l       let (_x_15 : int) = nodes (Destruct(Branch, 1, _x_13)) in\l       let (_x_16 : bt) = cbal _x_11 in\l       let (_x_17 : int) = nodes (Destruct(Branch, 2, _x_16)) in\l       let (_x_18 : int) = nodes (Destruct(Branch, 1, _x_16)) in\l       ((_x_0 && _x_1 && _x_2) \|\| _x_6 \|\| _x_7 \|\| _x_8 \|\| _x_9)\l       && (not\l           (_x_2 && _x_1 && _x_0\l            && ((_x_14 + (-1) * _x_15 = 1) \|\| not (x0 + _x_12 \>= 1)\l                \|\| not Is_a(Branch, _x_13) \|\| (_x_14 = _x_15))\l            && ((_x_17 + (-1) * _x_18 = 1) \|\| not Is_a(Branch, _x_16)\l                \|\| not (_x_11 \>= 0) \|\| (_x_17 = _x_18)))\l           \|\| _x_6 \|\| _x_7 \|\| _x_8 \|\| _x_9)\l       :cases [let (_x_0 : bt) = cbal x0 in\l               let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in\l               let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in\l               not (x0 \>= 0) \|\| not Is_a(Branch, _x_0)\l               \|\| (not (1 = x0) && not (0 = x0) && (0 \<= x0))\l               \|\| (_x_1 + (-1) * _x_2 = 1) \|\| (_x_1 = _x_2);\l               let (_x_0 : int) = (-1) + x0 in\l               let (_x_1 : int) = _x_0 / 2 in\l               let (_x_2 : int) = (-1) * _x_1 in\l               let (_x_3 : bt) = cbal (_x_0 + _x_2) in\l               let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in\l               let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in\l               let (_x_6 : bt) = cbal _x_1 in\l               let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_6)) in\l               let (_x_8 : int) = nodes (Destruct(Branch, 1, _x_6)) in\l               let (_x_9 : bt) = cbal x0 in\l               let (_x_10 : int) = nodes (Destruct(Branch, 2, _x_9)) in\l               let (_x_11 : int) = nodes (Destruct(Branch, 1, _x_9)) in\l               not (0 \<= x0) \|\| (0 = x0) \|\| (1 = x0)\l               \|\| not\l                  ((_x_4 + (-1) * _x_5 = 1) \|\| not (x0 + _x_2 \>= 1)\l                   \|\| not Is_a(Branch, _x_3) \|\| (_x_4 = _x_5))\l               \|\| not\l                  ((_x_7 + (-1) * _x_8 = 1) \|\| not Is_a(Branch, _x_6)\l                   \|\| not (_x_1 \>= 0) \|\| (_x_7 = _x_8))\l               \|\| not (x0 \>= 0) \|\| not Is_a(Branch, _x_9)\l               \|\| (_x_10 + (-1) * _x_11 = 1) \|\| (_x_10 = _x_11)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_121 -> p_116 [label=""];
subgraph cluster_117 {
  color=blue;
p_116 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : int) = (-1) * _x_1 in\l       let (_x_3 : bt) = cbal (_x_0 + _x_2) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in\l       let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in\l       let (_x_6 : bt) = cbal _x_1 in\l       let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_6)) in\l       let (_x_8 : int) = nodes (Destruct(Branch, 1, _x_6)) in\l       let (_x_9 : bt) = cbal x0 in\l       let (_x_10 : int) = nodes (Destruct(Branch, 2, _x_9)) in\l       let (_x_11 : int) = nodes (Destruct(Branch, 1, _x_9)) in\l       not (0 \<= x0) \|\| (0 = x0) \|\| (1 = x0)\l       \|\| not\l          ((_x_4 + (-1) * _x_5 = 1) \|\| not (x0 + _x_2 \>= 1)\l           \|\| not Is_a(Branch, _x_3) \|\| (_x_4 = _x_5))\l       \|\| not\l          ((_x_7 + (-1) * _x_8 = 1) \|\| not Is_a(Branch, _x_6)\l           \|\| not (_x_1 \>= 0) \|\| (_x_7 = _x_8))\l       \|\| not (x0 \>= 0) \|\| not Is_a(Branch, _x_9)\l       \|\| (_x_10 + (-1) * _x_11 = 1) \|\| (_x_10 = _x_11) :name \"1.1\"\l       :time 3.330s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_116 -> p_115 [label=""];
p_115 [label="Simplify (let (_x_0 : int) = (-1) + x0 in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal _x_1 in\l          let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_5 : int) = (-1) * _x_4 in\l          let (_x_6 : bool) = _x_3 + _x_5 = 1 in\l          let (_x_7 : bool) = Is_a(Branch, _x_2) in\l          let (_x_8 : bool) = not _x_7 in\l          let (_x_9 : int) = _x_4 + _x_3 in\l          let (_x_10 : bool) = (-1) = _x_9 in\l          let (_x_11 : bool) = not (x0 \>= 0) in\l          let (_x_12 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_13 : bool) = Is_a(Branch, _x_12) in\l          let (_x_14 : bool) = not (_x_3 = _x_4) in\l          let (_x_15 : bool) = 0 = x0 in\l          let (_x_16 : bool) = 1 = x0 in\l          let (_x_17 : int) = (-1) * _x_3 in\l          let (_x_18 : bool) = _x_5 + _x_17 = 2 in\l          let (_x_19 : bool) = not _x_6 in\l          let (_x_20 : int) = nodes (Destruct(Branch, 2, _x_12)) in\l          let (_x_21 : int) = nodes (Destruct(Branch, 1, _x_12)) in\l          let (_x_22 : bool) = _x_20 + (-1) * _x_21 = 1 in\l          let (_x_23 : int) = _x_21 + _x_20 in\l          let (_x_24 : bool) = _x_23 = 0 in\l          let (_x_25 : bool) = not _x_13 in\l          let (_x_26 : bool) = _x_23 = (-1) in\l          let (_x_27 : bool) = not (_x_20 = _x_21) in\l          let (_x_28 : bool) = not _x_22 in\l          let (_x_29 : bool) = _x_23 + _x_5 + _x_17 = 1 in\l          let (_x_30 : bool) = _x_23 = _x_9 in\l          (_x_6 \|\| _x_8 \|\| _x_10 \|\| _x_11 \|\| _x_13 \|\| _x_14 \|\| _x_15 \|\| _x_16\l           \|\| _x_18)\l          && (_x_8 \|\| _x_19 \|\| _x_10 \|\| _x_11 \|\| _x_13 \|\| _x_15 \|\| _x_16\l              \|\| _x_18)\l          && (_x_7 \|\| _x_22 \|\| _x_24 \|\| _x_11 \|\| _x_25 \|\| _x_15 \|\| _x_26\l              \|\| _x_16 \|\| _x_27)\l          && (_x_28 \|\| _x_7 \|\| _x_24 \|\| _x_11 \|\| _x_25 \|\| _x_15 \|\| _x_26\l              \|\| _x_16)\l          && (_x_6 \|\| _x_29 \|\| _x_8 \|\| _x_22 \|\| _x_11 \|\| _x_30 \|\| _x_25\l              \|\| _x_14 \|\| _x_15 \|\| _x_16 \|\| _x_27)\l          && (_x_29 \|\| _x_8 \|\| _x_19 \|\| _x_22 \|\| _x_11 \|\| _x_30 \|\| _x_25\l              \|\| _x_15 \|\| _x_16 \|\| _x_27)\l          && (_x_28 \|\| _x_6 \|\| _x_29 \|\| _x_8 \|\| _x_11 \|\| _x_30 \|\| _x_25\l              \|\| _x_14 \|\| _x_15 \|\| _x_16)\l          && (_x_28 \|\| _x_29 \|\| _x_8 \|\| _x_19 \|\| _x_11 \|\| _x_30 \|\| _x_25\l              \|\| _x_15 \|\| _x_16)\l          :expansions [nodes;\l                       nodes;\l                       cbal;\l                       nodes;\l                       nodes;\l                       cbal;\l                       nodes;\l                       nodes;\l                       cbal;\l                       nodes;\l                       nodes;\l                       cbal;\l                       cbal]\l          :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_115 -> p_85 [label=""];
subgraph cluster_86 {
  color=blue;
p_85 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : int) = _x_4 + _x_3 in\l       let (_x_6 : bt) = cbal _x_1 in\l       let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_6)) in\l       let (_x_8 : int) = (-1) * _x_7 in\l       let (_x_9 : int) = nodes (Destruct(Branch, 2, _x_6)) in\l       not (_x_3 + (-1) * _x_4 = 1) \|\| (_x_5 + _x_8 + (-1) * _x_9 = 1)\l       \|\| not Is_a(Branch, _x_6) \|\| not (_x_9 + _x_8 = 1) \|\| not (x0 \>= 0)\l       \|\| (_x_5 = _x_7 + _x_9) \|\| not Is_a(Branch, _x_2) \|\| (0 = x0)\l       \|\| (1 = x0) :name \"1.1.1\" :time 2.850s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_85 -> p_84 [label=""];
p_84 [label="Simplify (let (_x_0 : int) = (-1) + x0 in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_5 : bt) = cbal _x_1 in\l          let (_x_6 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l          let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_5)) in\l          not (_x_3 + (-1) * _x_4 = 1) \|\| not Is_a(Branch, _x_5)\l          \|\| not (_x_6 + (-1) * _x_7 = 1) \|\| not (x0 \>= 0)\l          \|\| (_x_4 + _x_3 = _x_7 + _x_6) \|\| not Is_a(Branch, _x_2)\l          \|\| (0 = x0) :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_84 -> p_82 [label=""];
subgraph cluster_83 {
  color=blue;
p_82 [label="Start (let (_x_0 : int) = (-1) + ( :var_0: ) in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : bt) = cbal _x_1 in\l       let (_x_6 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l       let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_5)) in\l       not (_x_3 + (-1) * _x_4 = 1) \|\| not Is_a(Branch, _x_5)\l       \|\| not (_x_6 + (-1) * _x_7 = 1) \|\| not (( :var_0: ) \>= 0)\l       \|\| not Is_a(Branch, _x_2) \|\| (_x_4 + _x_3 = _x_7 + _x_6)\l       \|\| (0 = ( :var_0: )) :time 0.016s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_82 -> p_81 [label=""];
p_81 [label="Simplify (let (_x_0 : int) = (-1) + ( :var_0: ) in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_5 : bt) = cbal _x_1 in\l          let (_x_6 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l          let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_5)) in\l          (0 = ( :var_0: )) \|\| not (( :var_0: ) \>= 0)\l          \|\| not (_x_3 + (-1) * _x_4 = 1) \|\| not Is_a(Branch, _x_5)\l          \|\| not (_x_6 + (-1) * _x_7 = 1) \|\| (_x_4 + _x_3 = _x_7 + _x_6)\l          \|\| not Is_a(Branch, _x_2) :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_81 -> p_80 [label=""];
p_80 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in cbal (_x_0 + (-1) * (_x_0 / 2))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_80 -> p_79 [label=""];
p_79 [label="Unroll ([cbal (((-1) + x0) / 2)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_79 -> p_78 [label=""];
p_78 [label="Unsat",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
p_115 -> p_89 [label=""];
subgraph cluster_90 {
  color=blue;
p_89 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : bt) = cbal _x_1 in\l       let (_x_6 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l       let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_5)) in\l       let (_x_8 : int) = (-1) * _x_7 in\l       let (_x_9 : int) = _x_4 + _x_3 in\l       not (_x_3 + (-1) * _x_4 = 1) \|\| (_x_6 + _x_8 = 1)\l       \|\| (_x_9 + _x_8 + (-1) * _x_6 = 1) \|\| not Is_a(Branch, _x_5)\l       \|\| not (x0 \>= 0) \|\| (_x_9 = _x_7 + _x_6) \|\| not Is_a(Branch, _x_2)\l       \|\| not (_x_6 = _x_7) \|\| (0 = x0) \|\| (1 = x0) :name \"1.1.2\"\l       :time 2.850s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_89 -> p_88 [label=""];
p_88 [label="Simplify (let (_x_0 : int) = (-1) + x0 in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_5 : bt) = cbal _x_1 in\l          let (_x_6 : int) = nodes (Destruct(Branch, 1, _x_5)) in\l          let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l          not (_x_3 + (-1) * _x_4 = 1)\l          \|\| (_x_4 + _x_3 + (-1) * _x_6 + (-1) * _x_7 = 1)\l          \|\| not Is_a(Branch, _x_5) \|\| not (x0 \>= 0)\l          \|\| not Is_a(Branch, _x_2) \|\| not (_x_7 = _x_6) \|\| (0 = x0)\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_88 -> p_77 [label=""];
subgraph cluster_87 {
  color=blue;
p_77 [label="Start (let (_x_0 : int) = (-1) + ( :var_0: ) in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : bt) = cbal _x_1 in\l       let (_x_6 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l       let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_5)) in\l       not (_x_3 + (-1) * _x_4 = 1) \|\| not Is_a(Branch, _x_5)\l       \|\| not (( :var_0: ) \>= 0) \|\| not Is_a(Branch, _x_2)\l       \|\| not (_x_6 = _x_7) \|\| (_x_4 + _x_3 + (-1) * _x_7 + (-1) * _x_6 = 1)\l       \|\| (0 = ( :var_0: )) :time 0.029s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_77 -> p_76 [label=""];
p_76 [label="Simplify (let (_x_0 : int) = (-1) + ( :var_0: ) in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_5 : bt) = cbal _x_1 in\l          let (_x_6 : int) = nodes (Destruct(Branch, 1, _x_5)) in\l          let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l          (0 = ( :var_0: )) \|\| not (( :var_0: ) \>= 0)\l          \|\| (_x_3 + _x_4 + (-1) * _x_6 + (-1) * _x_7 = 1)\l          \|\| not (_x_4 + (-1) * _x_3 = 1) \|\| not (_x_7 = _x_6)\l          \|\| not Is_a(Branch, _x_5) \|\| not Is_a(Branch, _x_2) :expansions []\l          :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_76 -> p_75 [label=""];
p_75 [label="Unroll ([nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_75 -> p_74 [label=""];
p_74 [label="Unroll ([nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_74 -> p_73 [label=""];
p_73 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in cbal (_x_0 + (-1) * (_x_0 / 2))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_73 -> p_72 [label=""];
p_72 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes (Destruct(Branch, 2, cbal (_x_0 + (-1) * (_x_0 / 2))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_72 -> p_71 [label=""];
p_71 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes (Destruct(Branch, 1, cbal (_x_0 + (-1) * (_x_0 / 2))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_71 -> p_70 [label=""];
p_70 [label="Unroll ([cbal (((-1) + x0) / 2)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_70 -> p_69 [label=""];
p_69 [label="Unsat",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
p_115 -> p_93 [label=""];
subgraph cluster_94 {
  color=blue;
p_93 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_3 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_5 : int) = _x_3 + _x_4 in\l       let (_x_6 : bt) = cbal _x_1 in\l       let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_6)) in\l       let (_x_8 : int) = (-1) * _x_7 in\l       let (_x_9 : int) = nodes (Destruct(Branch, 2, _x_6)) in\l       (_x_5 + _x_8 + (-1) * _x_9 = 1) \|\| not Is_a(Branch, _x_6)\l       \|\| not (_x_9 + _x_8 = 1) \|\| (_x_4 + (-1) * _x_3 = 1) \|\| not (x0 \>= 0)\l       \|\| (_x_5 = _x_7 + _x_9) \|\| not Is_a(Branch, _x_2) \|\| (0 = x0)\l       \|\| (1 = x0) \|\| not (_x_4 = _x_3) :name \"1.1.3\" :time 2.850s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_93 -> p_92 [label=""];
p_92 [label="Simplify (let (_x_0 : int) = (-1) + x0 in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_5 : bt) = cbal _x_1 in\l          let (_x_6 : int) = (-1) * nodes (Destruct(Branch, 1, _x_5)) in\l          let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l          (_x_3 + _x_4 + _x_6 + (-1) * _x_7 = 1) \|\| not Is_a(Branch, _x_5)\l          \|\| not (_x_7 + _x_6 = 1) \|\| not (x0 \>= 0) \|\| not Is_a(Branch, _x_2)\l          \|\| (0 = x0) \|\| not (_x_4 = _x_3) :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_92 -> p_68 [label=""];
subgraph cluster_91 {
  color=blue;
p_68 [label="Start (let (_x_0 : int) = (-1) + ( :var_0: ) in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal _x_1 in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = (-1) * nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_6 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l       let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_5)) in\l       not Is_a(Branch, _x_2) \|\| not (_x_3 + _x_4 = 1)\l       \|\| not (( :var_0: ) \>= 0) \|\| not Is_a(Branch, _x_5)\l       \|\| not (_x_6 = _x_7) \|\| (_x_7 + _x_6 + _x_4 + (-1) * _x_3 = 1)\l       \|\| (0 = ( :var_0: )) :time 0.021s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_68 -> p_67 [label=""];
p_67 [label="Simplify (let (_x_0 : int) = (-1) + ( :var_0: ) in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_5 : bt) = cbal _x_1 in\l          let (_x_6 : int) = (-1) * nodes (Destruct(Branch, 1, _x_5)) in\l          let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l          (0 = ( :var_0: )) \|\| not (( :var_0: ) \>= 0)\l          \|\| (_x_3 + _x_4 + _x_6 + (-1) * _x_7 = 1) \|\| not (_x_4 = _x_3)\l          \|\| not Is_a(Branch, _x_5) \|\| not (_x_7 + _x_6 = 1)\l          \|\| not Is_a(Branch, _x_2) :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_67 -> p_66 [label=""];
p_66 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in cbal (_x_0 + (-1) * (_x_0 / 2))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_66 -> p_65 [label=""];
p_65 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes (Destruct(Branch, 1, cbal (_x_0 + (-1) * (_x_0 / 2))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_65 -> p_64 [label=""];
p_64 [label="Unroll ([nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_64 -> p_63 [label=""];
p_63 [label="Unroll ([cbal (((-1) + x0) / 2)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_63 -> p_62 [label=""];
p_62 [label="Unsat",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
p_115 -> p_97 [label=""];
subgraph cluster_98 {
  color=blue;
p_97 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal _x_1 in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : int) = (-1) * _x_4 in\l       let (_x_6 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_6)) in\l       let (_x_8 : int) = nodes (Destruct(Branch, 2, _x_6)) in\l       let (_x_9 : int) = _x_7 + _x_8 in\l       (_x_3 + _x_5 = 1) \|\| (_x_9 + _x_5 + (-1) * _x_3 = 1)\l       \|\| not Is_a(Branch, _x_2) \|\| (_x_8 + (-1) * _x_7 = 1) \|\| not (x0 \>= 0)\l       \|\| (_x_9 = _x_4 + _x_3) \|\| not Is_a(Branch, _x_6) \|\| not (_x_3 = _x_4)\l       \|\| (0 = x0) \|\| (1 = x0) \|\| not (_x_8 = _x_7) :name \"1.1.4\"\l       :time 2.850s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_97 -> p_96 [label=""];
p_96 [label="Simplify (let (_x_0 : int) = (-1) + x0 in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal _x_1 in\l          let (_x_3 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_3)) in\l          let (_x_5 : int) = nodes (Destruct(Branch, 2, _x_3)) in\l          let (_x_6 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          not Is_a(Branch, _x_2) \|\| not (x0 \>= 0)\l          \|\| (_x_4 + _x_5 = _x_6 + _x_7) \|\| not Is_a(Branch, _x_3)\l          \|\| not (_x_7 = _x_6) \|\| (0 = x0) \|\| not (_x_5 = _x_4)\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_96 -> p_61 [label=""];
subgraph cluster_95 {
  color=blue;
p_61 [label="Start (let (_x_0 : int) = (-1) + ( :var_0: ) in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal _x_1 in\l       let (_x_3 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_6 : int) = nodes (Destruct(Branch, 2, _x_3)) in\l       let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_3)) in\l       not Is_a(Branch, _x_2) \|\| not (( :var_0: ) \>= 0)\l       \|\| not Is_a(Branch, _x_3) \|\| not (_x_4 = _x_5) \|\| not (_x_6 = _x_7)\l       \|\| (_x_7 + _x_6 = _x_5 + _x_4) \|\| (0 = ( :var_0: )) :time 0.044s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_61 -> p_60 [label=""];
p_60 [label="Simplify (let (_x_0 : int) = (-1) + ( :var_0: ) in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal _x_1 in\l          let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_5 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_6 : int) = nodes (Destruct(Branch, 2, _x_5)) in\l          let (_x_7 : int) = nodes (Destruct(Branch, 1, _x_5)) in\l          (0 = ( :var_0: )) \|\| not (( :var_0: ) \>= 0) \|\| not (_x_3 = _x_4)\l          \|\| not (_x_6 = _x_7) \|\| not Is_a(Branch, _x_2)\l          \|\| (_x_7 + _x_6 = _x_4 + _x_3) \|\| not Is_a(Branch, _x_5)\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_60 -> p_59 [label=""];
p_59 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes (Destruct(Branch, 2, cbal (_x_0 + (-1) * (_x_0 / 2))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_59 -> p_58 [label=""];
p_58 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes (Destruct(Branch, 1, cbal (_x_0 + (-1) * (_x_0 / 2))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_58 -> p_57 [label=""];
p_57 [label="Unroll ([nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_57 -> p_56 [label=""];
p_56 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in cbal (_x_0 + (-1) * (_x_0 / 2))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_56 -> p_55 [label=""];
p_55 [label="Unroll ([nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_55 -> p_54 [label=""];
p_54 [label="Unroll ([cbal (((-1) + x0) / 2)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_54 -> p_53 [label=""];
p_53 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes\l         (Destruct(Branch, 1,\l                   Destruct(Branch, 2, cbal (_x_0 + (-1) * (_x_0 / 2)))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_53 -> p_52 [label=""];
p_52 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes\l         (Destruct(Branch, 2,\l                   Destruct(Branch, 2, cbal (_x_0 + (-1) * (_x_0 / 2)))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_52 -> p_51 [label=""];
p_51 [label="Unroll ([nodes (Destruct(Branch, 1, Destruct(Branch, 1, cbal …)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_51 -> p_50 [label=""];
p_50 [label="Unroll ([nodes (Destruct(Branch, 2, Destruct(Branch, 1, cbal …)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_50 -> p_49 [label=""];
p_49 [label="Unroll ([cbal (rhs_split ((-2) + x0 + (-1) * (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_49 -> p_48 [label=""];
p_48 [label="Unroll ([cbal (lhs_split ((-2) + x0 + (-1) * (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_48 -> p_47 [label=""];
p_47 [label="Unsat",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
p_115 -> p_101 [label=""];
subgraph cluster_102 {
  color=blue;
p_101 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : int) = _x_4 + _x_3 in\l       not (_x_3 + (-1) * _x_4 = 1) \|\| Is_a(Branch, cbal _x_1) \|\| (_x_5 = 0)\l       \|\| not (x0 \>= 0) \|\| not Is_a(Branch, _x_2) \|\| (0 = x0)\l       \|\| (_x_5 = (-1)) \|\| (1 = x0) :name \"1.1.5\" :time 2.850s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_101 -> p_100 [label=""];
p_100 [label="Simplify (let (_x_0 : int) = (-1) + x0 in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          not (_x_3 + (-1) * _x_4 = 1) \|\| Is_a(Branch, cbal _x_1)\l          \|\| not (x0 \>= 0) \|\| not Is_a(Branch, _x_2) \|\| (0 = x0)\l          \|\| (_x_4 + _x_3 = (-1)) :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_100 -> p_46 [label=""];
subgraph cluster_99 {
  color=blue;
p_46 [label="Start (let (_x_0 : int) = (-1) + ( :var_0: ) in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       not (_x_3 + (-1) * _x_4 = 1) \|\| not (( :var_0: ) \>= 0)\l       \|\| not Is_a(Branch, _x_2) \|\| Is_a(Branch, cbal _x_1)\l       \|\| (0 = ( :var_0: )) \|\| (_x_4 + _x_3 = (-1)) :time 0.016s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_46 -> p_45 [label=""];
p_45 [label="Simplify (let (_x_0 : int) = (-1) + ( :var_0: ) in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          Is_a(Branch, cbal _x_1) \|\| (0 = ( :var_0: ))\l          \|\| not (( :var_0: ) \>= 0) \|\| (_x_3 + _x_4 = (-1))\l          \|\| not (_x_4 + (-1) * _x_3 = 1) \|\| not Is_a(Branch, _x_2)\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_45 -> p_44 [label=""];
p_44 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in cbal (_x_0 + (-1) * (_x_0 / 2))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_44 -> p_43 [label=""];
p_43 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes (Destruct(Branch, 2, cbal (_x_0 + (-1) * (_x_0 / 2))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_43 -> p_42 [label=""];
p_42 [label="Unroll ([cbal (((-1) + x0) / 2)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_42 -> p_41 [label=""];
p_41 [label="Unsat",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
p_115 -> p_105 [label=""];
subgraph cluster_106 {
  color=blue;
p_105 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : int) = _x_4 + _x_3 in\l       Is_a(Branch, cbal _x_1) \|\| (_x_3 + (-1) * _x_4 = 1) \|\| (_x_5 = 0)\l       \|\| not (x0 \>= 0) \|\| not Is_a(Branch, _x_2) \|\| (0 = x0)\l       \|\| (_x_5 = (-1)) \|\| (1 = x0) \|\| not (_x_3 = _x_4) :name \"1.1.6\"\l       :time 2.850s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_105 -> p_104 [label=""];
p_104 [label="Simplify (let (_x_0 : int) = (-1) + x0 in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          Is_a(Branch, cbal _x_1) \|\| (_x_3 + _x_4 = 0) \|\| not (x0 \>= 0)\l          \|\| not Is_a(Branch, _x_2) \|\| (0 = x0) \|\| not (_x_4 = _x_3)\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_104 -> p_40 [label=""];
subgraph cluster_103 {
  color=blue;
p_40 [label="Start (let (_x_0 : int) = (-1) + ( :var_0: ) in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       not (( :var_0: ) \>= 0) \|\| not Is_a(Branch, _x_2) \|\| not (_x_3 = _x_4)\l       \|\| Is_a(Branch, cbal _x_1) \|\| (_x_4 + _x_3 = 0) \|\| (0 = ( :var_0: ))\l       :time 0.016s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_40 -> p_39 [label=""];
p_39 [label="Simplify (let (_x_0 : int) = (-1) + ( :var_0: ) in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal (_x_0 + (-1) * _x_1) in\l          let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          Is_a(Branch, cbal _x_1) \|\| (0 = ( :var_0: ))\l          \|\| not (( :var_0: ) \>= 0) \|\| not (_x_3 = _x_4) \|\| (_x_4 + _x_3 = 0)\l          \|\| not Is_a(Branch, _x_2) :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_39 -> p_38 [label=""];
p_38 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes (Destruct(Branch, 1, cbal (_x_0 + (-1) * (_x_0 / 2))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_38 -> p_37 [label=""];
p_37 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in cbal (_x_0 + (-1) * (_x_0 / 2))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_37 -> p_36 [label=""];
p_36 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in\l         nodes (Destruct(Branch, 2, cbal (_x_0 + (-1) * (_x_0 / 2))))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_36 -> p_35 [label=""];
p_35 [label="Unroll ([cbal (((-1) + x0) / 2)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_35 -> p_34 [label=""];
p_34 [label="Unsat",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
p_115 -> p_109 [label=""];
subgraph cluster_110 {
  color=blue;
p_109 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal _x_1 in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : int) = (-1) * _x_4 in\l       not Is_a(Branch, _x_2) \|\| not (_x_3 + _x_5 = 1)\l       \|\| ((-1) = _x_4 + _x_3) \|\| not (x0 \>= 0)\l       \|\| Is_a(Branch, cbal (_x_0 + (-1) * _x_1)) \|\| (0 = x0) \|\| (1 = x0)\l       \|\| (_x_5 + (-1) * _x_3 = 2) :name \"1.1.7\" :time 2.850s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_109 -> p_108 [label=""];
p_108 [label="Simplify (let (_x_0 : int) = (-1) + x0 in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal _x_1 in\l          let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          not Is_a(Branch, _x_2) \|\| not (_x_3 + (-1) * _x_4 = 1)\l          \|\| ((-1) = _x_4 + _x_3) \|\| not (x0 \>= 0)\l          \|\| Is_a(Branch, cbal (_x_0 + (-1) * _x_1)) \|\| (0 = x0)\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_108 -> p_33 [label=""];
subgraph cluster_107 {
  color=blue;
p_33 [label="Start (let (_x_0 : int) = (-1) + ( :var_0: ) in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal _x_1 in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       not Is_a(Branch, _x_2) \|\| not (_x_3 + (-1) * _x_4 = 1)\l       \|\| not (( :var_0: ) \>= 0) \|\| ((-1) = _x_4 + _x_3)\l       \|\| Is_a(Branch, cbal (_x_0 + (-1) * _x_1)) \|\| (0 = ( :var_0: ))\l       :time 0.015s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_33 -> p_32 [label=""];
p_32 [label="Simplify (let (_x_0 : int) = (-1) + ( :var_0: ) in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal _x_1 in\l          let (_x_3 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          (0 = ( :var_0: )) \|\| not (( :var_0: ) \>= 0) \|\| ((-1) = _x_3 + _x_4)\l          \|\| Is_a(Branch, cbal (_x_0 + (-1) * _x_1))\l          \|\| not Is_a(Branch, _x_2) \|\| not (_x_4 + (-1) * _x_3 = 1)\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_32 -> p_31 [label=""];
p_31 [label="Unroll ([nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_31 -> p_30 [label=""];
p_30 [label="Unroll ([cbal (((-1) + x0) / 2)], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_30 -> p_29 [label=""];
p_29 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in cbal (_x_0 + (-1) * (_x_0 / 2))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_29 -> p_28 [label=""];
p_28 [label="Unsat",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
p_115 -> p_113 [label=""];
subgraph cluster_114 {
  color=blue;
p_113 [label="Start (let (_x_0 : int) = (-1) + x0 in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal _x_1 in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       let (_x_5 : int) = (-1) * _x_4 in\l       (_x_3 + _x_5 = 1) \|\| not Is_a(Branch, _x_2) \|\| ((-1) = _x_4 + _x_3)\l       \|\| not (x0 \>= 0) \|\| Is_a(Branch, cbal (_x_0 + (-1) * _x_1))\l       \|\| not (_x_3 = _x_4) \|\| (0 = x0) \|\| (1 = x0)\l       \|\| (_x_5 + (-1) * _x_3 = 2) :name \"1.1.8\" :time 2.851s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_113 -> p_112 [label=""];
p_112 [label="Simplify (let (_x_0 : int) = (-1) + x0 in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal _x_1 in\l          let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          not Is_a(Branch, _x_2) \|\| not (x0 \>= 0)\l          \|\| Is_a(Branch, cbal (_x_0 + (-1) * _x_1)) \|\| not (_x_3 = _x_4)\l          \|\| (0 = x0) \|\| ((-1) * _x_4 + (-1) * _x_3 = 2) :expansions []\l          :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_112 -> p_27 [label=""];
subgraph cluster_111 {
  color=blue;
p_27 [label="Start (let (_x_0 : int) = (-1) + ( :var_0: ) in\l       let (_x_1 : int) = _x_0 / 2 in\l       let (_x_2 : bt) = cbal _x_1 in\l       let (_x_3 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l       let (_x_4 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l       not Is_a(Branch, _x_2) \|\| not (( :var_0: ) \>= 0) \|\| not (_x_3 = _x_4)\l       \|\| Is_a(Branch, cbal (_x_0 + (-1) * _x_1)) \|\| (0 = ( :var_0: ))\l       \|\| ((-1) * _x_4 + (-1) * _x_3 = 2) :time 0.015s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_27 -> p_26 [label=""];
p_26 [label="Simplify (let (_x_0 : int) = (-1) + ( :var_0: ) in\l          let (_x_1 : int) = _x_0 / 2 in\l          let (_x_2 : bt) = cbal _x_1 in\l          let (_x_3 : int) = nodes (Destruct(Branch, 1, _x_2)) in\l          let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_2)) in\l          (0 = ( :var_0: )) \|\| not (( :var_0: ) \>= 0)\l          \|\| ((-1) * _x_3 + (-1) * _x_4 = 2)\l          \|\| Is_a(Branch, cbal (_x_0 + (-1) * _x_1)) \|\| not (_x_4 = _x_3)\l          \|\| not Is_a(Branch, _x_2) :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_26 -> p_25 [label=""];
p_25 [label="Unroll ([nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_25 -> p_24 [label=""];
p_24 [label="Unroll ([nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))], [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_24 -> p_23 [label=""];
p_23 [label="Unroll ([let (_x_0 : int) = (-1) + x0 in cbal (_x_0 + (-1) * (_x_0 / 2))],\l        [[]])",shape=box,style=filled,fontname="courier",fontsize=14];
p_23 -> p_22 [label=""];
p_22 [label="Unsat",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}
p_121 -> p_119 [label=""];
subgraph cluster_120 {
  color=blue;
p_119 [label="Start (let (_x_0 : bt) = cbal x0 in\l       let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in\l       let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in\l       not (x0 \>= 0) \|\| not Is_a(Branch, _x_0)\l       \|\| (not (1 = x0) && not (0 = x0) && (0 \<= x0))\l       \|\| (_x_1 + (-1) * _x_2 = 1) \|\| (_x_1 = _x_2) :name \"1.2\" :time 3.330s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_119 -> p_118 [label=""];
p_118 [label="Simplify (true :expansions [nodes; nodes; cbal; cbal] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

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.

into:	true
expansions:	[nodes, cbal]
rewrite_steps:
forward_chaining: