OAI/Combinatorics/KMedianRecovery/Machines/Program2.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.embedStacks_refl line 10
  2. abbrev OAI.MetricKMedianRecovery.BitMachine.While.program line 17
  3. def OAI.MetricKMedianRecovery.BitMachine.While.runCfg line 33
  4. def OAI.MetricKMedianRecovery.BitMachine.While.controlCfg line 35
  5. lemma OAI.MetricKMedianRecovery.BitMachine.While.run_step line 38
  6. lemma OAI.MetricKMedianRecovery.BitMachine.While.initial line 52
  7. lemma OAI.MetricKMedianRecovery.BitMachine.While.start line 56
  8. lemma OAI.MetricKMedianRecovery.BitMachine.While.stop line 63
  9. lemma OAI.MetricKMedianRecovery.BitMachine.While.handoff line 70
  10. def OAI.MetricKMedianRecovery.BitMachine.While.advance line 78
  11. def OAI.MetricKMedianRecovery.BitMachine.While.next line 86
  12. lemma OAI.MetricKMedianRecovery.BitMachine.While.next_fixed line 89
  13. def OAI.MetricKMedianRecovery.BitMachine.While.outputs line 92
  14. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.whileLoop line 122