OAI/Combinatorics/EditApproximation/Binary/BitMemoMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A proof-only view of a binary-word memo as its rational-value memo. The tree shape and every lookup/insertion path are preserved.

  1. def OAI.EditApproximation.BinaryMemo.mapValues line 11
  2. theorem OAI.EditApproximation.BinaryMemo.mapValues_value line 15
  3. theorem OAI.EditApproximation.BinaryMemo.mapValues_left line 18
  4. theorem OAI.EditApproximation.BinaryMemo.mapValues_right line 21
  5. theorem OAI.EditApproximation.BinaryMemo.mapValues_lookup line 24
  6. theorem OAI.EditApproximation.BinaryMemo.mapValues_insert line 30
  7. theorem OAI.EditApproximation.BinaryMemo.mapValues_nodes line 38