This translation extends 'mini_prelude'. Definition of refinement invariant: |- (∀a x_9 v. STATUS_TYPE a (Finished x_9) v ⇔ ∃v4_1. (v = Conv "Finished" [v4_1]) ∧ LIST_TYPE a x_9 v4_1) ∧ (∀a x_8 x_7 x_6 v. STATUS_TYPE a (Appending x_8 x_7 x_6) v ⇔ ∃v3_1 v3_2 v3_3. (v = Conv "Appending" [v3_1; v3_2; v3_3]) ∧ NUM x_8 v3_1 ∧ LIST_TYPE a x_7 v3_2 ∧ LIST_TYPE a x_6 v3_3) ∧ (∀a x_5 x_4 x_3 x_2 x_1 v. STATUS_TYPE a (Reversing x_5 x_4 x_3 x_2 x_1) v ⇔ ∃v2_1 v2_2 v2_3 v2_4 v2_5. (v = Conv "Reversing" [v2_1; v2_2; v2_3; v2_4; v2_5]) ∧ NUM x_5 v2_1 ∧ LIST_TYPE a x_4 v2_2 ∧ LIST_TYPE a x_3 v2_3 ∧ LIST_TYPE a x_2 v2_4 ∧ LIST_TYPE a x_1 v2_5) ∧ ∀a v. STATUS_TYPE a Idle v ⇔ (v = Conv "Idle" []) Certificate theorem for exec: |- DeclAssum HoodMelvilleQueue_decls env ⇒ Eval env (Var "exec") ((STATUS_TYPE a --> STATUS_TYPE a) exec) Certificate theorem for invalidate: |- DeclAssum HoodMelvilleQueue_decls env ⇒ Eval env (Var "invalidate") ((STATUS_TYPE a --> STATUS_TYPE a) invalidate) Definition of refinement invariant: |- ∀a x_5 x_4 x_3 x_2 x_1 v. QUEUE_TYPE a (QUEUE x_5 x_4 x_3 x_2 x_1) v ⇔ ∃v1_1 v1_2 v1_3 v1_4 v1_5. (v = Conv "Queue" [v1_1; v1_2; v1_3; v1_4; v1_5]) ∧ NUM x_5 v1_1 ∧ LIST_TYPE a x_4 v1_2 ∧ STATUS_TYPE a x_3 v1_3 ∧ NUM x_2 v1_4 ∧ LIST_TYPE a x_1 v1_5 Certificate theorem for exec2: |- DeclAssum HoodMelvilleQueue_decls env ⇒ Eval env (Var "exec2") ((QUEUE_TYPE a --> QUEUE_TYPE a) exec2) Certificate theorem for check: |- DeclAssum HoodMelvilleQueue_decls env ⇒ Eval env (Var "check") ((QUEUE_TYPE a --> QUEUE_TYPE a) check) Certificate theorem for empty: |- DeclAssum HoodMelvilleQueue_decls env ⇒ Eval env (Var "empty") (QUEUE_TYPE a empty) Certificate theorem for is_empty: |- DeclAssum HoodMelvilleQueue_decls env ⇒ Eval env (Var "is_empty") ((INT --> a --> b --> c --> d --> BOOL) is_empty) Certificate theorem for snoc: |- DeclAssum HoodMelvilleQueue_decls env ⇒ Eval env (Var "snoc") ((QUEUE_TYPE a --> a --> QUEUE_TYPE a) snoc) Certificate theorem for head: |- DeclAssum HoodMelvilleQueue_decls env ∧ head_side x ⇒ Eval env (Var "head") ((Eq (QUEUE_TYPE a) x --> a) head) Definition of side condition for head: |- head_side v2 ⇔ (∃v0 v1 v1' v2' v3 v4. v2 = QUEUE v0 (v1::v1') v2' v3 v4) ∧ ∀v7 v5 v4 v3. v2 ≠ QUEUE v7 [] v5 v4 v3 Certificate theorem for tail: |- DeclAssum HoodMelvilleQueue_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 v7 ⇔ (∃v6 v5 v4 v3 v2 v1. v7 = QUEUE v6 (v5::v4) v3 v2 v1) ∧ ∀v7' v5 v4 v3. v7 ≠ QUEUE v7' [] v5 v4 v3 Definition of declaration list: |- HoodMelvilleQueue_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"],"status", [("Finished",[Tapp [Tvar "a"] "list"]); ("Appending", [Tnum; Tapp [Tvar "a"] "list"; Tapp [Tvar "a"] "list"]); ("Reversing", [Tnum; Tapp [Tvar "a"] "list"; Tapp [Tvar "a"] "list"; Tapp [Tvar "a"] "list"; Tapp [Tvar "a"] "list"]); ("Idle",[])])]; Dlet (Pvar "exec") (Fun "v22" (Mat (Var "v22") [(Pcon "Idle" [],Con "Idle" []); (Pcon "Reversing" [Pvar "v13"; Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"], Mat (Var "v12") [(Pcon "Nil" [], Mat (Var "v10") [(Pcon "Nil" [], Con "Reversing" [Var "v13"; Con "Nil" []; Var "v11"; Con "Nil" []; Var "v9"]); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Nil" [], Con "Appending" [Var "v13"; Var "v11"; Con "Cons" [Var "v4"; Var "v9"]]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Reversing" [Var "v13"; Con "Nil" []; Var "v11"; Con "Cons" [Var "v4"; Con "Cons" [Var "v2"; Var "v1"]]; Var "v9"])])]); (Pcon "Cons" [Pvar "v8"; Pvar "v7"], Mat (Var "v10") [(Pcon "Nil" [], Con "Reversing" [Var "v13"; Con "Cons" [Var "v8"; Var "v7"]; Var "v11"; Con "Nil" []; Var "v9"]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Con "Reversing" [App (Opn Plus) (Var "v13") (Val (Lit (IntLit 1))); Var "v7"; Con "Cons" [Var "v8"; Var "v11"]; Var "v5"; Con "Cons" [Var "v6"; Var "v9"]])])]); (Pcon "Appending" [Pvar "v20"; Pvar "v19"; Pvar "v18"], If (App (Opb Leq) (Var "v20") (Val (Lit (IntLit 0)))) (Mat (Var "v19") [(Pcon "Nil" [],Con "Finished" [Var "v18"]); (Pcon "Cons" [Pvar "v15"; Pvar "v14"], Con "Finished" [Var "v18"])]) (Mat (Var "v19") [(Pcon "Nil" [], Con "Appending" [Var "v20"; Con "Nil" []; Var "v18"]); (Pcon "Cons" [Pvar "v17"; Pvar "v16"], Con "Appending" [App (Opn Minus) (Var "v20") (Val (Lit (IntLit 1))); Var "v16"; Con "Cons" [Var "v17"; Var "v18"]])])); (Pcon "Finished" [Pvar "v21"], Con "Finished" [Var "v21"])])); Dlet (Pvar "invalidate") (Fun "v12" (Mat (Var "v12") [(Pcon "Idle" [],Con "Idle" []); (Pcon "Reversing" [Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"], Con "Reversing" [Let "k" (App (Opn Minus) (Var "v5") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")); Var "v4"; Var "v3"; Var "v2"; Var "v1"]); (Pcon "Appending" [Pvar "v10"; Pvar "v9"; Pvar "v8"], If (App (Opb Leq) (Var "v10") (Val (Lit (IntLit 0)))) (Mat (Var "v8") [(Pcon "Nil" [], Con "Appending" [Val (Lit (IntLit 0)); Var "v9"; Con "Nil" []]); (Pcon "Cons" [Pvar "v7"; Pvar "v6"], Con "Finished" [Var "v6"])]) (Con "Appending" [App (Opn Minus) (Var "v10") (Val (Lit (IntLit 1))); Var "v9"; Var "v8"])); (Pcon "Finished" [Pvar "v11"], Con "Finished" [Var "v11"])])); Dtype [(["a"],"queue", [("Queue", [Tnum; Tapp [Tvar "a"] "list"; Tapp [Tvar "a"] "status"; Tnum; Tapp [Tvar "a"] "list"])])]; Dlet (Pvar "exec2") (Fun "v15" (Mat (Var "v15") [(Pcon "Queue" [Pvar "v14"; Pvar "v13"; Pvar "v12"; Pvar "v11"; Pvar "v10"], Mat (App Opapp (Var "exec") (App Opapp (Var "exec") (Var "v12"))) [(Pcon "Idle" [], Con "Queue" [Var "v14"; Var "v13"; Con "Idle" []; Var "v11"; Var "v10"]); (Pcon "Reversing" [Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"], Con "Queue" [Var "v14"; Var "v13"; Con "Reversing" [Var "v5"; Var "v4"; Var "v3"; Var "v2"; Var "v1"]; Var "v11"; Var "v10"]); (Pcon "Appending" [Pvar "v8"; Pvar "v7"; Pvar "v6"], Con "Queue" [Var "v14"; Var "v13"; Con "Appending" [Var "v8"; Var "v7"; Var "v6"]; Var "v11"; Var "v10"]); (Pcon "Finished" [Pvar "v9"], Con "Queue" [Var "v14"; Var "v9"; Con "Idle" []; Var "v11"; Var "v10"])])])); Dlet (Pvar "check") (Fun "v7" (Mat (Var "v7") [(Pcon "Queue" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"], If (App (Opb Leq) (Var "v3") (Var "v6")) (App Opapp (Var "exec2") (Con "Queue" [Var "v6"; Var "v5"; Var "v4"; Var "v3"; Var "v2"])) (Let "v1" (Con "Reversing" [Val (Lit (IntLit 0)); Var "v5"; Con "Nil" []; Var "v2"; Con "Nil" []]) (App Opapp (Var "exec2") (Con "Queue" [App (Opn Plus) (Var "v6") (Var "v3"); Var "v5"; Var "v1"; Val (Lit (IntLit 0)); Con "Nil" []]))))])); Dlet (Pvar "empty") (Con "Queue" [Val (Lit (IntLit 0)); Con "Nil" []; Con "Idle" []; Val (Lit (IntLit 0)); Con "Nil" []]); Dlet (Pvar "is_empty") (Fun "v1" (Fun "v2" (Fun "v3" (Fun "v4" (Fun "v5" (App Equality (Var "v1") (Val (Lit (IntLit 0))))))))); Dlet (Pvar "snoc") (Fun "v6" (Fun "v7" (Mat (Var "v6") [(Pcon "Queue" [Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"], App Opapp (Var "check") (Con "Queue" [Var "v5"; Var "v4"; Var "v3"; App (Opn Plus) (Var "v2") (Val (Lit (IntLit 1))); Con "Cons" [Var "v7"; Var "v1"]]))]))); Dlet (Pvar "head") (Fun "x" (Mat (Var "x") [(Pcon "Queue" [Pvar "v7"; Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], Mat (Var "v6") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v2")])])); Dlet (Pvar "tail") (Fun "x" (Mat (Var "x") [(Pcon "Queue" [Pvar "v7"; Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], Mat (Var "v6") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (Var "check") (Con "Queue" [Let "k" (App (Opn Minus) (Var "v7") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")); Var "v1"; App Opapp (Var "invalidate") (Var "v5"); Var "v4"; Var "v3"]))])]))]