OAI/GroupTheory/PeriodicGroups/Formulas/Tableaux.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.Tableau.Wire line 10
  2. def OAI.SourceBurnside.Tableau.Wire.eval line 12
  3. lemma OAI.SourceBurnside.Tableau.Wire.eval_map line 16
  4. def OAI.SourceBurnside.Tableau.nand line 21
  5. inductive OAI.SourceBurnside.Tableau.Circuit line 23
  6. def OAI.SourceBurnside.Tableau.Circuit.evaluate line 32
  7. def OAI.SourceBurnside.Tableau.Circuit.Satisfies line 37
  8. theorem OAI.SourceBurnside.Tableau.Circuit.evaluate_input line 43
  9. theorem OAI.SourceBurnside.Tableau.Circuit.evaluate_satisfies line 53
  10. theorem OAI.SourceBurnside.Tableau.Circuit.assignment_unique line 61
  11. structure OAI.SourceBurnside.Tableau.Circuit.Clause line 76
  12. def OAI.SourceBurnside.Tableau.Circuit.Clause.Holds line 80
  13. def OAI.SourceBurnside.Tableau.Circuit.Clause.map line 83
  14. lemma OAI.SourceBurnside.Tableau.Circuit.Clause.map_holds line 87
  15. def OAI.SourceBurnside.Tableau.Circuit.nandClauses line 92
  16. lemma OAI.SourceBurnside.Tableau.Circuit.nandClauses_iff line 97
  17. def OAI.SourceBurnside.Tableau.Circuit.clauses line 104
  18. theorem OAI.SourceBurnside.Tableau.Circuit.clauses_length line 110
  19. theorem OAI.SourceBurnside.Tableau.Circuit.clauses_iff line 116
  20. abbrev OAI.SourceBurnside.Tableau.Rectangle.Bits line 131
  21. abbrev OAI.SourceBurnside.Tableau.Rectangle.Row line 132
  22. def OAI.SourceBurnside.Tableau.Rectangle.neighborhood line 134
  23. def OAI.SourceBurnside.Tableau.Rectangle.localOutput line 140
  24. def OAI.SourceBurnside.Tableau.Rectangle.step line 143
  25. def OAI.SourceBurnside.Tableau.Rectangle.run line 146
  26. def OAI.SourceBurnside.Tableau.Rectangle.assignment line 150
  27. lemma OAI.SourceBurnside.Tableau.Rectangle.assignment_input line 153
  28. lemma OAI.SourceBurnside.Tableau.Rectangle.assignment_evaluate line 157
  29. def OAI.SourceBurnside.Tableau.Rectangle.Valid line 165
  30. lemma OAI.SourceBurnside.Tableau.Rectangle.valid_transition line 174
  31. theorem OAI.SourceBurnside.Tableau.Rectangle.valid_run line 189
  32. theorem OAI.SourceBurnside.Tableau.Rectangle.run_valid line 211
  33. theorem OAI.SourceBurnside.Tableau.Rectangle.accepting_tableau_iff line 226
  34. def OAI.SourceBurnside.Tableau.Layout.certificateCount line 241
  35. def OAI.SourceBurnside.Tableau.Layout.clauseCount line 243
  36. def OAI.SourceBurnside.Tableau.Layout.xAddress line 246
  37. def OAI.SourceBurnside.Tableau.Layout.yAddress line 248
  38. lemma OAI.SourceBurnside.Tableau.Layout.pack_lt line 251
  39. lemma OAI.SourceBurnside.Tableau.Layout.pack_injective line 256
  40. lemma OAI.SourceBurnside.Tableau.Layout.xAddress_lt line 267
  41. lemma OAI.SourceBurnside.Tableau.Layout.yAddress_lt line 271
  42. lemma OAI.SourceBurnside.Tableau.Layout.xAddress_injective line 277
  43. lemma OAI.SourceBurnside.Tableau.Layout.yAddress_injective line 285
  44. lemma OAI.SourceBurnside.Tableau.Layout.address_disjoint line 296
  45. lemma OAI.SourceBurnside.Tableau.Layout.rectangle_le line 302
  46. lemma OAI.SourceBurnside.Tableau.Layout.certificateCount_bound line 307
  47. lemma OAI.SourceBurnside.Tableau.Layout.clauseCount_bound line 313
  48. lemma OAI.SourceBurnside.Tableau.Layout.exponential_margin line 324
  49. theorem OAI.SourceBurnside.Tableau.Layout.layout_fits line 335