Binary Trees

Binary Trees Sam Owre, John Rushby, and N. Shankar

Computer Science Laboratory

SRI International Menlo Park CA USA Binary trees can be defined as abstract datatypes.

The following datatype declaration introduces the constructor leaf with recognizer leaf?, and constructor node with accessors val, left, and right, and recognizer node?.

Typechecking this datatype declaration generates the theories

binary tree adt and binary tree rec mod (shown below).
binary_tree[T : TYPE] : DATATYPE
 BEGIN
  leaf : leaf?
  node(val : T, left : binary_tree, right : binary_tree) : node?
 END binary_tree

Abstract datatype theory

binary_tree_adt[T: TYPE]: THEORY
BEGIN
binary_tree: TYPE
leaf?, node?: [binary_tree -> boolean]
leaf: (leaf?)
node: [T, binary_tree, binary_tree -> (node?)]
val: [(node?) -> T]
left: [(node?) -> binary_tree]
right: [(node?) -> binary_tree]
leaf_extensionality:
  AXIOM
    (FORALL (leaf?_var: (leaf?)), (leaf?_var2: (leaf?)):
       leaf?_var = leaf?_var2)
node_extensionality:
  AXIOM
    (FORALL (node?_var: (node?)), (node?_var2: (node?)):
       val(node?_var) = val(node?_var2)
         AND left(node?_var) = left(node?_var2)
           AND right(node?_var) = right(node?_var2)
         IMPLIES node?_var = node?_var2)

Abstract datatype theory (continued 1)

node_eta:
  AXIOM
    (FORALL (node?_var: (node?)):
       node(val(node?_var), left(node?_var), right(node?_var)) = node?_var)
val_node:
  AXIOM
    (FORALL (node1_var: T), (node2_var: binary_tree),
            (node3_var: binary_tree):
       val(node(node1_var, node2_var, node3_var)) = node1_var)
left_node:
  AXIOM
    (FORALL (node1_var: T), (node2_var: binary_tree),
            (node3_var: binary_tree):
       left(node(node1_var, node2_var, node3_var)) = node2_var)
right_node:
  AXIOM
    (FORALL (node1_var: T), (node2_var: binary_tree),
            (node3_var: binary_tree):
       right(node(node1_var, node2_var, node3_var)) = node3_var)

binary_tree_disjoint:
  AXIOM
    (FORALL (binary_tree_var: binary_tree):
       NOT (leaf?(binary_tree_var) AND node?(binary_tree_var)))
binary_tree_inclusive:
  AXIOM
    (FORALL (binary_tree_var: binary_tree):
       leaf?(binary_tree_var) OR node?(binary_tree_var))
binary_tree_induction:
  AXIOM
    (FORALL (p: [binary_tree -> boolean]):
       p(leaf)
         AND
         (FORALL (node1_var: T), (node2_var: binary_tree),
                 (node3_var: binary_tree):
            p(node2_var) AND p(node3_var)
              IMPLIES p(node(node1_var, node2_var, node3_var)))
         IMPLIES (FORALL (binary_tree_var: binary_tree): p(binary_tree_var)))

binary_tree_nat_rec((leaf?_fun: nat), (node?_fun: [T, nat, nat -> nat])):
[binary_tree -> nat]
=
LAMBDA (binary_tree_var: binary_tree):
CASES binary_tree_var OF
  leaf: leaf?_fun,
  node(node1_var, node2_var, node3_var):
      node?_fun(node1_var,
                binary_tree_nat_rec(leaf?_fun,
                                    node?_fun)(node2_var),
                binary_tree_nat_rec(leaf?_fun,
                                    node?_fun)(node3_var))
ENDCASES

binary_tree_ordinal_rec((leaf?_fun: ordinal),
(node?_fun: [T, ordinal, ordinal -> ordinal])):
[binary_tree -> ordinal]
=
LAMBDA (binary_tree_var: binary_tree):
CASES binary_tree_var OF
leaf: leaf?_fun,
node(node1_var, node2_var, node3_var):
node?_fun(node1_var,
binary_tree_ordinal_rec(leaf?_fun,
                        node?_fun)(node2_var),
binary_tree_ordinal_rec(leaf?_fun,
                        node?_fun)(node3_var))
ENDCASES
END binary_tree_adt

Recursion combinator

