This translation extends 'std_prelude'.

Certificate theorem for word_add:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_add") ((WORD --> WORD --> WORD) $+)

Certificate theorem for word_mul:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_mul") ((WORD --> WORD --> WORD) $* )

Certificate theorem for word_add_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_add_1") ((WORD --> WORD --> WORD) $+)

Certificate theorem for word_mul_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_mul_1") ((WORD --> WORD --> WORD) $* )

Certificate theorem for word_add_2:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_add_2") ((WORD --> WORD --> WORD) $+)

Certificate theorem for word_mul_2:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_mul_2") ((WORD --> WORD --> WORD) $* )

Certificate theorem for BITWISE:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "BITWISE")
     ((NUM --> (BOOL --> BOOL --> BOOL) --> NUM --> NUM --> NUM)
        BITWISE)

Certificate theorem for word_xor:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_xor") ((WORD --> WORD --> WORD) $??)

Certificate theorem for word_xor_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_xor_1") ((WORD --> WORD --> WORD) $??)

Certificate theorem for word_xor_2:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_xor_2") ((WORD --> WORD --> WORD) $??)

Certificate theorem for word_or:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_or") ((WORD --> WORD --> WORD) $||)

Certificate theorem for word_or_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_or_1") ((WORD --> WORD --> WORD) $||)

Certificate theorem for word_and:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_and") ((WORD --> WORD --> WORD) $&&)

Certificate theorem for word_lsl:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_lsl") ((WORD --> NUM --> WORD) $<<)

Certificate theorem for word_lsl_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_lsl_1") ((WORD --> NUM --> WORD) $<<)

Certificate theorem for word_lsl_2:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_lsl_2") ((WORD --> NUM --> WORD) $<<)

Certificate theorem for word_lsr:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_lsr") ((WORD --> NUM --> WORD) $>>>)

Certificate theorem for word_lsr_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_lsr_1") ((WORD --> NUM --> WORD) $>>>)

Certificate theorem for word_lsr_2:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_lsr_2") ((WORD --> NUM --> WORD) $>>>)

Certificate theorem for word_msb:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_msb") ((WORD --> BOOL) word_msb)

Certificate theorem for word_msb_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_msb_1") ((WORD --> BOOL) word_msb)

Certificate theorem for word_msb_2:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_msb_2") ((WORD --> BOOL) word_msb)

Certificate theorem for word_lsb:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_lsb") ((WORD --> BOOL) word_lsb)

Certificate theorem for word_lsb_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_lsb_1") ((WORD --> BOOL) word_lsb)

Certificate theorem for word_lsb_2:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_lsb_2") ((WORD --> BOOL) word_lsb)

Certificate theorem for word_asr:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_asr") ((WORD --> NUM --> WORD) $>>)

Certificate theorem for word_asr_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_asr_1") ((WORD --> NUM --> WORD) $>>)

Certificate theorem for word_sub:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_sub") ((WORD --> WORD --> WORD) $-)

Certificate theorem for word_sub_1:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_sub_1") ((WORD --> WORD --> WORD) $-)

Certificate theorem for word_sub_2:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_sub_2") ((WORD --> WORD --> WORD) $-)

Certificate theorem for word_bits:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_bits") ((NUM --> NUM --> WORD --> WORD) $--)

Certificate theorem for word_ror:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_ror") ((WORD --> NUM --> WORD) $#>>)

Certificate theorem for word_rol:

