Finding nth term in a sequence

I found this to be an interesting task from a regional math contest.

Given:
$a_0 = 6$
$a_k = 1/2 a_{k-1}$ , $a_{k-1}$ even
$a_k = 3 a_{k-1} + 1$ , $a_{k-1}$ odd
Find $a_{2018}$ .

Starting with a_6, the sequence repeats with $(4, 2, 1)$ for numbers of the form $(3k, 3k + 1, 3k + 2)$ (see proof below). 2018 is of the form 3k + 2, thus the answer is 1.

Checking it with Idris:

testseq : Integer -> Integer
testseq 0     = 6
testseq k     = let previous = testseq (k - 1) in
                     if (mod previous 2 == 0) then
                     (div previous 2) else
                     3 * previous + 1

infiniteSeq : Stream Nat
infiniteSeq = map (\x => fromIntegerNat (testseq x)) [0..]

-- *test> take 20 infiniteSeq
-- [6, 3, 10, 5, 16, 8, 4, 2, 1, 4, 2, 1, 4, 2, 1, 4, 2, 1, 4, 2] : List Integer

getItemFromSeq : Nat -> Nat
getItemFromSeq n = index n infiniteSeq

-- *test> getItemFromSeq 2018
-- 1 : Integer

Proof for repeating sequence. Given:
$a_0 = 4$
$a_k = 1/2 a_{k-1}$ , $a_{k-1}$ even
$a_k = 3 a_{k-1} + 1$ , $a_{k-1}$ odd

Prove that the sequence repeats $(4, 2, 1)$ , i.e. for any triplet $(a_k, a_{k+1}, a_{k+2})$ we have that it equals to some of $\{ (4, 2, 1), (1, 4, 2), (2, 1, 4) \}$ .

Base case: $(a_0, a_1, a_2) = (4, 2, 1)$

Inductive step:
Case 1: Assume that $(a_k, a_{k+1}, a_{k+2}) = (4, 2, 1)$
Since $a_{k+2} = 1$ , by definition we have that $a_{k+3} = 4$ .
Thus $(a_{k+1}, a_{k+2}, a_{k+3}) = (2, 1, 4)$ , which is what we needed to show.