From d7429287d758c2cc3d86d0be1fb5eba825cf6f76 Mon Sep 17 00:00:00 2001
From: Archie <94995351+archiebrowne@users.noreply.github.com>
Date: Mon, 13 Nov 2023 20:37:35 +0000
Subject: [PATCH] halfing defined for collatz

---
 Game/Levels/Hard/level_2.lean | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/Game/Levels/Hard/level_2.lean b/Game/Levels/Hard/level_2.lean
index e167083..47783a9 100644
--- a/Game/Levels/Hard/level_2.lean
+++ b/Game/Levels/Hard/level_2.lean
@@ -22,16 +22,11 @@ LemmaDoc MyNat.Colatz as "Collatz" in "Hard" "
 `Collatz` is the proof of disproof of the Collatz conjecture.
 "
 
-def even (n : ℕ) : Prop
-  | zero => true
-  | succ a => ¬ (even a)
-
+-- halving used for the sequence
 def half (n : ℕ) :=
-  | zero => zero
-  | succ a =>
-  match even a with
-  | true => half a + 1
-  | false => half a
+  | 0 => 0
+  | 1 => 0
+  | (a + 2) => half a + 1
 
 -- 'collatz function'
 def f (x : ℕ) :=