This translation extends 'mini_prelude'.

Certificate theorem for mrg:

|- DeclAssum BottomUpMergeSort_decls env ⇒
   Eval env (Var "mrg")
     (((a --> a --> BOOL) --> LIST_TYPE a --> LIST_TYPE a -->
       LIST_TYPE a) mrg)

Certificate theorem for empty:

|- DeclAssum BottomUpMergeSort_decls env ⇒
   Eval env (Var "empty") (PAIR_TYPE INT (LIST_TYPE a) empty)

Certificate theorem for add_seg:

|- DeclAssum BottomUpMergeSort_decls env ∧ add_seg_side v1 v2 v3 v4 ⇒
   Eval env (Var "add_seg")
     ((Eq (a --> a --> BOOL) v1 --> Eq (LIST_TYPE a) v2 -->
       Eq (LIST_TYPE (LIST_TYPE a)) v3 --> Eq NUM v4 -->
       LIST_TYPE (LIST_TYPE a)) add_seg)

Definition of side condition for add_seg:

|- add_seg_side v1 v2 v3 v4 ⇔
   PRECONDITION T ∧
   ∀v__1.
     (v4 MOD 2 = SUC v__1) ⇒
     (PRECONDITION
        (add_seg_side v1 (mrg v1 v2 (HD v3)) (TL v3) (v4 DIV 2)) ∧
      PRECONDITION T) ∧ PRECONDITION (v3 ≠ [])

Certificate theorem for add:

|- DeclAssum BottomUpMergeSort_decls env ∧ add_side v3 v4 v5 ⇒
   Eval env (Var "add")
     ((Eq (a --> a --> BOOL) v3 --> Eq a v4 -->
       Eq (PAIR_TYPE NUM (LIST_TYPE (LIST_TYPE a))) v5 -->
       PAIR_TYPE NUM (LIST_TYPE (LIST_TYPE a))) add)

Definition of side condition for add:

|- add_side v3 v4 v5 ⇔
   ∀v2 v1. (v5 = (v2,v1)) ⇒ add_seg_side v3 [v4] v1 v2

Certificate theorem for mrg_all:

|- DeclAssum BottomUpMergeSort_decls env ⇒
   Eval env (Var "mrg_all")
     (((a --> a --> BOOL) --> LIST_TYPE a -->
       LIST_TYPE (LIST_TYPE a) --> LIST_TYPE a) mrg_all)

Certificate theorem for sort:

|- DeclAssum BottomUpMergeSort_decls env ⇒
   Eval env (Var "sort")
     (((a --> a --> BOOL) --> PAIR_TYPE b (LIST_TYPE (LIST_TYPE a)) -->
       LIST_TYPE a) sort)

Definition of declaration list:

|- BottomUpMergeSort_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" [])));
    Dletrec
      [("mrg","v7",
        Fun "v8"
          (Fun "v9"
             (Mat (Var "v8")
                [(Pcon "Nil" [],
                  Mat (Var "v9")
                    [(Pcon "Nil" [],Con "Nil" []);
                     (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                      Con "Cons" [Var "v2"; Var "v1"])]);
                 (Pcon "Cons" [Pvar "v6"; Pvar "v5"],
                  Mat (Var "v9")
                    [(Pcon "Nil" [],Con "Cons" [Var "v6"; Var "v5"]);
                     (Pcon "Cons" [Pvar "v4"; Pvar "v3"],
                      If
                        (App Opapp (App Opapp (Var "v7") (Var "v6"))
                           (Var "v4"))
                        (Con "Cons"
                           [Var "v6";
                            App Opapp
                              (App Opapp
                                 (App Opapp (Var "mrg") (Var "v7"))
                                 (Var "v5"))
                              (Con "Cons" [Var "v4"; Var "v3"])])
                        (Con "Cons"
                           [Var "v4";
                            App Opapp
                              (App Opapp
                                 (App Opapp (Var "mrg") (Var "v7"))
                                 (Con "Cons" [Var "v6"; Var "v5"]))
                              (Var "v3")]))])])))];
    Dlet (Pvar "empty")
      (Con "Pair" [Val (Lit (IntLit 0)); Con "Nil" []]);
    Dletrec
      [("add_seg","v1",
        Fun "v2"
          (Fun "v3"
             (Fun "v4"
                (If
                   (App (Opb Leq)
                      (App (Opn Modulo) (Var "v4")
                         (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0))))
                   (Con "Cons" [Var "v2"; Var "v3"])
                   (App Opapp
                      (App Opapp
                         (App Opapp
                            (App Opapp (Var "add_seg") (Var "v1"))
                            (App Opapp
                               (App Opapp
                                  (App Opapp (Var "mrg") (Var "v1"))
                                  (Var "v2"))
                               (App Opapp (Var "HD") (Var "v3"))))
                         (App Opapp (Var "TL") (Var "v3")))
                      (App (Opn Divide) (Var "v4")
                         (Val (Lit (IntLit 2)))))))))];
    Dlet (Pvar "add")
      (Fun "v3"
         (Fun "v4"
            (Fun "v5"
               (Mat (Var "v5")
                  [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                    Con "Pair"
                      [App (Opn Plus) (Var "v2") (Val (Lit (IntLit 1)));
                       App Opapp
                         (App Opapp
                            (App Opapp
                               (App Opapp (Var "add_seg") (Var "v3"))
                               (Con "Cons" [Var "v4"; Con "Nil" []]))
                            (Var "v1")) (Var "v2")])]))));
    Dletrec
      [("mrg_all","v3",
        Fun "v4"
          (Fun "v5"
             (Mat (Var "v5")
                [(Pcon "Nil" [],Var "v4");
                 (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                  App Opapp
                    (App Opapp (App Opapp (Var "mrg_all") (Var "v3"))
                       (App Opapp
                          (App Opapp (App Opapp (Var "mrg") (Var "v3"))
                             (Var "v4")) (Var "v2"))) (Var "v1"))])))];
    Dlet (Pvar "sort")
      (Fun "v3"
         (Fun "v4"
            (Mat (Var "v4")
               [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                 App Opapp
                   (App Opapp (App Opapp (Var "mrg_all") (Var "v3"))
                      (Con "Nil" [])) (Var "v1"))])))]