Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

MSetGenTree : sets via generic trees

This module factorizes common parts in implementations of finite sets as AVL trees and as Red-Black trees. The nodes of the trees defined here include an generic information parameter, that will be the height in AVL trees and the color in Red-Black trees. Without more details here about these information parameters, trees here are not known to be well-balanced, but simply binary-search-trees.
The operations we could define and prove correct here are the one that do not build non-empty trees, but only analyze them :
Require Import FunInd Orders OrdersFacts MSetInterface PeanoNat.
Local Open Scope list_scope.
Local Open Scope lazy_bool_scope.

(* For nicer extraction, we create induction principles
   only when needed *)
Local Unset Elimination Schemes.

Module Type InfoTyp.
 Parameter t : Set.
End InfoTyp.

Ops : the pure functions

Module Type Ops (X:OrderedType)(Info:InfoTyp).

Definition elt := X.t.
Hint Transparent elt : core.

Inductive tree  : Type :=
| Leaf : tree
| Node : Info.t -> tree -> X.t -> tree -> tree.

The empty set and emptyness test

Definition empty := Leaf.

Definition is_empty t :=
 match t with
 | Leaf => true
 | _ => false
 end.

Membership test

The mem function is deciding membership. It exploits the binary search tree invariant to achieve logarithmic complexity.
Fixpoint mem x t :=
 match t with
 | Leaf => false
 | Node _ l k r =>
   match X.compare x k with
     | Lt => mem x l
     | Eq => true
     | Gt => mem x r
   end
 end.

Minimal, maximal, arbitrary elements

Fixpoint min_elt (t : tree) : option elt :=
 match t with
 | Leaf => None
 | Node _ Leaf x r => Some x
 | Node _ l x r => min_elt l
 end.

Fixpoint max_elt (t : tree) : option elt :=
  match t with
  | Leaf => None
  | Node _ l x Leaf => Some x
  | Node _ l x r => max_elt r
  end.

Definition choose := min_elt.

Iteration on elements

Fixpoint fold {A: Type} (f: elt -> A -> A) (t: tree) (base: A) : A :=
  match t with
  | Leaf => base
  | Node _ l x r => fold f r (f x (fold f l base))
 end.

Fixpoint elements_aux acc s :=
  match s with
   | Leaf => acc
   | Node _ l x r => elements_aux (x :: elements_aux acc r) l
  end.

Definition elements := elements_aux nil.

Fixpoint rev_elements_aux acc s :=
  match s with
   | Leaf => acc
   | Node _ l x r => rev_elements_aux (x :: rev_elements_aux acc l) r
  end.

Definition rev_elements := rev_elements_aux nil.

Fixpoint cardinal (s : tree) : nat :=
  match s with
   | Leaf => 0
   | Node _ l _ r => S (cardinal l + cardinal r)
  end.

Fixpoint maxdepth s :=
 match s with
 | Leaf => 0
 | Node _ l _ r => S (max (maxdepth l) (maxdepth r))
 end.

Fixpoint mindepth s :=
 match s with
 | Leaf => 0
 | Node _ l _ r => S (min (mindepth l) (mindepth r))
 end.

Testing universal or existential properties.

We do not use the standard boolean operators of Coq, but lazy ones.
Fixpoint for_all (f:elt->bool) s := match s with
  | Leaf => true
  | Node _ l x r => f x &&& for_all f l &&& for_all f r
end.

Fixpoint exists_ (f:elt->bool) s := match s with
  | Leaf => false
  | Node _ l x r => f x ||| exists_ f l ||| exists_ f r
end.

Comparison of trees

The algorithm here has been suggested by Xavier Leroy, and transformed into c.p.s. by Benjamin Grégoire. The original ocaml code (with non-structural recursive calls) has also been formalized (thanks to Function+measure), see ocaml_compare in MSetFullAVL. The following code with continuations computes dramatically faster in Coq, and should be almost as efficient after extraction.
Enumeration of the elements of a tree. This corresponds to the "samefringe" notion in the literature.
Inductive enumeration :=
 | End : enumeration
 | More : elt -> tree -> enumeration -> enumeration.
cons t e adds the elements of tree t on the head of enumeration e.
Fixpoint cons s e : enumeration :=
 match s with
  | Leaf => e
  | Node _ l x r => cons l (More x r e)
 end.
One step of comparison of elements
Definition compare_more x1 (cont:enumeration->comparison) e2 :=
 match e2 with
 | End => Gt
 | More x2 r2 e2 =>
     match X.compare x1 x2 with
      | Eq => cont (cons r2 e2)
      | Lt => Lt
      | Gt => Gt
     end
 end.
Comparison of left tree, middle element, then right tree
Fixpoint compare_cont s1 (cont:enumeration->comparison) e2 :=
 match s1 with
  | Leaf => cont e2
  | Node _ l1 x1 r1 =>
     compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2
  end.
Initial continuation
Definition compare_end e2 :=
 match e2 with End => Eq | _ => Lt end.
The complete comparison
Definition compare s1 s2 := compare_cont s1 compare_end (cons s2 End).

Definition equal s1 s2 :=
 match compare s1 s2 with Eq => true | _ => false end.

Subset test

In ocaml, recursive calls are made on "half-trees" such as (Node _ l1 x1 Leaf) and (Node _ Leaf x1 r1). Instead of these non-structural calls, we propose here two specialized functions for these situations. This version should be almost as efficient as the one of ocaml (closures as arguments may slow things a bit), it is simply less compact. The exact ocaml version has also been formalized (thanks to Function+measure), see ocaml_subset in MSetFullAVL.
Fixpoint subsetl (subset_l1 : tree -> bool) x1 s2 : bool :=
 match s2 with
  | Leaf => false
  | Node _ l2 x2 r2 =>
     match X.compare x1 x2 with
      | Eq => subset_l1 l2
      | Lt => subsetl subset_l1 x1 l2
      | Gt => mem x1 r2 &&& subset_l1 s2
     end
 end.

Fixpoint subsetr (subset_r1 : tree -> bool) x1 s2 : bool :=
 match s2 with
  | Leaf => false
  | Node _ l2 x2 r2 =>
     match X.compare x1 x2 with
      | Eq => subset_r1 r2
      | Lt => mem x1 l2 &&& subset_r1 s2
      | Gt => subsetr subset_r1 x1 r2
     end
 end.

Fixpoint subset s1 s2 : bool := match s1, s2 with
  | Leaf, _ => true
  | Node _ _ _ _, Leaf => false
  | Node _ l1 x1 r1, Node _ l2 x2 r2 =>
     match X.compare x1 x2 with
      | Eq => subset l1 l2 &&& subset r1 r2
      | Lt => subsetl (subset l1) x1 l2 &&& subset r1 s2
      | Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2
     end
 end.

End Ops.

Props : correctness proofs of these generic operations

Module Type Props (X:OrderedType)(Info:InfoTyp)(Import M:Ops X Info).

Occurrence in a tree

Inductive InT (x : elt) : tree -> Prop :=
  | IsRoot : forall c l r y, X.eq x y -> InT x (Node c l y r)
  | InLeft : forall c l r y, InT x l -> InT x (Node c l y r)
  | InRight : forall c l r y, InT x r -> InT x (Node c l y r).

Definition In := InT.

Some shortcuts

Definition Equal s s' := forall a : elt, InT a s <-> InT a s'.
Definition Subset s s' := forall a : elt, InT a s -> InT a s'.
Definition Empty s := forall a : elt, ~ InT a s.
Definition For_all (P : elt -> Prop) s := forall x, InT x s -> P x.
Definition Exists (P : elt -> Prop) s := exists x, InT x s /\ P x.

Binary search trees

lt_tree x s: all elements in s are smaller than x (resp. greater for gt_tree)
Definition lt_tree x s := forall y, InT y s -> X.lt y x.
Definition gt_tree x s := forall y, InT y s -> X.lt x y.
bst t : t is a binary search tree
Inductive bst : tree -> Prop :=
  | BSLeaf : bst Leaf
  | BSNode : forall c x l r, bst l -> bst r ->
     lt_tree x l -> gt_tree x r -> bst (Node c l x r).
bst is the (decidable) invariant our trees will have to satisfy.
Definition IsOk := bst.

Class Ok (s:tree) : Prop := ok : bst s.

Instance bst_Ok s (Hs : bst s) : Ok s := { ok := Hs }.

Fixpoint ltb_tree x s :=
 match s with
  | Leaf => true
  | Node _ l y r =>
     match X.compare x y with
      | Gt => ltb_tree x l && ltb_tree x r
      | _ => false
     end
 end.

Fixpoint gtb_tree x s :=
 match s with
  | Leaf => true
  | Node _ l y r =>
     match X.compare x y with
      | Lt => gtb_tree x l && gtb_tree x r
      | _ => false
     end
 end.

Fixpoint isok s :=
 match s with
  | Leaf => true
  | Node _  l x r => isok l && isok r && ltb_tree x l && gtb_tree x r
 end.

Known facts about ordered types

Module Import MX := OrderedTypeFacts X.

Automation and dedicated tactics

Scheme tree_ind := Induction for tree Sort Prop.
Scheme bst_ind := Induction for bst Sort Prop.

Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core.
Local Hint Immediate MX.eq_sym : core.
Local Hint Unfold In lt_tree gt_tree : core.
Local Hint Constructors InT bst : core.
Local Hint Unfold Ok : core.
Automatic treatment of Ok hypothesis
Ltac clear_inversion H := inversion H; clear H; subst.

Ltac inv_ok := match goal with
 | H:Ok (Node _ _ _ _) |- _ => clear_inversion H; inv_ok
 | H:Ok Leaf |- _ => clear H; inv_ok
 | H:bst ?x |- _ => change (Ok x) in H; inv_ok
 | _ => idtac
end.
A tactic to repeat inversion_clear on all hyps of the form (f (Node _ _ _ _))
Ltac is_tree_constr c :=
  match c with
   | Leaf => idtac
   | Node _ _ _ _ => idtac
   | _ => fail
  end.

Ltac invtree f :=
  match goal with
     | H:f ?s |- _ => is_tree_constr s; clear_inversion H; invtree f
     | H:f _ ?s |- _ => is_tree_constr s; clear_inversion H; invtree f
     | H:f _ _ ?s |- _ => is_tree_constr s; clear_inversion H; invtree f
     | _ => idtac
  end.

Ltac inv := inv_ok; invtree InT.

Ltac intuition_in := repeat (intuition; inv).
Helper tactic concerning order of elements.
Ltac order := match goal with
 | U: lt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
 | U: gt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
 | _ => MX.order
end.
isok is indeed a decision procedure for Ok

forall (x : X.t) (s : tree), lt_tree x s <-> ltb_tree x s = true

forall (x : X.t) (s : tree), lt_tree x s <-> ltb_tree x s = true
x:X.t

lt_tree x Leaf <-> true = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
lt_tree x (Node c l y r) <-> match X.compare x y with | Gt => ltb_tree x l && ltb_tree x r | _ => false end = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true

lt_tree x (Node c l y r) <-> match X.compare x y with | Gt => ltb_tree x l && ltb_tree x r | _ => false end = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.eq x y

lt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt x y
lt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt y x
lt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.eq x y
H0:lt_tree x (Node c l y r)

false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt x y
lt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt y x
lt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.eq x y
H0:lt_tree x (Node c l y r)
H1:X.lt y x

false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt x y
lt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt y x
lt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt x y

lt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt y x
lt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt x y
H0:lt_tree x (Node c l y r)

false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt y x
lt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt x y
H0:lt_tree x (Node c l y r)
H1:X.lt y x

false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt y x
lt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt y x

lt_tree x (Node c l y r) <-> ltb_tree x l && ltb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:lt_tree x l <-> ltb_tree x l = true
IHr:lt_tree x r <-> ltb_tree x r = true
H:X.lt y x

lt_tree x (Node c l y r) <-> lt_tree x l /\ lt_tree x r
unfold lt_tree; intuition_in; order. Qed.

forall (x : X.t) (s : tree), gt_tree x s <-> gtb_tree x s = true

forall (x : X.t) (s : tree), gt_tree x s <-> gtb_tree x s = true
x:X.t

gt_tree x Leaf <-> true = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
gt_tree x (Node c l y r) <-> match X.compare x y with | Lt => gtb_tree x l && gtb_tree x r | _ => false end = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true

gt_tree x (Node c l y r) <-> match X.compare x y with | Lt => gtb_tree x l && gtb_tree x r | _ => false end = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.eq x y

gt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt x y
gt_tree x (Node c l y r) <-> gtb_tree x l && gtb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt y x
gt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.eq x y
H0:gt_tree x (Node c l y r)