|- DeclAssum word_prelude_decls env ⇒
   Eval env (Var "word_rol") ((WORD --> NUM --> WORD) $#<<)

Definition of declaration list:

|- word_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"]))]))];
    Dlet (Pvar "word_add")
      (Fun "v1"
         (Fun "v2"
            (Let "x" (App (Opn Plus) (Var "v1") (Var "v2"))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 4294967296)))))));
    Dlet (Pvar "word_mul")
      (Fun "v1"
         (Fun "v2"
            (Let "x" (App (Opn Times) (Var "v1") (Var "v2"))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 4294967296)))))));
    Dlet (Pvar "word_add_1")
      (Fun "v1"
         (Fun "v2"
            (Let "x" (App (Opn Plus) (Var "v1") (Var "v2"))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 65536)))))));
    Dlet (Pvar "word_mul_1")
      (Fun "v1"
         (Fun "v2"
            (Let "x" (App (Opn Times) (Var "v1") (Var "v2"))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 65536)))))));
    Dlet (Pvar "word_add_2")
      (Fun "v1"
         (Fun "v2"
            (Let "x" (App (Opn Plus) (Var "v1") (Var "v2"))
               (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))));
    Dlet (Pvar "word_mul_2")
      (Fun "v1"
         (Fun "v2"
            (Let "x" (App (Opn Times) (Var "v1") (Var "v2"))
               (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))));
    Dletrec
      [("BITWISE","v1",
        Fun "v2"
          (Fun "v3"
             (Fun "v4"
                (If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0))))
                   (Val (Lit (IntLit 0)))
                   (App (Opn Plus)
                      (App Opapp
                         (App Opapp
                            (App Opapp
                               (App Opapp (Var "BITWISE")
                                  (App (Opn Minus) (Var "v1")
                                     (Val (Lit (IntLit 1)))))
                               (Var "v2")) (Var "v3")) (Var "v4"))
                      (App Opapp
                         (App Opapp (Var "SBIT")
                            (App Opapp
                               (App Opapp (Var "v2")
                                  (App Opapp
                                     (App Opapp (Var "BIT")
                                        (App (Opn Minus) (Var "v1")
                                           (Val (Lit (IntLit 1)))))
                                     (Var "v3")))
                               (App Opapp
                                  (App Opapp (Var "BIT")
                                     (App (Opn Minus) (Var "v1")
                                        (Val (Lit (IntLit 1)))))
                                  (Var "v4"))))
                         (App (Opn Minus) (Var "v1")
                            (Val (Lit (IntLit 1))))))))))];
    Dlet (Pvar "word_xor")
      (Fun "v4"
         (Fun "v3"
            (Let "x"
               (App Opapp
                  (App Opapp
                     (App Opapp
                        (App Opapp (Var "BITWISE")
                           (Val (Lit (IntLit 32))))
                        (Fun "v2"
                           (Fun "v1"
                              (App Equality
                                 (App Equality (Var "v2") (Var "v1"))
                                 (Val (Lit (Bool F))))))) (Var "v4"))
                  (Var "v3"))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 4294967296)))))));
    Dlet (Pvar "word_xor_1")
      (Fun "v4"
         (Fun "v3"
            (Let "x"
               (App Opapp
                  (App Opapp
                     (App Opapp
                        (App Opapp (Var "BITWISE")
                           (Val (Lit (IntLit 8))))
                        (Fun "v2"
                           (Fun "v1"
                              (App Equality
                                 (App Equality (Var "v2") (Var "v1"))
                                 (Val (Lit (Bool F))))))) (Var "v4"))
                  (Var "v3"))
               (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))));
    Dlet (Pvar "word_xor_2")
      (Fun "v4"
         (Fun "v3"
            (Let "x"
               (App Opapp
                  (App Opapp
                     (App Opapp
                        (App Opapp (Var "BITWISE")
                           (Val (Lit (IntLit 16))))
                        (Fun "v2"
                           (Fun "v1"
                              (App Equality
                                 (App Equality (Var "v2") (Var "v1"))
                                 (Val (Lit (Bool F))))))) (Var "v4"))
                  (Var "v3"))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 65536)))))));
    Dlet (Pvar "word_or")
      (Fun "v4"
         (Fun "v3"
            (Let "x"
               (App Opapp
                  (App Opapp
                     (App Opapp
                        (App Opapp (Var "BITWISE")
                           (Val (Lit (IntLit 32))))
                        (Fun "v2"
                           (Fun "v1" (Log Or (Var "v2") (Var "v1")))))
                     (Var "v4")) (Var "v3"))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 4294967296)))))));
    Dlet (Pvar "word_or_1")
      (Fun "v4"
         (Fun "v3"
            (Let "x"
               (App Opapp
                  (App Opapp
                     (App Opapp
                        (App Opapp (Var "BITWISE")
                           (Val (Lit (IntLit 16))))
                        (Fun "v2"
                           (Fun "v1" (Log Or (Var "v2") (Var "v1")))))
                     (Var "v4")) (Var "v3"))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 65536)))))));
    Dlet (Pvar "word_and")
      (Fun "v4"
         (Fun "v3"
            (Let "x"
               (App Opapp
                  (App Opapp
                     (App Opapp
                        (App Opapp (Var "BITWISE")
                           (Val (Lit (IntLit 32))))
                        (Fun "v2"
                           (Fun "v1" (Log And (Var "v2") (Var "v1")))))
                     (Var "v4")) (Var "v3"))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 4294967296)))))));
    Dlet (Pvar "word_lsl")
      (Fun "v1"
         (Fun "v2"
            (App Opapp
               (App Opapp (Var "word_mul")
                  (Let "x"
                     (App Opapp
                        (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                        (Var "v2"))
                     (App (Opn Modulo) (Var "x")
                        (Val (Lit (IntLit 4294967296))))))
               (Var "v1"))));
    Dlet (Pvar "word_lsl_1")
      (Fun "v1"
         (Fun "v2"
            (App Opapp
               (App Opapp (Var "word_mul_1")
                  (Let "x"
                     (App Opapp
                        (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                        (Var "v2"))
                     (App (Opn Modulo) (Var "x")
                        (Val (Lit (IntLit 65536)))))) (Var "v1"))));
    Dlet (Pvar "word_lsl_2")
      (Fun "v1"
         (Fun "v2"
            (App Opapp
               (App Opapp (Var "word_mul_2")
                  (Let "x"
                     (App Opapp
                        (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                        (Var "v2"))
                     (App (Opn Modulo) (Var "x")
                        (Val (Lit (IntLit 256)))))) (Var "v1"))));
    Dlet (Pvar "word_lsr")
      (Fun "v2"
         (Fun "v1"
            (Let "x"
               (App (Opn Divide) (Var "v2")
                  (App Opapp
                     (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                     (Var "v1")))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 4294967296)))))));
    Dlet (Pvar "word_lsr_1")
      (Fun "v2"
         (Fun "v1"
            (Let "x"
               (App (Opn Divide) (Var "v2")
                  (App Opapp
                     (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                     (Var "v1")))
               (App (Opn Modulo) (Var "x")
                  (Val (Lit (IntLit 65536)))))));
    Dlet (Pvar "word_lsr_2")
      (Fun "v2"
         (Fun "v1"
            (Let "x"
               (App (Opn Divide) (Var "v2")
                  (App Opapp
                     (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                     (Var "v1")))
               (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))));
    Dlet (Pvar "word_msb")
      (Fun "v1"
         (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 31))))
            (Var "v1")));
    Dlet (Pvar "word_msb_1")
      (Fun "v1"
         (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 15))))
            (Var "v1")));
    Dlet (Pvar "word_msb_2")
      (Fun "v1"
         (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 7))))
            (Var "v1")));
    Dlet (Pvar "word_lsb")
      (Fun "v1"
         (App Equality
            (App (Opb Leq)
               (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2))))
               (Val (Lit (IntLit 0)))) (Val (Lit (Bool F)))));
    Dlet (Pvar "word_lsb_1")
      (Fun "v1"
         (App Equality
            (App (Opb Leq)
               (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2))))
               (Val (Lit (IntLit 0)))) (Val (Lit (Bool F)))));
    Dlet (Pvar "word_lsb_2")
      (Fun "v1"
         (App Equality
            (App (Opb Leq)
               (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2))))
               (Val (Lit (IntLit 0)))) (Val (Lit (Bool F)))));
    Dlet (Pvar "word_asr")
      (Fun "v2"
         (Fun "v1"
            (If (App Opapp (Var "word_msb") (Var "v2"))
               (App Opapp
                  (App Opapp (Var "word_or")
                     (Let "x"
                        (Let "k"
                           (App (Opn Minus)
                              (Val (Lit (IntLit 4294967296)))
                              (App Opapp
                                 (App Opapp (Var "EXP")
                                    (Val (Lit (IntLit 2))))
                                 (Let "k"
                                    (App (Opn Minus)
                                       (Val (Lit (IntLit 32)))
                                       (App Opapp
                                          (App Opapp (Var "MIN")
                                             (Var "v1"))
                                          (Val (Lit (IntLit 32)))))
                                    (If
                                       (App (Opb Lt) (Var "k")
                                          (Val (Lit (IntLit 0))))
                                       (Val (Lit (IntLit 0)))
                                       (Var "k")))))
                           (If
                              (App (Opb Lt) (Var "k")
                                 (Val (Lit (IntLit 0))))
                              (Val (Lit (IntLit 0))) (Var "k")))
                        (App (Opn Modulo) (Var "x")
                           (Val (Lit (IntLit 4294967296))))))
                  (App Opapp (App Opapp (Var "word_lsr") (Var "v2"))
                     (Var "v1")))
               (App Opapp (App Opapp (Var "word_lsr") (Var "v2"))
                  (Var "v1")))));
    Dlet (Pvar "word_asr_1")
      (Fun "v2"
         (Fun "v1"
            (If (App Opapp (Var "word_msb_1") (Var "v2"))
               (App Opapp
                  (App Opapp (Var "word_or_1")
                     (Let "x"
                        (Let "k"
                           (App (Opn Minus) (Val (Lit (IntLit 65536)))
                              (App Opapp
                                 (App Opapp (Var "EXP")
                                    (Val (Lit (IntLit 2))))
                                 (Let "k"
                                    (App (Opn Minus)
                                       (Val (Lit (IntLit 16)))
                                       (App Opapp
                                          (App Opapp (Var "MIN")
                                             (Var "v1"))
                                          (Val (Lit (IntLit 16)))))
                                    (If
                                       (App (Opb Lt) (Var "k")
                                          (Val (Lit (IntLit 0))))
                                       (Val (Lit (IntLit 0)))
                                       (Var "k")))))
                           (If
                              (App (Opb Lt) (Var "k")
                                 (Val (Lit (IntLit 0))))
                              (Val (Lit (IntLit 0))) (Var "k")))
                        (App (Opn Modulo) (Var "x")
                           (Val (Lit (IntLit 65536))))))
                  (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2"))
                     (Var "v1")))
               (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2"))
                  (Var "v1")))));
    Dlet (Pvar "word_sub")
      (Fun "v1"
         (Fun "v2"
            (App Opapp (App Opapp (Var "word_add") (Var "v1"))
               (Let "x"
                  (Let "k"
                     (App (Opn Minus) (Val (Lit (IntLit 4294967296)))
                        (Var "v2"))
                     (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                        (Val (Lit (IntLit 0))) (Var "k")))
                  (App (Opn Modulo) (Var "x")
                     (Val (Lit (IntLit 4294967296))))))));
    Dlet (Pvar "word_sub_1")
      (Fun "v1"
         (Fun "v2"
            (App Opapp (App Opapp (Var "word_add_1") (Var "v1"))
               (Let "x"
                  (Let "k"
                     (App (Opn Minus) (Val (Lit (IntLit 65536)))
                        (Var "v2"))
                     (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                        (Val (Lit (IntLit 0))) (Var "k")))
                  (App (Opn Modulo) (Var "x")
                     (Val (Lit (IntLit 65536))))))));
    Dlet (Pvar "word_sub_2")
      (Fun "v1"
         (Fun "v2"
            (App Opapp (App Opapp (Var "word_add_2") (Var "v1"))
               (Let "x"
                  (Let "k"
                     (App (Opn Minus) (Val (Lit (IntLit 256)))
                        (Var "v2"))
                     (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                        (Val (Lit (IntLit 0))) (Var "k")))
                  (App (Opn Modulo) (Var "x")
                     (Val (Lit (IntLit 256))))))));
    Dlet (Pvar "word_bits")
      (Fun "v1"
         (Fun "v2"
            (Fun "v3"
               (Let "x"
                  (App Opapp
                     (App Opapp
                        (App Opapp (Var "BITS")
                           (App Opapp (App Opapp (Var "MIN") (Var "v1"))
                              (Val (Lit (IntLit 31))))) (Var "v2"))
                     (Var "v3"))
                  (App (Opn Modulo) (Var "x")
                     (Val (Lit (IntLit 4294967296))))))));
    Dlet (Pvar "word_ror")
      (Fun "v3"
         (Fun "v2"
            (Let "v1"
               (App (Opn Modulo) (Var "v2") (Val (Lit (IntLit 32))))
               (App Opapp
                  (App Opapp (Var "word_or")
                     (App Opapp
                        (App Opapp
                           (App Opapp (Var "word_bits")
                              (Val (Lit (IntLit 31)))) (Var "v1"))
                        (Var "v3")))
                  (App Opapp
                     (App Opapp (Var "word_lsl")
                        (App Opapp
                           (App Opapp
                              (App Opapp (Var "word_bits")
                                 (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"))))
                              (Val (Lit (IntLit 0)))) (Var "v3")))
                     (Let "k"
                        (App (Opn Minus) (Val (Lit (IntLit 32)))
                           (Var "v1"))
                        (If
                           (App (Opb Lt) (Var "k")
                              (Val (Lit (IntLit 0))))
                           (Val (Lit (IntLit 0))) (Var "k"))))))));
    Dlet (Pvar "word_rol")
      (Fun "v2"
         (Fun "v1"
            (App Opapp (App Opapp (Var "word_ror") (Var "v2"))
               (Let "k"
                  (App (Opn Minus) (Val (Lit (IntLit 32)))
                     (App (Opn Modulo) (Var "v1")
                        (Val (Lit (IntLit 32)))))
                  (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                     (Val (Lit (IntLit 0))) (Var "k"))))))]