OAI/Combinatorics/EditApproximation/Binary/BinaryReadComposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Callback work is retained when a finite loop is supplied with a costed reader. These lemmas compare the literal loop counters, so a lookup cannot disappear when its returned word is passed to arithmetic.

  1. theorem OAI.EditApproximation.arithmeticMapWithWork_extra line 12
  2. theorem OAI.EditApproximation.arithmeticFlatMapWithWork_extra line 37
  3. theorem OAI.EditApproximation.filterWithWork_extra line 56
  4. theorem OAI.EditApproximation.sum_map_le_length_mul line 81
  5. theorem OAI.EditApproximation.arithmeticFlatMapWithWork_factor line 91
  6. theorem OAI.EditApproximation.filterWithWork_length_le_cost line 111
  7. theorem OAI.EditApproximation.arithmeticMapWithWork_length_le_cost line 117
  8. theorem OAI.EditApproximation.filterWithWork_add_read line 123