false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt x y
gt_tree x (Node c l y r) <-> gtb_tree x l && gtb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt y x
gt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.eq x y
H0:gt_tree x (Node c l y r)
H1:X.lt x y

false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt x y
gt_tree x (Node c l y r) <-> gtb_tree x l && gtb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt y x
gt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt x y

gt_tree x (Node c l y r) <-> gtb_tree x l && gtb_tree x r = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt y x
gt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt x y

gt_tree x (Node c l y r) <-> gt_tree x l /\ gt_tree x r
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt y x
gt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt y x

gt_tree x (Node c l y r) <-> false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt y x
H0:gt_tree x (Node c l y r)

false = true
x:X.t
c:Info.t
l:tree
y:X.t
r:tree
IHl:gt_tree x l <-> gtb_tree x l = true
IHr:gt_tree x r <-> gtb_tree x r = true
H:X.lt y x
H0:gt_tree x (Node c l y r)
H1:X.lt x y

false = true
order. Qed.

forall s : tree, Ok s <-> isok s = true

forall s : tree, Ok s <-> isok s = true

Ok Leaf <-> true = true
c:Info.t
l:tree
y:X.t
r:tree
IHl:Ok l <-> isok l = true
IHr:Ok r <-> isok r = true
Ok (Node c l y r) <-> isok l && isok r && ltb_tree y l && gtb_tree y r = true
c:Info.t
l:tree
y:X.t
r:tree
IHl:Ok l <-> isok l = true
IHr:Ok r <-> isok r = true

Ok (Node c l y r) <-> isok l && isok r && ltb_tree y l && gtb_tree y r = true
c:Info.t
l:tree
y:X.t
r:tree
IHl:Ok l <-> isok l = true
IHr:Ok r <-> isok r = true

Ok (Node c l y r) <-> ((Ok l /\ Ok r) /\ lt_tree y l) /\ gt_tree y r
intuition_in. Qed.
s:tree

isok s = true -> Ok s
s:tree

isok s = true -> Ok s
intros; apply <- isok_iff; auto. Qed.

Basic results about In


forall (s : tree) (x y : X.t), X.eq x y -> InT x s -> InT y s

forall (s : tree) (x y : X.t), X.eq x y -> InT x s -> InT y s
induction s; simpl; intuition_in; eauto. Qed. Local Hint Immediate In_1 : core.

Proper (X.eq ==> eq ==> iff) InT

Proper (X.eq ==> eq ==> iff) InT

Proper (X.eq ==> eq ==> impl) InT
x, y:X.t
H:X.eq x y
y0:tree
H1:InT x y0

InT y y0
apply In_1 with x; auto. Qed.

forall (c : Info.t) (l : tree) (x : X.t) (r : tree) (y : elt), InT y (Node c l x r) <-> InT y l \/ X.eq y x \/ InT y r

forall (c : Info.t) (l : tree) (x : X.t) (r : tree) (y : elt), InT y (Node c l x r) <-> InT y l \/ X.eq y x \/ InT y r
intuition_in. Qed.

forall x : elt, InT x Leaf <-> False

forall x : elt, InT x Leaf <-> False
intuition_in. Qed.
Results about lt_tree and gt_tree

forall x : elt, lt_tree x Leaf

forall x : elt, lt_tree x Leaf
red; inversion 1. Qed.

forall x : elt, gt_tree x Leaf

forall x : elt, gt_tree x Leaf
red; inversion 1. Qed.

forall (x y : elt) (l r : tree) (i : Info.t), lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node i l y r)

forall (x y : elt) (l r : tree) (i : Info.t), lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node i l y r)
unfold lt_tree; intuition_in; order. Qed.

forall (x y : elt) (l r : tree) (i : Info.t), gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node i l y r)

forall (x y : elt) (l r : tree) (i : Info.t), gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node i l y r)
unfold gt_tree; intuition_in; order. Qed. Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.

forall (x : elt) (t : tree), lt_tree x t -> ~ InT x t

forall (x : elt) (t : tree), lt_tree x t -> ~ InT x t
intros; intro; order. Qed.

forall x y : X.t, X.lt x y -> forall t : tree, lt_tree x t -> lt_tree y t

forall x y : X.t, X.lt x y -> forall t : tree, lt_tree x t -> lt_tree y t
eauto. Qed.

forall (x : elt) (t : tree), gt_tree x t -> ~ InT x t

forall (x : elt) (t : tree), gt_tree x t -> ~ InT x t
intros; intro; order. Qed.

forall x y : X.t, X.lt y x -> forall t : tree, gt_tree x t -> gt_tree y t

forall x y : X.t, X.lt y x -> forall t : tree, gt_tree x t -> gt_tree y t
eauto. Qed.

Proper (X.eq ==> eq ==> iff) lt_tree

Proper (X.eq ==> eq ==> iff) lt_tree

Proper (X.eq ==> eq ==> impl) lt_tree
x, x':X.t
Hx:X.eq x x'
s, s':tree
Hs:s = s'
H:lt_tree x s
y:elt
Hy:InT y s'

X.lt y x'
x, x':X.t
Hx:X.eq x x'
s':tree
H:lt_tree x s'
y:elt
Hy:InT y s'

X.lt y x'
setoid_rewrite <- Hx; auto. Qed.

Proper (X.eq ==> eq ==> iff) gt_tree

Proper (X.eq ==> eq ==> iff) gt_tree

Proper (X.eq ==> eq ==> impl) gt_tree
x, x':X.t
Hx:X.eq x x'
s, s':tree
Hs:s = s'
H:gt_tree x s
y:elt
Hy:InT y s'

X.lt x' y
x, x':X.t
Hx:X.eq x x'
s':tree
H:gt_tree x s'
y:elt
Hy:InT y s'

X.lt x' y
setoid_rewrite <- Hx; auto. Qed. Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. Ltac induct s x := induction s as [|i l IHl x' r IHr]; simpl; intros; [|elim_compare x x'; intros; inv]. Ltac auto_tc := auto with typeclass_instances. Ltac ok := inv; change bst with Ok in *; match goal with | |- Ok (Node _ _ _ _) => constructor; auto_tc; ok | |- lt_tree _ (Node _ _ _ _) => apply lt_tree_node; ok | |- gt_tree _ (Node _ _ _ _) => apply gt_tree_node; ok | _ => eauto with typeclass_instances end.

Empty set


Empty empty

Empty empty
x:elt
H:InT x empty

False
inversion H. Qed.

Ok empty

Ok empty
auto. Qed.

Emptyness test


forall s : tree, is_empty s = true <-> Empty s

forall s : tree, is_empty s = true <-> Empty s

true = true <-> Empty Leaf
c:Info.t
r:tree
x:X.t
l:tree
false = true <-> Empty (Node c r x l)

true = true <-> Empty Leaf

true = true -> Empty Leaf
x:elt
H:InT x Leaf

False
inv.
c:Info.t
r:tree
x:X.t
l:tree

false = true <-> Empty (Node c r x l)
c:Info.t
r:tree
x:X.t
l:tree

false = true -> Empty (Node c r x l)
c:Info.t
r:tree
x:X.t
l:tree
Empty (Node c r x l) -> false = true
c:Info.t
r:tree
x:X.t
l:tree

Empty (Node c r x l) -> false = true
intro H; elim (H x); auto. Qed.

Membership


forall (s : tree) (x : X.t), Ok s -> mem x s = true <-> InT x s

forall (s : tree) (x : X.t), Ok s -> mem x s = true <-> InT x s
s:tree
x:X.t
H:Ok s

mem x s = true -> InT x s
s:tree
x:X.t
H:Ok s
InT x s -> mem x s = true
s:tree
x:X.t
H:Ok s

mem x s = true -> InT x s
induct s x; now auto.
s:tree
x:X.t
H:Ok s

InT x s -> mem x s = true
induct s x; intuition_in; order. Qed.

Minimal and maximal elements

Functional Scheme min_elt_ind := Induction for min_elt Sort Prop.
Functional Scheme max_elt_ind := Induction for max_elt Sort Prop.

s:tree
x:elt

min_elt s = Some x -> InT x s
s:tree
x:elt

min_elt s = Some x -> InT x s
functional induction (min_elt s); auto; inversion 1; auto. Qed.
s:tree
x, y:elt
H:Ok s

min_elt s = Some x -> InT y s -> ~ X.lt y x
s:tree
x, y:elt
H:Ok s

min_elt s = Some x -> InT y s -> ~ X.lt y x
s:tree
x:elt
H:Ok s

forall y : elt, min_elt s = Some x -> InT y s -> ~ X.lt y x
x:elt
H:Ok Leaf

forall y : elt, None = Some x -> InT y Leaf -> ~ X.lt y x
x:elt
_x:Info.t
x0:X.t
r:tree
H:Ok (Node _x Leaf x0 r)
forall y : elt, Some x0 = Some x -> InT y (Node _x Leaf x0 r) -> ~ X.lt y x
x:elt
_x:Info.t
x0:X.t
r:tree
_x1:Info.t
l1:tree
x1:X.t
r1:tree
H:Ok (Node _x (Node _x1 l1 x1 r1) x0 r)
IHo:Ok (Node _x1 l1 x1 r1) -> forall y : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x1 l1 x1 r1) -> ~ X.lt y x
forall y : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x (Node _x1 l1 x1 r1) x0 r) -> ~ X.lt y x
x:elt
H:Ok Leaf

forall y : elt, None = Some x -> InT y Leaf -> ~ X.lt y x
discriminate.
x:elt
_x:Info.t
x0:X.t
r:tree
H:Ok (Node _x Leaf x0 r)

forall y : elt, Some x0 = Some x -> InT y (Node _x Leaf x0 r) -> ~ X.lt y x
x:elt
_x:Info.t
x0:X.t
r:tree
H:Ok (Node _x Leaf x0 r)
y:elt
V:Some x0 = Some x
W:InT y (Node _x Leaf x0 r)

~ X.lt y x
x:elt
_x:Info.t
r:tree
H:Ok (Node _x Leaf x r)
y:elt
W:InT y (Node _x Leaf x r)

~ X.lt y x
inv; order.
x:elt
_x:Info.t
x0:X.t
r:tree
_x1:Info.t
l1:tree
x1:X.t
r1:tree
H:Ok (Node _x (Node _x1 l1 x1 r1) x0 r)
IHo:Ok (Node _x1 l1 x1 r1) -> forall y : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x1 l1 x1 r1) -> ~ X.lt y x

forall y : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x (Node _x1 l1 x1 r1) x0 r) -> ~ X.lt y x
x:elt
_x:Info.t
x0:X.t
r:tree
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 x
y:elt
H0:min_elt (Node _x1 l1 x1 r1) = Some x
H7:Ok r
H8:lt_tree x0 (Node _x1 l1 x1 r1)
H9:gt_tree x0 r
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:X.eq y x0

~ X.lt y x
x:elt
_x:Info.t
x0:X.t
r:tree
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 x
y:elt
H0:min_elt (Node _x1 l1 x1 r1) = Some x
H7:Ok r
H8:lt_tree x0 (Node _x1 l1 x1 r1)
H9:gt_tree x0 r
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:InT y r
~ X.lt y x
x:elt
_x:Info.t
x0:X.t
r:tree
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 x
y:elt
H0:min_elt (Node _x1 l1 x1 r1) = Some x
H7:Ok r
H8:lt_tree x0 (Node _x1 l1 x1 r1)
H9:gt_tree x0 r
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:X.eq y x0

~ X.lt y x
x:elt
_x:Info.t
x0:X.t
r:tree
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 x
y:elt
H0:min_elt (Node _x1 l1 x1 r1) = Some x
H7:Ok r
H8:lt_tree x0 (Node _x1 l1 x1 r1)
H9:gt_tree x0 r
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:X.eq y x0
H:X.lt x x0

~ X.lt y x
order.
x:elt
_x:Info.t
x0:X.t
r:tree
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 x
y:elt
H0:min_elt (Node _x1 l1 x1 r1) = Some x
H7:Ok r
H8:lt_tree x0 (Node _x1 l1 x1 r1)
H9:gt_tree x0 r
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:InT y r

~ X.lt y x
x:elt
_x:Info.t
x0:X.t
r:tree
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 x
y:elt
H0:min_elt (Node _x1 l1 x1 r1) = Some x
H7:Ok r
H8:lt_tree x0 (Node _x1 l1 x1 r1)
H9:gt_tree x0 r
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:InT y r
H:X.lt x1 x0

