OAI/Combinatorics/EditApproximation/Binary/BinaryMemoSpace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A fixed-width binary memo has bounded height on every execution, including failed approximation events and repeated lookups. This bound uses the actual returned tree and does not count a complete table allocation.

  1. def OAI.EditApproximation.BinaryMemo.height line 13
  2. theorem OAI.EditApproximation.BinaryMemo.child_height line 17
  3. theorem OAI.EditApproximation.BinaryMemo.insert_height line 25
  4. theorem OAI.EditApproximation.BinaryMemo.nodes_le_height line 40
  5. theorem OAI.EditApproximation.FiniteQuery.run_height_bound line 54
  6. theorem OAI.EditApproximation.rankedMemoEvaluate_height_bound line 69
  7. theorem OAI.EditApproximation.rankedMemoEvaluate_nodes_bound line 96