def collatz_function (n : ℕ) : ℕ

Equations

• collatz_function n = if n % 2 = 0 then n / 2 else 3 * n + 1

def hailstone (init : ℕ) : ℕ → ℕ

Equations

• hailstone init pow = Nat.recOn pow init fun (x theval : ℕ) => collatz_function theval

def steps_required (bound : ℕ) (init : ℕ) : ℤ

Equations

• steps_required bound init = if h : ∃ k < bound, hailstone init k = 1 then ↑(Nat.find h) else -1

def steps_required_sequence (bound : ℕ) (len : ℕ) : List ℤ

Equations

• steps_required_sequence bound len = Nat.recOn len [] fun (n : ℕ) (seq_ind : List ℤ) => seq_ind ++ [steps_required bound n]