OAI/Computability/DirectedFeedback/Machines/AddressMachineInitial.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders line 59
  2. def OAI.DFVSGames.Reduction.AddressMachineInitial.initialized line 64
  3. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.input_header_inline_AddressMachineInitial line 68
  4. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.input_headerClean line 75
  5. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_frame line 96
  6. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_empty line 106
  7. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_source line 117
  8. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_variables line 122
  9. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_occurrences line 134
  10. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_base line 146
  11. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_capacity line 151
  12. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_reversed line 156
  13. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_work line 170
  14. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_current line 173
  15. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_remaining line 177
  16. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.afterHeaders_copyScratch line 181
  17. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_frame line 185
  18. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_header line 191
  19. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_source line 199
  20. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_variables line 206
  21. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_occurrences line 209
  22. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_base line 212
  23. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_capacity line 216
  24. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_reversed line 220
  25. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_current line 226
  26. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_remaining line 231
  27. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_savedIndex line 237
  28. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_empty line 241
  29. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_work line 247
  30. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_index line 251
  31. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_scratch line 258
  32. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_copyScratch line 265
  33. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_field line 270
  34. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_finalOutput line 278
  35. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_privateAddress line 287
  36. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_edgeClean line 297
  37. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.initialized_eq_setDigits_zero line 312
  38. def OAI.DFVSGames.Reduction.AddressMachineInitial.inTime line 337
  39. def OAI.DFVSGames.Reduction.AddressMachineInitial.timePolynomial line 371
  40. theorem OAI.DFVSGames.Reduction.AddressMachineInitial.timePolynomial_eval line 375
  41. def OAI.DFVSGames.Reduction.AddressMachineInitial.inPolynomialTime line 382
  42. def OAI.DFVSGames.Reduction.OccurrenceTupleOrder.readCoordinates line 405
  43. theorem OAI.DFVSGames.Reduction.OccurrenceTupleOrder.readCoordinates_apply line 408
  44. theorem OAI.DFVSGames.Reduction.OccurrenceTupleOrder.readCoordinates_involutive line 411
  45. def OAI.DFVSGames.Reduction.OccurrenceTupleOrder.coordinateEquiv line 416
  46. theorem OAI.DFVSGames.Reduction.OccurrenceTupleOrder.readCoordinates_snoc line 422
  47. theorem OAI.DFVSGames.Reduction.OccurrenceTupleOrder.tupleOrder_readCoordinates line 426
  48. theorem OAI.DFVSGames.Reduction.OccurrenceTupleOrder.functions_readCoordinates line 451
  49. theorem OAI.DFVSGames.Reduction.OccurrenceTupleOrder.functions_flatMap line 458
  50. theorem OAI.DFVSGames.Reduction.OccurrenceTupleOrder.actualSchedule_order line 473
  51. theorem OAI.DFVSGames.Reduction.OccurrenceTupleOrder.actualSchedule_flatMap line 479
  52. def OAI.DFVSGames.Integration.AddressTupleBudget.radixBound line 502
  53. def OAI.DFVSGames.Integration.AddressTupleBudget.magnitude line 504
  54. def OAI.DFVSGames.Integration.AddressTupleBudget.magnitudePolynomial line 508
  55. theorem OAI.DFVSGames.Integration.AddressTupleBudget.magnitudePolynomial_eval line 513
  56. theorem OAI.DFVSGames.Integration.AddressTupleBudget.source_counts_le line 519
  57. theorem OAI.DFVSGames.Integration.AddressTupleBudget.radix_le line 524
  58. theorem OAI.DFVSGames.Integration.AddressTupleBudget.radix_le_magnitude line 531
  59. theorem OAI.DFVSGames.Integration.AddressTupleBudget.capacity_le_magnitude line 538
  60. theorem OAI.DFVSGames.Integration.AddressTupleBudget.field_length_le_magnitude line 546
  61. theorem OAI.DFVSGames.Integration.AddressTupleBudget.canonicalValues_le line 550
  62. theorem OAI.DFVSGames.Integration.AddressTupleBudget.loaded_fields_le_magnitude line 567
  63. theorem OAI.DFVSGames.Integration.AddressTupleBudget.queryWords_lt_radix line 583
  64. theorem OAI.DFVSGames.Integration.AddressTupleBudget.queryWords_encoded_length_le_magnitude line 596
  65. theorem OAI.DFVSGames.Integration.AddressTupleBudget.queryWords_digits_le_magnitude line 611
  66. theorem OAI.DFVSGames.Integration.AddressTupleBudget.selected_values_bound line 626
  67. def OAI.DFVSGames.Integration.AddressTupleBudget.rowPolynomial line 650
  68. theorem OAI.DFVSGames.Integration.AddressTupleBudget.eval_sum_constant_inline_AddressTupleBudget line 655
  69. theorem OAI.DFVSGames.Integration.AddressTupleBudget.selected_polynomial_eval line 664
  70. theorem OAI.DFVSGames.Integration.AddressTupleBudget.rows_budget_le line 675
  71. theorem OAI.DFVSGames.Integration.AddressTupleBudget.physicalField_le line 697
  72. theorem OAI.DFVSGames.Integration.AddressTupleBudget.lengthSum_le_of_mem_inline_AddressTupleBudget line 710
  73. theorem OAI.DFVSGames.Integration.AddressTupleBudget.cleanup_budget_le line 723
  74. def OAI.DFVSGames.Integration.AddressTupleBudget.timePolynomial line 745
  75. theorem OAI.DFVSGames.Integration.AddressTupleBudget.timePolynomial_eval line 751
  76. theorem OAI.DFVSGames.Integration.AddressTupleBudget.budget_le_timePolynomial line 757
  77. def OAI.DFVSGames.Integration.AddressTuplePolynomial.run_actual line 786
  78. theorem OAI.DFVSGames.Integration.AddressTuplePolynomial.trace_actual line 813