OAI/Combinatorics/KMedianRecovery/Encoding/WordExtras.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.WordEq.value_length_injective line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.WordEq.eq line 24
  3. def OAI.MetricKMedianRecovery.BitMachine.WordEq.eq_computes line 25
  4. lemma OAI.MetricKMedianRecovery.BitMachine.WordEq.eq_pair line 37
  5. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.encode_injective line 41
  6. def OAI.MetricKMedianRecovery.BitMachine.WordList.Drop.run line 61
  7. def OAI.MetricKMedianRecovery.BitMachine.WordList.Drop.run_computes line 62
  8. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Drop.drop_iterate line 77
  9. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Drop.run_encode line 94
  10. def OAI.MetricKMedianRecovery.BitMachine.WordList.lengthBits line 102
  11. def OAI.MetricKMedianRecovery.BitMachine.WordList.lengthBits_computes line 103
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.lengthBits_encode line 104
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.labels_injective line 111
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.eq_labels line 115
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.missing line 122
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.missing_computes line 123
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.allIn line 125
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.allIn_computes line 126
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.allIn_pack line 128
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.contains_setBits line 137
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.jumpBits line 145
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.ctxBits line 149
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.cf line 151
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.jf line 152
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.cf_computes line 153
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.jf_computes line 154
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.tagIs line 155
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.tagIs_computes line 156
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.copied line 158
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.copied_computes line 159
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.source line 163
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.source_computes line 165
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.target line 168
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.target_computes line 171
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.labelsCheck line 175
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.labelsCheck_computes line 177
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.accepts line 184
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.accepts_computes line 188
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.source_pack line 193
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.target_pack line 200
  41. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.accepts_pack line 207