OAI/Combinatorics/KMedian/Binary/BooleanMachine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Binary.Machine line 11
  2. def OAI.MetricKMedian.Binary.Machine.tm line 29
  3. instance OAI.MetricKMedian.Binary.Machine.allWorkFinite line 40
  4. abbrev OAI.MetricKMedian.Binary.Machine.Cfg line 43
  5. def OAI.MetricKMedian.Binary.Machine.initialCfg line 45
  6. def OAI.MetricKMedian.Binary.Machine.finalCfg line 48
  7. theorem OAI.MetricKMedian.Binary.Machine.init_eq line 51
  8. theorem OAI.MetricKMedian.Binary.Machine.halt_eq line 55
  9. abbrev OAI.MetricKMedian.Binary.Machine.step line 59
  10. theorem OAI.MetricKMedian.Binary.cfg_ext line 63
  11. inductive OAI.MetricKMedian.Binary.Trace line 72
  12. theorem OAI.MetricKMedian.Binary.Trace.trans line 79
  13. theorem OAI.MetricKMedian.Binary.Trace.map line 85
  14. theorem OAI.MetricKMedian.Binary.Trace.iterate_eq line 92
  15. theorem OAI.MetricKMedian.Binary.Trace.of_iterate line 100
  16. def OAI.MetricKMedian.Binary.Trace.inTime line 127
  17. theorem OAI.MetricKMedian.Binary.Trace.of_inTime line 130
  18. def OAI.MetricKMedian.Binary.Machine.pushes line 138
  19. def OAI.MetricKMedian.Binary.Machine.volume line 147
  20. theorem OAI.MetricKMedian.Binary.Machine.volume_update line 151
  21. theorem OAI.MetricKMedian.Binary.Machine.stepAux_volume line 164
  22. def OAI.MetricKMedian.Binary.Machine.growth line 191
  23. theorem OAI.MetricKMedian.Binary.Machine.step_volume line 193
  24. theorem OAI.MetricKMedian.Binary.Machine.trace_volume line 205
  25. theorem OAI.MetricKMedian.Binary.Machine.initial_volume line 215
  26. theorem OAI.MetricKMedian.Binary.Machine.final_volume line 221
  27. theorem OAI.MetricKMedian.Binary.Machine.output_length line 227