OAI/Combinatorics/EditApproximation/Binary/BinaryKeyedOnline.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The online branch computes its representative, all guards, coordinate count, iteration bound and accepted source residue before executing the literal finite optimizer.

  1. theorem OAI.EditApproximation.BinaryFraction.reduceOnlineIntegerWithWork_value line 19
  2. theorem OAI.EditApproximation.BinaryFraction.onlineIndexSetupWithWork_value line 30
  3. def OAI.EditApproximation.BinaryFraction.onlineBandReference line 35
  4. theorem OAI.EditApproximation.BinaryFraction.onlineBandReference_congr line 49
  5. def OAI.EditApproximation.BinaryFraction.keyedOnlineWithWork line 61
  6. theorem OAI.EditApproximation.BinaryFraction.keyedOnlineWithWork_value line 85