(* This code extends 'mini_prelude'. *)

val FST = 
  (fn v3 => 
    (case v3 of 
        (Pair (v2, v1)) => v2)) ;

val SND = 
  (fn v3 => 
    (case v3 of 
        (Pair (v2, v1)) => v1)) ;

val CURRY = 
  (fn v1 => 
    (fn v2 => 
      (fn v3 => (v1 (Pair (v2, v3)))))) ;

val UNCURRY = 
  (fn v1 => 
    (fn v2 => ((v1 (FST v2)) (SND v2)))) ;

val op o = 
  (fn v2 => 
    (fn v3 => 
      (fn v1 => (v2 (v3 v1))))) ;

val I = 
  (fn v1 => v1) ;

val C = 
  (fn v3 => 
    (fn v2 => 
      (fn v1 => ((v3 v1) v2)))) ;

val K = 
  (fn v2 => 
    (fn v1 => v2)) ;

val S = 
  (fn v3 => 
    (fn v2 => 
      (fn v1 => ((v3 v1) (v2 v1))))) ;

val UPDATE = 
  (fn v3 => 
    (fn v4 => 
      (fn v2 => 
        (fn v1 => 
          (if (v3 = v1) 
          then v4 
          else (v2 v1)))))) ;

val W = 
  (fn v2 => 
    (fn v1 => ((v2 v1) v1))) ;

datatype one = 
    One ;

