Lemma: MrTheorem18_Collatz_1c53d8a4.power_two_reaches_one

Every power of two 2^r reaches 1 after r Collatz steps, including r = 0.

Exact formal statement

∀ (r : Nat), Eq.{1} (Nat.iterate.{1} Corpus.WikipediaCollatzConjecture.collatzStep r (HPow.hPow.{0, 0, 0} 2 r)) 1

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.