binary_tree_rec_mod[T: TYPE, range: TYPE]: THEORY
BEGIN
IMPORTING binary_tree_adt[T]
binary_tree_rec((leaf?_fun: range), (node?_fun: [T, range, range -> range])):
  [binary_tree -> range]
    =
      LAMBDA (binary_tree_var: binary_tree):
        CASES binary_tree_var OF
          leaf: leaf?_fun,
          node(node1_var, node2_var, node3_var):
              node?_fun(node1_var,
                        binary_tree_rec(leaf?_fun, node?_fun)(node2_var),
                        binary_tree_rec(leaf?_fun, node?_fun)(node3_var))
        ENDCASES
END binary_tree_rec_mod

Ordered Binary Trees

obt [T : TYPE,  <= : (total_order?[T])] : THEORY
BEGIN
IMPORTING binary_tree
A, B, C: VAR binary_tree[T]
x, y, z: VAR T
pp: VAR pred[T]
checkall((pp : pred[T]), A): bool =
  binary_tree_rec(TRUE, (LAMBDA x, (a, b : bool):
                           (a AND b AND pp(x))))(A)
i, j, k: VAR nat
size(A) : nat =
  binary_tree_rec(0, (LAMBDA x, i, j: i + j + 1))(A)
ordered?(A) : RECURSIVE bool =
  (IF node?(A) THEN (checkall((LAMBDA y: y<=val(A)), left(A)) AND
                 checkall((LAMBDA y: val(A)<=y), right(A)) AND
                  ordered?(left(A)) AND ordered?(right(A)))
         ELSE TRUE ENDIF)
  MEASURE size

Ordered Binary Trees (continued)

insert(x, A): RECURSIVE binary_tree[T] =
  (CASES A OF
    leaf: node(x, leaf, leaf),
    node(y, B, C): (IF x<=y THEN node(y, insert(x, B), C)
                            ELSE node(y, B, insert(x, C))
                    ENDIF)
   ENDCASES)
  MEASURE (LAMBDA x, A: size(A))
ordered?_insert_step: FORMULA
   pp(x) AND checkall(pp, A) IMPLIES checkall(pp, insert(x, A))
ordered?_insert: FORMULA
   ordered?(A) IMPLIES ordered?(insert(x, A))
END obt

Example Proof

ordered?_insert :
  |-------
{1} (FORALL (A: binary_tree), (x: T):
         ordered?(A) IMPLIES ordered?(insert(x, A)))

Rule? (induct ”A”)

Inducting on A,
this yields  2 subgoals:
ordered?_insert.1 :
  |-------
{1} (FORALL (x: T): ordered?(leaf) IMPLIES ordered?(insert(x, leaf)))

Rule? (skosimp)

For the top quantifier in 1, we introduce Skolem constants: (x!1)
this simplifies to:
ordered?_insert.1 :
  |-------
{1} ordered?(leaf) IMPLIES ordered?(insert(x!1, leaf))
Applying disjunctive simplification to flatten sequent,
this simplifies to:

Example Proof (continued 1)

ordered?_insert.1 :
{-1} ordered?(leaf)
  |-------
{1} ordered?(insert(x!1, leaf))

Rule? (expand ”insert”)

Expanding the definition of insert
this simplifies to:
ordered?_insert.1 :
[-1]   ordered?(leaf)
  |-------
{1} ordered?(node(x!1, leaf, leaf))

Rule? (expand ”ordered?” +)

Expanding the definition of ordered?
this simplifies to:
ordered?_insert.1 :
[-1]   ordered?(leaf)
  |-------
{1} (checkall((LAMBDA (y: T): y <= x!1), leaf)
         AND checkall((LAMBDA (y: T): x!1 <= y), leaf)
           AND ordered?(leaf) AND ordered?(leaf))

binary-trees 12

Rule? (assert)

Invoking decision procedures,
this simplifies to:
ordered?_insert.1 :
[-1]   ordered?(leaf)
  |-------
{1} (checkall((LAMBDA (y: T): y <= x!1), leaf)
         AND checkall((LAMBDA (y: T): x!1 <= y), leaf))

Rule? (auto-rewrite ”binary˙ tree˙ rec[T, bool]”)

Installing automatic rewrites:
  binary_tree_rec[T, bool],
this simplifies to:
ordered?_insert.1 :
[-1]   ordered?(leaf)
  |-------
[1]   (checkall((LAMBDA (y: T): y <= x!1), leaf)
         AND checkall((LAMBDA (y: T): x!1 <= y), leaf))

Rule? (split)

Splitting conjunctions,
this yields  2 subgoals:

