OAI/Combinatorics/EditApproximation/Specification/Footprint.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EditApproximation.BitQuery.Footprint.cells line 15
  2. theorem OAI.EditApproximation.BitQuery.Footprint.runCells_congr line 41
  3. def OAI.EditApproximation.BitQuery.Heap.footprint line 58

    Source documentation

    Forget only the local allocation/work certificates, preserving the exact trace.

    def footprint {ι β : Type*} {program : BitQuery ι β} : Heap program → Footprint program
  | .done value => .done value
  | .read key next continuation => .read key next (fun word => (continuation word).footprint)
  | .charge localCells _ next => .charge localCells next.footprint

    Mentions: OAI.EditApproximation.BitQuery, OAI.EditApproximation.BitQuery.Heap, OAI.EditApproximation.BitQuery.Footprint, OAI.EditApproximation.BitQuery.value

  4. theorem OAI.EditApproximation.BitQuery.Heap.footprint_done line 63
  5. theorem OAI.EditApproximation.BitQuery.Heap.footprint_read line 66
  6. theorem OAI.EditApproximation.BitQuery.Heap.footprint_charge line 71
  7. theorem OAI.EditApproximation.BitQuery.Heap.footprint_cells line 75
  8. theorem OAI.EditApproximation.BitQuery.Heap.footprint_bind line 83
  9. theorem OAI.EditApproximation.BitQuery.Heap.footprint_compute line 97
  10. theorem OAI.EditApproximation.BitQuery.Heap.footprint_chargeOf line 102
  11. theorem OAI.EditApproximation.BitQuery.Heap.footprint_computeOf line 106
  12. theorem OAI.EditApproximation.BitQuery.Heap.footprint_collect line 111
  13. theorem OAI.EditApproximation.BitQuery.Heap.footprint_mapKeysWithWork line 126
  14. theorem OAI.EditApproximation.BitQuery.Heap.map_decidable_cases line 144
  15. theorem OAI.EditApproximation.BitQuery.Heap.footprint_mpr_congr line 150
  16. theorem OAI.EditApproximation.BitQuery.Heap.footprint_restrictWithWork line 156
  17. theorem OAI.EditApproximation.BitQuery.Heap.footprint_normalize line 181
  18. theorem OAI.EditApproximation.BitQuery.Heap.footprint_runCells line 186
  19. theorem OAI.EditApproximation.BitQuery.Heap.footprint_rankedBitMemoCells line 196