Lemma: Agent20_CollatzPartial_01a13459_E20.merge_family

For every natural a, U iterated six times on 64*a+15 equals U(54*a+13), and 54*a+13 is smaller than 64*a+15.

Exact formal statement

∀ (a : Nat),
  And
    (Eq.{1} (Agent20_CollatzPartial_01a13459_E20.iter (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 64 a) 15) 6)
      (Agent20_CollatzPartial_01a13459_E20.U (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 54 a) 13)))
    (LT.lt.{0} (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 54 a) 13) (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 64 a) 15))

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

Environment availability: available.

Public JSON record