This translation extends 'mini_prelude'.

Certificate theorem for empty:

|- DeclAssum BinaryRandomAccessLists_decls env ⇒
   Eval env (Var "empty") (LIST_TYPE a empty)

Certificate theorem for is_empty:

|- DeclAssum BinaryRandomAccessLists_decls env ⇒
   Eval env (Var "is_empty") ((LIST_TYPE a --> BOOL) is_empty)

Definition of refinement invariant:

|- (∀a x_4 x_3 x_2 v.
      TREE_TYPE a (Node x_4 x_3 x_2) v ⇔
      ∃v2_1 v2_2 v2_3.
        (v = Conv "Node" [v2_1; v2_2; v2_3]) ∧ NUM x_4 v2_1 ∧
        TREE_TYPE a x_3 v2_2 ∧ TREE_TYPE a x_2 v2_3) ∧
   ∀a x_1 v.
     TREE_TYPE a (Leaf x_1) v ⇔
     ∃v1_1. (v = Conv "Leaf" [v1_1]) ∧ a x_1 v1_1

Certificate theorem for size:

|- DeclAssum BinaryRandomAccessLists_decls env ⇒
   Eval env (Var "size") ((TREE_TYPE a --> NUM) size)

Certificate theorem for link:

|- DeclAssum BinaryRandomAccessLists_decls env ⇒
   Eval env (Var "link")
     ((TREE_TYPE a --> TREE_TYPE a --> TREE_TYPE a) link)

Definition of refinement invariant:

|- (∀a x_1 v.
      DIGIT_TYPE a (One x_1) v ⇔
      ∃v2_1. (v = Conv "One" [v2_1]) ∧ TREE_TYPE a x_1 v2_1) ∧
   ∀a v. DIGIT_TYPE a Zero v ⇔ (v = Conv "Zero" [])

Certificate theorem for cons_tree:

|- DeclAssum BinaryRandomAccessLists_decls env ⇒
   Eval env (Var "cons_tree")
     ((TREE_TYPE a --> LIST_TYPE (DIGIT_TYPE a) -->
       LIST_TYPE (DIGIT_TYPE a)) cons_tree)

Certificate theorem for uncons_tree:

|- DeclAssum BinaryRandomAccessLists_decls env ∧ uncons_tree_side x ⇒
   Eval env (Var "uncons_tree")
     ((Eq (LIST_TYPE (DIGIT_TYPE a)) x -->
       PAIR_TYPE (TREE_TYPE a) (LIST_TYPE (DIGIT_TYPE a))) uncons_tree)

Definition of side condition for uncons_tree:

|- uncons_tree_side v1 ⇔
   case v1 of
     [] => F
   | Zero::v__9 =>
       ∀v__8 v__7.
         uncons_tree_side v__9 ∧
         ((uncons_tree v__9 = (v__8,v__7)) ⇒ ∀v__6. v__8 ≠ Leaf v__6)
   | One v5::v__9 => (v__9 = []) ∨ ∃v__3 v__2. v__9 = v__3::v__2

Certificate theorem for cons:

|- DeclAssum BinaryRandomAccessLists_decls env ⇒
   Eval env (Var "cons")
     ((a --> LIST_TYPE (DIGIT_TYPE a) --> LIST_TYPE (DIGIT_TYPE a))
        cons)

Certificate theorem for head:

|- DeclAssum BinaryRandomAccessLists_decls env ∧ head_side v7 ⇒
   Eval env (Var "head") ((Eq (LIST_TYPE (DIGIT_TYPE a)) v7 --> a) head)

Definition of side condition for head:

|- head_side v7 ⇔
   ∀v6 v5.
     uncons_tree_side v7 ∧
     ((uncons_tree v7 = (v6,v5)) ⇒ ∀v4 v3 v2. v6 ≠ Node v4 v3 v2)

Certificate theorem for tail:

|- DeclAssum BinaryRandomAccessLists_decls env ∧ tail_side v4 ⇒
   Eval env (Var "tail")
     ((Eq (LIST_TYPE (DIGIT_TYPE a)) v4 --> LIST_TYPE (DIGIT_TYPE a))
        tail)

Definition of side condition for tail:

|- tail_side v4 ⇔ uncons_tree_side v4

Certificate theorem for lookup_tree:

|- DeclAssum BinaryRandomAccessLists_decls env ∧
   lookup_tree_side x1 x2 ⇒
   Eval env (Var "lookup_tree")
     ((Eq NUM x1 --> Eq (TREE_TYPE a) x2 --> a) lookup_tree)

Definition of side condition for lookup_tree:

|- lookup_tree_side v1 v2 ⇔
   case v2 of
     Leaf v__8 => v1 = 0
   | Node v__7 v__6 v__5 =>
       (v1 < v__7 DIV 2 ⇒ lookup_tree_side v1 v__6) ∧
       (¬(v1 < v__7 DIV 2) ⇒ lookup_tree_side (v1 − v__7 DIV 2) v__5)

Certificate theorem for update_tree:

|- DeclAssum BinaryRandomAccessLists_decls env ∧
   update_tree_side x1 x2 x3 ⇒
   Eval env (Var "update_tree")
     ((Eq NUM x1 --> Eq a x2 --> Eq (TREE_TYPE a) x3 --> TREE_TYPE a)
        update_tree)

Definition of side condition for update_tree:

|- update_tree_side v1 v2 v3 ⇔
   case v3 of
     Leaf v__8 => v1 = 0
   | Node v__7 v__6 v__5 =>
       (v1 < v__7 DIV 2 ⇒ update_tree_side v1 v2 v__6) ∧
       (¬(v1 < v__7 DIV 2) ⇒ update_tree_side (v1 − v__7 DIV 2) v2 v__5)

Certificate theorem for lookup:

|- DeclAssum BinaryRandomAccessLists_decls env ∧ lookup_side x x1 ⇒
   Eval env (Var "lookup")
     ((Eq NUM x --> Eq (LIST_TYPE (DIGIT_TYPE a)) x1 --> a) lookup)

Definition of side condition for lookup:

|- lookup_side v1 v2 ⇔
   case v2 of
     [] => F
   | Zero::v__5 => lookup_side v1 v__5
   | One v__4::v__5 =>
       (v1 < size v__4 ⇒ lookup_tree_side v1 v__4) ∧
       (¬(v1 < size v__4) ⇒ lookup_side (v1 − size v__4) v__5)

Certificate theorem for update:

|- DeclAssum BinaryRandomAccessLists_decls env ∧ update_side x x1 x2 ⇒
   Eval env (Var "update")
     ((Eq NUM x --> Eq a x1 --> Eq (LIST_TYPE (DIGIT_TYPE a)) x2 -->
       LIST_TYPE (DIGIT_TYPE a)) update)

Definition of side condition for update:

|- update_side v1 v2 v3 ⇔
   case v3 of
     [] => F
   | Zero::v__5 => update_side v1 v2 v__5
   | One v__4::v__5 =>
       (v1 < size v__4 ⇒ update_tree_side v1 v2 v__4) ∧
       (¬(v1 < size v__4) ⇒ update_side (v1 − size v__4) v2 v__5)

Definition of declaration list:

