Lemma: Agent20_CollatzRound2_01a13459_E20_V2.merge_539_family

For every natural a, U^10(1024*a+539)=U^6(576*a+303), with 0<576*a+303<1024*a+539. Uses the locally defined genuine reduced Collatz map.

Exact formal statement

∀ (a : Nat),
  And
    (Eq.{1} (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 1024 a) 539) 10)
      (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 576 a) 303) 6))
    (And (LT.lt.{0} 0 (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 576 a) 303))
      (LT.lt.{0} (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 576 a) 303)
        (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 1024 a) 539)))

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

Environment availability: available.

Public JSON record