halfing defined for collatz

leanprover-community · Nov 13, 2023 · d742928 · d742928
1 parent f217111
commit d742928
Showing 1 changed file with 4 additions and 9 deletions.
diff --git 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 : ℕ) :=