OAI/Computability/MinUncut/PCP/DescriptorEmission.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.codedEquation line 14
  2. def OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorWords line 18
  3. def OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorBits line 21
  4. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorWords_length line 24
  5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorBits_length_le line 28
  6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.decode_descriptorBits line 32
  7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.parse_descriptorWords line 36
  8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.decode_codedEquation line 42
  9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.codedEquation_global line 53
  10. def OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorPushBound line 62
  11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorPushBound_le line 65
  12. instance OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.localInputDecidableEq line 81
  13. def OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor line 87
  14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.stepAux_emitDescriptor line 93
  15. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor_push_bound line 104
  16. def OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptorInTime line 111
  17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceDescriptorEmission.descriptor_output_frame line 124
  18. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceTestEmit.Label line 140
  19. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceTestEmit.State line 141
  20. def OAI.MinUncutGames.Foundations.Hastad.SourceTestEmit.localEquation line 143
  21. def OAI.MinUncutGames.Foundations.Hastad.SourceTestEmit.bodyLabel line 146
  22. def OAI.MinUncutGames.Foundations.Hastad.SourceTestEmit.program line 151
  23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTestEmit.testTrace line 159
  24. def OAI.MinUncutGames.Foundations.Hastad.SourceTestEmit.testInTime line 180
  25. def OAI.MinUncutGames.Foundations.Hastad.SourceTestEmit.sourceTestInTime line 197
  26. inductive OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.Label line 235
  27. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.State line 240
  28. structure OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.Layout line 242
  29. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.equationBits line 254
  30. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.steps line 257
  31. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.bodyLabel line 263
  32. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.statement line 267
  33. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.program line 276
  34. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.resultTapes line 280
  35. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.resultTapes_other line 283
  36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.resultTapes_source line 287
  37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.resultTapes_temporary line 291
  38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.resultTapes_scratch line 295
  39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.emitTrace line 299
  40. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.appendTrace line 327
  41. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.appendInTime line 370
  42. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.programInTime line 386
  43. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.sourceAppendInTime line 398
  44. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.Tape line 434
  45. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.standardLayout line 436
  46. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.machine line 448
  47. def OAI.MinUncutGames.Foundations.Hastad.SourceTestAppend.machineInTime line 459
  48. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.Query line 477
  49. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.State line 478
  50. inductive OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.Label line 480
  51. def OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.finish line 487
  52. def OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.statement line 493
  53. def OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.prefixBits line 505
  54. def OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.prefixSteps line 511
  55. theorem OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.resultTapes_append line 517
  56. theorem OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.prefixTrace line 528
  57. theorem OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.prefixSteps_le line 580
  58. theorem OAI.MinUncutGames.Foundations.Hastad.SourceQueryLoop.loopInTime line 592