Lemma: MrTheorem18_Collatz_1c53d8a4.compose_trajectories

If n reaches m after a Collatz steps and m reaches 1 after b steps, then n reaches 1 after a+b steps.

Exact formal statement

∀ (n m a b : Nat),
  Eq.{1} (Nat.iterate.{1} Corpus.WikipediaCollatzConjecture.collatzStep a n) m →
    Eq.{1} (Nat.iterate.{1} Corpus.WikipediaCollatzConjecture.collatzStep b m) 1 →
      Eq.{1} (Nat.iterate.{1} Corpus.WikipediaCollatzConjecture.collatzStep (HAdd.hAdd.{0, 0, 0} a b) n) 1

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

Environment availability: available.

Public JSON record