Predicate program of insertion into AVL-tree

The AVL-tree operators are usually presented in functional languages in compact and elegant stile. However functional programs for insertion and removal operators are ineffective. They implement the construction of new tree but not the modification of the source tree. The paper describes the predicate programs for two algorithms of insertions into an AVL-tree. The predicate program can be automatically transformed to effective imperative programs.