This translation extends 'mini_prelude'. Definition of refinement invariant: |- ∀a x_4 x_3 x_2 x_1 v. QUEUE_TYPE a (QUEUE x_4 x_3 x_2 x_1) v ⇔ ∃v1_1 v1_2 v1_3 v1_4. (v = Conv "Queue" [v1_1; v1_2; v1_3; v1_4]) ∧ NUM x_4 v1_1 ∧ LIST_TYPE a x_3 v1_2 ∧ NUM x_2 v1_3 ∧ LIST_TYPE a x_1 v1_4 Certificate theorem for empty: |- DeclAssum BankersQueue_decls env ⇒ Eval env (Var "empty") (QUEUE_TYPE a empty) Certificate theorem for is_empty: |- DeclAssum BankersQueue_decls env ⇒ Eval env (Var "is_empty") ((QUEUE_TYPE a --> BOOL) is_empty) Certificate theorem for checkf: |- DeclAssum BankersQueue_decls env ⇒ Eval env (Var "checkf") ((QUEUE_TYPE a --> QUEUE_TYPE a) checkf) Certificate theorem for snoc: |- DeclAssum BankersQueue_decls env ⇒ Eval env (Var "snoc") ((QUEUE_TYPE a --> a --> QUEUE_TYPE a) snoc) Certificate theorem for head: |- DeclAssum BankersQueue_decls env ∧ head_side x ⇒ Eval env (Var "head") ((Eq (QUEUE_TYPE a) x --> a) head) Definition of side condition for head: |- head_side v6 ⇔ (∃v5 v4 v3 v2 v1. v6 = QUEUE v5 (v4::v3) v2 v1) ∧ ∀v6' v4 v3. v6 ≠ QUEUE v6' [] v4 v3 Certificate theorem for tail: |- DeclAssum BankersQueue_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 v6 ⇔ (∃v5 v4 v3 v2 v1. v6 = QUEUE v5 (v4::v3) v2 v1) ∧ ∀v6' v4 v3. v6 ≠ QUEUE v6' [] v4 v3 Definition of declaration list: |- BankersQueue_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", [Tnum; Tapp [Tvar "a"] "list"; Tnum; Tapp [Tvar "a"] "list"])])]; Dlet (Pvar "empty") (Con "Queue" [Val (Lit (IntLit 0)); Con "Nil" []; Val (Lit (IntLit 0)); Con "Nil" []]); Dlet (Pvar "is_empty") (Fun "v5" (Mat (Var "v5") [(Pcon "Queue" [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"], App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0))))])); Dlet (Pvar "checkf") (Fun "v5" (Mat (Var "v5") [(Pcon "Queue" [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v2") (Var "v4")) (Con "Queue" [Var "v4"; Var "v3"; Var "v2"; Var "v1"]) (Con "Queue" [App (Opn Plus) (Var "v4") (Var "v2"); App Opapp (App Opapp (Var "APPEND") (Var "v3")) (App Opapp (Var "REVERSE") (Var "v1")); Val (Lit (IntLit 0)); Con "Nil" []]))])); Dlet (Pvar "snoc") (Fun "v5" (Fun "v6" (Mat (Var "v5") [(Pcon "Queue" [Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"], App Opapp (Var "checkf") (Con "Queue" [Var "v4"; Var "v3"; App (Opn Plus) (Var "v2") (Val (Lit (IntLit 1))); Con "Cons" [Var "v6"; Var "v1"]]))]))); Dlet (Pvar "head") (Fun "x" (Mat (Var "x") [(Pcon "Queue" [Pvar "v6"; 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 "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], Mat (Var "v5") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (Var "checkf") (Con "Queue" [Let "k" (App (Opn Minus) (Var "v6") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")); Var "v1"; Var "v4"; Var "v3"]))])]))]