This translation extends 'mini_prelude'.

Definition of refinement invariant:

|- (∀a x_4 x_3 x_2 x_1 v.
      HEAP_TYPE a (Tree x_4 x_3 x_2 x_1) v ⇔
      ∃v2_1 v2_2 v2_3 v2_4.
        (v = Conv "Tree" [v2_1; v2_2; v2_3; v2_4]) ∧ NUM x_4 v2_1 ∧
        a x_3 v2_2 ∧ HEAP_TYPE a x_2 v2_3 ∧ HEAP_TYPE a x_1 v2_4) ∧
   ∀a v. HEAP_TYPE a Empty v ⇔ (v = Conv "Empty" [])

Certificate theorem for rank:

|- DeclAssum LeftistHeap_decls env ⇒
   Eval env (Var "rank") ((HEAP_TYPE a --> NUM) rank)

Certificate theorem for make_node:

|- DeclAssum LeftistHeap_decls env ⇒
   Eval env (Var "make_node")
     ((a --> HEAP_TYPE a --> HEAP_TYPE a --> HEAP_TYPE a) make_node)

Certificate theorem for empty:

|- DeclAssum LeftistHeap_decls env ⇒
   Eval env (Var "empty") (HEAP_TYPE a empty)

Certificate theorem for is_empty:

|- DeclAssum LeftistHeap_decls env ⇒
   Eval env (Var "is_empty") ((HEAP_TYPE a --> BOOL) is_empty)

Certificate theorem for merge:

|- DeclAssum LeftistHeap_decls env ⇒
   Eval env (Var "merge")
     (((a --> b) --> (b --> b --> BOOL) --> HEAP_TYPE a -->
       HEAP_TYPE a --> HEAP_TYPE a) merge)

Certificate theorem for insert:

|- DeclAssum LeftistHeap_decls env ⇒
   Eval env (Var "insert")
     (((a --> b) --> (b --> b --> BOOL) --> a --> HEAP_TYPE a -->
       HEAP_TYPE a) insert)

Certificate theorem for find_min:

|- DeclAssum LeftistHeap_decls env ∧ find_min_side x1 ⇒
   Eval env (Var "find_min") ((Eq (HEAP_TYPE a) x1 --> a) find_min)

Definition of side condition for find_min:

|- find_min_side v2 ⇔
   v2 ≠ Empty ∧ ∃v0 v1 v1' v2'. v2 = Tree v0 v1 v1' v2'

Certificate theorem for delete_min:

|- DeclAssum LeftistHeap_decls env ∧ delete_min_side x1 x2 x3 ⇒
   Eval env (Var "delete_min")
     ((Eq (a --> b) x1 --> Eq (b --> b --> BOOL) x2 -->
       Eq (HEAP_TYPE a) x3 --> HEAP_TYPE a) delete_min)

Definition of side condition for delete_min:

|- delete_min_side v6 v5 v4 ⇔
   (∃v0 v3 v2 v1. v4 = Tree v0 v3 v2 v1) ∧ v4 ≠ Empty

Definition of declaration list:

