OAI/Combinatorics/EditApproximation/Binary/BitMemoRun.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Execution of charged adaptive queries on actual binary-word memos. The rational view is used only to prove preservation of the memo trace; Boolean local work is retained as an additional counter.

  1. def OAI.EditApproximation.BitRecursiveMemoResult.decode line 15
  2. theorem OAI.EditApproximation.BitQuery.runMemo_decode line 24