case zero
n : ℕ
⊢ hyperoperation (n + 4) 0 Nat.zero = if Even Nat.zero then 1 else 0

case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 4) 0 (Nat.succ kk) = if Even (Nat.succ kk) then 1 else 0
n k : ℕ
⊢ hyperoperation (n + 4) 0 k = if Even k then 1 else 0
induction' k with kk kih
case zero
n : ℕ
⊢ 1 = if Even Nat.zero then 1 else 0
case zero
n : ℕ
⊢ hyperoperation (n + 4) 0 Nat.zero = if Even Nat.zero then 1 else 0
rw [hyperoperation_ge_three_eq_one]
no goals
case zero
n : ℕ
⊢ 1 = if Even Nat.zero then 1 else 0
simp only [even_zero, if_true]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (hyperoperation (n + 3 + 1) 0 kk) = if Even (Nat.succ kk) then 1 else 0
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 4) 0 (Nat.succ kk) = if Even (Nat.succ kk) then 1 else 0
rw [hyperoperation_recursion]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if Even (Nat.succ kk) then 1 else 0
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (hyperoperation (n + 3 + 1) 0 kk) = if Even (Nat.succ kk) then 1 else 0
rw [kih]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if ¬Even kk then 1 else 0
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if Even (Nat.succ kk) then 1 else 0
simp_rw [Nat.even_add_one]
case succ.inl
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : Even kk
⊢ hyperoperation (n + 3) 0 1 = 0

case succ.inr
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : ¬Even kk
⊢ hyperoperation (n + 3) 0 0 = 1
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if ¬Even kk then 1 else 0
split_ifs
no goals
case succ.inl
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : Even kk
⊢ hyperoperation (n + 3) 0 1 = 0
exact hyperoperation_ge_two_eq_self (n + 1) 0
no goals
case succ.inr
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : ¬Even kk
⊢ hyperoperation (n + 3) 0 0 = 1
exact hyperoperation_ge_three_eq_one n 0