Library prelude.bintree
Inductive bintree:Set :=
Leaf : bintree
| Bin : bintree -> bintree -> bintree.
Inductive unit : Set := void.
Definition decompose : bintree -> unit + bintree * bintree.
intro t;case t.
left.
constructor.
intros t1 t2;right;exact (pair t1 t2).
Defined.
Definition compose : ( unit + bintree * bintree) -> bintree.
destruct 1.
exact Leaf.
case p. intros t1 t2;exact (Bin t1 t2).
Defined.
Lemma bij : forall t, compose (decompose t)=t.
destruct t;simpl;auto.
Qed.
Lemma bijR : forall t:( unit + bintree * bintree), decompose (compose t)=t.
destruct t.
simpl.
case u.
trivial.
simpl;auto.
case p.
simpl;auto.
Qed.
Definition K (n p:nat) := (n+p)*(S (n +p)).
Definition shift_n_omega_l (n:nat) (i:nat) := i.
Definition shift_n_omega_r (n:nat) (i:nat) := (S (i + n)).
Fixpoint tree_nat (t:bintree) : nat :=
match t with Leaf => shift_n_omega_l 0 0
| Bin t1 t2 => shift_n_omega_r 0 (K (tree_nat t1) (tree_nat t2))
end.
Eval compute in (tree_nat Leaf).
Eval compute in (tree_nat (Bin Leaf Leaf)).
Eval compute in (tree_nat (Bin Leaf (Bin Leaf Leaf))).