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]) ∧ a x_3 v2_1 ∧ HEAP_TYPE 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 LazyPairingHeap_decls env ⇒ Eval env (Var "empty") (HEAP_TYPE a empty) Certificate theorem for is_empty: |- DeclAssum LazyPairingHeap_decls env ⇒ Eval env (Var "is_empty") ((HEAP_TYPE a --> BOOL) is_empty) Certificate theorem for merge: |- DeclAssum LazyPairingHeap_decls env ⇒ Eval env (Var "merge") (((a --> b) --> (b --> b --> BOOL) --> HEAP_TYPE a --> HEAP_TYPE a --> HEAP_TYPE a) merge) Certificate theorem for insert: |- DeclAssum LazyPairingHeap_decls env ⇒ Eval env (Var "insert") (((a --> b) --> (b --> b --> BOOL) --> a --> HEAP_TYPE a --> HEAP_TYPE a) insert) Certificate theorem for find_min: |- DeclAssum LazyPairingHeap_decls env ∧ find_min_side x1 ⇒ Eval env (Var "find_min") ((Eq (HEAP_TYPE a) x1 --> a) find_min) Definition of side condition for find_min: |- find_min_side v2 ⇔ v2 ≠ Empty ∧ ∃v1 v0 v1'. v2 = Tree v1 v0 v1' Certificate theorem for delete_min: |- DeclAssum LazyPairingHeap_decls env ∧ delete_min_side x1 x2 x3 ⇒ Eval env (Var "delete_min") ((Eq (a --> b) x1 --> Eq (b --> b --> BOOL) x2 --> Eq (HEAP_TYPE a) x3 --> HEAP_TYPE a) delete_min) Definition of side condition for delete_min: |- delete_min_side v5 v4 v3 ⇔ (∃v0 v2 v1. v3 = Tree v0 v2 v1) ∧ v3 ≠ Empty Definition of declaration list: |- LazyPairingHeap_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", [Tvar "a"; Tapp [Tvar "a"] "heap"; 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 [("merge","v18", Fun "v19" (Fun "v16" (Fun "v17" (Mat (Var "v16") [(Pcon "Empty" [], Mat (Var "v17") [(Pcon "Empty" [],Con "Empty" []); (Pcon "Tree" [Pvar "v3"; Pvar "v2"; Pvar "v1"], Con "Tree" [Var "v3"; Var "v2"; Var "v1"])]); (Pcon "Tree" [Pvar "v15"; Pvar "v14"; Pvar "v13"], Mat (Var "v17") [(Pcon "Empty" [], Con "Tree" [Var "v15"; Var "v14"; Var "v13"]); (Pcon "Tree" [Pvar "v12"; Pvar "v11"; Pvar "v10"], If (App Opapp (App Opapp (Var "v19") (App Opapp (Var "v18") (Var "v15"))) (App Opapp (Var "v18") (Var "v12"))) (Mat (Var "v14") [(Pcon "Empty" [], Con "Tree" [Var "v15"; Con "Tree" [Var "v12"; Var "v11"; Var "v10"]; Var "v13"]); (Pcon "Tree" [Pvar "v6"; Pvar "v5"; Pvar "v4"], Con "Tree" [Var "v15"; Con "Empty" []; App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v18")) (Var "v19")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v18")) (Var "v19")) (Con "Tree" [Var "v12"; Var "v11"; Var "v10"])) (Var "v14"))) (Var "v13")])]) (Mat (Var "v11") [(Pcon "Empty" [], Con "Tree" [Var "v12"; Con "Tree" [Var "v15"; Var "v14"; Var "v13"]; Var "v10"]); (Pcon "Tree" [Pvar "v9"; Pvar "v8"; Pvar "v7"], Con "Tree" [Var "v12"; Con "Empty" []; App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v18")) (Var "v19")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v18")) (Var "v19")) (Con "Tree" [Var "v15"; Var "v14"; Var "v13"])) (Var "v11"))) (Var "v10")])]))])]))))]; Dlet (Pvar "insert") (Fun "v2" (Fun "v3" (Fun "v4" (Fun "v1" (App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "v2")) (Var "v3")) (Con "Tree" [Var "v4"; Con "Empty" []; Con "Empty" []])) (Var "v1")))))); Dlet (Pvar "find_min") (Fun "x1" (Mat (Var "x1") [(Pcon "Empty" [],Raise Bind_error); (Pcon "Tree" [Pvar "v3"; Pvar "v2"; Pvar "v1"], Var "v3")])); Dlet (Pvar "delete_min") (Fun "x1" (Fun "x2" (Fun "x3" (Mat (Var "x3") [(Pcon "Empty" [],Raise Bind_error); (Pcon "Tree" [Pvar "v3"; Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (App Opapp (App Opapp (Var "merge") (Var "x1")) (Var "x2")) (Var "v2")) (Var "v1"))]))))]