OAI/Computability/DirectedFeedback/Encoding/Setup.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.Alphabet line 14
  2. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.Ports line 16
  3. inductive OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.Label line 18
  4. instance OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.(instance at line 23) line 23
  5. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.statement line 28
  6. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.resultTapes line 47
  7. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.resultTapes_other line 56
  8. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.setupInTime line 62
  9. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.tableSetupInTime line 152
  10. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.program line 179
  11. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Setup.machine line 182
  12. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet line 203
  13. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.State line 204
  14. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.relationEquiv line 206
  15. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.relationFintype line 212
  16. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.stateFintype line 215
  17. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlot line 220
  18. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlot line 230
  19. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots line 240
  20. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords line 246
  21. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots line 249
  22. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_preserves_correct line 255
  23. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_mem line 267
  24. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_finRange line 280
  25. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords_finRange line 287
  26. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlots line 299
  27. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation line 315
  28. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation line 320
  29. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation_fromTapes line 331
  30. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots_pushBound line 345
  31. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation_pushBound line 355
  32. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.parser line 361
  33. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.parser_pushBound line 366
  34. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.parserStep line 371
  35. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.parserTrace line 385
  36. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.ReadRelation.parserInTime line 397
  37. abbrev OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.Buffer line 418
  38. def OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.emptyBuffer line 420
  39. def OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.readSlots line 426
  40. def OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.fill line 435
  41. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.fill_apply line 438
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.fill_all line 449
  43. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readSlots line 456
  44. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readAll line 472
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_readSlots line 486
  46. def OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.writeSlots line 494
  47. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_writeSlots line 499
  48. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_writeSlots line 514
  49. def OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.blockStmt line 530
  50. def OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.finishAt line 537
  51. def OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.blockMapAt line 542
  52. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockStmt line 546
  53. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockMapAt line 553
  54. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockStmt line 561
  55. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockMapAt line 575
  56. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.step_blockMapAt line 586
  57. def OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.machine line 603
  58. theorem OAI.DFVSGames.Foundations.Complexity.MachineFixedBlockMap.machine_statementPushBound line 614