OAI/Computability/PerfectCompleteness/Reduction/CompletionAlphabetLemmas.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CompletionAlphabet.size line 18
  2. theorem OAI.PerfectCompleteness.CompletionAlphabet.size_positive line 20
  3. theorem OAI.PerfectCompleteness.CompletionAlphabet.cap_le_size line 24
  4. theorem OAI.PerfectCompleteness.CompletionAlphabet.size_budget line 27
  5. theorem OAI.PerfectCompleteness.CompletionAlphabet.exists_target line 37
  6. theorem OAI.PerfectCompleteness.exists_completion_tables line 74
  7. structure OAI.PerfectCompleteness.HierarchicalGame.Family line 103
  8. def OAI.PerfectCompleteness.HierarchicalGame.toBlockFamily line 117
  9. abbrev OAI.PerfectCompleteness.HierarchicalGame.LeftVertex line 125
  10. abbrev OAI.PerfectCompleteness.HierarchicalGame.RightVertex line 126
  11. abbrev OAI.PerfectCompleteness.HierarchicalGame.LeftLabel line 127
  12. abbrev OAI.PerfectCompleteness.HierarchicalGame.RightLabel line 128
  13. abbrev OAI.PerfectCompleteness.HierarchicalGame.leftAt line 130
  14. abbrev OAI.PerfectCompleteness.HierarchicalGame.rightAt line 131
  15. theorem OAI.PerfectCompleteness.HierarchicalGame.leftVertex_finite line 133
  16. theorem OAI.PerfectCompleteness.HierarchicalGame.rightVertex_finite line 134
  17. theorem OAI.PerfectCompleteness.HierarchicalGame.leftLabel_finite line 135
  18. theorem OAI.PerfectCompleteness.HierarchicalGame.rightLabel_finite line 136
  19. theorem OAI.PerfectCompleteness.HierarchicalGame.leftKey_eq line 138
  20. theorem OAI.PerfectCompleteness.HierarchicalGame.rightKey_eq line 142
  21. abbrev OAI.PerfectCompleteness.HierarchicalGame.edge line 147
  22. theorem OAI.PerfectCompleteness.HierarchicalGame.edge_eq_iff line 150
  23. theorem OAI.PerfectCompleteness.HierarchicalGame.edge_at_most_two line 167
  24. def OAI.PerfectCompleteness.HierarchicalGame.game line 171
  25. def OAI.PerfectCompleteness.HierarchicalGame.satisfyingStrategy line 176
  26. theorem OAI.PerfectCompleteness.HierarchicalGame.edge_satisfyingStrategy line 181
  27. theorem OAI.PerfectCompleteness.HierarchicalGame.success_satisfyingStrategy line 187
  28. theorem OAI.PerfectCompleteness.HierarchicalGame.value_eq_one line 192
  29. def OAI.PerfectCompleteness.HierarchicalGameTable.strategy line 221
  30. def OAI.PerfectCompleteness.HierarchicalGameTable.background line 224
  31. def OAI.PerfectCompleteness.HierarchicalGameTable.matrix line 230
  32. theorem OAI.PerfectCompleteness.HierarchicalGameTable.accepts_iff line 235