ordered?_insert.1.1 :
[-1]   ordered?(leaf)
  |-------
{1} checkall((LAMBDA (y: T): y <= x!1), leaf)

Rule? (expand ”checkall”)

Rewriting binary_tree_rec(TRUE,
                (LAMBDA (x: T), (a, b: bool): (a AND b AND x <= x!1)))(leaf) to TRUE.
Expanding the definition of checkall
this simplifies to:
ordered?_insert.1.1 :
[-1]   ordered?(leaf)
  |-------
{1} TRUE
which is trivially true.
This completes the proof of ordered?_insert.1.1.

ordered?_insert.1.2 :
[-1]   ordered?(leaf)
  |-------
{1} checkall((LAMBDA (y: T): x!1 <= y), leaf)

Rule? (expand ”checkall”)

Rewriting binary_tree_rec(TRUE,
                (LAMBDA (x: T), (a, b: bool): (a AND b AND x!1 <= x)))(leaf) to TRUE.
Expanding the definition of checkall
this simplifies to:
ordered?_insert.1.2 :
[-1]   ordered?(leaf)
  |-------
{1} TRUE
which is trivially true.
This completes the proof of ordered?_insert.1.2.

This completes the proof of ordered?_insert.1.

ordered?_insert.2 :
  |-------
{1} (FORALL (node1_var: T), (node2_var: binary_tree),
              (node3_var: binary_tree):
         (FORALL (x: T):
            ordered?(node2_var) IMPLIES ordered?(insert(x, node2_var)))
           AND
           (FORALL (x: T):
              ordered?(node3_var) IMPLIES ordered?(insert(x, node3_var)))
           IMPLIES
           (FORALL (x: T):
              ordered?(node(node1_var, node2_var, node3_var))
                IMPLIES
                ordered?(insert(x, node(node1_var, node2_var, node3_var)))))

Rule? (skosimp)

For the top quantifier in 1, we introduce Skolem constants: (node1_var!1 node2_var!1 node3_var!1)
this simplifies to:

ordered?_insert.2 :
  |-------
{1} (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
        AND
        (FORALL (x: T):
           ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
        IMPLIES
        (FORALL (x: T):
           ordered?(node(node1_var!1, node2_var!1, node3_var!1))
             IMPLIES
             ordered?(insert(x, node(node1_var!1, node2_var!1, node3_var!1))))
Applying disjunctive simplification to flatten sequent,
this simplifies to:
ordered?_insert.2 :
{-1} (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
{-2} (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
  |-------
{1} (FORALL (x: T):
         ordered?(node(node1_var!1, node2_var!1, node3_var!1))
           IMPLIES
           ordered?(insert(x, node(node1_var!1, node2_var!1, node3_var!1))))

binary-trees 17

Rule? (skolem!)

For the top quantifier in 1, we introduce Skolem constants: (x!1)
this simplifies to:
ordered?_insert.2 :
[-1]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-2]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
  |-------
{1} ordered?(node(node1_var!1, node2_var!1, node3_var!1))
        IMPLIES
        ordered?(insert(x!1, node(node1_var!1, node2_var!1, node3_var!1)))

Rule? (rewrite ”ordered?” +)

Rewriting using ordered?,
this simplifies to:

ordered?_insert.2 :
[-1]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-2]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
  |-------
{1} (checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
         AND checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
           AND ordered?(node2_var!1) AND ordered?(node3_var!1))
        IMPLIES
        ordered?(insert(x!1, node(node1_var!1, node2_var!1, node3_var!1)))

Rule? (flatten)

Applying disjunctive simplification to flatten sequent,
this simplifies to:

ordered?_insert.2 :
[-1]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-2]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
{-3} checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
{-4} checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
{-5} ordered?(node2_var!1)
{-6} ordered?(node3_var!1)
  |-------
{1} ordered?(insert(x!1, node(node1_var!1, node2_var!1, node3_var!1)))

Rule? (expand ”insert” +)

Expanding the definition of insert
this simplifies to:

ordered?_insert.2 :
[-1]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-2]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
[-3]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-4]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-5]   ordered?(node2_var!1)
[-6]   ordered?(node3_var!1)
  |-------
{1} IF x!1 <= node1_var!1
        THEN ordered?(node(node1_var!1, insert(x!1, node2_var!1), node3_var!1))
      ELSE ordered?(node(node1_var!1, node2_var!1, insert(x!1, node3_var!1)))
      ENDIF

Rule? (prop)

