This translation extends 'mini_prelude'. Definition of refinement invariant: |- (∀a x_3 x_2 v. TIMES_TYPE a (Twice x_3 x_2) v ⇔ ∃v2_1 v2_2. (v = Conv "Twice" [v2_1; v2_2]) ∧ TIMES_TYPE a x_3 v2_1 ∧ TIMES_TYPE a x_2 v2_2) ∧ ∀a x_1 v. TIMES_TYPE a (Once x_1) v ⇔ ∃v1_1. (v = Conv "Once" [v1_1]) ∧ a x_1 v1_1 Definition of refinement invariant: |- (∀a x_3 x_2 v. DIGIT_TYPE a (Two x_3 x_2) v ⇔ ∃v3_1 v3_2. (v = Conv "Two" [v3_1; v3_2]) ∧ TIMES_TYPE a x_3 v3_1 ∧ TIMES_TYPE a x_2 v3_2) ∧ (∀a x_1 v. DIGIT_TYPE a (One x_1) v ⇔ ∃v2_1. (v = Conv "One" [v2_1]) ∧ TIMES_TYPE a x_1 v2_1) ∧ ∀a v. DIGIT_TYPE a Zero v ⇔ (v = Conv "Zero" []) Definition of refinement invariant: |- (∀a x_4 x_3 x_2 v. QUEUE_TYPE a (Deep x_4 x_3 x_2) v ⇔ ∃v2_1 v2_2 v2_3. (v = Conv "Deep" [v2_1; v2_2; v2_3]) ∧ DIGIT_TYPE a x_4 v2_1 ∧ QUEUE_TYPE a x_3 v2_2 ∧ DIGIT_TYPE a x_2 v2_3) ∧ ∀a x_1 v. QUEUE_TYPE a (Shallow x_1) v ⇔ ∃v1_1. (v = Conv "Shallow" [v1_1]) ∧ DIGIT_TYPE a x_1 v1_1 Certificate theorem for empty: |- DeclAssum ImplicitQueue_decls env ⇒ Eval env (Var "empty") (QUEUE_TYPE a empty) Certificate theorem for is_empty: |- DeclAssum ImplicitQueue_decls env ⇒ Eval env (Var "is_empty") ((QUEUE_TYPE a --> BOOL) is_empty) Certificate theorem for snoc: |- DeclAssum ImplicitQueue_decls env ∧ snoc_side x x1 ⇒ Eval env (Var "snoc") ((Eq (QUEUE_TYPE a) x --> Eq (TIMES_TYPE a) x1 --> QUEUE_TYPE a) snoc) Definition of side condition for snoc: |- snoc_side v1 v2 ⇔ case v1 of Shallow Zero => T | Shallow (One v13) => T | Shallow (Two v__8 v__7) => F | Deep v__14 v__13 Zero => T | Deep v__14 v__13 (One v__11) => snoc_side v__13 (Twice v__11 v2) | Deep v__14 v__13 (Two v__10 v__9) => F Certificate theorem for head: |- DeclAssum ImplicitQueue_decls env ∧ head_side x ⇒ Eval env (Var "head") ((Eq (QUEUE_TYPE a) x --> TIMES_TYPE a) head) Definition of side condition for head: |- head_side v9 ⇔ ((∃v1. v9 = Shallow (One v1)) ∨ (∃v4 v3 v2. v9 = Deep (One v4) v3 v2) ∨ ∃v8 v7 v6 v5. v9 = Deep (Two v8 v7) v6 v5) ∧ ∀v4 v10 v9' v8. ((v9 = Shallow v4) ⇒ ∀v3 v2. v4 ≠ Zero ∧ v4 ≠ Two v3 v2) ∧ (v9 ≠ Deep v10 v9' v8 ∨ v10 ≠ Zero) Certificate theorem for tail: |- DeclAssum ImplicitQueue_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 v1 ⇔ case v1 of Shallow Zero => F | Shallow (One v11) => T | Shallow (Two v__10 v__9) => F | Deep Zero v__16 v__15 => F | Deep (One v__14) v__16 v__15 => ¬is_empty v__16 ⇒ ∀v__13 v__12 v__11. head_side v__16 ∧ head v__16 ≠ Once v__13 ∧ ((head v__16 = Twice v__12 v__11) ⇒ tail_side v__16) | Deep (Two v18 v19) v__16 v__15 => T Definition of declaration list: |- ImplicitQueue_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"],"times", [("Twice",[Tapp [Tvar "a"] "times"; Tapp [Tvar "a"] "times"]); ("Once",[Tvar "a"])])]; Dtype [(["a"],"digit", [("Two",[Tapp [Tvar "a"] "times"; Tapp [Tvar "a"] "times"]); ("One",[Tapp [Tvar "a"] "times"]); ("Zero",[])])]; Dtype [(["a"],"queue", [("Deep", [Tapp [Tvar "a"] "digit"; Tapp [Tvar "a"] "queue"; Tapp [Tvar "a"] "digit"]); ("Shallow",[Tapp [Tvar "a"] "digit"])])]; Dlet (Pvar "empty") (Con "Shallow" [Con "Zero" []]); Dlet (Pvar "is_empty") (Fun "v8" (Mat (Var "v8") [(Pcon "Shallow" [Pvar "v4"], Mat (Var "v4") [(Pcon "Zero" [],Val (Lit (Bool T))); (Pcon "One" [Pvar "v1"],Val (Lit (Bool F))); (Pcon "Two" [Pvar "v3"; Pvar "v2"], Val (Lit (Bool F)))]); (Pcon "Deep" [Pvar "v7"; Pvar "v6"; Pvar "v5"], Val (Lit (Bool F)))])); Dletrec [("snoc","x", Fun "x1" (Mat (Var "x") [(Pcon "Shallow" [Pvar "v4"], Mat (Var "v4") [(Pcon "Zero" [],Con "Shallow" [Con "One" [Var "x1"]]); (Pcon "One" [Pvar "v1"], Con "Deep" [Con "Two" [Var "v1"; Var "x1"]; Var "empty"; Con "Zero" []]); (Pcon "Two" [Pvar "v3"; Pvar "v2"], Raise Bind_error)]); (Pcon "Deep" [Pvar "v10"; Pvar "v9"; Pvar "v8"], Mat (Var "v8") [(Pcon "Zero" [], Con "Deep" [Var "v10"; Var "v9"; Con "One" [Var "x1"]]); (Pcon "One" [Pvar "v5"], Con "Deep" [Var "v10"; App Opapp (App Opapp (Var "snoc") (Var "v9")) (Con "Twice" [Var "v5"; Var "x1"]); Con "Zero" []]); (Pcon "Two" [Pvar "v7"; Pvar "v6"], Raise Bind_error)])]))]; Dlet (Pvar "head") (Fun "x" (Mat (Var "x") [(Pcon "Shallow" [Pvar "v4"], Mat (Var "v4") [(Pcon "Zero" [],Raise Bind_error); (Pcon "One" [Pvar "v1"],Var "v1"); (Pcon "Two" [Pvar "v3"; Pvar "v2"],Raise Bind_error)]); (Pcon "Deep" [Pvar "v10"; Pvar "v9"; Pvar "v8"], Mat (Var "v10") [(Pcon "Zero" [],Raise Bind_error); (Pcon "One" [Pvar "v5"],Var "v5"); (Pcon "Two" [Pvar "v7"; Pvar "v6"],Var "v7")])])); Dletrec [("tail","x", Mat (Var "x") [(Pcon "Shallow" [Pvar "v4"], Mat (Var "v4") [(Pcon "Zero" [],Raise Bind_error); (Pcon "One" [Pvar "v1"],Var "empty"); (Pcon "Two" [Pvar "v3"; Pvar "v2"],Raise Bind_error)]); (Pcon "Deep" [Pvar "v13"; Pvar "v12"; Pvar "v11"], Mat (Var "v13") [(Pcon "Zero" [],Raise Bind_error); (Pcon "One" [Pvar "v8"], If (App Opapp (Var "is_empty") (Var "v12")) (Con "Shallow" [Var "v11"]) (Mat (App Opapp (Var "head") (Var "v12")) [(Pcon "Once" [Pvar "v5"],Raise Bind_error); (Pcon "Twice" [Pvar "v7"; Pvar "v6"], Con "Deep" [Con "Two" [Var "v7"; Var "v6"]; App Opapp (Var "tail") (Var "v12"); Var "v11"])])); (Pcon "Two" [Pvar "v10"; Pvar "v9"], Con "Deep" [Con "One" [Var "v9"]; Var "v12"; Var "v11"])])])]]