Lemma: Agent20_CollatzPartial_01a13459_E20.initial_growth_formula

For every natural k and positive natural t, U^k(2^k*t-1)=3^k*t-1.

Exact formal statement

∀ (k t : Nat),
  LT.lt.{0} 0 t →
    Eq.{1}
      (Agent20_CollatzPartial_01a13459_E20.iter
        (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 k) t) 1) k)
      (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 3 k) t) 1)

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

Environment availability: available.

Public JSON record