This translation extends 'mini_prelude'.

Certificate theorem for FST:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "FST") ((PAIR_TYPE a b --> a) FST)

Certificate theorem for SND:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "SND") ((PAIR_TYPE a b --> b) SND)

Certificate theorem for CURRY:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "CURRY")
     (((PAIR_TYPE a b --> c) --> a --> b --> c) CURRY)

Certificate theorem for UNCURRY:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "UNCURRY")
     (((a --> b --> c) --> PAIR_TYPE a b --> c) UNCURRY)

Certificate theorem for o:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "o") (((c --> b) --> (a --> c) --> a --> b) $o)

Certificate theorem for I:

|- DeclAssum std_prelude_decls env ⇒ Eval env (Var "I") ((a --> a) I)

Certificate theorem for C:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "C") (((a --> b --> c) --> b --> a --> c) combin$C)

Certificate theorem for K:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "K") ((a --> b --> a) K)

Certificate theorem for S:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "S") (((a --> b --> c) --> (a --> b) --> a --> c) S)

Certificate theorem for UPDATE:

|- DeclAssum std_prelude_decls env ∧ EqualityType a ⇒
   Eval env (Var "UPDATE") ((a --> b --> (a --> b) --> a --> b) $=+)

Certificate theorem for W:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "W") (((a --> a --> b) --> a --> b) W)

Definition of refinement invariant:

|- ∀v. ONE_TYPE () v ⇔ (v = Conv "One" [])

Definition of refinement invariant:

|- (∀a x_1 v.
      OPTION_TYPE a (SOME x_1) v ⇔
      ∃v2_1. (v = Conv "Some" [v2_1]) ∧ a x_1 v2_1) ∧
   ∀a v. OPTION_TYPE a NONE v ⇔ (v = Conv "None" [])

Certificate theorem for THE:

|- DeclAssum std_prelude_decls env ∧ IS_SOME x1 ⇒
   Eval env (Var "THE") ((Eq (OPTION_TYPE a) x1 --> a) THE)

Certificate theorem for IS_NONE:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "IS_NONE") ((OPTION_TYPE a --> BOOL) IS_NONE)

Certificate theorem for IS_SOME:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "IS_SOME") ((OPTION_TYPE a --> BOOL) IS_SOME)

Certificate theorem for OPTION_MAP:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "OPTION_MAP")
     (((a --> b) --> OPTION_TYPE a --> OPTION_TYPE b) OPTION_MAP)

Certificate theorem for OPTION_MAP2:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "OPTION_MAP2")
     (((b --> c --> a) --> OPTION_TYPE b --> OPTION_TYPE c -->
       OPTION_TYPE a) OPTION_MAP2)

Definition of refinement invariant:

|- (∀a b x_2 v.
      SUM_TYPE a b (INR x_2) v ⇔
      ∃v2_1. (v = Conv "Inr" [v2_1]) ∧ b x_2 v2_1) ∧
   ∀a b x_1 v.
     SUM_TYPE a b (INL x_1) v ⇔
     ∃v1_1. (v = Conv "Inl" [v1_1]) ∧ a x_1 v1_1

Certificate theorem for ISL:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "ISL") ((SUM_TYPE a b --> BOOL) ISL)

Certificate theorem for ISR:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "ISR") ((SUM_TYPE a b --> BOOL) ISR)

Certificate theorem for OUTL:

|- DeclAssum std_prelude_decls env ∧ ISL x1 ⇒
   Eval env (Var "OUTL") ((Eq (SUM_TYPE a b) x1 --> a) OUTL)

Certificate theorem for OUTR:

|- DeclAssum std_prelude_decls env ∧ ISR x1 ⇒
   Eval env (Var "OUTR") ((Eq (SUM_TYPE a b) x1 --> b) OUTR)

Certificate theorem for ++:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "++")
     (((a --> c) --> (b --> d) --> SUM_TYPE a b --> SUM_TYPE c d) $++)

Certificate theorem for LENGTH_AUX:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "LENGTH_AUX")
     ((LIST_TYPE a --> NUM --> NUM) LENGTH_AUX)

Certificate theorem for LENGTH:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "LENGTH") ((LIST_TYPE a --> NUM) LENGTH)

Certificate theorem for MAP:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "MAP")
     (((a --> b) --> LIST_TYPE a --> LIST_TYPE b) MAP)

Certificate theorem for FILTER:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "FILTER")
     (((a --> BOOL) --> LIST_TYPE a --> LIST_TYPE a) FILTER)

Certificate theorem for FOLDR:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "FOLDR")
     (((a --> b --> b) --> b --> LIST_TYPE a --> b) FOLDR)

Certificate theorem for FOLDL:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "FOLDL")
     (((b --> a --> b) --> b --> LIST_TYPE a --> b) FOLDL)

Certificate theorem for SUM:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "SUM") ((LIST_TYPE NUM --> NUM) SUM)

Certificate theorem for UNZIP:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "UNZIP")
     ((LIST_TYPE (PAIR_TYPE a b) -->
       PAIR_TYPE (LIST_TYPE a) (LIST_TYPE b)) UNZIP)

Certificate theorem for FLAT:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "FLAT")
     ((LIST_TYPE (LIST_TYPE a) --> LIST_TYPE a) FLAT)

Certificate theorem for TAKE:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "TAKE") ((NUM --> LIST_TYPE a --> LIST_TYPE a) TAKE)

Certificate theorem for DROP:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "DROP") ((NUM --> LIST_TYPE a --> LIST_TYPE a) DROP)

Certificate theorem for SNOC:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "SNOC") ((a --> LIST_TYPE a --> LIST_TYPE a) SNOC)

Certificate theorem for EVERY:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "EVERY")
     (((a --> BOOL) --> LIST_TYPE a --> BOOL) EVERY)

