This translation extends 'mini_prelude'.

Definition of refinement invariant:

|- (∀v. COLOR_TYPE Black v ⇔ (v = Conv "Black" [])) ∧
   ∀v. COLOR_TYPE Red v ⇔ (v = Conv "Red" [])

Definition of refinement invariant:

|- (∀a x_4 x_3 x_2 x_1 v.
      TREE_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]) ∧
        COLOR_TYPE x_4 v2_1 ∧ TREE_TYPE a x_3 v2_2 ∧ a x_2 v2_3 ∧
        TREE_TYPE a x_1 v2_4) ∧
   ∀a v. TREE_TYPE a Empty v ⇔ (v = Conv "Empty" [])

Certificate theorem for empty:

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

Certificate theorem for member:

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

Definition of refinement invariant:

|- (∀a x_1 v.
      OPTION_TYPE a (SOME x_1) v ⇔
      ∃v2_1. (v = Conv "Some" [v2_1]) ∧ a x_1 v2_1) ∧
   ∀a v. OPTION_TYPE a NONE v ⇔ (v = Conv "None" [])

Certificate theorem for balance_left_left:

|- DeclAssum RedBlackSet_decls env ⇒
   Eval env (Var "balance_left_left")
     ((TREE_TYPE a --> a --> TREE_TYPE a --> OPTION_TYPE (TREE_TYPE a))
        balance_left_left)

Certificate theorem for balance_left_right:

|- DeclAssum RedBlackSet_decls env ⇒
   Eval env (Var "balance_left_right")
     ((TREE_TYPE a --> a --> TREE_TYPE a --> OPTION_TYPE (TREE_TYPE a))
        balance_left_right)

Certificate theorem for balance_right_left:

|- DeclAssum RedBlackSet_decls env ⇒
   Eval env (Var "balance_right_left")
     ((TREE_TYPE a --> a --> TREE_TYPE a --> OPTION_TYPE (TREE_TYPE a))
        balance_right_left)

Certificate theorem for balance_right_right:

|- DeclAssum RedBlackSet_decls env ⇒
   Eval env (Var "balance_right_right")
     ((TREE_TYPE a --> a --> TREE_TYPE a --> OPTION_TYPE (TREE_TYPE a))
        balance_right_right)

Certificate theorem for balance':

