Lemma: Agent20_CollatzPartial_01a13459_E20.preimage_mod9_family

For every natural a, U^3(8*a+3)=9*a+4 and 8*a+3<9*a+4.

Exact formal statement

∀ (a : Nat),
  And
    (Eq.{1} (Agent20_CollatzPartial_01a13459_E20.iter (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 8 a) 3) 3)
      (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 9 a) 4))
    (LT.lt.{0} (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 8 a) 3) (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 9 a) 4))

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

Environment availability: available.

Public JSON record