OAI/Computability/MinUncut/Machines/RawInitialMachinePhases.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_scratch line 11
  2. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_reversed line 14
  3. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachinePhases.copyInTime line 17
  4. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachinePhases.relationInTime line 32
  5. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachinePhases.bitWord_head line 45
  6. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachinePhases.loadSigns_step line 49
  7. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachinePhases.loadSignsInTime line 58
  8. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachinePhases.cleanupFieldInTime line 69
  9. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachinePhases.cleanupFinalInTime line 77
  10. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.fieldValue line 91
  11. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes line 96
  12. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_input line 102
  13. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_field line 106
  14. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_other line 110
  15. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_name line 118
  16. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.trace_trans line 124
  17. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.fieldsTrace line 128
  18. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.readClauseTrace line 224
  19. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineReadClause.readClauseInTime line 244
  20. abbrev OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.advance line 265
  21. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.outputTapes line 267
  22. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.outputTapes_reversed line 270
  23. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.outputTapes_other line 273
  24. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.outputTapes_twice line 277
  25. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.trace_trans line 284
  26. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.copyTrace line 288
  27. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.closeTailTrace line 296
  28. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.closeReverseTrace line 304
  29. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.reverse_encodeWord_add line 314
  30. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.rowEndBits line 320
  31. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.rowEndTrace line 324
  32. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.rowEndBits_append line 356
  33. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.falseRowTrace line 365
  34. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.trueRowTrace line 403
  35. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.pairWords line 432
  36. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.pairTrace line 437
  37. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.rowsTrace line 463
  38. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineRows.rowsInTime line 510
  39. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineCleanup.trace_trans line 532
  40. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineCleanup.incrementIndexTrace line 536
  41. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineCleanup.cleanupTrace line 542
  42. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineCleanup.cleanupInTime line 625
  43. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineBody.trace_trans line 645
  44. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineBody.guardTrace_succ line 649
  45. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineBody.guardTrace_zero line 664
  46. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineBody.bodyTrace line 678