OAI/Computability/DirectedFeedback/Encoding/Lookup.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet line 14
  2. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.skipBits line 16
  3. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits line 27
  4. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits_fromTapes line 44
  5. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.skipBits_pushBound line 58
  6. inductive OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.Label line 66
  7. instance OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.(instance at line 70) line 70
  8. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.statement line 74
  9. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.program line 83
  10. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.rowBits line 87
  11. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.rowBits_eq line 89
  12. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits line 94
  13. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_nil line 97
  14. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_cons line 99
  15. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.skipCost line 103
  16. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.prefixCost line 106
  17. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost line 109
  18. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace line 121
  19. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace_fromTapes line 150
  20. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.selectTrace line 164
  21. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailTrace line 182
  22. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost_le line 250
  23. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailInTime line 269
  24. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.tableTailTrace line 292
  25. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.fullTableTailTrace line 324
  26. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.lookup_frame line 364
  27. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost line 370
  28. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost_le line 374
  29. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headIndex line 397
  30. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headValue line 400
  31. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headValue_eq_semantics line 403
  32. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.HeadTapes line 406
  33. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes line 408
  34. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost line 417
  35. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost_le line 421
  36. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headTimePolynomial line 430
  37. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headLookupInTime line 433
  38. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_head line 525
  39. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_frame line 530
  40. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes line 536
  41. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_source line 541
  42. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_tail line 547
  43. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_reverse line 553
  44. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_frame line 559
  45. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost line 565
  46. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_le line 568
  47. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_table_le line 575
  48. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.readRowInTime line 584
  49. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Lookup.machine line 668
  50. inductive OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape line 686
  51. instance OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.(instance at line 692) line 692
  52. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.Alphabet line 698
  53. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.Flags line 700
  54. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.Ambient line 701
  55. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.State line 702
  56. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.normal line 704
  57. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.initial line 707
  58. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.context line 709
  59. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv line 712
  60. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv_normal line 719
  61. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterEquiv line 724
  62. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts line 730
  63. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts_injective line 733
  64. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts line 737
  65. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts_injective line 740
  66. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.rowSources line 744
  67. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.headerSources line 745
  68. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.fieldPorts line 746
  69. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts line 748
  70. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_ne_output line 752
  71. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_cover line 755
  72. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareStatement line 777
  73. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterStatement line 782
  74. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.storeLoop line 786
  75. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_storeLoop line 789
  76. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.nextRow line 794
  77. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_nextRow line 798
  78. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.RuntimeModel.transportInTime line 806