~ X.lt y x
x:elt
_x:Info.t
x0:X.t
r:tree
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, min_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt y0 x
y:elt
H0:min_elt (Node _x1 l1 x1 r1) = Some x
H7:Ok r
H8:lt_tree x0 (Node _x1 l1 x1 r1)
H9:gt_tree x0 r
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:InT y r
H:X.lt x1 x0
H1:~ X.lt x1 x

~ X.lt y x
order. Qed.
s:tree

min_elt s = None -> Empty s
s:tree

min_elt s = None -> Empty s

None = None -> Empty Leaf
_x:Info.t
x:X.t
_x0:tree
Some x = None -> Empty (Node _x Leaf x _x0)
_x:Info.t
x:X.t
_x0:tree
_x1:Info.t
_x2:tree
_x3:X.t
_x4:tree
IHo:min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)
min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x (Node _x1 _x2 _x3 _x4) x _x0)
_x:Info.t
x:X.t
_x0:tree

Some x = None -> Empty (Node _x Leaf x _x0)
_x:Info.t
x:X.t
_x0:tree
_x1:Info.t
_x2:tree
_x3:X.t
_x4:tree
IHo:min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)
min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x (Node _x1 _x2 _x3 _x4) x _x0)
_x:Info.t
x:X.t
_x0:tree
_x1:Info.t
_x2:tree
_x3:X.t
_x4:tree
IHo:min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)

min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x (Node _x1 _x2 _x3 _x4) x _x0)
_x:Info.t
x:X.t
_x0:tree
_x1:Info.t
_x2:tree
_x3:X.t
_x4:tree
IHo:min_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)
H0:min_elt (Node _x1 _x2 _x3 _x4) = None

Empty (Node _x (Node _x1 _x2 _x3 _x4) x _x0)
destruct (IHo H0 _x3); auto. Qed.
s:tree
x:elt

max_elt s = Some x -> InT x s
s:tree
x:elt

max_elt s = Some x -> InT x s
functional induction (max_elt s); auto; inversion 1; auto. Qed.
s:tree
x, y:elt
H:Ok s

max_elt s = Some x -> InT y s -> ~ X.lt x y
s:tree
x, y:elt
H:Ok s

max_elt s = Some x -> InT y s -> ~ X.lt x y
s:tree
x:elt
H:Ok s

forall y : elt, max_elt s = Some x -> InT y s -> ~ X.lt x y
x:elt
H:Ok Leaf

forall y : elt, None = Some x -> InT y Leaf -> ~ X.lt x y
x:elt
_x:Info.t
r:tree
x0:X.t
H:Ok (Node _x r x0 Leaf)
forall y : elt, Some x0 = Some x -> InT y (Node _x r x0 Leaf) -> ~ X.lt x y
x:elt
_x:Info.t
r:tree
x0:X.t
_x1:Info.t
l1:tree
x1:X.t
r1:tree
H:Ok (Node _x r x0 (Node _x1 l1 x1 r1))
IHo:Ok (Node _x1 l1 x1 r1) -> forall y : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x1 l1 x1 r1) -> ~ X.lt x y
forall y : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x r x0 (Node _x1 l1 x1 r1)) -> ~ X.lt x y
x:elt
H:Ok Leaf

forall y : elt, None = Some x -> InT y Leaf -> ~ X.lt x y
discriminate.
x:elt
_x:Info.t
r:tree
x0:X.t
H:Ok (Node _x r x0 Leaf)

forall y : elt, Some x0 = Some x -> InT y (Node _x r x0 Leaf) -> ~ X.lt x y
x:elt
_x:Info.t
r:tree
x0:X.t
H:Ok (Node _x r x0 Leaf)
y:elt
V:Some x0 = Some x
W:InT y (Node _x r x0 Leaf)

~ X.lt x y
x:elt
_x:Info.t
r:tree
H:Ok (Node _x r x Leaf)
y:elt
W:InT y (Node _x r x Leaf)

~ X.lt x y
inv; order.
x:elt
_x:Info.t
r:tree
x0:X.t
_x1:Info.t
l1:tree
x1:X.t
r1:tree
H:Ok (Node _x r x0 (Node _x1 l1 x1 r1))
IHo:Ok (Node _x1 l1 x1 r1) -> forall y : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x1 l1 x1 r1) -> ~ X.lt x y

forall y : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y (Node _x r x0 (Node _x1 l1 x1 r1)) -> ~ X.lt x y
x:elt
_x:Info.t
r:tree
x0:X.t
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0
y:elt
H0:max_elt (Node _x1 l1 x1 r1) = Some x
H6:Ok r
H8:lt_tree x0 r
H9:gt_tree x0 (Node _x1 l1 x1 r1)
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:X.eq y x0

~ X.lt x y
x:elt
_x:Info.t
r:tree
x0:X.t
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0
y:elt
H0:max_elt (Node _x1 l1 x1 r1) = Some x
H6:Ok r
H8:lt_tree x0 r
H9:gt_tree x0 (Node _x1 l1 x1 r1)
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:InT y r
~ X.lt x y
x:elt
_x:Info.t
r:tree
x0:X.t
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0
y:elt
H0:max_elt (Node _x1 l1 x1 r1) = Some x
H6:Ok r
H8:lt_tree x0 r
H9:gt_tree x0 (Node _x1 l1 x1 r1)
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:X.eq y x0

~ X.lt x y
x:elt
_x:Info.t
r:tree
x0:X.t
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0
y:elt
H0:max_elt (Node _x1 l1 x1 r1) = Some x
H6:Ok r
H8:lt_tree x0 r
H9:gt_tree x0 (Node _x1 l1 x1 r1)
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:X.eq y x0
H:X.lt x0 x

~ X.lt x y
order.
x:elt
_x:Info.t
r:tree
x0:X.t
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0
y:elt
H0:max_elt (Node _x1 l1 x1 r1) = Some x
H6:Ok r
H8:lt_tree x0 r
H9:gt_tree x0 (Node _x1 l1 x1 r1)
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:InT y r

~ X.lt x y
x:elt
_x:Info.t
r:tree
x0:X.t
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0
y:elt
H0:max_elt (Node _x1 l1 x1 r1) = Some x
H6:Ok r
H8:lt_tree x0 r
H9:gt_tree x0 (Node _x1 l1 x1 r1)
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:InT y r
H:X.lt x0 x1

~ X.lt x y
x:elt
_x:Info.t
r:tree
x0:X.t
_x1:Info.t
l1:tree
x1:X.t
r1:tree
IHo:Ok (Node _x1 l1 x1 r1) -> forall y0 : elt, max_elt (Node _x1 l1 x1 r1) = Some x -> InT y0 (Node _x1 l1 x1 r1) -> ~ X.lt x y0
y:elt
H0:max_elt (Node _x1 l1 x1 r1) = Some x
H6:Ok r
H8:lt_tree x0 r
H9:gt_tree x0 (Node _x1 l1 x1 r1)
H5:Ok l1
H10:Ok r1
H11:lt_tree x1 l1
H12:gt_tree x1 r1
H2:InT y r
H:X.lt x0 x1
H1:~ X.lt x x1

~ X.lt x y
order. Qed.
s:tree

max_elt s = None -> Empty s
s:tree

max_elt s = None -> Empty s

None = None -> Empty Leaf
_x:Info.t
_x0:tree
x:X.t
Some x = None -> Empty (Node _x _x0 x Leaf)
_x:Info.t
_x0:tree
x:X.t
_x1:Info.t
_x2:tree
_x3:X.t
_x4:tree
IHo:max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)
max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x _x0 x (Node _x1 _x2 _x3 _x4))
_x:Info.t
_x0:tree
x:X.t

Some x = None -> Empty (Node _x _x0 x Leaf)
_x:Info.t
_x0:tree
x:X.t
_x1:Info.t
_x2:tree
_x3:X.t
_x4:tree
IHo:max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)
max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x _x0 x (Node _x1 _x2 _x3 _x4))
_x:Info.t
_x0:tree
x:X.t
_x1:Info.t
_x2:tree
_x3:X.t
_x4:tree
IHo:max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)

max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x _x0 x (Node _x1 _x2 _x3 _x4))
_x:Info.t
_x0:tree
x:X.t
_x1:Info.t
_x2:tree
_x3:X.t
_x4:tree
IHo:max_elt (Node _x1 _x2 _x3 _x4) = None -> Empty (Node _x1 _x2 _x3 _x4)
H0:max_elt (Node _x1 _x2 _x3 _x4) = None

Empty (Node _x _x0 x (Node _x1 _x2 _x3 _x4))
destruct (IHo H0 _x3); auto. Qed.

forall (s : tree) (x : elt), choose s = Some x -> InT x s

forall (s : tree) (x : elt), choose s = Some x -> InT x s
exact min_elt_spec1. Qed.

forall s : tree, choose s = None -> Empty s

forall s : tree, choose s = None -> Empty s
exact min_elt_spec3. Qed.

forall (s s' : tree) (x x' : elt), Ok s -> Ok s' -> choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'

forall (s s' : tree) (x x' : elt), Ok s -> Ok s' -> choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'

X.eq x x'
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'

~ X.lt x x'
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'
H0:~ X.lt x x'
X.eq x x'
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'

InT x s'
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'
H0:~ X.lt x x'
X.eq x x'
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'
H0:~ X.lt x x'

X.eq x x'
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'
H0:~ X.lt x x'

~ X.lt x' x
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'
H0:~ X.lt x x'
H1:~ X.lt x' x
X.eq x x'
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'
H0:~ X.lt x x'

InT x' s
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'
H0:~ X.lt x x'
H1:~ X.lt x' x
X.eq x x'
s, s':tree
x, x':elt
Hb:Ok s
Hb':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:forall a : elt, InT a s <-> InT a s'
H0:~ X.lt x x'
H1:~ X.lt x' x

X.eq x x'
elim_compare x x'; intuition. Qed.

Elements


forall (s : tree) (acc : list X.t) (x : X.t), InA X.eq x (elements_aux acc s) <-> InT x s \/ InA X.eq x acc

forall (s : tree) (acc : list X.t) (x : X.t), InA X.eq x (elements_aux acc s) <-> InT x s \/ InA X.eq x acc

forall (acc : list X.t) (x : X.t), InA X.eq x acc <-> InT x Leaf \/ InA X.eq x acc
c:Info.t
l:tree
x:X.t
r:tree
Hl:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc l) <-> InT x0 l \/ InA X.eq x0 acc
Hr:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc r) <-> InT x0 r \/ InA X.eq x0 acc
forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux (x :: elements_aux acc r) l) <-> InT x0 (Node c l x r) \/ InA X.eq x0 acc
acc:list X.t
x:X.t
H0:InT x Leaf

InA X.eq x acc
c:Info.t
l:tree
x:X.t
r:tree
Hl:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc l) <-> InT x0 l \/ InA X.eq x0 acc
Hr:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc r) <-> InT x0 r \/ InA X.eq x0 acc
forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux (x :: elements_aux acc r) l) <-> InT x0 (Node c l x r) \/ InA X.eq x0 acc
c:Info.t
l:tree
x:X.t
r:tree
Hl:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc l) <-> InT x0 l \/ InA X.eq x0 acc
Hr:forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux acc r) <-> InT x0 r \/ InA X.eq x0 acc

forall (acc : list X.t) (x0 : X.t), InA X.eq x0 (elements_aux (x :: elements_aux acc r) l) <-> InT x0 (Node c l x r) \/ InA X.eq x0 acc
c:Info.t
l:tree
x:X.t
r:tree
Hl:forall (acc0 : list X.t) (x1 : X.t), InA X.eq x1 (elements_aux acc0 l) <-> InT x1 l \/ InA X.eq x1 acc0
Hr:forall (acc0 : list X.t) (x1 : X.t), InA X.eq x1 (elements_aux acc0 r) <-> InT x1 r \/ InA X.eq x1 acc0
acc:list X.t
x0:X.t

InA X.eq x0 (elements_aux (x :: elements_aux acc r) l) <-> InT x0 (Node c l x r) \/ InA X.eq x0 acc
c:Info.t
l:tree
x:X.t
r:tree
Hl:forall (acc0 : list X.t) (x1 : X.t), InA X.eq x1 (elements_aux acc0 l) <-> InT x1 l \/ InA X.eq x1 acc0
Hr:forall (acc0 : list X.t) (x1 : X.t), InA X.eq x1 (elements_aux acc0 r) <-> InT x1 r \/ InA X.eq x1 acc0
acc:list X.t
x0:X.t

InT x0 l \/ InA X.eq x0 (x :: elements_aux acc r) <-> InT x0 (Node c l x r) \/ InA X.eq x0 acc
c:Info.t
l:tree
x:X.t
r:tree
acc:list X.t
x0:X.t
H:InA X.eq x0 (elements_aux acc r) -> InT x0 r \/ InA X.eq x0 acc
H0:InT x0 r \/ InA X.eq x0 acc -> InA X.eq x0 (elements_aux acc r)

