OAI/Combinatorics/KMedianRecovery/Machines/DeleteFold.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedianRecovery.CanonicalDelete.Acc line 9
  2. def OAI.MetricKMedianRecovery.CanonicalDelete.step line 15
  3. lemma OAI.MetricKMedianRecovery.CanonicalDelete.fold_result line 21
  4. structure OAI.MetricKMedianRecovery.CanonicalDelete.Bounds line 32
  5. lemma OAI.MetricKMedianRecovery.CanonicalDelete.Bounds.step line 41
  6. lemma OAI.MetricKMedianRecovery.CanonicalDelete.Bounds.fold line 90
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.accBits line 108
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.contextBits line 110
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.cf line 112
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.sf line 113
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.cf_computes line 114
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.sf_computes line 115
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.rest line 117
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.rest_computes line 118
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.retained line 119
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.retained_computes line 120
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.openSet line 122
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.openSet_computes line 124
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.extended line 126
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.extended_computes line 128
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.added line 130
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.added_computes line 131
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.extras line 133
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.extras_computes line 134
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.vertex line 135
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.vertex_computes line 136
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.vertices line 138
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.vertices_computes line 139
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.step line 141
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.step_computes line 142
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.tail_labels line 152
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.base_open line 157
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.step_pack line 162