OAI/Combinatorics/EditApproximation/Binary/IntegerInputInspection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit linear scans select the input-dependent symbol and position widths. The alphabet exponent is used only in the analysis.

  1. theorem OAI.EditApproximation.integerMagnitudeWithWork_spec line 15
  2. theorem OAI.EditApproximation.integerMagnitude_append line 23
  3. theorem OAI.EditApproximation.size_div_two line 32

    Source documentation

    Count the shifts in a literal binary-length loop.

    private theorem size_div_two (n : ℕ) (hn : n ≠ 0) : n.size = (n / 2).size + 1 := by
…
  4. theorem OAI.EditApproximation.inputBitLengthWithWork_spec line 38
  5. theorem OAI.EditApproximation.integerInputInspectionWithWork_spec line 51
  6. theorem OAI.EditApproximation.integerInputInspectionWithWork_cost line 58