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";; *)
open Imandra_discover_bridge.User_level;;
Out[1]:

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

In [2]:
#max_induct 1;;
#induct_unroll 20;;
Out[2]:

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

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

In [3]:
type bt = | Empty
          | Branch of
            {value : int;
             left : bt;
             right : bt;};;
Out[3]:
type bt = Empty | Branch of { value : Z.t; left : bt; right : bt; }

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

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

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

In [5]:
discover db ~iterations:2i ["+";"lhs_split";"rhs_split"];;
Out[5]:
 <===DISCOVER===================================>
 We are running Discover on the following signature:
 
+:int->int->int
lhs_split:int->int
rhs_split:int->int

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

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

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

lhs_split x0 + rhs_split x0 = x0.

1 tautological subgoal.

Subgoal 1:

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

But this is obviously true.

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

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

      Warning

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

      Warning

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

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

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

      Termination proof

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

                  This is simply the size of the tree.

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

                  Termination proof

                  call `nodes (Destruct(Branch, 1, tree))` from `nodes tree`
                  original:nodes tree
                  sub:nodes (Destruct(Branch, 1, tree))
                  original ordinal:Ordinal.Int (_cnt tree)
                  sub ordinal:Ordinal.Int (_cnt (Destruct(Branch, 1, tree)))
                  path:[Is_a(Branch, tree)]
                  proof:
                  detailed proof
                  ground_instances:3
                  definitions:0
                  inductions:0
                  search_time:
                  0.013s
                  details:
                  Expand
                  smt_stats:
                  num checks:8
                  arith assert lower:45
                  arith tableau max rows:8
                  arith tableau max columns:23
                  arith pivots:18
                  rlimit count:7986
                  mk clause:68
                  datatype occurs check:24
                  mk bool var:199
                  arith assert upper:67
                  datatype splits:7
                  decisions:84
                  arith row summations:29
                  arith bound prop:1
                  propagations:96
                  conflicts:21
                  arith fixed eqs:15
                  datatype accessor ax:13
                  minimized lits:1
                  arith conflicts:4
                  arith num rows:8
                  arith assert diseq:7
                  datatype constructor ax:34
                  num allocs:294612948
                  final checks:6
                  added eqs:171
                  del clause:44
                  arith eq adapter:41
                  memory:22.990000
                  max memory:23.020000
                  Expand
                  • start[0.013s]
                      let (_x_0 : int) = count.bt tree in
                      let (_x_1 : bt) = Destruct(Branch, 1, tree) in
                      let (_x_2 : int) = count.bt _x_1 in
                      let (_x_3 : bool) = not Is_a(Branch, _x_1) in
                      Is_a(Branch, tree) && ((_x_0 >= 0) && (_x_2 >= 0))
                      ==> (_x_3 && _x_3) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                  • simplify
                    into:
                    let (_x_0 : bt) = Destruct(Branch, 1, tree) in
                    let (_x_1 : int) = count.bt _x_0 in
                    let (_x_2 : int) = count.bt tree in
                    Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                    || not Is_a(Branch, _x_0)
                    || not (Is_a(Branch, tree) && (_x_2 >= 0) && (_x_1 >= 0))
                    expansions:
                    []
                    rewrite_steps:
                      forward_chaining:
                      • unroll
                        expr:
                        (|count.bt_1262/client| (|get.Branch.left_519/server| tree_521/server))
                        expansions:
                        • unroll
                          expr:
                          (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                          (|count.bt_1262/client|
                                            (|get…
                          expansions:
                          • unroll
                            expr:
                            (|count.bt_1262/client| tree_521/server)
                            expansions:
                            • Unsat
                            call `nodes (Destruct(Branch, 2, tree))` from `nodes tree`
                            original:nodes tree
                            sub:nodes (Destruct(Branch, 2, tree))
                            original ordinal:Ordinal.Int (_cnt tree)
                            sub ordinal:Ordinal.Int (_cnt (Destruct(Branch, 2, tree)))
                            path:[Is_a(Branch, tree)]
                            proof:
                            detailed proof
                            ground_instances:3
                            definitions:0
                            inductions:0
                            search_time:
                            0.012s
                            details:
                            Expand
                            smt_stats:
                            num checks:8
                            arith assert lower:27
                            arith tableau max rows:9
                            arith tableau max columns:24
                            arith pivots:21
                            rlimit count:3818
                            mk clause:50
                            datatype occurs check:19
                            mk bool var:141
                            arith assert upper:37
                            datatype splits:5
                            decisions:44
                            arith row summations:46
                            arith bound prop:1
                            propagations:47
                            conflicts:17
                            arith fixed eqs:10
                            datatype accessor ax:9
                            minimized lits:2
                            arith conflicts:5
                            arith num rows:9
                            arith assert diseq:5
                            datatype constructor ax:24
                            num allocs:264878116
                            final checks:5
                            added eqs:103
                            del clause:26
                            arith eq adapter:27
                            memory:23.020000
                            max memory:23.020000
                            Expand
                            • start[0.012s]
                                let (_x_0 : int) = count.bt tree in
                                let (_x_1 : bt) = Destruct(Branch, 2, tree) in
                                let (_x_2 : int) = count.bt _x_1 in
                                let (_x_3 : bool) = not Is_a(Branch, _x_1) in
                                Is_a(Branch, tree) && ((_x_0 >= 0) && (_x_2 >= 0))
                                ==> (_x_3 && _x_3) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                            • simplify
                              into:
                              let (_x_0 : bt) = Destruct(Branch, 2, tree) in
                              let (_x_1 : int) = count.bt _x_0 in
                              let (_x_2 : int) = count.bt tree in
                              not Is_a(Branch, _x_0)
                              || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                              || not (Is_a(Branch, tree) && (_x_2 >= 0) && (_x_1 >= 0))
                              expansions:
                              []
                              rewrite_steps:
                                forward_chaining:
                                • unroll
                                  expr:
                                  (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                  (|count.bt_1262/client|
                                                    (|get…
                                  expansions:
                                  • unroll
                                    expr:
                                    (|count.bt_1262/client| (|get.Branch.right_520/server| tree_521/server))
                                    expansions:
                                    • unroll
                                      expr:
                                      (|count.bt_1262/client| tree_521/server)
                                      expansions:
                                      • Unsat

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

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

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

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

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

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

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

                                              What about the zero or negative case?

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

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

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

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

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

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

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

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

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

                                                  In [16]:
                                                  lemma discover_cbal_balanced_0 x0 = x0 >= 0 ==> (is_balanced (cbal x0)) [@@auto];;
                                                  
                                                  Out[16]:
                                                  val discover_cbal_balanced_0 : discover_int -> discover_bool = <fun>
                                                  Goal:
                                                  
                                                  x0 >= 0 ==> is_balanced (cbal x0).
                                                  
                                                  1 nontautological subgoal.
                                                  
                                                  Subgoal 1:
                                                  
                                                   H0. Is_a(Branch, cbal x0)
                                                   H1. x0 >= 0
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 2, cbal x0))
                                                       = nodes (Destruct(Branch, 1, cbal x0))
                                                   C1. nodes (Destruct(Branch, 2, cbal x0))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
                                                  
                                                  
                                                  Must try induction.
                                                  
                                                  We shall induct according to a scheme derived from cbal.
                                                  
                                                  Induction scheme:
                                                  
                                                   (not (not (1 = x0) && (not (0 = x0) && not (x0 < 0))) ==> φ x0)
                                                   && (not (x0 < 0)
                                                       && (not (0 = x0)
                                                           && (not (1 = x0)
                                                               && (φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1)))))
                                                       ==> φ x0).
                                                  
                                                  2 nontautological subgoals.
                                                  
                                                  Subgoal 1.2:
                                                  
                                                   H0. x0 >= 0
                                                   H1. Is_a(Branch, cbal x0)
                                                  |---------------------------------------------------------------------------
                                                   C0. not (1 = x0) && not (0 = x0) && (0 <= x0)
                                                   C1. nodes (Destruct(Branch, 2, cbal x0))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
                                                   C2. nodes (Destruct(Branch, 2, cbal x0))
                                                       = nodes (Destruct(Branch, 1, cbal x0))
                                                  
                                                  But simplification reduces this to true, using the definitions of cbal and
                                                  nodes.
                                                  
                                                  Subgoal 1.1:
                                                  
                                                   H0. 0 <= x0
                                                   H1. not (0 = x0)
                                                   H2. not (1 = x0)
                                                   H3. (nodes
                                                        (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                        + (-1)
                                                          * nodes
                                                            (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                        = 1)
                                                       || not (x0 + (-1) * (((-1) + x0) / 2) >= 1)
                                                       || not Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                       || (nodes
                                                           (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                           = nodes
                                                             (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))))
                                                   H4. (nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                        + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1)
                                                       || not Is_a(Branch, cbal (((-1) + x0) / 2))
                                                       || not (((-1) + x0) / 2 >= 0)
                                                       || (nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                           = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))))
                                                   H5. x0 >= 0
                                                   H6. Is_a(Branch, cbal x0)
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 2, cbal x0))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1
                                                   C1. nodes (Destruct(Branch, 2, cbal x0))
                                                       = nodes (Destruct(Branch, 1, cbal x0))
                                                  
                                                  This simplifies, using the definitions of cbal and nodes to the following 8
                                                  subgoals:
                                                  
                                                  Subgoal 1.1.8:
                                                  
                                                   H0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H1. x0 >= 0
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                   C1. (-1)
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                         + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   C3. 0 = x0
                                                   C4. 1 = x0
                                                   C5. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.8':
                                                  
                                                   H0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H1. x0 >= 0
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   C1. 0 = x0
                                                   C2. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
                                                  
                                                  But we verify Subgoal 1.1.8' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.7:
                                                  
                                                   H0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                   H2. x0 >= 0
                                                  |---------------------------------------------------------------------------
                                                   C0. (-1)
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                         + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   C2. 0 = x0
                                                   C3. 1 = x0
                                                   C4. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.7':
                                                  
                                                   H0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                   H2. x0 >= 0
                                                  |---------------------------------------------------------------------------
                                                   C0. (-1)
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                         + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   C2. 0 = x0
                                                  
                                                  But we verify Subgoal 1.1.7' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.6:
                                                  
                                                   H0. x0 >= 0
                                                   H1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes
                                                         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   C1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 1
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 0
                                                   C3. 0 = x0
                                                   C4. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = (-1)
                                                   C5. 1 = x0
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.6':
                                                  
                                                   H0. x0 >= 0
                                                   H1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes
                                                         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 0
                                                   C2. 0 = x0
                                                  
                                                  But we verify Subgoal 1.1.6' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.5:
                                                  
                                                   H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 1
                                                   H1. x0 >= 0
                                                   H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 0
                                                   C2. 0 = x0
                                                   C3. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = (-1)
                                                   C4. 1 = x0
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.5':
                                                  
                                                   H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 1
                                                   H1. x0 >= 0
                                                   H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   C1. 0 = x0
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = (-1)
                                                  
                                                  But we verify Subgoal 1.1.5' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.4:
                                                  
                                                   H0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H1. x0 >= 0
                                                   H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   H3. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                   H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes
                                                         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 1
                                                   C3. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                         + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C4. 0 = x0
                                                   C5. 1 = x0
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.4':
                                                  
                                                   H0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H1. x0 >= 0
                                                   H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   H3. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                   H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes
                                                         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                         + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C1. 0 = x0
                                                  
                                                  But we verify Subgoal 1.1.4' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.3:
                                                  
                                                   H0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                   H2. x0 >= 0
                                                   H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes
                                                         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 1
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                         + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C3. 0 = x0
                                                   C4. 1 = x0
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.3':
                                                  
                                                   H0. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                   H2. x0 >= 0
                                                   H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes
                                                         (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C1. 0 = x0
                                                  
                                                  But we verify Subgoal 1.1.3' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.2:
                                                  
                                                   H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 1
                                                   H1. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H2. x0 >= 0
                                                   H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   H4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                         + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C3. 0 = x0
                                                   C4. 1 = x0
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.2':
                                                  
                                                   H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 1
                                                   H1. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H2. x0 >= 0
                                                   H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                   H4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C1. 0 = x0
                                                  
                                                  But we verify Subgoal 1.1.2' by recursive unrolling.
                                                  
                                                  Subgoal 1.1.1:
                                                  
                                                   H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 1
                                                   H1. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                   H3. x0 >= 0
                                                   H4. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
                                                   C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                         + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C2. 0 = x0
                                                   C3. 1 = x0
                                                  
                                                  This simplifies to:
                                                  
                                                  Subgoal 1.1.1':
                                                  
                                                   H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + (-1)
                                                         * nodes
                                                           (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = 1
                                                   H1. Is_a(Branch, cbal (((-1) + x0) / 2))
                                                   H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                       + (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
                                                   H3. x0 >= 0
                                                   H4. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
                                                  |---------------------------------------------------------------------------
                                                   C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       + nodes
                                                         (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
                                                       = nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
                                                         + nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
                                                   C1. 0 = x0
                                                  
                                                  But we verify Subgoal 1.1.1' by recursive unrolling.
                                                  
                                                   Rules:
                                                      (:def cbal)
                                                      (:def nodes)
                                                      (:induct cbal)
                                                  
                                                  
                                                  Proved
                                                  proof
                                                  ground_instances:37
                                                  definitions:17
                                                  inductions:1
                                                  search_time:
                                                  3.652s
                                                  details:
                                                  Expand
                                                  smt_stats:
                                                  num checks:6
                                                  arith-assume-eqs:6
                                                  arith-make-feasible:75
                                                  arith-max-columns:48
                                                  arith-conflicts:8
                                                  rlimit count:1112956
                                                  arith-gcd-calls:2
                                                  arith-cheap-eqs:25
                                                  mk clause:349
                                                  datatype occurs check:79
                                                  mk bool var:459
                                                  arith-lower:114
                                                  arith-diseq:74
                                                  datatype splits:46
                                                  decisions:202
                                                  arith-propagations:67
                                                  propagations:429
                                                  arith-patches:2
                                                  interface eqs:6
                                                  arith-bound-propagations-cheap:67
                                                  arith-max-rows:26
                                                  conflicts:39
                                                  datatype accessor ax:23
                                                  minimized lits:14
                                                  arith-bound-propagations-lp:13
                                                  datatype constructor ax:58
                                                  final checks:19
                                                  added eqs:584
                                                  del clause:145
                                                  arith eq adapter:66
                                                  arith-upper:67
                                                  arith-branch:1
                                                  time:0.002000
                                                  memory:53.130000
                                                  max memory:53.840000
                                                  num allocs:60388558788.000000
                                                  Expand
                                                  • start[3.652s, "Goal"]
                                                      let (_x_0 : bt) = cbal ( :var_0: ) in
                                                      let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
                                                      let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
                                                      ( :var_0: ) >= 0
                                                      ==> (if Is_a(Branch, _x_0) then (_x_1 = _x_2) || (_x_1 - _x_2 = 1)
                                                           else true)
                                                  • subproof

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

                                                          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.