Certificate theorem for EXISTS:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "EXISTS")
     (((a --> BOOL) --> LIST_TYPE a --> BOOL) EXISTS)

Certificate theorem for GENLIST:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "GENLIST")
     (((NUM --> a) --> NUM --> LIST_TYPE a) GENLIST)

Certificate theorem for PAD_RIGHT:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "PAD_RIGHT")
     ((a --> NUM --> LIST_TYPE a --> LIST_TYPE a) PAD_RIGHT)

Certificate theorem for PAD_LEFT:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "PAD_LEFT")
     ((a --> NUM --> LIST_TYPE a --> LIST_TYPE a) PAD_LEFT)

Certificate theorem for MEM:

|- DeclAssum std_prelude_decls env ∧ EqualityType a ⇒
   Eval env (Var "MEM") ((a --> LIST_TYPE a --> BOOL) MEM)

Certificate theorem for ALL_DISTINCT:

|- DeclAssum std_prelude_decls env ∧ EqualityType a ⇒
   Eval env (Var "ALL_DISTINCT") ((LIST_TYPE a --> BOOL) ALL_DISTINCT)

Certificate theorem for isPREFIX:

|- DeclAssum std_prelude_decls env ∧ EqualityType a ⇒
   Eval env (Var "isPREFIX")
     ((LIST_TYPE a --> LIST_TYPE a --> BOOL) isPREFIX)

Certificate theorem for FRONT:

|- DeclAssum std_prelude_decls env ∧ x1 ≠ [] ∧ EqualityType a ⇒
   Eval env (Var "FRONT") ((Eq (LIST_TYPE a) x1 --> LIST_TYPE a) FRONT)

Certificate theorem for ZIP:

|- DeclAssum std_prelude_decls env ∧
   (LENGTH (FST x1) = LENGTH (SND x1)) ⇒
   Eval env (Var "ZIP")
     ((Eq (PAIR_TYPE (LIST_TYPE a) (LIST_TYPE b)) x1 -->
       LIST_TYPE (PAIR_TYPE a b)) ZIP)

Certificate theorem for EL:

|- DeclAssum std_prelude_decls env ∧ v1 < LENGTH v2 ⇒
   Eval env (Var "EL") ((Eq NUM v1 --> Eq (LIST_TYPE a) v2 --> a) EL)

Certificate theorem for PART:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "PART")
     (((a --> BOOL) --> LIST_TYPE a --> LIST_TYPE a --> LIST_TYPE a -->
       PAIR_TYPE (LIST_TYPE a) (LIST_TYPE a)) PART)

Certificate theorem for PARTITION:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "PARTITION")
     (((a --> BOOL) --> LIST_TYPE a -->
       PAIR_TYPE (LIST_TYPE a) (LIST_TYPE a)) PARTITION)

Certificate theorem for QSORT:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "QSORT")
     (((a --> a --> BOOL) --> LIST_TYPE a --> LIST_TYPE a) QSORT)

Certificate theorem for EXP_AUX:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "EXP_AUX") ((NUM --> NUM --> NUM --> NUM) EXP_AUX)

Certificate theorem for EXP:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "EXP") ((NUM --> NUM --> NUM) $** )

Certificate theorem for MIN:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "MIN") ((NUM --> NUM --> NUM) MIN)

Certificate theorem for MAX:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "MAX") ((NUM --> NUM --> NUM) MAX)

Certificate theorem for EVEN:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "EVEN") ((NUM --> BOOL) EVEN)

Certificate theorem for ODD:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "ODD") ((NUM --> BOOL) ODD)

Certificate theorem for FUNPOW:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "FUNPOW") (((a --> a) --> NUM --> a --> a) FUNPOW)

Certificate theorem for MOD_2EXP:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "MOD_2EXP") ((NUM --> NUM --> NUM) MOD_2EXP)

Certificate theorem for DIV_2EXP:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "DIV_2EXP") ((NUM --> NUM --> NUM) DIV_2EXP)

Certificate theorem for PRE:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "PRE") ((NUM --> NUM) PRE)

Certificate theorem for ABS_DIFF:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "ABS_DIFF") ((NUM --> NUM --> NUM) ABS_DIFF)

Certificate theorem for DIV2:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "DIV2") ((NUM --> NUM) DIV2)

Certificate theorem for string_lt:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "string_lt")
     ((LIST_TYPE CHAR --> LIST_TYPE CHAR --> BOOL) $<)

Certificate theorem for string_le:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "string_le")
     ((LIST_TYPE CHAR --> LIST_TYPE CHAR --> BOOL) $<=)

Certificate theorem for string_gt:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "string_gt")
     ((LIST_TYPE CHAR --> LIST_TYPE CHAR --> BOOL) $>)

Certificate theorem for string_ge:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "string_ge")
     ((LIST_TYPE CHAR --> LIST_TYPE CHAR --> BOOL) $>=)

Certificate theorem for BITS:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "BITS") ((NUM --> NUM --> NUM --> NUM) BITS)

Certificate theorem for BIT:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "BIT") ((NUM --> NUM --> BOOL) BIT)

Certificate theorem for SBIT:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "SBIT") ((BOOL --> NUM --> NUM) SBIT)

Definition of refinement invariant:

|- (∀a x_6 x_5 x_4 x_3 v.
      PTREE_TYPE a (Branch x_6 x_5 x_4 x_3) v ⇔
      ∃v3_1 v3_2 v3_3 v3_4.
        (v = Conv "Branch" [v3_1; v3_2; v3_3; v3_4]) ∧ NUM x_6 v3_1 ∧
        NUM x_5 v3_2 ∧ PTREE_TYPE a x_4 v3_3 ∧ PTREE_TYPE a x_3 v3_4) ∧
   (∀a x_2 x_1 v.
      PTREE_TYPE a (Leaf x_2 x_1) v ⇔
      ∃v2_1 v2_2.
        (v = Conv "Leaf" [v2_1; v2_2]) ∧ NUM x_2 v2_1 ∧ a x_1 v2_2) ∧
   ∀a v. PTREE_TYPE a <{}> v ⇔ (v = Conv "Empty" [])

