OAI/GroupTheory/PeriodicGroups/Rules/TemplateHierarchy.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.FiniteTable.Rigid.adjacent_blocks line 15
  2. def OAI.SourceBurnside.FiniteTable.Rigid.Template.cell line 47
  3. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.pos line 58
  4. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.metadata line 60
  5. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.first_iff line 63
  6. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.last_iff line 77
  7. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.adjacent line 104
  8. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.payload_format line 125
  9. def OAI.SourceBurnside.FiniteTable.Rigid.Template.region line 141
  10. lemma OAI.SourceBurnside.FiniteTable.Region.acquire line 161
  11. theorem OAI.SourceBurnside.FiniteTable.Region.literal_change line 167
  12. theorem OAI.SourceBurnside.FiniteTable.Region.literal_zero line 175
  13. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.idle_cell line 193
  14. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.idle_word line 199
  15. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.locate line 206
  16. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.slot line 215
  17. lemma OAI.SourceBurnside.FiniteTable.Rigid.Template.certificate line 224
  18. theorem OAI.SourceBurnside.FiniteTable.Rigid.Template.replacement line 234
  19. theorem OAI.SourceBurnside.FiniteTable.Rigid.Template.zero line 239
  20. def OAI.SourceBurnside.SourceMachine.regionData line 251
  21. def OAI.SourceBurnside.SourceMachine.regionCert line 253
  22. lemma OAI.SourceBurnside.SourceMachine.physical_assemble line 255
  23. lemma OAI.SourceBurnside.SourceMachine.candidate_region line 259
  24. theorem OAI.SourceBurnside.SourceMachine.fixed_region_entry line 270
  25. def OAI.SourceBurnside.FiniteTable.Codec.Step line 301
  26. abbrev OAI.SourceBurnside.FiniteTable.Codec.Reach line 303
  27. def OAI.SourceBurnside.FiniteTable.Codec.Survives line 304
  28. lemma OAI.SourceBurnside.FiniteTable.Codec.replacement_symm line 306
  29. lemma OAI.SourceBurnside.FiniteTable.Codec.step_symm line 311
  30. lemma OAI.SourceBurnside.FiniteTable.Codec.step_encode line 315
  31. lemma OAI.SourceBurnside.FiniteTable.Codec.reach_encode line 320
  32. lemma OAI.SourceBurnside.FiniteTable.Codec.split_encoding line 325
  33. lemma OAI.SourceBurnside.FiniteTable.Codec.step_from_encoding line 330
  34. lemma OAI.SourceBurnside.FiniteTable.Codec.reach_from_encoding line 339
  35. lemma OAI.SourceBurnside.FiniteTable.Codec.survives_encode_iff line 348
  36. def OAI.SourceBurnside.SourceMachine.bits line 366
  37. def OAI.SourceBurnside.SourceMachine.scalars line 367
  38. lemma OAI.SourceBurnside.SourceMachine.bits_scalars line 368
  39. lemma OAI.SourceBurnside.SourceMachine.scalars_bits line 371
  40. lemma OAI.SourceBurnside.SourceMachine.checkedSwap_raw line 374
  41. lemma OAI.SourceBurnside.SourceMachine.checkedReach_raw line 391
  42. lemma OAI.SourceBurnside.SourceMachine.checkedZero_raw line 401
  43. lemma OAI.SourceBurnside.SourceMachine.clean_nonzero line 413
  44. def OAI.SourceBurnside.SourceMachine.embedding line 428
  45. theorem OAI.SourceBurnside.SourceMachine.fixed_clean_nonzero line 431
  46. def OAI.SourceBurnside.SourceMachine.templateData line 457
  47. lemma OAI.SourceBurnside.SourceMachine.candidate_template line 462
  48. lemma OAI.SourceBurnside.SourceMachine.physical_template line 468
  49. lemma OAI.SourceBurnside.SourceMachine.template_certificate line 487
  50. theorem OAI.SourceBurnside.SourceMachine.fixed_forward line 498
  51. structure OAI.SourceBurnside.SourceMachine.MachineHierarchy line 544
  52. def OAI.SourceBurnside.SourceMachine.hierarchy line 563
  53. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.code line 575
  54. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.next_large line 576
  55. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.data_pos line 577
  56. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.height_pos line 578
  57. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.schedule line 579
  58. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.region_entry line 581
  59. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.faithful line 593
  60. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.simulate line 601
  61. lemma OAI.SourceBurnside.SourceMachine.embedding_length line 637
  62. lemma OAI.SourceBurnside.SourceMachine.idleCore_survives line 640
  63. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.nonzero_letter line 648
  64. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.unbounded_survivors line 656