OAI/Combinatorics/KMedian/CookLevin/TableauSystem.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.PCP.Tableau.Value line 16
  2. abbrev OAI.MetricKMedian.PCP.Tableau.Query line 17
  3. def OAI.MetricKMedian.PCP.Tableau.q0 line 18
  4. def OAI.MetricKMedian.PCP.Tableau.q1 line 19
  5. def OAI.MetricKMedian.PCP.Tableau.qtop line 20
  6. def OAI.MetricKMedian.PCP.Tableau.qwin line 21
  7. instance OAI.MetricKMedian.PCP.Tableau.queryNonempty line 22
  8. abbrev OAI.MetricKMedian.PCP.Tableau.Var line 23
  9. def OAI.MetricKMedian.PCP.Tableau.ctrl line 24
  10. def OAI.MetricKMedian.PCP.Tableau.resp line 25
  11. def OAI.MetricKMedian.PCP.Tableau.cell line 26
  12. def OAI.MetricKMedian.PCP.Tableau.time0 line 28
  13. def OAI.MetricKMedian.PCP.Tableau.now line 29
  14. def OAI.MetricKMedian.PCP.Tableau.later line 30
  15. def OAI.MetricKMedian.PCP.Tableau.clamp line 31
  16. inductive OAI.MetricKMedian.PCP.Tableau.Clause line 33
  17. def OAI.MetricKMedian.PCP.Tableau.query line 41
  18. def OAI.MetricKMedian.PCP.Tableau.relation line 57
  19. def OAI.MetricKMedian.PCP.Tableau.system line 66
  20. lemma OAI.MetricKMedian.PCP.Tableau.satisfies_iff line 69
  21. def OAI.MetricKMedian.PCP.Tableau.getControl line 73
  22. def OAI.MetricKMedian.PCP.Tableau.getResponse line 75
  23. def OAI.MetricKMedian.PCP.Tableau.getRow line 77
  24. lemma OAI.MetricKMedian.PCP.Tableau.row_valid line 79
  25. def OAI.MetricKMedian.PCP.Tableau.decodeRow line 84
  26. lemma OAI.MetricKMedian.PCP.Tableau.decodeRow_length line 87
  27. lemma OAI.MetricKMedian.PCP.Tableau.decodeRow_cell line 91
  28. def OAI.MetricKMedian.PCP.Tableau.decodeCfg line 95
  29. lemma OAI.MetricKMedian.PCP.Tableau.clamp_decode line 99
  30. lemma OAI.MetricKMedian.PCP.Tableau.decoded_transition line 105