Certificate theorem for BRANCHING_BIT:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "BRANCHING_BIT") ((NUM --> NUM --> NUM) BRANCHING_BIT)

Certificate theorem for PEEK:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "PEEK") ((PTREE_TYPE a --> NUM --> OPTION_TYPE a) $')

Certificate theorem for MOD_2EXP_EQ:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "MOD_2EXP_EQ")
     ((NUM --> NUM --> NUM --> BOOL) MOD_2EXP_EQ)

Certificate theorem for JOIN:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "JOIN")
     ((PAIR_TYPE NUM
         (PAIR_TYPE (PTREE_TYPE a) (PAIR_TYPE NUM (PTREE_TYPE a))) -->
       PTREE_TYPE a) JOIN)

Certificate theorem for ADD:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "ADD")
     ((PTREE_TYPE a --> PAIR_TYPE NUM a --> PTREE_TYPE a) $|+)

Certificate theorem for BRANCH:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "BRANCH")
     ((PAIR_TYPE NUM
         (PAIR_TYPE NUM (PAIR_TYPE (PTREE_TYPE a) (PTREE_TYPE a))) -->
       PTREE_TYPE a) BRANCH)

Certificate theorem for REMOVE:

|- DeclAssum std_prelude_decls env ⇒
   Eval env (Var "REMOVE") ((PTREE_TYPE a --> NUM --> PTREE_TYPE a) $\\)

Definition of declaration list:

