Sparse-entry miss copy — definitions

An update scan must preserve every unmatched sparse entry. This module first emits the decoded address/value pair to the output stream and then restores the ordinary next-entry scan invariant.

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.encodeTapes {n : ℕ} (tapes : EntryMatchTapes n) : EntryEncodeTapes n

View the decoded address and value tapes as entry-emission sources.

Equations

• tapes.encodeTapes = { address := tapes.address, value := tapes.value, ne := ⋯ }

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.encodeTapes_address {n : ℕ} (tapes : EntryMatchTapes n) : tapes.encodeTapes.address = tapes.address

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.encodeTapes_value {n : ℕ} (tapes : EntryMatchTapes n) : tapes.encodeTapes.value = tapes.value

def Complexity.RAM.RegisterStore.Machine.entryMissCopiedWork {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (work : Fin n → Tape) (i : Fin n) : Tape

Exact work family after the decoded address and value have been emitted. Only their heads change; their canonical contents and every other tape remain literal copies of the readable-match endpoint.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryMissCopyTM {n : ℕ} (tapes : EntryMatchTapes n) : TM n

Emit the decoded unmatched entry and restore the next-iteration scratch invariant.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryMissCopyTime {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (queryBits : List Bool) (initialWork matchedWork : Fin n → Tape) : ℕ

Compositional runtime bound for copying and cleaning one unmatched entry.

Equations

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