datatype AVLTree where
| Node(AVLTree, Int, AVLTree, Int) // node of (left, key, right, height)
| Empty // empty tree
end

function get_height(tree: AVLTree) -> Int
begin
    match tree with
    | Node(_left, _key, _right, height) => height
    | Empty => 0
    end
end

function balance_factor(tree: AVLTree) -> Int
begin
    match tree with
    | Node(left, _key, right, _height) => get_height(left) - get_height(right)
    | Empty => 0
    end
end

function new_node(left: AVLTree, key: Int, right: AVLTree) -> AVLTree
begin
    let left_height = get_height(left);
    let right_height = get_height(right);
    if left_height < right_height then
        Node(left, key, right, right_height + 1)
    else
        Node(left, key, right, left_height + 1)
end

function insert(tree: AVLTree, x: Int) -> AVLTree
begin
    match tree with
    | Node(left, y, right, _height) =>
        condition
        | x < y =>
            rebalance(new_node(insert(left, x), y, right))
        | x > y =>
            rebalance(new_node(left, y, insert(right, x)))
        | x == y =>
            tree
        end
    | Empty => Node(Empty, x, Empty, 1)
    end
end

function rebalance(tree: AVLTree) -> AVLTree
begin
    let bf = balance_factor(tree);
    condition
    | bf >= -1 && bf <= 1 =>
        tree
    | bf <= -2 =>
        let Node(left, x, right, _height) = tree;
        if balance_factor(right) <= 0 then
            rotate_left(tree)
        else
            rotate_left(new_node(left, x, rotate_right(right)))
    | bf >= 2 =>
        let Node(left, x, right, _height) = tree;
        if balance_factor(left) >= 0 then
            rotate_right(tree)
        else
            rotate_right(new_node(rotate_left(left), x, right))
    end
end

function rotate_left(tree: AVLTree) -> AVLTree
begin
    let Node(left, key, Node(r_left, r_key, r_right, _), _) = tree;
    new_node(new_node(left, key, r_left), r_key, r_right)
end

function rotate_right(tree: AVLTree) -> AVLTree
begin
    let Node(Node(l_left, l_key, l_right, _), key, right, _) = tree;
    new_node(l_left, l_key, new_node(l_right, key, right))
end

function is_balanced(tree: AVLTree) -> Bool
begin
    match tree with
    | Node(left, _key, right, height) =>
        if is_balanced(left) && is_balanced(right) then
            let left_height = get_height(left);
            let right_height = get_height(right);
            if left_height < right_height then
                (height == right_height + 1) && (right_height - left_height <= 1)
            else
                (height == left_height + 1) && (left_height - right_height <= 1)
        else
            false 
    | Empty => true
    end
end

function is_sorted(tree: AVLTree) -> Bool
begin
    match tree with
    | Node(left, x, right, _height) =>
        is_sorted_max(left, x) && is_sorted_min(right, x)
    | Empty => true
    end
end

function is_sorted_min(tree: AVLTree, min: Int) -> Bool
begin
    match tree with
    | Node(left, x, right, _height) =>
        x > min &&
        is_sorted_min_max(left, min, x) && is_sorted_min(right, x)
    | Empty => true
    end
end

function is_sorted_max(tree: AVLTree, max: Int) -> Bool
begin
    match tree with
    | Node(left, x, right, _height) =>
        x < max &&
        is_sorted_max(left, x) && is_sorted_min_max(right, x, max)
    | Empty => true
    end
end

function is_sorted_min_max(tree: AVLTree, min: Int, max: Int) -> Bool
begin
    match tree with
    | Node(left, x, right, _height) =>
        x > min && x < max &&
        is_sorted_min_max(left, min, x) && is_sorted_min_max(right, x, max)
    | Empty => true
    end
end

function keep_sorted_and_balanced(tree: AVLTree, x: Int)
begin
    guard is_sorted(tree);
    guard is_balanced(tree);
    let res = insert(tree, x);
    alternative
    | guard !is_sorted(res);
    | guard !is_balanced(res);
    end
end

query keep_sorted_and_balanced(depth_step=5, depth_limit=50, answer_limit=1)