OAI/Computability/DirectedFeedback/Machines/MachineExpanderFamilyTapes.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.boolWord line 55
  2. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.toBoolWord line 60
  3. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes line 65
  4. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes line 68
  5. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.toBoolWord_boolWord line 71
  6. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.boolWord_toBoolWord line 77
  7. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.toBool_fromBool line 83
  8. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.fromBool_toBool line 88
  9. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.transport_tapes_apply_inline_MachineExpanderFamilyTapes line 93
  10. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_eq_transport line 100
  11. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_eq_transport line 108
  12. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_update line 116
  13. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_update line 125
  14. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.configuration_fromBool line 135
  15. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.configuration_toBool line 141
  16. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.controlStatementInverse line 157
  17. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.controlTrace line 164
  18. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.controlDrainTrace line 188
  19. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.controlTransferTrace line 207
  20. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.clearRegister line 232
  21. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.registerStates_reset line 235
  22. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_idempotent line 239
  23. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.caller_clearRegister line 242
  24. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_position line 245
  25. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_register line 248
  26. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.boolTraceActual line 253
  27. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.drainBoolTrace line 264
  28. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.transferBoolTrace line 281
  29. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.installedTapes line 304
  30. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.cleanedCounterTapes line 311
  31. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.installTableBoolTrace line 314
  32. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersBoolTrace line 373
  33. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.installTableTrace line 391
  34. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersTrace line 404
  35. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.installTableInTime line 415
  36. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersInTime line 430
  37. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_scratch line 452
  38. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_destination line 455
  39. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affine_scratch_ne_destination line 458
  40. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes line 461
  41. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_other line 468
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_source line 474
  43. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_scratch line 479
  44. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_destination line 484
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseBoolTrace line 492
  46. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseTrace line 537
  47. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseInTime line 552
  48. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.copyCountInTime line 565
  49. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.multiplySizeInTime line 582
  50. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.emitSteps line 609
  51. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.affinePlan_bits line 611
  52. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.affinePlan_steps line 622
  53. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.emittedWord line 629
  54. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.emittedWord_target line 633
  55. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.emittedWord_other line 638
  56. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.program_firstEmit line 646
  57. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.program_secondEmit line 652
  58. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.program_outputEmit line 658
  59. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.firstEmitTraceAt line 668
  60. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.secondEmitTraceAt line 699
  61. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.outputEmitTraceAt line 730
  62. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTimeAt line 761
  63. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTimeAt line 779
  64. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTimeAt line 797
  65. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.firstEmitTrace line 817
  66. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.secondEmitTrace line 829
  67. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.outputEmitTrace line 841
  68. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTime line 853
  69. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTime line 865
  70. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTime line 877