decRegTM: decrement a register

decRegTM q erases the last mark of the unary register q: scan right over the marks, erase the final one, rewind. From regTape d to regTape (d - 1) (truncated: the zero register is left unchanged) in 2d + 4 steps. The missing primitive for descending loop fuels — the pairwise at-most-one families iterate over shrinking suffixes.

Mirror of incRegTM (RegisterOps.lean) with an erase phase.

inductive Complexity.TM.DecPhase : Type

Control states of decRegTM: scan right over the marks, erase the last one, move back to the sentinel, park on cell 1, then done.

• scan : DecPhase
• erase : DecPhase
• back : DecPhase
• park : DecPhase
• done : DecPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqDecPhase : DecidableEq DecPhase

Equations

• Complexity.TM.instDecidableEqDecPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeDecPhase : Fintype DecPhase

DecPhase is a finite type, as required by the TM structure.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.decRegTM {n : ℕ} (q : Fin n) : TM n

Decrement register q: scan right over the marks, erase the last one, rewind to cell 1. From regTape d to regTape (d - 1) in 2d + 4 steps; every other tape untouched. The zero register is unchanged.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.decRegTM_hoareTime {n : ℕ} (q : Fin n) (d : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), i ≠ q → Parked (work₀ i)) (hq : work₀ q = regTape d) : (decRegTM q).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update work₀ q (regTape (d - 1))) ys) (2 * d + 4)

decRegTM Hoare specification. From regTape d in register q, reach regTape (d - 1) in 2d + 4 steps (regTape 0 is left unchanged); the input, output, and every other work tape are untouched.