Formal target: Corpus.OtherBeaverMathOlympiad.beaver_math_olympiad_problem_2_antihydra

BMO#2 Antihydra is a sequence starting at 8, and iterating the function $$H(n) = \left\lfloor \frac {3n}2 \right\rfloor.$$ The conjecture states that the cumulative number of odd values in this sequence is never more than twice the cumulative number of even values.

Exact formal statement

∀ (a : Nat → Nat) (b : Nat → Int),
  Eq.{1} (a 0) 8 →
    (∀ (n : Nat), Eq.{1} (a (HAdd.hAdd.{0, 0, 0} n 1)) (HDiv.hDiv.{0, 0, 0} (HMul.hMul.{0, 0, 0} 3 (a n)) 2)) →
      Eq.{1} (b 0) 0 →
        (∀ (n : Nat),
            Eq.{1} (b (HAdd.hAdd.{0, 0, 0} n 1))
              (ite.{1} (Eq.{1} (HMod.hMod.{0, 0, 0} (a n) 2) 0) (HAdd.hAdd.{0, 0, 0} (b n) 2)
                (HSub.hSub.{0, 0, 0} (b n) 1))) →
          ∀ (n : Nat), GE.ge.{0} (b n) 0

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record