OAI/Combinatorics/KMedianRecovery/Machines/FiniteMachine.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.initial line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.initial_computes line 15
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.initial_pack line 17
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.finished line 25
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.finished_computes line 26
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.completedTrace line 28
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.completed_trace_computes line 29
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.completed line 31
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.completed_computes line 32
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.completed_pack line 35
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.complete line 43
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.complete_computes line 45
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.complete_pack line 50
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.data line 58
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.data_computes line 59
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.phase line 60
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.phase_computes line 62
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.start line 68
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.start_computes line 70
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.start_pack line 72
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.historyBits line 82
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.history line 83
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.history_computes line 85
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.continuation line 87
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.continuation_computes line 89
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.continuation_pack line 95
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.copied line 107
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.copied_computes line 111
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.copied_pack line 118
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.swapped line 125
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.swapped_computes line 129
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.swapped_pack line 134
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.labels_append line 143
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.labels_cons line 145
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.labels_nil line 147
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.union line 149
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.union_computes line 150
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.union_pack line 152
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.union_list_pack line 156
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.replaceOpen line 160
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.replaceOpen_computes line 163
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.replaceOpen_pack line 171
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.historyBits_append line 181
  44. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.historyBits_cons line 184
  45. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.historyBits_nil line 186
  46. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.flatten_historyBits line 187
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.after line 193
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.after_computes line 195
  49. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteMachine.after_pack line 197