InT x0 l \/ InA X.eq x0 (x :: elements_aux acc r) <-> InT x0 (Node c l x r) \/ InA X.eq x0 acc
intuition; inversion_clear H3; intuition. Qed.

forall (s : tree) (x : X.t), InA X.eq x (elements s) <-> InT x s

forall (s : tree) (x : X.t), InA X.eq x (elements s) <-> InT x s
s:tree
x:X.t
H:InT x s -> InA X.eq x (elements_aux nil s)
H1:InA X.eq x (elements s)
H0:InA X.eq x nil
H3:InA X.eq x (elements_aux nil s)

InT x s
inversion_clear H0. Qed.

forall (s : tree) (acc : list X.t), Ok s -> Sorted X.lt acc -> (forall x y : elt, InA X.eq x acc -> InT y s -> X.lt y x) -> Sorted X.lt (elements_aux acc s)

forall (s : tree) (acc : list X.t), Ok s -> Sorted X.lt acc -> (forall x y : elt, InA X.eq x acc -> InT y s -> X.lt y x) -> Sorted X.lt (elements_aux acc s)
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H:Ok (Node c l y r)
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x

Sorted X.lt (elements_aux (y :: elements_aux acc r) l)
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r

Sorted X.lt (elements_aux (y :: elements_aux acc r) l)
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r

Sorted X.lt (y :: elements_aux acc r)
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
forall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 x
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r

Sorted X.lt (elements_aux acc r)
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
HdRel X.lt y (elements_aux acc r)
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
forall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 x
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r

HdRel X.lt y (elements_aux acc r)
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
forall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 x
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r

forall y0 : X.t, InA OrderTac.TO.eq y0 (elements_aux acc r) -> X.lt y y0
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
forall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 x
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y1 : elt, InA X.eq x acc0 -> InT y1 l -> X.lt y1 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y1 : elt, InA X.eq x acc0 -> InT y1 r -> X.lt y1 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y1 : elt, InA X.eq x acc -> InT y1 (Node c l y r) -> X.lt y1 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
y0:X.t
H:InA OrderTac.TO.eq y0 (elements_aux acc r)

X.lt y y0
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
forall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 x
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 l -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x y0 : elt, InA X.eq x acc0 -> InT y0 r -> X.lt y0 x) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x y0 : elt, InA X.eq x acc -> InT y0 (Node c l y r) -> X.lt y0 x
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r

forall x y0 : elt, InA X.eq x (y :: elements_aux acc r) -> InT y0 l -> X.lt y0 x
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 l -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 r -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x0 y1 : elt, InA X.eq x0 acc -> InT y1 (Node c l y r) -> X.lt y1 x0
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
x, y0:elt
H:InA X.eq x (y :: elements_aux acc r)
H2:InT y0 l

X.lt y0 x
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 l -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 r -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x0 y1 : elt, InA X.eq x0 acc -> InT y1 (Node c l y r) -> X.lt y1 x0
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
x, y0:elt
H2:InT y0 l
H3:X.eq x y

X.lt y0 x
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 l -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 r -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x0 y1 : elt, InA X.eq x0 acc -> InT y1 (Node c l y r) -> X.lt y1 x0
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
x, y0:elt
H2:InT y0 l
H3:InA X.eq x (elements_aux acc r)
X.lt y0 x
c:Info.t
l:tree
y:X.t
r:tree
Hl:forall acc0 : list X.t, Ok l -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 l -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 l)
Hr:forall acc0 : list X.t, Ok r -> Sorted X.lt acc0 -> (forall x0 y1 : elt, InA X.eq x0 acc0 -> InT y1 r -> X.lt y1 x0) -> Sorted X.lt (elements_aux acc0 r)
acc:list X.t
H0:Sorted X.lt acc
H1:forall x0 y1 : elt, InA X.eq x0 acc -> InT y1 (Node c l y r) -> X.lt y1 x0
H6:Ok l
H7:Ok r
H8:lt_tree y l
H9:gt_tree y r
x, y0:elt
H2:InT y0 l
H3:InA X.eq x (elements_aux acc r)

X.lt y0 x
destruct (elements_spec1' r acc x); intuition eauto. Qed.

forall s : tree, Ok s -> Sorted X.lt (elements s)

forall s : tree, Ok s -> Sorted X.lt (elements s)
s:tree
H:Ok s

forall x y : elt, InA X.eq x nil -> InT y s -> X.lt y x
intros; inversion H0. Qed. Local Hint Resolve elements_spec2 : core.

forall s : tree, Ok s -> NoDupA X.eq (elements s)

forall s : tree, Ok s -> NoDupA X.eq (elements s)
s:tree
H:Ok s

NoDupA X.eq (elements s)
eapply SortA_NoDupA; eauto with *. Qed.

forall (s : tree) (acc : list X.t), length acc + cardinal s = length (elements_aux acc s)

forall (s : tree) (acc : list X.t), length acc + cardinal s = length (elements_aux acc s)
s:tree
t:Info.t
t0:tree
H:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)
t1:X.t
t2:tree
H0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)
acc:list X.t

length acc + S (cardinal t0 + cardinal t2) = length (elements_aux (t1 :: elements_aux acc t2) t0)
s:tree
t:Info.t
t0:tree
H:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)
t1:X.t
t2:tree
H0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)
acc:list X.t

length acc + S (cardinal t0 + cardinal t2) = length (t1 :: elements_aux acc t2) + cardinal t0
s:tree
t:Info.t
t0:tree
H:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)
t1:X.t
t2:tree
H0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)
acc:list X.t

length acc + S (cardinal t0 + cardinal t2) = S (length (elements_aux acc t2) + cardinal t0)
s:tree
t:Info.t
t0:tree
H:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)
t1:X.t
t2:tree
H0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)
acc:list X.t

length acc + S (cardinal t0 + cardinal t2) = S (length acc + cardinal t2 + cardinal t0)
s:tree
t:Info.t
t0:tree
H:forall acc0 : list X.t, length acc0 + cardinal t0 = length (elements_aux acc0 t0)
t1:X.t
t2:tree
H0:forall acc0 : list X.t, length acc0 + cardinal t2 = length (elements_aux acc0 t2)
acc:list X.t

length acc + S (cardinal t2 + cardinal t0) = S (length acc + cardinal t2 + cardinal t0)
now rewrite <- Nat.add_succ_r, Nat.add_assoc. Qed.

forall s : tree, cardinal s = length (elements s)

forall s : tree, cardinal s = length (elements s)
exact (fun s => elements_aux_cardinal s nil). Qed. Definition cardinal_spec (s:tree)(Hs:Ok s) := elements_cardinal s.

forall (s : tree) (acc : list X.t), elements_aux acc s = elements s ++ acc

forall (s : tree) (acc : list X.t), elements_aux acc s = elements s ++ acc
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:forall acc0 : list X.t, elements_aux acc0 s1 = elements s1 ++ acc0
IHs2:forall acc0 : list X.t, elements_aux acc0 s2 = elements s2 ++ acc0
acc:list X.t

elements_aux (t0 :: elements_aux acc s2) s1 = elements (Node t s1 t0 s2) ++ acc
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:forall acc0 : list X.t, elements_aux acc0 s1 = elements s1 ++ acc0
IHs2:forall acc0 : list X.t, elements_aux acc0 s2 = elements s2 ++ acc0
acc:list X.t

elements s1 ++ t0 :: elements s2 ++ acc = elements (Node t s1 t0 s2) ++ acc
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:forall acc0 : list X.t, elements_aux acc0 s1 = elements s1 ++ acc0
IHs2:forall acc0 : list X.t, elements_aux acc0 s2 = elements s2 ++ acc0
acc:list X.t

elements_aux nil s1 ++ t0 :: elements_aux nil s2 ++ acc = elements_aux (t0 :: elements_aux nil s2) s1 ++ acc
rewrite 2 IHs1, IHs2, !app_nil_r, !app_ass; auto. Qed.
c:Info.t
l:tree
x:X.t
r:tree

elements (Node c l x r) = elements l ++ x :: elements r
c:Info.t
l:tree
x:X.t
r:tree

elements (Node c l x r) = elements l ++ x :: elements r
c:Info.t
l:tree
x:X.t
r:tree

elements_aux (x :: elements_aux nil r) l = elements_aux nil l ++ x :: elements_aux nil r
now rewrite !elements_app, !app_nil_r. Qed.

forall (s : tree) (acc : list X.t), rev_elements_aux acc s = rev_elements s ++ acc

forall (s : tree) (acc : list X.t), rev_elements_aux acc s = rev_elements s ++ acc
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:forall acc0 : list X.t, rev_elements_aux acc0 s1 = rev_elements s1 ++ acc0
IHs2:forall acc0 : list X.t, rev_elements_aux acc0 s2 = rev_elements s2 ++ acc0
acc:list X.t

rev_elements_aux (t0 :: rev_elements_aux acc s1) s2 = rev_elements (Node t s1 t0 s2) ++ acc
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:forall acc0 : list X.t, rev_elements_aux acc0 s1 = rev_elements s1 ++ acc0
IHs2:forall acc0 : list X.t, rev_elements_aux acc0 s2 = rev_elements s2 ++ acc0
acc:list X.t

rev_elements s2 ++ t0 :: rev_elements s1 ++ acc = rev_elements (Node t s1 t0 s2) ++ acc
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:forall acc0 : list X.t, rev_elements_aux acc0 s1 = rev_elements s1 ++ acc0
IHs2:forall acc0 : list X.t, rev_elements_aux acc0 s2 = rev_elements s2 ++ acc0
acc:list X.t

rev_elements_aux nil s2 ++ t0 :: rev_elements_aux nil s1 ++ acc = rev_elements_aux (t0 :: rev_elements_aux nil s1) s2 ++ acc
rewrite IHs1, 2 IHs2, !app_nil_r, !app_ass; auto. Qed.
c:Info.t
l:tree
x:X.t
r:tree

rev_elements (Node c l x r) = rev_elements r ++ x :: rev_elements l
c:Info.t
l:tree
x:X.t
r:tree

rev_elements (Node c l x r) = rev_elements r ++ x :: rev_elements l
c:Info.t
l:tree
x:X.t
r:tree

rev_elements_aux (x :: rev_elements_aux nil l) r = rev_elements_aux nil r ++ x :: rev_elements_aux nil l
now rewrite !rev_elements_app, !app_nil_r. Qed.
s:tree

rev_elements s = rev (elements s)
s:tree

rev_elements s = rev (elements s)
c:Info.t
l:tree
x:X.t
r:tree
IHl:rev_elements l = rev (elements l)
IHr:rev_elements r = rev (elements r)

rev_elements (Node c l x r) = rev (elements (Node c l x r))
c:Info.t
l:tree
x:X.t
r:tree
IHl:rev_elements l = rev (elements l)
IHr:rev_elements r = rev (elements r)

rev (elements r) ++ x :: rev (elements l) = rev (x :: elements r) ++ rev (elements l)
c:Info.t
l:tree
x:X.t
r:tree
IHl:rev_elements l = rev (elements l)
IHr:rev_elements r = rev (elements r)

rev (elements r) ++ x :: rev (elements l) = (rev (elements r) ++ x :: nil) ++ rev (elements l)
now rewrite !app_ass. Qed.
The converse of elements_spec2, used in MSetRBT
(* TODO: TO MIGRATE ELSEWHERE... *)

l1, l2:list X.t

Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
l1, l2:list X.t

Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
l2:list X.t

Sorted X.lt (nil ++ l2) -> Sorted X.lt nil /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 nil -> InA X.eq x2 l2 -> X.lt x1 x2)
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Sorted X.lt ((a1 :: l1) ++ l2) -> Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)
l2:list X.t

Sorted X.lt (nil ++ l2) -> Sorted X.lt nil /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 nil -> InA X.eq x2 l2 -> X.lt x1 x2)
l2:list X.t
H:Sorted X.lt l2

forall x1 x2 : X.t, InA X.eq x1 nil -> InA X.eq x2 l2 -> X.lt x1 x2
l2:list X.t
H:Sorted X.lt l2
x1, x2:X.t
H0:InA X.eq x1 nil
H1:InA X.eq x2 l2

X.lt x1 x2
now rewrite InA_nil in *.
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)

Sorted X.lt ((a1 :: l1) ++ l2) -> Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)

Sorted X.lt (a1 :: l1 ++ l2) -> Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)

Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2

Sorted X.lt (a1 :: l1) /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2)
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2