|- LeftistHeap_decls =
   [Dtype [(["a"; "b"],"prod",[("Pair",[Tvar "a"; Tvar "b"])])];
    Dtype
      [(["a"],"list",
        [("Cons",[Tvar "a"; Tapp [Tvar "a"] "list"]); ("Nil",[])])];
    Dlet (Pvar "HD")
      (Fun "x1"
         (Mat (Var "x1")
            [(Pcon "Nil" [],Raise Bind_error);
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v2")]));
    Dlet (Pvar "TL")
      (Fun "x1"
         (Mat (Var "x1")
            [(Pcon "Nil" [],Raise Bind_error);
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v1")]));
    Dletrec
      [("APPEND","v3",
        Fun "v4"
          (Mat (Var "v3")
             [(Pcon "Nil" [],Var "v4");
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               Con "Cons"
                 [Var "v2";
                  App Opapp (App Opapp (Var "APPEND") (Var "v1"))
                    (Var "v4")])]))];
    Dletrec
      [("REV","v3",
        Fun "v4"
          (Mat (Var "v3")
             [(Pcon "Nil" [],Var "v4");
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               App Opapp (App Opapp (Var "REV") (Var "v1"))
                 (Con "Cons" [Var "v2"; Var "v4"]))]))];
    Dlet (Pvar "REVERSE")
      (Fun "v1"
         (App Opapp (App Opapp (Var "REV") (Var "v1")) (Con "Nil" [])));
    Dtype
      [(["a"],"heap",
        [("Tree",
          [Tnum; Tvar "a"; Tapp [Tvar "a"] "heap";
           Tapp [Tvar "a"] "heap"]); ("Empty",[])])];
    Dlet (Pvar "rank")
      (Fun "v5"
         (Mat (Var "v5")
            [(Pcon "Empty" [],Val (Lit (IntLit 0)));
             (Pcon "Tree" [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
              Var "v4")]));
    Dlet (Pvar "make_node")
      (Fun "v3"
         (Fun "v1"
            (Fun "v2"
               (If
                  (App (Opb Geq) (App Opapp (Var "rank") (Var "v1"))
                     (App Opapp (Var "rank") (Var "v2")))
                  (Con "Tree"
                     [App (Opn Plus) (App Opapp (Var "rank") (Var "v2"))
                        (Val (Lit (IntLit 1))); Var "v3"; Var "v1";
                      Var "v2"])
                  (Con "Tree"
                     [App (Opn Plus) (App Opapp (Var "rank") (Var "v1"))
                        (Val (Lit (IntLit 1))); Var "v3"; Var "v2";
                      Var "v1"])))));
    Dlet (Pvar "empty") (Con "Empty" []);
    Dlet (Pvar "is_empty")
      (Fun "v5"
         (Mat (Var "v5")
            [(Pcon "Empty" [],Val (Lit (Bool T)));
             (Pcon "Tree" [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
              Val (Lit (Bool F)))]));
    Dletrec
      [("merge","v13",
        Fun "v14"
          (Fun "v15"
             (Fun "v16"
                (Mat (Var "v15")
                   [(Pcon "Empty" [],
                     Mat (Var "v16")
                       [(Pcon "Empty" [],Con "Empty" []);
                        (Pcon "Tree"
                           [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
                         Con "Tree"
                           [Var "v4"; Var "v3"; Var "v2"; Var "v1"])]);
                    (Pcon "Tree"
                       [Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"],
                     Mat (Var "v16")
                       [(Pcon "Empty" [],
                         Con "Tree"
                           [Var "v12"; Var "v11"; Var "v10"; Var "v9"]);
                        (Pcon "Tree"
                           [Pvar "v8"; Pvar "v7"; Pvar "v6"; Pvar "v5"],
                         If
                           (App Opapp
                              (App Opapp (Var "v14")
                                 (App Opapp (Var "v13") (Var "v11")))
                              (App Opapp (Var "v13") (Var "v7")))
                           (App Opapp
                              (App Opapp
                                 (App Opapp (Var "make_node")
                                    (Var "v11")) (Var "v10"))
                              (App Opapp
                                 (App Opapp
                                    (App Opapp
                                       (App Opapp (Var "merge")
                                          (Var "v13")) (Var "v14"))
                                    (Var "v9"))
                                 (Con "Tree"
                                    [Var "v8"; Var "v7"; Var "v6";
                                     Var "v5"])))
                           (App Opapp
                              (App Opapp
                                 (App Opapp (Var "make_node")
                                    (Var "v7")) (Var "v6"))
                              (App Opapp
                                 (App Opapp
                                    (App Opapp
                                       (App Opapp (Var "merge")
                                          (Var "v13")) (Var "v14"))
                                    (Con "Tree"
                                       [Var "v12"; Var "v11"; Var "v10";
                                        Var "v9"]))
                                 (Var "v5"))))])]))))];
    Dlet (Pvar "insert")
      (Fun "v1"
         (Fun "v3"
            (Fun "v4"
               (Fun "v2"
                  (App Opapp
                     (App Opapp
                        (App Opapp (App Opapp (Var "merge") (Var "v1"))
                           (Var "v3"))
                        (Con "Tree"
                           [Val (Lit (IntLit 1)); Var "v4";
                            Con "Empty" []; Con "Empty" []]))
                     (Var "v2"))))));
    Dlet (Pvar "find_min")
      (Fun "x1"
         (Mat (Var "x1")
            [(Pcon "Empty" [],Raise Bind_error);
             (Pcon "Tree" [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
              Var "v3")]));
    Dlet (Pvar "delete_min")
      (Fun "x1"
         (Fun "x2"
            (Fun "x3"
               (Mat (Var "x3")
                  [(Pcon "Empty" [],Raise Bind_error);
                   (Pcon "Tree"
                      [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
                    App Opapp
                      (App Opapp
                         (App Opapp (App Opapp (Var "merge") (Var "x1"))
                            (Var "x2")) (Var "v2")) (Var "v1"))]))))]