|- std_prelude_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 "FST")
      (Fun "v3"
         (Mat (Var "v3")
            [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v2")]));
    Dlet (Pvar "SND")
      (Fun "v3"
         (Mat (Var "v3")
            [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v1")]));
    Dlet (Pvar "CURRY")
      (Fun "v1"
         (Fun "v2"
            (Fun "v3"
               (App Opapp (Var "v1")
                  (Con "Pair" [Var "v2"; Var "v3"])))));
    Dlet (Pvar "UNCURRY")
      (Fun "v1"
         (Fun "v2"
            (App Opapp
               (App Opapp (Var "v1") (App Opapp (Var "FST") (Var "v2")))
               (App Opapp (Var "SND") (Var "v2")))));
    Dlet (Pvar "o")
      (Fun "v2"
         (Fun "v3"
            (Fun "v1"
               (App Opapp (Var "v2")
                  (App Opapp (Var "v3") (Var "v1"))))));
    Dlet (Pvar "I") (Fun "v1" (Var "v1"));
    Dlet (Pvar "C")
      (Fun "v3"
         (Fun "v2"
            (Fun "v1"
               (App Opapp (App Opapp (Var "v3") (Var "v1"))
                  (Var "v2")))));
    Dlet (Pvar "K") (Fun "v2" (Fun "v1" (Var "v2")));
    Dlet (Pvar "S")
      (Fun "v3"
         (Fun "v2"
            (Fun "v1"
               (App Opapp (App Opapp (Var "v3") (Var "v1"))
                  (App Opapp (Var "v2") (Var "v1"))))));
    Dlet (Pvar "UPDATE")
      (Fun "v3"
         (Fun "v4"
            (Fun "v2"
               (Fun "v1"
                  (If (App Equality (Var "v3") (Var "v1")) (Var "v4")
                     (App Opapp (Var "v2") (Var "v1")))))));
    Dlet (Pvar "W")
      (Fun "v2"
         (Fun "v1"
            (App Opapp (App Opapp (Var "v2") (Var "v1")) (Var "v1"))));
    Dtype [([],"one",[("One",[])])];
    Dtype [(["a"],"option",[("Some",[Tvar "a"]); ("None",[])])];
    Dlet (Pvar "THE")
      (Fun "x1"
         (Mat (Var "x1")
            [(Pcon "None" [],Raise Bind_error);
             (Pcon "Some" [Pvar "v1"],Var "v1")]));
    Dlet (Pvar "IS_NONE")
      (Fun "v2"
         (Mat (Var "v2")
            [(Pcon "None" [],Val (Lit (Bool T)));
             (Pcon "Some" [Pvar "v1"],Val (Lit (Bool F)))]));
    Dlet (Pvar "IS_SOME")
      (Fun "v2"
         (Mat (Var "v2")
            [(Pcon "None" [],Val (Lit (Bool F)));
             (Pcon "Some" [Pvar "v1"],Val (Lit (Bool T)))]));
    Dlet (Pvar "OPTION_MAP")
      (Fun "v2"
         (Fun "v3"
            (Mat (Var "v3")
               [(Pcon "None" [],Con "None" []);
                (Pcon "Some" [Pvar "v1"],
                 Con "Some" [App Opapp (Var "v2") (Var "v1")])])));
    Dlet (Pvar "OPTION_MAP2")
      (Fun "v1"
         (Fun "v2"
            (Fun "v3"
               (If
                  (Log And (App Opapp (Var "IS_SOME") (Var "v2"))
                     (App Opapp (Var "IS_SOME") (Var "v3")))
                  (Con "Some"
                     [App Opapp
                        (App Opapp (Var "v1")
                           (App Opapp (Var "THE") (Var "v2")))
                        (App Opapp (Var "THE") (Var "v3"))])
                  (Con "None" [])))));
    Dtype [(["a"; "b"],"sum",[("Inr",[Tvar "b"]); ("Inl",[Tvar "a"])])];
    Dlet (Pvar "ISL")
      (Fun "v3"
         (Mat (Var "v3")
            [(Pcon "Inl" [Pvar "v1"],Val (Lit (Bool T)));
             (Pcon "Inr" [Pvar "v2"],Val (Lit (Bool F)))]));
    Dlet (Pvar "ISR")
      (Fun "v3"
         (Mat (Var "v3")
            [(Pcon "Inl" [Pvar "v1"],Val (Lit (Bool F)));
             (Pcon "Inr" [Pvar "v2"],Val (Lit (Bool T)))]));
    Dlet (Pvar "OUTL")
      (Fun "x1"
         (Mat (Var "x1")
            [(Pcon "Inl" [Pvar "v1"],Var "v1");
             (Pcon "Inr" [Pvar "v2"],Raise Bind_error)]));
    Dlet (Pvar "OUTR")
      (Fun "x1"
         (Mat (Var "x1")
            [(Pcon "Inl" [Pvar "v1"],Raise Bind_error);
             (Pcon "Inr" [Pvar "v2"],Var "v2")]));
    Dlet (Pvar "++")
      (Fun "v3"
         (Fun "v4"
            (Fun "v5"
               (Mat (Var "v5")
                  [(Pcon "Inl" [Pvar "v1"],
                    Con "Inl" [App Opapp (Var "v3") (Var "v1")]);
                   (Pcon "Inr" [Pvar "v2"],
                    Con "Inr" [App Opapp (Var "v4") (Var "v2")])]))));
    Dletrec
      [("LENGTH_AUX","v3",
        Fun "v4"
          (Mat (Var "v3")
             [(Pcon "Nil" [],Var "v4");
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               App Opapp (App Opapp (Var "LENGTH_AUX") (Var "v1"))
                 (App (Opn Plus) (Var "v4")
                    (Val (Lit (IntLit 1)))))]))];
    Dlet (Pvar "LENGTH")
      (Fun "v1"
         (App Opapp (App Opapp (Var "LENGTH_AUX") (Var "v1"))
            (Val (Lit (IntLit 0)))));
    Dletrec
      [("MAP","v3",
        Fun "v4"
          (Mat (Var "v4")
             [(Pcon "Nil" [],Con "Nil" []);
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               Con "Cons"
                 [App Opapp (Var "v3") (Var "v2");
                  App Opapp (App Opapp (Var "MAP") (Var "v3"))
                    (Var "v1")])]))];
    Dletrec
      [("FILTER","v3",
        Fun "v4"
          (Mat (Var "v4")
             [(Pcon "Nil" [],Con "Nil" []);
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               If (App Opapp (Var "v3") (Var "v2"))
                 (Con "Cons"
                    [Var "v2";
                     App Opapp (App Opapp (Var "FILTER") (Var "v3"))
                       (Var "v1")])
                 (App Opapp (App Opapp (Var "FILTER") (Var "v3"))
                    (Var "v1")))]))];
    Dletrec
      [("FOLDR","v3",
        Fun "v4"
          (Fun "v5"
             (Mat (Var "v5")
                [(Pcon "Nil" [],Var "v4");
                 (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                  App Opapp (App Opapp (Var "v3") (Var "v2"))
                    (App Opapp
                       (App Opapp (App Opapp (Var "FOLDR") (Var "v3"))
                          (Var "v4")) (Var "v1")))])))];
    Dletrec
      [("FOLDL","v3",
        Fun "v4"
          (Fun "v5"
             (Mat (Var "v5")
                [(Pcon "Nil" [],Var "v4");
                 (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                  App Opapp
                    (App Opapp (App Opapp (Var "FOLDL") (Var "v3"))
                       (App Opapp (App Opapp (Var "v3") (Var "v4"))
                          (Var "v2"))) (Var "v1"))])))];
    Dletrec
      [("SUM","v3",
        Mat (Var "v3")
          [(Pcon "Nil" [],Val (Lit (IntLit 0)));
           (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
            App (Opn Plus) (Var "v2")
              (App Opapp (Var "SUM") (Var "v1")))])];
    Dletrec
      [("UNZIP","v3",
        Mat (Var "v3")
          [(Pcon "Nil" [],Con "Pair" [Con "Nil" []; Con "Nil" []]);
           (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
            Con "Pair"
              [Con "Cons"
                 [App Opapp (Var "FST") (Var "v2");
                  App Opapp (Var "FST")
                    (App Opapp (Var "UNZIP") (Var "v1"))];
               Con "Cons"
                 [App Opapp (Var "SND") (Var "v2");
                  App Opapp (Var "SND")
                    (App Opapp (Var "UNZIP") (Var "v1"))]])])];
    Dletrec
      [("FLAT","v3",
        Mat (Var "v3")
          [(Pcon "Nil" [],Con "Nil" []);
           (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
            App Opapp (App Opapp (Var "APPEND") (Var "v2"))
              (App Opapp (Var "FLAT") (Var "v1")))])];
    Dletrec
      [("TAKE","v3",
        Fun "v4"
          (Mat (Var "v4")
             [(Pcon "Nil" [],Con "Nil" []);
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0))))
                 (Con "Nil" [])
                 (Con "Cons"
                    [Var "v2";
                     App Opapp
                       (App Opapp (Var "TAKE")
                          (App (Opn Minus) (Var "v3")
                             (Val (Lit (IntLit 1))))) (Var "v1")]))]))];
    Dletrec
      [("DROP","v3",
        Fun "v4"
          (Mat (Var "v4")
             [(Pcon "Nil" [],Con "Nil" []);
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0))))
                 (Con "Cons" [Var "v2"; Var "v1"])
                 (App Opapp
                    (App Opapp (Var "DROP")
                       (App (Opn Minus) (Var "v3")
                          (Val (Lit (IntLit 1))))) (Var "v1")))]))];
    Dletrec
      [("SNOC","v3",
        Fun "v4"
          (Mat (Var "v4")
             [(Pcon "Nil" [],Con "Cons" [Var "v3"; Con "Nil" []]);
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               Con "Cons"
                 [Var "v2";
                  App Opapp (App Opapp (Var "SNOC") (Var "v3"))
                    (Var "v1")])]))];
    Dletrec
      [("EVERY","v3",
        Fun "v4"
          (Mat (Var "v4")
             [(Pcon "Nil" [],Val (Lit (Bool T)));
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               Log And (App Opapp (Var "v3") (Var "v2"))
                 (App Opapp (App Opapp (Var "EVERY") (Var "v3"))
                    (Var "v1")))]))];
    Dletrec
      [("EXISTS","v3",
        Fun "v4"
          (Mat (Var "v4")
             [(Pcon "Nil" [],Val (Lit (Bool F)));
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               Log Or (App Opapp (Var "v3") (Var "v2"))
                 (App Opapp (App Opapp (Var "EXISTS") (Var "v3"))
                    (Var "v1")))]))];
    Dletrec
      [("GENLIST","v1",
        Fun "v2"
          (If (App (Opb Leq) (Var "v2") (Val (Lit (IntLit 0))))
             (Con "Nil" [])
             (App Opapp
                (App Opapp (Var "SNOC")
                   (App Opapp (Var "v1")
                      (App (Opn Minus) (Var "v2")
                         (Val (Lit (IntLit 1))))))
                (App Opapp (App Opapp (Var "GENLIST") (Var "v1"))
                   (App (Opn Minus) (Var "v2")
                      (Val (Lit (IntLit 1))))))))];
    Dlet (Pvar "PAD_RIGHT")
      (Fun "v1"
         (Fun "v2"
            (Fun "v3"
               (App Opapp (App Opapp (Var "APPEND") (Var "v3"))
                  (App Opapp
                     (App Opapp (Var "GENLIST")
                        (App Opapp (Var "K") (Var "v1")))
                     (Let "k"
                        (App (Opn Minus) (Var "v2")
                           (App Opapp (Var "LENGTH") (Var "v3")))
                        (If
                           (App (Opb Lt) (Var "k")
                              (Val (Lit (IntLit 0))))
                           (Val (Lit (IntLit 0))) (Var "k"))))))));
    Dlet (Pvar "PAD_LEFT")
      (Fun "v1"
         (Fun "v2"
            (Fun "v3"
               (App Opapp
                  (App Opapp (Var "APPEND")
                     (App Opapp
                        (App Opapp (Var "GENLIST")
                           (App Opapp (Var "K") (Var "v1")))
                        (Let "k"
                           (App (Opn Minus) (Var "v2")
                              (App Opapp (Var "LENGTH") (Var "v3")))
                           (If
                              (App (Opb Lt) (Var "k")
                                 (Val (Lit (IntLit 0))))
                              (Val (Lit (IntLit 0))) (Var "k")))))
                  (Var "v3")))));
    Dletrec
      [("MEM","v3",
        Fun "v4"
          (Mat (Var "v4")
             [(Pcon "Nil" [],Val (Lit (Bool F)));
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               Log Or (App Equality (Var "v3") (Var "v2"))
                 (App Opapp (App Opapp (Var "MEM") (Var "v3"))
                    (Var "v1")))]))];
    Dletrec
      [("ALL_DISTINCT","v3",
        Mat (Var "v3")
          [(Pcon "Nil" [],Val (Lit (Bool T)));
           (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
            Log And
              (App Equality
                 (App Opapp (App Opapp (Var "MEM") (Var "v2"))
                    (Var "v1")) (Val (Lit (Bool F))))
              (App Opapp (Var "ALL_DISTINCT") (Var "v1")))])];
    Dletrec
      [("isPREFIX","v5",
        Fun "v6"
          (Mat (Var "v5")
             [(Pcon "Nil" [],Val (Lit (Bool T)));
              (Pcon "Cons" [Pvar "v4"; Pvar "v3"],
               Mat (Var "v6")
                 [(Pcon "Nil" [],Val (Lit (Bool F)));
                  (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                   Log And (App Equality (Var "v4") (Var "v2"))
                     (App Opapp (App Opapp (Var "isPREFIX") (Var "v3"))
                        (Var "v1")))])]))];
    Dletrec
      [("FRONT","x1",
        Mat (Var "x1")
          [(Pcon "Nil" [],Raise Bind_error);
           (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
            If (App Equality (Var "v1") (Con "Nil" [])) (Con "Nil" [])
              (Con "Cons"
                 [Var "v2"; App Opapp (Var "FRONT") (Var "v1")]))])];
    Dletrec
      [("ZIP","x1",
        Mat (Var "x1")
          [(Pcon "Pair" [Pvar "v8"; Pvar "v7"],
            Mat (Var "v8")
              [(Pcon "Nil" [],
                Mat (Var "v7")
                  [(Pcon "Nil" [],Con "Nil" []);
                   (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                    Raise Bind_error)]);
               (Pcon "Cons" [Pvar "v6"; Pvar "v5"],
                Mat (Var "v7")
                  [(Pcon "Nil" [],Raise Bind_error);
                   (Pcon "Cons" [Pvar "v4"; Pvar "v3"],
                    Con "Cons"
                      [Con "Pair" [Var "v6"; Var "v4"];
                       App Opapp (Var "ZIP")
                         (Con "Pair" [Var "v5"; Var "v3"])])])])])];
    Dletrec
      [("EL","v1",
        Fun "v2"
          (If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0))))
             (App Opapp (Var "HD") (Var "v2"))
             (App Opapp
                (App Opapp (Var "EL")
                   (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1)))))
                (App Opapp (Var "TL") (Var "v2")))))];
    Dletrec
      [("PART","v3",
        Fun "v4"
          (Fun "v5"
             (Fun "v6"
                (Mat (Var "v4")
                   [(Pcon "Nil" [],Con "Pair" [Var "v5"; Var "v6"]);
                    (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                     If (App Opapp (Var "v3") (Var "v2"))
                       (App Opapp
                          (App Opapp
                             (App Opapp
                                (App Opapp (Var "PART") (Var "v3"))
                                (Var "v1"))
                             (Con "Cons" [Var "v2"; Var "v5"]))
                          (Var "v6"))
                       (App Opapp
                          (App Opapp
                             (App Opapp
                                (App Opapp (Var "PART") (Var "v3"))
                                (Var "v1")) (Var "v5"))
                          (Con "Cons" [Var "v2"; Var "v6"])))]))))];
    Dlet (Pvar "PARTITION")
      (Fun "v1"
         (Fun "v2"
            (App Opapp
               (App Opapp
                  (App Opapp (App Opapp (Var "PART") (Var "v1"))
                     (Var "v2")) (Con "Nil" [])) (Con "Nil" []))));
    Dletrec
      [("QSORT","v7",
        Fun "v8"
          (Mat (Var "v8")
             [(Pcon "Nil" [],Con "Nil" []);
              (Pcon "Cons" [Pvar "v6"; Pvar "v5"],
               Let "v3"
                 (App Opapp
                    (App Opapp (Var "PARTITION")
                       (Fun "v4"
                          (App Opapp (App Opapp (Var "v7") (Var "v4"))
                             (Var "v6")))) (Var "v5"))
                 (Mat (Var "v3")
                    [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                      App Opapp
                        (App Opapp (Var "APPEND")
                           (App Opapp
                              (App Opapp (Var "APPEND")
                                 (App Opapp
                                    (App Opapp (Var "QSORT") (Var "v7"))
                                    (Var "v2")))
                              (Con "Cons" [Var "v6"; Con "Nil" []])))
                        (App Opapp (App Opapp (Var "QSORT") (Var "v7"))
                           (Var "v1")))]))]))];
    Dletrec
      [("EXP_AUX","v2",
        Fun "v3"
          (Fun "v1"
             (If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0))))
                (Var "v1")
                (App Opapp
                   (App Opapp (App Opapp (Var "EXP_AUX") (Var "v2"))
                      (App (Opn Minus) (Var "v3")
                         (Val (Lit (IntLit 1)))))
                   (App (Opn Times) (Var "v2") (Var "v1"))))))];
    Dlet (Pvar "EXP")
      (Fun "v1"
         (Fun "v2"
            (App Opapp
               (App Opapp (App Opapp (Var "EXP_AUX") (Var "v1"))
                  (Var "v2")) (Val (Lit (IntLit 1))))));
    Dlet (Pvar "MIN")
      (Fun "v1"
         (Fun "v2"
            (If (App (Opb Lt) (Var "v1") (Var "v2")) (Var "v1")
               (Var "v2"))));
    Dlet (Pvar "MAX")
      (Fun "v1"
         (Fun "v2"
            (If (App (Opb Lt) (Var "v1") (Var "v2")) (Var "v2")
               (Var "v1"))));
    Dlet (Pvar "EVEN")
      (Fun "v1"
         (App (Opb Leq)
            (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2))))
            (Val (Lit (IntLit 0)))));
    Dlet (Pvar "ODD")
      (Fun "v1"
         (App (Opb Lt) (Val (Lit (IntLit 0)))
            (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2))))));
    Dletrec
      [("FUNPOW","v1",
        Fun "v2"
          (Fun "v3"
             (If (App (Opb Leq) (Var "v2") (Val (Lit (IntLit 0))))
                (Var "v3")
                (App Opapp
                   (App Opapp (App Opapp (Var "FUNPOW") (Var "v1"))
                      (App (Opn Minus) (Var "v2")
                         (Val (Lit (IntLit 1)))))
                   (App Opapp (Var "v1") (Var "v3"))))))];
    Dlet (Pvar "MOD_2EXP")
      (Fun "v2"
         (Fun "v1"
            (App (Opn Modulo) (Var "v1")
               (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                  (Var "v2")))));
    Dlet (Pvar "DIV_2EXP")
      (Fun "v2"
         (Fun "v1"
            (App (Opn Divide) (Var "v1")
               (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                  (Var "v2")))));
    Dlet (Pvar "PRE")
      (Fun "v1"
         (Let "k" (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))
            (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
               (Val (Lit (IntLit 0))) (Var "k"))));
    Dlet (Pvar "ABS_DIFF")
      (Fun "v2"
         (Fun "v1"
            (If (App (Opb Lt) (Var "v2") (Var "v1"))
               (Let "k" (App (Opn Minus) (Var "v1") (Var "v2"))
                  (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                     (Val (Lit (IntLit 0))) (Var "k")))
               (Let "k" (App (Opn Minus) (Var "v2") (Var "v1"))
                  (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                     (Val (Lit (IntLit 0))) (Var "k"))))));
    Dlet (Pvar "DIV2")
      (Fun "v1" (App (Opn Divide) (Var "v1") (Val (Lit (IntLit 2)))));
    Dletrec
      [("string_lt","v7",
        Fun "v8"
          (Mat (Var "v7")
             [(Pcon "Nil" [],
               Mat (Var "v8")
                 [(Pcon "Nil" [],Val (Lit (Bool F)));
                  (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                   Val (Lit (Bool T)))]);
              (Pcon "Cons" [Pvar "v6"; Pvar "v5"],
               Mat (Var "v8")
                 [(Pcon "Nil" [],Val (Lit (Bool F)));
                  (Pcon "Cons" [Pvar "v4"; Pvar "v3"],
                   Log Or
                     (App Opapp
                        (Let "m" (Var "v6")
                           (Fun "n" (App (Opb Lt) (Var "m") (Var "n"))))
                        (Var "v4"))
                     (Log And (App Equality (Var "v6") (Var "v4"))
                        (App Opapp
                           (App Opapp (Var "string_lt") (Var "v5"))
                           (Var "v3"))))])]))];
    Dlet (Pvar "string_le")
      (Fun "v1"
         (Fun "v2"
            (Log Or (App Equality (Var "v1") (Var "v2"))
               (App Opapp (App Opapp (Var "string_lt") (Var "v1"))
                  (Var "v2")))));
    Dlet (Pvar "string_gt")
      (Fun "v1"
         (Fun "v2"
            (App Opapp (App Opapp (Var "string_lt") (Var "v2"))
               (Var "v1"))));
    Dlet (Pvar "string_ge")
      (Fun "v1"
         (Fun "v2"
            (App Opapp (App Opapp (Var "string_le") (Var "v2"))
               (Var "v1"))));
    Dlet (Pvar "BITS")
      (Fun "v1"
         (Fun "v2"
            (Fun "v3"
               (App (Opn Divide)
                  (App (Opn Modulo) (Var "v3")
                     (App Opapp
                        (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                        (App (Opn Plus) (Var "v1")
                           (Val (Lit (IntLit 1))))))
                  (App Opapp
                     (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                     (Var "v2"))))));
    Dlet (Pvar "BIT")
      (Fun "v1"
         (Fun "v2"
            (App Equality
               (App (Opn Modulo)
                  (App (Opn Divide) (Var "v2")
                     (App Opapp
                        (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                        (Var "v1"))) (Val (Lit (IntLit 2))))
               (Val (Lit (IntLit 1))))));
    Dlet (Pvar "SBIT")
      (Fun "v1"
         (Fun "v2"
            (If (Var "v1")
               (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                  (Var "v2")) (Val (Lit (IntLit 0))))));
    Dtype
      [(["a"],"ptree",
        [("Branch",
          [Tnum; Tnum; Tapp [Tvar "a"] "ptree";
           Tapp [Tvar "a"] "ptree"]); ("Leaf",[Tnum; Tvar "a"]);
         ("Empty",[])])];
    Dletrec
      [("BRANCHING_BIT","v1",
        Fun "v2"
          (If
             (Log Or
                (App Equality (App Opapp (Var "ODD") (Var "v1"))
                   (App Opapp (Var "EVEN") (Var "v2")))
                (App Equality (Var "v1") (Var "v2")))
             (Val (Lit (IntLit 0)))
             (App (Opn Plus)
                (App Opapp
                   (App Opapp (Var "BRANCHING_BIT")
                      (App Opapp (Var "DIV2") (Var "v1")))
                   (App Opapp (Var "DIV2") (Var "v2")))
                (Val (Lit (IntLit 1))))))];
    Dletrec
      [("PEEK","v7",
        Fun "v8"
          (Mat (Var "v7")
             [(Pcon "Empty" [],Con "None" []);
              (Pcon "Leaf" [Pvar "v2"; Pvar "v1"],
               If (App Equality (Var "v8") (Var "v2"))
                 (Con "Some" [Var "v1"]) (Con "None" []));
              (Pcon "Branch"
                 [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"],
               App Opapp
                 (App Opapp (Var "PEEK")
                    (If
                       (App Opapp (App Opapp (Var "BIT") (Var "v5"))
                          (Var "v8")) (Var "v4") (Var "v3")))
                 (Var "v8"))]))];
    Dlet (Pvar "MOD_2EXP_EQ")
      (Fun "v3"
         (Fun "v1"
            (Fun "v2"
               (App Equality
                  (App Opapp (App Opapp (Var "MOD_2EXP") (Var "v3"))
                     (Var "v1"))
                  (App Opapp (App Opapp (Var "MOD_2EXP") (Var "v3"))
                     (Var "v2"))))));
    Dlet (Pvar "JOIN")
      (Fun "v8"
         (Mat (Var "v8")
            [(Pcon "Pair" [Pvar "v7"; Pvar "v6"],
              Mat (Var "v6")
                [(Pcon "Pair" [Pvar "v5"; Pvar "v4"],
                  Mat (Var "v4")
                    [(Pcon "Pair" [Pvar "v3"; Pvar "v2"],
                      Let "v1"
                        (App Opapp
                           (App Opapp (Var "BRANCHING_BIT") (Var "v7"))
                           (Var "v3"))
                        (If
                           (App Opapp (App Opapp (Var "BIT") (Var "v1"))
                              (Var "v7"))
                           (Con "Branch"
                              [App Opapp
                                 (App Opapp (Var "MOD_2EXP") (Var "v1"))
                                 (Var "v7"); Var "v1"; Var "v5";
                               Var "v2"])
                           (Con "Branch"
                              [App Opapp
                                 (App Opapp (Var "MOD_2EXP") (Var "v1"))
                                 (Var "v7"); Var "v1"; Var "v2";
                               Var "v5"])))])])]));
    Dletrec
      [("ADD","v13",
        Fun "v14"
          (Mat (Var "v13")
             [(Pcon "Empty" [],
               Mat (Var "v14")
                 [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                   Con "Leaf" [Var "v2"; Var "v1"])]);
              (Pcon "Leaf" [Pvar "v6"; Pvar "v5"],
               Mat (Var "v14")
                 [(Pcon "Pair" [Pvar "v4"; Pvar "v3"],
                   If (App Equality (Var "v6") (Var "v4"))
                     (Con "Leaf" [Var "v4"; Var "v3"])
                     (App Opapp (Var "JOIN")
                        (Con "Pair"
                           [Var "v4";
                            Con "Pair"
                              [Con "Leaf" [Var "v4"; Var "v3"];
                               Con "Pair"
                                 [Var "v6";
                                  Con "Leaf"
                                    [Var "v6"; Var "v5"]]]])))]);
              (Pcon "Branch"
                 [Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"],
               Mat (Var "v14")
                 [(Pcon "Pair" [Pvar "v8"; Pvar "v7"],
                   If
                     (App Opapp
                        (App Opapp
                           (App Opapp (Var "MOD_2EXP_EQ") (Var "v11"))
                           (Var "v8")) (Var "v12"))
                     (If
                        (App Opapp (App Opapp (Var "BIT") (Var "v11"))
                           (Var "v8"))
                        (Con "Branch"
                           [Var "v12"; Var "v11";
                            App Opapp
                              (App Opapp (Var "ADD") (Var "v10"))
                              (Con "Pair" [Var "v8"; Var "v7"]);
                            Var "v9"])
                        (Con "Branch"
                           [Var "v12"; Var "v11"; Var "v10";
                            App Opapp (App Opapp (Var "ADD") (Var "v9"))
                              (Con "Pair" [Var "v8"; Var "v7"])]))
                     (App Opapp (Var "JOIN")
                        (Con "Pair"
                           [Var "v8";
                            Con "Pair"
                              [Con "Leaf" [Var "v8"; Var "v7"];
                               Con "Pair"
                                 [Var "v12";
                                  Con "Branch"
                                    [Var "v12"; Var "v11"; Var "v10";
                                     Var "v9"]]]])))])]))];
    Dlet (Pvar "BRANCH")
      (Fun "v31"
         (Mat (Var "v31")
            [(Pcon "Pair" [Pvar "v30"; Pvar "v29"],
              Mat (Var "v29")
                [(Pcon "Pair" [Pvar "v28"; Pvar "v27"],
                  Mat (Var "v27")
                    [(Pcon "Pair" [Pvar "v26"; Pvar "v25"],
                      Mat (Var "v26")
                        [(Pcon "Empty" [],
                          Mat (Var "v25")
                            [(Pcon "Empty" [],Con "Empty" []);
                             (Pcon "Leaf" [Pvar "v2"; Pvar "v1"],
                              Con "Leaf" [Var "v2"; Var "v1"]);
                             (Pcon "Branch"
                                [Pvar "v6"; Pvar "v5"; Pvar "v4";
                                 Pvar "v3"],
                              Con "Branch"
                                [Var "v6"; Var "v5"; Var "v4";
                                 Var "v3"])]);
                         (Pcon "Leaf" [Pvar "v14"; Pvar "v13"],
                          Mat (Var "v25")
                            [(Pcon "Empty" [],
                              Con "Leaf" [Var "v14"; Var "v13"]);
                             (Pcon "Leaf" [Pvar "v8"; Pvar "v7"],
                              Con "Branch"
                                [Var "v30"; Var "v28";
                                 Con "Leaf" [Var "v14"; Var "v13"];
                                 Con "Leaf" [Var "v8"; Var "v7"]]);
                             (Pcon "Branch"
                                [Pvar "v12"; Pvar "v11"; Pvar "v10";
                                 Pvar "v9"],
                              Con "Branch"
                                [Var "v30"; Var "v28";
                                 Con "Leaf" [Var "v14"; Var "v13"];
                                 Con "Branch"
                                   [Var "v12"; Var "v11"; Var "v10";
                                    Var "v9"]])]);
                         (Pcon "Branch"
                            [Pvar "v24"; Pvar "v23"; Pvar "v22";
                             Pvar "v21"],
                          Mat (Var "v25")
                            [(Pcon "Empty" [],
                              Con "Branch"
                                [Var "v24"; Var "v23"; Var "v22";
                                 Var "v21"]);
                             (Pcon "Leaf" [Pvar "v16"; Pvar "v15"],
                              Con "Branch"
                                [Var "v30"; Var "v28";
                                 Con "Branch"
                                   [Var "v24"; Var "v23"; Var "v22";
                                    Var "v21"];
                                 Con "Leaf" [Var "v16"; Var "v15"]]);
                             (Pcon "Branch"
                                [Pvar "v20"; Pvar "v19"; Pvar "v18";
                                 Pvar "v17"],
                              Con "Branch"
                                [Var "v30"; Var "v28";
                                 Con "Branch"
                                   [Var "v24"; Var "v23"; Var "v22";
                                    Var "v21"];
                                 Con "Branch"
                                   [Var "v20"; Var "v19"; Var "v18";
                                    Var "v17"]])])])])])]));
    Dletrec
      [("REMOVE","v7",
        Fun "v8"
          (Mat (Var "v7")
             [(Pcon "Empty" [],Con "Empty" []);
              (Pcon "Leaf" [Pvar "v2"; Pvar "v1"],
               If (App Equality (Var "v2") (Var "v8")) (Con "Empty" [])
                 (Con "Leaf" [Var "v2"; Var "v1"]));
              (Pcon "Branch"
                 [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"],
               If
                 (App Opapp
                    (App Opapp
                       (App Opapp (Var "MOD_2EXP_EQ") (Var "v5"))
                       (Var "v8")) (Var "v6"))
                 (If
                    (App Opapp (App Opapp (Var "BIT") (Var "v5"))
                       (Var "v8"))
                    (App Opapp (Var "BRANCH")
                       (Con "Pair"
                          [Var "v6";
                           Con "Pair"
                             [Var "v5";
                              Con "Pair"
                                [App Opapp
                                   (App Opapp (Var "REMOVE") (Var "v4"))
                                   (Var "v8"); Var "v3"]]]))
                    (App Opapp (Var "BRANCH")
                       (Con "Pair"
                          [Var "v6";
                           Con "Pair"
                             [Var "v5";
                              Con "Pair"
                                [Var "v4";
                                 App Opapp
                                   (App Opapp (Var "REMOVE") (Var "v3"))
                                   (Var "v8")]]])))
                 (Con "Branch"
                    [Var "v6"; Var "v5"; Var "v4"; Var "v3"]))]))]]