Sorted X.lt (a1 :: l1)
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2
Sorted X.lt l2
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2
forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2

Sorted X.lt (a1 :: l1)
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2

HdRel X.lt a1 l1
destruct l1; simpl in *; auto; inversion_clear Hhd; auto.
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2

Sorted X.lt l2
trivial.
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x1 x2 : X.t, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2

forall x1 x2 : X.t, InA X.eq x1 (a1 :: l1) -> InA X.eq x2 l2 -> X.lt x1 x2
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3
x1, x2:X.t
Hx1:InA X.eq x1 (a1 :: l1)
Hx2:InA X.eq x2 l2

X.lt x1 x2
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3
x1, x2:X.t
Hx1:X.eq x1 a1 \/ InA X.eq x1 l1
Hx2:InA X.eq x2 l2

X.lt x1 x2
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3
x1, x2:X.t
H:X.eq x1 a1
Hx2:InA X.eq x2 l2

X.lt x1 x2
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3
x1, x2:X.t
H:InA X.eq x1 l1
Hx2:InA X.eq x2 l2
X.lt x1 x2
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3
x1, x2:X.t
H:X.eq x1 a1
Hx2:InA X.eq x2 l2

X.lt x1 x2
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3
x1, x2:X.t
H:X.eq x1 a1
Hx2:InA X.eq x2 l2

X.lt a1 x2
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3
x1, x2:X.t
H:X.eq x1 a1
Hx2:InA X.eq x2 l2

InA X.eq x2 (l1 ++ l2)
rewrite InA_app_iff; auto_tc.
a1:X.t
l1, l2:list X.t
IHl1:Sorted X.lt (l1 ++ l2) -> Sorted X.lt l1 /\ Sorted X.lt l2 /\ (forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3)
Hs:Sorted X.lt (l1 ++ l2)
Hhd:HdRel X.lt a1 (l1 ++ l2)
H1:Sorted X.lt l1
H2:Sorted X.lt l2
H3:forall x0 x3 : X.t, InA X.eq x0 l1 -> InA X.eq x3 l2 -> X.lt x0 x3
x1, x2:X.t
H:InA X.eq x1 l1
Hx2:InA X.eq x2 l2

X.lt x1 x2
auto. Qed.
s:tree

Sorted X.lt (elements s) -> Ok s
s:tree

Sorted X.lt (elements s) -> Ok s

Sorted X.lt (elements Leaf) -> Ok Leaf
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
Sorted X.lt (elements (Node c l x r)) -> Ok (Node c l x r)

Sorted X.lt (elements Leaf) -> Ok Leaf
auto.
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r

Sorted X.lt (elements (Node c l x r)) -> Ok (Node c l x r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r

Sorted X.lt (elements l ++ x :: elements r) -> Ok (Node c l x r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)

Ok (Node c l x r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H2:Sorted X.lt (x :: elements r)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2

Ok (Node c l x r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)

Ok (Node c l x r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)

lt_tree x l
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)
gt_tree x r
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)

lt_tree x l
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)
y:elt
Hy:InT y l

X.lt y x
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)
y:elt
Hy:InT y l

InA X.eq y (elements l)
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)
y:elt
Hy:InT y l
InA X.eq x (x :: elements r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)
y:elt
Hy:InT y l

InA X.eq y (elements l)
now rewrite elements_spec1.
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)
y:elt
Hy:InT y l

InA X.eq x (x :: elements r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)
y:elt
Hy:InT y l

X.eq x x \/ InA X.eq x (elements r)
now left.
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)

gt_tree x r
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)
y:elt
Hy:InT y r

X.lt x y
c:Info.t
l:tree
x:X.t
r:tree
IHl:Sorted X.lt (elements l) -> Ok l
IHr:Sorted X.lt (elements r) -> Ok r
H:Sorted X.lt (elements l ++ x :: elements r)
H1:Sorted X.lt (elements l)
H3:forall x1 x2 : X.t, InA X.eq x1 (elements l) -> InA X.eq x2 (x :: elements r) -> X.lt x1 x2
H0:Sorted X.lt (elements r)
H4:HdRel X.lt x (elements r)
y:elt
Hy:InT y r

InA X.eq y (elements r)
now rewrite elements_spec1. Qed.

for_all and

s:tree
f:X.t -> bool

Proper (X.eq ==> eq) f -> for_all f s = true <-> For_all (fun x : elt => f x = true) s
s:tree
f:X.t -> bool

Proper (X.eq ==> eq) f -> for_all f s = true <-> For_all (fun x : elt => f x = true) s
s:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

for_all f s = true <-> (forall x : elt, InT x s -> f x = true)
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

true = true <-> (forall x : elt, InT x Leaf -> f x = true)
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
IHl:for_all f l = true <-> (forall x0 : elt, InT x0 l -> f x0 = true)
IHr:for_all f r = true <-> (forall x0 : elt, InT x0 r -> f x0 = true)
f x &&& for_all f l &&& for_all f r = true <-> (forall x0 : elt, InT x0 (Node i l x r) -> f x0 = true)
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

true = true <-> (forall x : elt, InT x Leaf -> f x = true)
split; intros; inv; auto.
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
IHl:for_all f l = true <-> (forall x0 : elt, InT x0 l -> f x0 = true)
IHr:for_all f r = true <-> (forall x0 : elt, InT x0 r -> f x0 = true)

f x &&& for_all f l &&& for_all f r = true <-> (forall x0 : elt, InT x0 (Node i l x r) -> f x0 = true)
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
IHl:for_all f l = true <-> (forall x0 : elt, InT x0 l -> f x0 = true)
IHr:for_all f r = true <-> (forall x0 : elt, InT x0 r -> f x0 = true)

(f x = true /\ (forall x0 : elt, InT x0 l -> f x0 = true)) /\ (forall x0 : elt, InT x0 r -> f x0 = true) <-> (forall x0 : elt, InT x0 (Node i l x r) -> f x0 = true)
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

(f x = true /\ (forall x0 : elt, InT x0 l -> f x0 = true)) /\ (forall x0 : elt, InT x0 r -> f x0 = true) <-> (forall x0 : elt, InT x0 (Node i l x r) -> f x0 = true)
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
H1:forall x1 : elt, InT x1 r -> f x1 = true
H:f x = true
H2:forall x1 : elt, InT x1 l -> f x1 = true
x0:elt
H4:X.eq x0 x

f x0 = true
eauto. Qed.
s:tree
f:X.t -> bool

Proper (X.eq ==> eq) f -> exists_ f s = true <-> Exists (fun x : elt => f x = true) s
s:tree
f:X.t -> bool

Proper (X.eq ==> eq) f -> exists_ f s = true <-> Exists (fun x : elt => f x = true) s
s:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

exists_ f s = true <-> (exists x : elt, InT x s /\ f x = true)
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

false = true <-> (exists x : elt, InT x Leaf /\ f x = true)
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
IHl:exists_ f l = true <-> (exists x0 : elt, InT x0 l /\ f x0 = true)
IHr:exists_ f r = true <-> (exists x0 : elt, InT x0 r /\ f x0 = true)
f x ||| exists_ f l ||| exists_ f r = true <-> (exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true)
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

false = true <-> (exists x : elt, InT x Leaf /\ f x = true)
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

false = true -> exists x : elt, InT x Leaf /\ f x = true
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
(exists x : elt, InT x Leaf /\ f x = true) -> false = true
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

false = true -> exists x : elt, InT x Leaf /\ f x = true
discriminate.
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

(exists x : elt, InT x Leaf /\ f x = true) -> false = true
intros (y,(H,_)); inv.
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
IHl:exists_ f l = true <-> (exists x0 : elt, InT x0 l /\ f x0 = true)
IHr:exists_ f r = true <-> (exists x0 : elt, InT x0 r /\ f x0 = true)

f x ||| exists_ f l ||| exists_ f r = true <-> (exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true)
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
IHl:exists_ f l = true <-> (exists x0 : elt, InT x0 l /\ f x0 = true)
IHr:exists_ f r = true <-> (exists x0 : elt, InT x0 r /\ f x0 = true)

(f x = true \/ (exists x0 : elt, InT x0 l /\ f x0 = true)) \/ (exists x0 : elt, InT x0 r /\ f x0 = true) <-> (exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true)
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f

(f x = true \/ (exists x0 : elt, InT x0 l /\ f x0 = true)) \/ (exists x0 : elt, InT x0 r /\ f x0 = true) <-> (exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true)
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
H:f x = true

exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
y:elt
H:InT y l
H':f y = true
exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
y:elt
H:InT y r
H':f y = true
exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
y:elt
H:InT y (Node i l x r)
H':f y = true
(f x = true \/ (exists x0 : elt, InT x0 l /\ f x0 = true)) \/ (exists x0 : elt, InT x0 r /\ f x0 = true)
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
H:f x = true

exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true
exists x; auto.
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
y:elt
H:InT y l
H':f y = true

exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true
exists y; auto.
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
y:elt
H:InT y r
H':f y = true

exists x0 : elt, InT x0 (Node i l x r) /\ f x0 = true
exists y; auto.
i:Info.t
l:tree
x:X.t
r:tree
f:X.t -> bool
Hf:Proper (X.eq ==> eq) f
y:elt
H:InT y (Node i l x r)
H':f y = true

(f x = true \/ (exists x0 : elt, InT x0 l /\ f x0 = true)) \/ (exists x0 : elt, InT x0 r /\ f x0 = true)
inv; [left;left|left;right|right]; try (exists y); eauto. Qed.

Fold

A:Type
f:elt -> A -> A
s:tree
i:A
acc:list elt

fold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i)
A:Type
f:elt -> A -> A
s:tree
i:A
acc:list elt

fold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i)
A:Type
f:elt -> A -> A
s:tree

forall (i : A) (acc : list elt), fold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i)
A:Type
f:elt -> A -> A
c:Info.t
l:tree
x:X.t
r:tree
IHl:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 l) i0 = fold_left (flip f) acc0 (fold f l i0)
IHr:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 r) i0 = fold_left (flip f) acc0 (fold f r i0)
i:A
acc:list elt

fold_left (flip f) (elements_aux (x :: elements_aux acc r) l) i = fold_left (flip f) acc (fold f r (f x (fold f l i)))
A:Type
f:elt -> A -> A
c:Info.t
l:tree
x:X.t
r:tree
IHl:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 l) i0 = fold_left (flip f) acc0 (fold f l i0)
IHr:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 r) i0 = fold_left (flip f) acc0 (fold f r i0)
i:A
acc:list elt

fold_left (flip f) (x :: elements_aux acc r) (fold f l i) = fold_left (flip f) acc (fold f r (f x (fold f l i)))
A:Type
f:elt -> A -> A
c:Info.t
l:tree
x:X.t
r:tree
IHl:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 l) i0 = fold_left (flip f) acc0 (fold f l i0)
IHr:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 r) i0 = fold_left (flip f) acc0 (fold f r i0)
i:A
acc:list elt

fold_left (flip f) (elements_aux acc r) (flip f (fold f l i) x) = fold_left (flip f) acc (fold f r (f x (fold f l i)))
A:Type
f:elt -> A -> A
c:Info.t
l:tree
x:X.t
r:tree
IHl:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 l) i0 = fold_left (flip f) acc0 (fold f l i0)
IHr:forall (i0 : A) (acc0 : list elt), fold_left (flip f) (elements_aux acc0 r) i0 = fold_left (flip f) acc0 (fold f r i0)
i:A
acc:list elt

fold_left (flip f) (elements_aux acc r) (f x (fold f l i)) = fold_left (flip f) acc (fold f r (f x (fold f l i)))
apply IHr. Qed.
s:tree
A:Type
i:A
f:elt -> A -> A

fold f s i = fold_left (flip f) (elements s) i
s:tree
A:Type
i:A
f:elt -> A -> A

fold f s i = fold_left (flip f) (elements s) i
s:tree
A:Type
f:elt -> A -> A

forall i : A, fold f s i = fold_left (flip f) (elements s) i
s:tree
A:Type
f:elt -> A -> A

forall i : A, fold f s i = fold_left (flip f) (elements_aux nil s) i
c:Info.t
l:tree
x:X.t
r:tree
A:Type
f:elt -> A -> A
IHl:forall i0 : A, fold f l i0 = fold_left (flip f) (elements_aux nil l) i0
IHr:forall i0 : A, fold f r i0 = fold_left (flip f) (elements_aux nil r) i0
i:A

