This translation extends 'mini_prelude'.

Definition of refinement invariant:

|- (HEAP_TYPE a (Tree x_2 x_1) v ⇔
    ∃v2_1 v2_2.
      (v = Conv "Tree" [v2_1; v2_2]) ∧ a x_2 v2_1 ∧
      LIST_TYPE (HEAP_TYPE a) x_1 v2_2) ∧
   (HEAP_TYPE a Empty v ⇔ (v = Conv "Empty" []))

Certificate theorem for empty:

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

Certificate theorem for is_empty:

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

Certificate theorem for merge:

|- DeclAssum PairingHeap_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 PairingHeap_decls env ⇒
   Eval env (Var "insert")
     (((a --> b) --> (b --> b --> BOOL) --> a --> HEAP_TYPE a -->
       HEAP_TYPE a) insert)

Certificate theorem for merge_pairs:

|- DeclAssum PairingHeap_decls env ⇒
   Eval env (Var "merge_pairs")
     (((a --> b) --> (b --> b --> BOOL) --> LIST_TYPE (HEAP_TYPE a) -->
       HEAP_TYPE a) merge_pairs)

Certificate theorem for find_min:

|- DeclAssum PairingHeap_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 ∧ ∃v1 v0. v2 = Tree v1 v0

Certificate theorem for delete_min:

|- DeclAssum PairingHeap_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 v5 v4 v3 ⇔ (∃v2 v1. v3 = Tree v2 v1) ∧ v3 ≠ Empty

Definition of declaration list:

|- PairingHeap_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",[Tvar "a"; Tapp [Tapp [Tvar "a"] "heap"] "list"]);
         ("Empty",[])])]; Dlet (Pvar "empty") (Con "Empty" []);
    Dlet (Pvar "is_empty")
      (Fun "v3"
         (Mat (Var "v3")
            [(Pcon "Empty" [],Val (Lit (Bool T)));
             (Pcon "Tree" [Pvar "v2"; Pvar "v1"],Val (Lit (Bool F)))]));
    Dlet (Pvar "merge")
      (Fun "v8"
         (Fun "v9"
            (Fun "v10"
               (Fun "v7"
                  (Mat (Var "v10")
                     [(Pcon "Empty" [],
                       Mat (Var "v7")
                         [(Pcon "Empty" [],Con "Empty" []);
                          (Pcon "Tree" [Pvar "v2"; Pvar "v1"],
                           Con "Tree" [Var "v2"; Var "v1"])]);
                      (Pcon "Tree" [Pvar "v6"; Pvar "v5"],
                       Mat (Var "v7")
                         [(Pcon "Empty" [],
                           Con "Tree" [Var "v6"; Var "v5"]);
                          (Pcon "Tree" [Pvar "v4"; Pvar "v3"],
                           If
                             (App Opapp
                                (App Opapp (Var "v9")
                                   (App Opapp (Var "v8") (Var "v6")))
                                (App Opapp (Var "v8") (Var "v4")))
                             (Con "Tree"
                                [Var "v6";
                                 Con "Cons"
                                   [Con "Tree" [Var "v4"; Var "v3"];
                                    Var "v5"]])
                             (Con "Tree"
                                [Var "v4";
                                 Con "Cons"
                                   [Con "Tree" [Var "v6"; Var "v5"];
                                    Var "v3"]]))])])))));
    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" [Var "v4"; Con "Nil" []]))
                     (Var "v2"))))));
    Dletrec
      [("merge_pairs","v5",
        Fun "v6"
          (Fun "v7"
             (Mat (Var "v7")
                [(Pcon "Nil" [],Con "Empty" []);
                 (Pcon "Cons" [Pvar "v4"; Pvar "v3"],
                  Mat (Var "v3")
                    [(Pcon "Nil" [],Var "v4");
                     (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                      App Opapp
                        (App Opapp
                           (App Opapp
                              (App Opapp (Var "merge") (Var "v5"))
                              (Var "v6"))
                           (App Opapp
                              (App Opapp
                                 (App Opapp
                                    (App Opapp (Var "merge") (Var "v5"))
                                    (Var "v6")) (Var "v4")) (Var "v2")))
                        (App Opapp
                           (App Opapp
                              (App Opapp (Var "merge_pairs") (Var "v5"))
                              (Var "v6")) (Var "v1")))])])))];
    Dlet (Pvar "find_min")
      (Fun "x1"
         (Mat (Var "x1")
            [(Pcon "Empty" [],Raise Bind_error);
             (Pcon "Tree" [Pvar "v2"; Pvar "v1"],Var "v2")]));
    Dlet (Pvar "delete_min")
      (Fun "x1"
         (Fun "x2"
            (Fun "x3"
               (Mat (Var "x3")
                  [(Pcon "Empty" [],Raise Bind_error);
                   (Pcon "Tree" [Pvar "v2"; Pvar "v1"],
                    App Opapp
                      (App Opapp
                         (App Opapp (Var "merge_pairs") (Var "x1"))
                         (Var "x2")) (Var "v1"))]))))]