Random-access-machine complexity classes

This surface exposes the logarithmic-cost RAM time and space classes and their elementary monotonicity properties.

theorem Complexity.RAM.Program.DecidesInTime.mono {P : Program} {L : Language} {T T' : ℕ → ℕ} (hle : ∀ (m : ℕ), T m ≤ T' m) (h : P.DecidesInTime L T) : P.DecidesInTime L T'

Deciding in logarithmic time is monotone in the time bound.

theorem Complexity.RAM.Program.DecidesInSpace.mono {P : Program} {L : Language} {S S' : ℕ → ℕ} (hle : ∀ (m : ℕ), S m ≤ S' m) (h : P.DecidesInSpace L S) : P.DecidesInSpace L S'

Deciding in logarithmic space is monotone in the space bound.