By propositional simplification,
this yields  2 subgoals:

ordered?_insert.2.1 :
{-1} x!1 <= node1_var!1
[-2]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-3]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
[-4]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-5]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-6]   ordered?(node2_var!1)
[-7]   ordered?(node3_var!1)
  |-------
{1} ordered?(node(node1_var!1, insert(x!1, node2_var!1), node3_var!1))

Rule? (expand ”ordered?” +)

Expanding the definition of ordered?
this simplifies to:

ordered?_insert.2.1 :
[-1]   x!1 <= node1_var!1
[-2]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-3]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
[-4]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-5]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-6]   ordered?(node2_var!1)
[-7]   ordered?(node3_var!1)
  |-------
{1} (checkall((LAMBDA (y: T): y <= node1_var!1), insert(x!1, node2_var!1))
         AND checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
           AND ordered?(insert(x!1, node2_var!1)) AND ordered?(node3_var!1))

Rule? (quant?)

Found substitution:
x gets x!1,
Instantiating quantified variables,
this simplifies to:

ordered?_insert.2.1 :
[-1]   x!1 <= node1_var!1
{-2} ordered?(node2_var!1) IMPLIES ordered?(insert(x!1, node2_var!1))
[-3]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
[-4]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-5]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-6]   ordered?(node2_var!1)
[-7]   ordered?(node3_var!1)
  |-------
[1]   (checkall((LAMBDA (y: T): y <= node1_var!1), insert(x!1, node2_var!1))
         AND checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
           AND ordered?(insert(x!1, node2_var!1)) AND ordered?(node3_var!1))

Rule? (prop)

By propositional simplification,
this simplifies to:

ordered?_insert.2.1 :
{-1} ordered?(insert(x!1, node2_var!1))
[-2]   x!1 <= node1_var!1
[-3]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
[-4]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-5]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-6]   ordered?(node2_var!1)
[-7]   ordered?(node3_var!1)
  |-------
{1} checkall((LAMBDA (y: T): y <= node1_var!1), insert(x!1, node2_var!1))

Rule? (lemma ”binary˙ tree˙ induction[T]”)

Applying binary_tree_induction[T] where
this simplifies to:

ordered?_insert.2.1 :
{-1} (FORALL (p: [binary_tree -> boolean]):
         p(leaf)
           AND
           (FORALL (node1_var: T), (node2_var: binary_tree),
                   (node3_var: binary_tree):
              p(node2_var) AND p(node3_var)
                IMPLIES p(node(node1_var, node2_var, node3_var)))
           IMPLIES (FORALL (binary_tree_var: binary_tree): p(binary_tree_var)))
[-2]   ordered?(insert(x!1, node2_var!1))
[-3]   x!1 <= node1_var!1
[-4]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
[-5]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-6]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-7]   ordered?(node2_var!1)
[-8]   ordered?(node3_var!1)
  |-------
[1]   checkall((LAMBDA (y: T): y <= node1_var!1), insert(x!1, node2_var!1))

Rule? (rewrite ”ordered?˙ insert˙ step”)

Rewriting using ordered?_insert_step,
This completes the proof of ordered?_insert.2.1.

ordered?_insert.2.2 :
[-1]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-2]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
[-3]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-4]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-5]   ordered?(node2_var!1)
[-6]   ordered?(node3_var!1)
  |-------
{1} x!1 <= node1_var!1
{2} ordered?(node(node1_var!1, node2_var!1, insert(x!1, node3_var!1)))

Rule? (expand ”ordered?” +)

Expanding the definition of ordered?
this simplifies to:

ordered?_insert.2.2 :
[-1]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-2]   (FORALL (x: T):
         ordered?(node3_var!1) IMPLIES ordered?(insert(x, node3_var!1)))
[-3]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-4]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-5]   ordered?(node2_var!1)
[-6]   ordered?(node3_var!1)
  |-------
[1]   x!1 <= node1_var!1
{2} (checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
         AND
         checkall((LAMBDA (y: T): node1_var!1 <= y), insert(x!1, node3_var!1))
           AND ordered?(node2_var!1) AND ordered?(insert(x!1, node3_var!1)))

Rule? (quant? -2)

Found substitution:
x gets x!1,
Instantiating quantified variables,
this simplifies to:

ordered?_insert.2.2 :
[-1]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
{-2} ordered?(node3_var!1) IMPLIES ordered?(insert(x!1, node3_var!1))
[-3]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-4]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-5]   ordered?(node2_var!1)
[-6]   ordered?(node3_var!1)
  |-------