fold f r (f x (fold f l i)) = fold_left (flip f) (elements_aux (x :: elements_aux nil r) l) i
c:Info.t
l:tree
x:X.t
r:tree
A:Type
f:elt -> A -> A
IHl:forall i0 : A, fold f l i0 = fold_left (flip f) (elements_aux nil l) i0
IHr:forall i0 : A, fold f r i0 = fold_left (flip f) (elements_aux nil r) i0
i:A

fold f r (f x (fold f l i)) = fold_left (flip f) (x :: elements_aux nil r) (fold f l i)
c:Info.t
l:tree
x:X.t
r:tree
A:Type
f:elt -> A -> A
IHl:forall i0 : A, fold f l i0 = fold_left (flip f) (elements_aux nil l) i0
IHr:forall i0 : A, fold f r i0 = fold_left (flip f) (elements_aux nil r) i0
i:A

fold_left (flip f) (elements_aux nil r) (f x (fold f l i)) = fold_left (flip f) (x :: elements_aux nil r) (fold f l i)
simpl; auto. Qed.

Subset


forall (subset_l1 : tree -> bool) (l1 : tree) (x1 : X.t) (c1 : Info.t) (s2 : tree), Ok (Node c1 l1 x1 Leaf) -> Ok s2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 s2 = true <-> Subset (Node c1 l1 x1 Leaf) s2

forall (subset_l1 : tree -> bool) (l1 : tree) (x1 : X.t) (c1 : Info.t) (s2 : tree), Ok (Node c1 l1 x1 Leaf) -> Ok s2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 s2 = true <-> Subset (Node c1 l1 x1 Leaf) s2
subset_l1:tree -> bool
l1:tree
x1:X.t
c1:Info.t
H:Ok (Node c1 l1 x1 Leaf)
H0:Ok Leaf
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s

false = true <-> Subset (Node c1 l1 x1 Leaf) Leaf
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok (Node c1 l1 x1 Leaf) -> Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok (Node c1 l1 x1 Leaf) -> Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H:Ok (Node c1 l1 x1 Leaf)
H0:Ok (Node c2 l2 x2 r2)
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
match X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1:Info.t
H:Ok (Node c1 l1 x1 Leaf)
H0:Ok Leaf
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H2:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a Leaf

false = true
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok (Node c1 l1 x1 Leaf) -> Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok (Node c1 l1 x1 Leaf) -> Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H:Ok (Node c1 l1 x1 Leaf)
H0:Ok (Node c2 l2 x2 r2)
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
match X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok (Node c1 l1 x1 Leaf) -> Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok (Node c1 l1 x1 Leaf) -> Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H:Ok (Node c1 l1 x1 Leaf)
H0:Ok (Node c2 l2 x2 r2)
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s

match X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok (Node c1 l1 x1 Leaf) -> Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H:Ok (Node c1 l1 x1 Leaf)
H0:Ok (Node c2 l2 x2 r2)
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s

match X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H:Ok (Node c1 l1 x1 Leaf)
H0:Ok (Node c2 l2 x2 r2)
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s

match X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf

match X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.eq x1 x2

subset_l1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2
subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.eq x1 x2

Subset l1 l2 <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2
subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.eq x1 x2

(forall a : elt, InT a l1 -> InT a l2) <-> (forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2))
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2
subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.eq x1 x2
H0:bool
H1:forall a0 : elt, InT a0 l1 -> InT a0 l2
a:elt
H4:X.eq a x1

InT a (Node c2 l2 x2 r2)
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.eq x1 x2
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H2:InT a l1
InT a l2
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2
subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.eq x1 x2
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H2:InT a l1

InT a l2
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2
subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2

subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2

Subset (Node c1 l1 x1 Leaf) l2 <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2

(forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a l2) <-> (forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2))
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H4:X.eq a x1

InT a l2
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H4:InT a l1
InT a l2
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x1 x2
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 l1 x1 Leaf) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H4:InT a l1

InT a l2
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:Ok l2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 l2 = true <-> Subset (Node c1 l1 x1 Leaf) l2
IHr2:Ok r2 -> (forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s) -> subsetl subset_l1 x1 r2 = true <-> Subset (Node c1 l1 x1 Leaf) r2
H1:forall s : tree, Ok s -> subset_l1 s = true <-> Subset l1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1

mem x1 r2 &&& subset_l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1

mem x1 r2 = true /\ Subset l1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 Leaf) (Node c2 l2 x2 r2)
subset_l1:tree -> bool
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1

mem x1 r2 = true /\ (forall a : elt, InT a l1 -> InT a (Node c2 l2 x2 r2)) <-> (forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2))
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
H0:bool
H2:mem x1 r2 = true
H3:forall a0 : elt, InT a0 l1 -> InT a0 (Node c2 l2 x2 r2)
a:elt
H10:X.eq a x1

InT a (Node c2 l2 x2 r2)
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
H0:bool
H1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)
mem x1 r2 = true
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
H0:bool
H2:mem x1 r2 = true
H3:forall a0 : elt, InT a0 l1 -> InT a0 (Node c2 l2 x2 r2)
a:elt
H10:X.eq a x1

InT a r2
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
H0:bool
H1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)
mem x1 r2 = true
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
H0:bool
H2:mem x1 r2 = true
H3:forall a0 : elt, InT a0 l1 -> InT a0 (Node c2 l2 x2 r2)
a:elt
H10:X.eq a x1

InT x1 r2
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
H0:bool
H1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)
mem x1 r2 = true
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
H0:bool
H1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)

mem x1 r2 = true
l1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H5:Ok l1
H11:lt_tree x1 l1
H12:gt_tree x1 Leaf
H:X.lt x2 x1
H0:bool
H1:forall a : elt, InT a (Node c1 l1 x1 Leaf) -> InT a (Node c2 l2 x2 r2)

InT x1 r2
assert (InT x1 (Node c2 l2 x2 r2)) by auto; intuition_in; order. Qed.

forall (subset_r1 : tree -> bool) (r1 : tree) (x1 : X.t) (c1 : Info.t) (s2 : tree), bst (Node c1 Leaf x1 r1) -> bst s2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 s2 = true <-> Subset (Node c1 Leaf x1 r1) s2

forall (subset_r1 : tree -> bool) (r1 : tree) (x1 : X.t) (c1 : Info.t) (s2 : tree), bst (Node c1 Leaf x1 r1) -> bst s2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 s2 = true <-> Subset (Node c1 Leaf x1 r1) s2
subset_r1:tree -> bool
r1:tree
x1:X.t
c1:Info.t
H:bst (Node c1 Leaf x1 r1)
H0:bst Leaf
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s

false = true <-> Subset (Node c1 Leaf x1 r1) Leaf
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst (Node c1 Leaf x1 r1) -> bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst (Node c1 Leaf x1 r1) -> bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H:bst (Node c1 Leaf x1 r1)
H0:bst (Node c2 l2 x2 r2)
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
match X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1:Info.t
H:bst (Node c1 Leaf x1 r1)
H0:bst Leaf
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H2:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a Leaf

false = true
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst (Node c1 Leaf x1 r1) -> bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst (Node c1 Leaf x1 r1) -> bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H:bst (Node c1 Leaf x1 r1)
H0:bst (Node c2 l2 x2 r2)
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
match X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst (Node c1 Leaf x1 r1) -> bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst (Node c1 Leaf x1 r1) -> bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H:bst (Node c1 Leaf x1 r1)
H0:bst (Node c2 l2 x2 r2)
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s

match X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst (Node c1 Leaf x1 r1) -> bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H:bst (Node c1 Leaf x1 r1)
H0:bst (Node c2 l2 x2 r2)
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s

match X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H:bst (Node c1 Leaf x1 r1)
H0:bst (Node c2 l2 x2 r2)
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s

match X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1

match X.compare x1 x2 with | Eq => subset_r1 r2 | Lt => mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) | Gt => subsetr subset_r1 x1 r2 end = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.eq x1 x2

subset_r1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.eq x1 x2

Subset r1 r2 <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.eq x1 x2

(forall a : elt, InT a r1 -> InT a r2) <-> (forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2))
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.eq x1 x2
H0:bool
H1:forall a0 : elt, InT a0 r1 -> InT a0 r2
a:elt
H4:X.eq a x1

InT a (Node c2 l2 x2 r2)
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.eq x1 x2
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H2:InT a r1
InT a r2
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.eq x1 x2
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H2:InT a r1

InT a r2
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2

mem x1 l2 &&& subset_r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2

mem x1 l2 = true /\ Subset r1 (Node c2 l2 x2 r2) <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2

mem x1 l2 = true /\ (forall a : elt, InT a r1 -> InT a (Node c2 l2 x2 r2)) <-> (forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2))
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
H0:bool
H2:mem x1 l2 = true
H3:forall a0 : elt, InT a0 r1 -> InT a0 (Node c2 l2 x2 r2)
a:elt
H5:X.eq a x1

InT a (Node c2 l2 x2 r2)
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
H0:bool
H1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)
mem x1 l2 = true
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
H0:bool
H2:mem x1 l2 = true
H3:forall a0 : elt, InT a0 r1 -> InT a0 (Node c2 l2 x2 r2)
a:elt
H5:X.eq a x1

InT a l2
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
H0:bool
H1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)
mem x1 l2 = true
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
H0:bool
H2:mem x1 l2 = true
H3:forall a0 : elt, InT a0 r1 -> InT a0 (Node c2 l2 x2 r2)
a:elt
H5:X.eq a x1

InT x1 l2
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
H0:bool
H1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)
mem x1 l2 = true
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
H0:bool
H1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)

mem x1 l2 = true
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x1 x2
H0:bool
H1:forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2)

InT x1 l2
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
IHl2:bst l2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 l2 = true <-> Subset (Node c1 Leaf x1 r1) l2
IHr2:bst r2 -> (forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s) -> subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) r2
H1:forall s : tree, bst s -> subset_r1 s = true <-> Subset r1 s
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1

subsetr subset_r1 x1 r2 = true <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1

Subset (Node c1 Leaf x1 r1) r2 <-> Subset (Node c1 Leaf x1 r1) (Node c2 l2 x2 r2)
subset_r1:tree -> bool
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1

(forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a r2) <-> (forall a : elt, InT a (Node c1 Leaf x1 r1) -> InT a (Node c2 l2 x2 r2))
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H4:X.eq a x1

InT a r2
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H4:InT a r1
InT a r2
r1:tree
x1:X.t
c1, c2:Info.t
l2:tree
x2:X.t
r2:tree
H6:Ok l2
H7:Ok r2
H8:lt_tree x2 l2
H9:gt_tree x2 r2
H10:Ok r1
H11:lt_tree x1 Leaf
H12:gt_tree x1 r1
H:X.lt x2 x1
H0:bool
H1:forall a0 : elt, InT a0 (Node c1 Leaf x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H4:InT a r1

InT a r2
assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. Qed.

forall s1 s2 : tree, Ok s1 -> Ok s2 -> subset s1 s2 = true <-> Subset s1 s2

forall s1 s2 : tree, Ok s1 -> Ok s2 -> subset s1 s2 = true <-> Subset s1 s2
s2:tree
H:Ok Leaf
H0:Ok s2

true = true <-> Subset Leaf s2
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s0 : tree, Ok l1 -> Ok s0 -> subset l1 s0 = true <-> Subset l1 s0
IHr1:forall s0 : tree, Ok r1 -> Ok s0 -> subset r1 s0 = true <-> Subset r1 s0
s2:tree
H:Ok (Node c1 l1 x1 r1)
H0:Ok s2
match s2 with | Leaf => false | Node _ l2 x2 r2 => match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 s2 | Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2 end end = true <-> Subset (Node c1 l1 x1 r1) s2
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s0 : tree, Ok l1 -> Ok s0 -> subset l1 s0 = true <-> Subset l1 s0
IHr1:forall s0 : tree, Ok r1 -> Ok s0 -> subset r1 s0 = true <-> Subset r1 s0
s2:tree
H:Ok (Node c1 l1 x1 r1)
H0:Ok s2

match s2 with | Leaf => false | Node _ l2 x2 r2 => match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 s2 | Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2 end end = true <-> Subset (Node c1 l1 x1 r1) s2
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
H:Ok (Node c1 l1 x1 r1)
H0:Ok Leaf

false = true <-> Subset (Node c1 l1 x1 r1) Leaf
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H:Ok (Node c1 l1 x1 r1)
H0:Ok (Node c2 l2 x2 r2)
match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) | Gt => subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
H1:forall a : elt, InT a (Node c1 l1 x1 r1) -> InT a Leaf
H6:Ok l1
H7:Ok r1
H8:lt_tree x1 l1
H9:gt_tree x1 r1

