Theorem Marketplace

Theorem Details

-- Antihydra Halts?
-- https://bbchallenge.org/antihydra

import Mathlib

def iter (x : ℕ × ℤ) : ℕ × ℤ :=
  let ⟨a, b⟩ := x;
  if a % 2 = 0 then (3 * a / 2, b + 2) else ((3 * a - 1)/2, b-1)

lemma antihydra_halts : (∃ n v : ℕ, Nat.repeat iter n ⟨8, 0⟩ = ⟨v, -1⟩) := sorry

Bounty: 0.006 ETH

Status: Open

Submit Your Proof

Back to Bounties

Theorem Details

-- Antihydra Halts? -- https://bbchallenge.org/antihydra import Mathlib def iter (x : ℕ × ℤ) : ℕ × ℤ := let ⟨a, b⟩ := x; if a % 2 = 0 then (3 * a / 2, b + 2) else ((3 * a - 1)/2, b-1) lemma antihydra_halts : (∃ n v : ℕ, Nat.repeat iter n ⟨8, 0⟩ = ⟨v, -1⟩) := sorry

Submit Your Proof