OAI/Combinatorics/KMedianRecovery/Machines/SuffixMachine.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.cuts_prune line 9
  2. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.cuts_grow line 15
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.slices_labels line 27
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.cut_fields line 30
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.pruneOp line 35
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.pruneOp_computes line 36
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.pruneInput line 37
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.pruneInput_computes line 38
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.prune line 39
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.prune_computes line 40
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.prune_pack line 41
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.growOp line 48
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.growOp_computes line 51
  14. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.grow line 55
  15. def OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.grow_computes line 56
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySuffix.grow_pack line 58