false = true
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H:Ok (Node c1 l1 x1 r1)
H0:Ok (Node c2 l2 x2 r2)
match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) | Gt => subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H:Ok (Node c1 l1 x1 r1)
H0:Ok (Node c2 l2 x2 r2)

match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) | Gt => subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1

match X.compare x1 x2 with | Eq => subset l1 l2 &&& subset r1 r2 | Lt => subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) | Gt => subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) end = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.eq x1 x2

subset l1 l2 &&& subset r1 r2 = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2
subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.eq x1 x2

Subset l1 l2 /\ Subset r1 r2 <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2
subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.eq x1 x2

Subset l1 l2 /\ Subset r1 r2 <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2
subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.eq x1 x2
H1:forall a0 : elt, InT a0 l1 -> InT a0 l2
H2:forall a0 : elt, InT a0 r1 -> InT a0 r2
a:elt
H12:X.eq a x1

InT a (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.eq x1 x2
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H1:InT a l1
InT a l2
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.eq x1 x2
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H1:InT a r1
InT a r2
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2
subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.eq x1 x2
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H1:InT a l1

InT a l2
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.eq x1 x2
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H1:InT a r1
InT a r2
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2
subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.eq x1 x2
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H1:InT a r1

InT a r2
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2
subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2

subsetl (subset l1) x1 l2 &&& subset r1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2

subsetl (subset l1) x1 l2 = true /\ Subset r1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2

Subset (Node c1 l1 x1 Leaf) l2 /\ Subset r1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2

Subset (Node c1 l1 x1 Leaf) l2 /\ Subset r1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H3:X.eq a x1

InT a l2
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H3:InT a l1
InT a l2
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x1 x2
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H3:InT a l1

InT a l2
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1

subsetr (subset r1) x1 r2 &&& subset l1 (Node c2 l2 x2 r2) = true <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1

subsetr (subset r1) x1 r2 = true /\ Subset l1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
IHl1:forall s2 : tree, Ok l1 -> Ok s2 -> subset l1 s2 = true <-> Subset l1 s2
IHr1:forall s2 : tree, Ok r1 -> Ok s2 -> subset r1 s2 = true <-> Subset r1 s2
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1

Subset (Node c1 Leaf x1 r1) r2 /\ Subset l1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1

Subset (Node c1 Leaf x1 r1) r2 /\ Subset l1 (Node c2 l2 x2 r2) <-> Subset (Node c1 l1 x1 r1) (Node c2 l2 x2 r2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H3:X.eq a x1

InT a r2
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H3:InT a r1
InT a r2
c1:Info.t
l1:tree
x1:X.t
r1:tree
c2:Info.t
l2:tree
x2:X.t
r2:tree
H5:Ok l2
H6:Ok r2
H7:lt_tree x2 l2
H8:gt_tree x2 r2
H4:Ok l1
H9:Ok r1
H10:lt_tree x1 l1
H11:gt_tree x1 r1
H:X.lt x2 x1
H0:forall a0 : elt, InT a0 (Node c1 l1 x1 r1) -> InT a0 (Node c2 l2 x2 r2)
a:elt
H3:InT a r1

InT a r2
assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. Qed.

Comparison

Relations eq and lt over trees
Module L := MSetInterface.MakeListOrdering X.

Definition eq := Equal.

Equivalence eq

Equivalence eq
firstorder. Qed.

forall s s' : tree, eq s s' <-> L.eq (elements s) (elements s')

forall s s' : tree, eq s s' <-> L.eq (elements s) (elements s')
s, s':tree

(forall a : elt, InT a s <-> InT a s') <-> (forall x : X.t, InA X.eq x (elements s) <-> InA X.eq x (elements s'))
s, s':tree

(forall a : elt, InT a s <-> InT a s') <-> (forall x : X.t, InT x s <-> InT x s')
firstorder. Qed. Definition lt (s1 s2 : tree) : Prop := exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2' /\ L.lt (elements s1') (elements s2'). Declare Equivalent Keys L.eq equivlistA.

StrictOrder lt

StrictOrder lt

Irreflexive lt

Transitive lt
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)

False

Transitive lt
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)

eqlistA X.eq (elements s1) (elements s2)
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)
H:eqlistA X.eq (elements s1) (elements s2)
False

Transitive lt
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)

equivlistA X.eq (elements s1) (elements s2)
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)
H:eqlistA X.eq (elements s1) (elements s2)
False

Transitive lt
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)

eq s1 s2
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)
H:eqlistA X.eq (elements s1) (elements s2)
False

Transitive lt
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)

eq s1 s
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)
H:eqlistA X.eq (elements s1) (elements s2)
False

Transitive lt
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s1) (elements s2)
H:eqlistA X.eq (elements s1) (elements s2)

False

Transitive lt
s, s1, s2:tree
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt (elements s2) (elements s2)
H:eqlistA X.eq (elements s1) (elements s2)

False

Transitive lt

Transitive lt
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')

lt s1 s3
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')

L.lt (elements s1') (elements s3')
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')

eqlistA X.eq (elements s2') (elements s2'')
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')
H:eqlistA X.eq (elements s2') (elements s2'')
L.lt (elements s1') (elements s3')
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')

equivlistA X.eq (elements s2') (elements s2'')
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')
H:eqlistA X.eq (elements s2') (elements s2'')
L.lt (elements s1') (elements s3')
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')

eq s2' s2''
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')
H:eqlistA X.eq (elements s2') (elements s2'')
L.lt (elements s1') (elements s3')
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')

eq s2' s2
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')
H:eqlistA X.eq (elements s2') (elements s2'')
L.lt (elements s1') (elements s3')
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')
H:eqlistA X.eq (elements s2') (elements s2'')

L.lt (elements s1') (elements s3')
s1, s2, s3, s1', s2':tree
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt (elements s1') (elements s2')
s2'', s3':tree
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt (elements s2'') (elements s3')
H:eqlistA X.eq (elements s2') (elements s2'')

L.lt (elements s2') (elements s3')
rewrite H; auto. Qed.

Proper (eq ==> eq ==> iff) lt

Proper (eq ==> eq ==> iff) lt
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4

lt s1 s3 <-> lt s2 s4
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4

lt s1 s3 -> lt s2 s4
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt (elements s1') (elements s3')

lt s2 s4
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt (elements s1') (elements s3')

eq s2 s1' /\ eq s4 s3' /\ L.lt (elements s1') (elements s3')
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt (elements s1') (elements s3')

eq s2 s1'
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt (elements s1') (elements s3')
eq s4 s3' /\ L.lt (elements s1') (elements s3')
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt (elements s1') (elements s3')

eq s2 s1
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt (elements s1') (elements s3')
eq s4 s3' /\ L.lt (elements s1') (elements s3')
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt (elements s1') (elements s3')

eq s4 s3' /\ L.lt (elements s1') (elements s3')
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt (elements s1') (elements s3')

eq s4 s3'
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt (elements s1') (elements s3')

eq s4 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4

lt s2 s4 -> lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt (elements s1') (elements s3')

lt s1 s3
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt (elements s1') (elements s3')

eq s1 s1' /\ eq s3 s3' /\ L.lt (elements s1') (elements s3')
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt (elements s1') (elements s3')

eq s1 s1'
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt (elements s1') (elements s3')
eq s3 s3' /\ L.lt (elements s1') (elements s3')
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt (elements s1') (elements s3')

eq s3 s3' /\ L.lt (elements s1') (elements s3')
s1, s2:tree
E12:eq s1 s2
s3, s4:tree
E34:eq s3 s4
s1', s3':tree
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt (elements s1') (elements s3')

eq s3 s3'
transitivity s4; auto. Qed.
Proof of the comparison algorithm
flatten_e e returns the list of elements of e i.e. the list of elements actually compared
Fixpoint flatten_e (e : enumeration) : list elt := match e with
  | End => nil
  | More x t r => x :: elements t ++ flatten_e r
 end.


forall (l : tree) (x : elt) (r : tree) (c : Info.t) (e : enumeration), elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e

forall (l : tree) (x : elt) (r : tree) (c : Info.t) (e : enumeration), elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e
l:tree
x:elt
r:tree
c:Info.t
e:enumeration

elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e
now rewrite elements_node, app_ass. Qed.

forall (s : tree) (e : enumeration), flatten_e (cons s e) = elements s ++ flatten_e e

forall (s : tree) (e : enumeration), flatten_e (cons s e) = elements s ++ flatten_e e
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:forall e0 : enumeration, flatten_e (cons s1 e0) = elements s1 ++ flatten_e e0
IHs2:forall e0 : enumeration, flatten_e (cons s2 e0) = elements s2 ++ flatten_e e0
e:enumeration

flatten_e (cons s1 (More t0 s2 e)) = elements (Node t s1 t0 s2) ++ flatten_e e
rewrite IHs1; apply flatten_e_elements. Qed.
Correctness of this comparison
Definition Cmp c x y := CompSpec L.eq L.lt x y c.

Local Hint Unfold Cmp flip : core.


forall e2 : enumeration, Cmp (compare_end e2) nil (flatten_e e2)

forall e2 : enumeration, Cmp (compare_end e2) nil (flatten_e e2)

L.eq nil nil
reflexivity. Qed.

forall (x1 : X.t) (cont : enumeration -> comparison) (x2 : elt) (r2 : tree) (e2 : enumeration) (l : list X.t), Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> Cmp (compare_more x1 cont (More x2 r2 e2)) (x1 :: l) (flatten_e (More x2 r2 e2))

forall (x1 : X.t) (cont : enumeration -> comparison) (x2 : elt) (r2 : tree) (e2 : enumeration) (l : list X.t), Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> Cmp (compare_more x1 cont (More x2 r2 e2)) (x1 :: l) (flatten_e (More x2 r2 e2))
simpl; intros; elim_compare x1 x2; simpl; red; auto. Qed.

forall (s1 : tree) (cont : enumeration -> comparison) (e2 : enumeration) (l : list X.t), (forall e : enumeration, Cmp (cont e) l (flatten_e e)) -> Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2)

forall (s1 : tree) (cont : enumeration -> comparison) (e2 : enumeration) (l : list X.t), (forall e : enumeration, Cmp (cont e) l (flatten_e e)) -> Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
Hl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)
Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)
cont:enumeration -> comparison
e2:enumeration
l:list X.t
H:forall e : enumeration, Cmp (cont e) l (flatten_e e)

Cmp (compare_cont (Node c1 l1 x1 r1) cont e2) (elements (Node c1 l1 x1 r1) ++ l) (flatten_e e2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
Hl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)
Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)
cont:enumeration -> comparison
e2:enumeration
l:list X.t
H:forall e : enumeration, Cmp (cont e) l (flatten_e e)

Cmp (compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2) (elements l1 ++ x1 :: elements r1 ++ l) (flatten_e e2)
c1:Info.t
l1:tree
x1:X.t
r1:tree
Hl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)
Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)
cont:enumeration -> comparison
e2:enumeration
l:list X.t
H:forall e : enumeration, Cmp (cont e) l (flatten_e e)

forall e : enumeration, Cmp (compare_more x1 (compare_cont r1 cont) e) (x1 :: elements r1 ++ l) (flatten_e e)
c1:Info.t
l1:tree
x1:X.t
r1:tree
Hl1:forall (cont0 : enumeration -> comparison) (e2 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e2) (elements l1 ++ l0) (flatten_e e2)
Hr1:forall (cont0 : enumeration -> comparison) (e2 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e2) (elements r1 ++ l0) (flatten_e e2)
cont:enumeration -> comparison
l:list X.t
H:forall e : enumeration, Cmp (cont e) l (flatten_e e)

forall e : enumeration, Cmp (compare_more x1 (compare_cont r1 cont) e) (x1 :: elements r1 ++ l) (flatten_e e)
c1:Info.t
l1:tree
x1:X.t
r1:tree
Hl1:forall (cont0 : enumeration -> comparison) (e2 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e2) (elements l1 ++ l0) (flatten_e e2)
Hr1:forall (cont0 : enumeration -> comparison) (e2 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e2) (elements r1 ++ l0) (flatten_e e2)
cont:enumeration -> comparison
l:list X.t
H:forall e : enumeration, Cmp (cont e) l (flatten_e e)

Cmp (compare_more x1 (compare_cont r1 cont) End) (x1 :: elements r1 ++ l) (flatten_e End)
c1:Info.t
l1:tree
x1:X.t
r1:tree
Hl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)
Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)
cont:enumeration -> comparison
l:list X.t
H:forall e : enumeration, Cmp (cont e) l (flatten_e e)
x2:elt
r2:tree
e2:enumeration
Cmp (compare_more x1 (compare_cont r1 cont) (More x2 r2 e2)) (x1 :: elements r1 ++ l) (flatten_e (More x2 r2 e2))
c1:Info.t
l1:tree
x1:X.t
r1:tree
Hl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)
Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)
cont:enumeration -> comparison
l:list X.t
H:forall e : enumeration, Cmp (cont e) l (flatten_e e)
x2:elt
r2:tree
e2:enumeration

