Pure binary-counted iteration states

The existing counter transition, iteration law and arithmetic bound are moved unchanged from the legacy binary calculus. They store a binary counter with the current state, not a unary list.

def Turing.MultiTapeTM.Internal.BinaryCounter.countStep {β : Type} (step : β → β) : Option (ℕ × β) → Option (ℕ × β)

A round of the counted iteration: stop at zero, otherwise count down and apply step.

theorem Turing.MultiTapeTM.Internal.BinaryCounter.countStep_eq {β : Type} [Inhabited β] (step : β → β) (o : Option (ℕ × β)) : countStep step o = if (o.isSome && !decide ((o.getD default).1 = 0)) = true then some ((o.getD default).1 - 1, step (o.getD default).2) else none

theorem Turing.MultiTapeTM.Internal.BinaryCounter.iterate_countStep {β : Type} (step : β → β) (t : ℕ) (b : β) {k : ℕ} (hk : k ≤ t) : (countStep step)^[k] (some (t, b)) = some (t - k, step^[k] b)

theorem Turing.MultiTapeTM.Internal.BinaryCounter.sum_le {c₀ c₁ k k' A M X Y : ℕ} (hX : X ≤ k * (M + 1)) (hY : Y ≤ c₀ * (A + 1)) : c₀ * (A + 1) + X + c₁ * (Y + 1) ≤ (c₀ + c₁ * (c₀ + 1) + k + k') * (A + M + 1)

theorem Turing.MultiTapeTM.Internal.BinaryCounter.iterate_sub_one (k n : ℕ) : (fun (x : ℕ) => x - 1)^[k] n = n - k