Sparse-entry final append — definitions

When an update exhausts the old store without a match, a nonzero new value is appended using the preserved query and replacement tapes. Both sources are then restored exactly so the caller retains its canonical work frame.

def Complexity.RAM.RegisterStore.Machine.EntryReplaceTapes.appendEncodeTapes {n : ℕ} (tapes : EntryReplaceTapes n) : EntryEncodeTapes n

View the preserved query and replacement tapes as a fresh-entry encoder.

Equations

• tapes.appendEncodeTapes = { address := tapes.entry.query, value := tapes.replacement, ne := ⋯ }

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryReplaceTapes.appendEncodeTapes_address {n : ℕ} (tapes : EntryReplaceTapes n) : tapes.appendEncodeTapes.address = tapes.entry.query

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryReplaceTapes.appendEncodeTapes_value {n : ℕ} (tapes : EntryReplaceTapes n) : tapes.appendEncodeTapes.value = tapes.replacement

def Complexity.RAM.RegisterStore.Machine.entryAppendRestoreTM {n : ℕ} (tapes : EntryReplaceTapes n) : TM n

Emit a fresh query/value entry and restore both canonical source cursors.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryAppendRestoreTime (address newValue : ℕ) : ℕ

Exact compositional bound for final append and two-source restoration.

Equations

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