(* This code extends 'mini_prelude'. *)

val empty = Nil ;

val is_empty = 
  (fn v3 => 
    (case v3 of 
        Nil => true 
      | (Cons (v2, v1)) => false)) ;

datatype ('a) tree = 
    Node of int * 'a * (('a) tree) list ;

val rank = 
  (fn v4 => 
    (case v4 of 
        (Node (v3, v2, v1)) => v3)) ;

val root = 
  (fn v4 => 
    (case v4 of 
        (Node (v3, v2, v1)) => v2)) ;

val link = 
  (fn v8 => 
    (fn v9 => 
      (fn v10 => 
        (fn v7 => 
          (case v10 of 
              (Node (v6, v5, v4)) => 
                (case v7 of 
                    (Node (v3, v2, v1)) => 
                      (if ((v9 (v8 v5)) (v8 v2)) 
                      then (Node ((v6 + 1), v5, (Cons ((Node (v3, v2, v1)), v4)))) 
                      else (Node ((v6 + 1), v2, (Cons ((Node (v6, v5, v4)), v1))))))))))) ;

fun ins_tree v3 = 
  (fn v4 => 
    (fn v5 => 
      (fn v6 => 
        (case v6 of 
            Nil => (Cons (v5, Nil)) 
          | (Cons (v2, v1)) => 
              (if ((rank v5) < (rank v2)) 
              then (Cons (v5, (Cons (v2, v1)))) 
              else ((((ins_tree v3) v4) ((((link v3) v4) v5) v2)) v1)))))) ;

val insert = 
  (fn v1 => 
    (fn v2 => 
      (fn v4 => 
        (fn v3 => ((((ins_tree v1) v2) (Node (0, v4, Nil))) v3))))) ;

fun merge v8 = 
  (fn v9 => 
    (fn v10 => 
      (fn v7 => 
        (case v10 of 
            Nil => 
              (case v7 of 
                  Nil => Nil 
                | (Cons (v2, v1)) => (Cons (v2, v1))) 
          | (Cons (v6, v5)) => 
              (case v7 of 
                  Nil => (Cons (v6, v5)) 
                | (Cons (v4, v3)) => 
                    (if ((rank v6) < (rank v4)) 
                    then (Cons (v6, ((((merge v8) v9) v5) (Cons (v4, v3))))) 
                    else 
                      (if ((rank v4) < (rank v6)) 
                      then (Cons (v4, ((((merge v8) v9) (Cons (v6, v5))) v3))) 
                      else ((((ins_tree v8) v9) ((((link v8) v9) v6) v4)) ((((merge v8) v9) v5) v3))))))))) ;

fun remove_min_tree x = 
  (fn x1 => 
    (fn x2 => 
      (case x2 of 
          Nil => (raise Bind) 
        | (Cons (v7, v6)) => 
            (case v6 of 
                Nil => (Pair (v7, Nil)) 
              | (Cons (v5, v4)) => 
                  let val v3 = (((remove_min_tree x) x1) (Cons (v5, v4))) 
                  in 
                    (case v3 of 
                        (Pair (v2, v1)) => 
                          (if ((x1 (x (root v7))) (x (root v2))) 
                          then (Pair (v7, (Cons (v5, v4)))) 
                          else (Pair (v2, (Cons (v7, v1)))))) 
                  end )))) ;

val find_min = 
  (fn v4 => 
    (fn v5 => 
      (fn v6 => 
        let val v3 = (((remove_min_tree v4) v5) v6) 
        in 
          (case v3 of 
              (Pair (v2, v1)) => (root v2)) 
        end ))) ;

val delete_min = 
  (fn v6 => 
    (fn v7 => 
      (fn v8 => 
        (case (((remove_min_tree v6) v7) v8) of 
            (Pair (v5, v4)) => 
              (case v5 of 
                  (Node (v3, v2, v1)) => ((((merge v6) v7) (REVERSE v1)) v4)))))) ;