OAI/Combinatorics/KMedian/Binary/BooleanTransducer.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Binary.Transducer line 12
  2. def OAI.MetricKMedian.Binary.Transducer.run line 23
  3. def OAI.MetricKMedian.Binary.Transducer.width line 27
  4. theorem OAI.MetricKMedian.Binary.Transducer.finish_length line 30
  5. theorem OAI.MetricKMedian.Binary.Transducer.next_length line 33
  6. theorem OAI.MetricKMedian.Binary.Transducer.run_length line 36
  7. inductive OAI.MetricKMedian.Binary.Transducer.Key line 46
  8. instance OAI.MetricKMedian.Binary.Transducer.(instance at line 47) line 47
  9. abbrev OAI.MetricKMedian.Binary.Transducer.Label line 51
  10. abbrev OAI.MetricKMedian.Binary.Transducer.State line 52
  11. def OAI.MetricKMedian.Binary.Transducer.emit line 54
  12. theorem OAI.MetricKMedian.Binary.Transducer.emit_step line 59
  13. def OAI.MetricKMedian.Binary.Transducer.transfer line 69
  14. def OAI.MetricKMedian.Binary.Transducer.code line 75
  15. abbrev OAI.MetricKMedian.Binary.Transducer.machine line 84
  16. def OAI.MetricKMedian.Binary.Transducer.store line 94
  17. theorem OAI.MetricKMedian.Binary.Transducer.stacks_update_input line 99
  18. theorem OAI.MetricKMedian.Binary.Transducer.stacks_update_buffer line 104
  19. theorem OAI.MetricKMedian.Binary.Transducer.stacks_update_output line 109
  20. def OAI.MetricKMedian.Binary.Transducer.readCfg line 114
  21. def OAI.MetricKMedian.Binary.Transducer.transferCfg line 117
  22. theorem OAI.MetricKMedian.Binary.Transducer.read_cons line 120
  23. theorem OAI.MetricKMedian.Binary.Transducer.read_nil line 127
  24. theorem OAI.MetricKMedian.Binary.Transducer.read_run line 132
  25. theorem OAI.MetricKMedian.Binary.Transducer.transfer_cons line 141
  26. theorem OAI.MetricKMedian.Binary.Transducer.transfer_nil line 146
  27. theorem OAI.MetricKMedian.Binary.Transducer.transfer_run line 155
  28. theorem OAI.MetricKMedian.Binary.Transducer.run_trace line 164
  29. def OAI.MetricKMedian.Binary.Transducer.program line 178