OAI/Computability/DirectedFeedback/Machines/MachineProductPower.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Explicit.MachineProductPower.digits line 16
  2. theorem OAI.DFVSGames.Explicit.MachineProductPower.value_eq line 18
  3. abbrev OAI.DFVSGames.Explicit.MachineProductPower.Label line 25
  4. def OAI.DFVSGames.Explicit.MachineProductPower.instruction line 27
  5. def OAI.DFVSGames.Explicit.MachineProductPower.steps line 34
  6. theorem OAI.DFVSGames.Explicit.MachineProductPower.powerTrace line 37
  7. def OAI.DFVSGames.Explicit.MachineProductPower.timePolynomial line 79
  8. theorem OAI.DFVSGames.Explicit.MachineProductPower.steps_le line 83
  9. abbrev OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.Alphabet line 107
  10. def OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.prefixScan line 109
  11. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.update_source_inline_MachineInitialHeaders line 120
  12. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.update_scratch_inline_MachineInitialHeaders line 134
  13. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.update_output_inline_MachineInitialHeaders line 145
  14. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_true line 151
  15. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_false line 162
  16. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.replicate_append_cons_inline_MachineInitialHeaders line 172
  17. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.prefixScanTrace line 177
  18. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.prefixTrace line 214
  19. def OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.prefixInTime line 264
  20. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.prefixScan_pushBound line 283
  21. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.literalTrace line 290
  22. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.trace_trans_inline_MachineInitialHeaders line 303
  23. theorem OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.headerTrace line 307
  24. def OAI.DFVSGames.Foundations.Complexity.MachineInitialHeaders.headerInTime line 387
  25. abbrev OAI.DFVSGames.Explicit.MachineProductSeed.Command line 431
  26. abbrev OAI.DFVSGames.Explicit.MachineProductSeed.LocalLabel line 432
  27. abbrev OAI.DFVSGames.Explicit.MachineProductSeed.Label line 433
  28. def OAI.DFVSGames.Explicit.MachineProductSeed.entry line 435
  29. def OAI.DFVSGames.Explicit.MachineProductSeed.localInstruction line 438
  30. def OAI.DFVSGames.Explicit.MachineProductSeed.instruction line 442
  31. def OAI.DFVSGames.Explicit.MachineProductSeed.result line 446
  32. def OAI.DFVSGames.Explicit.MachineProductSeed.finalTapes line 449
  33. theorem OAI.DFVSGames.Explicit.MachineProductSeed.sequence_steps line 452
  34. theorem OAI.DFVSGames.Explicit.MachineProductSeed.seedTrace line 460
  35. theorem OAI.DFVSGames.Explicit.MachineProductSeed.finalTapes_frame line 478
  36. theorem OAI.DFVSGames.Explicit.MachineProductSeed.finalTapes_field line 488
  37. inductive OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.Tape line 514
  38. inductive OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.Label line 518
  39. def OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.labelAt line 525
  40. def OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.statement line 528
  41. def OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.digitOutput line 541
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.digitOutput_frame line 546
  43. def OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.digitInTime line 556
  44. def OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.stageTapes line 607
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.stageTapes_frame line 612
  46. theorem OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.stageTapes_current line 624
  47. theorem OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.stageTapes_remaining line 647
  48. def OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.prefixInTime line 669
  49. def OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.initializeInTime line 701
  50. theorem OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.output_current line 724
  51. theorem OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.output_remaining line 730
  52. theorem OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.output_radix line 736
  53. theorem OAI.DFVSGames.Foundations.Complexity.MachineOdometerInit.output_scratch line 742