OAI/Computability/DirectedFeedback/Machines/OutputSize.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Reduction.OutputSize.explicitBodies_length_le line 59
  2. def OAI.DFVSGames.Reduction.OutputSize.vertexCoefficient line 68
  3. def OAI.DFVSGames.Reduction.OutputSize.edgeCoefficient line 71
  4. theorem OAI.DFVSGames.Reduction.OutputSize.collect_vertex_coefficient_inline_OutputSize line 75
  5. theorem OAI.DFVSGames.Reduction.OutputSize.collect_edge_coefficient_inline_OutputSize line 80
  6. theorem OAI.DFVSGames.Reduction.OutputSize.output_vertices_le line 85
  7. theorem OAI.DFVSGames.Reduction.OutputSize.output_constraints_eq line 99
  8. def OAI.DFVSGames.Reduction.OutputSize.sizeBound line 106
  9. theorem OAI.DFVSGames.Reduction.OutputSize.sizeBound_mono line 112
  10. theorem OAI.DFVSGames.Reduction.OutputSize.output_bits_length_le line 124
  11. def OAI.DFVSGames.Reduction.OutputSize.outputPolynomial line 138
  12. theorem OAI.DFVSGames.Reduction.OutputSize.outputPolynomial_eval line 144
  13. theorem OAI.DFVSGames.Reduction.OutputSize.output_bits_polynomial_in_occurrences line 149
  14. theorem OAI.DFVSGames.Reduction.OutputSize.output_bits_polynomial_in_input line 157
  15. theorem OAI.DFVSGames.Reduction.OutputSize.fixed_parameters_output_size line 166
  16. def OAI.DFVSGames.Reduction.AddressOutputSize.vertexBound line 186
  17. def OAI.DFVSGames.Reduction.AddressOutputSize.edgeBound line 190
  18. def OAI.DFVSGames.Reduction.AddressOutputSize.bitsBound line 193
  19. theorem OAI.DFVSGames.Reduction.AddressOutputSize.bitsBound_mono line 197
  20. def OAI.DFVSGames.Reduction.AddressOutputSize.sizeBound line 205
  21. theorem OAI.DFVSGames.Reduction.AddressOutputSize.table_constraints_eq line 208
  22. theorem OAI.DFVSGames.Reduction.AddressOutputSize.scaled_sum_le_inline_AddressOutputSize line 216
  23. theorem OAI.DFVSGames.Reduction.AddressOutputSize.output_constraints_eq line 223
  24. theorem OAI.DFVSGames.Reduction.AddressOutputSize.output_vertices_le_input line 232
  25. theorem OAI.DFVSGames.Reduction.AddressOutputSize.output_constraints_le_input line 251
  26. theorem OAI.DFVSGames.Reduction.AddressOutputSize.output_bits_length_le line 260
  27. def OAI.DFVSGames.Reduction.AddressOutputSize.outputPolynomial line 269
  28. theorem OAI.DFVSGames.Reduction.AddressOutputSize.outputPolynomial_eval line 277
  29. theorem OAI.DFVSGames.Reduction.AddressOutputSize.output_bits_polynomial_in_input line 283
  30. theorem OAI.DFVSGames.Reduction.AddressOutputSize.fixed_parameters_output_size line 291
  31. def OAI.DFVSGames.Reduction.AddressOutputSize.directVertexBound line 298
  32. def OAI.DFVSGames.Reduction.AddressOutputSize.directEdgeCoefficient line 301
  33. def OAI.DFVSGames.Reduction.AddressOutputSize.directSizeBound line 304
  34. theorem OAI.DFVSGames.Reduction.AddressOutputSize.direct_vertices_le_input line 308
  35. theorem OAI.DFVSGames.Reduction.AddressOutputSize.direct_constraints_eq line 324
  36. theorem OAI.DFVSGames.Reduction.AddressOutputSize.direct_constraints_le_input line 332
  37. theorem OAI.DFVSGames.Reduction.AddressOutputSize.direct_bits_length_le line 340
  38. def OAI.DFVSGames.Reduction.AddressOutputSize.directOutputPolynomial line 349
  39. theorem OAI.DFVSGames.Reduction.AddressOutputSize.directOutputPolynomial_eval line 356
  40. theorem OAI.DFVSGames.Reduction.AddressOutputSize.direct_bits_polynomial_in_input line 362
  41. theorem OAI.DFVSGames.Reduction.AddressOutputSize.fixed_parameters_direct_output_size line 370
  42. def OAI.DFVSGames.Reduction.AddressMachineLoop.bits line 390
  43. def OAI.DFVSGames.Reduction.AddressMachineLoop.stateTapes line 395
  44. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.stateTapes_frame line 401
  45. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.stateTapes_savedIndex line 411
  46. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.stateTapes_private line 416
  47. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.stateTapes_header line 424
  48. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.stateTapes_ready line 435
  49. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.stateTapes_clean line 462
  50. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.stateTapes_base line 478
  51. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.stateTapes_capacity line 487
  52. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.appended_stateTapes line 499
  53. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.bodyTrace line 511
  54. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.setDigits_initialized_zero line 533
  55. def OAI.DFVSGames.Reduction.AddressMachineLoop.finalTapes line 553
  56. def OAI.DFVSGames.Reduction.AddressMachineLoop.traversal line 557
  57. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.allBits_eq line 593
  58. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.final_reversed line 599
  59. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.headerBits_eq line 612
  60. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.final_accumulator line 634
  61. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.final_other line 640
  62. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.final_outputEmpty line 647
  63. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.final_current line 657
  64. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.final_remaining line 661
  65. def OAI.DFVSGames.Reduction.AddressMachineLoop.timePolynomial line 666
  66. theorem OAI.DFVSGames.Reduction.AddressMachineLoop.timePolynomial_eval line 669
  67. def OAI.DFVSGames.Reduction.AddressMachineLoop.inPolynomialTime line 674
  68. def OAI.DFVSGames.Reduction.AddressMachineFinish.timePolynomial line 699
  69. def OAI.DFVSGames.Reduction.AddressMachineFinish.completePrefix line 703
  70. def OAI.DFVSGames.Reduction.MachineAddressGame.output line 763
  71. def OAI.DFVSGames.Reduction.MachineAddressGame.prefixPolynomial line 767
  72. def OAI.DFVSGames.Reduction.MachineAddressGame.timePolynomial line 770
  73. def OAI.DFVSGames.Reduction.MachineAddressGame.prefixInTime line 773
  74. def OAI.DFVSGames.Reduction.MachineAddressGame.fullRunInTime line 785
  75. def OAI.DFVSGames.Reduction.MachineAddressGame.computableInPolyTime line 795
  76. theorem OAI.DFVSGames.Reduction.MachineAddressGame.workAlphabetFinite line 810