OAI/Combinatorics/KMedianRecovery/Machines/MatchFold.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedianRecovery.CanonicalMatch.Acc line 10
  2. def OAI.MetricKMedianRecovery.CanonicalMatch.step line 16
  3. lemma OAI.MetricKMedianRecovery.CanonicalMatch.fold_result line 20
  4. lemma OAI.MetricKMedianRecovery.CanonicalMatch.fold_bounds line 32
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.accBits line 66
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.contextBits line 68
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.cf line 70
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.sf line 71
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.item line 72
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.cf_computes line 73
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.sf_computes line 74
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.item_computes line 76
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.copied line 77
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.copied_computes line 79
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.advancingInput line 81
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.advancingInput_computes line 83
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.advanced line 93
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.advanced_computes line 94
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.front line 96
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.prefix_computes line 97
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.rest line 99
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.suffix_computes line 100
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.vertices line 101
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.vertices_computes line 102
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.step line 104
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.step_computes line 105
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.advanced_pack line 113
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.step_pack line 126