OAI/Computability/DirectedFeedback/Machines/MachineProductField.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Explicit.MachineProductField.Layout line 16
  2. def OAI.DFVSGames.Explicit.MachineProductField.gatherSlots line 18
  3. def OAI.DFVSGames.Explicit.MachineProductField.hornerRole line 21
  4. theorem OAI.DFVSGames.Explicit.MachineProductField.hornerRole_injective line 30
  5. def OAI.DFVSGames.Explicit.MachineProductField.hornerSlots line 42
  6. def OAI.DFVSGames.Explicit.MachineProductField.clearTapes line 45
  7. abbrev OAI.DFVSGames.Explicit.MachineProductField.Label line 49
  8. def OAI.DFVSGames.Explicit.MachineProductField.entry line 53
  9. def OAI.DFVSGames.Explicit.MachineProductField.instruction line 56
  10. structure OAI.DFVSGames.Explicit.MachineProductField.Ready line 69
  11. def OAI.DFVSGames.Explicit.MachineProductField.gathered line 80
  12. def OAI.DFVSGames.Explicit.MachineProductField.evaluated line 85
  13. def OAI.DFVSGames.Explicit.MachineProductField.emitted line 90
  14. def OAI.DFVSGames.Explicit.MachineProductField.finalTapes line 96
  15. def OAI.DFVSGames.Explicit.MachineProductField.steps line 101
  16. theorem OAI.DFVSGames.Explicit.MachineProductField.gathered_extra line 110
  17. theorem OAI.DFVSGames.Explicit.MachineProductField.fieldTrace line 119
  18. theorem OAI.DFVSGames.Explicit.MachineProductGather.affine_final_length line 212
  19. theorem OAI.DFVSGames.Explicit.MachineProductGather.finalTapes_length line 244
  20. theorem OAI.DFVSGames.Explicit.MachineProductField.mem_clearTapes line 280
  21. theorem OAI.DFVSGames.Explicit.MachineProductField.extra_not_mem_clearTapes line 286
  22. theorem OAI.DFVSGames.Explicit.MachineProductField.Ready.empty_clearTapes line 295
  23. theorem OAI.DFVSGames.Explicit.MachineProductField.gathered_frame line 302
  24. theorem OAI.DFVSGames.Explicit.MachineProductField.finalTapes_eq line 312
  25. theorem OAI.DFVSGames.Explicit.MachineProductField.Ready.output_update line 338
  26. theorem OAI.DFVSGames.Explicit.MachineProductField.final_ready line 355
  27. theorem OAI.DFVSGames.Explicit.MachineProductField.emitted_clear_length line 362
  28. theorem OAI.DFVSGames.Explicit.MachineProductField.clearTapes_length line 380
  29. theorem OAI.DFVSGames.Explicit.MachineProductField.cleanup_steps_le line 383
  30. abbrev OAI.DFVSGames.Explicit.MachineProductRow.Layout line 417
  31. abbrev OAI.DFVSGames.Explicit.MachineProductRow.Command line 418
  32. def OAI.DFVSGames.Explicit.MachineProductRow.fieldRole line 420
  33. theorem OAI.DFVSGames.Explicit.MachineProductRow.fieldRole_injective line 424
  34. def OAI.DFVSGames.Explicit.MachineProductRow.fieldSlots line 437
  35. abbrev OAI.DFVSGames.Explicit.MachineProductRow.LocalLabel line 441
  36. abbrev OAI.DFVSGames.Explicit.MachineProductRow.Label line 444
  37. def OAI.DFVSGames.Explicit.MachineProductRow.localMain line 447
  38. def OAI.DFVSGames.Explicit.MachineProductRow.localInstruction line 450
  39. def OAI.DFVSGames.Explicit.MachineProductRow.entry line 455
  40. def OAI.DFVSGames.Explicit.MachineProductRow.instruction line 459
  41. def OAI.DFVSGames.Explicit.MachineProductRow.outputTape line 465
  42. def OAI.DFVSGames.Explicit.MachineProductRow.appendField line 467
  43. def OAI.DFVSGames.Explicit.MachineProductRow.rowBits line 470
  44. def OAI.DFVSGames.Explicit.MachineProductRow.result line 473
  45. theorem OAI.DFVSGames.Explicit.MachineProductRow.resultOf_eq line 477
  46. structure OAI.DFVSGames.Explicit.MachineProductRow.Ready line 488
  47. theorem OAI.DFVSGames.Explicit.MachineProductRow.Ready.appendField line 495
  48. theorem OAI.DFVSGames.Explicit.MachineProductRow.rowTrace line 515
  49. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.row_table_lookup line 569
  50. def OAI.DFVSGames.Explicit.ProductMachineSemantics.inputTable line 590
  51. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.inputTable_source line 592
  52. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.inputTable_target line 597
  53. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.inputTable_image line 602
  54. def OAI.DFVSGames.Explicit.ProductMachineSemantics.reverseDigits line 609
  55. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.reverseDigits_at line 612
  56. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.reverseDigits_words line 615
  57. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.horner_ofFin line 628
  58. def OAI.DFVSGames.Explicit.ProductMachineSemantics.sourceCommand line 634
  59. def OAI.DFVSGames.Explicit.ProductMachineSemantics.targetCommand line 635
  60. def OAI.DFVSGames.Explicit.ProductMachineSemantics.imageCommand line 636
  61. def OAI.DFVSGames.Explicit.ProductMachineSemantics.commands line 639
  62. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.commands_length line 642
  63. def OAI.DFVSGames.Explicit.ProductMachineSemantics.fields line 645
  64. def OAI.DFVSGames.Explicit.ProductMachineSemantics.fieldValue line 649
  65. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.source_fields line 654
  66. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.target_fields line 659
  67. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.image_fields line 664
  68. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.selected line 673
  69. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.command_offset_lt line 685
  70. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.fields_lt line 696
  71. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.source_value line 709
  72. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.target_value line 716
  73. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.image_value line 723
  74. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.encodeWords_map_inline_ProductMachineSemantics line 733
  75. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.rowBits_eq line 739
  76. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.encodeWords_flatMap_inline_ProductMachineSemantics line 765
  77. def OAI.DFVSGames.Explicit.ProductMachineSemantics.allRowsBits line 771
  78. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.allRowsBits_eq line 775
  79. theorem OAI.DFVSGames.Explicit.ProductMachineSemantics.gameBits_eq line 789