(* This code extends 'word_prelude'. *)

val ShiftXor = 
  (fn v7 => 
    (case v7 of 
        (Pair (v6, v5)) => 
          (case v5 of 
              (Pair (v4, v3)) => 
                (case v3 of 
                    (Pair (v2, v1)) => ((word_xor ((word_add ((word_lsl v6) 4)) v2)) ((word_xor ((word_add v6) v4)) ((word_add ((word_asr v6) 5)) v1))))))) ;

val Round = 
  (fn v15 => 
    (case v15 of 
        (Pair (v14, v13)) => 
          (case v14 of 
              (Pair (v12, v11)) => 
                (case v13 of 
                    (Pair (v10, v9)) => 
                      (case v10 of 
                          (Pair (v8, v7)) => 
                            (case v7 of 
                              (Pair (v6, v5)) => 
                              (case v5 of 
                              (Pair (v4, v3)) => 
                              let val v2 = ((word_add v9) 
                              let val x = 2654435769 
                              in (x mod 4294967296) 
                              end ) 
                              in 
                              let val v1 = ((word_add v12) (ShiftXor (Pair (v11, (Pair (v2, (Pair (v8, v6)))))))) 
                              in (Pair ((Pair (v1, ((word_add v11) (ShiftXor (Pair (v1, (Pair (v2, (Pair (v4, v3)))))))))), (Pair ((Pair (v8, (Pair (v6, (Pair (v4, v3)))))), v2)))) 
                              end 
                              end ))))))) ;

val InvRound = 
  (fn v13 => 
    (case v13 of 
        (Pair (v12, v11)) => 
          (case v12 of 
              (Pair (v10, v9)) => 
                (case v11 of 
                    (Pair (v8, v7)) => 
                      (case v8 of 
                          (Pair (v6, v5)) => 
                            (case v5 of 
                              (Pair (v4, v3)) => 
                              (case v3 of 
                              (Pair (v2, v1)) => (Pair ((Pair (((word_sub v10) (ShiftXor (Pair (((word_sub v9) (ShiftXor (Pair (v10, (Pair (v7, (Pair (v2, v1)))))))), (Pair (v7, (Pair (v6, v4)))))))), ((word_sub v9) (ShiftXor (Pair (v10, (Pair (v7, (Pair (v2, v1)))))))))), (Pair ((Pair (v6, (Pair (v4, (Pair (v2, v1)))))), ((word_sub v7) 
                              let val x = 2654435769 
                              in (x mod 4294967296) 
                              end )))))))))))) ;

fun Rounds v3 = 
  (case v3 of 
      (Pair (v2, v1)) => 
        (if (v2 = 
        let val x = 0 
        in (x mod 4294967296) 
        end ) 
        then v1 
        else (Rounds (Pair (((word_sub v2) 
          let val x = 1 
          in (x mod 4294967296) 
          end ), (Round v1)))))) ;

fun InvRounds v3 = 
  (case v3 of 
      (Pair (v2, v1)) => 
        (if (v2 = 
        let val x = 0 
        in (x mod 4294967296) 
        end ) 
        then v1 
        else (InvRounds (Pair (((word_sub v2) 
          let val x = 1 
          in (x mod 4294967296) 
          end ), (InvRound v1)))))) ;

val teaEncrypt = 
  (fn v8 => 
    (case v8 of 
        (Pair (v7, v6)) => 
          let val v5 = (Rounds (Pair (
          let val x = 32 
          in (x mod 4294967296) 
          end , (Pair (v6, (Pair (v7, 
          let val x = 0 
          in (x mod 4294967296) 
          end ))))))) 
          in 
            (case v5 of 
                (Pair (v4, v3)) => 
                  (case v3 of 
                      (Pair (v2, v1)) => v4)) 
          end )) ;

val teaDecrypt = 
  (fn v8 => 
    (case v8 of 
        (Pair (v7, v6)) => 
          let val v5 = (InvRounds (Pair (
          let val x = 32 
          in (x mod 4294967296) 
          end , (Pair (v6, (Pair (v7, ((word_lsl 
          let val x = 2654435769 
          in (x mod 4294967296) 
          end ) 5)))))))) 
          in 
            (case v5 of 
                (Pair (v4, v3)) => 
                  (case v3 of 
                      (Pair (v2, v1)) => v4)) 
          end )) ;