OAI/Combinatorics/EditApproximation/Refinement/ComputedCacheWords.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit multiword cache storage after substituting the computed height.

  1. theorem OAI.EditApproximation.cacheWordBudget_le_cube line 10
  2. theorem OAI.EditApproximation.computed_input_size_le_height line 27
  3. theorem OAI.EditApproximation.computed_cacheWordBudget_le_cube line 31
  4. theorem OAI.EditApproximation.computed_refinementBase_length line 40