OAI/Computability/VertexCover/Machines/AlphabetFrame.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.Machine.AlphabetMachine.relationFintype line 46
  2. theorem OAI.VertexCover.Machine.AlphabetMachine.relationCode_injective line 51
  3. abbrev OAI.VertexCover.Machine.AlphabetMachine.State line 54
  4. def OAI.VertexCover.Machine.AlphabetMachine.code line 55
  5. def OAI.VertexCover.Machine.AlphabetMachine.old line 56
  6. def OAI.VertexCover.Machine.AlphabetMachine.head line 57
  7. def OAI.VertexCover.Machine.AlphabetMachine.tablePoly line 59
  8. def OAI.VertexCover.Machine.AlphabetMachine.indexPoly line 60
  9. def OAI.VertexCover.Machine.AlphabetMachine.verticesPoly line 61
  10. def OAI.VertexCover.Machine.AlphabetMachine.dartsPoly line 63
  11. def OAI.VertexCover.Machine.AlphabetMachine.oldPoly line 65
  12. def OAI.VertexCover.Machine.AlphabetMachine.tailPoly line 66
  13. def OAI.VertexCover.Machine.AlphabetMachine.reversePoly line 68
  14. def OAI.VertexCover.Machine.AlphabetMachine.relationPoly line 70
  15. def OAI.VertexCover.Machine.AlphabetMachine.headPoly line 72
  16. def OAI.VertexCover.Machine.AlphabetMachine.loopPoly line 75
  17. abbrev OAI.VertexCover.Machine.AlphabetMachine.Local line 78
  18. def OAI.VertexCover.Machine.AlphabetMachine.blockCount line 79
  19. def OAI.VertexCover.Machine.AlphabetMachine.blockEquiv line 80
  20. theorem OAI.VertexCover.Machine.AlphabetMachine.block_pos line 83
  21. theorem OAI.VertexCover.Machine.AlphabetMachine.block_val line 86
  22. theorem OAI.VertexCover.Machine.AlphabetMachine.dart_block_val line 91