This translation extends 'mini_prelude'. Definition of refinement invariant: |- (∀a x_3 x_2 x_1 v. HEAP_TYPE a (Tree x_3 x_2 x_1) v ⇔ ∃v2_1 v2_2 v2_3. (v = Conv "Tree" [v2_1; v2_2; v2_3]) ∧ HEAP_TYPE a x_3 v2_1 ∧ a x_2 v2_2 ∧ HEAP_TYPE a x_1 v2_3) ∧ ∀a v. HEAP_TYPE a Empty v ⇔ (v = Conv "Empty" []) Certificate theorem for empty: |- DeclAssum SplayHeap_decls env ⇒ Eval env (Var "empty") (HEAP_TYPE a empty) Certificate theorem for is_empty: |- DeclAssum SplayHeap_decls env ⇒ Eval env (Var "is_empty") ((HEAP_TYPE a --> BOOL) is_empty) Certificate theorem for partition: |- DeclAssum SplayHeap_decls env ⇒ Eval env (Var "partition") (((a --> b) --> (b --> b --> BOOL) --> a --> HEAP_TYPE a --> PAIR_TYPE (HEAP_TYPE a) (HEAP_TYPE a)) partition) Certificate theorem for insert: |- DeclAssum SplayHeap_decls env ⇒ Eval env (Var "insert") (((a --> b) --> (b --> b --> BOOL) --> a --> HEAP_TYPE a --> HEAP_TYPE a) insert) Certificate theorem for merge: |- DeclAssum SplayHeap_decls env ⇒ Eval env (Var "merge") (((a --> b) --> (b --> b --> BOOL) --> HEAP_TYPE a --> HEAP_TYPE a --> HEAP_TYPE a) merge) Certificate theorem for find_min: |- DeclAssum SplayHeap_decls env ∧ find_min_side x ⇒ Eval env (Var "find_min") ((Eq (HEAP_TYPE a) x --> a) find_min) Definition of side condition for find_min: |- find_min_side v1 ⇔ case v1 of Empty => F | Tree Empty v__12 v__11 => T | Tree (Tree v__10 v__9 v__8) v__12 v__11 => find_min_side (Tree v__10 v__9 v__8) Certificate theorem for delete_min: |- DeclAssum SplayHeap_decls env ∧ delete_min_side x ⇒ Eval env (Var "delete_min") ((Eq (HEAP_TYPE a) x --> HEAP_TYPE a) delete_min) Definition of side condition for delete_min: |- delete_min_side v1 ⇔ case v1 of Empty => F | Tree Empty v__21 v__20 => T | Tree (Tree Empty v__18 v__17) v__21 v__20 => T | Tree (Tree (Tree v__16 v__15 v__14) v__18 v__17) v__21 v__20 => delete_min_side (Tree v__16 v__15 v__14) Definition of declaration list: |- SplayHeap_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"],"heap", [("Tree", [Tapp [Tvar "a"] "heap"; Tvar "a"; Tapp [Tvar "a"] "heap"]); ("Empty",[])])]; Dlet (Pvar "empty") (Con "Empty" []); Dlet (Pvar "is_empty") (Fun "v4" (Mat (Var "v4") [(Pcon "Empty" [],Val (Lit (Bool T))); (Pcon "Tree" [Pvar "v3"; Pvar "v2"; Pvar "v1"], Val (Lit (Bool F)))])); Dletrec [("partition","v22", Fun "v23" (Fun "v24" (Fun "v25" (Mat (Var "v25") [(Pcon "Empty" [], Con "Pair" [Con "Empty" []; Con "Empty" []]); (Pcon "Tree" [Pvar "v21"; Pvar "v20"; Pvar "v19"], If (App Opapp (App Opapp (Var "v23") (App Opapp (Var "v22") (Var "v20"))) (App Opapp (Var "v22") (Var "v24"))) (Mat (Var "v19") [(Pcon "Empty" [], Con "Pair" [Con "Tree" [Var "v21"; Var "v20"; Var "v19"]; Con "Empty" []]); (Pcon "Tree" [Pvar "v9"; Pvar "v8"; Pvar "v7"], If (App Opapp (App Opapp (Var "v23") (App Opapp (Var "v22") (Var "v8"))) (App Opapp (Var "v22") (Var "v24"))) (Let "v3" (App Opapp (App Opapp (App Opapp (App Opapp (Var "partition") (Var "v22")) (Var "v23")) (Var "v24")) (Var "v7")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Con "Tree" [Con "Tree" [Var "v21"; Var "v20"; Var "v9"]; Var "v8"; Var "v2"]; Var "v1"])])) (Let "v6" (App Opapp (App Opapp (App Opapp (App Opapp (Var "partition") (Var "v22")) (Var "v23")) (Var "v24")) (Var "v9")) (Mat (Var "v6") [(Pcon "Pair" [Pvar "v5"; Pvar "v4"], Con "Pair" [Con "Tree" [Var "v21"; Var "v20"; Var "v5"]; Con "Tree" [Var "v4"; Var "v8"; Var "v7"]])])))]) (Mat (Var "v21") [(Pcon "Empty" [], Con "Pair" [Con "Empty" []; Con "Tree" [Var "v21"; Var "v20"; Var "v19"]]); (Pcon "Tree" [Pvar "v18"; Pvar "v17"; Pvar "v16"], If (App Opapp (App Opapp (Var "v23") (App Opapp (Var "v22") (Var "v17"))) (App Opapp (Var "v22") (Var "v24"))) (Let "v12" (App Opapp (App Opapp (App Opapp (App Opapp (Var "partition") (Var "v22")) (Var "v23")) (Var "v24")) (Var "v16")) (Mat (Var "v12") [(Pcon "Pair" [Pvar "v11"; Pvar "v10"], Con "Pair" [Con "Tree" [Var "v18"; Var "v17"; Var "v11"]; Con "Tree" [Var "v10"; Var "v20"; Var "v19"]])])) (Let "v15" (App Opapp (App Opapp (App Opapp (App Opapp (Var "partition") (Var "v22")) (Var "v23")) (Var "v24")) (Var "v18")) (Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Con "Pair" [Var "v14"; Con "Tree" [Var "v13"; Var "v17"; Con "Tree" [Var "v16"; Var "v20"; Var "v19"]]])])))]))]))))]; Dlet (Pvar "insert") (Fun "v4" (Fun "v5" (Fun "v7" (Fun "v6" (Let "v3" (App Opapp (App Opapp (App Opapp (App Opapp (Var "partition") (Var "v4")) (Var "v5")) (Var "v7")) (Var "v6")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Tree" [Var "v2"; Var "v7"; Var "v1"])])))))); Dletrec [("merge","v8", Fun "v9" (Fun "v10" (Fun "v7" (Mat (Var "v10") [(Pcon "Empty" [],Var "v7"); (Pcon "Tree" [Pvar "v6"; Pvar "v5"; Pvar "v4"], Let "v3" (App Opapp (App Opapp (App Opapp (App Opapp (Var "partition") (Var "v8")) (Var "v9")) (Var "v5")) (Var "v7")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Tree" [App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v8")) (Var "v9")) (Var "v2")) (Var "v6"); Var "v5"; App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v8")) (Var "v9")) (Var "v1")) (Var "v4")])]))]))))]; Dletrec [("find_min","x", Mat (Var "x") [(Pcon "Empty" [],Raise Bind_error); (Pcon "Tree" [Pvar "v6"; Pvar "v5"; Pvar "v4"], Mat (Var "v6") [(Pcon "Empty" [],Var "v5"); (Pcon "Tree" [Pvar "v3"; Pvar "v2"; Pvar "v1"], App Opapp (Var "find_min") (Con "Tree" [Var "v3"; Var "v2"; Var "v1"]))])])]; Dletrec [("delete_min","x", Mat (Var "x") [(Pcon "Empty" [],Raise Bind_error); (Pcon "Tree" [Pvar "v9"; Pvar "v8"; Pvar "v7"], Mat (Var "v9") [(Pcon "Empty" [],Var "v7"); (Pcon "Tree" [Pvar "v6"; Pvar "v5"; Pvar "v4"], Mat (Var "v6") [(Pcon "Empty" [], Con "Tree" [Var "v4"; Var "v8"; Var "v7"]); (Pcon "Tree" [Pvar "v3"; Pvar "v2"; Pvar "v1"], Con "Tree" [App Opapp (Var "delete_min") (Con "Tree" [Var "v3"; Var "v2"; Var "v1"]); Var "v5"; Con "Tree" [Var "v4"; Var "v8"; Var "v7"]])])])])]]