This translation extends 'mini_prelude'. Definition of refinement invariant: |- ∀a x_2 x_1 v. QUEUE_TYPE a (QUEUE x_2 x_1) v ⇔ ∃v1_1 v1_2. (v = Conv "Queue" [v1_1; v1_2]) ∧ LIST_TYPE a x_2 v1_1 ∧ LIST_TYPE a x_1 v1_2 Certificate theorem for empty: |- DeclAssum BatchedQueue_decls env ⇒ Eval env (Var "empty") (QUEUE_TYPE a empty) Certificate theorem for is_empty: |- DeclAssum BatchedQueue_decls env ⇒ Eval env (Var "is_empty") ((QUEUE_TYPE a --> BOOL) is_empty) Certificate theorem for checkf: |- DeclAssum BatchedQueue_decls env ⇒ Eval env (Var "checkf") ((QUEUE_TYPE a --> QUEUE_TYPE a) checkf) Certificate theorem for snoc: |- DeclAssum BatchedQueue_decls env ⇒ Eval env (Var "snoc") ((QUEUE_TYPE a --> a --> QUEUE_TYPE a) snoc) Certificate theorem for head: |- DeclAssum BatchedQueue_decls env ∧ head_side x ⇒ Eval env (Var "head") ((Eq (QUEUE_TYPE a) x --> a) head) Definition of side condition for head: |- head_side v4 ⇔ (∃v3 v2 v1. v4 = QUEUE (v3::v2) v1) ∧ ∀v3. v4 ≠ QUEUE [] v3 Certificate theorem for tail: |- DeclAssum BatchedQueue_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 v4 ⇔ (∃v3 v2 v1. v4 = QUEUE (v3::v2) v1) ∧ ∀v3. v4 ≠ QUEUE [] v3 Definition of declaration list: |- BatchedQueue_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"])])]; Dlet (Pvar "empty") (Con "Queue" [Con "Nil" []; Con "Nil" []]); Dlet (Pvar "is_empty") (Fun "v5" (Mat (Var "v5") [(Pcon "Queue" [Pvar "v4"; Pvar "v3"], Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Val (Lit (Bool F)))])])); Dlet (Pvar "checkf") (Fun "v5" (Mat (Var "v5") [(Pcon "Queue" [Pvar "v4"; Pvar "v3"], Mat (Var "v4") [(Pcon "Nil" [], Con "Queue" [App Opapp (Var "REVERSE") (Var "v3"); Con "Nil" []]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Queue" [Con "Cons" [Var "v2"; Var "v1"]; Var "v3"])])])); Dlet (Pvar "snoc") (Fun "v3" (Fun "v4" (Mat (Var "v3") [(Pcon "Queue" [Pvar "v2"; Pvar "v1"], App Opapp (Var "checkf") (Con "Queue" [Var "v2"; Con "Cons" [Var "v4"; Var "v1"]]))]))); Dlet (Pvar "head") (Fun "x" (Mat (Var "x") [(Pcon "Queue" [Pvar "v4"; Pvar "v3"], Mat (Var "v4") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v2")])])); Dlet (Pvar "tail") (Fun "x" (Mat (Var "x") [(Pcon "Queue" [Pvar "v4"; Pvar "v3"], Mat (Var "v4") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (Var "checkf") (Con "Queue" [Var "v1"; Var "v3"]))])]))]