OAI/Computability/MinUncut/Machines/MachineInitialHeaders.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.Alphabet line 16
  2. def OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.prefixScan line 18
  3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.update_source line 29
  4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.update_scratch line 43
  5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.update_output line 54
  6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_true line 60
  7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_false line 71
  8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.replicate_append_cons line 81
  9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.prefixScanTrace line 86
  10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.prefixTrace line 123
  11. def OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.prefixInTime line 173
  12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.prefixScan_pushBound line 192
  13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.literalTrace line 199
  14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.trace_trans line 212
  15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.headerTrace line 216
  16. def OAI.MinUncutGames.Foundations.Complexity.MachineInitialHeaders.headerInTime line 296
  17. inductive OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.Tape line 335
  18. abbrev OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.Signs line 340
  19. abbrev OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.State line 341
  20. abbrev OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.Alphabet line 342
  21. inductive OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.CopyPhase line 344
  22. inductive OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.Label line 352
  23. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.initialState line 366
  24. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.stateKeys line 368
  25. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.stateKeys_complete line 373
  26. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.nameField line 379
  27. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.copySource line 381
  28. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.copyScale line 386
  29. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.copyNext line 390
  30. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.relationNext line 399
  31. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.finalTape line 405
  32. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.drain line 408
  33. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.headerTape line 411
  34. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.relationOutput line 413
  35. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.program line 417
  36. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineModel.machine line 467
  37. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.inputTapes line 486
  38. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.firstTapes line 490
  39. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.counterTapes line 495
  40. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.headerTapes line 501
  41. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.startTapes line 508
  42. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.initList_eq line 516
  43. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.trace_trans line 525
  44. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.readCountersTrace line 530
  45. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.headersTrace line 563
  46. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.initializeIndexTrace line 582
  47. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.startTrace line 594
  48. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.formulaStartTrace line 604
  49. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.startInTime line 614
  50. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineStart.formulaStartInTime line 623
  51. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput line 641
  52. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_nil line 644
  53. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_cons line 646
  54. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput line 650
  55. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.mapIdx_ofFn line 654
  56. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_nil line 660
  57. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_cons line 662
  58. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_numbered line 669
  59. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.tableWords_decomposition line 679
  60. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.loopTapes line 686
  61. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.startTapes_eq line 694
  62. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.decrement_counter line 700
  63. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoopData.increment_index line 706