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

datatype OptionInt where
| Some(Int)
| None
end

function is_balanced(tree: AVLTree) -> Bool
begin
    match is_balanced_help(tree) with
    | Some(_) => true 
    | None => false
    end
end

function is_balanced_help(tree: AVLTree) -> OptionInt
begin
    match tree with
    | Node(left, _, right) => 
        match (is_balanced_help(left), is_balanced_help(right)) with
        | (Some(left_height), Some(right_height)) =>
            let diff_height = left_height - right_height;
            if diff_height >= -1 && diff_height <= 1 then
                if left_height < right_height then 
                    Some(right_height + 1)
                else
                    Some(left_height + 1)
            else
                None
        | (None, _) => None
        | (_, None) => None
        end
    | Empty => Some(0)
    end
end

function is_sorted(tree: AVLTree) -> Bool
begin
    match tree with
    | Node(left, x, right) =>
        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) =>
        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) =>
        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) =>
        x > min && x < max &&
        is_sorted_min_max(left, min, x) && is_sorted_min_max(right, x, max)
    | Empty => true
    end
end

function gen_sorted_balanced(tree: AVLTree)
begin
    guard is_sorted(tree);
    guard is_balanced(tree);
end

query gen_sorted_balanced(depth_step=5, depth_limit=70)