OAI/Combinatorics/KMedianRecovery/Branching/CopyComputes.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.copy_computes line 9
  2. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryResources.copies_replicate line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.cap line 19
  4. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryResources.cap_length line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.inc line 23
  6. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.inc_computes line 24
  7. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryResources.inc_iter line 28
  8. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.lengthBits line 32
  9. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.lengthBits_computes line 34
  10. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryResources.lengthBits_eq line 37
  11. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.triple line 44
  12. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.triple_computes line 45
  13. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryResources.triple_iter line 49
  14. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryResources.three_power_length line 53
  15. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.threePower line 60
  16. def OAI.MetricKMedianRecovery.BitMachine.UnaryResources.threePower_computes line 62
  17. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryResources.threePower_eq line 65
  18. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.encode_append line 73
  19. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.copies_encode line 77
  20. def OAI.MetricKMedianRecovery.BitMachine.WordList.repeatWords line 83
  21. def OAI.MetricKMedianRecovery.BitMachine.WordList.repeatWords_computes line 85
  22. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.repeatWords_pair line 88
  23. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.repeatWords_ofFn line 91