proposition: Lemma join_avl_1 : forall l x d r, avl l -> avl r -> avl (join l x d r) /\ 0<= height (join l x d r) - max (height l) (height r) <= 1.
proof: Proof. join_tac. - split; simpl; auto. destruct (add_avl_1 x d H0). avl_nns; omega_max. - set (l:=Node ll lx ld lr lh) in *. split; auto. destruct (add_avl_1 x d H). simpl (height (Leaf elt)). avl_nns; omega_max. - inversion_clear H. assert (height (Node rl rx rd rr rh) = rh); auto. set (r := Node rl rx rd rr rh) in *; clearbody r. destruct (Hlr x d r H2 H0); clear Hrl Hlr. set (j := join lr x d r) in *; clearbody j. simpl. assert (-(3) <= height ll - height j <= 3) by omega_max. split. + apply bal_avl; auto. + omega_bal. - inversion_clear H0. assert (height (Node ll lx ld lr lh) = lh); auto. set (l := Node ll lx ld lr lh) in *; clearbody l. destruct (Hrl H H1); clear Hrl Hlr. set (j := join l x d rl) in *; clearbody j. simpl. assert (-(3) <= height j - height rr <= 3) by omega_max. split. + apply bal_avl; auto. + omega_bal. - clear Hrl Hlr. assert (height (Node ll lx ld lr lh) = lh); auto. assert (height (Node rl rx rd rr rh) = rh); auto. set (l := Node ll lx ld lr lh) in *; clearbody l. set (r := Node rl rx rd rr rh) in *; clearbody r. assert (-(2) <= height l - height r <= 2) by omega_max. split. + apply create_avl; auto. + rewrite create_height; auto; omega_max. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia