This translation extends 'mini_prelude'.

Definition of refinement invariant:

|- ∀a x_3 x_2 x_1 v.
     QUEUE_TYPE a (QUEUE x_3 x_2 x_1) v ⇔
     ∃v1_1 v1_2 v1_3.
       (v = Conv "Queue" [v1_1; v1_2; v1_3]) ∧ LIST_TYPE a x_3 v1_1 ∧
       LIST_TYPE a x_2 v1_2 ∧ LIST_TYPE a x_1 v1_3

Certificate theorem for empty:

|- DeclAssum RealTimeQueue_decls env ⇒
   Eval env (Var "empty") (QUEUE_TYPE a empty)

Certificate theorem for is_empty:

|- DeclAssum RealTimeQueue_decls env ⇒
   Eval env (Var "is_empty") ((QUEUE_TYPE a --> BOOL) is_empty)

Certificate theorem for rotate:

|- DeclAssum RealTimeQueue_decls env ∧ rotate_side x ⇒
   Eval env (Var "rotate")
     ((Eq (QUEUE_TYPE a) x --> LIST_TYPE a) rotate)

Definition of side condition for rotate:

|- rotate_side v1 ⇔
   case v1 of
     QUEUE [] [] v__13 => F
   | QUEUE [] (v12::v13) v__13 => T
   | QUEUE (v__12::v__11) [] v__13 => F
   | QUEUE (v__12::v__11) (v__10::v__9) v__13 =>
       rotate_side (QUEUE v__11 v__9 (v__10::v__13))

Certificate theorem for exec:

|- DeclAssum RealTimeQueue_decls env ∧ exec_side v7 ⇒
   Eval env (Var "exec") ((Eq (QUEUE_TYPE a) v7 --> QUEUE_TYPE a) exec)

Definition of side condition for exec:

|- exec_side v7 ⇔
   ∀v6 v5. (v7 = QUEUE v6 v5 []) ⇒ rotate_side (QUEUE v6 v5 [])

Certificate theorem for snoc:

|- DeclAssum RealTimeQueue_decls env ∧ snoc_side v4 v5 ⇒
   Eval env (Var "snoc")
     ((Eq (QUEUE_TYPE a) v4 --> Eq a v5 --> QUEUE_TYPE a) snoc)

Definition of side condition for snoc:

|- snoc_side v4 v5 ⇔
   ∀v3 v2 v1. (v4 = QUEUE v3 v2 v1) ⇒ exec_side (QUEUE v3 (v5::v2) v1)

Certificate theorem for head:

|- DeclAssum RealTimeQueue_decls env ∧ head_side x ⇒
   Eval env (Var "head") ((Eq (QUEUE_TYPE a) x --> a) head)

Definition of side condition for head:

|- head_side v5 ⇔
   (∃v4 v3 v2 v1. v5 = QUEUE (v4::v3) v2 v1) ∧
   ∀v4 v3. v5 ≠ QUEUE [] v4 v3

Certificate theorem for tail:

|- DeclAssum RealTimeQueue_decls env ∧ tail_side x ⇒
   Eval env (Var "tail") ((Eq (QUEUE_TYPE a) x --> QUEUE_TYPE a) tail)

Definition of side condition for tail:

|- tail_side v5 ⇔
   (∃v4 v3 v2 v1. v5 = QUEUE (v4::v3) v2 v1) ∧
   ∀v5' v4 v3.
     (v5 = QUEUE v5' v4 v3) ⇒
     ∀v2 v1. v5' ≠ [] ∧ ((v5' = v2::v1) ⇒ exec_side (QUEUE v1 v4 v3))

Definition of declaration list:

|- RealTimeQueue_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"],"queue",
        [("Queue",
          [Tapp [Tvar "a"] "list"; Tapp [Tvar "a"] "list";
           Tapp [Tvar "a"] "list"])])];
    Dlet (Pvar "empty")
      (Con "Queue" [Con "Nil" []; Con "Nil" []; Con "Nil" []]);
    Dlet (Pvar "is_empty")
      (Fun "v6"
         (Mat (Var "v6")
            [(Pcon "Queue" [Pvar "v5"; Pvar "v4"; Pvar "v3"],
              Mat (Var "v5")
                [(Pcon "Nil" [],Val (Lit (Bool T)));
                 (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                  Val (Lit (Bool F)))])]));
    Dletrec
      [("rotate","x",
        Mat (Var "x")
          [(Pcon "Queue" [Pvar "v9"; Pvar "v8"; Pvar "v7"],
            Mat (Var "v9")
              [(Pcon "Nil" [],
                Mat (Var "v8")
                  [(Pcon "Nil" [],Raise Bind_error);
                   (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                    Con "Cons" [Var "v2"; Var "v7"])]);
               (Pcon "Cons" [Pvar "v6"; Pvar "v5"],
                Mat (Var "v8")
                  [(Pcon "Nil" [],Raise Bind_error);
                   (Pcon "Cons" [Pvar "v4"; Pvar "v3"],
                    Con "Cons"
                      [Var "v6";
                       App Opapp (Var "rotate")
                         (Con "Queue"
                            [Var "v5"; Var "v3";
                             Con "Cons" [Var "v4"; Var "v7"]])])])])])];
    Dlet (Pvar "exec")
      (Fun "v7"
         (Mat (Var "v7")
            [(Pcon "Queue" [Pvar "v6"; Pvar "v5"; Pvar "v4"],
              Mat (Var "v4")
                [(Pcon "Nil" [],
                  Let "v1"
                    (App Opapp (Var "rotate")
                       (Con "Queue" [Var "v6"; Var "v5"; Con "Nil" []]))
                    (Con "Queue" [Var "v1"; Con "Nil" []; Var "v1"]));
                 (Pcon "Cons" [Pvar "v3"; Pvar "v2"],
                  Con "Queue" [Var "v6"; Var "v5"; Var "v2"])])]));
    Dlet (Pvar "snoc")
      (Fun "v4"
         (Fun "v5"
            (Mat (Var "v4")
               [(Pcon "Queue" [Pvar "v3"; Pvar "v2"; Pvar "v1"],
                 App Opapp (Var "exec")
                   (Con "Queue"
                      [Var "v3"; Con "Cons" [Var "v5"; Var "v2"];
                       Var "v1"]))])));
    Dlet (Pvar "head")
      (Fun "x"
         (Mat (Var "x")
            [(Pcon "Queue" [Pvar "v5"; Pvar "v4"; Pvar "v3"],
              Mat (Var "v5")
                [(Pcon "Nil" [],Raise Bind_error);
                 (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v2")])]));
    Dlet (Pvar "tail")
      (Fun "x"
         (Mat (Var "x")
            [(Pcon "Queue" [Pvar "v5"; Pvar "v4"; Pvar "v3"],
              Mat (Var "v5")
                [(Pcon "Nil" [],Raise Bind_error);
                 (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                  App Opapp (Var "exec")
                    (Con "Queue" [Var "v1"; Var "v4"; Var "v3"]))])]))]