[1]   x!1 <= node1_var!1
[2]   (checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
         AND
         checkall((LAMBDA (y: T): node1_var!1 <= y), insert(x!1, node3_var!1))
           AND ordered?(node2_var!1) AND ordered?(insert(x!1, node3_var!1)))

Rule? (prop)

By propositional simplification,
this simplifies to:

ordered?_insert.2.2 :
{-1} ordered?(insert(x!1, node3_var!1))
[-2]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-3]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-4]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-5]   ordered?(node2_var!1)
[-6]   ordered?(node3_var!1)
  |-------
{1} checkall((LAMBDA (y: T): node1_var!1 <= y), insert(x!1, node3_var!1))
[2]   x!1 <= node1_var!1

Rule? (rewrite ”ordered?˙ insert˙ step”)

Rewriting using ordered?_insert_step,
this simplifies to:

ordered?_insert.2.2 :
[-1]   ordered?(insert(x!1, node3_var!1))
[-2]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-3]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-4]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-5]   ordered?(node2_var!1)
[-6]   ordered?(node3_var!1)
  |-------
{1} node1_var!1 <= x!1
[2]   checkall((LAMBDA (y: T): node1_var!1 <= y), insert(x!1, node3_var!1))
[3]   x!1 <= node1_var!1

Rule? (typepred ”obt.<=”)

Adding type constraints for  obt.<=,
this simplifies to:

ordered?_insert.2.2 :
{-1} total_order?[T](obt.<=)
[-2]   ordered?(insert(x!1, node3_var!1))
[-3]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-4]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-5]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-6]   ordered?(node2_var!1)
[-7]   ordered?(node3_var!1)
  |-------
[1]   node1_var!1 <= x!1
[2]   checkall((LAMBDA (y: T): node1_var!1 <= y), insert(x!1, node3_var!1))
[3]   x!1 <= node1_var!1

Rule? (expand ”total˙ order?”)

Expanding the definition of total_order?
this simplifies to:

ordered?_insert.2.2 :
{-1} partial_order?(obt.<=) & FORALL (x, y: T): x <= y OR y <= x
[-2]   ordered?(insert(x!1, node3_var!1))
[-3]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-4]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-5]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-6]   ordered?(node2_var!1)
[-7]   ordered?(node3_var!1)
  |-------
[1]   node1_var!1 <= x!1
[2]   checkall((LAMBDA (y: T): node1_var!1 <= y), insert(x!1, node3_var!1))
[3]   x!1 <= node1_var!1

Rule? (flatten)

Applying disjunctive simplification to flatten sequent,
this simplifies to:

ordered?_insert.2.2 :
{-1} partial_order?(obt.<=)
{-2} FORALL (x, y: T): x <= y OR y <= x
[-3]   ordered?(insert(x!1, node3_var!1))
[-4]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-5]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-6]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-7]   ordered?(node2_var!1)
[-8]   ordered?(node3_var!1)
  |-------
[1]   node1_var!1 <= x!1
[2]   checkall((LAMBDA (y: T): node1_var!1 <= y), insert(x!1, node3_var!1))
[3]   x!1 <= node1_var!1

Rule? (quant?)

Found substitution:
y gets x!1,
x gets node1_var!1,
Instantiating quantified variables,
this simplifies to:

ordered?_insert.2.2 :
[-1]   partial_order?(obt.<=)
{-2} node1_var!1 <= x!1 OR x!1 <= node1_var!1
[-3]   ordered?(insert(x!1, node3_var!1))
[-4]   (FORALL (x: T):
         ordered?(node2_var!1) IMPLIES ordered?(insert(x, node2_var!1)))
[-5]   checkall((LAMBDA (y: T): y <= node1_var!1), node2_var!1)
[-6]   checkall((LAMBDA (y: T): node1_var!1 <= y), node3_var!1)
[-7]   ordered?(node2_var!1)
[-8]   ordered?(node3_var!1)
  |-------
[1]   node1_var!1 <= x!1
[2]   checkall((LAMBDA (y: T): node1_var!1 <= y), insert(x!1, node3_var!1))
[3]   x!1 <= node1_var!1

Rule? (prop)

By propositional simplification,
This completes the proof of ordered?_insert.2.2.
This completes the proof of ordered?_insert.2.
Q.E.D.
Run time  = 18.12 secs.
Real time = 356.59 secs.

binary-trees 35