(* This code extends 'mini_prelude'. *)

datatype ('a) heap = 
    Tree of 'a * ('a) heap * ('a) heap 
  | Empty ;

val empty = Empty ;

val is_empty = 
  (fn v4 => 
    (case v4 of 
        Empty => true 
      | (Tree (v3, v2, v1)) => false)) ;

fun merge v18 = 
  (fn v19 => 
    (fn v16 => 
      (fn v17 => 
        (case v16 of 
            Empty => 
              (case v17 of 
                  Empty => Empty 
                | (Tree (v3, v2, v1)) => (Tree (v3, v2, v1))) 
          | (Tree (v15, v14, v13)) => 
              (case v17 of 
                  Empty => (Tree (v15, v14, v13)) 
                | (Tree (v12, v11, v10)) => 
                    (if ((v19 (v18 v15)) (v18 v12)) 
                    then 
                      (case v14 of 
                          Empty => (Tree (v15, (Tree (v12, v11, v10)), v13)) 
                        | (Tree (v6, v5, v4)) => (Tree (v15, Empty, ((((merge v18) v19) ((((merge v18) v19) (Tree (v12, v11, v10))) v14)) v13)))) 
                    else 
                      (case v11 of 
                          Empty => (Tree (v12, (Tree (v15, v14, v13)), v10)) 
                        | (Tree (v9, v8, v7)) => (Tree (v12, Empty, ((((merge v18) v19) ((((merge v18) v19) (Tree (v15, v14, v13))) v11)) v10)))))))))) ;

val insert = 
  (fn v2 => 
    (fn v3 => 
      (fn v4 => 
        (fn v1 => ((((merge v2) v3) (Tree (v4, Empty, Empty))) v1))))) ;

val find_min = 
  (fn x1 => 
    (case x1 of 
        Empty => (raise Bind) 
      | (Tree (v3, v2, v1)) => v3)) ;

val delete_min = 
  (fn x1 => 
    (fn x2 => 
      (fn x3 => 
        (case x3 of 
            Empty => (raise Bind) 
          | (Tree (v3, v2, v1)) => ((((merge x1) x2) v2) v1))))) ;