datatype ('a) option = 
    Some of 'a 
  | None ;

val THE = 
  (fn x1 => 
    (case x1 of 
        None => (raise Bind) 
      | (Some (v1)) => v1)) ;

val IS_NONE = 
  (fn v2 => 
    (case v2 of 
        None => true 
      | (Some (v1)) => false)) ;

val IS_SOME = 
  (fn v2 => 
    (case v2 of 
        None => false 
      | (Some (v1)) => true)) ;

val OPTION_MAP = 
  (fn v2 => 
    (fn v3 => 
      (case v3 of 
          None => None 
        | (Some (v1)) => (Some ((v2 v1)))))) ;

val OPTION_MAP2 = 
  (fn v1 => 
    (fn v2 => 
      (fn v3 => 
        (if ((IS_SOME v2) andalso (IS_SOME v3)) 
        then (Some (((v1 (THE v2)) (THE v3)))) 
        else None)))) ;

datatype ('a, 'b) sum = 
    Inr of 'b 
  | Inl of 'a ;

val ISL = 
  (fn v3 => 
    (case v3 of 
        (Inl (v1)) => true 
      | (Inr (v2)) => false)) ;

val ISR = 
  (fn v3 => 
    (case v3 of 
        (Inl (v1)) => false 
      | (Inr (v2)) => true)) ;

val OUTL = 
  (fn x1 => 
    (case x1 of 
        (Inl (v1)) => v1 
      | (Inr (v2)) => (raise Bind))) ;

val OUTR = 
  (fn x1 => 
    (case x1 of 
        (Inl (v1)) => (raise Bind) 
      | (Inr (v2)) => v2)) ;

val ++ = 
  (fn v3 => 
    (fn v4 => 
      (fn v5 => 
        (case v5 of 
            (Inl (v1)) => (Inl ((v3 v1))) 
          | (Inr (v2)) => (Inr ((v4 v2))))))) ;

fun LENGTH_AUX v3 = 
  (fn v4 => 
    (case v3 of 
        Nil => v4 
      | (Cons (v2, v1)) => ((LENGTH_AUX v1) (v4 + 1)))) ;

val LENGTH = 
  (fn v1 => ((LENGTH_AUX v1) 0)) ;

fun MAP v3 = 
  (fn v4 => 
    (case v4 of 
        Nil => Nil 
      | (Cons (v2, v1)) => (Cons ((v3 v2), ((MAP v3) v1))))) ;

fun FILTER v3 = 
  (fn v4 => 
    (case v4 of 
        Nil => Nil 
      | (Cons (v2, v1)) => 
          (if (v3 v2) 
          then (Cons (v2, ((FILTER v3) v1))) 
          else ((FILTER v3) v1)))) ;

fun FOLDR v3 = 
  (fn v4 => 
    (fn v5 => 
      (case v5 of 
          Nil => v4 
        | (Cons (v2, v1)) => ((v3 v2) (((FOLDR v3) v4) v1))))) ;

fun FOLDL v3 = 
  (fn v4 => 
    (fn v5 => 
      (case v5 of 
          Nil => v4 
        | (Cons (v2, v1)) => (((FOLDL v3) ((v3 v4) v2)) v1)))) ;

fun SUM v3 = 
  (case v3 of 
      Nil => 0 
    | (Cons (v2, v1)) => (v2 + (SUM v1))) ;

fun UNZIP v3 = 
  (case v3 of 
      Nil => (Pair (Nil, Nil)) 
    | (Cons (v2, v1)) => (Pair ((Cons ((FST v2), (FST (UNZIP v1)))), (Cons ((SND v2), (SND (UNZIP v1))))))) ;

fun FLAT v3 = 
  (case v3 of 
      Nil => Nil 
    | (Cons (v2, v1)) => ((APPEND v2) (FLAT v1))) ;

fun TAKE v3 = 
  (fn v4 => 
    (case v4 of 
        Nil => Nil 
      | (Cons (v2, v1)) => 
          (if (v3 <= 0) 
          then Nil 
          else (Cons (v2, ((TAKE (v3 - 1)) v1)))))) ;

fun DROP v3 = 
  (fn v4 => 
    (case v4 of 
        Nil => Nil 
      | (Cons (v2, v1)) => 
          (if (v3 <= 0) 
          then (Cons (v2, v1)) 
          else ((DROP (v3 - 1)) v1)))) ;

fun SNOC v3 = 
  (fn v4 => 
    (case v4 of 
        Nil => (Cons (v3, Nil)) 
      | (Cons (v2, v1)) => (Cons (v2, ((SNOC v3) v1))))) ;

fun EVERY v3 = 
  (fn v4 => 
    (case v4 of 
        Nil => true 
      | (Cons (v2, v1)) => ((v3 v2) andalso ((EVERY v3) v1)))) ;

fun EXISTS v3 = 
  (fn v4 => 
    (case v4 of 
        Nil => false 
      | (Cons (v2, v1)) => ((v3 v2) orelse ((EXISTS v3) v1)))) ;

fun GENLIST v1 = 
  (fn v2 => 
    (if (v2 <= 0) 
    then Nil 
    else ((SNOC (v1 (v2 - 1))) ((GENLIST v1) (v2 - 1))))) ;

val PAD_RIGHT = 
  (fn v1 => 
    (fn v2 => 
      (fn v3 => ((APPEND v3) ((GENLIST (K v1)) 
        let val k = (v2 - (LENGTH v3)) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end ))))) ;

val PAD_LEFT = 
  (fn v1 => 
    (fn v2 => 
      (fn v3 => ((APPEND ((GENLIST (K v1)) 
        let val k = (v2 - (LENGTH v3)) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end )) v3)))) ;

fun MEM v3 = 
  (fn v4 => 
    (case v4 of 
        Nil => false 
      | (Cons (v2, v1)) => ((v3 = v2) orelse ((MEM v3) v1)))) ;

fun ALL_DISTINCT v3 = 
  (case v3 of 
      Nil => true 
    | (Cons (v2, v1)) => ((((MEM v2) v1) = false) andalso (ALL_DISTINCT v1))) ;

fun isPREFIX v5 = 
  (fn v6 => 
    (case v5 of 
        Nil => true 
      | (Cons (v4, v3)) => 
          (case v6 of 
              Nil => false 
            | (Cons (v2, v1)) => ((v4 = v2) andalso ((isPREFIX v3) v1))))) ;

fun FRONT x1 = 
  (case x1 of 
      Nil => (raise Bind) 
    | (Cons (v2, v1)) => 
        (if (v1 = Nil) 
        then Nil 
        else (Cons (v2, (FRONT v1))))) ;

fun ZIP x1 = 
  (case x1 of 
      (Pair (v8, v7)) => 
        (case v8 of 
            Nil => 
              (case v7 of 
                  Nil => Nil 
                | (Cons (v2, v1)) => (raise Bind)) 
          | (Cons (v6, v5)) => 
              (case v7 of 
                  Nil => (raise Bind) 
                | (Cons (v4, v3)) => (Cons ((Pair (v6, v4)), (ZIP (Pair (v5, v3)))))))) ;

fun EL v1 = 
  (fn v2 => 
    (if (v1 <= 0) 
    then (HD v2) 
    else ((EL (v1 - 1)) (TL v2)))) ;

fun PART v3 = 
  (fn v4 => 
    (fn v5 => 
      (fn v6 => 
        (case v4 of 
            Nil => (Pair (v5, v6)) 
          | (Cons (v2, v1)) => 
              (if (v3 v2) 
              then ((((PART v3) v1) (Cons (v2, v5))) v6) 
              else ((((PART v3) v1) v5) (Cons (v2, v6)))))))) ;

val PARTITION = 
  (fn v1 => 
    (fn v2 => ((((PART v1) v2) Nil) Nil))) ;

fun QSORT v7 = 
  (fn v8 => 
    (case v8 of 
        Nil => Nil 
      | (Cons (v6, v5)) => 
          let val v3 = ((PARTITION 
          (fn v4 => ((v7 v4) v6))) v5) 
          in 
            (case v3 of 
                (Pair (v2, v1)) => ((APPEND ((APPEND ((QSORT v7) v2)) (Cons (v6, Nil)))) ((QSORT v7) v1))) 
          end )) ;

fun EXP_AUX v2 = 
  (fn v3 => 
    (fn v1 => 
      (if (v3 <= 0) 
      then v1 
      else (((EXP_AUX v2) (v3 - 1)) (v2 * v1))))) ;

val EXP = 
  (fn v1 => 
    (fn v2 => (((EXP_AUX v1) v2) 1))) ;

val MIN = 
  (fn v1 => 
    (fn v2 => 
      (if (v1 < v2) 
      then v1 
      else v2))) ;

val MAX = 
  (fn v1 => 
    (fn v2 => 
      (if (v1 < v2) 
      then v2 
      else v1))) ;

val EVEN = 
  (fn v1 => ((v1 mod 2) <= 0)) ;

val ODD = 
  (fn v1 => (0 < (v1 mod 2))) ;

fun FUNPOW v1 = 
  (fn v2 => 
    (fn v3 => 
      (if (v2 <= 0) 
      then v3 
      else (((FUNPOW v1) (v2 - 1)) (v1 v3))))) ;

val MOD_2EXP = 
  (fn v2 => 
    (fn v1 => (v1 mod ((EXP 2) v2)))) ;

val DIV_2EXP = 
  (fn v2 => 
    (fn v1 => (v1 div ((EXP 2) v2)))) ;

val PRE = 
  (fn v1 => 
    let val k = (v1 - 1) 
    in 
      (if (k < 0) 
      then 0 
      else k) 
    end ) ;

val ABS_DIFF = 
  (fn v2 => 
    (fn v1 => 
      (if (v2 < v1) 
      then 
        let val k = (v1 - v2) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end 
      else 
        let val k = (v2 - v1) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end ))) ;

val DIV2 = 
  (fn v1 => (v1 div 2)) ;

fun string_lt v7 = 
  (fn v8 => 
    (case v7 of 
        Nil => 
          (case v8 of 
              Nil => false 
            | (Cons (v2, v1)) => true) 
      | (Cons (v6, v5)) => 
          (case v8 of 
              Nil => false 
            | (Cons (v4, v3)) => ((
                let val m = v6 
                in 
                  (fn n => (m < n)) 
                end v4) orelse ((v6 = v4) andalso ((string_lt v5) v3)))))) ;

val string_le = 
  (fn v1 => 
    (fn v2 => ((v1 = v2) orelse ((string_lt v1) v2)))) ;

val string_gt = 
  (fn v1 => 
    (fn v2 => ((string_lt v2) v1))) ;

val string_ge = 
  (fn v1 => 
    (fn v2 => ((string_le v2) v1))) ;

val BITS = 
  (fn v1 => 
    (fn v2 => 
      (fn v3 => ((v3 mod ((EXP 2) (v1 + 1))) div ((EXP 2) v2))))) ;

val BIT = 
  (fn v1 => 
    (fn v2 => (((v2 div ((EXP 2) v1)) mod 2) = 1))) ;

val SBIT = 
  (fn v1 => 
    (fn v2 => 
      (if v1 
      then ((EXP 2) v2) 
      else 0))) ;

datatype ('a) ptree = 
    Branch of int * int * ('a) ptree * ('a) ptree 
  | Leaf of int * 'a 
  | Empty ;

fun BRANCHING_BIT v1 = 
  (fn v2 => 
    (if (((ODD v1) = (EVEN v2)) orelse (v1 = v2)) 
    then 0 
    else (((BRANCHING_BIT (DIV2 v1)) (DIV2 v2)) + 1))) ;

fun PEEK v7 = 
  (fn v8 => 
    (case v7 of 
        Empty => None 
      | (Leaf (v2, v1)) => 
          (if (v8 = v2) 
          then (Some (v1)) 
          else None) 
      | (Branch (v6, v5, v4, v3)) => ((PEEK 
          (if ((BIT v5) v8) 
          then v4 
          else v3)) v8))) ;

val MOD_2EXP_EQ = 
  (fn v3 => 
    (fn v1 => 
      (fn v2 => (((MOD_2EXP v3) v1) = ((MOD_2EXP v3) v2))))) ;

val JOIN = 
  (fn v8 => 
    (case v8 of 
        (Pair (v7, v6)) => 
          (case v6 of 
              (Pair (v5, v4)) => 
                (case v4 of 
                    (Pair (v3, v2)) => 
                      let val v1 = ((BRANCHING_BIT v7) v3) 
                      in 
                        (if ((BIT v1) v7) 
                        then (Branch (((MOD_2EXP v1) v7), v1, v5, v2)) 
                        else (Branch (((MOD_2EXP v1) v7), v1, v2, v5))) 
                      end )))) ;

fun ADD v13 = 
  (fn v14 => 
    (case v13 of 
        Empty => 
          (case v14 of 
              (Pair (v2, v1)) => (Leaf (v2, v1))) 
      | (Leaf (v6, v5)) => 
          (case v14 of 
              (Pair (v4, v3)) => 
                (if (v6 = v4) 
                then (Leaf (v4, v3)) 
                else (JOIN (Pair (v4, (Pair ((Leaf (v4, v3)), (Pair (v6, (Leaf (v6, v5))))))))))) 
      | (Branch (v12, v11, v10, v9)) => 
          (case v14 of 
              (Pair (v8, v7)) => 
                (if (((MOD_2EXP_EQ v11) v8) v12) 
                then 
                  (if ((BIT v11) v8) 
                  then (Branch (v12, v11, ((ADD v10) (Pair (v8, v7))), v9)) 
                  else (Branch (v12, v11, v10, ((ADD v9) (Pair (v8, v7)))))) 
                else (JOIN (Pair (v8, (Pair ((Leaf (v8, v7)), (Pair (v12, (Branch (v12, v11, v10, v9))))))))))))) ;

val BRANCH = 
  (fn v31 => 
    (case v31 of 
        (Pair (v30, v29)) => 
          (case v29 of 
              (Pair (v28, v27)) => 
                (case v27 of 
                    (Pair (v26, v25)) => 
                      (case v26 of 
                          Empty => 
                            (case v25 of 
                              Empty => Empty 
                              | (Leaf (v2, v1)) => (Leaf (v2, v1)) 
                              | (Branch (v6, v5, v4, v3)) => (Branch (v6, v5, v4, v3))) 
                        | (Leaf (v14, v13)) => 
                            (case v25 of 
                              Empty => (Leaf (v14, v13)) 
                              | (Leaf (v8, v7)) => (Branch (v30, v28, (Leaf (v14, v13)), (Leaf (v8, v7)))) 
                              | (Branch (v12, v11, v10, v9)) => (Branch (v30, v28, (Leaf (v14, v13)), (Branch (v12, v11, v10, v9))))) 
                        | (Branch (v24, v23, v22, v21)) => 
                            (case v25 of 
                              Empty => (Branch (v24, v23, v22, v21)) 
                              | (Leaf (v16, v15)) => (Branch (v30, v28, (Branch (v24, v23, v22, v21)), (Leaf (v16, v15)))) 
                              | (Branch (v20, v19, v18, v17)) => (Branch (v30, v28, (Branch (v24, v23, v22, v21)), (Branch (v20, v19, v18, v17)))))))))) ;

fun REMOVE v7 = 
  (fn v8 => 
    (case v7 of 
        Empty => Empty 
      | (Leaf (v2, v1)) => 
          (if (v2 = v8) 
          then Empty 
          else (Leaf (v2, v1))) 
      | (Branch (v6, v5, v4, v3)) => 
          (if (((MOD_2EXP_EQ v5) v8) v6) 
          then 
            (if ((BIT v5) v8) 
            then (BRANCH (Pair (v6, (Pair (v5, (Pair (((REMOVE v4) v8), v3))))))) 
            else (BRANCH (Pair (v6, (Pair (v5, (Pair (v4, ((REMOVE v3) v8))))))))) 
          else (Branch (v6, v5, v4, v3))))) ;