This translation extends 'mini_prelude'.

Definition of refinement invariant:

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

Certificate theorem for empty:

|- DeclAssum UnbalancedSet_decls env ⇒
   Eval env (Var "empty") (TREE_TYPE a empty)

Certificate theorem for member:

|- DeclAssum UnbalancedSet_decls env ⇒
   Eval env (Var "member")
     (((a --> a --> BOOL) --> a --> TREE_TYPE a --> BOOL) member)

Certificate theorem for insert:

|- DeclAssum UnbalancedSet_decls env ⇒
   Eval env (Var "insert")
     (((a --> a --> BOOL) --> a --> TREE_TYPE a --> TREE_TYPE a) insert)

Definition of declaration list:

|- UnbalancedSet_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"],"tree",
        [("Tree",
          [Tapp [Tvar "a"] "tree"; Tvar "a"; Tapp [Tvar "a"] "tree"]);
         ("Empty",[])])]; Dlet (Pvar "empty") (Con "Empty" []);
    Dletrec
      [("member","v4",
        Fun "v5"
          (Fun "v6"
             (Mat (Var "v6")
                [(Pcon "Empty" [],Val (Lit (Bool F)));
                 (Pcon "Tree" [Pvar "v3"; Pvar "v2"; Pvar "v1"],
                  If
                    (App Opapp (App Opapp (Var "v4") (Var "v5"))
                       (Var "v2"))
                    (App Opapp
                       (App Opapp (App Opapp (Var "member") (Var "v4"))
                          (Var "v5")) (Var "v3"))
                    (If
                       (App Opapp (App Opapp (Var "v4") (Var "v2"))
                          (Var "v5"))
                       (App Opapp
                          (App Opapp
                             (App Opapp (Var "member") (Var "v4"))
                             (Var "v5")) (Var "v1"))
                       (Val (Lit (Bool T)))))])))];
    Dletrec
      [("insert","v4",
        Fun "v5"
          (Fun "v6"
             (Mat (Var "v6")
                [(Pcon "Empty" [],
                  Con "Tree"
                    [Con "Empty" []; Var "v5"; Con "Empty" []]);
                 (Pcon "Tree" [Pvar "v3"; Pvar "v2"; Pvar "v1"],
                  If
                    (App Opapp (App Opapp (Var "v4") (Var "v5"))
                       (Var "v2"))
                    (Con "Tree"
                       [App Opapp
                          (App Opapp
                             (App Opapp (Var "insert") (Var "v4"))
                             (Var "v5")) (Var "v3"); Var "v2";
                        Var "v1"])
                    (If
                       (App Opapp (App Opapp (Var "v4") (Var "v2"))
                          (Var "v5"))
                       (Con "Tree"
                          [Var "v3"; Var "v2";
                           App Opapp
                             (App Opapp
                                (App Opapp (Var "insert") (Var "v4"))
                                (Var "v5")) (Var "v1")])
                       (Con "Tree"
                          [Var "v3"; Var "v2"; Var "v1"])))])))]]