OAI/Combinatorics/KMedianRecovery/Sampling/ExtractPrefix.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.extractPrefix line 9
  2. lemma OAI.MetricKMedianRecovery.BitMachine.extractPrefix_pair line 13
  3. abbrev OAI.MetricKMedianRecovery.BitMachine.headProgram line 20
  4. def OAI.MetricKMedianRecovery.BitMachine.headCfg line 42
  5. def OAI.MetricKMedianRecovery.BitMachine.headEnd line 44
  6. lemma OAI.MetricKMedianRecovery.BitMachine.head_initial line 47
  7. lemma OAI.MetricKMedianRecovery.BitMachine.head_final line 52
  8. lemma OAI.MetricKMedianRecovery.BitMachine.head_clear_nil line 57
  9. lemma OAI.MetricKMedianRecovery.BitMachine.head_clear_cons line 62
  10. def OAI.MetricKMedianRecovery.BitMachine.head_clear_outputs line 67
  11. lemma OAI.MetricKMedianRecovery.BitMachine.head_step_nil line 73
  12. lemma OAI.MetricKMedianRecovery.BitMachine.head_step_one line 78
  13. lemma OAI.MetricKMedianRecovery.BitMachine.head_step_false line 83
  14. lemma OAI.MetricKMedianRecovery.BitMachine.head_step_true line 88
  15. def OAI.MetricKMedianRecovery.BitMachine.head_outputs line 93
  16. def OAI.MetricKMedianRecovery.BitMachine.extractReverse_computes line 111
  17. def OAI.MetricKMedianRecovery.BitMachine.extractPrefix_computes line 118