OAI/Combinatorics/KMedianRecovery/Recovery/Store2.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.WordOperations.store line 12
  2. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.store0 line 13
  3. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.store1 line 14
  4. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.upd0 line 15
  5. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.upd1 line 17
  6. abbrev OAI.MetricKMedianRecovery.BitMachine.WordOperations.appendProgram line 20
  7. def OAI.MetricKMedianRecovery.BitMachine.WordOperations.cfg line 42
  8. def OAI.MetricKMedianRecovery.BitMachine.WordOperations.done line 43
  9. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.parse_nil line 45
  10. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.parse_one line 47
  11. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.parse_false line 49
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.parse_true line 51
  13. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.restore_nil line 54
  14. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.restore_cons line 56
  15. def OAI.MetricKMedianRecovery.BitMachine.WordOperations.parse_phase line 60
  16. def OAI.MetricKMedianRecovery.BitMachine.WordOperations.restore_phase line 80
  17. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.initial line 89
  18. lemma OAI.MetricKMedianRecovery.BitMachine.WordOperations.final line 93
  19. def OAI.MetricKMedianRecovery.BitMachine.WordOperations.append_computes line 98
  20. abbrev OAI.MetricKMedianRecovery.BitMachine.WordOperations.prefixProgram line 111
  21. def OAI.MetricKMedianRecovery.BitMachine.WordOperations.prefix_computes line 121
  22. abbrev OAI.MetricKMedianRecovery.BitMachine.WordOperations.tailProgram line 130
  23. def OAI.MetricKMedianRecovery.BitMachine.WordOperations.tail_computes line 140
  24. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.append line 151
  25. def OAI.MetricKMedianRecovery.BitMachine.const_computes line 156