OAI/Combinatorics/KMedian/Binary/BooleanFinite.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.FiniteTransducer.prefixes line 15
  2. theorem OAI.MetricKMedian.Binary.FiniteTransducer.mem_prefixes line 18
  3. abbrev OAI.MetricKMedian.Binary.FiniteTransducer.Q line 24
  4. def OAI.MetricKMedian.Binary.FiniteTransducer.state line 26
  5. abbrev OAI.MetricKMedian.Binary.FiniteTransducer.table line 29
  6. theorem OAI.MetricKMedian.Binary.FiniteTransducer.next_state line 37
  7. theorem OAI.MetricKMedian.Binary.FiniteTransducer.finish_state line 41
  8. theorem OAI.MetricKMedian.Binary.FiniteTransducer.run_state line 49
  9. def OAI.MetricKMedian.Binary.FiniteTransducer.program line 63
  10. theorem OAI.MetricKMedian.Binary.encodeBool_injective line 69
  11. theorem OAI.MetricKMedian.Binary.quote_injective line 73
  12. theorem OAI.MetricKMedian.Binary.encodePair_injective line 81
  13. def OAI.MetricKMedian.Binary.PolyProgram.boolFunction line 91
  14. def OAI.MetricKMedian.Binary.PolyProgram.boolNot line 95
  15. def OAI.MetricKMedian.Binary.PolyProgram.boolAnd line 97
  16. def OAI.MetricKMedian.Binary.PolyProgram.boolOr line 99