|- DeclAssum RedBlackSet_decls env ⇒
   Eval env (Var "balance'")
     ((COLOR_TYPE --> TREE_TYPE a --> a --> TREE_TYPE a --> TREE_TYPE a)
        balance')

Certificate theorem for ins:

|- DeclAssum RedBlackSet_decls env ⇒
   Eval env (Var "ins")
     (((a --> a --> BOOL) --> a --> TREE_TYPE a --> TREE_TYPE a) ins)

Certificate theorem for insert:

|- DeclAssum RedBlackSet_decls env ∧ insert_side v5 v7 v6 ⇒
   Eval env (Var "insert")
     ((Eq (a --> a --> BOOL) v5 --> Eq a v7 --> Eq (TREE_TYPE a) v6 -->
       TREE_TYPE a) insert)

Definition of side condition for insert:

|- insert_side v5 v7 v6 ⇔ ins v5 v7 v6 ≠ Empty

Definition of declaration list:

|- RedBlackSet_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 [([],"color",[("Black",[]); ("Red",[])])];
    Dtype
      [(["a"],"tree",
        [("Tree",
          [Tapp [] "color"; Tapp [Tvar "a"] "tree"; Tvar "a";
           Tapp [Tvar "a"] "tree"]); ("Empty",[])])];
    Dlet (Pvar "empty") (Con "Empty" []);
    Dletrec
      [("member","v5",
        Fun "v6"
          (Fun "v7"
             (Mat (Var "v7")
                [(Pcon "Empty" [],Val (Lit (Bool F)));
                 (Pcon "Tree"
                    [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
                  If
                    (App Opapp (App Opapp (Var "v5") (Var "v6"))
                       (Var "v2"))
                    (App Opapp
                       (App Opapp (App Opapp (Var "member") (Var "v5"))
                          (Var "v6")) (Var "v3"))
                    (If
                       (App Opapp (App Opapp (Var "v5") (Var "v2"))
                          (Var "v6"))
                       (App Opapp
                          (App Opapp
                             (App Opapp (Var "member") (Var "v5"))
                             (Var "v6")) (Var "v1"))
                       (Val (Lit (Bool T)))))])))];
    Dtype [(["a"],"option",[("Some",[Tvar "a"]); ("None",[])])];
    Dlet (Pvar "balance_left_left")
      (Fun "v11"
         (Fun "v9"
            (Fun "v10"
               (Mat (Var "v11")
                  [(Pcon "Empty" [],Con "None" []);
                   (Pcon "Tree"
                      [Pvar "v8"; Pvar "v7"; Pvar "v6"; Pvar "v5"],
                    Mat (Var "v8")
                      [(Pcon "Red" [],
                        Mat (Var "v7")
                          [(Pcon "Empty" [],Con "None" []);
                           (Pcon "Tree"
                              [Pvar "v4"; Pvar "v3"; Pvar "v2";
                               Pvar "v1"],
                            Mat (Var "v4")
                              [(Pcon "Red" [],
                                Con "Some"
                                  [Con "Tree"
                                     [Con "Red" [];
                                      Con "Tree"
                                        [Con "Black" []; Var "v3";
                                         Var "v2"; Var "v1"]; Var "v6";
                                      Con "Tree"
                                        [Con "Black" []; Var "v5";
                                         Var "v9"; Var "v10"]]]);
                               (Pcon "Black" [],Con "None" [])])]);
                       (Pcon "Black" [],Con "None" [])])]))));
    Dlet (Pvar "balance_left_right")
      (Fun "v11"
         (Fun "v9"
            (Fun "v10"
               (Mat (Var "v11")
                  [(Pcon "Empty" [],Con "None" []);
                   (Pcon "Tree"
                      [Pvar "v8"; Pvar "v7"; Pvar "v6"; Pvar "v5"],
                    Mat (Var "v8")
                      [(Pcon "Red" [],
                        Mat (Var "v5")
                          [(Pcon "Empty" [],Con "None" []);
                           (Pcon "Tree"
                              [Pvar "v4"; Pvar "v3"; Pvar "v2";
                               Pvar "v1"],
                            Mat (Var "v4")
                              [(Pcon "Red" [],
                                Con "Some"
                                  [Con "Tree"
                                     [Con "Red" [];
                                      Con "Tree"
                                        [Con "Black" []; Var "v7";
                                         Var "v6"; Var "v3"]; Var "v2";
                                      Con "Tree"
                                        [Con "Black" []; Var "v1";
                                         Var "v9"; Var "v10"]]]);
                               (Pcon "Black" [],Con "None" [])])]);
                       (Pcon "Black" [],Con "None" [])])]))));
    Dlet (Pvar "balance_right_left")
      (Fun "v11"
         (Fun "v9"
            (Fun "v10"
               (Mat (Var "v10")
                  [(Pcon "Empty" [],Con "None" []);
                   (Pcon "Tree"
                      [Pvar "v8"; Pvar "v7"; Pvar "v6"; Pvar "v5"],
                    Mat (Var "v8")
                      [(Pcon "Red" [],
                        Mat (Var "v7")
                          [(Pcon "Empty" [],Con "None" []);
                           (Pcon "Tree"
                              [Pvar "v4"; Pvar "v3"; Pvar "v2";
                               Pvar "v1"],
                            Mat (Var "v4")
                              [(Pcon "Red" [],
                                Con "Some"
                                  [Con "Tree"
                                     [Con "Red" [];
                                      Con "Tree"
                                        [Con "Black" []; Var "v11";
                                         Var "v9"; Var "v3"]; Var "v2";
                                      Con "Tree"
                                        [Con "Black" []; Var "v1";
                                         Var "v6"; Var "v5"]]]);
                               (Pcon "Black" [],Con "None" [])])]);
                       (Pcon "Black" [],Con "None" [])])]))));
    Dlet (Pvar "balance_right_right")
      (Fun "v11"
         (Fun "v9"
            (Fun "v10"
               (Mat (Var "v10")
                  [(Pcon "Empty" [],Con "None" []);
                   (Pcon "Tree"
                      [Pvar "v8"; Pvar "v7"; Pvar "v6"; Pvar "v5"],
                    Mat (Var "v8")
                      [(Pcon "Red" [],
                        Mat (Var "v5")
                          [(Pcon "Empty" [],Con "None" []);
                           (Pcon "Tree"
                              [Pvar "v4"; Pvar "v3"; Pvar "v2";
                               Pvar "v1"],
                            Mat (Var "v4")
                              [(Pcon "Red" [],
                                Con "Some"
                                  [Con "Tree"
                                     [Con "Red" [];
                                      Con "Tree"
                                        [Con "Black" []; Var "v11";
                                         Var "v9"; Var "v7"]; Var "v6";
                                      Con "Tree"
                                        [Con "Black" []; Var "v3";
                                         Var "v2"; Var "v1"]]]);
                               (Pcon "Black" [],Con "None" [])])]);
                       (Pcon "Black" [],Con "None" [])])]))));
    Dlet (Pvar "balance'")
      (Fun "v7"
         (Fun "v5"
            (Fun "v8"
               (Fun "v6"
                  (If (App Equality (Var "v7") (Con "Black" []))
                     (Mat
                        (App Opapp
                           (App Opapp
                              (App Opapp (Var "balance_left_left")
                                 (Var "v5")) (Var "v8")) (Var "v6"))
                        [(Pcon "None" [],
                          Mat
                            (App Opapp
                               (App Opapp
                                  (App Opapp (Var "balance_left_right")
                                     (Var "v5")) (Var "v8")) (Var "v6"))
                            [(Pcon "None" [],
                              Mat
                                (App Opapp
                                   (App Opapp
                                      (App Opapp
                                         (Var "balance_right_left")
                                         (Var "v5")) (Var "v8"))
                                   (Var "v6"))
                                [(Pcon "None" [],
                                  Mat
                                    (App Opapp
                                       (App Opapp
                                          (App Opapp
                                             (Var "balance_right_right")
                                             (Var "v5")) (Var "v8"))
                                       (Var "v6"))
                                    [(Pcon "None" [],
                                      Con "Tree"
                                        [Con "Black" []; Var "v5";
                                         Var "v8"; Var "v6"]);
                                     (Pcon "Some" [Pvar "v1"],
                                      Var "v1")]);
                                 (Pcon "Some" [Pvar "v2"],Var "v2")]);
                             (Pcon "Some" [Pvar "v3"],Var "v3")]);
                         (Pcon "Some" [Pvar "v4"],Var "v4")])
                     (Con "Tree"
                        [Var "v7"; Var "v5"; Var "v8"; Var "v6"]))))));
    Dletrec
      [("ins","v5",
        Fun "v6"
          (Fun "v7"
             (Mat (Var "v7")
                [(Pcon "Empty" [],
                  Con "Tree"
                    [Con "Red" []; Con "Empty" []; Var "v6";
                     Con "Empty" []]);
                 (Pcon "Tree"
                    [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
                  If
                    (App Opapp (App Opapp (Var "v5") (Var "v6"))
                       (Var "v2"))
                    (App Opapp
                       (App Opapp
                          (App Opapp
                             (App Opapp (Var "balance'") (Var "v4"))
                             (App Opapp
                                (App Opapp
                                   (App Opapp (Var "ins") (Var "v5"))
                                   (Var "v6")) (Var "v3"))) (Var "v2"))
                       (Var "v1"))
                    (If
                       (App Opapp (App Opapp (Var "v5") (Var "v2"))
                          (Var "v6"))
                       (App Opapp
                          (App Opapp
                             (App Opapp
                                (App Opapp (Var "balance'") (Var "v4"))
                                (Var "v3")) (Var "v2"))
                          (App Opapp
                             (App Opapp
                                (App Opapp (Var "ins") (Var "v5"))
                                (Var "v6")) (Var "v1")))
                       (Con "Tree"
                          [Var "v4"; Var "v3"; Var "v2";
                           Var "v1"])))])))];
    Dlet (Pvar "insert")
      (Fun "v5"
         (Fun "v7"
            (Fun "v6"
               (Mat
                  (App Opapp
                     (App Opapp (App Opapp (Var "ins") (Var "v5"))
                        (Var "v7")) (Var "v6"))
                  [(Pcon "Empty" [],Raise Bind_error);
                   (Pcon "Tree"
                      [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
                    Con "Tree"
                      [Con "Black" []; Var "v3"; Var "v2";
                       Var "v1"])]))))]