|- BinaryRandomAccessLists_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" [])));
    Dlet (Pvar "empty") (Con "Nil" []);
    Dlet (Pvar "is_empty")
      (Fun "v3"
         (Mat (Var "v3")
            [(Pcon "Nil" [],Val (Lit (Bool T)));
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Val (Lit (Bool F)))]));
    Dtype
      [(["a"],"tree",
        [("Node",
          [Tnum; Tapp [Tvar "a"] "tree"; Tapp [Tvar "a"] "tree"]);
         ("Leaf",[Tvar "a"])])];
    Dlet (Pvar "size")
      (Fun "v5"
         (Mat (Var "v5")
            [(Pcon "Leaf" [Pvar "v1"],Val (Lit (IntLit 1)));
             (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],
              Var "v4")]));
    Dlet (Pvar "link")
      (Fun "v1"
         (Fun "v2"
            (Con "Node"
               [App (Opn Plus) (App Opapp (Var "size") (Var "v1"))
                  (App Opapp (Var "size") (Var "v2")); Var "v1";
                Var "v2"])));
    Dtype
      [(["a"],"digit",[("One",[Tapp [Tvar "a"] "tree"]); ("Zero",[])])];
    Dletrec
      [("cons_tree","v4",
        Fun "v5"
          (Mat (Var "v5")
             [(Pcon "Nil" [],
               Con "Cons" [Con "One" [Var "v4"]; Con "Nil" []]);
              (Pcon "Cons" [Pvar "v3"; Pvar "v2"],
               Mat (Var "v3")
                 [(Pcon "Zero" [],
                   Con "Cons" [Con "One" [Var "v4"]; Var "v2"]);
                  (Pcon "One" [Pvar "v1"],
                   Con "Cons"
                     [Con "Zero" [];
                      App Opapp
                        (App Opapp (Var "cons_tree")
                           (App Opapp
                              (App Opapp (Var "link") (Var "v4"))
                              (Var "v1"))) (Var "v2")])])]))];
    Dletrec
      [("uncons_tree","x",
        Mat (Var "x")
          [(Pcon "Nil" [],Raise Bind_error);
           (Pcon "Cons" [Pvar "v11"; Pvar "v10"],
            Mat (Var "v11")
              [(Pcon "Zero" [],
                Mat (App Opapp (Var "uncons_tree") (Var "v10"))
                  [(Pcon "Pair" [Pvar "v6"; Pvar "v5"],
                    Mat (Var "v6")
                      [(Pcon "Leaf" [Pvar "v1"],Raise Bind_error);
                       (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],
                        Con "Pair"
                          [Var "v3";
                           Con "Cons"
                             [Con "One" [Var "v2"]; Var "v5"]])])]);
               (Pcon "One" [Pvar "v9"],
                Mat (Var "v10")
                  [(Pcon "Nil" [],Con "Pair" [Var "v9"; Con "Nil" []]);
                   (Pcon "Cons" [Pvar "v8"; Pvar "v7"],
                    Con "Pair"
                      [Var "v9";
                       Con "Cons"
                         [Con "Zero" [];
                          Con "Cons" [Var "v8"; Var "v7"]]])])])])];
    Dlet (Pvar "cons")
      (Fun "v2"
         (Fun "v1"
            (App Opapp
               (App Opapp (Var "cons_tree") (Con "Leaf" [Var "v2"]))
               (Var "v1"))));
    Dlet (Pvar "head")
      (Fun "v7"
         (Mat (App Opapp (Var "uncons_tree") (Var "v7"))
            [(Pcon "Pair" [Pvar "v6"; Pvar "v5"],
              Mat (Var "v6")
                [(Pcon "Leaf" [Pvar "v1"],Var "v1");
                 (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],
                  Raise Bind_error)])]));
    Dlet (Pvar "tail")
      (Fun "v4"
         (Let "v3" (App Opapp (Var "uncons_tree") (Var "v4"))
            (Mat (Var "v3")
               [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v1")])));
    Dletrec
      [("lookup_tree","x1",
        Fun "x2"
          (Mat (Var "x2")
             [(Pcon "Leaf" [Pvar "v1"],
               If (App (Opb Leq) (Var "x1") (Val (Lit (IntLit 0))))
                 (Var "v1") (Raise Bind_error));
              (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],
               If
                 (App (Opb Lt) (Var "x1")
                    (App (Opn Divide) (Var "v4")
                       (Val (Lit (IntLit 2)))))
                 (App Opapp (App Opapp (Var "lookup_tree") (Var "x1"))
                    (Var "v3"))
                 (App Opapp
                    (App Opapp (Var "lookup_tree")
                       (Let "k"
                          (App (Opn Minus) (Var "x1")
                             (App (Opn Divide) (Var "v4")
                                (Val (Lit (IntLit 2)))))
                          (If
                             (App (Opb Lt) (Var "k")
                                (Val (Lit (IntLit 0))))
                             (Val (Lit (IntLit 0))) (Var "k"))))
                    (Var "v2")))]))];
    Dletrec
      [("update_tree","x1",
        Fun "x2"
          (Fun "x3"
             (Mat (Var "x3")
                [(Pcon "Leaf" [Pvar "v1"],
                  If (App (Opb Leq) (Var "x1") (Val (Lit (IntLit 0))))
                    (Con "Leaf" [Var "x2"]) (Raise Bind_error));
                 (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],
                  If
                    (App (Opb Lt) (Var "x1")
                       (App (Opn Divide) (Var "v4")
                          (Val (Lit (IntLit 2)))))
                    (Con "Node"
                       [Var "v4";
                        App Opapp
                          (App Opapp
                             (App Opapp (Var "update_tree") (Var "x1"))
                             (Var "x2")) (Var "v3"); Var "v2"])
                    (Con "Node"
                       [Var "v4"; Var "v3";
                        App Opapp
                          (App Opapp
                             (App Opapp (Var "update_tree")
                                (Let "k"
                                   (App (Opn Minus) (Var "x1")
                                      (App (Opn Divide) (Var "v4")
                                         (Val (Lit (IntLit 2)))))
                                   (If
                                      (App (Opb Lt) (Var "k")
                                         (Val (Lit (IntLit 0))))
                                      (Val (Lit (IntLit 0)))
                                      (Var "k")))) (Var "x2"))
                          (Var "v2")]))])))];
    Dletrec
      [("lookup","x",
        Fun "x1"
          (Mat (Var "x1")
             [(Pcon "Nil" [],Raise Bind_error);
              (Pcon "Cons" [Pvar "v3"; Pvar "v2"],
               Mat (Var "v3")
                 [(Pcon "Zero" [],
                   App Opapp (App Opapp (Var "lookup") (Var "x"))
                     (Var "v2"));
                  (Pcon "One" [Pvar "v1"],
                   If
                     (App (Opb Lt) (Var "x")
                        (App Opapp (Var "size") (Var "v1")))
                     (App Opapp
                        (App Opapp (Var "lookup_tree") (Var "x"))
                        (Var "v1"))
                     (App Opapp
                        (App Opapp (Var "lookup")
                           (Let "k"
                              (App (Opn Minus) (Var "x")
                                 (App Opapp (Var "size") (Var "v1")))
                              (If
                                 (App (Opb Lt) (Var "k")
                                    (Val (Lit (IntLit 0))))
                                 (Val (Lit (IntLit 0))) (Var "k"))))
                        (Var "v2")))])]))];
    Dletrec
      [("update","x",
        Fun "x1"
          (Fun "x2"
             (Mat (Var "x2")
                [(Pcon "Nil" [],Raise Bind_error);
                 (Pcon "Cons" [Pvar "v3"; Pvar "v2"],
                  Mat (Var "v3")
                    [(Pcon "Zero" [],
                      Con "Cons"
                        [Con "Zero" [];
                         App Opapp
                           (App Opapp
                              (App Opapp (Var "update") (Var "x"))
                              (Var "x1")) (Var "v2")]);
                     (Pcon "One" [Pvar "v1"],
                      If
                        (App (Opb Lt) (Var "x")
                           (App Opapp (Var "size") (Var "v1")))
                        (Con "Cons"
                           [Con "One"
                              [App Opapp
                                 (App Opapp
                                    (App Opapp (Var "update_tree")
                                       (Var "x")) (Var "x1"))
                                 (Var "v1")]; Var "v2"])
                        (Con "Cons"
                           [Con "One" [Var "v1"];
                            App Opapp
                              (App Opapp
                                 (App Opapp (Var "update")
                                    (Let "k"
                                       (App (Opn Minus) (Var "x")
                                          (App Opapp (Var "size")
                                             (Var "v1")))
                                       (If
                                          (App (Opb Lt) (Var "k")
                                             (Val (Lit (IntLit 0))))
                                          (Val (Lit (IntLit 0)))
                                          (Var "k")))) (Var "x1"))
                              (Var "v2")]))])])))]]