Using Imandra Discover

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

Balanced Binary Trees

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

Demonstration

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

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

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

In [2]:
Imandra_discover_bridge.Top.init ();;
Out[2]:
- : unit = ()

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

In [3]:
#max_induct 1;;
Out[3]:

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

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

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

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

In [5]:
let lhs_split n = n/2;;
let rhs_split n = n - lhs_split n;;
Out[5]:
val lhs_split : Z.t -> Z.t = <fun>
val rhs_split : Z.t -> Z.t = <fun>

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

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

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

In [7]:
lemma discover__2 x0 = ((lhs_split x0) + (rhs_split x0)) = x0 [@@rewrite]  [@@auto];;
Out[7]:
val discover__2 : discover_int -> bool = <fun>
Goal:

lhs_split x0 + rhs_split x0 = x0.

1 tautological subgoal.

Subgoal 1:

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

But this is obviously true.

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

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

      Warning

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

      Warning

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

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

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

      Termination proof

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

                  This is simply the size of the tree.

                  In [9]:
                  let rec nodes tree =
                    match tree with
                    | Empty -> 0
                    | Branch {left; right; _} -> 1 + (nodes left) + (nodes right);;
                  
                  Out[9]:
                  val nodes : bt -> discover_int = <fun>
                  
                  termination proof

                  Termination proof

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

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

                                      In [10]:
                                      let nonnegative x = x >= 0;;
                                      let leq_zero x = x <= 0;;
                                      
                                      Out[10]:
                                      val nonnegative : discover_int -> bool = <fun>
                                      val leq_zero : discover_int -> bool = <fun>
                                      

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

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

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

                                      In [12]:
                                      lemma discover__0 x0 = x0 >= 0 ==> (nodes (cbal x0)) = x0   [@@auto];;
                                      
                                      Out[12]:
                                      val discover__0 : discover_int -> bool = <fun>
                                      Goal:
                                      
                                      x0 >= 0 ==> nodes (cbal x0) = x0.
                                      
                                      1 nontautological subgoal.
                                      
                                      Subgoal 1:
                                      
                                       H0. x0 >= 0
                                      |---------------------------------------------------------------------------
                                       nodes (cbal x0) = x0
                                      
                                      
                                      Must try induction.
                                      
                                      We shall induct according to a scheme derived from cbal.
                                      
                                      Induction scheme:
                                      
                                       (not (not (1 = x0) && not (0 = x0) && not (x0 < 0)) ==> φ x0)
                                       && (not (x0 < 0)
                                           && not (0 = x0)
                                              && not (1 = x0) && φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1))
                                           ==> φ x0).
                                      
                                      2 nontautological subgoals.
                                      
                                      Subgoal 1.2:
                                      
                                       H0. x0 >= 0
                                      |---------------------------------------------------------------------------
                                       C0. (not (1 = x0) && not (0 = x0)) && 0 <= x0
                                       C1. nodes (cbal x0) = x0
                                      
                                      But simplification reduces this to true, using the definitions of cbal and
                                      nodes.
                                      
                                      Subgoal 1.1:
                                      
                                       H0. x0 >= 0
                                       H1. 0 <= x0
                                       H2. not (0 = x0)
                                       H3. not (1 = x0)
                                       H4. (x0 + (-1) * ((-1) + x0) / 2) >= 1
                                           ==> nodes (cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)) =
                                               (-1) + x0 + (-1) * ((-1) + x0) / 2
                                       H5. (((-1) + x0) / 2) >= 0
                                           ==> nodes (cbal (((-1) + x0) / 2)) = ((-1) + x0) / 2
                                      |---------------------------------------------------------------------------
                                       nodes (cbal x0) = x0
                                      
                                      But simplification reduces this to true, using the definitions of cbal and
                                      nodes.
                                      
                                       Rules:
                                          (:def cbal)
                                          (:def nodes)
                                          (:induct cbal)
                                      
                                      
                                      Proved
                                      proof
                                      ground_instances:0
                                      definitions:6
                                      inductions:1
                                      search_time:
                                      0.147s
                                      Expand
                                      • start[0.147s, "Goal"]
                                          ( :var_0: ) >= 0 ==> nodes (cbal ( :var_0: )) = ( :var_0: )
                                      • subproof

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

                                              What about the zero or negative case?

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

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

                                              In [14]:
                                              lemma discover__0_neg x0 = x0 <= 0 ==> (cbal x0) = Empty [@@auto];;
                                              
                                              Out[14]:
                                              val discover__0_neg : discover_int -> bool = <fun>
                                              Goal:
                                              
                                              x0 <= 0 ==> cbal x0 = Empty.
                                              
                                              1 nontautological subgoal.
                                              
                                              Subgoal 1:
                                              
                                               H0. x0 <= 0
                                              |---------------------------------------------------------------------------
                                               cbal x0 = Empty
                                              
                                              But simplification reduces this to true, using the definition of cbal.
                                              
                                               Rules:
                                                  (:def cbal)
                                              
                                              
                                              Proved
                                              proof
                                              ground_instances:0
                                              definitions:1
                                              inductions:0
                                              search_time:
                                              0.012s
                                              Expand
                                              • start[0.012s, "Goal"] ( :var_0: ) <= 0 ==> cbal ( :var_0: ) = Empty
                                              • subproof

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

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

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

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

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

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

                                                  In [17]:
                                                  lemma discover_cbal_balanced_0 x0 = x0 >= 0 ==> (is_balanced (cbal x0)) [@@auto];;
                                                  
                                                  Out[17]:
                                                  val discover_cbal_balanced_0 : discover_int -> discover_bool = <fun>
                                                  Goal:
                                                  
                                                  x0 >= 0 ==> is_balanced (cbal x0).
                                                  
                                                  1 nontautological subgoal.
                                                  
                                                  Subgoal 1:
                                                  
                                                   H0. x0 >= 0
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal x0)
                                                   C1. nodes (Destruct(Branch, 2, cbal x0)) =
                                                       nodes (Destruct(Branch, 1, cbal x0))
                                                   C2. nodes (Destruct(Branch, 2, cbal x0))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
                                                  
                                                  
                                                  Must try induction.
                                                  
                                                  We shall induct according to a scheme derived from cbal.
                                                  
                                                  Induction scheme:
                                                  
                                                   (not (not (1 = x0) && not (0 = x0) && not (x0 < 0)) ==> φ x0)
                                                   && (not (x0 < 0)
                                                       && not (0 = x0)
                                                          && not (1 = x0) && φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1))
                                                       ==> φ x0).
                                                  
                                                  2 nontautological subgoals.
                                                  
                                                  Subgoal 1.2:
                                                  
                                                   H0. x0 >= 0
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 2, cbal x0))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
                                                   C1. Is_a(Empty, cbal x0)
                                                   C2. nodes (Destruct(Branch, 2, cbal x0)) =
                                                       nodes (Destruct(Branch, 1, cbal x0))
                                                   C3. (not (1 = x0) && not (0 = x0)) && 0 <= x0
                                                  
                                                  But simplification reduces this to true, using the definitions of cbal and
                                                  nodes.
                                                  
                                                  Subgoal 1.1:
                                                  
                                                   H0. x0 >= 0
                                                   H1. 0 <= x0
                                                   H2. not (0 = x0)
                                                   H3. not (1 = x0)
                                                   H4. ((nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                         + (-1)
                                                           * nodes
                                                             (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                         = 1
                                                         || nodes
                                                            (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
                                                            nodes
                                                            (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))))
                                                        || Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       || not ((x0 + (-1) * ((-1) + x0) / 2) >= 1)
                                                   H5. ((Is_a(Empty, cbal (((-1) + x0) / 2)) || not ((((-1) + x0) / 2) >= 0))
                                                        || nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                           nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))))
                                                       || nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                          + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 
                                                          1
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 2, cbal x0))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
                                                   C1. Is_a(Empty, cbal x0)
                                                   C2. nodes (Destruct(Branch, 2, cbal x0)) =
                                                       nodes (Destruct(Branch, 1, cbal x0))
                                                  
                                                  This simplifies, using the definitions of cbal and nodes to the following 8
                                                  subgoals:
                                                  
                                                  Subgoal 1.1.8:
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 1
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C3. 0 = x0
                                                   C4. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C5. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                   C6. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.8':
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C2. 0 = x0
                                                   C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  But we verify Subgoal 1.1.8' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.7:
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                   H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 1
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C3. 0 = x0
                                                   C4. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C5. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.7':
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                   H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. 0 = x0
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  
                                                  Cross-fertilizing with:
                                                  
                                                   nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
                                                   nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                  
                                                  This produces the modified subgoal:
                                                  
                                                  Subgoal 1.1.7'':
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. 0 = x0
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.7''':
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. 0 = x0
                                                   C2. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                   C3. 2
                                                       * nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                  
                                                  But we verify Subgoal 1.1.7''' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.6:
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 1
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C2. 0 = x0
                                                   C3. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                   C5. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.6':
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 1
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. 0 = x0
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  But we verify Subgoal 1.1.6' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.5:
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                   H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C2. 0 = x0
                                                   C3. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C4. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.5':
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                   H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C2. 0 = x0
                                                   C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  But we verify Subgoal 1.1.5' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.4:
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                   H2. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 1
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 0
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = (-1)
                                                   C3. 0 = x0
                                                   C4. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.4':
                                                  
                                                   H0. x0 >= 0
                                                   H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                   H2. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 0
                                                   C1. 0 = x0
                                                   C2. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  But we verify Subgoal 1.1.4' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.3:
                                                  
                                                   H0. x0 >= 0
                                                   H1. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 0
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = (-1)
                                                   C2. 0 = x0
                                                   C3. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.3':
                                                  
                                                   H0. x0 >= 0
                                                   H1. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2)))
                                                       = (-1)
                                                   C1. 0 = x0
                                                   C2. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                  
                                                  But we verify Subgoal 1.1.3' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.2:
                                                  
                                                   H0. x0 >= 0
                                                   H1. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
                                                   C2. (-1) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C3. 0 = x0
                                                   C4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.2':
                                                  
                                                   H0. x0 >= 0
                                                   H1. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. (-1) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C2. 0 = x0
                                                  
                                                  But we verify Subgoal 1.1.2' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.1:
                                                  
                                                   H0. x0 >= 0
                                                   H1. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
                                                   C2. (-1) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C3. 0 = x0
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.1':
                                                  
                                                   H0. x0 >= 0
                                                   H1. Is_a(Empty, cbal ((-1) + x0 + (-1) * ((-1) + x0) / 2))
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) =
                                                       nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Empty, cbal (((-1) + x0) / 2))
                                                   C1. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
                                                   C2. 0 = x0
                                                  
                                                  But we verify Subgoal 1.1.1' by recursive unrolling.
                                                  
                                                   Rules:
                                                      (:def cbal)
                                                      (:def nodes)
                                                      (:induct cbal)
                                                  
                                                  
                                                  Proved
                                                  proof
                                                  ground_instances:36
                                                  definitions:20
                                                  inductions:1
                                                  search_time:
                                                  3.489s
                                                  details:
                                                  Expand
                                                  smt_stats:
                                                  num checks:8
                                                  arith-assume-eqs:1
                                                  arith-make-feasible:31
                                                  arith-max-columns:36
                                                  arith-conflicts:2
                                                  rlimit count:1018496
                                                  arith-gcd-calls:1
                                                  arith-cheap-eqs:22
                                                  mk clause:217
                                                  datatype occurs check:22
                                                  mk bool var:208
                                                  arith-lower:25
                                                  arith-diseq:39
                                                  datatype splits:9
                                                  decisions:54
                                                  arith-propagations:27
                                                  propagations:172
                                                  arith-patches:1
                                                  interface eqs:1
                                                  arith-bound-propagations-cheap:27
                                                  arith-max-rows:17
                                                  conflicts:15
                                                  datatype accessor ax:7
                                                  minimized lits:4
                                                  arith-bound-propagations-lp:8
                                                  datatype constructor ax:14
                                                  final checks:10
                                                  added eqs:260
                                                  del clause:96
                                                  arith eq adapter:15
                                                  arith-upper:44
                                                  arith-branch:1
                                                  memory:11.150000
                                                  max memory:12.630000
                                                  num allocs:28920300388.000000
                                                  Expand
                                                  • start[3.489s, "Goal"]
                                                      let (_x_0 : bt) = cbal ( :var_0: ) in
                                                      let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
                                                      let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
                                                      ( :var_0: ) >= 0
                                                      ==> (if Is_a(Empty, _x_0) then true else _x_1 = _x_2 || _x_1 - _x_2 = 1)
                                                  • subproof

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

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