OAI/Combinatorics/EditApproximation/Binary/BitMemoWorkOn.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The same exact fresh-key work accounting applies to normalized programs whose simulation is justified on reachable child values.

  1. theorem OAI.EditApproximation.rankedBitMemoEvaluate_work_transfer_on line 11
  2. theorem OAI.EditApproximation.rankedBitProgramValue_value_on line 30