Lemma: Agent20_CollatzRound2_01a13459_E20_V2.arbitrary_odd_block_merge

For all natural m and positive t with 3^(m+1)*t congruent to 3 mod 4, U^(m+4)(2^(m+2)*t-1)=U^(m+3)(2^(m+1)*t-1); the latter start is positive and smaller. Block length m is unbounded.

Exact formal statement

∀ (m t : Nat),
  LT.lt.{0} 0 t →
    Eq.{1} (HMod.hMod.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 3 (HAdd.hAdd.{0, 0, 0} m 1)) t) 4) 3 →
      And
        (Eq.{1}
          (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter
            (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} m 2)) t) 1)
            (HAdd.hAdd.{0, 0, 0} m 4))
          (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter
            (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} m 1)) t) 1)
            (HAdd.hAdd.{0, 0, 0} m 3)))
        (And
          (LT.lt.{0} 0
            (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} m 1)) t) 1))
          (LT.lt.{0} (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} m 1)) t) 1)
            (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} m 2)) t) 1)))

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

Environment availability: available.

Public JSON record