Cmp (compare_more x1 (compare_cont r1 cont) (More x2 r2 e2)) (x1 :: elements r1 ++ l) (flatten_e (More x2 r2 e2))
c1:Info.t
l1:tree
x1:X.t
r1:tree
Hl1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont l1 cont0 e0) (elements l1 ++ l0) (flatten_e e0)
Hr1:forall (cont0 : enumeration -> comparison) (e0 : enumeration) (l0 : list X.t), (forall e : enumeration, Cmp (cont0 e) l0 (flatten_e e)) -> Cmp (compare_cont r1 cont0 e0) (elements r1 ++ l0) (flatten_e e0)
cont:enumeration -> comparison
l:list X.t
H:forall e : enumeration, Cmp (cont e) l (flatten_e e)
x2:elt
r2:tree
e2:enumeration

Cmp (compare_cont r1 cont (cons r2 e2)) (elements r1 ++ l) (elements r2 ++ flatten_e e2)
rewrite <- cons_1; auto. Qed.

forall s1 s2 : tree, Cmp (compare s1 s2) (elements s1) (elements s2)

forall s1 s2 : tree, Cmp (compare s1 s2) (elements s1) (elements s2)
s1, s2:tree

Cmp (compare_cont s1 compare_end (cons s2 End)) (elements s1) (elements s2)
s1, s2:tree

Cmp (compare_cont s1 compare_end (cons s2 End)) (elements s1 ++ nil) (elements s2)
s1, s2:tree

Cmp (compare_cont s1 compare_end (cons s2 End)) (elements s1 ++ nil) (flatten_e (cons s2 End))
s1, s2:tree

forall e : enumeration, Cmp (compare_end e) nil (flatten_e e)
s1, s2:tree
e:enumeration

Cmp (compare_end e) nil (flatten_e e)
apply compare_end_Cmp; auto. Qed.

forall s1 s2 : tree, Ok s1 -> Ok s2 -> CompSpec eq lt s1 s2 (compare s1 s2)

forall s1 s2 : tree, Ok s1 -> Ok s2 -> CompSpec eq lt s1 s2 (compare s1 s2)
s1, s2:tree
H:Ok s1
H0:Ok s2

CompSpec eq lt s1 s2 (compare s1 s2)
s1, s2:tree
H:Ok s1
H0:Ok s2
H1:L.eq (elements s1) (elements s2)

eq s1 s2
s1, s2:tree
H:Ok s1
H0:Ok s2
H1:L.lt (elements s1) (elements s2)
lt s1 s2
s1, s2:tree
H:Ok s1
H0:Ok s2
H1:L.lt (elements s2) (elements s1)
lt s2 s1
s1, s2:tree
H:Ok s1
H0:Ok s2
H1:L.lt (elements s1) (elements s2)

lt s1 s2
s1, s2:tree
H:Ok s1
H0:Ok s2
H1:L.lt (elements s2) (elements s1)
lt s2 s1
s1, s2:tree
H:Ok s1
H0:Ok s2
H1:L.lt (elements s2) (elements s1)

lt s2 s1
intros; exists s2, s1; repeat split; auto. Qed.

Equality test


forall s1 s2 : tree, Ok s1 -> Ok s2 -> equal s1 s2 = true <-> eq s1 s2

forall s1 s2 : tree, Ok s1 -> Ok s2 -> equal s1 s2 = true <-> eq s1 s2
s1, s2:tree
B1:Ok s1
B2:Ok s2

match compare s1 s2 with | Eq => true | _ => false end = true <-> eq s1 s2
s1, s2:tree
B1:Ok s1
B2:Ok s2
H:lt s1 s2
H':eq s1 s2

false = true
s1, s2:tree
B1:Ok s1
B2:Ok s2
H:lt s2 s1
H':eq s1 s2
false = true
s1, s2:tree
B1:Ok s1
B2:Ok s2
H:lt s2 s2
H':eq s1 s2

false = true
s1, s2:tree
B1:Ok s1
B2:Ok s2
H:lt s2 s1
H':eq s1 s2
false = true
s1, s2:tree
B1:Ok s1
B2:Ok s2
H:lt s2 s1
H':eq s1 s2

false = true
s1, s2:tree
B1:Ok s1
B2:Ok s2
H:lt s2 s2
H':eq s1 s2

false = true
elim (StrictOrder_Irreflexive s2); auto. Qed.

A few results about mindepth and maxdepth

s:tree

mindepth s <= maxdepth s
s:tree

mindepth s <= maxdepth s
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:mindepth s1 <= maxdepth s1
IHs2:mindepth s2 <= maxdepth s2

S (Init.Nat.min (mindepth s1) (mindepth s2)) <= S (Init.Nat.max (maxdepth s1) (maxdepth s2))
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:mindepth s1 <= maxdepth s1
IHs2:mindepth s2 <= maxdepth s2

Init.Nat.min (mindepth s1) (mindepth s2) <= Init.Nat.max (maxdepth s1) (maxdepth s2)
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:mindepth s1 <= maxdepth s1
IHs2:mindepth s2 <= maxdepth s2

Init.Nat.min (mindepth s1) (mindepth s2) <= mindepth s1
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:mindepth s1 <= maxdepth s1
IHs2:mindepth s2 <= maxdepth s2
mindepth s1 <= Init.Nat.max (maxdepth s1) (maxdepth s2)
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:mindepth s1 <= maxdepth s1
IHs2:mindepth s2 <= maxdepth s2

mindepth s1 <= Init.Nat.max (maxdepth s1) (maxdepth s2)
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:mindepth s1 <= maxdepth s1
IHs2:mindepth s2 <= maxdepth s2

mindepth s1 <= maxdepth s1
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:mindepth s1 <= maxdepth s1
IHs2:mindepth s2 <= maxdepth s2
maxdepth s1 <= Init.Nat.max (maxdepth s1) (maxdepth s2)
t:Info.t
s1:tree
t0:X.t
s2:tree
IHs1:mindepth s1 <= maxdepth s1
IHs2:mindepth s2 <= maxdepth s2

maxdepth s1 <= Init.Nat.max (maxdepth s1) (maxdepth s2)
apply Nat.le_max_l. Qed.
s:tree

cardinal s < 2 ^ maxdepth s
s:tree

cardinal s < 2 ^ maxdepth s
s:tree

S (cardinal s) <= 2 ^ maxdepth s

S (cardinal Leaf) <= 2 ^ maxdepth Leaf
c:Info.t
l:tree
x:X.t
r:tree
IHl:S (cardinal l) <= 2 ^ maxdepth l
IHr:S (cardinal r) <= 2 ^ maxdepth r
S (cardinal (Node c l x r)) <= 2 ^ maxdepth (Node c l x r)

S (cardinal Leaf) <= 2 ^ maxdepth Leaf
auto.
c:Info.t
l:tree
x:X.t
r:tree
IHl:S (cardinal l) <= 2 ^ maxdepth l
IHr:S (cardinal r) <= 2 ^ maxdepth r

S (cardinal (Node c l x r)) <= 2 ^ maxdepth (Node c l x r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:S (cardinal l) <= 2 ^ maxdepth l
IHr:S (cardinal r) <= 2 ^ maxdepth r

S (S (cardinal l + cardinal r)) <= 2 ^ Init.Nat.max (maxdepth l) (maxdepth r) + (2 ^ Init.Nat.max (maxdepth l) (maxdepth r) + 0)
c:Info.t
l:tree
x:X.t
r:tree
IHl:S (cardinal l) <= 2 ^ maxdepth l
IHr:S (cardinal r) <= 2 ^ maxdepth r

S (cardinal l) + S (cardinal r) <= 2 ^ Init.Nat.max (maxdepth l) (maxdepth r) + 2 ^ Init.Nat.max (maxdepth l) (maxdepth r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:S (cardinal l) <= 2 ^ maxdepth l
IHr:S (cardinal r) <= 2 ^ maxdepth r

maxdepth l <= Init.Nat.max (maxdepth l) (maxdepth r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:S (cardinal l) <= 2 ^ maxdepth l
IHr:S (cardinal r) <= 2 ^ maxdepth r
maxdepth r <= Init.Nat.max (maxdepth l) (maxdepth r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:S (cardinal l) <= 2 ^ maxdepth l
IHr:S (cardinal r) <= 2 ^ maxdepth r

maxdepth l <= Init.Nat.max (maxdepth l) (maxdepth r)
apply Nat.le_max_l.
c:Info.t
l:tree
x:X.t
r:tree
IHl:S (cardinal l) <= 2 ^ maxdepth l
IHr:S (cardinal r) <= 2 ^ maxdepth r

maxdepth r <= Init.Nat.max (maxdepth l) (maxdepth r)
apply Nat.le_max_r. Qed.
s:tree

2 ^ mindepth s <= S (cardinal s)
s:tree

2 ^ mindepth s <= S (cardinal s)
s:tree

2 ^ mindepth s <= S (cardinal s)

2 ^ mindepth Leaf <= S (cardinal Leaf)
c:Info.t
l:tree
x:X.t
r:tree
IHl:2 ^ mindepth l <= S (cardinal l)
IHr:2 ^ mindepth r <= S (cardinal r)
2 ^ mindepth (Node c l x r) <= S (cardinal (Node c l x r))

2 ^ mindepth Leaf <= S (cardinal Leaf)
auto.
c:Info.t
l:tree
x:X.t
r:tree
IHl:2 ^ mindepth l <= S (cardinal l)
IHr:2 ^ mindepth r <= S (cardinal r)

2 ^ mindepth (Node c l x r) <= S (cardinal (Node c l x r))
c:Info.t
l:tree
x:X.t
r:tree
IHl:2 ^ mindepth l <= S (cardinal l)
IHr:2 ^ mindepth r <= S (cardinal r)

2 ^ Init.Nat.min (mindepth l) (mindepth r) + (2 ^ Init.Nat.min (mindepth l) (mindepth r) + 0) <= S (S (cardinal l + cardinal r))
c:Info.t
l:tree
x:X.t
r:tree
IHl:2 ^ mindepth l <= S (cardinal l)
IHr:2 ^ mindepth r <= S (cardinal r)

2 ^ Init.Nat.min (mindepth l) (mindepth r) + 2 ^ Init.Nat.min (mindepth l) (mindepth r) <= S (cardinal l) + S (cardinal r)
c:Info.t
l:tree
x:X.t
r:tree
IHl:2 ^ mindepth l <= S (cardinal l)
IHr:2 ^ mindepth r <= S (cardinal r)

Init.Nat.min (mindepth l) (mindepth r) <= mindepth l
c:Info.t
l:tree
x:X.t
r:tree
IHl:2 ^ mindepth l <= S (cardinal l)
IHr:2 ^ mindepth r <= S (cardinal r)
Init.Nat.min (mindepth l) (mindepth r) <= mindepth r
c:Info.t
l:tree
x:X.t
r:tree
IHl:2 ^ mindepth l <= S (cardinal l)
IHr:2 ^ mindepth r <= S (cardinal r)

Init.Nat.min (mindepth l) (mindepth r) <= mindepth l
apply Nat.le_min_l.
c:Info.t
l:tree
x:X.t
r:tree
IHl:2 ^ mindepth l <= S (cardinal l)
IHr:2 ^ mindepth r <= S (cardinal r)

Init.Nat.min (mindepth l) (mindepth r) <= mindepth r
apply Nat.le_min_r. Qed.
s:tree

s <> Leaf -> Nat.log2 (cardinal s) < maxdepth s
s:tree

s <> Leaf -> Nat.log2 (cardinal s) < maxdepth s
s:tree
H:s <> Leaf

Nat.log2 (cardinal s) < maxdepth s
s:tree
H:s <> Leaf

0 < cardinal s
s:tree
H:s <> Leaf
cardinal s < 2 ^ maxdepth s
s:tree
H:s <> Leaf

cardinal s < 2 ^ maxdepth s
apply maxdepth_cardinal. Qed.
s:tree

mindepth s <= Nat.log2 (S (cardinal s))
s:tree

mindepth s <= Nat.log2 (S (cardinal s))
s:tree

0 < S (cardinal s)
s:tree
2 ^ mindepth s <= S (cardinal s)
s:tree

2 ^ mindepth s <= S (cardinal s)
apply mindepth_cardinal. Qed. End Props.