This translation extends 'mini_prelude'. Certificate theorem for empty: |- DeclAssum BinomialHeap_decls env ⇒ Eval env (Var "empty") (LIST_TYPE a empty) Certificate theorem for is_empty: |- DeclAssum BinomialHeap_decls env ⇒ Eval env (Var "is_empty") ((LIST_TYPE a --> BOOL) is_empty) Definition of refinement invariant: |- TREE_TYPE a (Node x_3 x_2 x_1) v ⇔ ∃v1_1 v1_2 v1_3. (v = Conv "Node" [v1_1; v1_2; v1_3]) ∧ NUM x_3 v1_1 ∧ a x_2 v1_2 ∧ LIST_TYPE (TREE_TYPE a) x_1 v1_3 Certificate theorem for rank: |- DeclAssum BinomialHeap_decls env ⇒ Eval env (Var "rank") ((TREE_TYPE a --> NUM) rank) Certificate theorem for root: |- DeclAssum BinomialHeap_decls env ⇒ Eval env (Var "root") ((TREE_TYPE a --> a) root) Certificate theorem for link: |- DeclAssum BinomialHeap_decls env ⇒ Eval env (Var "link") (((a --> b) --> (b --> b --> BOOL) --> TREE_TYPE a --> TREE_TYPE a --> TREE_TYPE a) link) Certificate theorem for ins_tree: |- DeclAssum BinomialHeap_decls env ⇒ Eval env (Var "ins_tree") (((a --> b) --> (b --> b --> BOOL) --> TREE_TYPE a --> LIST_TYPE (TREE_TYPE a) --> LIST_TYPE (TREE_TYPE a)) ins_tree) Certificate theorem for insert: |- DeclAssum BinomialHeap_decls env ⇒ Eval env (Var "insert") (((a --> b) --> (b --> b --> BOOL) --> a --> LIST_TYPE (TREE_TYPE a) --> LIST_TYPE (TREE_TYPE a)) insert) Certificate theorem for merge: |- DeclAssum BinomialHeap_decls env ⇒ Eval env (Var "merge") (((a --> b) --> (b --> b --> BOOL) --> LIST_TYPE (TREE_TYPE a) --> LIST_TYPE (TREE_TYPE a) --> LIST_TYPE (TREE_TYPE a)) merge) Certificate theorem for remove_min_tree: |- DeclAssum BinomialHeap_decls env ∧ remove_min_tree_side x x1 x2 ⇒ Eval env (Var "remove_min_tree") ((Eq (a --> b) x --> Eq (b --> b --> BOOL) x1 --> Eq (LIST_TYPE (TREE_TYPE a)) x2 --> PAIR_TYPE (TREE_TYPE a) (LIST_TYPE (TREE_TYPE a))) remove_min_tree) Definition of side condition for remove_min_tree: |- remove_min_tree_side v1 v2 v3 ⇔ case v3 of [] => F | [v__8] => T | v__8::v__6::v__5 => remove_min_tree_side v1 v2 (v__6::v__5) Certificate theorem for find_min: |- DeclAssum BinomialHeap_decls env ∧ find_min_side v4 v5 v6 ⇒ Eval env (Var "find_min") ((Eq (a --> b) v4 --> Eq (b --> b --> BOOL) v5 --> Eq (LIST_TYPE (TREE_TYPE a)) v6 --> a) find_min) Definition of side condition for find_min: |- find_min_side v4 v5 v6 ⇔ remove_min_tree_side v4 v5 v6 Certificate theorem for delete_min: |- DeclAssum BinomialHeap_decls env ∧ delete_min_side v6 v7 v8 ⇒ Eval env (Var "delete_min") ((Eq (a --> b) v6 --> Eq (b --> b --> BOOL) v7 --> Eq (LIST_TYPE (TREE_TYPE a)) v8 --> LIST_TYPE (TREE_TYPE a)) delete_min) Definition of side condition for delete_min: |- delete_min_side v6 v7 v8 ⇔ remove_min_tree_side v6 v7 v8 Definition of declaration list: |- BinomialHeap_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" []))); Dlet (Pvar "empty") (Con "Nil" []); Dlet (Pvar "is_empty") (Fun "v3" (Mat (Var "v3") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Val (Lit (Bool F)))])); Dtype [(["a"],"tree", [("Node", [Tnum; Tvar "a"; Tapp [Tapp [Tvar "a"] "tree"] "list"])])]; Dlet (Pvar "rank") (Fun "v4" (Mat (Var "v4") [(Pcon "Node" [Pvar "v3"; Pvar "v2"; Pvar "v1"], Var "v3")])); Dlet (Pvar "root") (Fun "v4" (Mat (Var "v4") [(Pcon "Node" [Pvar "v3"; Pvar "v2"; Pvar "v1"], Var "v2")])); Dlet (Pvar "link") (Fun "v8" (Fun "v9" (Fun "v10" (Fun "v7" (Mat (Var "v10") [(Pcon "Node" [Pvar "v6"; Pvar "v5"; Pvar "v4"], Mat (Var "v7") [(Pcon "Node" [Pvar "v3"; Pvar "v2"; Pvar "v1"], If (App Opapp (App Opapp (Var "v9") (App Opapp (Var "v8") (Var "v5"))) (App Opapp (Var "v8") (Var "v2"))) (Con "Node" [App (Opn Plus) (Var "v6") (Val (Lit (IntLit 1))); Var "v5"; Con "Cons" [Con "Node" [Var "v3"; Var "v2"; Var "v1"]; Var "v4"]]) (Con "Node" [App (Opn Plus) (Var "v6") (Val (Lit (IntLit 1))); Var "v2"; Con "Cons" [Con "Node" [Var "v6"; Var "v5"; Var "v4"]; Var "v1"]]))])]))))); Dletrec [("ins_tree","v3", Fun "v4" (Fun "v5" (Fun "v6" (Mat (Var "v6") [(Pcon "Nil" [],Con "Cons" [Var "v5"; Con "Nil" []]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App (Opb Lt) (App Opapp (Var "rank") (Var "v5")) (App Opapp (Var "rank") (Var "v2"))) (Con "Cons" [Var "v5"; Con "Cons" [Var "v2"; Var "v1"]]) (App Opapp (App Opapp (App Opapp (App Opapp (Var "ins_tree") (Var "v3")) (Var "v4")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "link") (Var "v3")) (Var "v4")) (Var "v5")) (Var "v2"))) (Var "v1")))]))))]; Dlet (Pvar "insert") (Fun "v1" (Fun "v2" (Fun "v4" (Fun "v3" (App Opapp (App Opapp (App Opapp (App Opapp (Var "ins_tree") (Var "v1")) (Var "v2")) (Con "Node" [Val (Lit (IntLit 0)); Var "v4"; Con "Nil" []])) (Var "v3")))))); Dletrec [("merge","v8", Fun "v9" (Fun "v10" (Fun "v7" (Mat (Var "v10") [(Pcon "Nil" [], Mat (Var "v7") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [Var "v2"; Var "v1"])]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Mat (Var "v7") [(Pcon "Nil" [],Con "Cons" [Var "v6"; Var "v5"]); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], If (App (Opb Lt) (App Opapp (Var "rank") (Var "v6")) (App Opapp (Var "rank") (Var "v4"))) (Con "Cons" [Var "v6"; App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v8")) (Var "v9")) (Var "v5")) (Con "Cons" [Var "v4"; Var "v3"])]) (If (App (Opb Lt) (App Opapp (Var "rank") (Var "v4")) (App Opapp (Var "rank") (Var "v6"))) (Con "Cons" [Var "v4"; App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v8")) (Var "v9")) (Con "Cons" [Var "v6"; Var "v5"])) (Var "v3")]) (App Opapp (App Opapp (App Opapp (App Opapp (Var "ins_tree") (Var "v8")) (Var "v9")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "link") (Var "v8")) (Var "v9")) (Var "v6")) (Var "v4"))) (App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v8")) (Var "v9")) (Var "v5")) (Var "v3")))))])]))))]; Dletrec [("remove_min_tree","x", Fun "x1" (Fun "x2" (Mat (Var "x2") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v7"; Pvar "v6"], Mat (Var "v6") [(Pcon "Nil" [], Con "Pair" [Var "v7"; Con "Nil" []]); (Pcon "Cons" [Pvar "v5"; Pvar "v4"], Let "v3" (App Opapp (App Opapp (App Opapp (Var "remove_min_tree") (Var "x")) (Var "x1")) (Con "Cons" [Var "v5"; Var "v4"])) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], If (App Opapp (App Opapp (Var "x1") (App Opapp (Var "x") (App Opapp (Var "root") (Var "v7")))) (App Opapp (Var "x") (App Opapp (Var "root") (Var "v2")))) (Con "Pair" [Var "v7"; Con "Cons" [Var "v5"; Var "v4"]]) (Con "Pair" [Var "v2"; Con "Cons" [Var "v7"; Var "v1"]]))]))])])))]; Dlet (Pvar "find_min") (Fun "v4" (Fun "v5" (Fun "v6" (Let "v3" (App Opapp (App Opapp (App Opapp (Var "remove_min_tree") (Var "v4")) (Var "v5")) (Var "v6")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], App Opapp (Var "root") (Var "v2"))]))))); Dlet (Pvar "delete_min") (Fun "v6" (Fun "v7" (Fun "v8" (Mat (App Opapp (App Opapp (App Opapp (Var "remove_min_tree") (Var "v6")) (Var "v7")) (Var "v8")) [(Pcon "Pair" [Pvar "v5"; Pvar "v4"], Mat (Var "v5") [(Pcon "Node" [Pvar "v3"; Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v6")) (Var "v7")) (App Opapp (Var "REVERSE") (Var "v1"))) (Var "v4"))])]))))]